Merge pull request #453 from ethereum/fix-cvc5-incremental

Fix cvc5 incremental use
ethereum · Feb 20, 2024 · ad2e70e · ad2e70e
2 parents 9dc261e + de6ba30
commit ad2e70e
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 0 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -36,6 +36,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 - Traces now correctly perform source mapping to display contract details
 - Event traces now correctly display indexed arguments and argument names
 - JSON reading of foundry JSONs was dependent on locale and did not work with many locales.
+- CVC5 needs `--incremental` flag to work properly in abstraction-refinement mode
 
 ## [0.52.0] - 2023-10-26
 

diff --git a/src/EVM/Solvers.hs b/src/EVM/Solvers.hs
@@ -269,6 +269,7 @@ solverArgs solver timeout = case solver of
     , "--produce-models"
     , "--print-success"
     , "--interactive"
+    , "--incremental"
     , "--tlimit-per=" <> mkTimeout timeout
     ]
   Custom _ -> []