[K-Bug] LLVM Backend crash when comparing MInt

[virgil-serbanuta]

What component is the issue in?

llvm-backend

Which command

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

What K Version?

v7.1.217-0-gf236685fdd

Operating System

Linux

K Definitions (If Possible)

module A
  imports BOOL
  imports INT
  imports K-EQUAL-SYNTAX
  imports MINT

  syntax MInt{8}

  syntax KItem ::= "a" | b(MInt{8}, MInt{8}) | c(Bool)

  rule a => b(Int2MInt(2), Int2MInt(2))
  rule b(X, Y) => c(X ==K Y)
endmodule

Steps to Reproduce

kompile a.k
echo "a" >> a.in
krun a.in

This crashes with

.../lib/kframework/k-util.sh: line 114: 399174 Aborted                 (core dumped) "$@"
[Error] krun: ./a-kompiled/interpreter 

GDB has this in the stack trace:

#4  0x00007ffff70287f3 in __GI_abort () at ./stdlib/abort.c:79
#5  0x0000555555683f4e in hook_KEQUAL_eq (arg1=0x7e00000001a8, arg2=0x7e00000001d0)
    at /mnt/data/runtime-verification/k/llvm-backend/src/main/native/llvm-backend/runtime/collections/kelemle.cpp:161
#6  0x0000555555683eb9 in hook_KEQUAL_eq (arg1=0x7e00000001b8, arg2=0x7e00000001e0)
    at /mnt/data/runtime-verification/k/llvm-backend/src/main/native/llvm-backend/runtime/collections/kelemle.cpp:112
#7  0x00005555555c5972 in k_step ()

This is the code that seems to be crashing:
https://github.com/runtimeverification/llvm-backend/blob/4203a45110504a6661ca086816e28dafa9e7ac54/runtime/collections/kelemle.cpp#L156-L166

Expected Results

Not crashing. The <k> cell should contain c(true).