More

ethereum · Feb 13, 2025 · c45ddbf · c45ddbf
1 parent 1dd727e
commit c45ddbf
Showing 1 changed file with 10 additions and 4 deletions.
diff --git a/test/test.hs b/test/test.hs
@@ -2394,7 +2394,7 @@ tests = testGroup "hevm"
       assertEqualM "number of counterexamples" 2 numCexes
       assertEqualM "number of errors" 1 numErrs
       assertEqualM "number of qed-s" 0 numQeds
-    , testCase "call-symbolic-reent" $ do
+    , testCase "call-symbolic-noreent" $ do
       let conf = testEnv.config {promiseNoReent = True}
       let myTestEnv :: Env = (testEnv :: Env) {config = conf :: Config}
       runEnv myTestEnv $ do
@@ -2409,9 +2409,15 @@ tests = testGroup "hevm"
           }
           |]
         let sig = Just (Sig "checkval(address,uint256,uint256)" [AbiAddressType, AbiUIntType 256, AbiUIntType 256])
-        (expr, _) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
-        assertBoolM "The expression MUST be partial" $ Prelude.not $ Expr.containsNode isPartial expr
-      , test "call-symbolic-noreent" $ do
+        (expr, ret) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
+        assertBoolM "The expression MUST NOT be partial" $ Prelude.not $ Expr.containsNode isPartial expr
+        let numCexes = sum $ map (fromEnum . isCex) ret
+        let numErrs = sum $ map (fromEnum . isError) ret
+        let numQeds = sum $ map (fromEnum . isQed) ret
+        assertEqualM "number of counterexamples" 2 numCexes
+        assertEqualM "number of errors" 0 numErrs
+        assertEqualM "number of qed-s" 0 numQeds
+      , test "call-symbolic-reent" $ do
         Just c <- solcRuntime "C"
           [i|
           contract C {