[K-Bug] The LLVM backend ignores rule priorities

[virgil-serbanuta]

What component is the issue in?

llvm-backend

Which command

• kompile
• kast
• krun
• kprove
• kprovex
• ksearch

What K Version?

v7.1.164-0-g459fdd7b84

Operating System

Linux

K Definitions (If Possible)

a.k:

module A
  imports K-EQUAL-SYNTAX

  syntax Stuff ::= "a" | "b" | "c"

  rule A:Stuff => b requires A ==K a [priority(10)]
  rule a => c

endmodule

Steps to Reproduce

use this a.in file:

a

Then, kompile a.k && krun a.in produces

<k>
  c ~> .K
</k>

This is wrong, it should have produced b instead of c.

A few more notes:
Commenting out rule a => c produces b as a result. Removing the requires clause from rule A:Stuff => b requires A ==K a makes the backend enter an infinite loop. Replacing the same rule with rule a => b, while keeping the priority produces the expected result.

Expected Results

The command above should have produced this (both in the main case described above and in the infinite loop one):

<k>
  b ~> .K
</k>