Regression in the `implies` endpoint of `booster-dev`

[tothtamas28]

Related:

• runtimeverification/evm-semantics#2483

K version: v7.1.3

From the kevm-pyk directory of runtimeverification/evm-semantics:

$ make test-integration PYTEST_ARGS='-n0 -k benchmarks/storagevar02-overflow-spec.k --use-booster-dev --bug-report'

Bug report: bug-report.zip

In order to produce the bug report I had to apply a patch to pyk:

• Make JSON RPC request ID-s random. For some reason, multiple requests and repsonses got the same file path in the archive, so half of them were not written successfully. Will have to debug this properly.

Once fixed, the test (tests/specs/benchmarks/storagevar02-overflow-spec.k) should be removed from the failing list: https://github.com/runtimeverification/evm-semantics/blob/master/tests/failing-symbolic.haskell-booster-dev

[goodlyrottenapple]

Looking into the bug report, this looks like an issue with map matching. We may need to call simplify on the inputs in this case.

{"error":"match remainder: [ ( Map:update(VarS:SortMap{}, \"0\", \"0\")\n, Map:update(\n    VarS:SortMap{},\n    \"0\",\n    chop(_)_WORD_Int_Int(_+Int_(lookup(VarS:SortMap{}, \"0\"), \"1\"))\n) )\n, ( \"\\NUL\\NUL\\NUL\\NUL\\NUL\\NUL\\NUL\\NUL\\NUL\\NUL\\NUL\\NUL\\NUL\\NUL\\NUL\\NUL...truncated\"\n, buf(\"32\", chop(_)_WORD_Int_Int(_+Int_(lookup(VarS:SortMap{}, \"0\"), \"1\"))) ) ]"},"message":"Implication check error"}