[K-Bug] Broken condition for heating rules with result

[virgil-serbanuta]

What component is the issue in?

Front-End

Which command

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

What K Version?

v7.1.164-0-g459fdd7b84

Operating System

Linux

K Definitions (If Possible)

module A
  imports BOOL

  syntax KResult

  syntax Stuff ::= "a" | "b" | "c"
  syntax KItem ::= thing(Stuff, Stuff)  [seqstrict, result(MyResult)]

  rule thing(c, c) => .K

  rule b => c
  rule a => c

  syntax Bool ::= isMyResult(K)  [function, total, symbol(isMyResult)]
  rule isMyResult(_) => false  [owise]
  rule isMyResult(c) => true


endmodule

Steps to Reproduce

echo "thing(a, b)" > a.in
kompile a.k
krun a.in

Note that execution stops without heating the second argument of "thing". As far as I can tell, this happens because the second heating rule (the one for "b") requires that the first argument is KResult instead of MyResult.

Expected Results

The second argument of "thing" should be heated, then evaluated to "c" and put back, then "thing(c, c)" should be rewritten to ".K". That is, the end result should be:

<k>
  .K
</k>