Merge pull request #544 from ethereum/simplification-tests

Add tests for detecting unsatisfiability
ethereum · Aug 27, 2024 · d02cc99 · d02cc99
2 parents 0163d8f + c33e29f
commit d02cc99
Showing 1 changed file with 10 additions and 0 deletions.
diff --git a/test/test.hs b/test/test.hs
@@ -685,6 +685,16 @@ tests = testGroup "hevm"
           t = [PEq (Var "x") (Lit 1), POr (PEq (Var "x") (Lit 2)) (PEq (Var "x") (Lit 0)), PEq (Var "y") (Lit 2)]
           cannotBeSat = Expr.isUnsat t
         assertEqualM "Must be equal" cannotBeSat True
+    , ignoreTest $ test "disequality-and-equality" $ do
+        let
+          t = [PNeg (PEq (Lit 1) (Var "arg1")), PEq (Lit 1) (Var "arg1")]
+          cannotBeSat = Expr.isUnsat t
+        assertEqualM "Must be equal" cannotBeSat True
+    , test "equality-and-disequality" $ do
+        let
+          t = [PEq (Lit 1) (Var "arg1"), PNeg (PEq (Lit 1) (Var "arg1"))]
+          cannotBeSat = Expr.isUnsat t
+        assertEqualM "Must be equal" cannotBeSat True
   ]
   , testGroup "simpProp-concrete-tests" [
       test "simpProp-concrete-trues" $ do