[PARKED] Use uninterpreted functions for 2-phase solving approach

cli/cli.hs

@@ -102,6 +102,7 @@ data CommonOptions = CommonOptions
   , cacheDir      ::Maybe String
   , earlyAbort    ::Bool
   , mergeMaxBudget :: Int
+  , abstractArith ::Bool
   }
 
 commonOptions :: Parser CommonOptions
@@ -133,6 +134,7 @@ commonOptions = CommonOptions
   <*> (optional $ strOption $ long "cache-dir" <> help "Directory to save and load RPC cache")
   <*> (switch $  long "early-abort" <> help "Stop exploration immediately upon finding the first counterexample")
   <*> (option auto $ long "merge-max-budget" <> showDefault <> value 100 <> help "Max instructions for speculative merge exploration during path merging")
+  <*> (switch $  long "abstract-arith" <> help "Use uninterpreted functions for div/mod in SMT queries (Halmos-style two-phase solving)")
 
 data CommonExecOptions = CommonExecOptions
   { address       ::Maybe Addr
@@ -377,6 +379,7 @@ main = do
         , onlyDeployed = cOpts.onlyDeployed
         , earlyAbort = cOpts.earlyAbort
         , mergeMaxBudget = cOpts.mergeMaxBudget
+        , abstractArith = cOpts.abstractArith
         } }
 
 

hevm.cabal

@@ -98,6 +98,7 @@ library
     EVM.Dapp,
     EVM.Expr,
     EVM.SMT,
+    EVM.SMT.DivModEncoding,
     EVM.Solvers,
     EVM.Exec,
     EVM.Format,
@@ -270,7 +271,6 @@ common test-common
     ghc-options: -threaded -with-rtsopts=-N
   build-depends:
     test-utils,
-    vector,
   other-modules:
     EVM.Test.Utils
     EVM.Test.BlockchainTests
@@ -303,6 +303,7 @@ test-suite test
     quickcheck-instances,
     regex,
     tasty-quickcheck,
+    vector,
 
 -- these tests require network access so we split them into a separate test
 -- suite to make it easy to skip them when running nix-build

src/EVM/Effects.hs

@@ -48,6 +48,7 @@ data Config = Config
   , onlyDeployed     :: Bool
   , earlyAbort       :: Bool
   , mergeMaxBudget   :: Int        -- ^ Max instructions for speculative merge exploration
+  , abstractArith    :: Bool
   }
   deriving (Show, Eq)
 
@@ -69,6 +70,7 @@ defaultConfig = Config
   , onlyDeployed = False
   , earlyAbort = False
   , mergeMaxBudget = 100
+  , abstractArith = False
   }
 
 -- Write to the console