From 7cfda4f432c032f5e918234981b9d73f190c769b Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Thu, 20 Jan 2022 16:21:16 -0800
Subject: [PATCH 1/4] Export some additional operations from `What4.Expr`, and
 define a new dummy data type that can be used for the expression builder
 state field.

---
 what4/src/What4/Expr.hs | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/what4/src/What4/Expr.hs b/what4/src/What4/Expr.hs
index d225a3a84..75514982b 100644
--- a/what4/src/What4/Expr.hs
+++ b/what4/src/What4/Expr.hs
@@ -13,6 +13,16 @@ module What4.Expr
   ( -- * Expression builder
     ExprBuilder
   , newExprBuilder
+  , startCaching
+  , stopCaching
+  , userState
+  , exprCounter
+  , curProgramLoc
+  , unaryThreshold
+  , cacheStartSize
+  , exprBuilderSplitConfig
+  , exprBuilderFreshConfig
+  , EmptyExprBuilderState(..)
 
     -- * Flags
   , FloatMode
@@ -97,3 +107,9 @@ import What4.Expr.Builder
 import What4.Expr.GroundEval
 import What4.Expr.WeightedSum
 import What4.Expr.UnaryBV
+
+
+-- | A \"dummy\" data type that can be used for the
+--   user state field of an @ExprBuilder@ when there
+--   is no other interesting state to track.
+data EmptyExprBuilderState t = EmptyExprBuilderState

From fe93384c28aebacf73562f8da0ceac3f3f5b28b1 Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Fri, 21 Jan 2022 10:57:26 -0800
Subject: [PATCH 2/4] Update tests and examples to use the new
 `EmptyExprBuilderState`.

---
 what4-transition-system/test/Main.hs |  8 +++-----
 what4/README.md                      |  7 +++----
 what4/doc/QuickStart.hs              |  7 +++----
 what4/test/AdapterTest.hs            | 23 ++++++++++++-----------
 what4/test/ExprBuilderSMTLib2.hs     |  7 +++----
 what4/test/ExprsTest.hs              |  6 ++----
 what4/test/IteExprs.hs               |  5 ++---
 what4/test/OnlineSolverTest.hs       |  8 +++-----
 what4/test/TestTemplate.hs           |  5 ++---
 9 files changed, 33 insertions(+), 43 deletions(-)

diff --git a/what4-transition-system/test/Main.hs b/what4-transition-system/test/Main.hs
index ec0847878..eef93410e 100644
--- a/what4-transition-system/test/Main.hs
+++ b/what4-transition-system/test/Main.hs
@@ -28,6 +28,7 @@ import What4.Expr
   ( ExprBuilder,
     FloatModeRepr (FloatIEEERepr),
     newExprBuilder,
+    EmptyExprBuilderState(..)
   )
 import What4.Expr.Builder (SymbolBinding (..))
 import qualified What4.Interface as What4
@@ -54,17 +55,14 @@ main :: IO ()
 main =
   do
     withIONonceGenerator $ \nonceGen -> do
-      sym <- newExprBuilder FloatIEEERepr State nonceGen
+      sym <- newExprBuilder FloatIEEERepr EmptyExprBuilderState nonceGen
       ts <- counterTransitionSystem sym
       displayTransitionSystem sym ts
     withIONonceGenerator $ \nonceGen -> do
-      sym <- newExprBuilder FloatIEEERepr State nonceGen
+      sym <- newExprBuilder FloatIEEERepr EmptyExprBuilderState nonceGen
       ts <- realsTransitionSystem sym
       displayTransitionSystem sym ts
 
--- We don't need any information in the state
-data State t = State
-
 makeFieldNames ::
   forall stateType.
   [What4.SolverSymbol] ->
diff --git a/what4/README.md b/what4/README.md
index 6e8f491bb..3bbfe1db0 100644
--- a/what4/README.md
+++ b/what4/README.md
@@ -57,7 +57,8 @@ import Data.Parameterized.Some (Some(..))
 import What4.Config (extendConfig)
 import What4.Expr
          ( ExprBuilder,  FloatModeRepr(..), newExprBuilder
-         , BoolExpr, GroundValue, groundEval )
+         , BoolExpr, GroundValue, groundEval
+		 , EmptyExprBuilderState(..) )
 import What4.Interface
          ( BaseTypeRepr(..), getConfiguration
          , freshConstant, safeSymbol
@@ -75,8 +76,6 @@ to our backend solver, which is Z3 in this example.
 point to your Z3.)
 
 ```
-data BuilderState st = EmptyState
-
 z3executable :: FilePath
 z3executable = "z3"
 ```
