diff --git a/CHANGES.md b/CHANGES.md
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,3 +1,12 @@
+# 1.6.1 (Sep 2024)
+
+* Fix a bug in which `what4`'s CVC5 adapter would fail to parse models
+  involving structs. ([#265](https://github.com/GaloisInc/what4/issues/265))
+
+* Add `What4.Expr.GroundEval.groundToSym`, which allows injecting
+  `GroundValue`s back into `SymExpr`s.
+  ([#268](https://github.com/GaloisInc/what4/pull/268))
+
 # 1.6 (May 2024)
 
 * Allow building with GHC 9.8.
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
@@ -25,6 +25,7 @@
   ( -- * Ground evaluation
     GroundValue
   , GroundValueWrapper(..)
+  , groundToSym
   , GroundArray(..)
   , lookupArray
   , GroundEvalFn(..)
@@ -82,6 +83,41 @@
   GroundValue (BaseStringType si)   = StringLiteral si
   GroundValue (BaseArrayType idx b) = GroundArray idx b
   GroundValue (BaseStructType ctx)  = Ctx.Assignment GroundValueWrapper ctx
+
+-- | Inject a 'GroundValue' back into a 'SymExpr'.
+--
+-- c.f. 'What4.Interface.concreteToSym'.
+groundToSym ::
+  IsExprBuilder sym =>
+  sym ->
+  BaseTypeRepr tp ->
+  GroundValue tp ->
+  IO (SymExpr sym tp)
+groundToSym sym tpr val =
+  case tpr of
+    BaseBoolRepr -> pure (if val then truePred sym else falsePred sym)
+    BaseBVRepr w -> bvLit sym w val
+    BaseIntegerRepr -> intLit sym val
+    BaseRealRepr -> realLit sym val
+    BaseFloatRepr fpp -> floatLit sym fpp val
+    BaseStringRepr _ -> stringLit sym val
+    BaseComplexRepr -> mkComplexLit sym val
+    BaseStructRepr tps ->
+      mkStruct sym =<< Ctx.zipWithM (\tp (GVW gv) -> groundToSym sym tp gv) tps val
+    BaseArrayRepr idxTy tpr' ->
+      case val of
+        ArrayConcrete def xs0 -> do
+          def' <- groundToSym sym tpr' def
+          arr <- constantArray sym idxTy def'
+          go (Map.toAscList xs0) arr
+        ArrayMapping _ -> fail "Can't evaluate `groundToSym` on `ArrayMapping`"
+      where
+      go [] arr = return arr
+      go ((i, x) : xs) arr =
+        do arr' <- go xs arr
+           i' <- traverseFC (indexLit sym) i
+           x' <- groundToSym sym tpr' x
+           arrayUpdate sym arr' i' x'
 
 -- | A function that calculates ground values for elements.
 --   Clients of solvers should use the @groundEval@ function for computing
diff --git a/src/What4/Solver/CVC4.hs b/src/What4/Solver/CVC4.hs
--- a/src/What4/Solver/CVC4.hs
+++ b/src/What4/Solver/CVC4.hs
@@ -131,6 +131,14 @@
   smtlib2arraySelect a i = SMT2.arraySelect a (indexCtor i)
   smtlib2arrayUpdate a i = SMT2.arrayStore a (indexCtor i)
 
+  -- CVC4's support for user-defined datatypes is somewhat buggy (see
+  -- https://github.com/cvc5/cvc5/issues/3402). Instead of using user-defined
+  -- datatypes to encode What4 structs, we instead use CVC4's built-in Tuple
+  -- datatype, which does not suffer from this bug. We use the Tuple syntax
+  -- described in https://cvc4.github.io/datatypes.html#tuples.
+  --
+  -- Note that this bug has been fixed in CVC5, so we do not apply the same
+  -- workaround in What4.Solver.CVC5.
   smtlib2declareStructCmd _ = Nothing
   smtlib2StructSort []  = Syntax.varSort "Tuple"
   smtlib2StructSort tps = Syntax.Sort $ "(Tuple" <> foldMap f tps <> ")"
diff --git a/src/What4/Solver/CVC5.hs b/src/What4/Solver/CVC5.hs
--- a/src/What4/Solver/CVC5.hs
+++ b/src/What4/Solver/CVC5.hs
@@ -125,14 +125,6 @@
   smtlib2arraySelect a i = SMT2.arraySelect a (indexCtor i)
   smtlib2arrayUpdate a i = SMT2.arrayStore a (indexCtor i)
 
-  smtlib2declareStructCmd _ = Nothing
-  smtlib2StructSort []  = Syntax.varSort "Tuple"
-  smtlib2StructSort tps = Syntax.Sort $ "(Tuple" <> foldMap f tps <> ")"
-    where f x = " " <> Syntax.unSort x
-
-  smtlib2StructCtor args = Syntax.term_app "mkTuple" args
-  smtlib2StructProj _n i x = Syntax.term_app (Syntax.builder_list ["_", "tupSel", fromString (show i)]) [ x ]
-
 cvc5Features :: ProblemFeatures
 cvc5Features = useComputableReals
            .|. useIntegerArithmetic
diff --git a/test/ExprBuilderSMTLib2.hs b/test/ExprBuilderSMTLib2.hs
--- a/test/ExprBuilderSMTLib2.hs
+++ b/test/ExprBuilderSMTLib2.hs
@@ -53,6 +53,7 @@
 import           What4.SatResult
 import           What4.Solver.Adapter
 import qualified What4.Solver.CVC4 as CVC4
+import qualified What4.Solver.CVC5 as CVC5
 import qualified What4.Solver.Z3 as Z3
 import qualified What4.Solver.Yices as Yices
 import qualified What4.Utils.BVDomain as WUB
@@ -114,6 +115,8 @@
     (\(h,s) -> void $ try @SomeException (shutdownSolverProcess s `finally` maybeClose h))
     (\(_,s) -> action sym s)
 
+data CVC = CVC4 | CVC5 deriving (Eq, Show)
+
 withCVC4
   :: (forall t . SimpleExprBuilder t (Flags FloatReal) -> SolverProcess t (Writer CVC4.CVC4) -> IO a)
   -> IO a
@@ -126,6 +129,18 @@
     (\(h,s) -> void $ try @SomeException (shutdownSolverProcess s `finally` maybeClose h))
     (\(_,s) -> action sym s)
 
+withCVC5
+  :: (forall t . SimpleExprBuilder t (Flags FloatReal) -> SolverProcess t (Writer CVC5.CVC5) -> IO a)
+  -> IO a
+withCVC5 action = withSym FloatRealRepr $ \sym -> do
+  extendConfig CVC5.cvc5Options (getConfiguration sym)
+  bracket
+    (do h <- if debugOutputFiles then Just <$> openFile "cvc5.out" WriteMode else return Nothing
+        s <- startSolverProcess (defaultFeatures CVC5.CVC5) h sym
+        return (h,s))
+    (\(h,s) -> void $ try @SomeException (shutdownSolverProcess s `finally` maybeClose h))
+    (\(_,s) -> action sym s)
+
 withModel
   :: Session t Z3.Z3
   -> BoolExpr t
@@ -1068,8 +1083,8 @@
     let idx = Ctx.Empty Ctx.:> idxInt
     let arrLookup = arrayLookup sym arr idx
     elt <- arrLookup
-    bvZero <- bvZero sym w
-    p <- bvEq sym elt bvZero
+    zeroBV <- bvZero sym w
+    p <- bvEq sym elt zeroBV
 
     checkSatisfiableWithModel solver "test" p $ \case
       Sat fn ->
@@ -1246,38 +1261,54 @@
         , arraySetTest
         , arrayCopySetTest
         ]
-  let cvc4Tests =
-        let skipPre1_8 why =
-              let shouldSkip = case lookup (SolverName "cvc4") solvers of
+  let cvcTests cvc =
+        let cvcTestCase name assertion = testCase (show cvc ++ " " ++ name) assertion
+            skipPre1_8CVC4 why =
+              let shouldSkip = cvc == CVC4 && case lookup (SolverName "cvc4") solvers of
                     Just (SolverVersion v) -> any (`elem` [ "1.7" ]) $ words v
                     Nothing -> True
               in if shouldSkip then expectFailBecause why else id
             unsuppStrings = "unicode and string escaping not supported for older CVC4 versions; upgrade to at least 1.8"
+            ignoreCVC4TestBecause reason =
+              if cvc == CVC4 then ignoreTestBecause reason else id
+
+            withCVC ::
+                 (forall t solver. OnlineSolver solver
+                   => SimpleExprBuilder t (Flags FloatReal)
+                   -> SolverProcess t solver
+                   -> IO a)
+              -> IO a
+            withCVC k =
+              case cvc of
+                CVC4 -> withCVC4 k
+                CVC5 -> withCVC5 k
         in
         [
-          ignoreTestBecause "This test stalls the solver for some reason; line-buffering issue?" $
-          testCase "CVC4 0-tuple" $ withCVC4 zeroTupleTest
-        , testCase "CVC4 1-tuple" $ withCVC4 oneTupleTest
-        , testCase "CVC4 pair"    $ withCVC4 pairTest
-        , testCase "CVC4 forall binder" $ withCVC4 forallTest
+          ignoreCVC4TestBecause "This test stalls the solver for some reason; line-buffering issue?" $
+          cvcTestCase "0-tuple" $ withCVC zeroTupleTest
+        , cvcTestCase "1-tuple" $ withCVC oneTupleTest
+        , cvcTestCase "pair"    $ withCVC pairTest
+        , cvcTestCase "forall binder" $ withCVC forallTest
 
-        , testCase "CVC4 string1" $ withCVC4 stringTest1
-        , testCase "CVC4 string2" $ withCVC4 stringTest2
-        , skipPre1_8 unsuppStrings $ testCase "CVC4 string3" $ withCVC4 stringTest3
-        , testCase "CVC4 string4" $ withCVC4 stringTest4
-        , testCase "CVC4 string5" $ withCVC4 stringTest5
-        , skipPre1_8 unsuppStrings $ testCase "CVC4 string6" $ withCVC4 stringTest6
-        , testCase "CVC4 string7" $ withCVC4 stringTest7
+        , cvcTestCase "string1" $ withCVC stringTest1
+        , cvcTestCase "string2" $ withCVC stringTest2
+        , skipPre1_8CVC4 unsuppStrings $ cvcTestCase "string3" $ withCVC stringTest3
+        , cvcTestCase "string4" $ withCVC stringTest4
+        , cvcTestCase "string5" $ withCVC stringTest5
+        , skipPre1_8CVC4 unsuppStrings $ cvcTestCase "string6" $ withCVC stringTest6
+        , cvcTestCase "string7" $ withCVC stringTest7
 
-        , testCase "CVC4 binder tuple1" $ withCVC4 binderTupleTest1
-        , testCase "CVC4 binder tuple2" $ withCVC4 binderTupleTest2
+        , cvcTestCase "binder tuple1" $ withCVC binderTupleTest1
+        , cvcTestCase "binder tuple2" $ withCVC binderTupleTest2
 
-        , testCase "CVC4 rounding" $ withCVC4 roundingTest
+        , cvcTestCase "rounding" $ withCVC roundingTest
 
-        , testCase "CVC4 multidim array"$ withCVC4 multidimArrayTest
+        , cvcTestCase "multidim array"$ withCVC multidimArrayTest
 
-        , testCase "CVC4 #182 test case" $ withCVC4 issue182Test
+        , cvcTestCase "#182 test case" $ withCVC issue182Test
         ]
+  let cvc4Tests = cvcTests CVC4
+  let cvc5Tests = cvcTests CVC5
   let yicesTests =
         [
           testResolveSymBV WURB.ExponentialSearch
@@ -1289,7 +1320,6 @@
         , testCase "Yices rounding" $ withYices roundingTest
         , testCase "Yices #182 test case" $ withYices issue182Test
         ]
-  let cvc5Tests = cvc4Tests
   let skipIfNotPresent nm = if SolverName nm `elem` (fst <$> solvers) then id
                             else fmap (ignoreTestBecause (nm <> " not present"))
   defaultMain $ testGroup "Tests" $
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.6
+Version:       1.6.1
 Author:        Galois Inc.
 Maintainer:    rscott@galois.com, kquick@galois.com
 Copyright:     (c) Galois, Inc 2014-2023