Crash on KEVM proof test overflow00-nooverflow-spec.k

[ehildenb]

On KEVM commit 6937f1eb, running make build-haskell, and modifying tests/specs/benchmarks/overflow00-nooverflow-spec.k like such (which seems an innocuous and positive change):

diff --git a/tests/specs/benchmarks/overflow00-nooverflow-spec.k b/tests/specs/benchmarks/overflow00-nooverflow-spec.k
index 45ac5a22..fa50dc69 100644
--- a/tests/specs/benchmarks/overflow00-nooverflow-spec.k
+++ b/tests/specs/benchmarks/overflow00-nooverflow-spec.k
@@ -121,7 +121,7 @@ _
 
 andBool #rangeUInt(256, CONTRACT_BAL)
 andBool #rangeUInt(256, CALLEE_BAL) andBool #range(0 <= CD < 1024)
-andBool #rangeAddress(MSG_SENDER) andBool #range(0 <= A0 < 2 ^Int 256 -Int 1)
+andBool #rangeAddress(MSG_SENDER) andBool #rangeUInt(256, A0 +Int 1)
     ensures true

and then make tests/specs/benchmarks/overflow00-nooverflow-spec.k TEST_SYMBOLIC_BACKEND=haskell, results in a crash:

kore-exec: [2020-07-12 00:29:24.896385891] Error (ErrorException):
    Assertion failed
    CallStack (from HasCallStack):
      assert, called at src/Kore/Internal/Substitution.hs:434:11 in kore-0.24.0.0-JGugWVddYonHzQ725yhKpC:Kore.Internal.Substitution
      unsafeWrap, called at src/Kore/Internal/Condition.hs:187:11 in kore-0.24.0.0-JGugWVddYonHzQ725yhKpC:Kore.Internal.Condition

Generated bug report attached.
kevm-bug.tar.gz

[ttuegel]

Fixed in #1997.