diff --git a/test/test.hs b/test/test.hs index 130c712e7..f4500e02d 100644 --- 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