Add test to expose the bug

ethereum · Sep 26, 2024 · 4833abb · 4833abb
1 parent cf9fb24
commit 4833abb
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/test/test.hs b/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