[K-Bug] Broken MInt literal parsing

[virgil-serbanuta]

What component is the issue in?

None

Which command

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

What K Version?

v7.1.104-0-g34892bf1cc

Operating System

Linux

K Definitions (If Possible)

module A-SYNTAX
imports INT
imports MINT

syntax MInt{64}
syntax A ::= a(Int, MInt{64})

endmodule

module A
imports A-SYNTAX
syntax A ::= b(MInt{64}, MInt{64}, MInt{64})

rule a(I, M) => b(Int2MInt(I), M, 100p64)

configuration <k> $PGM:A </k>

endmodule

Steps to Reproduce

kompile a.k
krun -cPGM='a(100, 100p64)'

Note that the result is

<k>
  b ( 100p64 , 6p64 , 100p64 ) ~> .K
</k>

i.e., 100p64 in the input was parsed, for some reason as 6p64. Note that 100p64 is parsed properly in the k file. Also, a simple kast call parses the value properly:

$ kast -e 'a(100,100p64)'
`a(_,_)_A-SYNTAX_A_Int_MInt`(#token("100","Int"),#token("100p64","MInt{64}"))

Expected Results

b ( 100p64 , 100p64 , 100p64 ) ~> .K