Merge pull request #569 from ethereum/check-equivalence-bug

Add test to expose a bug in our checking of Expr equivalence for CopySlice

test/test.hs

@@ -536,6 +536,12 @@ tests = testGroup "hevm"
           b = Expr.simplify a
         ret <- checkEquiv a b
         assertBoolM "must be equivalent" ret
+    , ignoreTest $ test "read-beyond-bound (negative-test)" $ do
+      let
+        e1 = CopySlice (Lit 1) (Lit 0) (Lit 2) (ConcreteBuf "a") (ConcreteBuf "")
+        e2 = ConcreteBuf "Definitely not the same!"
+      equal <- checkEquiv e1 e2
+      assertBoolM "Should not be equivalent!" $ not equal
     ]
   -- These tests fuzz the simplifier by generating a random expression,
   -- applying some simplification rules, and then using the smt encoding to