diff --git a/cli/cli.hs b/cli/cli.hs
index f9260a151..5990e04d4 100644
--- a/cli/cli.hs
+++ b/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
         } }
 
 
diff --git a/hevm.cabal b/hevm.cabal
index 1069c3784..a489e328d 100644
--- a/hevm.cabal
+++ b/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
diff --git a/src/EVM/Effects.hs b/src/EVM/Effects.hs
index 8360ad897..49db60569 100644
--- a/src/EVM/Effects.hs
+++ b/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
diff --git a/src/EVM/SMT.hs b/src/EVM/SMT.hs
index cfd5ce948..6c4c0afee 100644
--- a/src/EVM/SMT.hs
+++ b/src/EVM/SMT.hs
@@ -6,17 +6,22 @@ module EVM.SMT
 (
   module EVM.SMT.Types,
   module EVM.SMT.SMTLIB,
+  module EVM.SMT.DivModEncoding,
 
   collapse,
   getVar,
   formatSMT2,
   declareIntermediates,
   assertProps,
-  exprToSMT,
+  assertPropsAbstract,
+  assertPropsHelperWith,
+  decompose,
+  exprToSMTWith,
   encodeConcreteStore,
+  sp,
   zero,
   one,
-  propToSMT,
+  propToSMTWith,
   parseVar,
   parseEAddr,
   parseBlockCtx,
@@ -25,7 +30,8 @@ module EVM.SMT
   getVars,
   queryMaxReads,
   getBufs,
-  getStore
+  getStore,
+  wordAsBV
 ) where
 
 import Prelude hiding (LT, GT, Foldable(..))
@@ -66,6 +72,7 @@ import EVM.Types
 import EVM.Effects
 import EVM.SMT.Types
 import EVM.SMT.SMTLIB
+import EVM.SMT.DivModEncoding
 
 
 -- ** Encoding ** ----------------------------------------------------------------------------------
@@ -93,7 +100,10 @@ formatSMT2 (SMT2 (SMTScript entries) _ ps) = expr <> smt2
 
 -- | Reads all intermediate variables from the builder state and produces SMT declaring them as constants
 declareIntermediates :: BufEnv -> StoreEnv -> Err [SMTEntry]
-declareIntermediates bufs stores = do
+declareIntermediates = declareIntermediatesWith ConcreteDivMod
+
+declareIntermediatesWith :: DivModEncoding -> BufEnv -> StoreEnv -> Err [SMTEntry]
+declareIntermediatesWith enc bufs stores = do
   let encSs = Map.mapWithKey encodeStore stores
       encBs = Map.mapWithKey encodeBuf bufs
   snippets <- sequence $ Map.elems $ encSs <> encBs
@@ -101,46 +111,55 @@ declareIntermediates bufs stores = do
   pure $ (SMTComment "intermediate buffers & stores") : decls
   where
     encodeBuf n expr = do
-      buf <- exprToSMT expr
+      buf <- exprToSMTWith enc expr
       bufLen <- encodeBufLen n expr
       pure [SMTCommand ("(define-fun buf" <> (Data.Text.Lazy.Builder.Int.decimal n) <> "() Buf " <> buf <> ")\n"), bufLen]
     encodeBufLen n expr = do
-      bufLen <- exprToSMT (bufLengthEnv bufs True expr)
+      bufLen <- exprToSMTWith enc (bufLengthEnv bufs True expr)
       pure $ SMTCommand ("(define-fun buf" <> (Data.Text.Lazy.Builder.Int.decimal n) <>"_length () (_ BitVec 256) " <> bufLen <> ")")
     encodeStore n expr = do
-      storage <- exprToSMT expr
+      storage <- exprToSMTWith enc expr
       pure [SMTCommand ("(define-fun store" <> (Data.Text.Lazy.Builder.Int.decimal n) <> " () Storage " <> storage <> ")")]
 
+decompose :: Config -> [Prop] -> [Prop]
+decompose conf props = if conf.decomposeStorage && safeExprs && safeProps
+                    then fromMaybe props (mapM (mapPropM Expr.decomposeStorage) props)
+                    else props
+  where
+    -- All in these lists must be a `Just ()` or we cannot decompose
+    safeExprs = all (isJust . mapPropM_ Expr.safeToDecompose) props
+    safeProps = all Expr.safeToDecomposeProp props
+
 -- simplify to rewrite sload/sstore combos
 -- notice: it is VERY important not to concretize early, because Keccak assumptions
 --         need unconcretized Props
 assertProps :: Config -> [Prop] -> Err SMT2
 assertProps conf ps =
-  if not conf.simp then assertPropsHelper False ps
-  else assertPropsHelper True (decompose ps)
-  where
-    decompose :: [Prop] -> [Prop]
-    decompose props = if conf.decomposeStorage && safeExprs && safeProps
-                      then fromMaybe props (mapM (mapPropM Expr.decomposeStorage) props)
-                      else props
-      where
-        -- All in these lists must be a `Just ()` or we cannot decompose
-        safeExprs = all (isJust . mapPropM_ Expr.safeToDecompose) props
-        safeProps = all Expr.safeToDecomposeProp props
-
+  if not conf.simp then assertPropsHelperWith ConcreteDivMod False [] ps
+  else assertPropsHelperWith ConcreteDivMod True [] (decompose conf ps)
+
+-- | Assert props with abstract div/mod (uninterpreted functions + encoding constraints).
+assertPropsAbstract :: Config -> [Prop] -> Err SMT2
+assertPropsAbstract conf ps = do
+  let mkBase s = assertPropsHelperWith AbstractDivMod s divModAbstractDecls
+  base <- if not conf.simp then mkBase False ps
+          else mkBase True (decompose conf ps)
+  shiftBounds <- divModEncoding (exprToSMTWith AbstractDivMod) ps
+  pure $ base <> SMT2 (SMTScript shiftBounds) mempty mempty
 
 -- Note: we need a version that does NOT call simplify,
 -- because we make use of it to verify the correctness of our simplification
 -- passes through property-based testing.
