diff --git a/test/test.hs b/test/test.hs index 60cc6da69..09364e423 100644 --- 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 {