@@ -87,7 +86,7 @@ We're ready to start our `main` function:
 main :: IO ()
 main = do
   Some ng <- newIONonceGenerator
-  sym <- newExprBuilder FloatIEEERepr EmptyState ng
+  sym <- newExprBuilder FloatIEEERepr EmptyExprBuilderState ng
 ```
 
 Most of the functions in `What4.Interface`, the module for building up
diff --git a/what4/doc/QuickStart.hs b/what4/doc/QuickStart.hs
index faaecbf09..8daf605f6 100644
--- a/what4/doc/QuickStart.hs
+++ b/what4/doc/QuickStart.hs
@@ -10,7 +10,8 @@ import Data.Parameterized.Some (Some(..))
 import What4.Config (extendConfig)
 import What4.Expr
          ( ExprBuilder,  FloatModeRepr(..), newExprBuilder
-         , BoolExpr, GroundValue, groundEval )
+         , BoolExpr, GroundValue, groundEval
+         , EmptyExprBuilderState(..) )
 import What4.Interface
          ( BaseTypeRepr(..), getConfiguration
          , freshConstant, safeSymbol
@@ -21,15 +22,13 @@ import What4.Protocol.SMTLib2
          (assume, sessionWriter, runCheckSat)
 
 
-data BuilderState st = EmptyState
-
 z3executable :: FilePath
 z3executable = "z3"
 
 main :: IO ()
 main = do
   Some ng <- newIONonceGenerator
-  sym <- newExprBuilder FloatIEEERepr EmptyState ng
+  sym <- newExprBuilder FloatIEEERepr EmptyExprBuilderState ng
 
   -- This line is necessary for working with z3.
   extendConfig z3Options (getConfiguration sym)
diff --git a/what4/test/AdapterTest.hs b/what4/test/AdapterTest.hs
index 64aa67b31..aab1d411b 100644
--- a/what4/test/AdapterTest.hs
+++ b/what4/test/AdapterTest.hs
@@ -39,8 +39,6 @@ import           What4.Protocol.SMTWriter ( parserStrictness, ResponseStrictness
 import           What4.Protocol.VerilogWriter
 import           What4.Solver
 
-data State t = State
-
 allAdapters :: [SolverAdapter State]
 allAdapters =
   [ cvc4Adapter
@@ -61,13 +59,16 @@ drealAdpt = []
 #endif
 
 
-withSym :: SolverAdapter State -> (forall t . ExprBuilder t State (Flags FloatUninterpreted) -> IO a) -> IO a
+withSym ::
+  SolverAdapter EmptyBuilderState ->
+  (forall t . ExprBuilder t EmptyBuilderState (Flags FloatUninterpreted) -> IO a) ->
+  IO a
 withSym adpt pred_gen = withIONonceGenerator $ \gen ->
-  do sym <- newExprBuilder FloatUninterpretedRepr State gen
+  do sym <- newExprBuilder FloatUninterpretedRepr EmptyBuilderState gen
      extendConfig (solver_adapter_config_options adpt) (getConfiguration sym)
      pred_gen sym
 
-mkSmokeTest :: SolverAdapter State -> TestTree
+mkSmokeTest :: SolverAdapter EmptyBuilderState -> TestTree
 mkSmokeTest adpt = testCase (solver_adapter_name adpt) $
   withSym adpt $ \sym ->
    do res <- smokeTest sym adpt
@@ -109,13 +110,13 @@ mkConfigTests adapters =
              show e)
           _ -> assertFailure $
                "Expected OptGetFailure exception but got: " <> show err
-    withAdapters :: [SolverAdapter State]
-                 -> (forall t . ExprBuilder t State (Flags FloatUninterpreted) -> IO a)
+    withAdapters :: [SolverAdapter EmptyBuilderState]
+                 -> (forall t . ExprBuilder t EmptyBuilderState (Flags FloatUninterpreted) -> IO a)
                  -> IO a
     withAdapters adptrs op = do
         (cfgs, _getDefAdapter) <- solverAdapterOptions adptrs
         withIONonceGenerator $ \gen ->
-          do sym <- newExprBuilder FloatUninterpretedRepr State gen
+          do sym <- newExprBuilder FloatUninterpretedRepr EmptyBuilderState gen
              extendConfig cfgs (getConfiguration sym)
              op sym
 
@@ -536,7 +537,7 @@ mkConfigTests adapters =
 
 ----------------------------------------------------------------------
 
-nonlinearRealTest :: SolverAdapter State -> TestTree
+nonlinearRealTest :: SolverAdapter EmptyBuilderState -> TestTree
 nonlinearRealTest adpt =
   let wrap = if solver_adapter_name adpt `elem` [ "ABC", "boolector", "stp" ]
              then expectFailBecause
@@ -579,7 +580,7 @@ nonlinearRealTest adpt =
                 ((-2) <= x2_y' && x2_y' <= (-1)) @? "correct bounds"
 
 
-mkQuickstartTest :: SolverAdapter State -> TestTree
+mkQuickstartTest :: SolverAdapter EmptyBuilderState -> TestTree
 mkQuickstartTest adpt =
   let wrap = if solver_adapter_name adpt == "stp"
              then ignoreTestBecause "STP cannot generate the model"
@@ -638,7 +639,7 @@ mkQuickstartTest adpt =
 
 verilogTest :: TestTree
 verilogTest = testCase "verilogTest" $ withIONonceGenerator $ \gen ->
-  do sym <- newExprBuilder FloatUninterpretedRepr State gen
+  do sym <- newExprBuilder FloatUninterpretedRepr EmptyBuilderState gen
      let w = knownNat @8
      x <- freshConstant sym (safeSymbol "x") (BaseBVRepr w)
      one <- bvLit sym w (mkBV w 1)
diff --git a/what4/test/ExprBuilderSMTLib2.hs b/what4/test/ExprBuilderSMTLib2.hs
index ad37391bc..fb2995db5 100644
--- a/what4/test/ExprBuilderSMTLib2.hs
+++ b/what4/test/ExprBuilderSMTLib2.hs
@@ -52,10 +52,9 @@ import qualified What4.Solver.Yices as Yices
 import           What4.Utils.StringLiteral
 import           What4.Utils.Versions (ver, SolverBounds(..), emptySolverBounds)
 
-data State t = State
 data SomePred = forall t . SomePred (BoolExpr t)
 deriving instance Show SomePred
-type SimpleExprBuilder t fs = ExprBuilder t State fs
+type SimpleExprBuilder t fs = ExprBuilder t EmptyExprBuilderState fs
 
 instance TestShow Text.Text where testShow = show
 instance TestShow (StringLiteral Unicode) where testShow = show
@@ -76,7 +75,7 @@ userSymbol' s = case userSymbol s of
 
 withSym :: FloatModeRepr fm -> (forall t . SimpleExprBuilder t (Flags fm) -> IO a) -> IO a
 withSym floatMode pred_gen = withIONonceGenerator $ \gen ->
-  pred_gen =<< newExprBuilder floatMode State gen
+  pred_gen =<< newExprBuilder floatMode EmptyExprBuilderState gen
 
 withYices :: (forall t. SimpleExprBuilder t (Flags FloatReal) -> SolverProcess t Yices.Connection -> IO ()) -> IO ()
 withYices action = withSym FloatRealRepr $ \sym ->
@@ -90,7 +89,7 @@ withYices action = withSym FloatRealRepr $ \sym ->
 
 withZ3 :: (forall t . SimpleExprBuilder t (Flags FloatIEEE) -> Session t Z3.Z3 -> IO ()) -> IO ()
 withZ3 action = withIONonceGenerator $ \nonce_gen -> do
-  sym <- newExprBuilder FloatIEEERepr State nonce_gen
+  sym <- newExprBuilder FloatIEEERepr EmptyExprBuilderState nonce_gen
   extendConfig Z3.z3Options (getConfiguration sym)
   Z3.withZ3 sym "z3" defaultLogData { logCallbackVerbose = (\_ -> putStrLn) } (action sym)
 
diff --git a/what4/test/ExprsTest.hs b/what4/test/ExprsTest.hs
index e8c8d4032..dfa7919c8 100644
--- a/what4/test/ExprsTest.hs
+++ b/what4/test/ExprsTest.hs
@@ -33,13 +33,11 @@ import           What4.Concrete
 import           What4.Expr
 import           What4.Interface
 
-
-data State t = State
-type IteExprBuilder t fs = ExprBuilder t State fs
+type IteExprBuilder t fs = ExprBuilder t EmptyExprBuilderState fs
 
 withTestSolver :: (forall t. IteExprBuilder t (Flags FloatIEEE) -> IO a) -> IO a
 withTestSolver f = withIONonceGenerator $ \nonce_gen ->
-  f =<< newExprBuilder FloatIEEERepr State nonce_gen
+  f =<< newExprBuilder FloatIEEERepr EmptyExprBuilderState nonce_gen
 
 
 -- | Test natDiv and natMod properties described at their declaration
diff --git a/what4/test/IteExprs.hs b/what4/test/IteExprs.hs
index a00061809..79197fae0 100644
--- a/what4/test/IteExprs.hs
+++ b/what4/test/IteExprs.hs
@@ -36,12 +36,11 @@ import           What4.Expr
 import           What4.Interface
 
 
-data State t = State
-type IteExprBuilder t fs = ExprBuilder t State fs
+type IteExprBuilder t fs = ExprBuilder t EmptyExprBuilderState fs
 
 withTestSolver :: (forall t. IteExprBuilder t (Flags FloatIEEE) -> IO a) -> IO a
 withTestSolver f = withIONonceGenerator $ \nonce_gen ->
-  f =<< newExprBuilder FloatIEEERepr State nonce_gen
+  f =<< newExprBuilder FloatIEEERepr EmptyExprBuilderState nonce_gen
 
 -- | What branch (arm) is expected from the ITE evaluation?
 data ExpITEArm = Then | Else
diff --git a/what4/test/OnlineSolverTest.hs b/what4/test/OnlineSolverTest.hs
index f2a54b04f..9aaf6f41f 100644
--- a/what4/test/OnlineSolverTest.hs
+++ b/what4/test/OnlineSolverTest.hs
@@ -50,8 +50,6 @@ import           What4.Protocol.SMTWriter
 import qualified What4.Protocol.SMTLib2 as SMT2
 import qualified What4.Solver.Yices as Yices
 
-data State t = State
-
 type SolverTestData = (SolverName, AnOnlineSolver, ProblemFeatures, [ConfigDesc], Maybe (ConfigOption BaseIntegerType))
 
 allOnlineSolvers :: [SolverTestData]
@@ -83,7 +81,7 @@ instance TCL.TestShow [PP.Doc ann] where
 mkSmokeTest :: (SolverTestData, SolverVersion) -> TestTree
 mkSmokeTest ((SolverName nm, AnOnlineSolver (_ :: Proxy s), features, opts, _), _) =
   testCase nm $ withIONonceGenerator $ \gen ->
-  do sym <- newExprBuilder FloatUninterpretedRepr State gen
+  do sym <- newExprBuilder FloatUninterpretedRepr EmptyBuilderState gen
      extendConfig opts (getConfiguration sym)
      proc <- startSolverProcess @s features Nothing sym
      let conn = solverConn proc
@@ -168,7 +166,7 @@ quickstartTest useFrames ((SolverName nm, AnOnlineSolver (Proxy :: Proxy s), fea
   in wrap $
   testCaseSteps nm $ \step ->
   withIONonceGenerator $ \gen ->
-  do sym <- newExprBuilder FloatUninterpretedRepr State gen
+  do sym <- newExprBuilder FloatUninterpretedRepr EmptyExprBuilderState gen
      extendConfig opts (getConfiguration sym)
 
      (p,q,r,f) <- mkFormula1 sym
@@ -256,7 +254,7 @@ longTimeTest :: SolverTestData -> Maybe Time -> IO Bool
 longTimeTest (SolverName nm, AnOnlineSolver (Proxy :: Proxy s), features, opts, mb'timeoutOpt) goal_tmo =
   TCL.withChecklist "timer tests" $
   withIONonceGenerator $ \gen ->
-  do sym <- newExprBuilder FloatUninterpretedRepr State gen
+  do sym <- newExprBuilder FloatUninterpretedRepr EmptyExprBuilderState gen
      extendConfig opts (getConfiguration sym)
 
      -- Configure a solver timeout in What4 if specified for this test.
diff --git a/what4/test/TestTemplate.hs b/what4/test/TestTemplate.hs
index e30dedf04..3d71e4aa0 100644
--- a/what4/test/TestTemplate.hs
+++ b/what4/test/TestTemplate.hs
@@ -38,6 +38,7 @@ import qualified What4.Protocol.Online as Online
 import           What4.Protocol.Online (SolverProcess(..), OnlineSolver(..))
 import qualified What4.Solver.CVC4 as CVC4
 
+import What4.Expr
 import What4.Expr.App (reduceApp)
 import What4.Expr.Builder
 import What4.Expr.GroundEval
@@ -53,8 +54,6 @@ import GHC.Stack
 
 --import Debug.Trace (trace)
 
-data State t = State
-
 
 
 main :: IO ()
@@ -66,7 +65,7 @@ main =
               (do r <- roundingModes
                   (Some <$> floatTemplates [r] 1 fpp))
 
-     sym <- newExprBuilder FloatIEEERepr State globalNonceGenerator
+     sym <- newExprBuilder FloatIEEERepr EmptyExprBuilderState globalNonceGenerator
 
      extendConfig CVC4.cvc4Options (getConfiguration sym)
      proc <- Online.startSolverProcess @(SMT2.Writer CVC4.CVC4) CVC4.cvc4Features Nothing sym

From d70e1f73aaedbe2b12028d9e3faf4026e9b7b5e3 Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Fri, 21 Jan 2022 10:57:50 -0800
Subject: [PATCH 3/4] haddock tweak

---
 what4/src/What4/Expr.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/what4/src/What4/Expr.hs b/what4/src/What4/Expr.hs
index 75514982b..ff97fcfd6 100644
--- a/what4/src/What4/Expr.hs
+++ b/what4/src/What4/Expr.hs
@@ -110,6 +110,6 @@ import What4.Expr.UnaryBV
 
 
 -- | A \"dummy\" data type that can be used for the
---   user state field of an @ExprBuilder@ when there
+--   user state field of an 'ExprBuilder' when there
 --   is no other interesting state to track.
 data EmptyExprBuilderState t = EmptyExprBuilderState

From f14b4a4fc7e9e0beffdaabfd71bb2117dce86c2a Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Fri, 21 Jan 2022 11:21:46 -0800
Subject: [PATCH 4/4] Test fixs

---
 what4/test/AdapterTest.hs      | 26 +++++++++++++-------------
 what4/test/OnlineSolverTest.hs |  2 +-
 2 files changed, 14 insertions(+), 14 deletions(-)

diff --git a/what4/test/AdapterTest.hs b/what4/test/AdapterTest.hs
index aab1d411b..ca669d645 100644
--- a/what4/test/AdapterTest.hs
+++ b/what4/test/AdapterTest.hs
@@ -39,7 +39,7 @@ import           What4.Protocol.SMTWriter ( parserStrictness, ResponseStrictness
 import           What4.Protocol.VerilogWriter
 import           What4.Solver
 
-allAdapters :: [SolverAdapter State]
+allAdapters :: [SolverAdapter EmptyExprBuilderState]
 allAdapters =
   [ cvc4Adapter
   , yicesAdapter
@@ -51,7 +51,7 @@ allAdapters =
 #endif
   ] <> drealAdpt
 
-drealAdpt :: [SolverAdapter State]
+drealAdpt :: [SolverAdapter EmptyExprBuilderState]
 #ifdef TEST_DREAL
 drealAdpt = [drealAdapter]
 #else
@@ -60,15 +60,15 @@ drealAdpt = []
 
 
 withSym ::
-  SolverAdapter EmptyBuilderState ->
-  (forall t . ExprBuilder t EmptyBuilderState (Flags FloatUninterpreted) -> IO a) ->
+  SolverAdapter EmptyExprBuilderState ->
+  (forall t . ExprBuilder t EmptyExprBuilderState (Flags FloatUninterpreted) -> IO a) ->
   IO a
 withSym adpt pred_gen = withIONonceGenerator $ \gen ->
-  do sym <- newExprBuilder FloatUninterpretedRepr EmptyBuilderState gen
+  do sym <- newExprBuilder FloatUninterpretedRepr EmptyExprBuilderState gen
      extendConfig (solver_adapter_config_options adpt) (getConfiguration sym)
      pred_gen sym
 
-mkSmokeTest :: SolverAdapter EmptyBuilderState -> TestTree
+mkSmokeTest :: SolverAdapter EmptyExprBuilderState -> TestTree
 mkSmokeTest adpt = testCase (solver_adapter_name adpt) $
   withSym adpt $ \sym ->
    do res <- smokeTest sym adpt
@@ -79,7 +79,7 @@ mkSmokeTest adpt = testCase (solver_adapter_name adpt) $
 
 ----------------------------------------------------------------------
 
-mkConfigTests :: [SolverAdapter State] -> [TestTree]
+mkConfigTests :: [SolverAdapter EmptyExprBuilderState] -> [TestTree]
 mkConfigTests adapters =
   [
     testGroup "deprecated configs" (deprecatedConfigTests adapters)
@@ -110,13 +110,13 @@ mkConfigTests adapters =
              show e)
           _ -> assertFailure $
                "Expected OptGetFailure exception but got: " <> show err
-    withAdapters :: [SolverAdapter EmptyBuilderState]
-                 -> (forall t . ExprBuilder t EmptyBuilderState (Flags FloatUninterpreted) -> IO a)
+    withAdapters :: [SolverAdapter EmptyExprBuilderState]
+                 -> (forall t . ExprBuilder t EmptyExprBuilderState (Flags FloatUninterpreted) -> IO a)
                  -> IO a
     withAdapters adptrs op = do
         (cfgs, _getDefAdapter) <- solverAdapterOptions adptrs
         withIONonceGenerator $ \gen ->
-          do sym <- newExprBuilder FloatUninterpretedRepr EmptyBuilderState gen
+          do sym <- newExprBuilder FloatUninterpretedRepr EmptyExprBuilderState gen
              extendConfig cfgs (getConfiguration sym)
              op sym
 
@@ -537,7 +537,7 @@ mkConfigTests adapters =
 
 ----------------------------------------------------------------------
 
-nonlinearRealTest :: SolverAdapter EmptyBuilderState -> TestTree
+nonlinearRealTest :: SolverAdapter EmptyExprBuilderState -> TestTree
 nonlinearRealTest adpt =
   let wrap = if solver_adapter_name adpt `elem` [ "ABC", "boolector", "stp" ]
              then expectFailBecause
@@ -580,7 +580,7 @@ nonlinearRealTest adpt =
                 ((-2) <= x2_y' && x2_y' <= (-1)) @? "correct bounds"
 
 
-mkQuickstartTest :: SolverAdapter EmptyBuilderState -> TestTree
+mkQuickstartTest :: SolverAdapter EmptyExprBuilderState -> TestTree
 mkQuickstartTest adpt =
   let wrap = if solver_adapter_name adpt == "stp"
              then ignoreTestBecause "STP cannot generate the model"
@@ -639,7 +639,7 @@ mkQuickstartTest adpt =
 
 verilogTest :: TestTree
 verilogTest = testCase "verilogTest" $ withIONonceGenerator $ \gen ->
-  do sym <- newExprBuilder FloatUninterpretedRepr EmptyBuilderState gen
+  do sym <- newExprBuilder FloatUninterpretedRepr EmptyExprBuilderState gen
      let w = knownNat @8
      x <- freshConstant sym (safeSymbol "x") (BaseBVRepr w)
      one <- bvLit sym w (mkBV w 1)
diff --git a/what4/test/OnlineSolverTest.hs b/what4/test/OnlineSolverTest.hs
index 9aaf6f41f..3b3d8a911 100644
--- a/what4/test/OnlineSolverTest.hs
+++ b/what4/test/OnlineSolverTest.hs
@@ -81,7 +81,7 @@ instance TCL.TestShow [PP.Doc ann] where
 mkSmokeTest :: (SolverTestData, SolverVersion) -> TestTree
 mkSmokeTest ((SolverName nm, AnOnlineSolver (_ :: Proxy s), features, opts, _), _) =
   testCase nm $ withIONonceGenerator $ \gen ->
-  do sym <- newExprBuilder FloatUninterpretedRepr EmptyBuilderState gen
+  do sym <- newExprBuilder FloatUninterpretedRepr EmptyExprBuilderState gen
      extendConfig opts (getConfiguration sym)
      proc <- startSolverProcess @s features Nothing sym
      let conn = solverConn proc