-assertPropsHelper :: Bool -> [Prop]  -> Err SMT2
-assertPropsHelper simp psPreConc = do
- encs <- mapM propToSMT psElim
- intermediates <- declareIntermediates bufs stores
+assertPropsHelperWith :: DivModEncoding -> Bool -> [SMTEntry] -> [Prop]  -> Err SMT2
+assertPropsHelperWith divEnc simp extraDecls psPreConc = do
+ encs <- mapM (propToSMTWith divEnc) psElim
+ intermediates <- declareIntermediatesWith divEnc bufs stores
  readAssumes' <- readAssumes
  keccakAssertions' <- keccakAssertions
  frameCtxs <- (declareFrameContext . nubOrd $ foldl' (<>) [] frameCtx)
  blockCtxs <- (declareBlockContext . nubOrd $ foldl' (<>) [] blockCtx)
  pure $ prelude
+  <> SMT2 (SMTScript extraDecls) mempty mempty
   <> SMT2 (SMTScript (declareAbstractStores abstractStores)) mempty mempty
   <> declareConstrainAddrs addresses
   <> (declareBufs toDeclarePsElim bufs stores)
@@ -163,9 +182,9 @@ assertPropsHelper simp psPreConc = do
 
     -- vars, frames, and block contexts in need of declaration
     allVars = fmap referencedVars toDeclarePsElim <> fmap referencedVars bufVals <> fmap referencedVars storeVals
-    frameCtx = fmap referencedFrameContext toDeclarePsElim <> fmap referencedFrameContext bufVals <> fmap referencedFrameContext storeVals
+    frameCtx = fmap (referencedFrameContext divEnc) toDeclarePsElim <> fmap (referencedFrameContext divEnc) bufVals <> fmap (referencedFrameContext divEnc) storeVals
     blockCtx = fmap referencedBlockContext toDeclarePsElim <> fmap referencedBlockContext bufVals <> fmap referencedBlockContext storeVals
-    gasOrder = enforceGasOrder psPreConc
+    gasOrder = enforceGasOrder divEnc psPreConc
 
     -- Buf, Storage, etc. declarations needed
     bufVals = Map.elems bufs
@@ -181,13 +200,13 @@ assertPropsHelper simp psPreConc = do
     keccAssump = keccakAssumptions $ Set.toList allKeccaks
     keccComp = [(PEq (Lit l) (Keccak buf)) | (buf, l) <- Set.toList concreteKecc]
     keccakAssertions = do
-      assumps <- mapM assertSMT keccAssump
-      comps <- mapM assertSMT keccComp
+      assumps <- mapM (assertSMTWith divEnc) keccAssump
+      comps <- mapM (assertSMTWith divEnc) keccComp
       pure $ ((SMTComment "keccak assumptions") : assumps) <> ((SMTComment "keccak computations") : comps)
 
     -- assert that reads beyond size of buffer & storage is zero
     readAssumes = do
-      assumps <- mapM assertSMT $ assertReads psElim bufs stores
+      assumps <- mapM (assertSMTWith divEnc) $ assertReads psElim bufs stores
       pure (SMTComment "read assumptions" : assumps)
 
     cexInfo :: StorageReads -> CexVars
@@ -224,8 +243,8 @@ referencedVars expr = nubOrd $ foldTerm go [] expr
       Var s -> [fromText s]
       _ -> []
 
-referencedFrameContext :: TraversableTerm a => a -> [(Builder, [Prop])]
-referencedFrameContext expr = nubOrd $ foldTerm go [] expr
+referencedFrameContext :: DivModEncoding -> TraversableTerm a => a -> [(Builder, [Prop])]
+referencedFrameContext enc expr = nubOrd $ foldTerm go [] expr
   where
     go :: Expr a -> [(Builder, [Prop])]
     go = \case
@@ -234,6 +253,8 @@ referencedFrameContext expr = nubOrd $ foldTerm go [] expr
       o@(Gas _ _) -> [(fromRight' $ exprToSMT o, [])]
       o@(CodeHash (LitAddr _)) -> [(fromRight' $ exprToSMT o, [])]
       _ -> []
+    exprToSMT :: Expr x -> Err Builder
+    exprToSMT = exprToSMTWith enc
 
 referencedBlockContext :: TraversableTerm a => a -> [(Builder, [Prop])]
 referencedBlockContext expr = nubOrd $ foldTerm go [] expr
@@ -357,14 +378,14 @@ declareConstrainAddrs names = SMT2 (SMTScript ([SMTComment "concrete and symboli
 -- The gas is a tuple of (prefix, index). Within each prefix, the gas is strictly decreasing as the
 -- index increases. This function gets a map of Prefix -> [Int], and for each prefix,
 -- enforces the order
-enforceGasOrder :: [Prop] -> [SMTEntry]
-enforceGasOrder ps = [SMTComment "gas ordering"] <> (concatMap (uncurry order) indices)
+enforceGasOrder :: DivModEncoding -> [Prop] -> [SMTEntry]
+enforceGasOrder enc ps = [SMTComment "gas ordering"] <> (concatMap (uncurry order) indices)
   where
     order :: TS.Text -> [Int] -> [SMTEntry]
     order prefix n = consecutivePairs (nubInt n) >>= \(x, y)->
       -- The GAS instruction itself costs gas, so it's strictly decreasing
-      [SMTCommand $ "(assert (bvugt " <> fromRight' (exprToSMT (Gas prefix x)) <> " " <>
-        fromRight' ((exprToSMT (Gas prefix y))) <> "))"]
+      [SMTCommand $ "(assert (bvugt " <> fromRight' (exprToSMTWith enc (Gas prefix x)) <> " " <>
+        fromRight' ((exprToSMTWith enc (Gas prefix y))) <> "))"]
     consecutivePairs :: [Int] -> [(Int, Int)]
     consecutivePairs [] = []
     consecutivePairs l@(_:t) = zip l t
@@ -402,8 +423,11 @@ declareBlockContext names = do
     cexvars = (mempty :: CexVars){ blockContext = fmap (toLazyText . fst) names }
 
 assertSMT :: Prop -> Either String SMTEntry
-assertSMT p = do
-  p' <- propToSMT p
+assertSMT = assertSMTWith ConcreteDivMod
+
+assertSMTWith :: DivModEncoding -> Prop -> Either String SMTEntry
+assertSMTWith enc p = do
+  p' <- propToSMTWith enc p
   pure $ SMTCommand ("(assert " <> p' <> ")")
 
 wordAsBV :: forall a. Integral a => a -> Builder
@@ -412,8 +436,8 @@ wordAsBV w = "(_ bv" <> Data.Text.Lazy.Builder.Int.decimal w <> " 256)"
 byteAsBV :: Word8 -> Builder
 byteAsBV b = "(_ bv" <> Data.Text.Lazy.Builder.Int.decimal b <> " 8)"
 
-exprToSMT :: Expr a -> Err Builder
-exprToSMT = \case
+exprToSMTWith :: DivModEncoding -> Expr a -> Err Builder
+exprToSMTWith divEnc = \case
   Lit w -> pure $ wordAsBV w
   Var s -> pure $ fromText s
   GVar (BufVar n) -> pure $ fromString $ "buf" <> (show n)
@@ -423,7 +447,7 @@ exprToSMT = \case
     eight nine ten eleven twelve thirteen fourteen fifteen
     sixteen seventeen eighteen nineteen twenty twentyone twentytwo twentythree
     twentyfour twentyfive twentysix twentyseven twentyeight twentynine thirty thirtyone
-    -> concatBytes [
+    -> concatBytesWith divEnc [
         z, o, two, three, four, five, six, seven
         , eight, nine, ten, eleven, twelve, thirteen, fourteen, fifteen
         , sixteen, seventeen, eighteen, nineteen, twenty, twentyone, twentytwo, twentythree
@@ -442,7 +466,7 @@ exprToSMT = \case
         pure $ "(bvshl " <> one `sp` benc <> ")"
     _ -> case b of
       -- b is limited below, otherwise SMT query will be huge, and eventually Haskell stack overflows
-      Lit b' | b' < 1000 -> expandExp a b'
+      Lit b' | b' < 1000 -> expandExpWith divEnc a b'
       _ -> Left $ "Cannot encode symbolic exponent into SMT. Offending symbolic value: " <> show b
   Min a b -> do
     aenc <- exprToSMT a
@@ -491,9 +515,9 @@ exprToSMT = \case
   CLZ a -> op1 "clz256" a
   SEx a b -> op2 "signext" a b
   Div a b -> op2CheckZero "bvudiv" a b
-  SDiv a b -> op2CheckZero "bvsdiv" a b
+  SDiv a b -> divModOp "bvsdiv" "abst_evm_bvsdiv" a b
   Mod a b -> op2CheckZero "bvurem" a b
-  SMod a b -> op2CheckZero "bvsrem" a b
+  SMod a b -> divModOp "bvsrem" "abst_evm_bvsrem" a b
   -- NOTE: this needs to do the MUL at a higher precision, then MOD, then downcast
   MulMod a b c -> do
     aExp <- exprToSMT a
@@ -553,7 +577,7 @@ exprToSMT = \case
   ReadByte idx src -> op2 "select" src idx
 
   ConcreteBuf "" -> pure "((as const Buf) #b00000000)"
-  ConcreteBuf bs -> writeBytes bs mempty
+  ConcreteBuf bs -> writeBytesWith divEnc bs mempty
   AbstractBuf s -> pure $ fromText s
   ReadWord idx prev -> op2 "readWord" idx prev
   BufLength (AbstractBuf b) -> pure $ fromText b <> "_length"
@@ -572,10 +596,10 @@ exprToSMT = \case
   CopySlice srcIdx dstIdx size src dst -> do
     srcSMT <- exprToSMT src
     dstSMT <- exprToSMT dst
-    copySlice srcIdx dstIdx size srcSMT dstSMT
+    copySliceWith divEnc srcIdx dstIdx size srcSMT dstSMT
 
   -- we need to do a bit of processing here.
-  ConcreteStore s -> encodeConcreteStore s
+  ConcreteStore s -> encodeConcreteStore divEnc s
   AbstractStore a idx -> pure $ storeName a idx
   SStore idx val prev -> do
     encIdx  <- exprToSMT idx
@@ -589,20 +613,29 @@ exprToSMT = \case
 
   a -> internalError $ "TODO: implement: " <> show a
   where
+    exprToSMT :: Expr x -> Err Builder
+    exprToSMT = exprToSMTWith divEnc
+    op1 :: Builder -> Expr x -> Err Builder
     op1 op a = do
       enc <- exprToSMT a
       pure $ "(" <> op `sp` enc <> ")"
+    op2 :: Builder -> Expr x -> Expr y -> Err Builder
     op2 op a b = do
        aenc <- exprToSMT a
        benc <- exprToSMT b
        pure $ "(" <> op `sp` aenc `sp` benc <> ")"
+    op2CheckZero :: Builder -> Expr x -> Expr y -> Err Builder
     op2CheckZero op a b = do
       aenc <- exprToSMT a
       benc <- exprToSMT b
       pure $ "(ite (= " <> benc <> " (_ bv0 256)) (_ bv0 256) " <>  "(" <> op `sp` aenc `sp` benc <> "))"
+    divModOp :: Builder -> Builder -> Expr x -> Expr y -> Err Builder
+    divModOp concreteOp abstractOp a b = case divEnc of
+      ConcreteDivMod -> op2CheckZero concreteOp a b
+      AbstractDivMod -> op2 abstractOp a b
 
 sp :: Builder -> Builder -> Builder
-a `sp` b = a <> (fromText " ") <> b
+a `sp` b = a <> " " <> b
 
 zero :: Builder
 zero = "(_ bv0 256)"
@@ -610,8 +643,8 @@ zero = "(_ bv0 256)"
 one :: Builder
 one = "(_ bv1 256)"
 
-propToSMT :: Prop -> Err Builder
-propToSMT = \case
+propToSMTWith :: DivModEncoding -> Prop -> Err Builder
+propToSMTWith divEnc = \case
   PEq a b -> op2 "=" a b
   PLT a b -> op2 "bvult" a b
   PGT a b -> op2 "bvugt" a b
@@ -634,19 +667,18 @@ propToSMT = \case
     pure $ "(=> " <> aenc <> " " <> benc <> ")"
   PBool b -> pure $ if b then "true" else "false"
   where
+    propToSMT :: Prop -> Err Builder
+    propToSMT = propToSMTWith divEnc
+    op2 :: Builder -> Expr x -> Expr y -> Err Builder
     op2 op a b = do
-      aenc <- exprToSMT a
-      benc <- exprToSMT b
+      aenc <- exprToSMTWith divEnc a
+      benc <- exprToSMTWith divEnc b
       pure $ "(" <> op <> " " <> aenc <> " " <> benc <> ")"
 
-
-
 -- ** Helpers ** ---------------------------------------------------------------------------------
 
-
--- | Stores a region of src into dst
-copySlice :: Expr EWord -> Expr EWord -> Expr EWord -> Builder -> Builder -> Err Builder
-copySlice srcOffset dstOffset (Lit size) src dst = do
+copySliceWith :: DivModEncoding -> Expr EWord -> Expr EWord -> Expr EWord -> Builder -> Builder -> Err Builder
+copySliceWith divEnc srcOffset dstOffset (Lit size) src dst = do
   sz <- internal size
   pure $ "(let ((src " <> src <> ")) " <> sz <> ")"
   where
@@ -659,38 +691,35 @@ copySlice srcOffset dstOffset (Lit size) src dst = do
       pure $ "(store " <> child `sp` encDstOff `sp` "(select src " <> encSrcOff <> "))"
     offset :: W256 -> Expr EWord -> Err Builder
     offset o (Lit b) = pure $ wordAsBV $ o + b
-    offset o e = exprToSMT $ Expr.add (Lit o) e
-copySlice _ _ _ _ _ = Left "CopySlice with a symbolically sized region not currently implemented, cannot execute SMT solver on this query"
+    offset o e = exprToSMTWith divEnc $ Expr.add (Lit o) e
+copySliceWith _ _ _ _ _ _ = Left "CopySlice with a symbolically sized region not currently implemented, cannot execute SMT solver on this query"
 
--- | Unrolls an exponentiation into a series of multiplications
-expandExp :: Expr EWord -> W256 -> Err Builder
-expandExp base expnt
+expandExpWith :: DivModEncoding -> Expr EWord -> W256 -> Err Builder
+expandExpWith divEnc base expnt
   -- in EVM, anything (including 0) to the power of 0 is 1
   | expnt == 0 = pure one
-  | expnt == 1 = exprToSMT base
+  | expnt == 1 = exprToSMTWith divEnc base
   | otherwise = do
-    b <- exprToSMT base
-    n <- expandExp base (expnt - 1)
+    b <- exprToSMTWith divEnc base
+    n <- expandExpWith divEnc base (expnt - 1)
     pure $ "(bvmul " <> b `sp` n <> ")"
 
--- | Concatenates a list of bytes into a larger bitvector
-concatBytes :: [Expr Byte] -> Err Builder
-concatBytes bytes = do
+concatBytesWith :: DivModEncoding -> [Expr Byte] -> Err Builder
+concatBytesWith divEnc bytes = do
   case List.uncons $ reverse bytes of
     Nothing -> Left "unexpected empty bytes"
     Just (h, t) -> do
-      a2 <- exprToSMT h
+      a2 <- exprToSMTWith divEnc h
       foldM wrap a2 t
   where
     wrap :: Builder -> Expr a -> Err Builder
     wrap inner byte = do
-      byteSMT <- exprToSMT byte
+      byteSMT <- exprToSMTWith divEnc byte
       pure $ "(concat " <> byteSMT `sp` inner <> ")"
 
--- | Concatenates a list of bytes into a larger bitvector
-writeBytes :: ByteString -> Expr Buf -> Err Builder
-writeBytes bytes buf =  do
-  smtText <- exprToSMT buf
+writeBytesWith :: DivModEncoding -> ByteString -> Expr Buf -> Err Builder
+writeBytesWith divEnc bytes buf =  do
+  smtText <- exprToSMTWith divEnc buf
   let ret = BS.foldl wrap (0, smtText) bytes
   pure $ snd ret
   where
@@ -704,13 +733,13 @@ writeBytes bytes buf =  do
       where
         !idx' = idx + 1
 
-encodeConcreteStore :: Map W256 W256 -> Err Builder
-encodeConcreteStore s = foldM encodeWrite ("((as const Storage) #x0000000000000000000000000000000000000000000000000000000000000000)") (Map.toList s)
+encodeConcreteStore :: DivModEncoding -> Map W256 W256 -> Err Builder
+encodeConcreteStore enc s = foldM encodeWrite ("((as const Storage) #x0000000000000000000000000000000000000000000000000000000000000000)") (Map.toList s)
   where
     encodeWrite :: Builder -> (W256, W256) -> Err Builder
     encodeWrite prev (key, val) = do
-      encKey <- exprToSMT $ Lit key
-      encVal <- exprToSMT $ Lit val
+      encKey <- exprToSMTWith enc $ Lit key
+      encVal <- exprToSMTWith enc $ Lit val
       pure $ "(store " <> prev `sp` encKey `sp` encVal <> ")"
 
 storeName :: Expr EAddr -> Maybe W256 -> Builder
@@ -885,8 +914,8 @@ getStore getVal (StorageReads innerMap) = do
 queryValue :: ValGetter -> Expr EWord -> MaybeIO W256
 queryValue _ (Lit w) = pure w
 queryValue getVal w = do
-  -- this exprToSMT should never fail, since we have already ran the solver
-  let expr = toLazyText $ fromRight' $ exprToSMT w
+  -- this exprToSMTWith should never fail, since we have already ran the solver, in refined mode
+  let expr = toLazyText $ fromRight' $ exprToSMTWith ConcreteDivMod w
   raw <- getVal expr
   hoistMaybe $ do
     valTxt <- extractValue raw
diff --git a/src/EVM/SMT/DivModEncoding.hs b/src/EVM/SMT/DivModEncoding.hs
new file mode 100644
index 000000000..9215588bc
--- /dev/null
+++ b/src/EVM/SMT/DivModEncoding.hs
@@ -0,0 +1,216 @@
+{- | Abstract div/mobsolud encoding for two-phase SMT solving. -}
+module EVM.SMT.DivModEncoding
+  ( divModGroundTruth
+  , divModEncoding
+  , divModAbstractDecls
+  ) where
+
+import Data.Bits ((.&.), countTrailingZeros)
+import Data.Containers.ListUtils (nubOrd)
+import Data.List (groupBy, sortBy)
+import Data.Ord (comparing)
+import Data.Text.Lazy.Builder
+import qualified Data.Text.Lazy.Builder.Int
+import EVM.SMT.Types
+import EVM.Traversals
+import EVM.Types (Prop(..), EType(EWord), Err, W256, Expr, Expr(Lit), Expr(SHL))
+import EVM.Types qualified as T
+
+-- | Uninterpreted function declarations for abstract div/mod.
+divModAbstractDecls :: [SMTEntry]
+divModAbstractDecls =
+  [ SMTComment "abstract division/modulo (uninterpreted functions)"
+  , SMTCommand "(declare-fun abst_evm_bvsdiv ((_ BitVec 256) (_ BitVec 256)) (_ BitVec 256))"
+  , SMTCommand "(declare-fun abst_evm_bvsrem ((_ BitVec 256) (_ BitVec 256)) (_ BitVec 256))"
+  ]
+
+-- | Local helper for trivial SMT constructs
+sp :: Builder -> Builder -> Builder
+a `sp` b = a <> " " <> b
+
+zero :: Builder
+zero = "(_ bv0 256)"
+
+wordAsBV :: forall a. Integral a => a -> Builder
+wordAsBV w = "(_ bv" <> Data.Text.Lazy.Builder.Int.decimal w <> " 256)"
+
+data DivModKind = IsDiv | IsMod
+  deriving (Eq, Ord)
+
+type DivModOp = (DivModKind, Expr EWord, Expr EWord)
+
+data AbstractKey = AbstractKey (Expr EWord) (Expr EWord) DivModKind
+  deriving (Eq, Ord)
+
+isDiv :: DivModKind -> Bool
+isDiv IsDiv = True
+isDiv _     = False
+
+-- | Collect all div/mod operations from an expression.
+collectDivMods :: Expr a -> [DivModOp]
+collectDivMods = \case
+  T.SDiv a b -> [(IsDiv, a, b)]
+  T.SMod a b -> [(IsMod, a, b)]
+  _          -> []
+
+abstractKey :: DivModOp -> AbstractKey
+abstractKey (kind, a, b) = AbstractKey a b kind
+
+-- | Declare abs_a, abs_b, and unsigned result variables for a signed group.
+declareAbsolute :: (Expr EWord -> Err Builder) -> Int -> Expr EWord -> Expr EWord -> Builder -> Err ([SMTEntry], (Builder, Builder))
+declareAbsolute enc groupIdx firstA firstB unsignedResult = do
+  aenc <- enc firstA
+  benc <- enc firstB
+  let absoluteAEnc = smtAbsolute aenc
+      absoluteBEnc = smtAbsolute benc
+      absoluteAName = fromString $ "absolute_a" <> show groupIdx
+      absoluteBName = fromString $ "absolute_b" <> show groupIdx
+  let decls = [ SMTCommand $ "(declare-const" `sp` absoluteAName `sp` "(_ BitVec 256))"
+              , SMTCommand $ "(declare-const" `sp` absoluteBName `sp` "(_ BitVec 256))"
+              , SMTCommand $ "(declare-const" `sp` unsignedResult `sp` "(_ BitVec 256))"
+              , SMTCommand $ "(assert (=" `sp` absoluteAName `sp` absoluteAEnc <> "))"
+              , SMTCommand $ "(assert (=" `sp` absoluteBName `sp` absoluteBEnc <> "))"
+              ]
+  pure (decls, (absoluteAName, absoluteBName))
+
+-- | Assert "abstract sdiv/smod(a,b)" = signed result derived from unsigned result.
+assertAbstEqSignedResult :: (Expr EWord -> Err Builder) -> Builder -> DivModOp -> Err SMTEntry
+assertAbstEqSignedResult enc unsignedResult (kind, a, b) = do
+  aenc <- enc a
+  benc <- enc b
+  let fname = if isDiv kind then "abst_evm_bvsdiv" else "abst_evm_bvsrem"
+      abstract = "(" <> fname `sp` aenc `sp` benc <> ")"
+      concrete = if isDiv kind
+                 then signedFromUnsignedDiv aenc benc unsignedResult
+                 else signedFromUnsignedMod aenc benc unsignedResult
+  pure $ SMTCommand $ "(assert (=" `sp` abstract `sp` concrete <> "))"
+
+-- | Ground-truth axioms: for each sdiv/smod op, assert that the abstract
+-- uninterpreted function equals the real bvsdiv/bvsrem.
+-- e.g. (assert (= (abst_evm_bvsdiv a b) (bvsdiv a b)))
+divModGroundTruth :: (Expr EWord -> Err Builder) -> [Prop] -> Err [SMTEntry]
+divModGroundTruth enc props = do
+  let allDivMods = nubOrd $ concatMap (foldProp collectDivMods []) props
+  if null allDivMods then pure []
+  else do
+    axioms <- mapM mkGroundTruthAxiom allDivMods
+    pure $ (SMTComment "division/modulo ground-truth refinement") : axioms
+  where
+    mkGroundTruthAxiom :: DivModOp -> Err SMTEntry
+    mkGroundTruthAxiom (kind, a, b) = do
+      aenc <- enc a
+      benc <- enc b
+      let (abstFn, concFn) = if isDiv kind
+            then ("abst_evm_bvsdiv", "bvsdiv")
+            else ("abst_evm_bvsrem", "bvsrem")
+      pure $ SMTCommand $ "(assert (=" `sp`
+        "(" <> abstFn `sp` aenc `sp` benc <> ")" `sp`
+        "(" <> concFn `sp` aenc `sp` benc <> ")))"
+
+-- | Encode div/mod operations using abs values, shift-bounds, and congruence (no bvudiv).
+divModEncoding :: (Expr EWord -> Err Builder) -> [Prop] -> Err [SMTEntry]
+divModEncoding enc props = do
+  let allDivMods = nubOrd $ concatMap (foldProp collectDivMods []) props
+  if null allDivMods then pure []
+  else do
+    let groups = groupBy (\a b -> abstractKey a == abstractKey b) $ sortBy (comparing abstractKey) allDivMods
+        indexedGroups = zip [0..] groups
+    let links = mkCongruenceLinks indexedGroups
+    entries <- concat <$> mapM (uncurry mkGroupEncoding) indexedGroups
+    pure $ (SMTComment "division/modulo encoding (abs + shift-bounds + congruence, no bvudiv)") : entries <> links
+  where
+    knownPow2Bound :: Expr EWord -> Maybe W256
+    knownPow2Bound (SHL (Lit k) _) = Just k
+    knownPow2Bound (Lit n) | n > 0 = Just (fromIntegral $ countTrailingZeros n)
+    knownPow2Bound _ = Nothing
+
+    mkGroupEncoding :: Int -> [DivModOp] -> Err [SMTEntry]
+    mkGroupEncoding _ [] = pure []
+    mkGroupEncoding groupIdx lhs@((firstKind, firstA, firstB) : _) = do
+      let isDiv' = isDiv firstKind
+          prefix = if isDiv' then "udiv" else "urem"
+          unsignedResult = fromString $ prefix <> "_" <> show groupIdx
+      (decls, (absoluteA, absoluteB)) <- declareAbsolute enc groupIdx firstA firstB unsignedResult
+
+      -- When the dividend is a left-shift (a = x << k, i.e. a = x * 2^k),
+      -- we can bound the unsigned division result using cheap bitshift
+      -- operations instead of the expensive bvudiv SMT theory.
+      -- The pivot point is |a| >> k (= |a| / 2^k):
+      --   - If |b| >= 2^k: result <= |a| >> k  (upper bound)
+      --   - If |b| <  2^k and b != 0: result >= |a| >> k  (lower bound)
+      let shiftBounds = case (isDiv', knownPow2Bound firstA) of
+            (True, Just k) ->
+              let kLit = wordAsBV k
+                  -- twoPowK = 2^k
+                  twoPowK = "(bvshl (_ bv1 256) " <> kLit <> ")"
+                  -- shifted = |a| >> k = |a| / 2^k
+                  shifted = "(bvlshr" `sp` absoluteA `sp` kLit <> ")"
+              in  -- |b| >= 2^k  =>  |a|/|b| <= |a|/2^k
+                 [ SMTCommand $ "(assert (=> (bvuge" `sp` absoluteB `sp` twoPowK <> ") (bvule" `sp` unsignedResult `sp` shifted <> ")))"
+                  -- |b| < 2^k and |b| != 0  =>  |a|/|b| >= |a|/2^k
+                 , SMTCommand $ "(assert (=> "
+                   <> "(and (bvult" `sp` absoluteB `sp` twoPowK <> ") (distinct " `sp` absoluteB `sp` zero <> "))"
+                   <> "(bvuge" `sp` unsignedResult `sp` shifted <> ")))"
+                 ]
+            _ -> []
+      axioms <- mapM (assertAbstEqSignedResult enc unsignedResult) lhs
+      pure $ decls <> shiftBounds <> axioms
+
+-- | Congruence: if two signed groups have equal absolute inputs, their results are equal.
+mkCongruenceLinks :: [(Int, [DivModOp])] -> [SMTEntry]
+mkCongruenceLinks indexedGroups =
+  let signedDivGroups = [(i, ops) | (i, ops@((k,_,_):_)) <- indexedGroups , k == IsDiv]
+      signedModGroups = [(i, ops) | (i, ops@((k,_,_):_)) <- indexedGroups , k == IsMod]
+  in    concatMap (mkPairLinks "udiv") (allPairs signedDivGroups)
+     <> concatMap (mkPairLinks "urem") (allPairs signedModGroups)
+  where
+    allPairs xs = [(a, b) | a <- xs, b <- xs, fst a < fst b]
+    mkPairLinks prefix' ((i, _), (j, _)) =
+      let absoluteAi = fromString $ "absolute_a" <> show i
+          abosluteBi = fromString $ "absolute_b" <> show i
+          absoluteAj = fromString $ "absolute_a" <> show j
+          absoluteBj = fromString $ "absolute_b" <> show j
+          absoluteResI = fromString $ prefix' <> "_" <> show i
+          absoluteRedJ = fromString $ prefix' <> "_" <> show j
+      in [ SMTCommand $ "(assert (=> "
+            <> "(and (=" `sp` absoluteAi `sp` absoluteAj <> ") (=" `sp` abosluteBi `sp` absoluteBj <> "))"
+            <> "(=" `sp` absoluteResI `sp` absoluteRedJ <> ")))" ]
+
+-- | (ite (= divisor 0) 0 result)
+smtZeroGuard :: Builder -> Builder -> Builder
+smtZeroGuard divisor nonZeroResult =
+  "(ite (=" `sp` divisor `sp` zero <> ")" `sp` zero `sp` nonZeroResult <> ")"
+
+-- | |x| as SMT: ite(x >= 0, x, 0 - x).
+smtAbsolute :: Builder -> Builder
+smtAbsolute x = "(ite (bvsge" `sp` x `sp` zero <> ")" `sp` x `sp` "(bvsub" `sp` zero `sp` x <> "))"
+
+-- | -x as SMT.
+smtNeg :: Builder -> Builder
+smtNeg x = "(bvsub" `sp` zero `sp` x <> ")"
+
+-- | True if a and b have the same sign
+smtSameSign :: Builder -> Builder -> Builder
+smtSameSign a b = "(=" `sp` "(bvslt" `sp` a `sp` zero <> ")" `sp` "(bvslt" `sp` b `sp` zero <> "))"
+
+-- | x >= 0.
+smtIsNonNeg :: Builder -> Builder
+smtIsNonNeg x = "(bvsge" `sp` x `sp` zero <> ")"
+
+-- | sdiv(a,b) = ITE(b = 0,              0,
+--               ITE(sign(a) = sign(b),  udiv(|a|,|b|),
+--                                      -udiv(|a|,|b|)))
+signedFromUnsignedDiv :: Builder -> Builder -> Builder -> Builder
+signedFromUnsignedDiv aenc benc udivResult =
+  smtZeroGuard benc $
+  "(ite" `sp` (smtSameSign aenc benc) `sp`
+    udivResult `sp` (smtNeg udivResult) <> ")"
+
+-- | smod(a,b) = ITE(b = 0,   0,
+--               ITE(a ≥ 0,   urem(|a|,|b|),
+--                           -urem(|a|,|b|)))
+signedFromUnsignedMod :: Builder -> Builder -> Builder -> Builder
+signedFromUnsignedMod aenc benc uremResult =
+  smtZeroGuard benc $
+  "(ite" `sp` (smtIsNonNeg aenc) `sp`
+    uremResult `sp` (smtNeg uremResult) <> ")"
diff --git a/src/EVM/SMT/Types.hs b/src/EVM/SMT/Types.hs
index 57b9f95a1..3a595b079 100644
--- a/src/EVM/SMT/Types.hs
+++ b/src/EVM/SMT/Types.hs
@@ -11,6 +11,9 @@ import EVM.Types
 
 type MaybeIO = MaybeT IO
 
+data DivModEncoding = ConcreteDivMod | AbstractDivMod
+  deriving (Show, Eq)
+
 data SMTEntry = SMTCommand Builder | SMTComment Builder
   deriving (Eq)
 
diff --git a/src/EVM/Solvers.hs b/src/EVM/Solvers.hs
index e2938acfb..9d15a6b81 100644
--- a/src/EVM/Solvers.hs
+++ b/src/EVM/Solvers.hs
@@ -22,7 +22,7 @@ import Prelude hiding (LT, GT)
 import GHC.Natural
 import GHC.IO.Handle (Handle, hFlush, hSetBuffering, BufferMode(..))
 import Control.Concurrent.Chan (Chan, newChan, writeChan, readChan)
-import Control.Concurrent (forkIO, killThread)
+import Control.Concurrent (forkIO, killThread, myThreadId)
 import Control.Concurrent.QSem (QSem, newQSem, waitQSem, signalQSem)
 import Control.Exception (bracket, bracket_, try, IOException)
 import Control.Concurrent.STM (writeTChan, newTChan, TChan, tryReadTChan, atomically)
@@ -52,6 +52,7 @@ import EVM.Expr (simplifyProps)
 import EVM.Keccak qualified as Keccak (concreteKeccaks)
 import EVM.SMT
 import EVM.Types
+import Debug.Trace (traceM)
 
 
 -- In megabytes, i.e. 1GB
@@ -103,8 +104,8 @@ data MultiData = MultiData
 
 data SingleData = SingleData
   SMT2
-  (Maybe [Prop])
-  (Chan SMTResult) -- result channel
+  (Maybe [Prop])    -- Props that generated the SMT2, if available. Used for caching
+  (Chan SMTResult)  -- result channel
 
 -- returns True if a is a superset of any of the sets in bs
 supersetAny :: Set Prop -> [Set Prop] -> Bool
@@ -128,11 +129,21 @@ checkSatWithProps sg props = do
   if psSimp == [PBool False] then pure Qed
   else do
     let concreteKeccaks = fmap (\(buf,val) -> PEq (Lit val) (Keccak buf)) (toList $ Keccak.concreteKeccaks props)
-    let smt2 = assertProps conf (if conf.simp then psSimp <> concreteKeccaks else psSimp)
-    if isLeft smt2 then pure $ Error $ getError smt2
-    else liftIO $ checkSat sg (Just props) smt2
+    let allProps = if conf.simp then psSimp <> concreteKeccaks else psSimp
+    if not conf.abstractArith then do
+      let smt2 = assertProps conf allProps
+      if isLeft smt2 then pure $ Error $ getError smt2
+      else liftIO $ checkSat sg (Just props) smt2
+    else liftIO $ do
+      -- Two-phase solving with abstraction+refinement
+      let smt2Abstract = assertPropsAbstract conf allProps
+      let refinement = divModGroundTruth (exprToSMTWith AbstractDivMod) allProps
+      if isLeft smt2Abstract then pure $ Error $ getError smt2Abstract
+      else if isLeft refinement then pure $ Error $ getError refinement
+      else do
+        let x = (getNonError smt2Abstract) <> (SMT2 (SMTScript (getNonError refinement)) mempty mempty)
+        liftIO $ checkSat sg (Just props) (Right x)
 
--- When props is Nothing, the cache will not be filled or used
 checkSat :: SolverGroup -> Maybe [Prop] -> Err SMT2 -> IO SMTResult
 checkSat (SolverGroup taskq) props smt2 = do
   if isLeft smt2 then pure $ Error $ getError smt2
@@ -144,6 +155,7 @@ checkSat (SolverGroup taskq) props smt2 = do
     -- collect result
     readChan resChan
 
+
 writeSMT2File :: SMT2 -> FilePath -> String -> IO ()
 writeSMT2File smt2 path postfix = do
     let content = formatSMT2 smt2 <> "\n\n(check-sat)"
@@ -251,7 +263,7 @@ getMultiSol solver timeout maxMemory smt2@(SMT2 cmds cexvars _) multiSol r sem f
         (spawnSolver solver timeout maxMemory)
         (stopSolver)
         (\inst -> do
-          out <- sendScript inst cmds
+          out <- sendScript conf inst cmds
           case out of
             Left err -> do
               when conf.debug $ putStrLn $ "Issue while writing SMT to solver (maybe it got killed)?: " <> (T.unpack err)
@@ -263,47 +275,66 @@ getMultiSol solver timeout maxMemory smt2@(SMT2 cmds cexvars _) multiSol r sem f
         )
     )
 
-getOneSol :: (MonadIO m, ReadConfig m) => Solver -> Maybe Natural -> Natural -> SMT2 -> Maybe [Prop] -> Chan SMTResult -> TChan CacheEntry -> QSem -> Int -> m ()
+getOneSol :: forall m . (MonadIO m, ReadConfig m) =>
+  Solver -> Maybe Natural -> Natural -> SMT2 -> Maybe [Prop] -> Chan SMTResult -> TChan CacheEntry -> QSem -> Int -> m ()
 getOneSol solver timeout maxMemory smt2@(SMT2 cmds cexvars _) props r cacheq sem fileCounter = do
   conf <- readConfig
   liftIO $ bracket_
     (waitQSem sem)
     (signalQSem sem)
     (do
-      when (conf.dumpQueries) $ writeSMT2File smt2 "." (show fileCounter)
       bracket
         (spawnSolver solver timeout maxMemory)
         (stopSolver)
         (\inst -> do
-          out <- sendScript inst cmds
-          case out of
-            Left e -> writeChan r (Unknown $ "Issue while writing SMT to solver (maybe it got killed?): " <> T.unpack e)
-            Right () -> do
-              sat <- sendCommand inst $ SMTCommand "(check-sat)"
-              res <- do
-                  case sat of
-                    "unsat" -> do
-                      when (isJust props) $ liftIO . atomically $ writeTChan cacheq (CacheEntry (fromJust props))
-                      pure Qed
-                    "timeout" -> pure $ Unknown "Result timeout by SMT solver"
-                    "unknown" -> do
-                      dumpUnsolved smt2 fileCounter conf.dumpUnsolved
-                      pure $ Unknown "Result unknown by SMT solver"
-                    "sat" -> do
-                      mmodel <- getModel inst cexvars
-                      case mmodel of
-                        Just model -> pure $ Cex model
-                        Nothing -> pure $ Unknown "Solver died while extracting model"
-                    _ -> let  supportIssue =
-                                  ("does not yet support" `T.isInfixOf` sat)
-                                  || ("unsupported" `T.isInfixOf` sat)
-                                  || ("not support" `T.isInfixOf` sat)
-                      in case supportIssue of
-                       True -> pure . Error $ "SMT solver reported unsupported operation: " <> T.unpack sat
-                       False -> pure . Unknown $ "Unable to parse SMT solver output (maybe it got killed?): " <> T.unpack sat
-              writeChan r res
+          when (conf.dumpQueries) $ writeSMT2File smt2 "-abst." (show fileCounter)
+          ret <- sendAndCheck conf inst cmds $ \res -> do
+            case res of
+              "unsat" -> do
+                when conf.debug $ logWithTid "Query is UNSAT."
+                dealWithUnsat
+              "sat" -> dealWithModel conf inst
+              "timeout" -> pure $ Unknown "Abstract query timeout"
+              "unknown" -> dealWithUnknown conf
+              _ -> dealWithIssue conf res
+          writeChan r ret
         )
     )
+  where
+    sendAndCheck conf inst dat cont = do
+      out <- liftIO $ sendScript conf inst dat
+      case out of
+        Left e -> unknown conf $ "Issue while writing SMT to solver (maybe it got killed)?: " <> T.unpack e
+        Right () -> do
+          res <- liftIO $ sendCommand inst $ SMTCommand "(check-sat)"
+          cont res
+    dealWithUnsat = do
+      when (isJust props) $ liftIO . atomically $ writeTChan cacheq (CacheEntry (fromJust props))
+      pure Qed
+    dealWithUnknown conf = do
+      dumpUnsolved smt2 fileCounter conf.dumpUnsolved
+      unknown conf "SMT solver returned unknown (maybe it got killed?)"
+    dealWithModel conf inst = getModel inst cexvars >>= \case
+      Just model -> pure $ Cex model
+      Nothing -> unknown conf "Solver died while extracting model."
+    dealWithIssue conf sat = do
+      let supportIssue = ("does not yet support" `T.isInfixOf` sat)
+                         || ("unsupported" `T.isInfixOf` sat)
+                         || ("not support" `T.isInfixOf` sat)
+      case supportIssue of
+        True -> do
+          let txt = "SMT solver reported unsupported operation: " <> T.unpack sat
+          when conf.debug $ logWithTid txt
+          pure $ Error txt
+        False -> unknown conf $ "Unable to parse SMT solver output (maybe it got killed?): " <> T.unpack sat
+    unknown conf msg = do
+      when conf.debug $ logWithTid msg
+      pure $ Unknown msg
+
+logWithTid :: MonadIO m => String -> m ()
+logWithTid msg = do
+  tid <- liftIO myThreadId
+  traceM $ "[" <> show tid <> "] " <> msg
 
 dumpUnsolved :: SMT2 -> Int -> Maybe FilePath -> IO ()
 dumpUnsolved fullSmt fileCounter dump = do
@@ -493,8 +524,8 @@ stopSolver :: SolverInstance -> IO ()
 stopSolver (SolverInstance _ stdin stdout process) = cleanupProcess (Just stdin, Just stdout, Nothing, process)
 
 -- | Sends a list of commands to the solver. Returns the first error, if there was one.
-sendScript :: SolverInstance -> SMTScript -> IO (Either Text ())
-sendScript solver (SMTScript entries) = do
+sendScript :: Config -> SolverInstance -> SMTScript -> IO (Either Text ())
+sendScript conf solver (SMTScript entries) = do
   go entries
   where
     go [] = pure $ Right ()
@@ -503,7 +534,9 @@ sendScript solver (SMTScript entries) = do
       out <- sendCommand solver c
       case out of
         "success" -> go cs
-        e -> pure $ Left $ "Solver returned an error:\n" <> e <> "\nwhile sending the following command: " <> toLazyText command
+        e -> do
+          when conf.debug $ putStrLn $ "Error while writing SMT to solver: " <> T.unpack e <> " -- Command was: " <> T.unpack (toLazyText command)
+          pure $ Left $ "Solver returned an error:\n" <> e <> "\nwhile sending the following command: " <> toLazyText command
 
 -- | Returns Nothing if the solver died or returned an error
 checkCommand :: SolverInstance -> SMTEntry -> IO (Maybe ())
diff --git a/test/clitest.hs b/test/clitest.hs
index 681ecf7d8..c77e3dd65 100644
--- a/test/clitest.hs
+++ b/test/clitest.hs
@@ -135,7 +135,7 @@ main = do
           |])
         let hexStr = Types.bsToHex c
         (_, stdout, _) <- readProcessWithExitCode "cabal" ["run", "exe:hevm", "--", "symbolic", "--solver", "empty", "--code", hexStr] ""
-        stdout `shouldContain` "SMT solver says: Result unknown by SMT solver"
+        stdout `shouldContain` "SMT solver returned unknown"
       it "crash-of-hevm" $ do
         let hexStrA = "608060405234801561001057600080fd5b506004361061002b5760003560e01c8063efa2978514610030575b600080fd5b61004361003e3660046102ad565b610045565b005b60006100508561007a565b9050600061005d866100a8565b905080821461006e5761006e61034c565b50505050505050505050565b600061008761032e6103aa565b8261009457610197610098565b61013e5b6100a291906103e2565b92915050565b60006100b561032e6103aa565b6100be906103aa565b6100c7906103aa565b82806100d1575060005b806100da575060005b61013157605a6100ea60006103aa565b6100f3906103aa565b6100ff6001605a610404565b61010b6001605a610404565b61011891166101976103e2565b6101229190610493565b61012c9190610493565b610149565b604061013f8161013e6103e2565b6101499190610493565b61015391906103e2565b61016061032e60006103e2565b83801561016b575060015b15801590610177575060015b80156101a05750831515801561018b575060015b15158015610197575060015b806101a0575060005b610251576101976101b3605a602d610493565b602d60006101c2600182610493565b6101cd906001610404565b6101d8906001610404565b6101e1906103aa565b6101ea906103aa565b6101f491906103e2565b6101ff90605a610404565b604e61020c8160016103e2565b6102169190610493565b61022490600116605a610404565b1661022e906103aa565b61023891906103e2565b6102429190610493565b61024c9190610493565b610283565b604561025f8161013e6103e2565b6102699190610493565b60456102778161013e6103e2565b6102819190610493565b165b61028d91906103e2565b1692915050565b80358015155b81146100a257600080fd5b80358061029a565b600080600080600080600080610100898b0312156102ca57600080fd5b6102d48a8a610294565b97506102e38a60208b01610294565b96506102f28a60408b016102a5565b95506103018a60608b016102a5565b94506103108a60808b01610294565b935061031f8a60a08b016102a5565b925061032e8a60c08b01610294565b915061033d8a60e08b016102a5565b90509295985092959890939650565b7f4e487b7100000000000000000000000000000000000000000000000000000000600052600160045260246000fd5b7f4e487b7100000000000000000000000000000000000000000000000000000000600052601160045260246000fd5b60007f800000000000000000000000000000000000000000000000000000000000000082036103db576103db61037b565b5060000390565b818103600083128015838313168383129190911617156100a2576100a261037b565b60008261043a577f4e487b7100000000000000000000000000000000000000000000000000000000600052601260045260246000fd5b7f800000000000000000000000000000000000000000000000000000000000000082147fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff8414161561048e5761048e61037b565b500590565b80820160008212801584831290811690159190911617156100a2576100a261037b56fea26469706673582212200a37769e5bf4b8b890caac8ab643126d55feb821a0201d2f674203f23fa666ad64736f6c634300081e0033"
 
@@ -198,10 +198,9 @@ main = do
         shouldBe fileExists True
         removeFile filename
       it "early-abort" $ do
-        (exitcode, stdout, stderr) <- runForge "test/contracts/pass/early-abort.sol" ["--max-iterations", "1000"]
-        putStrLn $ "Exit code: " ++ show exitcode
-        putStrLn stderr
-        putStrLn stdout
+        (_, stdout, _) <- runForge "test/contracts/pass/early-abort.sol" ["--max-iterations", "1000"]
+        stdout `shouldContain` "[FAIL]"
+        (T.count "Counterexample:" (T.pack stdout)) `shouldBe` 9
       it "rpc-cache" $ do
         (_, stdout, stderr) <- runForge "test/contracts/fail/rpc-test.sol"
           ["--rpc", "http://mock.mock", "--prefix", "test_attack_symbolic"
diff --git a/test/test.hs b/test/test.hs
index b955b7084..ea16688b9 100644
--- a/test/test.hs
+++ b/test/test.hs
@@ -54,7 +54,7 @@ import EVM.Fetch qualified as Fetch
 import EVM.Format (hexText)
 import EVM.Precompiled
 import EVM.RLP
-import EVM.SMT hiding (one)
+import EVM.SMT
 import EVM.Solidity
 import EVM.Solvers
 import EVM.Stepper qualified as Stepper
@@ -105,6 +105,10 @@ testNoSimplify :: TestName -> ReaderT Env IO () -> TestTree
 testNoSimplify a b = let testEnvNoSimp = Env { config = testEnv.config { simp = False } }
   in testCase a $ runEnv testEnvNoSimp b
 
+testAbstractArith :: TestName -> ReaderT Env IO () -> TestTree
+testAbstractArith a b = let testEnvAbstract = Env { config = testEnv.config { abstractArith = True } }
+  in testCase a $ runEnv testEnvAbstract b
+
 prop :: Testable prop => ReaderT Env IO prop -> Property
 prop a = ioProperty $ runEnv testEnv a
 
@@ -122,6 +126,9 @@ withCVC5Solver = withSolvers CVC5 3 Nothing defMemLimit
 withBitwuzlaSolver :: App m => (SolverGroup -> m a) -> m a
 withBitwuzlaSolver = withSolvers Bitwuzla 3 Nothing defMemLimit
 
+withShortBitwuzlaSolver :: App m => (SolverGroup -> m a) -> m a
+withShortBitwuzlaSolver = withSolvers Bitwuzla 3 (Just 5) defMemLimit
+
 
 main :: IO ()
 main = defaultMain tests
@@ -1272,6 +1279,437 @@ tests = testGroup "hevm"
         let testFile = "test/contracts/pass/keccak.sol"
         runForgeTest testFile "prove_access" >>= assertEqualM "test result" (True, True)
     ]
+  , testGroup "Arith"
+    -- Tests adapted from halmos (tests/regression/test/Arith.t.sol, tests/solver/test/SignedDiv.t.sol, tests/solver/test/Math.t.sol)
+    -- Run with abstractArith = True to exercise two-phase solving
+    [ test "math-avg" $ do
+        Just c <- solcRuntime "C" [i|
+          contract C {
+            function prove_Avg(uint a, uint b) external pure {
+              require(a + b >= a);
+              unchecked {
+                uint r1 = (a & b) + (a ^ b) / 2;
+                uint r2 = (a + b) / 2;
+                assert(r1 == r2);
+              }
+            }
+          } |]
+        (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
+        assertEqualM "Must be QED" [] res
+      , test "unsigned-div-by-zero" $ do
+        Just c <- solcRuntime "C" [i|
+          contract C {
+            function prove_unsigned_div_by_zero(uint256 a) external pure {
+              uint256 result;
+              assembly { result := div(a, 0) }
+              assert(result == 0);
+            }
+          } |]
+        (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
+        assertEqualM "Must be QED" [] res
+      , test "arith-div-pass" $ do
+        Just c <- solcRuntime "C" [i|
+          contract C {
+            function prove_Div_pass(uint x, uint y) external pure {
+              require(x > y);
+              require(y > 0);
+              uint q;
+              assembly { q := div(x, y) }
+              assert(q != 0);
+            }
+          } |]
+        (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
+        assertEqualM "Must be QED" [] res
+    , test "arith-div-fail" $ do
+        Just c <- solcRuntime "C" [i|
+          contract C {
+            function prove_Div_fail(uint x, uint y) external pure {
+              require(x > y);
+              uint q;
+              assembly { q := div(x, y) }
+              assert(q != 0);
+            }
+          } |]
+        (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
+        assertBoolM "Expected counterexample" (any isCex res)
+    , test "arith-mod-fail" $ do
+        Just c <- solcRuntime "C" [i|
+          contract C {
+            function prove_Div_fail(uint x, uint y) external pure {
+              require(x > y);
+              uint q;
+              assembly { q := mod(x, y) }
+              assert(q != 0);
+            }
+          } |]
+        (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
+        assertBoolM "Expected counterexample" (any isCex res)
+    ]
+  , testGroup "Abstract-Arith"
+    -- "make verify-hevm T=prove_div_negative_divisor" in https://github.com/gustavo-grieco/abdk-math-64.64-verification
+    [ testCase "prove_div_values-abdk" $ do
+        Just c <- solcRuntime "C" [i|
+          contract C {
+              bool public IS_TEST = true;
+
+              int128 private constant MIN_64x64 = -0x80000000000000000000000000000000;
+              int128 private constant MAX_64x64 = 0x7FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF;
+
+              // ABDKMath64x64.fromInt(0) == 0
+              int128 private constant ZERO_FP = 0;
+              // ABDKMath64x64.fromInt(1) == 1 << 64
+              int128 private constant ONE_FP = 0x10000000000000000;
+
+              // ABDKMath64x64.div
+              function div(int128 x, int128 y) internal pure returns (int128) {
+                  unchecked {
+                      require(y != 0);
+                      int256 result = (int256(x) << 64) / y;
+                      require(result >= MIN_64x64 && result <= MAX_64x64);
+                      return int128(result);
+                  }
+              }
+
+              // ABDKMath64x64.abs
+              function abs(int128 x) internal pure returns (int128) {
+                  unchecked {
+                      require(x != MIN_64x64);
+                      return x < 0 ? -x : x;
+                  }
+              }
+
+              // Property: |x / y| <= |x| when |y| >= 1, and |x / y| >= |x| when |y| < 1
+              function prove_div_values(int128 x, int128 y) public pure {
+                  require(y != ZERO_FP);
+
+                  int128 x_y = abs(div(x, y));
+
+                  if (abs(y) >= ONE_FP) {
+                      assert(x_y <= abs(x));
+                  } else {
+                      assert(x_y >= abs(x));
+                  }
+              }
+          } |]
+        let sig = (Just $ Sig "prove_div_values(int128,int128)" [AbiIntType 128, AbiIntType 128])
+        let testEnvAbstract = Env { config = testEnv.config { abstractArith = True } }
+        runEnv testEnvAbstract $ do
+          (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
+        -- with abstract arith, we prove it
+          assertEqualM "Must be QED" res []
+        runEnv testEnv $ do
+          (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
+          -- without abstract arith, we time out
+          liftIO $ assertBool "Must be unknown" (all isUnknown res)
+    -- "make verify-hevm T=prove_div_negative_divisor" in https://github.com/gustavo-grieco/abdk-math-64.64-verification
+    , testCase "prove_div_negative_divisor" $ do
+        Just c <- solcRuntime "C" [i|
+          contract C {
+              bool public IS_TEST = true;
+
+              int128 private constant MIN_64x64 = -0x80000000000000000000000000000000;
+              int128 private constant MAX_64x64 = 0x7FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFF;
+
+              // ABDKMath64x64.fromInt(0) == 0
+              int128 private constant ZERO_FP = 0;
+
+              // ABDKMath64x64.div
+              function div(int128 x, int128 y) internal pure returns (int128) {
+                  unchecked {
+                      require(y != 0);
+                      int256 result = (int256(x) << 64) / y;
+                      require(result >= MIN_64x64 && result <= MAX_64x64);
+                      return int128(result);
+                  }
+              }
+
+              // ABDKMath64x64.neg
+              function neg(int128 x) internal pure returns (int128) {
+                  unchecked {
+                      require(x != MIN_64x64);
+                      return -x;
+                  }
+              }
+
+              // Property: x / (-y) == -(x / y)
+              function prove_div_negative_divisor(int128 x, int128 y) public pure {
+                  require(y < ZERO_FP);
+
+                  int128 x_y = div(x, y);
+                  int128 x_minus_y = div(x, neg(y));
+
+                  assert(x_y == neg(x_minus_y));
+              }
+          } |]
+        let sig = (Just $ Sig "prove_div_negative_divisor(int128,int128)" [AbiIntType 128, AbiIntType 128])
+        let testEnvAbstract = Env { config = testEnv.config { abstractArith = True } }
+        runEnv testEnvAbstract $ do
+          (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
+          -- with abstract arith, we prove it
+          assertEqualM "Must be QED" res []
+        runEnv testEnv $ do
+          (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts
+          -- without abstract arith, we time out
+          liftIO $ assertBool "Must be unknown" (all isUnknown res)
+
+    , testAbstractArith "sdiv-by-one" $ do
+        Just c <- solcRuntime "C" [i|
+          contract C {
+            function prove_sdiv_by_one(int256 a) external pure {
+              int256 result;
+              assembly { result := sdiv(a, 1) }
+              assert(result == a);
+            }
+          } |]
+        (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
+        assertEqualM "Must be QED" res []
+    , testAbstractArith "sdiv-by-neg-one" $ do
+        Just c <- solcRuntime "C" [i|
+          contract C {
+            function prove_sdiv_by_neg_one(int256 a) external pure {
+              int256 result;
+              assembly { result := sdiv(a, sub(0, 1)) }
+              if (a == -170141183460469231731687303715884105728 * 2**128) { // type(int256).min
+                  assert(result == a);
+              } else {
+                  assert(result == -a);
+              }
+            }
+          } |]
+        (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
+        assertEqualM "Must be QED" res []
+    , testAbstractArith "sdiv-intmin-by-two" $ do
+        Just c <- solcRuntime "C" [i|
+          contract C {
+            function prove_sdiv_intmin_by_two() external pure {
+              int256 result;
+              assembly {
+                let intmin := 0x8000000000000000000000000000000000000000000000000000000000000000
+                result := sdiv(intmin, 2)
+              }
+              // -2**254 is 0xc000...0000
+              assert(result == -0x4000000000000000000000000000000000000000000000000000000000000000);
+            }
+          } |]
+        (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
+        assertEqualM "Must be QED" [] res
+    , testAbstractArith "smod-by-zero" $ do
+        Just c <- solcRuntime "C" [i|
+          contract C {
+            function prove_smod_by_zero(int256 a) external pure {
+              int256 result;
+              assembly { result := smod(a, 0) }
+              assert(result == 0);
+            }
+          } |]
+        (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
+        assertEqualM "Must be QED" res []
+    , testAbstractArith "smod-intmin-by-three" $ do
+        Just c <- solcRuntime "C" [i|
+          contract C {
+            function prove_smod_intmin_by_three() external pure {
+              int256 result;
+              assembly { result := smod(0x8000000000000000000000000000000000000000000000000000000000000000, 3) }
+              assert(result == -2);
+            }
+          } |]
+        (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
+        assertEqualM "Must be QED" res []
+    , testAbstractArith "sdiv-by-zero" $ do
+        Just c <- solcRuntime "C" [i|
+          contract C {
+            function prove_sdiv_by_zero(int256 a) external pure {
+              int256 result;
+              assembly { result := sdiv(a, 0) }
+              assert(result == 0);
+            }
+          } |]
+        (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
+        assertEqualM "Must be QED" [] res
+    , testAbstractArith "sdiv-zero-dividend" $ do
+        Just c <- solcRuntime "C" [i|
+          contract C {
+            function prove_sdiv_zero_dividend(int256 b) external pure {
+              int256 result;
+              assembly { result := sdiv(0, b) }
+              assert(result == 0);
+            }
+          } |]
+        (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
+        assertEqualM "Must be QED" [] res
+    , testAbstractArith "sdiv-truncation" $ do
+        Just c <- solcRuntime "C" [i|
+          contract C {
+            function prove_sdiv_truncation() external pure {
+              int256 result;
+              assembly { result := sdiv(sub(0, 7), 2) }
+              assert(result == -3);
+            }
+          } |]
+        (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
+        assertEqualM "Must be QED" [] res
+    , testAbstractArith "sdiv-sign-symmetry" $ do
+        Just c <- solcRuntime "C" [i|
+          contract C {
+            function prove_sdiv_sign_symmetry(int256 a, int256 b) external pure {
+              if (a == -57896044618658097711785492504343953926634992332820282019728792003956564819968) return;
+              if (b == -57896044618658097711785492504343953926634992332820282019728792003956564819968) return;
+              if (b == 0) return;
+              int256 r1;
+              int256 r2;
+              assembly {
+                r1 := sdiv(a, b)
+                r2 := sdiv(sub(0, a), sub(0, b))
+              }
+              assert(r1 == r2);
+            }
+          } |]
+        (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
+        assertEqualM "Must be QED" [] res
+    , testAbstractArith "sdiv-sign-antisymmetry" $ do
+        Just c <- solcRuntime "C" [i|
+          contract C {
+            function prove_sdiv_sign_antisymmetry(int256 a, int256 b) external pure {
+              if (a == -57896044618658097711785492504343953926634992332820282019728792003956564819968) return;
+              if (b == 0) return;
+              int256 r1;
+              int256 r2;
+              assembly {
+                r1 := sdiv(a, b)
+                r2 := sdiv(sub(0, a), b)
+              }
+              assert(r1 == -r2);
+            }
+          } |]
+        (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
+        assertEqualM "Must be QED" [] res
+    , testAbstractArith "smod-by-one" $ do
+        Just c <- solcRuntime "C" [i|
+          contract C {
+            function prove_smod_by_one(int256 a) external pure {
+              int256 r1;
+              int256 r2;
+              assembly {
+                r1 := smod(a, 1)
+                r2 := smod(a, sub(0, 1))
+              }
+              assert(r1 == 0);
+              assert(r2 == 0);
+            }
+          } |]
+        (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
+        assertEqualM "Must be QED" [] res
+    , testAbstractArith "smod-zero-dividend" $ do
+        Just c <- solcRuntime "C" [i|
+          contract C {
+            function prove_smod_zero_dividend(int256 b) external pure {
+              int256 result;
+              assembly { result := smod(0, b) }
+              assert(result == 0);
+            }
+          } |]
+        (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
+        assertEqualM "Must be QED" [] res
+    , testAbstractArith "smod-sign-matches-dividend" $ do
+        Just c <- solcRuntime "C" [i|
+          contract C {
+            function prove_smod_sign_matches_dividend(int256 a, int256 b) external pure {
+              if (b == 0 || a == 0) return;
+              int256 result;
+              assembly { result := smod(a, b) }
+              if (result != 0) {
+                assert((a > 0 && result > 0) || (a < 0 && result < 0));
+              }
+            }
+          } |]
+        (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
+        assertEqualM "Must be QED" [] res
+    , testAbstractArith "smod-intmin" $ do
+        Just c <- solcRuntime "C" [i|
+          contract C {
+            function prove_smod_intmin() external pure {
+              int256 result;
+              assembly { result := smod(0x8000000000000000000000000000000000000000000000000000000000000000, 2) }
+              assert(result == 0);
+            }
+          } |]
+        (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
+        assertEqualM "Must be QED" [] res
+    , testAbstractArith "sdiv-intmin-by-neg-one" $ do
+        Just c <- solcRuntime "C" [i|
+          contract C {
+            function prove_sdiv_intmin_by_neg_one() external pure {
+              int256 result;
+              assembly {
+                let intmin := 0x8000000000000000000000000000000000000000000000000000000000000000
+                result := sdiv(intmin, sub(0, 1))
+              }
+              // EVM defines sdiv(MIN_INT, -1) = MIN_INT (overflow)
+              assert(result == -57896044618658097711785492504343953926634992332820282019728792003956564819968);
+            }
+          } |]
+        (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
+        assertEqualM "Must be QED" [] res
+    , testAbstractArith "smod-intmin-by-neg-one" $ do
+        Just c <- solcRuntime "C" [i|
+          contract C {
+            function prove_smod_intmin_by_neg_one() external pure {
+              int256 result;
+              assembly {
+                let intmin := 0x8000000000000000000000000000000000000000000000000000000000000000
+                result := smod(intmin, sub(0, 1))
+              }
+              // smod(MIN_INT, -1) = 0 since MIN_INT is divisible by -1
+              assert(result == 0);
+            }
+          } |]
+        (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
+        assertEqualM "Must be QED" [] res
+    , testAbstractArith "sdiv-intmin-by-intmin" $ do
+        Just c <- solcRuntime "C" [i|
+          contract C {
+            function prove_sdiv_intmin_by_intmin() external pure {
+              int256 result;
+              assembly {
+                let intmin := 0x8000000000000000000000000000000000000000000000000000000000000000
+                result := sdiv(intmin, intmin)
+              }
+              assert(result == 1);
+            }
+          } |]
+        (_, res) <- withShortBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
+        assertEqualM "Must be QED" [] res
+    , testAbstractArith "arith-mod" $ do
+        Just c <- solcRuntime "C" [i|
+          contract C {
+            function unchecked_smod(int x, int y) internal pure returns (int ret) {
+              assembly { ret := smod(x, y) }
+            }
+            function prove_Mod(int x, int y) external pure {
+              unchecked {
+                assert(unchecked_smod(x, 0) == 0);
+                assert(x % 1 == 0);
+                assert(x % 2 < 2 && x % 2 > -2);
+                assert(x % 4 < 4 && x % 4 > -4);
+                int x_smod_y = unchecked_smod(x, y);
+                assert(x_smod_y <= y || y < 0);}
+            }
+          } |]
+        (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
+        assertEqualM "Must be QED" [] res
+    , testAbstractArith "math-mint-fail" $ do
+        Just c <- solcRuntime "C" [i|
+          contract C {
+            function prove_mint(uint s, uint A1, uint S1) external pure {
+              uint a = (s * A1) / S1;
+              uint A2 = A1 + a;
+              uint S2 = S1 + s;
+              assert(A1 * S2 <= A2 * S1);
+            }
+          } |]
+        (_, res) <- withBitwuzlaSolver $ \s -> checkAssert s defaultPanicCodes c Nothing [] defaultVeriOpts
+        assertBoolM "Expected counterexample" (any isCex res)
+    ]
   , testGroup "max-iterations"
     [ test "concrete-loops-reached" $ do
         Just c <- solcRuntime "C"
@@ -3877,7 +4315,7 @@ tests = testGroup "hevm"
   [ testCase "encodeConcreteStore-overwrite" $
     assertEqual ""
       (pure "(store (store ((as const Storage) #x0000000000000000000000000000000000000000000000000000000000000000) (_ bv1 256) (_ bv2 256)) (_ bv3 256) (_ bv4 256))")
-      (EVM.SMT.encodeConcreteStore $ Map.fromList [(W256 1, W256 2), (W256 3, W256 4)])
+      (EVM.SMT.encodeConcreteStore ConcreteDivMod $ Map.fromList [(W256 1, W256 2), (W256 3, W256 4)])
   ]
   , testGroup "calling-solvers"
   [ test "no-error-on-large-buf" $ do