[Bug] [kprovex] - Failed encoding for anonymous variables

[ehildenb]

K Version

$ kompile --version
K version:    v5.2.13-3-g8882f5f46f-dirty
Build date:   Sat Nov 20 13:00:07 UTC 2021

Only differences with 5.2.13 are to pyk library, should not affect this bug.

Description

The output of the Haskell backend contains munged Kore variable names, instead of the proper unmunged name. Moreover, it looks like the Kore variable name that is generated is actually incorrect. This is either a problem in encoding variable names to Kore, or decoding them back. My guess would be on encoding, because the munged variable name is not even valid Kore variable name as far as I can tell.

Input Files

File test.k:

requires "domains.md"

module TEST

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

    syntax Foo ::= "a" | "b" | "c"
 // ------------------------------
    rule <k> a => b ... </k>
    rule <k> b => c ... </k>

endmodule

module TEST-SPEC
    imports TEST 

    claim <k> _V_9:Foo => . ... </k>

endmodule

Reproduction Steps

$ kompile test.k --backend haskell --main-module TEST --syntax-module TEST

$ kprovex test.k --spec-module TEST-SPEC
kore-exec: [176346] Warning (WarnStuckClaimState):
    (InfoReachability) while checking the implication:
    The claim cannot be rewritten further, and the claimed implication is not valid. /home/dev/src/k/test.k:17:11-17:37
  #Not ( {
    'UndsVUnds'9
  #Equals
    a
  } )
#And
  #Not ( {
    'UndsVUnds'9
  #Equals
    b
  } )
#And
  <k>
    'UndsVUnds'9:Foo ~> _DotVar1 ~> .
  </k>

Notice the variable 'UndsVUnds'9 in the K output, which should be _V_9. Also note that the correct munging of _V_9 should be 'Unds'V'Unds'9 (note the extra '), I believe.

Expected Behavior

The variable _V_9 is correctly munged/unmunged to Kore.

  #Not ( {
    _V_9
  #Equals
    a
  } )
#And
  #Not ( {
    _V_9
  #Equals
    b
  } )
#And
  <k>
    _V_9:Foo ~> _DotVar1 ~> .
  </k>