Timeout -> Unknown, as it's actually more expressive

cli/cli.hs

@@ -260,8 +260,8 @@ equivalence cmd = do
     case any isCex res of
       False -> liftIO $ do
         putStrLn "No discrepancies found"
-        when (any isTimeout res || any isError res) $ do
-          putStrLn $ "But " <> (show $ length $ filter isTimeout res) <> " timeout(s) and/or " <> (show $ length $ filter isError res) <> " error(s)/incomplete execution(s) occurred"
+        when (any isUnknown res || any isError res) $ do
+          putStrLn $ "But " <> (show $ length $ filter isUnknown res) <> " timeout(s) and/or " <> (show $ length $ filter isError res) <> " error(s)/incomplete execution(s) occurred"
           exitFailure
       True -> liftIO $ do
         let cexs = mapMaybe getCex res
@@ -345,7 +345,7 @@ assert cmd = do
         showExtras solvers cmd calldata expr
       _ -> do
         let cexs = snd <$> mapMaybe getCex res
-            timeouts = mapMaybe getTimeout res
+            smtUnknowns = mapMaybe getUnknown res
             counterexamples
               | null cexs = []
               | otherwise =
@@ -354,15 +354,15 @@ assert cmd = do
                  , ""
                  ] <> fmap (formatCex (fst calldata) Nothing) cexs
             unknowns
-              | null timeouts = []
+              | null smtUnknowns = []
               | otherwise =
                  [ ""
                  , "Could not determine reachability of the following end state(s):"
                  , ""
-                 ] <> fmap (formatExpr) timeouts
+                 ] <> fmap (formatExpr) smtUnknowns
         liftIO $ T.putStrLn $ T.unlines (counterexamples <> unknowns)
         showExtras solvers cmd calldata expr
-        liftIO $ exitFailure
+        liftIO exitFailure
 
 showExtras :: App m => SolverGroup -> Command Options.Unwrapped -> (Expr Buf, [Prop]) -> Expr End -> m ()
 showExtras solvers cmd calldata expr = do

src/EVM/Solvers.hs

@@ -65,7 +65,7 @@ data Task = Task
 data CheckSatResult
   = Sat SMTCex
   | Unsat
-  | Timeout String
+  | Unknown String
   | Error String
   deriving (Show, Eq)
 
@@ -144,8 +144,8 @@ withSolvers solver count threads timeout cont = do
                 res <- do
                     case sat of
                       "unsat" -> pure Unsat
-                      "timeout" -> pure $ Timeout "Result timeout by SMT solver"
-                      "unknown" -> pure $ Timeout "Result unknown by SMT solver"
+                      "timeout" -> pure $ Unknown "Result timeout by SMT solver"
+                      "unknown" -> pure $ Unknown "Result unknown by SMT solver"
                       "sat" -> if null refineEqs then Sat <$> getModel inst cexvars
                                else do
                                     let refinedSMT2 = SMT2 refineEqs mempty mempty (ps <> refps)
@@ -154,8 +154,8 @@ withSolvers solver count threads timeout cont = do
                                     sat2 <- sendLine inst "(check-sat)"
                                     case sat2 of
                                       "unsat" -> pure Unsat
-                                      "timeout" -> pure $ Timeout "Result timeout by SMT solver"
-                                      "unknown" -> pure $ Timeout "Result unknown by SMT solver"
+                                      "timeout" -> pure $ Unknown "Result timeout by SMT solver"
+                                      "unknown" -> pure $ Unknown "Result unknown by SMT solver"
                                       "sat" -> Sat <$> getModel inst cexvars
                                       _ -> pure . Error $ "Unable to parse solver output: " <> T.unpack sat2
                       _ -> pure . Error $ "Unable to parse SMT solver output: " <> T.unpack sat

src/EVM/SymExec.hs

@@ -56,14 +56,14 @@ data LoopHeuristic
   | StackBased
   deriving (Eq, Show, Read, ParseField, ParseFields, ParseRecord, Generic)
 
-data ProofResult a b c d = Qed a | Cex b | Timeout c | Error d
+data ProofResult a b c d = Qed a | Cex b | Unknown c | Error d
   deriving (Show, Eq)
 type VerifyResult = ProofResult () (Expr End, SMTCex) (Expr End) String
 type EquivResult = ProofResult () (SMTCex) () String
 
-isTimeout :: ProofResult a b c d -> Bool
-isTimeout (EVM.SymExec.Timeout _) = True
-isTimeout _ = False
+isUnknown :: ProofResult a b c d -> Bool
+isUnknown (EVM.SymExec.Unknown _) = True
+isUnknown _ = False
 
 isError :: ProofResult a b c d -> Bool
 isError (EVM.SymExec.Error _) = True
@@ -633,7 +633,7 @@ verify solvers opts preState maybepost = do
     toVRes :: (CheckSatResult, Expr End) -> VerifyResult
     toVRes (res, leaf) = case res of
       Sat model -> Cex (leaf, expandCex preState model)
-      EVM.Solvers.Timeout _ -> EVM.SymExec.Timeout leaf
+      EVM.Solvers.Unknown _ -> EVM.SymExec.Unknown leaf
       EVM.Solvers.Error e -> EVM.SymExec.Error e
       Unsat -> Qed ()
 
@@ -746,7 +746,7 @@ equivalenceCheck' solvers branchesA branchesB = do
               -- potential race, but it doesn't matter for correctness
               atomically $ readTVar knownUnsat >>= writeTVar knownUnsat . (props :)
               pure (Qed (), False)
-        (_, EVM.Solvers.Timeout _) -> pure (EVM.SymExec.Timeout (), False)
+        (_, EVM.Solvers.Unknown _) -> pure (EVM.SymExec.Unknown (), False)
         (_, EVM.Solvers.Error txt) -> pure (EVM.SymExec.Error txt, False)
 
     -- Allows us to run it in parallel. Note that this (seems to) run it
@@ -842,7 +842,7 @@ showModel cd (expr, res) = do
       putStrLn ""
       putStrLn "--- Branch ---"
       putStrLn $ "Error during SMT solving, cannot check branch " <> e
-    EVM.Solvers.Timeout reason -> do
+    EVM.Solvers.Unknown reason -> do
       putStrLn ""
       putStrLn "--- Branch ---"
       putStrLn $ "Unable to produce a model for the following end state due to '" <> reason <> "' :"
@@ -1056,6 +1056,6 @@ getCex :: ProofResult a b c d -> Maybe b
 getCex (Cex c) = Just c
 getCex _ = Nothing
 
-getTimeout :: ProofResult a b c d-> Maybe c
-getTimeout (EVM.SymExec.Timeout c) = Just c
-getTimeout _ = Nothing
+getUnknown :: ProofResult a b c d-> Maybe c
+getUnknown (EVM.SymExec.Unknown c) = Just c
+getUnknown _ = Nothing

test/test.hs

@@ -3719,7 +3719,7 @@ checkEquivBase mkprop l r expect = do
          Unsat -> Just True
          Sat _ -> Just False
          EVM.Solvers.Error _ -> Just (not expect)
-         EVM.Solvers.Timeout _ -> Nothing
+         EVM.Solvers.Unknown _ -> Nothing
      when (ret == Just (not expect)) $ print res
      pure ret