Merge pull request #587 from ethereum/timeout-option-equiv

Respect option for timeout in equivalence checking
ethereum · Oct 7, 2024 · 016d063 · 016d063
2 parents 999a794 + 7fdfde7
commit 016d063
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -54,6 +54,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Fixed a bug in our SMT encoding of reading multiple consecutive bytes from concrete index
 - Fixed bug in SMT encoding that caused empty and all-zero byte arrays to be considered equal
   and hence lead to false negatives through trivially UNSAT SMT expressions
+- Respect --smt-timeout in equivalence checking
 
 ## [0.53.0] - 2024-02-23
 

diff --git a/cli/cli.hs b/cli/cli.hs
@@ -252,7 +252,7 @@ equivalence cmd = do
   solver <- liftIO $ getSolver cmd
   cores <- liftIO $ unsafeInto <$> getNumProcessors
   let solverCount = fromMaybe cores cmd.numSolvers
-  withSolvers solver solverCount Nothing $ \s -> do
+  withSolvers solver solverCount cmd.smttimeout $ \s -> do
     res <- equivalenceCheck s bytecodeA bytecodeB veriOpts calldata
     case any isCex res of
       False -> liftIO $ do