diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,3 +1,12 @@
+# 1.7.1 (November 2025)
+
+* Add `asGround :: IsExpr e => e tp -> Maybe (GroundValue tp)`
+* Add `What4.Concretize`, a module for concretizing symbolic values using models
+  from solvers.
+* Expose `ExprBuilder`'s uninterpreted function cache
+* Fix a bug in which `sbvToInteger` could erroneously throw an `arithmetic
+  underflow` exception when called on a length-1 signed bitvector.
+
 # 1.7 (March 2025)
 
 * The `BoolMap` parameter of `ConjPred` is now a `ConjMap`. This is a `newtype`
diff --git a/src/What4/BaseTypes.hs b/src/What4/BaseTypes.hs
--- a/src/What4/BaseTypes.hs
+++ b/src/What4/BaseTypes.hs
@@ -22,6 +22,7 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
@@ -30,6 +31,7 @@
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
+
 module What4.BaseTypes
   ( -- * BaseType data kind
     type BaseType
@@ -289,13 +291,19 @@
 instance ShowF BaseTypeRepr
 
 instance Pretty (FloatPrecisionRepr fpp) where
-  pretty = viaShow
+  pretty (FloatingPointPrecisionRepr exp' sig) = 
+    parens ("FloatingPrecision" <+> (pretty $ natValue exp') <+> (pretty $ natValue sig))
+
 instance Show (FloatPrecisionRepr fpp) where
   showsPrec = $(structuralShowsPrec [t|FloatPrecisionRepr|])
 instance ShowF FloatPrecisionRepr
 
+-- | Prints string type reprs, matching the syntax of crucible atoms https://github.com/GaloisInc/crucible/blob/a2502010cab0de44ec4c3b802453dc1009181d6b/crucible-syntax/src/Lang/Crucible/Syntax/Atoms.hs#L148-L151
 instance Pretty (StringInfoRepr si) where
-  pretty = viaShow
+  pretty UnicodeRepr = "Unicode"
+  pretty Char16Repr = "Char16"
+  pretty Char8Repr = "Char8"
+
 instance Show (StringInfoRepr si) where
   showsPrec = $(structuralShowsPrec [t|StringInfoRepr|])
 instance ShowF StringInfoRepr
diff --git a/src/What4/Concretize.hs b/src/What4/Concretize.hs
new file mode 100644
--- /dev/null
+++ b/src/What4/Concretize.hs
@@ -0,0 +1,118 @@
+-----------------------------------------------------------------------
+-- |
+-- Module           : What4.Concretize
+-- Description      : Concretize values
+-- Copyright        : (c) Galois, Inc 2024
+-- License          : BSD3
+-- Maintainer       : Langston Barrett <langston@galois.com>
+-- Stability        : provisional
+--
+-- In our terminology, concretization is the process of (1) obtaining a
+-- model from an SMT solver and (2) requesting the value of a particular set
+-- of symbolic expressions in said model. The operation (2) alone is called
+-- "grounding", see "What4.GroundEval".
+-----------------------------------------------------------------------
+
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeOperators #-}
+
+module What4.Concretize
+  ( ConcretizationFailure(..)
+  , concretize
+  , UniqueConcretizationFailure(..)
+  , uniquelyConcretize
+  ) where
+
+import qualified What4.Expr.Builder as WEB
+import qualified What4.Expr.GroundEval as WEG
+import qualified What4.Interface as WI
+import qualified What4.Protocol.Online as WPO
+import qualified What4.Protocol.SMTWriter as WPS
+import qualified What4.SatResult as WSat
+
+-- | Reasons why attempting to resolve a symbolic expression as ground can fail.
+data ConcretizationFailure
+  = SolverUnknown
+    -- ^ Querying the SMT solver yielded @UNKNOWN@.
+  | UnsatInitialAssumptions
+    -- ^ Querying the SMT solver for an initial model of the expression failed
+    -- due to the initial assumptions in scope being unsatisfiable.
+  deriving Show
+
+-- | Get a 'WEG.GroundValue' for a 'WI.SymExpr' by asking an online solver for
+-- a model.
+--
+-- In contrast with 'uniquelyConcretize', this function returns the value of the
+-- 'WI.SymExpr' in just one of potentially many distinct models. See the Haddock
+-- on 'uniquelyConcretize' for a further comparison.
+concretize ::
+  ( sym ~ WEB.ExprBuilder scope st fs
+  , WPO.OnlineSolver solver
+  ) =>
+  WPO.SolverProcess scope solver ->
+  -- | The symbolic term to query from the model
+  WI.SymExpr sym tp ->
+  IO (Either ConcretizationFailure (WEG.GroundValue tp))
+concretize sp val =
+  case WEG.asGround val of
+    Just gVal -> pure (Right gVal)
+    Nothing -> do
+      WPO.inNewFrame sp $ do
+        msat <- WPO.checkAndGetModel sp "Ground value using model"
+        case msat of
+          WSat.Unknown -> pure $ Left SolverUnknown
+          WSat.Unsat {} -> pure $ Left UnsatInitialAssumptions
+          WSat.Sat mdl -> Right <$> WEG.groundEval mdl val
+
+data UniqueConcretizationFailure
+  = GroundingFailure ConcretizationFailure
+  | MultipleModels
+    -- ^ There are multiple possible models for the expression, which means it
+    -- is truly symbolic and therefore unable to be uniquely concretized.
+  deriving Show
+
+-- | Attempt to resolve the given 'WI.SymExpr' to a unique concrete value using
+-- an online SMT solver connection.
+--
+-- The implementation of this function (1) asks for a model from the solver.
+-- If it gets one, it (2) adds a blocking clause and asks for another. If there
+-- was only one model, concretize the initial value and return it with 'Right'.
+-- Otherwise, return an explanation of why concretization failed with 'Left'.
+-- This behavior is contrasted with 'concretize', which just does (1).
+uniquelyConcretize ::
+  ( sym ~ WEB.ExprBuilder scope st fs
+  , WPO.OnlineSolver solver
+  ) =>
+  -- | The symbolic backend
+  sym ->
+  WPO.SolverProcess scope solver ->
+  -- | The symbolic term to concretize
+  WI.SymExpr sym tp ->
+  IO (Either UniqueConcretizationFailure (WEG.GroundValue tp))
+uniquelyConcretize sym sp val =
+  case WEG.asGround val of
+    Just gVal -> pure (Right gVal)
+    Nothing -> do
+      -- First, check to see if there is a model of the symbolic value.
+      concVal_ <- concretize sp val
+      case concVal_ of
+        Left e -> pure (Left (GroundingFailure e))
+        Right concVal -> do
+          -- We found a model, so check to see if this is the only possible
+          -- model for this symbolic value.  We do this by adding a blocking
+          -- clause that assumes the `SymExpr` is /not/ equal to the model we
+          -- found in the previous step. If this is unsatisfiable, the SymExpr
+          -- can only be equal to that model, so we can conclude it is concrete.
+          -- If it is satisfiable, on the other hand, the `SymExpr` can be
+          -- multiple values, so it is truly symbolic.
+          WPO.inNewFrame sp $ do
+            injectedConcVal <- WEG.groundToSym sym (WI.exprType val) concVal
+            eq <- WI.isEq sym val injectedConcVal
+            block <- WI.notPred sym eq
+            WPS.assume (WPO.solverConn sp) block
+            msat' <- WPO.checkAndGetModel sp "Concretize value (with blocking clause)"
+            case msat' of
+              WSat.Unknown -> pure $ Left $ GroundingFailure $ SolverUnknown
+              WSat.Sat _mdl -> pure $ Left $ MultipleModels
+              WSat.Unsat {} -> pure $ Right concVal -- There is a single concrete result
diff --git a/src/What4/Expr/Builder.hs b/src/What4/Expr/Builder.hs
--- a/src/What4/Expr/Builder.hs
+++ b/src/What4/Expr/Builder.hs
@@ -80,6 +80,7 @@
   , stopCaching
   , exprBuilderSplitConfig
   , exprBuilderFreshConfig
+  , uninterpFnCache, UninterpFunCache
 
     -- * Specialized representations
   , bvUnary
@@ -414,7 +415,7 @@
 
         , sbVarBindings :: !(IORef (SymbolVarBimap t))
 
-        , sbUninterpFnCache :: !(IORef (Map (SolverSymbol, Some (Ctx.Assignment BaseTypeRepr)) (SomeSymFn (ExprBuilder t st fs))))
+        , sbUninterpFnCache :: !(IORef (UninterpFunCache t st fs))
 
           -- | Cache for Matlab functions
         , sbMatlabFnCache :: !(PH.HashTable RealWorld (MatlabFnWrapper t) (ExprSymFnWrapper t))
@@ -426,6 +427,11 @@
         , sbFloatMode :: !(FloatModeRepr fm)
         }
 
+-- | Keep track of uninterpred functions we've already made
+type UninterpFunCache t st fs =
+  Map SolverSymbol (PM.MapF (Assignment BaseTypeRepr)
+                            (SymFnWrapper (ExprBuilder t st fs)))
+
 type instance SymFn (ExprBuilder t st fs) = ExprSymFn t
 type instance SymExpr (ExprBuilder t st fs) = Expr t
 type instance BoundVar (ExprBuilder t st fs) = ExprBoundVar t
@@ -446,6 +452,9 @@
 pushMuxOps :: Getter (ExprBuilder t st fs) (CFG.OptionSetting BaseBoolType)
 pushMuxOps = to sbPushMuxOps
 
+uninterpFnCache :: Getter (ExprBuilder t st fs) (IORef (UninterpFunCache t st fs))
+uninterpFnCache = to sbUninterpFnCache
+
 -- | Return a new expr builder where the configuration object has
 --   been "split" using the @splitConfig@ operation.
 --   The returned sym will share any preexisting options with the
@@ -1655,54 +1664,74 @@
   Expr t (SR.SemiRingBase sr) ->
   IO (Expr t (SR.SemiRingBase sr))
 semiRingIte sym sr c x y
-    -- evaluate as constants
-  | Just True  <- asConstantPred c = return x
-  | Just False <- asConstantPred c = return y
-
-    -- reduce negations
-  | Just (NotPred c') <- asApp c
+  | Just (IteNot c') <- reduceIte c x y
   = semiRingIte sym sr c' y x
-
-    -- remove the ite if the then and else cases are the same
-  | x == y = return x
+  | Just (IteReduced e) <- reduceIte c x y
+  = return e
 
     -- Try to extract common sum information.
   | (z, x',y') <- WSum.extractCommon (asWeightedSum sr x) (asWeightedSum sr y)
   , not (WSum.isZero sr z) = do
     xr <- semiRingSum sym x'
     yr <- semiRingSum sym y'
-    let sz = 1 + iteSize xr + iteSize yr
-    r <- sbMakeExpr sym (BaseIte (SR.semiRingBase sr) sz c xr yr)
+    r <- baseIte sym c xr yr
     semiRingSum sym $! WSum.addVar sr z r
 
     -- final fallback, create the ite term
-  | otherwise =
-      let sz = 1 + iteSize x + iteSize y in
-      sbMakeExpr sym (BaseIte (SR.semiRingBase sr) sz c x y)
+  | otherwise
+  = baseIte sym c x y
 
+data ReduceIteResult t bt
+  = -- | We had @ite (not p)@, so reverse the branches and try again
+    IteNot (Expr t BaseBoolType)
+  | IteReduced (Expr t bt)
 
-mkIte ::
-  ExprBuilder t st fs ->
+-- | Perform common rewrites on @ite@ expressions
+reduceIte ::
   Expr t BaseBoolType ->
   Expr t bt ->
   Expr t bt ->
-  IO (Expr t bt)
-mkIte sym c x y
-    -- evaluate as constants
-  | Just True  <- asConstantPred c = return x
-  | Just False <- asConstantPred c = return y
+  Maybe (ReduceIteResult t bt)
+reduceIte c x y
+  | Just b <- asConstantPred c
+  = if b then Just (IteReduced x) else Just (IteReduced y)
 
-    -- reduce negations
-  | Just (NotPred c') <- asApp c
-  = mkIte sym c' y x
+  -- remove the ite if the then and else cases are the same
+  | x == y
+  = Just (IteReduced x)
 
-    -- remove the ite if the then and else cases are the same
-  | x == y = return x
+  | Just (NotPred c') <- asApp c
+  = Just (IteNot c')
 
   | otherwise =
-      let sz = 1 + iteSize x + iteSize y in
-      sbMakeExpr sym (BaseIte (exprType x) sz c x y)
+    Nothing
 
+mkIte ::
+  ExprBuilder t st fs ->
+  Expr t BaseBoolType ->
+  Expr t bt ->
+  Expr t bt ->
+  IO (Expr t bt)
+mkIte sym c x y =
+  case reduceIte c x y of
+    Just (IteNot c') -> baseIte sym c' y x
+    Just (IteReduced e) -> pure e
+    Nothing -> baseIte sym c x y
+
+-- | Construct 'BaseIte'.
+--
+-- 'Ex.assert's that the if-then-else is not trivially reducible.
+baseIte ::
+  ExprBuilder t st fs ->
+  Expr t BaseBoolType ->
+  Expr t x ->
+  Expr t x ->
+  IO (Expr t x)
+baseIte sym c x y =
+  Ex.assert (isNothing (reduceIte c x y)) $ do
+    let sz = 1 + iteSize x + iteSize y
+    sbMakeExpr sym $ BaseIte (exprType x) sz c x y
+
 semiRingLe ::
   ExprBuilder t st fs ->
   SR.OrderedSemiRingRepr sr ->
@@ -1753,7 +1782,10 @@
  where sr = SR.orderedSemiRing osr
 
 
+-- Note: requires that the equality is not trivially reducible, and asserts as
+-- much (by calling 'baseEq').
 semiRingEq ::
+  Abstractable (SR.SemiRingBase sr) =>
   ExprBuilder t st fs ->
   SR.SemiRingRepr sr ->
   (Expr t (SR.SemiRingBase sr) -> Expr t (SR.SemiRingBase sr) -> IO (Expr t BaseBoolType))
@@ -1762,9 +1794,6 @@
   Expr t (SR.SemiRingBase sr) ->
   IO (Expr t BaseBoolType)
 semiRingEq sym sr rec x y
-  -- Check for syntactic equality.
-  | x == y = return (truePred sym)
-
     -- Push some equalities under if/then/else
   | SemiRingLiteral _ _ _ <- x
   , Just (BaseIte _ _ c a b) <- asApp y
@@ -1781,10 +1810,9 @@
       (Just a, Just b) -> return $! backendPred sym (SR.eq sr a b)
       _ -> do xr <- semiRingSum sym x'
               yr <- semiRingSum sym y'
-              sbMakeExpr sym $ BaseEq (SR.semiRingBase sr) (min xr yr) (max xr yr)
+              baseEq sym xr yr
 
-  | otherwise =
-    sbMakeExpr sym $ BaseEq (SR.semiRingBase sr) (min x y) (max x y)
+  | otherwise = baseEq sym x y
 
 semiRingAdd ::
   forall t st fs sr.
@@ -2079,8 +2107,8 @@
     = sbMakeExpr sym (NotPred x)
 
   eqPred sym x y
-    | x == y
-    = return (truePred sym)
+    | Just b <- checkEq x y
+    = return $ backendPred sym b
 
     | Just (NotPred x') <- asApp x
     = xorPred sym x' y
@@ -2094,7 +2122,7 @@
         (Just True, _)     -> return y
         (_, Just False)    -> notPred sym x
         (_, Just True)     -> return x
-        _ -> sbMakeExpr sym $ BaseEq BaseBoolRepr (min x y) (max x y)
+        _ -> baseEq sym x y
 
   xorPred sym x y = notPred sym =<< eqPred sym x y
 
@@ -2159,24 +2187,15 @@
      = notPred sym =<< conjPred sym (BM.ConjMap (BM.fromVars [asNegAtom a, asNegAtom b]))
 
   itePred sb c x y
+    | Just (IteNot c') <- reduceIte c x y = itePred sb c' y x
+    | Just (IteReduced e) <- reduceIte c x y = return e
+
       -- ite c c y = c || y
     | c == x = orPred sb c y
 
       -- ite c x c = c && x
     | c == y = andPred sb c x
 
-      -- ite c x x = x
-    | x == y = return x
-
-      -- ite 1 x y = x
-    | Just True  <- asConstantPred c = return x
-
-      -- ite 0 x y = y
-    | Just False <- asConstantPred c = return y
-
-      -- ite !c x y = ite c y x
-    | Just (NotPred c') <- asApp c = itePred sb c' y x
-
       -- ite c 1 y = c || y
     | Just True  <- asConstantPred x = orPred sb c y
 
@@ -2190,9 +2209,7 @@
     | Just False <- asConstantPred y = andPred sb c x
 
       -- Default case
-    | otherwise =
-        let sz = 1 + iteSize x + iteSize y in
-        sbMakeExpr sb $ BaseIte BaseBoolRepr sz c x y
+    | otherwise = baseIte sb c x y
 
   ----------------------------------------------------------------------
   -- Integer operations.
@@ -2208,8 +2225,7 @@
   intIte sym c x y = semiRingIte sym SR.SemiRingIntegerRepr c x y
 
   intEq sym x y
-      -- Use range check
-    | Just b <- rangeCheckEq (exprAbsValue x) (exprAbsValue y)
+    | Just b <- checkEq x y
     = return $ backendPred sym b
 
       -- Reduce to bitvector equality, when possible
@@ -2705,6 +2721,9 @@
     | otherwise = sbMakeExpr sym $ BVFill w p
 
   bvIte sym c x y
+    | Just (IteNot c') <- reduceIte c x y = bvIte sym c' y x
+    | Just (IteReduced e) <- reduceIte c x y = return e
+
     | Just (BVFill w px) <- asApp x
     , Just (BVFill _w py) <- asApp y =
       do z <- itePred sym c px py
@@ -2740,18 +2759,16 @@
                 Just (Some flv) ->
                   semiRingIte sym (SR.SemiRingBVRepr flv (bvWidth x)) c x y
                 Nothing ->
-                  mkIte sym c x y)
+                  baseIte sym c x y)
 
   bvEq sym x y
-    | x == y = return $! truePred sym
+    | Just b <- checkEq x y
+    = return $ backendPred sym b
 
     | Just (BVFill _ px) <- asApp x
     , Just (BVFill _ py) <- asApp y =
       eqPred sym px py
 
-    | Just b <- BVD.eq (exprAbsValue x) (exprAbsValue y) = do
-      return $! backendPred sym b
-
     -- Push some equalities under if/then/else
     | SemiRingLiteral _ _ _ <- x
     , Just (BaseIte _ _ c a b) <- asApp y
@@ -2772,7 +2789,7 @@
           (Just a, Just b) -> return $! backendPred sym (SR.eq sr a b)
           _ -> do xr <- semiRingSum sym x'
                   yr <- semiRingSum sym y'
-                  sbMakeExpr sym $ BaseEq (SR.semiRingBase sr) (min xr yr) (max xr yr)
+                  baseEq sym xr yr
 
     | otherwise = do
         ut <- CFG.getOpt (sbUnaryThreshold sym)
@@ -2781,7 +2798,7 @@
            , Just uy <- asUnaryBV sym y
            -> UnaryBV.eq sym ux uy
            | otherwise
-           -> sbMakeExpr sym $ BaseEq (BaseBVRepr (bvWidth x)) (min x y) (max x y)
+           -> baseEq sym x y
 
   bvSlt sym x y
     | Just xc <- asBV x
@@ -3228,11 +3245,7 @@
         BaseStructRepr flds ->
           sbMakeExpr sym $ StructField s i (flds Ctx.! i)
 
-  structIte sym p x y
-    | Just True  <- asConstantPred p = return x
-    | Just False <- asConstantPred p = return y
-    | x == y                         = return x
-    | otherwise                      = mkIte sym p x y
+  structIte = mkIte
 
   --------------------------------------------------------------------
   -- String operations
@@ -3243,23 +3256,9 @@
     do l <- curProgramLoc sym
        return $! StringExpr s l
 
-  stringEq sym x y
-    | Just x' <- asString x
-    , Just y' <- asString y
-    = return $! backendPred sym (isJust (testEquality x' y'))
-  stringEq sym x y
-    = sbMakeExpr sym $ BaseEq (BaseStringRepr (stringInfo x)) x y
+  stringEq = mkEq
 
-  stringIte _sym c x y
-    | Just c' <- asConstantPred c
-    = if c' then return x else return y
-  stringIte _sym _c x y
-    | Just x' <- asString x
-    , Just y' <- asString y
-    , isJust (testEquality x' y')
-    = return x
-  stringIte sym c x y
-    = mkIte sym c x y
+  stringIte = mkIte
 
   stringIndexOf sym x y k
     | Just x' <- asString x
@@ -3460,34 +3459,33 @@
      else
       sbMakeExpr sym $ ArrayMap idx_tps baseRepr new_map def_map
 
-  arrayIte sym p x y = do
-    pmo <- CFG.getOpt (sbPushMuxOps sym)
-    if   -- Extract all concrete updates out.
-       | not pmo
-       , ArrayMapView mx x' <- viewArrayMap x
-       , ArrayMapView my y' <- viewArrayMap y
-       , not (AUM.null mx) || not (AUM.null my) -> do
-         case exprType x of
-           BaseArrayRepr idxRepr bRepr -> do
-             let both_fn _ u v = baseTypeIte sym p u v
-                 left_fn idx u = do
-                   v <- sbConcreteLookup sym y' (Just idx) =<< symbolicIndices sym idx
-                   both_fn idx u v
-                 right_fn idx v = do
-                   u <- sbConcreteLookup sym x' (Just idx) =<< symbolicIndices sym idx
-                   both_fn idx u v
-             mz <- AUM.mergeM bRepr both_fn left_fn right_fn mx my
-             z' <- arrayIte sym p x' y'
+  arrayIte sym p x y
+    | Just (IteNot p') <- reduceIte p x y = arrayIte sym p' y x
+    | Just (IteReduced e) <- reduceIte p x y = return e
+    | otherwise = do
+        pmo <- CFG.getOpt (sbPushMuxOps sym)
+        if   -- Extract all concrete updates out.
+           | not pmo
+           , ArrayMapView mx x' <- viewArrayMap x
+           , ArrayMapView my y' <- viewArrayMap y
+           , not (AUM.null mx) || not (AUM.null my) -> do
+             case exprType x of
+               BaseArrayRepr idxRepr bRepr -> do
+                 let both_fn _ u v = baseTypeIte sym p u v
+                     left_fn idx u = do
+                       v <- sbConcreteLookup sym y' (Just idx) =<< symbolicIndices sym idx
+                       both_fn idx u v
+                     right_fn idx v = do
+                       u <- sbConcreteLookup sym x' (Just idx) =<< symbolicIndices sym idx
+                       both_fn idx u v
+                 mz <- AUM.mergeM bRepr both_fn left_fn right_fn mx my
+                 z' <- arrayIte sym p x' y'
 
-             sbMakeExpr sym $ ArrayMap idxRepr bRepr mz z'
+                 sbMakeExpr sym $ ArrayMap idxRepr bRepr mz z'
 
-       | otherwise -> mkIte sym p x y
+           | otherwise -> baseIte sym p x y
 
-  arrayEq sym x y
-    | x == y =
-      return $! truePred sym
-    | otherwise =
-      sbMakeExpr sym $! BaseEq (exprType x) x y
+  arrayEq = mkEq
 
   arrayTrueOnEntries sym f a
     | Just True <- exprAbsValue a =
@@ -3625,8 +3623,7 @@
   realZero = sbZero
 
   realEq sym x y
-      -- Use range check
-    | Just b <- ravCheckEq (exprAbsValue x) (exprAbsValue y)
+    | Just b <- checkEq x y
     = return $ backendPred sym b
 
       -- Reduce to integer equality, when possible
@@ -4639,18 +4636,14 @@
   -> IO (SymFn sym args ret)
 cachedUninterpFn sym fn_name arg_types ret_type handler = do
   fn_cache <- readIORef $ sbUninterpFnCache sym
-  case Map.lookup fn_key fn_cache of
-    Just (SomeSymFn fn)
-      | Just Refl <- testEquality (fnArgTypes fn) arg_types
-      , Just Refl <- testEquality (fnReturnType fn) ret_type
-      -> return fn
-      | otherwise
-      -> fail "Duplicate uninterpreted function declaration."
+  case Map.lookup fn_name fn_cache >>= PM.lookup (arg_types Ctx.:> ret_type) of
+    Just (SymFnWrapper fn) -> pure fn
     Nothing -> do
       fn <- handler sym fn_name arg_types ret_type
-      atomicModifyIORef' (sbUninterpFnCache sym) (\m -> (Map.insert fn_key (SomeSymFn fn) m, ()))
+      let updArgs  = PM.insert (arg_types Ctx.:> ret_type) (SymFnWrapper fn)
+          updCache = Map.alter (Just . updArgs . fromMaybe PM.empty) fn_name
+      _ <- atomicModifyIORef' (sbUninterpFnCache sym) (\m -> (updCache m, ()))
       return fn
-  where fn_key =  (fn_name, Some (arg_types Ctx.:> ret_type))
 
 mkUninterpFnApp
   :: (sym ~ ExprBuilder t st fs)
@@ -4677,3 +4670,56 @@
   let arg_types = fmapFC exprType args
   fn <- freshTotalUninterpFn sym fn_name arg_types ret_type
   applySymFn sym fn args
+
+-- | Check if two symbolic values are known to be equal (@Just True@) or known
+-- to be unequal (@Just False@).
+checkEq ::
+  Abstractable x =>
+  Expr t x ->
+  Expr t x ->
+  Maybe Bool
+checkEq x y
+  | x == y = Just True
+
+  | Just x' <- asConcrete x
+  , Just y' <- asConcrete y = Just (x' == y')
+
+  | otherwise
+  = avCheckEq (exprType x) (exprAbsValue x) (exprAbsValue y)
+-- This function is inlined into contexts where the type is known, hence it will
+-- be specialized.
+{-# INLINE checkEq #-}
+
+mkEq ::
+  Abstractable x =>
+  ExprBuilder t st fs ->
+  Expr t x ->
+  Expr t x ->
+  IO (Expr t BaseBoolType)
+mkEq sym x y
+  | Just b <- checkEq x y
+  = return $ backendPred sym b
+
+  | otherwise
+  = sbMakeExpr sym $ BaseEq (exprType x) x y
+-- This function is inlined into contexts where the type is known, hence it will
+-- be specialized.
+{-# INLINE mkEq #-}
+
+-- | Construct 'BaseEq'.
+--
+-- Sorts the operands so that the lesser is the left hand side of the equality.
+-- This helps normalize equality expressions so that rewrites such as @x = y
+-- and x = y ==> true@ are more easily applied without worrying about symmetry
+-- of equality.
+--
+-- 'Ex.assert's that the two values are not easily known to be (dis)equal.
+baseEq ::
+  Abstractable x =>
+  ExprBuilder t st fs ->
+  Expr t x ->
+  Expr t x ->
+  IO (Expr t BaseBoolType)
+baseEq sym x y =
+  Ex.assert (isNothing (checkEq x y)) $
+    sbMakeExpr sym $ BaseEq (exprType x) (min x y) (max x y)
diff --git a/src/What4/Expr/GroundEval.hs b/src/What4/Expr/GroundEval.hs
--- a/src/What4/Expr/GroundEval.hs
+++ b/src/What4/Expr/GroundEval.hs
@@ -9,6 +9,8 @@
 --
 -- Given a collection of assignments to the symbolic values appearing in
 -- an expression, this module computes the ground value.
+--
+-- See also "What4.Concretize".
 ------------------------------------------------------------------------
 
 {-# LANGUAGE CPP #-}
@@ -24,8 +26,9 @@
 module What4.Expr.GroundEval
   ( -- * Ground evaluation
     GroundValue
-  , GroundValueWrapper(..)
+  , asGround
   , groundToSym
+  , GroundValueWrapper(..)
   , GroundArray(..)
   , lookupArray
   , GroundEvalFn(..)
@@ -82,6 +85,25 @@
   GroundValue (BaseStringType si)   = StringLiteral si
   GroundValue (BaseArrayType idx b) = GroundArray idx b
   GroundValue (BaseStructType ctx)  = Ctx.Assignment GroundValueWrapper ctx
+
+-- | Return a ground representation of a value, if it is ground.
+--
+-- c.f. 'What4.Interface.asConcrete'.
+asGround :: IsExpr e => e tp -> Maybe (GroundValue tp)
+asGround x =
+  case exprType x of
+    BaseBoolRepr       -> asConstantPred x
+    BaseIntegerRepr    -> asInteger x
+    BaseRealRepr       -> asRational x
+    BaseStringRepr _si -> asString x
+    BaseComplexRepr    -> asComplex x
+    BaseBVRepr _w       -> asBV x
+    BaseFloatRepr _fpp  -> asFloat x
+    BaseStructRepr _   -> asStruct x >>= traverseFC (fmap GVW . asGround)
+    BaseArrayRepr _idx _tp -> do
+      def <- asConstantArray x
+      groundDef <- asGround def
+      pure (ArrayConcrete groundDef Map.empty)
 
 -- | Inject a 'GroundValue' back into a 'SymExpr'.
 --
diff --git a/src/What4/Interface.hs b/src/What4/Interface.hs
--- a/src/What4/Interface.hs
+++ b/src/What4/Interface.hs
@@ -3199,6 +3199,8 @@
 
 -- | Return a concrete representation of a value, if it
 --   is concrete.
+--
+-- c.f. 'What4.GroundEval.asGround'.
 asConcrete :: IsExpr e => e tp -> Maybe (ConcreteVal tp)
 asConcrete x =
   case exprType x of
@@ -3218,6 +3220,8 @@
       pure (ConcreteArray idx c_def Map.empty)
 
 -- | Create a literal symbolic value from a concrete value.
+--
+-- c.f. 'What4.Expr.GroundEval.groundToSym'
 concreteToSym :: IsExprBuilder sym => sym -> ConcreteVal tp -> IO (SymExpr sym tp)
 concreteToSym sym = \case
    ConcreteBool True    -> return (truePred sym)
diff --git a/src/What4/Internal.hs b/src/What4/Internal.hs
new file mode 100644
--- /dev/null
+++ b/src/What4/Internal.hs
@@ -0,0 +1,25 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE TypeApplications #-}
+
+-- | Items in this module should /not/ be considered part of What4's API, they
+-- are exported only for the sake of the test suite.
+module What4.Internal
+  ( assertionsEnabled
+  ) where
+
+import qualified Control.Exception as X
+import           Data.Functor ((<&>))
+
+-- | Check if assertions are enabled.
+--
+-- Note [Asserts]: When optimizations are enabled, GHC compiles 'X.assert' to
+-- a no-op. However, Cabal enables @-O1@ by default. Therefore, if we want our
+-- assertions to be checked by our test suite, we must carefully ensure that we
+-- pass the correct flags to GHC for the @lib:what4@ target. We verify that we
+-- have done so by asserting as much in the test suite.
+assertionsEnabled :: IO Bool
+assertionsEnabled = do
+  X.try @X.AssertionFailed (X.assert False (pure ())) <&>
+    \case
+      Left _ -> True
+      Right () -> False
diff --git a/src/What4/InterpretedFloatingPoint.hs b/src/What4/InterpretedFloatingPoint.hs
--- a/src/What4/InterpretedFloatingPoint.hs
+++ b/src/What4/InterpretedFloatingPoint.hs
@@ -4,6 +4,7 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
@@ -99,8 +100,15 @@
 instance Hashable (FloatInfoRepr fi) where
   hashWithSalt = $(structuralHashWithSalt [t|FloatInfoRepr|] [])
 
+-- | Prints float type reprs, matching the atoms in crucible https://github.com/GaloisInc/crucible/blob/a2502010cab0de44ec4c3b802453dc1009181d6b/crucible-syntax/src/Lang/Crucible/Syntax/Atoms.hs#L153-L159
 instance Pretty (FloatInfoRepr fi) where
-  pretty = viaShow
+  pretty HalfFloatRepr =  "Half"
+  pretty SingleFloatRepr = "Float"
+  pretty DoubleFloatRepr = "Double"
+  pretty QuadFloatRepr = "Quad"
+  pretty X86_80FloatRepr = "X86_80"
+  pretty DoubleDoubleFloatRepr = "DoubleDouble"
+
 instance Show (FloatInfoRepr fi) where
   showsPrec = $(structuralShowsPrec [t|FloatInfoRepr|])
 instance ShowF FloatInfoRepr
diff --git a/src/What4/Protocol/SMTLib2/Parse.hs b/src/What4/Protocol/SMTLib2/Parse.hs
--- a/src/What4/Protocol/SMTLib2/Parse.hs
+++ b/src/What4/Protocol/SMTLib2/Parse.hs
@@ -42,18 +42,23 @@
 import           Control.Monad (when)
 import           Control.Monad.Reader (ReaderT(..))
 import qualified Data.ByteString as BS
-import qualified Data.ByteString.UTF8 as UTF8
 import           Data.Char
 import           Data.HashSet (HashSet)
 import qualified Data.HashSet as HSet
 import           Data.Ratio
 import           Data.String
+import qualified Data.Text as Text
+import           Data.Text.Encoding (decodeUtf8With)
+import           Data.Text.Encoding.Error (lenientDecode)
 import           Data.Word
 import           System.IO
 
 c2b :: Char -> Word8
 c2b = fromIntegral . fromEnum
 
+decode :: BS.ByteString -> String
+decode = Text.unpack . decodeUtf8With lenientDecode
+
 ------------------------------------------------------------------------
 -- Parser definitions
 
@@ -162,7 +167,7 @@
   matchChar '"'
   l <- takeChars (/= '"')
   matchChar '"'
-  pure $ UTF8.toString l
+  pure $ decode l
 
 -- | Defines common operations for parsing SMTLIB results.
 class CanParse a where
@@ -309,7 +314,7 @@
   case filter (\(m,_p) -> m == w) actions of
     [] -> do
       w' <- takeChars (\c -> c `notElem` ['\r', '\n'])
-      fail $ "Unsupported keyword: " ++ UTF8.toString (w <> w')
+      fail $ "Unsupported keyword: " ++ decode (w <> w')
     [(_,p)] -> p
     _:_:_ -> fail $ "internal error: Duplicate keywords " ++ show w
 
diff --git a/src/What4/Protocol/SMTWriter.hs b/src/What4/Protocol/SMTWriter.hs
--- a/src/What4/Protocol/SMTWriter.hs
+++ b/src/What4/Protocol/SMTWriter.hs
@@ -1598,31 +1598,41 @@
           => NatRepr w
           -> v
           -> v
-bvIntTerm w x = sumExpr ((\i -> digit (i-1)) <$> [1..natValue w])
- where digit :: Natural -> v
+bvIntTerm w x = sumExpr digits
+ where -- Precondition: 1 <= w. This is upheld by the `1 <= w` constraint in
+       -- bvIntTerm's type signature.
+       digits :: [v]
+       digits = (\i -> digit (i-1)) <$> [1..natValue w]
+
+       digit :: Natural -> v
        digit d = ite (bvTestBit w d x)
                      (fromInteger (2^d))
                      0
 
-sbvIntTerm :: SupportTermOps v
+-- @sbvIntTerm w x@ builds an integer term that has the same value as the
+-- signed integer value of the bitvector @x@. This is done by explicitly
+-- decomposing the positional notation of the bitvector into a sum of powers of
+-- 2, plus an offset to ensure that the number is signed appropriately.
+sbvIntTerm :: forall v w
+            . (SupportTermOps v, 1 <= w)
            => NatRepr w
            -> v
            -> v
-sbvIntTerm w0 x0 = sumExpr (signed_offset : go w0 x0 (natValue w0 - 2))
- where signed_offset = ite (bvTestBit w0 (natValue w0 - 1) x0)
-                           (fromInteger (negate (2^(widthVal w0 - 1))))
-                           0
-       go :: SupportTermOps v => NatRepr w -> v -> Natural -> [v]
-       go w x n
-        | n > 0     = digit w x n : go w x (n-1)
-        | n == 0    = [digit w x 0]
-        | otherwise = [] -- this branch should only be called in the degenerate case
-                         -- of length 1 signed bitvectors
+sbvIntTerm w x = sumExpr (signedOffset : digits)
+ where -- Precondition: 1 <= w. This is upheld by the `1 <= w` constraint in
+       -- sbvIntTerm's type signature.
+       signedOffset :: v
+       signedOffset = ite (bvTestBit w (natValue w - 1) x)
+                          (fromInteger (negate (2^(widthVal w - 1))))
+                          0
 
-       digit :: SupportTermOps v => NatRepr w -> v -> Natural -> v
-       digit w x d = ite (bvTestBit w d x)
-                         (fromInteger (2^d))
-                         0
+       digits :: [v]
+       digits = (\i -> digit (i-1)) <$> [1..natValue w]
+
+       digit :: SupportTermOps v => Natural -> v
+       digit d = ite (bvTestBit w d x)
+                     (fromInteger (2^d))
+                     0
 
 unsupportedTerm  :: MonadFail m => Expr t tp -> m a
 unsupportedTerm e =
diff --git a/src/What4/Solver/DReal.hs b/src/What4/Solver/DReal.hs
--- a/src/What4/Solver/DReal.hs
+++ b/src/What4/Solver/DReal.hs
@@ -31,10 +31,12 @@
 import           Control.Lens(folded)
 import           Control.Monad
 import           Data.Attoparsec.ByteString.Char8 hiding (try)
-import qualified Data.ByteString.UTF8 as UTF8
+import           Data.ByteString (ByteString)
 import           Data.Map (Map)
 import qualified Data.Map as Map
-import           Data.Text.Encoding ( decodeUtf8 )
+import           Data.Text (unpack)
+import           Data.Text.Encoding ( decodeUtf8, decodeUtf8With )
+import           Data.Text.Encoding.Error (lenientDecode)
 import           Data.Text.Lazy (Text)
 import qualified Data.Text.Lazy as Text
 import qualified Data.Text.Lazy.Builder as Builder
@@ -62,6 +64,9 @@
 import           What4.Utils.Streams (logErrorStream)
 import           What4.Utils.HandleReader
 
+decode :: ByteString -> String
+decode = unpack . decodeUtf8With lenientDecode
+
 data DReal = DReal deriving Show
 
 -- | Path to dReal
@@ -260,7 +265,7 @@
    , do _ <- char '['
         sign <- option 1 (char '-' >> return (-1))
         num <- takeWhile1 (\c -> c `elem` ("0123456789+-eE." :: String))
-        case readFloat (UTF8.toString num) of
+        case readFloat (decode num) of
           (x,""):_ -> return $ Just (sign * x)
           _ -> fail "expected rational bound"
    ]
@@ -271,7 +276,7 @@
    , do sign <- option 1 (char '-' >> return (-1))
         num <- takeWhile1 (\c -> c `elem` ("0123456789+-eE." :: String))
         _ <- char ']'
-        case readFloat (UTF8.toString num) of
+        case readFloat (decode num) of
           (x,""):_ -> return $ Just (sign * x)
           _ -> fail "expected rational bound"
    ]
diff --git a/src/What4/Utils/ResolveBounds/BV.hs b/src/What4/Utils/ResolveBounds/BV.hs
--- a/src/What4/Utils/ResolveBounds/BV.hs
+++ b/src/What4/Utils/ResolveBounds/BV.hs
@@ -87,6 +87,9 @@
 -- If it cannot, return the lower and upper bounds. This is primarly intended
 -- for compound expressions whose bounds cannot trivially be determined by
 -- using 'WI.signedBVBounds' or 'WI.unsignedBVBounds'.
+--
+-- For just resolving a bitvector as concrete without searching for bounds, see
+-- 'What4.Concretize.uniquelyConcretize'.
 resolveSymBV ::
      forall w sym solver scope st fs
    . ( 1 PN.<= w
diff --git a/src/What4/Utils/Streams.hs b/src/What4/Utils/Streams.hs
--- a/src/What4/Utils/Streams.hs
+++ b/src/What4/Utils/Streams.hs
@@ -11,11 +11,14 @@
 ( logErrorStream
 ) where
 
-import qualified Data.ByteString.UTF8 as UTF8
+import           Data.ByteString (ByteString)
+import           Data.Text (unpack)
+import           Data.Text.Encoding (decodeUtf8With)
+import           Data.Text.Encoding.Error (lenientDecode)
 import qualified System.IO.Streams as Streams
 
 -- | Write from input stream to a logging function.
-logErrorStream :: Streams.InputStream UTF8.ByteString
+logErrorStream :: Streams.InputStream ByteString
                -> (String -> IO ()) -- ^ Logging function
                -> IO ()
 logErrorStream err_stream logFn = do
@@ -23,5 +26,5 @@
   let write_err Nothing = return ()
       write_err (Just b) = logFn b
   err_output <- Streams.makeOutputStream write_err
-  lns <- Streams.map UTF8.toString =<< Streams.lines err_stream
+  lns <- Streams.map (unpack . decodeUtf8With lenientDecode) =<< Streams.lines err_stream
   Streams.connect lns err_output
diff --git a/test/ExprBuilderSMTLib2.hs b/test/ExprBuilderSMTLib2.hs
--- a/test/ExprBuilderSMTLib2.hs
+++ b/test/ExprBuilderSMTLib2.hs
@@ -1094,6 +1094,26 @@
 
       _ -> fail "expected satisfible model"
 
+-- | A regression test for #315.
+issue315Test ::
+  OnlineSolver solver =>
+  SimpleExprBuilder t fs ->
+  SolverProcess t solver ->
+  IO ()
+issue315Test sym solver = do
+    let w = knownNat @61
+    x <- freshConstant sym (safeSymbol "x") (BaseBVRepr w)
+    xsi <- sbvToInteger sym x
+    xi <- bvToInteger sym x
+    p <- intEq sym xsi xi
+
+    checkSatisfiableWithModel solver "test" p $ \case
+      Sat fn ->
+        do xEval <- groundEval fn x
+           (xEval == BV.zero w) @? "non-zero result"
+
+      _ -> fail "expected satisfible model"
+
 -- | These tests simply ensure that no exceptions are raised.
 testSolverInfo :: TestTree
 testSolverInfo = testGroup "solver info queries" $
@@ -1256,6 +1276,7 @@
         , testCase "Z3 multidim array"$ withOnlineZ3 multidimArrayTest
 
         , testCase "Z3 #182 test case" $ withOnlineZ3 issue182Test
+        , testCase "Z3 #315 test case" $ withOnlineZ3 issue315Test
 
         , arrayCopyTest
         , arraySetTest
@@ -1306,6 +1327,7 @@
         , cvcTestCase "multidim array"$ withCVC multidimArrayTest
 
         , cvcTestCase "#182 test case" $ withCVC issue182Test
+        , cvcTestCase "#315 test case" $ withCVC issue315Test
         ]
   let cvc4Tests = cvcTests CVC4
   let cvc5Tests = cvcTests CVC5
@@ -1319,6 +1341,7 @@
         , testCase "Yices pair"    $ withYices pairTest
         , testCase "Yices rounding" $ withYices roundingTest
         , testCase "Yices #182 test case" $ withYices issue182Test
+        , testCase "Yices #315 test case" $ withYices issue315Test
         ]
   let skipIfNotPresent nm = if SolverName nm `elem` (fst <$> solvers) then id
                             else fmap (ignoreTestBecause (nm <> " not present"))
diff --git a/test/ExprsTest.hs b/test/ExprsTest.hs
--- a/test/ExprsTest.hs
+++ b/test/ExprsTest.hs
@@ -32,6 +32,7 @@
 import           What4.Concrete
 import           What4.Expr
 import           What4.Interface
+import           What4.Internal (assertionsEnabled)
 
 import Bool (boolTests)
 
@@ -377,8 +378,11 @@
 
 main :: IO ()
 main = defaultMain $ testGroup "What4 Expressions"
-  [
-    testIntDivModProps
+   [ -- See Note [Asserts] in what4
+     testCase "assertions enabled" $ do
+       assertsEnabled <- assertionsEnabled
+       assertBool "assertions should be enabled" assertsEnabled
+  , testIntDivModProps
   , testBvIsNeg
   , testInt
   , testProperty "stringEmpty" $ property $ do
diff --git a/test/PrinterTests.hs b/test/PrinterTests.hs
new file mode 100644
--- /dev/null
+++ b/test/PrinterTests.hs
@@ -0,0 +1,60 @@
+{-# LANGUAGE DataKinds #-}
+
+import Data.Parameterized (knownNat)
+import Prettyprinter
+import Test.Tasty
+import Test.Tasty.HUnit
+import What4.BaseTypes (FloatPrecisionRepr (FloatingPointPrecisionRepr), NatRepr, StringInfoRepr (Char16Repr, Char8Repr, UnicodeRepr))
+import What4.InterpretedFloatingPoint (FloatInfoRepr (DoubleDoubleFloatRepr, DoubleFloatRepr, HalfFloatRepr, QuadFloatRepr, SingleFloatRepr, X86_80FloatRepr))
+
+testPrettyPrint :: (Pretty a) => String -> a -> String -> TestTree
+testPrettyPrint tcName obj expected =
+  testCase tcName $
+    let s = show $ pretty obj
+     in assertEqual "Should be equal" expected s
+
+testPrintHalfFloatRepr :: TestTree
+testPrintHalfFloatRepr = testPrettyPrint "Print half repr" HalfFloatRepr "Half"
+
+testPrintFloatInfoRepr :: TestTree
+testPrintFloatInfoRepr = testPrettyPrint "Print single repr" SingleFloatRepr "Float"
+
+testPrintDoubleInfoRepr :: TestTree
+testPrintDoubleInfoRepr = testPrettyPrint "Print double repr" DoubleFloatRepr "Double"
+
+testPrintQuadInfoRepr :: TestTree
+testPrintQuadInfoRepr = testPrettyPrint "Print quad repr" QuadFloatRepr "Quad"
+
+testPrintX86_80InfoRepr :: TestTree
+testPrintX86_80InfoRepr = testPrettyPrint "Print X86_80 repr" X86_80FloatRepr "X86_80"
+
+testPrintDoubleDoubleInfoRepr :: TestTree
+testPrintDoubleDoubleInfoRepr = testPrettyPrint "Print double double repr" DoubleDoubleFloatRepr "DoubleDouble"
+
+five :: NatRepr 5
+five = knownNat
+
+eleven :: NatRepr 11
+eleven = knownNat
+
+main :: IO ()
+main =
+  defaultMain $
+    testGroup "printers" $
+      [ testGroup "Float printers" $
+          [ testPrintFloatInfoRepr,
+            testPrintHalfFloatRepr,
+            testPrintDoubleInfoRepr,
+            testPrintQuadInfoRepr,
+            testPrintX86_80InfoRepr,
+            testPrintDoubleDoubleInfoRepr
+          ],
+        testGroup "String repr printers" $
+          [ testPrettyPrint "Print unicode repr" UnicodeRepr "Unicode",
+            testPrettyPrint "Print char16 repr" Char16Repr "Char16",
+            testPrettyPrint "Print char8 repr" Char8Repr "Char8"
+          ],
+        testGroup "Float precision repr prints" $
+          [ testPrettyPrint "Print float precision repr" (FloatingPointPrecisionRepr five eleven) "(FloatingPrecision 5 11)"
+          ]
+      ]
diff --git a/what4.cabal b/what4.cabal
--- a/what4.cabal
+++ b/what4.cabal
@@ -1,6 +1,6 @@
 Cabal-version: 2.4
 Name:          what4
-Version:       1.7
+Version:       1.7.1.0
 Author:        Galois Inc.
 Maintainer:    rscott@galois.com, kquick@galois.com
 Copyright:     (c) Galois, Inc 2014-2023
@@ -124,20 +124,17 @@
     s-cargot >= 0.1 && < 0.2,
     scientific >= 0.3.6,
     stm,
-    temporary >= 1.2,
     template-haskell,
     text >= 1.2.4.0 && < 2.2,
     th-lift >= 0.8.2 && < 0.9,
     th-lift-instances >= 0.1 && < 0.2,
-    time >= 1.8 && < 1.13,
+    time >= 1.8 && < 1.15,
     transformers >= 0.4,
     unliftio >= 0.2 && < 0.3,
     unordered-containers >= 0.2.10,
-    utf8-string >= 1.0.1,
     vector >= 0.12.1,
     versions >= 6.0.2 && < 6.1,
     zenc >= 0.1.0 && < 0.2.0,
-    ghc-prim >= 0.5.2
 
   default-extensions:
      NondecreasingIndentation
@@ -147,10 +144,12 @@
   exposed-modules:
     What4.BaseTypes
     What4.Concrete
+    What4.Concretize
     What4.Config
     What4.FunctionName
     What4.IndexLit
     What4.Interface
+    What4.Internal
     What4.InterpretedFloatingPoint
     What4.FloatMode
     What4.LabeledPred
@@ -302,6 +301,16 @@
                , prettyprinter
                , tasty-checklist >= 1.0 && < 1.1
                , text
+
+test-suite printer-test
+  import: bldflags, testdefs-hunit
+  main-is: PrinterTests.hs
+  type: exitcode-stdio-1.0
+  build-depends:
+    base,
+    prettyprinter,
+    tasty,
+    tasty-hunit
 
 test-suite online-solver-test
   import: bldflags, testdefs-hunit