From 7fdfde712557bc864e778b8ab3a8014862807f93 Mon Sep 17 00:00:00 2001
From: Mate Soos <mate.soos@ethereum.org>
Date: Mon, 7 Oct 2024 17:40:30 +0200
Subject: [PATCH] Respect option for timeout in equivalence checking

---
 CHANGELOG.md | 1 +
 cli/cli.hs   | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index e33ca03b1..459a7a235 100644
--- 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
index 3290e73af..6a79f82f8 100644
--- 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