diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,9 @@
+# 0.7.1 -- 2024-08-30
+
+* Add support for GHC 9.8
+
+* Deprecate `concreteizeSymSequence` in favor of `concretizeSymSequence`
+
 # 0.7 -- 2024-02-05
 
 * Add `TypedOverride`, `SomeTypedOverride`, and `runTypedOverride` to
diff --git a/crucible.cabal b/crucible.cabal
--- a/crucible.cabal
+++ b/crucible.cabal
@@ -1,6 +1,6 @@
 Cabal-version: 2.2
 Name:          crucible
-Version:       0.7
+Version:       0.7.1
 Author:        Galois Inc.
 Maintainer:    rscott@galois.com, kquick@galois.com, langston@galois.com
 Copyright:     (c) Galois, Inc 2014-2022
@@ -44,7 +44,8 @@
 library
   import: bldflags
   build-depends:
-    base >= 4.13 && < 4.19,
+    async,
+    base >= 4.13 && < 4.20,
     bimap,
     bv-sized >= 1.0.0 && < 1.1,
     containers >= 0.5.9.0,
@@ -60,7 +61,7 @@
     template-haskell,
     text,
     time >= 1.8 && < 2.0,
-    th-abstraction >=0.1 && <0.6,
+    th-abstraction >=0.1 && <0.7,
     transformers,
     unordered-containers,
     vector,
@@ -72,6 +73,9 @@
 
   hs-source-dirs: src
 
+  other-modules:
+    Lang.Crucible.Backend.Assumptions
+
   exposed-modules:
     Lang.Crucible.Analysis.DFS
     Lang.Crucible.Analysis.ForwardDataflow
@@ -83,7 +87,9 @@
     Lang.Crucible.Backend.AssumptionStack
     Lang.Crucible.Backend.ProofGoals
     Lang.Crucible.Backend.Online
+    Lang.Crucible.Backend.Prove
     Lang.Crucible.Backend.Simple
+    Lang.Crucible.Concretize
     Lang.Crucible.CFG.Common
     Lang.Crucible.CFG.Core
     Lang.Crucible.CFG.Expr
@@ -124,6 +130,8 @@
     Lang.Crucible.Utils.MuxTree
     Lang.Crucible.Utils.PrettyPrint
     Lang.Crucible.Utils.RegRewrite
+    Lang.Crucible.Utils.Seconds
+    Lang.Crucible.Utils.Timeout
     Lang.Crucible.Utils.StateContT
     Lang.Crucible.Utils.Structural
 
diff --git a/src/Lang/Crucible/Analysis/Fixpoint/Components.hs b/src/Lang/Crucible/Analysis/Fixpoint/Components.hs
--- a/src/Lang/Crucible/Analysis/Fixpoint/Components.hs
+++ b/src/Lang/Crucible/Analysis/Fixpoint/Components.hs
@@ -21,6 +21,7 @@
   weakTopologicalOrdering,
   WTOComponent(..),
   SCC(..),
+  parentWTOComponent,
   -- * Special cases
   cfgWeakTopologicalOrdering,
   cfgSuccessors,
@@ -238,6 +239,23 @@
 
 maxLabel :: Label
 maxLabel = Label maxBound
+
+-- | Construct a map from each vertex to the head of its parent WTO component.
+-- In particular, the head of a component is not in the map. The vertices that
+-- are not in any component are not in the map.
+parentWTOComponent :: (Ord n) => [WTOComponent n] -> M.Map n n
+parentWTOComponent = F.foldMap' $ \case
+  SCC scc' -> parentWTOComponent' scc'
+  Vertex{} -> M.empty
+
+parentWTOComponent' :: (Ord n) => SCC n -> M.Map n n
+parentWTOComponent' scc =
+  F.foldMap'
+    (\case
+      SCC scc' -> parentWTOComponent' scc'
+      Vertex v -> M.singleton v $ wtoHead scc)
+    (wtoComps scc)
+
 
 {- Note [Bourdoncle Components]
 
diff --git a/src/Lang/Crucible/Backend.hs b/src/Lang/Crucible/Backend.hs
--- a/src/Lang/Crucible/Backend.hs
+++ b/src/Lang/Crucible/Backend.hs
@@ -36,42 +36,22 @@
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE ViewPatterns #-}
 module Lang.Crucible.Backend
   ( IsSymBackend(..)
   , IsSymInterface
   , HasSymInterface(..)
-  , SomeBackend(..)
-
-    -- * Assumption management
-  , CrucibleAssumption(..)
-  , CrucibleEvent(..)
-  , CrucibleAssumptions(..)
-  , Assumption
   , Assertion
-  , Assumptions
-
-  , concretizeEvents
-  , ppEvent
-  , singleEvent
-  , singleAssumption
-  , trivialAssumption
-  , impossibleAssumption
-  , ppAssumption
-  , assumptionLoc
-  , eventLoc
-  , mergeAssumptions
-  , assumptionPred
-  , forgetAssumption
-  , assumptionsPred
-  , flattenAssumptions
-  , assumptionsTopLevelLocs
+  , SomeBackend(..)
   , ProofObligation
   , ProofObligations
   , AssumptionState
   , assert
+  , impossibleAssumption
 
     -- ** Reexports
+  , module Lang.Crucible.Backend.Assumptions
   , LabeledPred(..)
   , labeledPred
   , labeledPredMsg
@@ -95,222 +75,45 @@
   , addFailedAssertion
   , assertIsInteger
   , readPartExpr
+  , runCHC
+  , proofObligationsAsImplications
+  , convertProofObligationsAsImplications
+  , proofObligationsUninterpConstants
+  , pathConditionUninterpConstants
   , ppProofObligation
   , backendOptions
   , assertThenAssumeConfigOption
   ) where
 
 import           Control.Exception(Exception(..), throwIO)
-import           Control.Lens ((^.), Traversal, folded)
+import           Control.Lens ((^.))
 import           Control.Monad
 import           Control.Monad.IO.Class
-import           Data.Kind (Type)
 import           Data.Foldable (toList)
-import           Data.Functor.Identity
-import           Data.Functor.Const
-import qualified Data.Sequence as Seq
-import           Data.Sequence (Seq)
+import           Data.Set (Set)
 import qualified Prettyprinter as PP
 import           GHC.Stack
 
+import           Data.Parameterized.Map (MapF)
+
 import           What4.Concrete
 import           What4.Config
+import           What4.Expr.Builder
 import           What4.Interface
 import           What4.InterpretedFloatingPoint
 import           What4.LabeledPred
 import           What4.Partial
 import           What4.ProgramLoc
-import           What4.Expr (GroundValue, GroundValueWrapper(..))
 
+import           What4.Solver
+import qualified What4.Solver.Z3 as Z3
+
+import           Lang.Crucible.Backend.Assumptions
 import qualified Lang.Crucible.Backend.AssumptionStack as AS
 import qualified Lang.Crucible.Backend.ProofGoals as PG
 import           Lang.Crucible.Simulator.SimError
 
--- | This type describes assumptions made at some point during program execution.
-data CrucibleAssumption (e :: BaseType -> Type)
-  = GenericAssumption ProgramLoc String (e BaseBoolType)
-    -- ^ An unstructured description of the source of an assumption.
-
-  | BranchCondition ProgramLoc (Maybe ProgramLoc) (e BaseBoolType)
-    -- ^ This arose because we want to explore a specific path.
-    -- The first location is the location of the branch predicate.
-    -- The second one is the location of the branch target.
-
-  | AssumingNoError SimError (e BaseBoolType)
-    -- ^ An assumption justified by a proof of the impossibility of
-    -- a certain simulator error.
-
--- | This type describes events we can track during program execution.
-data CrucibleEvent (e :: BaseType -> Type) where
-  -- | This event describes the creation of a symbolic variable.
-  CreateVariableEvent ::
-    ProgramLoc {- ^ location where the variable was created -} ->
-    String {- ^ user-provided name for the variable -} ->
-    BaseTypeRepr tp {- ^ type of the variable -} ->
-    e tp {- ^ the variable expression -} ->
-    CrucibleEvent e
-
-  -- | This event describes reaching a particular program location.
-  LocationReachedEvent ::
-    ProgramLoc ->
-    CrucibleEvent e
-
--- | Pretty print an event
-ppEvent :: IsExpr e => CrucibleEvent e -> PP.Doc ann
-ppEvent (CreateVariableEvent loc nm _tpr v) =
-  "create var" PP.<+> PP.pretty nm PP.<+> "=" PP.<+> printSymExpr v PP.<+> "at" PP.<+> PP.pretty (plSourceLoc loc)
-ppEvent (LocationReachedEvent loc) =
-  "reached" PP.<+> PP.pretty (plSourceLoc loc) PP.<+> "in" PP.<+> PP.pretty (plFunction loc)
-
--- | Return the program location associated with an event
-eventLoc :: CrucibleEvent e -> ProgramLoc
-eventLoc (CreateVariableEvent loc _ _ _) = loc
-eventLoc (LocationReachedEvent loc) = loc
-
--- | Return the program location associated with an assumption
-assumptionLoc :: CrucibleAssumption e -> ProgramLoc
-assumptionLoc r =
-  case r of
-    GenericAssumption l _ _ -> l
-    BranchCondition  l _ _   -> l
-    AssumingNoError s _    -> simErrorLoc s
-
--- | Get the predicate associated with this assumption
-assumptionPred :: CrucibleAssumption e -> e BaseBoolType
-assumptionPred (AssumingNoError _ p) = p
-assumptionPred (BranchCondition _ _ p) = p
-assumptionPred (GenericAssumption _ _ p) = p
-
--- | If an assumption is clearly impossible, return an abort reason
---   that can be used to unwind the execution of this branch.
-impossibleAssumption :: IsExpr e => CrucibleAssumption e -> Maybe AbortExecReason
-impossibleAssumption (AssumingNoError err p)
-  | Just False <- asConstantPred p = Just (AssertionFailure err)
-impossibleAssumption (BranchCondition loc _ p)
-  | Just False <- asConstantPred p = Just (InfeasibleBranch loc)
-impossibleAssumption (GenericAssumption loc _ p)
-  | Just False <- asConstantPred p = Just (InfeasibleBranch loc)
-impossibleAssumption _ = Nothing
-
-forgetAssumption :: CrucibleAssumption e -> CrucibleAssumption (Const ())
-forgetAssumption = runIdentity . traverseAssumption (\_ -> Identity (Const ()))
-
-traverseAssumption :: Traversal (CrucibleAssumption e) (CrucibleAssumption e') (e BaseBoolType) (e' BaseBoolType)
-traverseAssumption f = \case
-  GenericAssumption loc msg p -> GenericAssumption loc msg <$> f p
-  BranchCondition l t p -> BranchCondition l t <$> f p
-  AssumingNoError err p -> AssumingNoError err <$> f p
-
--- | This type tracks both logical assumptions and program events
---   that are relevant when evaluating proof obligations arising
---   from simulation.
-data CrucibleAssumptions (e :: BaseType -> Type) where
-  SingleAssumption :: CrucibleAssumption e -> CrucibleAssumptions e
-  SingleEvent      :: CrucibleEvent e -> CrucibleAssumptions e
-  ManyAssumptions  :: Seq (CrucibleAssumptions e) -> CrucibleAssumptions e
-  MergeAssumptions ::
-    e BaseBoolType {- ^ branch condition -} ->
-    CrucibleAssumptions e {- ^ "then" assumptions -} ->
-    CrucibleAssumptions e {- ^ "else" assumptions -} ->
-    CrucibleAssumptions e
-
-instance Semigroup (CrucibleAssumptions e) where
-  ManyAssumptions xs <> ManyAssumptions ys = ManyAssumptions (xs <> ys)
-  ManyAssumptions xs <> y = ManyAssumptions (xs Seq.|> y)
-  x <> ManyAssumptions ys = ManyAssumptions (x Seq.<| ys)
-  x <> y = ManyAssumptions (Seq.fromList [x,y])
-
-instance Monoid (CrucibleAssumptions e) where
-  mempty = ManyAssumptions mempty
-
-singleAssumption :: CrucibleAssumption e -> CrucibleAssumptions e
-singleAssumption x = SingleAssumption x
-
-singleEvent :: CrucibleEvent e -> CrucibleAssumptions e
-singleEvent x = SingleEvent x
-
--- | Collect the program locations of all assumptions and
---   events that did not occur in the context of a symbolic branch.
---   These are locations that every program path represented by
---   this @CrucibleAssumptions@ structure must have passed through.
-assumptionsTopLevelLocs :: CrucibleAssumptions e -> [ProgramLoc]
-assumptionsTopLevelLocs (SingleEvent e)      = [eventLoc e]
-assumptionsTopLevelLocs (SingleAssumption a) = [assumptionLoc a]
-assumptionsTopLevelLocs (ManyAssumptions as) = concatMap assumptionsTopLevelLocs as
-assumptionsTopLevelLocs MergeAssumptions{}   = []
-
--- | Compute the logical predicate corresponding to this collection of assumptions.
-assumptionsPred :: IsExprBuilder sym => sym -> Assumptions sym -> IO (Pred sym)
-assumptionsPred sym (SingleEvent _) =
-  return (truePred sym)
-assumptionsPred _sym (SingleAssumption a) =
-  return (assumptionPred a)
-assumptionsPred sym (ManyAssumptions xs) =
-  andAllOf sym folded =<< traverse (assumptionsPred sym) xs
-assumptionsPred sym (MergeAssumptions c xs ys) =
-  do xs' <- assumptionsPred sym xs
-     ys' <- assumptionsPred sym ys
-     itePred sym c xs' ys'
-
-traverseEvent :: Applicative m =>
-  (forall tp. e tp -> m (e' tp)) ->
-  CrucibleEvent e -> m (CrucibleEvent e')
-traverseEvent f (CreateVariableEvent loc nm tpr v) = CreateVariableEvent loc nm tpr <$> f v
-traverseEvent _ (LocationReachedEvent loc) = pure (LocationReachedEvent loc)
-
--- | Given a ground evaluation function, compute a linear, ground-valued
---   sequence of events corresponding to this program run.
-concretizeEvents ::
-  IsExpr e =>
-  (forall tp. e tp -> IO (GroundValue tp)) ->
-  CrucibleAssumptions e ->
-  IO [CrucibleEvent GroundValueWrapper]
-concretizeEvents f = loop
-  where
-    loop (SingleEvent e) =
-      do e' <- traverseEvent (\v -> GVW <$> f v) e
-         return [e']
-    loop (SingleAssumption _) = return []
-    loop (ManyAssumptions as) = concat <$> traverse loop as
-    loop (MergeAssumptions p xs ys) =
-      do b <- f p
-         if b then loop xs else loop ys
-
--- | Given a @CrucibleAssumptions@ structure, flatten all the muxed assumptions into
---   a flat sequence of assumptions that have been appropriately weakened.
---   Note, once these assumptions have been flattened, their order might no longer
---   strictly correspond to any concrete program run.
-flattenAssumptions :: IsExprBuilder sym => sym -> Assumptions sym -> IO [Assumption sym]
-flattenAssumptions sym = loop Nothing
-  where
-    loop _mz (SingleEvent _) = return []
-    loop mz (SingleAssumption a) =
-      do a' <- maybe (pure a) (\z -> traverseAssumption (impliesPred sym z) a) mz
-         if trivialAssumption a' then return [] else return [a']
-    loop mz (ManyAssumptions as) =
-      concat <$> traverse (loop mz) as
-    loop mz (MergeAssumptions p xs ys) =
-      do pnot <- notPred sym p
-         px <- maybe (pure p) (andPred sym p) mz
-         py <- maybe (pure pnot) (andPred sym pnot) mz
-         xs' <- loop (Just px) xs
-         ys' <- loop (Just py) ys
-         return (xs' <> ys')
-
--- | Merge the assumptions collected from the branches of a conditional.
-mergeAssumptions ::
-  IsExprBuilder sym =>
-  sym ->
-  Pred sym ->
-  Assumptions sym ->
-  Assumptions sym ->
-  IO (Assumptions sym)
-mergeAssumptions _sym p thens elses =
-  return (MergeAssumptions p thens elses)
-
-type Assertion sym  = LabeledPred (Pred sym) SimError
-type Assumption sym = CrucibleAssumption (SymExpr sym)
-type Assumptions sym = CrucibleAssumptions (SymExpr sym)
+type Assertion sym = LabeledPred (Pred sym) SimError
 type ProofObligation sym = AS.ProofGoal (Assumptions sym) (Assertion sym)
 type ProofObligations sym = Maybe (AS.Goals (Assumptions sym) (Assertion sym))
 type AssumptionState sym = PG.GoalCollector (Assumptions sym) (Assertion sym)
@@ -338,6 +141,17 @@
 instance Exception AbortExecReason
 
 
+-- | If an assumption is clearly impossible, return an abort reason
+--   that can be used to unwind the execution of this branch.
+impossibleAssumption :: IsExpr e => CrucibleAssumption e -> Maybe AbortExecReason
+impossibleAssumption (AssumingNoError err p)
+  | Just False <- asConstantPred p = Just (AssertionFailure err)
+impossibleAssumption (BranchCondition loc _ p)
+  | Just False <- asConstantPred p = Just (InfeasibleBranch loc)
+impossibleAssumption (GenericAssumption loc _ p)
+  | Just False <- asConstantPred p = Just (InfeasibleBranch loc)
+impossibleAssumption _ = Nothing
+
 ppAbortExecReason :: AbortExecReason -> PP.Doc ann
 ppAbortExecReason e =
   case e of
@@ -349,47 +163,21 @@
       ]
     VariantOptionsExhausted l -> ppLocated l "Variant options exhausted."
     EarlyExit l -> ppLocated l "Program exited early."
+  where
+    ppLocated :: ProgramLoc -> PP.Doc ann -> PP.Doc ann
+    ppLocated l x = "in" PP.<+> ppFn l PP.<+> ppLoc l PP.<> ":" PP.<+> x
 
-ppAssumption :: (forall tp. e tp -> PP.Doc ann) -> CrucibleAssumption e -> PP.Doc ann
-ppAssumption ppDoc e =
-  case e of
-    GenericAssumption l msg p ->
-      PP.vsep [ ppLocated l (PP.pretty msg)
-              , ppDoc p
-              ]
-    BranchCondition l Nothing p ->
-      PP.vsep [ "The branch in" PP.<+> ppFn l PP.<+> "at" PP.<+> ppLoc l
-              , ppDoc p
-              ]
-    BranchCondition l (Just t) p ->
-      PP.vsep [ "The branch in" PP.<+> ppFn l PP.<+> "from" PP.<+> ppLoc l PP.<+> "to" PP.<+> ppLoc t
-              , ppDoc p
-              ]
-    AssumingNoError simErr p ->
-      PP.vsep [ "Assuming the following error does not occur:"
-              , PP.indent 2 (ppSimError simErr)
-              , ppDoc p
-              ]
+    ppFn :: ProgramLoc -> PP.Doc ann
+    ppFn l = PP.pretty (plFunction l)
 
+    ppLoc :: ProgramLoc -> PP.Doc ann
+    ppLoc l = PP.pretty (plSourceLoc l)
+
 throwUnsupported :: (IsExprBuilder sym, MonadIO m, HasCallStack) => sym -> String -> m a
 throwUnsupported sym msg = liftIO $
   do loc <- getCurrentProgramLoc sym
      throwIO $ SimError loc $ Unsupported callStack msg
 
-
--- | Check if an assumption is trivial (always true)
-trivialAssumption :: IsExpr e => CrucibleAssumption e -> Bool
-trivialAssumption a = asConstantPred (assumptionPred a) == Just True
-
-ppLocated :: ProgramLoc -> PP.Doc ann -> PP.Doc ann
-ppLocated l x = "in" PP.<+> ppFn l PP.<+> ppLoc l PP.<> ":" PP.<+> x
-
-ppFn :: ProgramLoc -> PP.Doc ann
-ppFn l = PP.pretty (plFunction l)
-
-ppLoc :: ProgramLoc -> PP.Doc ann
-ppLoc l = PP.pretty (plSourceLoc l)
-
 type IsSymInterface sym =
   ( IsSymExprBuilder sym
   , IsInterpretedFloatSymExprBuilder sym
@@ -612,6 +400,59 @@
   loc <- getCurrentProgramLoc sym
   addAssertion bak (LabeledPred p (SimError loc msg))
   return v
+
+
+-- | Run the CHC solver on the current proof obligations, and return the
+-- solution as a substitution from the uninterpreted functions to their
+-- definitions.
+runCHC ::
+  (IsSymBackend sym bak, sym ~ ExprBuilder t st fs, MonadIO m) =>
+  bak ->
+  [SomeSymFn sym] ->
+  m (MapF (SymFnWrapper sym) (SymFnWrapper sym))
+runCHC bak uninterp_inv_fns  = liftIO $ do
+  let sym = backendGetSym bak
+
+  implications <- proofObligationsAsImplications bak
+  clearProofObligations bak
+
+  -- log to stdout
+  let logData = defaultLogData
+        { logCallbackVerbose = \_ -> putStrLn
+        , logReason = "Crucible inv"
+        }
+  Z3.runZ3Horn sym True logData uninterp_inv_fns implications >>= \case
+    Sat sub -> return sub
+    Unsat{} -> fail "Prover returned Unsat"
+    Unknown -> fail "Prover returned Unknown"
+
+
+-- | Get proof obligations as What4 implications.
+proofObligationsAsImplications :: IsSymBackend sym bak => bak -> IO [Pred sym]
+proofObligationsAsImplications bak = do
+  let sym = backendGetSym bak
+  convertProofObligationsAsImplications sym =<< getProofObligations bak
+
+-- | Convert proof obligations to What4 implications.
+convertProofObligationsAsImplications :: IsSymInterface sym => sym -> ProofObligations sym -> IO [Pred sym]
+convertProofObligationsAsImplications sym goals = do
+  let obligations = maybe [] PG.goalsToList goals
+  forM obligations $ \(AS.ProofGoal hyps (LabeledPred concl _err)) -> do
+    hyp <- assumptionsPred sym hyps
+    impliesPred sym hyp concl
+
+-- | Get the set of uninterpreted constants that appear in the path condition.
+pathConditionUninterpConstants :: IsSymBackend sym bak => bak -> IO (Set (Some (BoundVar sym)))
+pathConditionUninterpConstants bak = do
+  let sym = backendGetSym bak
+  exprUninterpConstants sym <$> getPathCondition bak
+
+-- | Get the set of uninterpreted constants that appear in the proof obligations.
+proofObligationsUninterpConstants :: IsSymBackend sym bak => bak -> IO (Set (Some (BoundVar sym)))
+proofObligationsUninterpConstants bak = do
+  let sym = backendGetSym bak
+  foldMap (exprUninterpConstants sym) <$> proofObligationsAsImplications bak
+
 
 ppProofObligation :: IsExprBuilder sym => sym -> ProofObligation sym -> IO (PP.Doc ann)
 ppProofObligation sym (AS.ProofGoal asmps gl) =
diff --git a/src/Lang/Crucible/Backend/Assumptions.hs b/src/Lang/Crucible/Backend/Assumptions.hs
new file mode 100644
--- /dev/null
+++ b/src/Lang/Crucible/Backend/Assumptions.hs
@@ -0,0 +1,268 @@
+{-|
+Module      : Lang.Crucible.Backend.Assumptions
+Copyright   : (c) Galois, Inc 2014-2024
+License     : BSD3
+Maintainer  : Langston Barrett <langston@galois.com>
+-}
+
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ViewPatterns #-}
+
+module Lang.Crucible.Backend.Assumptions
+  ( CrucibleAssumption(..)
+  , CrucibleEvent(..)
+  , CrucibleAssumptions(..)
+  , Assumption
+  , Assumptions
+
+  , concretizeEvents
+  , ppEvent
+  , singleEvent
+  , singleAssumption
+  , trivialAssumption
+  , ppAssumption
+  , assumptionLoc
+  , eventLoc
+  , mergeAssumptions
+  , assumptionPred
+  , forgetAssumption
+  , assumptionsPred
+  , flattenAssumptions
+  , assumptionsTopLevelLocs
+  ) where
+
+
+import           Control.Lens (Traversal, folded)
+import           Data.Kind (Type)
+import           Data.Functor.Identity
+import           Data.Functor.Const
+import qualified Data.Sequence as Seq
+import           Data.Sequence (Seq)
+import qualified Prettyprinter as PP
+
+import           What4.Expr.Builder
+import           What4.Interface
+import           What4.ProgramLoc
+import           What4.Expr (GroundValue, GroundValueWrapper(..))
+
+import           Lang.Crucible.Simulator.SimError
+
+type Assumption sym = CrucibleAssumption (SymExpr sym)
+type Assumptions sym = CrucibleAssumptions (SymExpr sym)
+
+-- | This type describes assumptions made at some point during program execution.
+data CrucibleAssumption (e :: BaseType -> Type)
+  = GenericAssumption ProgramLoc String (e BaseBoolType)
+    -- ^ An unstructured description of the source of an assumption.
+
+  | BranchCondition ProgramLoc (Maybe ProgramLoc) (e BaseBoolType)
+    -- ^ This arose because we want to explore a specific path.
+    -- The first location is the location of the branch predicate.
+    -- The second one is the location of the branch target.
+
+  | AssumingNoError SimError (e BaseBoolType)
+    -- ^ An assumption justified by a proof of the impossibility of
+    -- a certain simulator error.
+
+-- | This type describes events we can track during program execution.
+data CrucibleEvent (e :: BaseType -> Type) where
+  -- | This event describes the creation of a symbolic variable.
+  CreateVariableEvent ::
+    ProgramLoc {- ^ location where the variable was created -} ->
+    String {- ^ user-provided name for the variable -} ->
+    BaseTypeRepr tp {- ^ type of the variable -} ->
+    e tp {- ^ the variable expression -} ->
+    CrucibleEvent e
+
+  -- | This event describes reaching a particular program location.
+  LocationReachedEvent ::
+    ProgramLoc ->
+    CrucibleEvent e
+
+-- | Pretty print an event
+ppEvent :: IsExpr e => CrucibleEvent e -> PP.Doc ann
+ppEvent (CreateVariableEvent loc nm _tpr v) =
+  "create var" PP.<+> PP.pretty nm PP.<+> "=" PP.<+> printSymExpr v PP.<+> "at" PP.<+> PP.pretty (plSourceLoc loc)
+ppEvent (LocationReachedEvent loc) =
+  "reached" PP.<+> PP.pretty (plSourceLoc loc) PP.<+> "in" PP.<+> PP.pretty (plFunction loc)
+
+-- | Return the program location associated with an event
+eventLoc :: CrucibleEvent e -> ProgramLoc
+eventLoc (CreateVariableEvent loc _ _ _) = loc
+eventLoc (LocationReachedEvent loc) = loc
+
+-- | Return the program location associated with an assumption
+assumptionLoc :: CrucibleAssumption e -> ProgramLoc
+assumptionLoc r =
+  case r of
+    GenericAssumption l _ _ -> l
+    BranchCondition  l _ _   -> l
+    AssumingNoError s _    -> simErrorLoc s
+
+-- | Get the predicate associated with this assumption
+assumptionPred :: CrucibleAssumption e -> e BaseBoolType
+assumptionPred (AssumingNoError _ p) = p
+assumptionPred (BranchCondition _ _ p) = p
+assumptionPred (GenericAssumption _ _ p) = p
+
+forgetAssumption :: CrucibleAssumption e -> CrucibleAssumption (Const ())
+forgetAssumption = runIdentity . traverseAssumption (\_ -> Identity (Const ()))
+
+-- | Check if an assumption is trivial (always true)
+trivialAssumption :: IsExpr e => CrucibleAssumption e -> Bool
+trivialAssumption a = asConstantPred (assumptionPred a) == Just True
+
+traverseAssumption :: Traversal (CrucibleAssumption e) (CrucibleAssumption e') (e BaseBoolType) (e' BaseBoolType)
+traverseAssumption f = \case
+  GenericAssumption loc msg p -> GenericAssumption loc msg <$> f p
+  BranchCondition l t p -> BranchCondition l t <$> f p
+  AssumingNoError err p -> AssumingNoError err <$> f p
+
+-- | This type tracks both logical assumptions and program events
+--   that are relevant when evaluating proof obligations arising
+--   from simulation.
+data CrucibleAssumptions (e :: BaseType -> Type) where
+  SingleAssumption :: CrucibleAssumption e -> CrucibleAssumptions e
+  SingleEvent      :: CrucibleEvent e -> CrucibleAssumptions e
+  ManyAssumptions  :: Seq (CrucibleAssumptions e) -> CrucibleAssumptions e
+  MergeAssumptions ::
+    e BaseBoolType {- ^ branch condition -} ->
+    CrucibleAssumptions e {- ^ "then" assumptions -} ->
+    CrucibleAssumptions e {- ^ "else" assumptions -} ->
+    CrucibleAssumptions e
+
+instance Semigroup (CrucibleAssumptions e) where
+  ManyAssumptions xs <> ManyAssumptions ys = ManyAssumptions (xs <> ys)
+  ManyAssumptions xs <> y = ManyAssumptions (xs Seq.|> y)
+  x <> ManyAssumptions ys = ManyAssumptions (x Seq.<| ys)
+  x <> y = ManyAssumptions (Seq.fromList [x,y])
+
+instance Monoid (CrucibleAssumptions e) where
+  mempty = ManyAssumptions mempty
+
+singleAssumption :: CrucibleAssumption e -> CrucibleAssumptions e
+singleAssumption x = SingleAssumption x
+
+singleEvent :: CrucibleEvent e -> CrucibleAssumptions e
+singleEvent x = SingleEvent x
+
+-- | Collect the program locations of all assumptions and
+--   events that did not occur in the context of a symbolic branch.
+--   These are locations that every program path represented by
+--   this @CrucibleAssumptions@ structure must have passed through.
+assumptionsTopLevelLocs :: CrucibleAssumptions e -> [ProgramLoc]
+assumptionsTopLevelLocs (SingleEvent e)      = [eventLoc e]
+assumptionsTopLevelLocs (SingleAssumption a) = [assumptionLoc a]
+assumptionsTopLevelLocs (ManyAssumptions as) = concatMap assumptionsTopLevelLocs as
+assumptionsTopLevelLocs MergeAssumptions{}   = []
+
+-- | Compute the logical predicate corresponding to this collection of assumptions.
+assumptionsPred :: IsExprBuilder sym => sym -> Assumptions sym -> IO (Pred sym)
+assumptionsPred sym (SingleEvent _) =
+  return (truePred sym)
+assumptionsPred _sym (SingleAssumption a) =
+  return (assumptionPred a)
+assumptionsPred sym (ManyAssumptions xs) =
+  andAllOf sym folded =<< traverse (assumptionsPred sym) xs
+assumptionsPred sym (MergeAssumptions c xs ys) =
+  do xs' <- assumptionsPred sym xs
+     ys' <- assumptionsPred sym ys
+     itePred sym c xs' ys'
+
+traverseEvent :: Applicative m =>
+  (forall tp. e tp -> m (e' tp)) ->
+  CrucibleEvent e -> m (CrucibleEvent e')
+traverseEvent f (CreateVariableEvent loc nm tpr v) = CreateVariableEvent loc nm tpr <$> f v
+traverseEvent _ (LocationReachedEvent loc) = pure (LocationReachedEvent loc)
+
+-- | Given a ground evaluation function, compute a linear, ground-valued
+--   sequence of events corresponding to this program run.
+concretizeEvents ::
+  IsExpr e =>
+  (forall tp. e tp -> IO (GroundValue tp)) ->
+  CrucibleAssumptions e ->
+  IO [CrucibleEvent GroundValueWrapper]
+concretizeEvents f = loop
+  where
+    loop (SingleEvent e) =
+      do e' <- traverseEvent (\v -> GVW <$> f v) e
+         return [e']
+    loop (SingleAssumption _) = return []
+    loop (ManyAssumptions as) = concat <$> traverse loop as
+    loop (MergeAssumptions p xs ys) =
+      do b <- f p
+         if b then loop xs else loop ys
+
+-- | Given a @CrucibleAssumptions@ structure, flatten all the muxed assumptions into
+--   a flat sequence of assumptions that have been appropriately weakened.
+--   Note, once these assumptions have been flattened, their order might no longer
+--   strictly correspond to any concrete program run.
+flattenAssumptions :: IsExprBuilder sym => sym -> Assumptions sym -> IO [Assumption sym]
+flattenAssumptions sym = loop Nothing
+  where
+    loop _mz (SingleEvent _) = return []
+    loop mz (SingleAssumption a) =
+      do a' <- maybe (pure a) (\z -> traverseAssumption (impliesPred sym z) a) mz
+         if trivialAssumption a' then return [] else return [a']
+    loop mz (ManyAssumptions as) =
+      concat <$> traverse (loop mz) as
+    loop mz (MergeAssumptions p xs ys) =
+      do pnot <- notPred sym p
+         px <- maybe (pure p) (andPred sym p) mz
+         py <- maybe (pure pnot) (andPred sym pnot) mz
+         xs' <- loop (Just px) xs
+         ys' <- loop (Just py) ys
+         return (xs' <> ys')
+
+-- | Merge the assumptions collected from the branches of a conditional.
+mergeAssumptions ::
+  IsExprBuilder sym =>
+  sym ->
+  Pred sym ->
+  Assumptions sym ->
+  Assumptions sym ->
+  IO (Assumptions sym)
+mergeAssumptions _sym p thens elses =
+  return (MergeAssumptions p thens elses)
+
+ppAssumption :: (forall tp. e tp -> PP.Doc ann) -> CrucibleAssumption e -> PP.Doc ann
+ppAssumption ppDoc e =
+  case e of
+    GenericAssumption l msg p ->
+      PP.vsep [ ppLocated l (PP.pretty msg)
+              , ppDoc p
+              ]
+    BranchCondition l Nothing p ->
+      PP.vsep [ "The branch in" PP.<+> ppFn l PP.<+> "at" PP.<+> ppLoc l
+              , ppDoc p
+              ]
+    BranchCondition l (Just t) p ->
+      PP.vsep [ "The branch in" PP.<+> ppFn l PP.<+> "from" PP.<+> ppLoc l PP.<+> "to" PP.<+> ppLoc t
+              , ppDoc p
+              ]
+    AssumingNoError simErr p ->
+      PP.vsep [ "Assuming the following error does not occur:"
+              , PP.indent 2 (ppSimError simErr)
+              , ppDoc p
+              ]
+  where
+    ppLocated :: ProgramLoc -> PP.Doc ann -> PP.Doc ann
+    ppLocated l x = "in" PP.<+> ppFn l PP.<+> ppLoc l PP.<> ":" PP.<+> x
+
+    ppFn :: ProgramLoc -> PP.Doc ann
+    ppFn l = PP.pretty (plFunction l)
+
+    ppLoc :: ProgramLoc -> PP.Doc ann
+    ppLoc l = PP.pretty (plSourceLoc l)
diff --git a/src/Lang/Crucible/Backend/ProofGoals.hs b/src/Lang/Crucible/Backend/ProofGoals.hs
--- a/src/Lang/Crucible/Backend/ProofGoals.hs
+++ b/src/Lang/Crucible/Backend/ProofGoals.hs
@@ -166,7 +166,7 @@
 --   primarily a debugging aid, to ensure that stack management
 --   remains well-bracketed.
 newtype FrameIdentifier = FrameIdentifier Word64
- deriving(Eq,Ord)
+ deriving(Eq,Ord,Show)
 
 
 -- | A data-strucutre that can incrementally collect goals in context.
diff --git a/src/Lang/Crucible/Backend/Prove.hs b/src/Lang/Crucible/Backend/Prove.hs
new file mode 100644
--- /dev/null
+++ b/src/Lang/Crucible/Backend/Prove.hs
@@ -0,0 +1,455 @@
+{-|
+Module      : Lang.Crucible.Backend.Prove
+Description : Proving goals under assumptions
+Copyright   : (c) Galois, Inc 2024
+License     : BSD3
+
+This module contains helpers to dispatch the proof obligations arising from
+symbolic execution using SMT solvers. There are several dimensions of
+configurability, encapsulated in a 'ProofStrategy':
+
+* Offline vs. online: Offline solvers ('offlineProver') are simpler to manage
+  and more easily parallelized, but starting processes adds overhead, and online
+  solvers ('onlineProver') can share state as assumptions are added. See the
+  top-level README for What4 for further discussion of this choice.
+* Failing fast ('failFast') vs. keeping going ('keepGoing')
+* Timeouts: Proving with timeouts ('offlineProveWithTimeout') vs. without
+  ('offlineProve')
+* Parallelism: Not yet available via helpers in this module, but may be added to
+  a 'ProofStrategy' by clients.
+
+Once an appropriate strategy has been selected, it can be passed to entrypoints
+such as 'proveObligations' to dispatch proof obligations.
+
+When proving a single goal, the overall approach is:
+
+* Gather all of the assumptions ('Assumptions') currently in scope (e.g.,
+  from branch conditions).
+* Negate the goal ('CB.Assertion') that we are trying to prove.
+* Attempt to prove the conjunction of the assumptions and the negated goal.
+
+If this goal is satisfiable ('W4R.Sat'), then there exists a counterexample
+that makes the original goal false, so we have disproven the goal. If the
+negated goal is unsatisfiable ('W4R.Unsat'), on the other hand, then the
+original goal is proven.
+
+Another way to think of this is as the negated material conditional
+(implication) @not (assumptions -> assertion)@. This formula is equivalent
+to @not ((not assumptions) and assertion)@, i.e., @assumptions and (not
+assertion)@.
+-}
+
+{-# LANGUAGE DeriveFunctor #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE TupleSections #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Lang.Crucible.Backend.Prove
+  ( -- * Strategy
+    ProofResult(..)
+  , ProofConsumer(..)
+  , ProofStrategy(..)
+    -- ** Combiner
+  , SubgoalResult(..)
+  , Combiner(..)
+  , keepGoing
+  , failFast
+    -- ** Prover
+  , Prover(..)
+    -- *** Offline
+  , offlineProve
+  , offlineProveWithTimeout
+  , offlineProver
+    -- *** Online
+  , onlineProve
+  , onlineProver
+    -- * Proving goals
+  , proveGoals
+  , proveObligations
+  , proveCurrentObligations
+  ) where
+
+import           Control.Lens ((^.))
+import           Control.Monad.Catch (MonadMask)
+import           Control.Monad.Error.Class (MonadError, liftEither)
+import           Control.Monad.IO.Class (MonadIO(liftIO))
+import qualified Control.Monad.Reader as Reader
+
+import qualified What4.Interface as W4
+import qualified What4.Expr as WE
+import qualified What4.Protocol.Online as WPO
+import qualified What4.Protocol.SMTWriter as W4SMT
+import qualified What4.SatResult as W4R
+import qualified What4.Solver.Adapter as WSA
+
+import qualified Lang.Crucible.Backend as CB
+import           Lang.Crucible.Backend.Assumptions (Assumptions)
+import           Lang.Crucible.Utils.Timeout (Timeout, TimedOut)
+import qualified Lang.Crucible.Utils.Timeout as CTO
+
+-- | Local helper
+consumeGoals ::
+  -- | Consume an 'Assuming'
+  (asmp -> a -> a) ->
+  -- | Consume a 'Prove'
+  (goal -> a) ->
+  -- | Consume a 'ProveConj'
+  (a -> a -> a) ->
+  CB.Goals asmp goal ->
+  a
+consumeGoals onAssumption onGoal onConj = go
+  where
+  go (CB.Prove gl) = onGoal gl
+  go (CB.Assuming as gl) = onAssumption as (go gl)
+  go (CB.ProveConj g1 g2) = onConj (go g1) (go g2)
+
+-- | Local helper
+consumeGoalsWithAssumptions ::
+  forall asmp goal a.
+  Monoid asmp =>
+  -- | Consume a 'Prove'
+  (asmp -> goal -> a) ->
+  -- | Consume a 'ProveConj'
+  (a -> a -> a) ->
+  CB.Goals asmp goal ->
+  a
+consumeGoalsWithAssumptions onGoal onConj goals =
+  Reader.runReader (go goals) mempty
+  where
+  go :: CB.Goals asmp goal -> Reader.Reader asmp a
+  go =
+    consumeGoals
+      (\asmp gl -> Reader.local (<> asmp) gl)
+      (\gl -> Reader.asks (\asmps -> onGoal asmps gl))
+      (\g1 g2 -> onConj <$> g1 <*> g2)
+
+---------------------------------------------------------------------
+-- * Strategy
+
+-- | The result of attempting to prove a goal with an SMT solver.
+--
+-- The constructors of this type correspond to those of 'W4R.SatResult'.
+--
+-- * @sym@ is the symbolic backend, usually 'WE.ExprBuilder'
+-- * @t@ is the \"brand\" parameter to 'WE.Expr' (/not/ a base type)
+data ProofResult sym t
+   = -- | The goal was proved.
+     --
+     -- Corresponds to 'W4R.Unsat'.
+     Proved
+     -- | The goal was disproved, and a model that falsifies it is available.
+     --
+     -- The 'WE.GroundEvalFn' is only available for use during the execution of
+     -- a 'ProofConsumer'. See 'WSA.SolverAdapter'.
+     --
+     -- The @'Maybe' 'WE.ExprRangeBindings'@ are 'Just' when using
+     -- 'offlineProve' and 'Nothing' when using 'onlineProve'.
+     --
+     -- Corresponds to 'W4R.Sat'.
+   | Disproved (WE.GroundEvalFn t) (Maybe (WE.ExprRangeBindings t))
+     -- | The SMT solver returned \"unknown\".
+     --
+     -- Corresponds to 'W4R.Unknown'.
+   | Unknown
+
+-- | A 'ProofStrategy' dictates how results are proved.
+--
+-- * @sym@ is the symbolic backend, usually 'WE.ExprBuilder'
+-- * @m@ is the monad in which the 'Prover' and 'Combiner' run
+-- * @t@ is the \"brand\" parameter to 'WE.Expr' (/not/ a base type)
+-- * @r@ is the return type of the eventual 'ProofConsumer'
+data ProofStrategy sym m t r
+  = ProofStrategy
+    { -- | Generally 'offlineProver' or 'onlineProver'
+      stratProver :: {-# UNPACK #-} !(Prover sym m t r)
+    , stratCombine :: Combiner m r
+    }
+
+-- | A callback used to consume a 'ProofResult'.
+--
+-- If the result is 'Disproved', then this function must consume the
+-- 'WE.GroundEvalFn' before returning. See 'WSA.SolverAdapter'.
+--
+-- * @sym@ is the symbolic backend, usually 'WE.ExprBuilder'
+-- * @t@ is the \"brand\" parameter to 'WE.Expr' (/not/ a base type)
+-- * @r@ is the return type of the callback
+newtype ProofConsumer sym t r
+  = ProofConsumer (CB.ProofObligation sym -> ProofResult sym t -> IO r)
+
+---------------------------------------------------------------------
+-- *** Combiner
+
+-- | Whether or not a subgoal was proved, together with the result from a
+-- 'ProofConsumer'.
+data SubgoalResult r
+  = SubgoalResult
+    { subgoalWasProved :: !Bool
+    , subgoalResult :: !r
+    }
+  deriving Functor
+
+-- | How to combine results of proofs, used as part of a 'ProofStrategy'.
+--
+-- * @m@ is the monad in which the 'Prover' and 'Combiner' run
+-- * @r@ is the return type of the eventual 'ProofConsumer'
+newtype Combiner m r
+  = Combiner
+    { getCombiner ::
+        m (SubgoalResult r) -> m (SubgoalResult r) -> m (SubgoalResult r)
+    }
+
+-- | Combine 'SubgoalResult's using the '<>' operator. Keep going when subgoals
+-- fail.
+keepGoing :: Monad m => Semigroup r => Combiner m r
+keepGoing = Combiner $ \a1 a2 -> subgoalAnd <$> a1 <*> a2
+  where
+  subgoalAnd ::
+    Semigroup r =>
+    SubgoalResult r ->
+    SubgoalResult r ->
+    SubgoalResult r
+  subgoalAnd (SubgoalResult ok1 r1) (SubgoalResult ok2 r2) =
+    SubgoalResult (ok1 && ok2) (r1 <> r2)
+
+-- | Combine 'SubgoalResult's using the '<>' operator. After the first subgoal
+-- fails, stop trying to prove further goals.
+failFast :: Monad m => Semigroup r => Combiner m r
+failFast = Combiner $ \sr1 sr2 -> do
+  SubgoalResult ok1 r1 <- sr1
+  if ok1
+  then do
+    SubgoalResult ok2 r2 <- sr2
+    pure (SubgoalResult ok2 (r1 <> r2))
+  else pure (SubgoalResult False r1)
+
+isProved :: ProofResult sym t -> Bool
+isProved =
+  \case
+    Proved {} -> True
+    Disproved {} -> False
+    Unknown {} -> False
+
+---------------------------------------------------------------------
+-- ** Prover
+
+-- | A collection of functions used to prove goals as part of a 'ProofStrategy'.
+data Prover sym m t r
+  = Prover
+    { -- | Prove a single goal under some 'Assumptions'.
+      proverProve ::
+        Assumptions sym ->
+        CB.Assertion sym ->
+        ProofConsumer sym t r ->
+        m (SubgoalResult r)
+      -- | Assume some 'Assumptions' in the scope of a subgoal.
+    , proverAssume ::
+        Assumptions sym ->
+        m (SubgoalResult r) ->
+        m (SubgoalResult r)
+    }
+
+---------------------------------------------------------------------
+-- *** Offline
+
+-- Not exported
+offlineProveIO ::
+  (sym ~ WE.ExprBuilder t st fs) =>
+  W4.IsSymExprBuilder sym =>
+  sym ->
+  WSA.LogData ->
+  WSA.SolverAdapter st ->
+  Assumptions sym ->
+  CB.Assertion sym ->
+  ProofConsumer sym t r ->
+  IO (SubgoalResult r)
+offlineProveIO sym ld adapter asmps goal (ProofConsumer k) = do
+  let goalPred = goal ^. CB.labeledPred
+  asmsPred <- CB.assumptionsPred sym asmps
+  notGoal <- W4.notPred sym goalPred
+  WSA.solver_adapter_check_sat adapter sym ld [asmsPred, notGoal] $ \r ->
+    let r' =
+          case r of
+            W4R.Sat (gfn, binds) -> Disproved gfn binds
+            W4R.Unsat () -> Proved
+            W4R.Unknown -> Unknown
+    in SubgoalResult (isProved r') <$> k (CB.ProofGoal asmps goal) r'
+
+-- | Prove a goal using an \"offline\" solver (i.e., one process per goal).
+--
+-- See 'offlineProveWithTimeout' for a version that integrates 'Timeout's.
+--
+-- See the module-level documentation for further discussion of offline vs.
+-- online solving.
+offlineProve ::
+  MonadIO m =>
+  (sym ~ WE.ExprBuilder t st fs) =>
+  W4.IsSymExprBuilder sym =>
+  sym ->
+  WSA.LogData ->
+  WSA.SolverAdapter st ->
+  Assumptions sym ->
+  CB.Assertion sym ->
+  ProofConsumer sym t r ->
+  m (SubgoalResult r)
+offlineProve sym ld adapter asmps goal k =
+  liftIO (offlineProveIO sym ld adapter asmps goal k)
+
+-- | Prove a goal using an \"offline\" solver, with a timeout.
+--
+-- See 'offlineProveWithTimeout' for a version without 'Timeout's.
+--
+-- See the module-level documentation for further discussion of offline vs.
+-- online solving.
+offlineProveWithTimeout ::
+  MonadError TimedOut m =>
+  MonadIO m =>
+  (sym ~ WE.ExprBuilder t st fs) =>
+  W4.IsSymExprBuilder sym =>
+  Timeout ->
+  sym ->
+  WSA.LogData ->
+  WSA.SolverAdapter st ->
+  Assumptions sym ->
+  CB.Assertion sym ->
+  ProofConsumer sym t r ->
+  m (SubgoalResult r)
+offlineProveWithTimeout to sym ld adapter asmps goal k = do
+  r <- liftIO (CTO.withTimeout to (offlineProveIO sym ld adapter asmps goal k))
+  liftEither r
+
+-- | Prove goals using 'offlineProveWithTimeout'.
+--
+-- See the module-level documentation for further discussion of offline vs.
+-- online solving.
+offlineProver ::
+  MonadError TimedOut m =>
+  MonadIO m =>
+  (sym ~ WE.ExprBuilder t st fs) =>
+  Timeout ->
+  W4.IsSymExprBuilder sym =>
+  sym ->
+  WSA.LogData ->
+  WSA.SolverAdapter st ->
+  Prover sym m t r
+offlineProver to sym ld adapter =
+  Prover
+  { proverProve = offlineProveWithTimeout to sym ld adapter
+  , proverAssume = \_asmps a -> a
+  }
+
+---------------------------------------------------------------------
+-- *** Online
+
+-- | Prove a goal using an \"online\" solver (i.e., one process for all goals).
+--
+-- See the module-level documentation for further discussion of offline vs.
+-- online solving.
+onlineProve ::
+  MonadIO m =>
+  W4SMT.SMTReadWriter solver =>
+  (sym ~ WE.ExprBuilder t st fs) =>
+  W4.IsSymExprBuilder sym =>
+  WPO.SolverProcess t solver ->
+  Assumptions sym ->
+  CB.Assertion sym ->
+  ProofConsumer sym t r ->
+  m (SubgoalResult r)
+onlineProve sProc asmps goal (ProofConsumer k) =
+  liftIO $ WPO.checkSatisfiableWithModel sProc "prove" (goal ^. CB.labeledPred) $ \r ->
+    let r' =
+          case r of
+            W4R.Sat gfn -> Disproved gfn Nothing
+            W4R.Unsat () -> Proved
+            W4R.Unknown -> Unknown
+    in SubgoalResult (isProved r') <$> k (CB.ProofGoal asmps goal) r'
+
+-- | Add an assumption by @push@ing a new frame ('WPO.inNewFrame').
+onlineAssume :: 
+  MonadIO m =>
+  MonadMask m =>
+  W4SMT.SMTReadWriter solver =>
+  W4.IsSymExprBuilder sym =>
+  (W4.SymExpr sym ~ WE.Expr t) =>
+  sym ->
+  WPO.SolverProcess t solver ->
+  Assumptions sym ->
+  m r ->
+  m r
+onlineAssume sym sProc asmps a =
+  WPO.inNewFrame sProc $ do
+    liftIO $ do
+      let conn = WPO.solverConn sProc
+      asmpsPred <- CB.assumptionsPred sym asmps
+      term <- W4SMT.mkFormula conn asmpsPred
+      W4SMT.assumeFormula conn term
+      pure ()
+    a
+
+-- | Prove goals using 'onlineProve' and 'onlineAssume'.
+--
+-- See the module-level documentation for further discussion of offline vs.
+-- online solving.
+onlineProver ::
+  MonadIO m =>
+  MonadMask m =>
+  W4SMT.SMTReadWriter solver =>
+  (sym ~ WE.ExprBuilder t st fs) =>
+  W4.IsSymExprBuilder sym =>
+  sym ->
+  WPO.SolverProcess t solver ->
+  Prover sym m t r
+onlineProver sym sProc =
+  Prover
+  { proverProve = onlineProve sProc
+  , proverAssume = onlineAssume sym sProc
+  }
+
+---------------------------------------------------------------------
+-- * Proving goals
+
+-- | Prove a collection of 'CB.Goals' using the specified 'ProofStrategy'.
+proveGoals ::
+  Functor m =>
+  ProofStrategy sym m t r ->
+  CB.Goals (CB.Assumptions sym) (CB.Assertion sym) ->
+  ProofConsumer sym t r ->
+  m r
+proveGoals (ProofStrategy prover (Combiner comb)) goals k =
+  fmap subgoalResult $
+    consumeGoalsWithAssumptions
+      (\asmps gl -> proverProve prover asmps gl k)
+      comb
+      goals
+
+-- | Prove a collection of 'CB.ProofObligations' using a 'ProofStrategy'.
+proveObligations ::
+  Applicative m =>
+  Monoid r =>
+  (sym ~ WE.ExprBuilder t st fs) =>
+  ProofStrategy sym m t r ->
+  CB.ProofObligations sym ->
+  ProofConsumer sym t r ->
+  m r
+proveObligations strat obligations k =
+  case obligations of
+    Nothing -> pure mempty
+    Just goals -> proveGoals strat goals k
+
+-- | Prove a the current collection of 'CB.ProofObligations' associated with the
+-- symbolic backend (retrieved via 'CB.getProofObligations').
+proveCurrentObligations ::
+  MonadIO m =>
+  Monoid r =>
+  (sym ~ WE.ExprBuilder t st fs) =>
+  CB.IsSymBackend sym bak =>
+  bak ->
+  ProofStrategy sym m t r ->
+  ProofConsumer sym t r ->
+  m r
+proveCurrentObligations bak strat k = do
+  obligations <- liftIO (CB.getProofObligations bak)
+  proveObligations strat obligations k
diff --git a/src/Lang/Crucible/CFG/Expr.hs b/src/Lang/Crucible/CFG/Expr.hs
--- a/src/Lang/Crucible/CFG/Expr.hs
+++ b/src/Lang/Crucible/CFG/Expr.hs
@@ -75,7 +75,6 @@
 import           Data.Parameterized.TraversableFC
 
 import           What4.Interface (RoundingMode(..),StringLiteral(..), stringLiteralInfo)
-import           What4.InterpretedFloatingPoint (X86_80Val(..))
 
 import           Lang.Crucible.CFG.Extension
 import           Lang.Crucible.FunctionHandle
diff --git a/src/Lang/Crucible/Concretize.hs b/src/Lang/Crucible/Concretize.hs
new file mode 100644
--- /dev/null
+++ b/src/Lang/Crucible/Concretize.hs
@@ -0,0 +1,607 @@
+-----------------------------------------------------------------------
+-- |
+-- Module           : Lang.Crucible.Concretize
+-- Description      : Get feasible concrete values from a model
+-- Copyright        : (c) Galois, Inc 2024
+-- License          : BSD3
+-- Maintainer       : Langston Barrett <langston@galois.com>
+-- Stability        : provisional
+--
+-- This module defines 'concRegValue', a function that takes a 'RegValue' (i.e.,
+-- a symbolic value), and a model from the SMT solver ('W4GE.GroundEvalFn'), and
+-- returns the concrete value that the symbolic value takes in the model.
+--
+-- This can be used to report specific values that lead to violations of
+-- assertions, including safety assertions.
+------------------------------------------------------------------------
+
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Lang.Crucible.Concretize
+  ( ConcRegValue
+  , ConcRV'(..)
+  , ConcAnyValue(..)
+  , ConcIntrinsic
+  , IntrinsicConcFn(..)
+  , ConcCtx(..)
+  , concRegValue
+  , concRegEntry
+  , concRegMap
+    -- * There and back again
+  , IntrinsicConcToSymFn(..)
+  , concToSym
+  ) where
+
+import qualified Data.Foldable as F
+import           Data.Kind (Type)
+import           Data.List.NonEmpty (NonEmpty)
+import qualified Data.List.NonEmpty as NE
+import           Data.Map (Map)
+import qualified Data.Map as Map
+import           Data.Sequence (Seq)
+import           Data.Text (Text)
+import qualified Data.Text as Text
+import qualified Data.Vector as V
+import           Data.Word (Word16)
+
+import qualified Data.Parameterized.Context as Ctx
+import           Data.Parameterized.Map (MapF)
+import qualified Data.Parameterized.Map as MapF
+import           Data.Parameterized.TraversableFC (traverseFC)
+
+import           What4.Expr (Expr, ExprBuilder, Flags, FloatModeRepr(..))
+import qualified What4.Expr.GroundEval as W4GE
+import           What4.Interface (SymExpr)
+import qualified What4.Interface as W4I
+import qualified What4.Partial as W4P
+
+import           Lang.Crucible.FunctionHandle (FnHandle, RefCell)
+import           Lang.Crucible.Simulator.Intrinsics (Intrinsic)
+import           Lang.Crucible.Simulator.RegMap (RegEntry, RegMap)
+import qualified Lang.Crucible.Simulator.RegMap as RM
+import           Lang.Crucible.Simulator.RegValue (RegValue, FnVal)
+import qualified Lang.Crucible.Simulator.RegValue as RV
+import qualified Lang.Crucible.Simulator.SymSequence as SymSeq
+import qualified Lang.Crucible.Utils.MuxTree as MuxTree
+import           Lang.Crucible.Types
+import           Lang.Crucible.Panic (panic)
+
+-- | Newtype to allow partial application of 'ConcRegValue'.
+--
+-- Type families cannot appear partially applied.
+type ConcRV' :: Type -> CrucibleType -> Type
+newtype ConcRV' sym tp = ConcRV' { unConcRV' :: ConcRegValue sym tp }
+
+-- | Defines the \"concrete\" interpretations of 'CrucibleType' (as opposed
+-- to the \"symbolic\" interpretations, which are defined by 'RegValue'), as
+-- returned by 'concRegValue'.
+--
+-- Unlike What4\'s 'W4GE.GroundValue', this type family is parameterized
+-- by @sym@, the symbolic backend. This is because Crucible makes use of
+-- \"interpreted\" floating point numbers ('SymInterpretedFloatType'). What4\'s
+-- @SymFloat@ always uses an IEEE-754 interpretation of symbolic floats, whereas
+-- 'SymInterpretedFloatType' can use IEEE-754, real numbers, or uninterpreted
+-- functions depending on how the symbolic backend is configured.
+type ConcRegValue :: Type -> CrucibleType -> Type
+type family ConcRegValue sym tp where
+  ConcRegValue sym (BaseToType bt) = W4GE.GroundValue bt
+  ConcRegValue sym (FloatType fi) = W4GE.GroundValue (SymInterpretedFloatType sym fi)
+  ConcRegValue sym AnyType = ConcAnyValue sym
+  ConcRegValue sym UnitType = ()
+  ConcRegValue sym NatType = Integer
+  ConcRegValue sym CharType = Word16
+  ConcRegValue sym (FunctionHandleType a r) = ConcFnVal sym a r
+  ConcRegValue sym (MaybeType tp) = Maybe (ConcRegValue sym tp)
+  ConcRegValue sym (VectorType tp) = V.Vector (ConcRV' sym tp)
+  ConcRegValue sym (SequenceType tp) = Seq (ConcRV' sym tp)
+  ConcRegValue sym (StructType ctx) = Ctx.Assignment (ConcRV' sym) ctx
+  ConcRegValue sym (VariantType ctx) = Ctx.Assignment (ConcVariantBranch sym) ctx
+  ConcRegValue sym (ReferenceType tp) = NonEmpty (RefCell tp)
+  ConcRegValue sym (WordMapType w tp) = ()  -- TODO: possible to do something meaningful?
+  ConcRegValue sym (RecursiveType nm ctx) = ConcRegValue sym (UnrollType nm ctx)
+  ConcRegValue sym (IntrinsicType nm ctx) = ConcIntrinsic nm ctx
+  ConcRegValue sym (StringMapType tp) = Map Text (ConcRV' sym tp)
+
+---------------------------------------------------------------------
+-- * ConcCtx
+
+-- | Context needed for 'concRegValue'
+--
+-- The @t@ parameter matches that on 'W4GE.GroundEvalFn' and 'Expr', namely, it
+-- is a phantom type brand used to relate nonces to a specific nonce generator
+-- (similar to the @s@ parameter of the @ST@ monad). It also appears as the
+-- first argument to 'ExprBuilder'.
+data ConcCtx sym t
+  = ConcCtx
+  { -- | Model returned from SMT solver
+    model :: W4GE.GroundEvalFn t
+    -- | How to ground intrinsics
+  , intrinsicConcFuns :: MapF SymbolRepr (IntrinsicConcFn t)
+  }
+
+-- | Helper, not exported
+ground ::
+  ConcCtx sym t ->
+  Expr t tp ->
+  IO (ConcRegValue sym (BaseToType tp))
+ground (ConcCtx (W4GE.GroundEvalFn ge) _) = ge
+
+---------------------------------------------------------------------
+-- * Helpers
+
+-- | Helper, not exported
+ite ::
+  (SymExpr sym ~ Expr t) =>
+  ConcCtx sym t ->
+  W4I.Pred sym ->
+  a ->
+  a ->
+  IO a
+ite ctx p t f = do
+  b <- ground ctx p
+  pure (if b then t else f)
+
+-- | Helper, not exported
+iteIO ::
+  (SymExpr sym ~ Expr t) =>
+  ConcCtx sym t ->
+  W4I.Pred sym ->
+  IO a ->
+  IO a ->
+  IO a
+iteIO ctx p t f = do
+  b <- ground ctx p
+  if b then t else f
+
+-- | Helper, not exported
+concPartial ::
+  (SymExpr sym ~ Expr t) =>
+  W4I.IsExprBuilder sym =>
+  ConcCtx sym t ->
+  TypeRepr tp ->
+  W4P.Partial (W4I.Pred sym) (RegValue sym tp) ->
+  IO (Maybe (ConcRegValue sym tp))
+concPartial ctx tp (W4P.Partial p v) =
+  iteIO ctx p (Just <$> concRegValue ctx tp v) (pure Nothing)
+
+-- | Helper, not exported
+concPartialWithErr ::
+  (SymExpr sym ~ Expr t) =>
+  W4I.IsExprBuilder sym =>
+  ConcCtx sym t ->
+  TypeRepr tp ->
+  W4P.PartialWithErr e (W4I.Pred sym) (RegValue sym tp) ->
+  IO (Maybe (ConcRegValue sym tp))
+concPartialWithErr ctx tp =
+  \case
+    W4P.Err _ -> pure Nothing
+    W4P.NoErr pv -> concPartial ctx tp pv
+
+---------------------------------------------------------------------
+-- * Intrinsics
+
+-- | Open type family for defining how intrinsics are concretized
+type ConcIntrinsic :: Symbol -> Ctx CrucibleType -> Type
+type family ConcIntrinsic nm ctx
+
+-- | Function for concretizing an intrinsic type
+type IntrinsicConcFn :: Type -> Symbol -> Type
+newtype IntrinsicConcFn t nm
+  = IntrinsicConcFn
+    (forall sym ctx.
+      SymExpr sym ~ Expr t =>
+      W4I.IsExprBuilder sym =>
+      ConcCtx sym t ->
+      Ctx.Assignment TypeRepr ctx ->
+      Intrinsic sym nm ctx ->
+      IO (ConcRegValue sym (IntrinsicType nm ctx)))
+
+-- | Helper, not exported
+tryConcIntrinsic ::
+  forall sym nm ctx t.
+  SymExpr sym ~ Expr t =>
+  W4I.IsExprBuilder sym =>
+  ConcCtx sym t ->
+  SymbolRepr nm ->
+  Ctx.Assignment TypeRepr ctx ->
+  RegValue sym (IntrinsicType nm ctx) ->
+  Maybe (IO (ConcRegValue sym (IntrinsicType nm ctx)))
+tryConcIntrinsic ctx nm tyCtx v = do
+    case MapF.lookup nm (intrinsicConcFuns ctx) of
+      Nothing -> Nothing
+      Just (IntrinsicConcFn f) -> Just (f @sym @ctx ctx tyCtx v)
+
+---------------------------------------------------------------------
+-- * Any
+
+-- | An 'AnyValue' concretized by 'concRegValue'
+data ConcAnyValue sym = forall tp. ConcAnyValue (TypeRepr tp) (ConcRV' sym tp)
+
+---------------------------------------------------------------------
+-- * FnVal
+
+-- | A 'FnVal' concretized by 'concRegValue'
+data ConcFnVal (sym :: Type) (args :: Ctx CrucibleType) (res :: CrucibleType) where
+  ConcClosureFnVal ::
+    !(ConcFnVal sym (args ::> tp) ret) ->
+    !(TypeRepr tp) ->
+    !(ConcRV' sym tp) ->
+    ConcFnVal sym args ret
+
+  ConcVarargsFnVal ::
+    !(FnHandle (args ::> VectorType AnyType) ret) ->
+    !(CtxRepr addlArgs) ->
+    ConcFnVal sym (args <+> addlArgs) ret
+
+  ConcHandleFnVal ::
+    !(FnHandle a r) ->
+    ConcFnVal sym a r
+
+-- | Helper, not exported
+concFnVal ::
+  (SymExpr sym ~ Expr t) =>
+  W4I.IsExprBuilder sym =>
+  ConcCtx sym t ->
+  CtxRepr args ->
+  TypeRepr ret ->
+  FnVal sym args ret ->
+  IO (ConcFnVal sym args ret)
+concFnVal ctx args ret =
+  \case
+    RV.ClosureFnVal fv t v -> do
+      concV <- concFnVal ctx (args Ctx.:> t) ret fv
+      v' <- concRegValue ctx t v
+      pure (ConcClosureFnVal concV t (ConcRV' v'))
+    RV.VarargsFnVal hdl extra ->
+      pure (ConcVarargsFnVal hdl extra)
+    RV.HandleFnVal hdl ->
+      pure (ConcHandleFnVal hdl)
+
+---------------------------------------------------------------------
+-- * Reference
+
+-- | Helper, not exported
+concMux ::
+  (SymExpr sym ~ Expr t) =>
+  W4I.IsExprBuilder sym =>
+  ConcCtx sym t ->
+  MuxTree.MuxTree sym a ->
+  IO (NonEmpty a)
+concMux ctx mt = do
+  l <- go (MuxTree.viewMuxTree mt)
+  case NE.nonEmpty l of
+    -- This is impossible because the only way to make a MuxTree is with
+    -- `toMuxTree`, which uses `truePred`.
+    Nothing ->
+      panic "Lang.Crucible.Concretize.concMux"
+        [ "Impossible: Mux tree had no feasible branches?" ]
+    Just ne -> pure ne
+  where
+    go [] = pure []
+    go ((val, p):xs) = do
+      f <- ite ctx p (val:) id
+      f <$> go xs
+
+---------------------------------------------------------------------
+-- * Sequence
+
+-- | Helper, not exported
+concSymSequence ::
+  (SymExpr sym ~ Expr t) =>
+  W4I.IsExprBuilder sym =>
+  ConcCtx sym t ->
+  TypeRepr tp ->
+  SymSeq.SymSequence sym (RegValue sym tp) ->
+  IO (Seq (ConcRV' sym tp))
+concSymSequence ctx tp =
+  SymSeq.concretizeSymSequence
+    (ground ctx)
+    (fmap ConcRV' . concRegValue ctx tp)
+
+---------------------------------------------------------------------
+-- * StringMap
+
+-- | Helper, not exported
+concStringMap ::
+  (SymExpr sym ~ Expr t) =>
+  W4I.IsExprBuilder sym =>
+  ConcCtx sym t ->
+  TypeRepr tp ->
+  RegValue sym (StringMapType tp) ->
+  IO (Map Text (ConcRV' sym tp))
+concStringMap ctx tp v = Map.fromList <$> go (Map.toList v)
+  where
+    go [] = pure []
+    go ((t, v'):xs) =
+      concPartialWithErr ctx tp v' >>=
+        \case
+          Nothing -> go xs
+          Just v'' -> ((t, ConcRV' v''):) <$> go xs
+
+---------------------------------------------------------------------
+-- * Variant
+
+-- | Note that we do not attempt to \"normalize\" variants in 'concRegValue'
+-- in any way. If the model reports that multiple branches of a variant are
+-- plausible, then multiple branches might be included as 'Just's.
+newtype ConcVariantBranch sym tp
+  = ConcVariantBranch (Maybe (ConcRV' sym tp))
+
+-- | Helper, not exported
+concVariant ::
+  forall sym variants t.
+  (SymExpr sym ~ Expr t) =>
+  W4I.IsExprBuilder sym =>
+  ConcCtx sym t ->
+  Ctx.Assignment TypeRepr variants ->
+  RegValue sym (VariantType variants) ->
+  IO (ConcRegValue sym (VariantType variants))
+concVariant ctx tps vs = Ctx.zipWithM concBranch tps vs
+  where
+    concBranch :: forall tp. TypeRepr tp -> RV.VariantBranch sym tp -> IO (ConcVariantBranch sym tp)
+    concBranch tp (RV.VB v) = do
+      v' <- concPartialWithErr ctx tp v
+      case v' of
+        Just v'' -> pure (ConcVariantBranch (Just (ConcRV' v'')))
+        Nothing -> pure (ConcVariantBranch Nothing)
+
+---------------------------------------------------------------------
+-- * 'concRegValue'
+
+-- | Pick a feasible concrete value from the model
+--
+-- This function does not attempt to \"normalize\" variants nor mux trees in any
+-- way. If the model reports that multiple branches of a variant or mux tree are
+-- plausible, then multiple branches might be included in the result.
+concRegValue ::
+  (SymExpr sym ~ Expr t) =>
+  W4I.IsExprBuilder sym =>
+  ConcCtx sym t ->
+  TypeRepr tp ->
+  RegValue sym tp ->
+  IO (ConcRegValue sym tp)
+concRegValue ctx tp v =
+  case (tp, v) of
+    -- Base types
+    (BoolRepr, _) -> ground ctx v
+    (BVRepr _width, _) -> ground ctx v
+    (ComplexRealRepr, _) -> ground ctx v
+    (FloatRepr _fpp, _) -> ground ctx v
+    (IEEEFloatRepr _fpp, _) -> ground ctx v
+    (IntegerRepr, _) -> ground ctx v
+    (NatRepr, _) -> ground ctx (W4I.natToIntegerPure v)
+    (RealValRepr, _) -> ground ctx v
+    (StringRepr _, _) -> ground ctx v
+    (SymbolicArrayRepr _idxs _tp', _) -> ground ctx v
+    (SymbolicStructRepr _tys, _) -> ground ctx v
+
+    -- Trivial cases
+    (UnitRepr, ()) -> pure ()
+    (CharRepr, _) -> pure v
+
+    -- Simple recursive cases
+    (AnyRepr, RV.AnyValue tp' v') ->
+      ConcAnyValue tp' . ConcRV' <$> concRegValue ctx tp' v'
+    (RecursiveRepr symb tyCtx, RV.RolledType v') ->
+      concRegValue ctx (unrollType symb tyCtx) v'
+    (StructRepr tps, _) ->
+      Ctx.zipWithM (\tp' (RV.RV v') -> ConcRV' <$> concRegValue ctx tp' v') tps v
+    (VectorRepr tp', _) ->
+      traverse (fmap ConcRV' . concRegValue ctx tp') v
+
+    -- Cases with helper functions
+    (MaybeRepr tp', _) ->
+      concPartialWithErr ctx tp' v
+    (FunctionHandleRepr args ret, _) ->
+      concFnVal ctx args ret v
+    (IntrinsicRepr nm tyCtx, _) ->
+      case tryConcIntrinsic ctx nm tyCtx v of
+        Nothing ->
+          let strNm = Text.unpack (symbolRepr nm) in
+          fail ("Missing concretization function for intrinsic: " ++ strNm)
+        Just r -> r
+    (ReferenceRepr _, _) ->
+      concMux ctx v
+    (SequenceRepr tp', _) ->
+      concSymSequence ctx tp' v
+    (StringMapRepr tp', _) ->
+      concStringMap ctx tp' v
+    (VariantRepr tps, _) ->
+      concVariant ctx tps v
+
+    -- Incomplete cases
+    (WordMapRepr _ _, _) -> pure ()
+
+-- | Like 'concRegValue', but for 'RegEntry'
+concRegEntry ::
+  (SymExpr sym ~ Expr t) =>
+  W4I.IsExprBuilder sym =>
+  ConcCtx sym t ->
+  RegEntry sym tp ->
+  IO (ConcRegValue sym tp)
+concRegEntry ctx e = concRegValue ctx (RM.regType e) (RM.regValue e)
+
+-- | Like 'concRegEntry', but for a whole 'RegMap'
+concRegMap ::
+  (SymExpr sym ~ Expr t) =>
+  W4I.IsExprBuilder sym =>
+  ConcCtx sym t ->
+  RegMap sym tps ->
+  IO (Ctx.Assignment (ConcRV' sym) tps)
+concRegMap ctx (RM.RegMap m) = traverseFC (fmap ConcRV' . concRegEntry ctx) m
+
+---------------------------------------------------------------------
+-- * concToSym
+
+-- | Function for re-symbolizing an intrinsic type
+type IntrinsicConcToSymFn :: Symbol -> Type
+newtype IntrinsicConcToSymFn nm
+  = IntrinsicConcToSymFn
+    (forall sym ctx.
+      W4I.IsExprBuilder sym =>
+      sym ->
+      Ctx.Assignment TypeRepr ctx ->
+      ConcIntrinsic nm ctx ->
+      IO (RegValue sym (IntrinsicType nm ctx)))
+
+-- | Helper, not exported
+concToSymAny ::
+  (sym ~ ExprBuilder scope st (Flags fm)) =>
+  sym ->
+  MapF SymbolRepr IntrinsicConcToSymFn ->
+  FloatModeRepr fm ->
+  ConcRegValue sym AnyType ->
+  IO (RegValue sym AnyType)
+concToSymAny sym iFns fm (ConcAnyValue tp' (ConcRV' v')) =
+  RV.AnyValue tp' <$> concToSym sym iFns fm tp' v'
+
+-- | Helper, not exported
+concToSymFn ::
+  (sym ~ ExprBuilder scope st (Flags fm)) =>
+  sym ->
+  MapF SymbolRepr IntrinsicConcToSymFn ->
+  FloatModeRepr fm ->
+  Ctx.Assignment (TypeRepr) as ->
+  TypeRepr r ->
+  ConcRegValue sym (FunctionHandleType as r) ->
+  IO (RegValue sym (FunctionHandleType as r))
+concToSymFn sym iFns fm as r f =
+  case f of
+    ConcClosureFnVal clos vtp (ConcRV' v) -> do
+      v' <- concToSym sym iFns fm vtp v
+      clos' <- concToSymFn sym iFns fm (as Ctx.:> vtp) r clos
+      pure (RV.ClosureFnVal clos' vtp v')
+
+    ConcVarargsFnVal hdl extra ->
+      pure (RV.VarargsFnVal hdl extra)
+
+    ConcHandleFnVal hdl ->
+      pure (RV.HandleFnVal hdl)
+
+-- | Helper, not exported
+concToSymIntrinsic ::
+  W4I.IsExprBuilder sym =>
+  sym ->
+  MapF SymbolRepr IntrinsicConcToSymFn ->
+  SymbolRepr nm ->
+  CtxRepr ctx ->
+  ConcRegValue sym (IntrinsicType nm ctx) ->
+  IO (RegValue sym (IntrinsicType nm ctx))
+concToSymIntrinsic sym iFns nm tyCtx v =
+  case MapF.lookup nm iFns of
+    Nothing ->
+      let strNm = Text.unpack (symbolRepr nm) in
+      fail ("Missing concretization function for intrinsic: " ++ strNm)
+    Just (IntrinsicConcToSymFn f) -> f sym tyCtx v
+
+-- | Helper, not exported
+concToSymMaybe ::
+  (sym ~ ExprBuilder scope st (Flags fm)) =>
+  sym ->
+  MapF SymbolRepr IntrinsicConcToSymFn ->
+  FloatModeRepr fm ->
+  TypeRepr tp ->
+  ConcRegValue sym (MaybeType tp) ->
+  IO (RegValue sym (MaybeType tp))
+concToSymMaybe sym iFns fm tp =
+  \case
+    Nothing -> pure (W4P.Err ())
+    Just v ->
+      W4P.justPartExpr sym <$> concToSym sym iFns fm tp v
+
+-- | Helper, not exported
+concToSymRef ::
+  W4I.IsExprBuilder sym =>
+  sym ->
+  ConcRegValue sym (ReferenceType tp) ->
+  IO (RegValue sym (ReferenceType tp))
+concToSymRef sym (v NE.:| _) = pure (MuxTree.toMuxTree sym v)
+
+-- | Helper, not exported
+concToSymVariant ::
+  forall sym tps scope st fm.
+  (sym ~ ExprBuilder scope st (Flags fm)) =>
+  sym ->
+  MapF SymbolRepr IntrinsicConcToSymFn ->
+  FloatModeRepr fm ->
+  CtxRepr tps ->
+  ConcRegValue sym (VariantType tps) ->
+  IO (RegValue sym (VariantType tps))
+concToSymVariant sym iFns fm tps v = Ctx.zipWithM go tps v
+  where
+    go :: forall tp. TypeRepr tp -> ConcVariantBranch sym tp -> IO (RV.VariantBranch sym tp)
+    go tp (ConcVariantBranch b) =
+      case b of
+        Nothing -> pure (RV.VB (W4P.Err ()))
+        Just (ConcRV' v') ->
+          RV.VB . W4P.justPartExpr sym <$> concToSym sym iFns fm tp v'
+
+-- | Inject a 'ConcRegValue' back into a 'RegValue'.
+concToSym ::
+  (sym ~ ExprBuilder scope st (Flags fm)) =>
+  sym ->
+  MapF SymbolRepr IntrinsicConcToSymFn ->
+  FloatModeRepr fm ->
+  TypeRepr tp ->
+  ConcRegValue sym tp ->
+  IO (RegValue sym tp)
+concToSym sym iFns fm tp v =
+  case tp of
+    -- Base types
+    BoolRepr -> W4GE.groundToSym sym BaseBoolRepr v
+    BVRepr width -> W4GE.groundToSym sym (BaseBVRepr width) v
+    ComplexRealRepr -> W4GE.groundToSym sym BaseComplexRepr v
+    FloatRepr fi ->
+      case fm of
+        FloatIEEERepr ->
+          W4I.floatLit sym (floatInfoToPrecisionRepr fi) v
+        FloatUninterpretedRepr -> do
+          sv <- W4GE.groundToSym sym (floatInfoToBVTypeRepr fi) v
+          iFloatFromBinary sym fi sv
+        FloatRealRepr ->
+          iFloatLitRational sym fi v
+    IEEEFloatRepr fpp -> W4GE.groundToSym sym (BaseFloatRepr fpp) v
+    IntegerRepr -> W4GE.groundToSym sym BaseIntegerRepr v
+    NatRepr -> W4I.integerToNat sym =<< W4GE.groundToSym sym BaseIntegerRepr v
+    RealValRepr -> W4GE.groundToSym sym BaseRealRepr v
+    StringRepr si -> W4GE.groundToSym sym (BaseStringRepr si) v
+    SymbolicArrayRepr idxs tp' -> W4GE.groundToSym sym (BaseArrayRepr idxs tp') v
+    SymbolicStructRepr tys -> W4GE.groundToSym sym (BaseStructRepr tys) v
+
+    -- Trivial cases
+    UnitRepr -> pure ()
+    CharRepr -> pure v
+
+    -- Simple recursive cases
+    RecursiveRepr symb tyCtx ->
+      RV.RolledType <$> concToSym sym iFns fm (unrollType symb tyCtx) v
+    SequenceRepr tp' -> do
+      l <- traverse (concToSym sym iFns fm tp' . unConcRV') (F.toList v)
+      SymSeq.fromListSymSequence sym l
+    StringMapRepr tp' ->
+      traverse (fmap (W4P.justPartExpr sym) . concToSym sym iFns fm tp' . unConcRV') v
+    StructRepr tps ->
+      Ctx.zipWithM (\tp' (ConcRV' v') -> RV.RV <$> concToSym sym iFns fm tp' v') tps v
+    VectorRepr tp' ->
+      traverse (concToSym sym iFns fm tp' . unConcRV') v
+
+    -- Cases with helper functions
+    AnyRepr -> concToSymAny sym iFns fm v
+    MaybeRepr tp' -> concToSymMaybe sym iFns fm tp' v
+    FunctionHandleRepr args ret -> concToSymFn sym iFns fm args ret v
+    IntrinsicRepr nm tyCtx -> concToSymIntrinsic sym iFns nm tyCtx v
+    ReferenceRepr _tp' -> concToSymRef sym v
+    VariantRepr tps -> concToSymVariant sym iFns fm tps v
+
+    -- Incomplete cases
+    WordMapRepr _ _ -> fail "concToSym does not yet support WordMap"
diff --git a/src/Lang/Crucible/FunctionHandle.hs b/src/Lang/Crucible/FunctionHandle.hs
--- a/src/Lang/Crucible/FunctionHandle.hs
+++ b/src/Lang/Crucible/FunctionHandle.hs
@@ -34,6 +34,7 @@
   , emptyHandleMap
   , insertHandleMap
   , lookupHandleMap
+  , updateHandleMap
   , searchHandleMap
   , handleMapToHandles
     -- * Reference cells
@@ -44,6 +45,7 @@
 
 import           Data.Hashable
 import           Data.Kind
+import           Data.Functor.Identity
 import qualified Data.List as List
 import           Data.Ord (comparing)
 
@@ -216,6 +218,19 @@
   case MapF.lookup (handleID hdl) m of
      Just (HandleElt _ x) -> Just x
      Nothing -> Nothing
+
+-- | Update the entry of the function handle in the map.
+updateHandleMap :: (f args ret -> f args ret)
+                -> FnHandle args ret
+                -> FnHandleMap f
+                -> FnHandleMap f
+updateHandleMap f hdl (FnHandleMap m) =
+  FnHandleMap $ MapF.updatedValue $ runIdentity $
+    MapF.updateAtKey
+      (handleID hdl)
+      (Identity Nothing)
+      (\(HandleElt hdl' x) -> Identity $ MapF.Set $ HandleElt hdl' $ f x)
+      m
 
 -- | Lookup the function name in the map by a linear scan of all
 -- entries.  This will be much slower than using 'lookupHandleMap' to
diff --git a/src/Lang/Crucible/Simulator/EvalStmt.hs b/src/Lang/Crucible/Simulator/EvalStmt.hs
--- a/src/Lang/Crucible/Simulator/EvalStmt.hs
+++ b/src/Lang/Crucible/Simulator/EvalStmt.hs
@@ -60,7 +60,6 @@
 
 import           What4.Config
 import           What4.Interface
-import           What4.InterpretedFloatingPoint (freshFloatConstant)
 import           What4.Partial
 import           What4.ProgramLoc
 
diff --git a/src/Lang/Crucible/Simulator/Evaluation.hs b/src/Lang/Crucible/Simulator/Evaluation.hs
--- a/src/Lang/Crucible/Simulator/Evaluation.hs
+++ b/src/Lang/Crucible/Simulator/Evaluation.hs
@@ -792,8 +792,8 @@
       bvSlt sym x y
     BoolToBV w xe -> do
       x <- evalSub xe
-      one <- bvLit sym w (BV.one w)
-      zro <- bvLit sym w (BV.zero w)
+      one <- bvOne sym w
+      zro <- bvZero sym w
       bvIte sym x one zro
     BVNonzero _ xe -> do
       x <- evalSub xe
diff --git a/src/Lang/Crucible/Simulator/Profiling.hs b/src/Lang/Crucible/Simulator/Profiling.hs
--- a/src/Lang/Crucible/Simulator/Profiling.hs
+++ b/src/Lang/Crucible/Simulator/Profiling.hs
@@ -76,6 +76,7 @@
 
 import           Lang.Crucible.Backend
 import           Lang.Crucible.CFG.Core
+import           Lang.Crucible.Panic (panic)
 import           Lang.Crucible.Simulator.CallFrame
 import           Lang.Crucible.Simulator.EvalStmt
 import           Lang.Crucible.Simulator.ExecutionTree
@@ -290,7 +291,11 @@
  go xs (e Seq.:<| es) =
    case cgEvent_type e of
      ENTER -> go (e:xs) es
-     EXIT  -> go (tail xs) es
+     EXIT  -> case xs of
+                (_:xss) -> go xss es
+                _ -> panic
+                       "openEventFrames"
+                       ["Encountered an EXIT without a preceding ENTER"]
      _     -> go xs es
 
 openToCloseEvent :: UTCTime -> Metrics Identity -> CGEvent -> CGEvent
diff --git a/src/Lang/Crucible/Simulator/SymSequence.hs b/src/Lang/Crucible/Simulator/SymSequence.hs
--- a/src/Lang/Crucible/Simulator/SymSequence.hs
+++ b/src/Lang/Crucible/Simulator/SymSequence.hs
@@ -14,6 +14,7 @@
 ( SymSequence(..)
 , nilSymSequence
 , consSymSequence
+, fromListSymSequence
 , appendSymSequence
 , muxSymSequence
 , isNilSymSequence
@@ -23,6 +24,7 @@
 , unconsSymSequence
 , traverseSymSequence
 , concreteizeSymSequence
+, concretizeSymSequence
 , prettySymSequence
 
   -- * Low-level evaluation primitives
@@ -40,6 +42,8 @@
 import qualified Data.Map as Map
 import           Data.Parameterized.Nonce
 import qualified Data.Parameterized.Map as MapF
+import           Data.Sequence (Seq)
+import qualified Data.Sequence as Seq
 import           Prettyprinter (Doc)
 import qualified Prettyprinter as PP
 
@@ -167,6 +171,12 @@
   do n <- freshNonce globalNonceGenerator
      pure (SymSequenceCons n x xs)
 
+fromListSymSequence :: sym -> [a] -> IO (SymSequence sym a)
+fromListSymSequence sym =
+  \case
+    [] -> nilSymSequence sym
+    (x:xs) -> consSymSequence sym x =<< fromListSymSequence sym xs
+
 -- | Append two sequences
 appendSymSequence ::
   sym ->
@@ -400,6 +410,24 @@
     loop SymSequenceNil = pure []
     loop (SymSequenceCons _ v tl) = (:) <$> eval v <*> loop tl
     loop (SymSequenceAppend _ xs ys) = (++) <$> loop xs <*> loop ys
+    loop (SymSequenceMerge _ p xs ys) =
+      do b <- conc p
+         if b then loop xs else loop ys
+{-# DEPRECATED concreteizeSymSequence "Use concretizeSymSequence instead" #-} 
+
+-- | Using the given evaluation function for booleans, and an evaluation
+--   function for values, compute a concrete sequence corresponding
+--   to the given symbolic sequence.
+concretizeSymSequence ::
+  (Pred sym -> IO Bool) {- ^ evaluation for booleans -} ->
+  (a -> IO b) {- ^ evaluation for values -} ->
+  SymSequence sym a ->
+  IO (Seq b)
+concretizeSymSequence conc eval = loop
+  where
+    loop SymSequenceNil = pure Seq.empty
+    loop (SymSequenceCons _ v tl) = (Seq.<|) <$> eval v <*> loop tl
+    loop (SymSequenceAppend _ xs ys) = (Seq.><) <$> loop xs <*> loop ys
     loop (SymSequenceMerge _ p xs ys) =
       do b <- conc p
          if b then loop xs else loop ys
diff --git a/src/Lang/Crucible/Types.hs b/src/Lang/Crucible/Types.hs
--- a/src/Lang/Crucible/Types.hs
+++ b/src/Lang/Crucible/Types.hs
@@ -95,16 +95,7 @@
   , module Data.Parameterized.NatRepr
   , module Data.Parameterized.SymbolRepr
   , module What4.BaseTypes
-  , FloatInfo
-  , HalfFloat
-  , SingleFloat
-  , DoubleFloat
-  , QuadFloat
-  , X86_80Float
-  , DoubleDoubleFloat
-  , FloatInfoRepr(..)
-  , FloatInfoToBitWidth
-  , floatInfoToBVTypeRepr
+  , module What4.InterpretedFloatingPoint
   ) where
 
 import           Data.Hashable
diff --git a/src/Lang/Crucible/Utils/Seconds.hs b/src/Lang/Crucible/Utils/Seconds.hs
new file mode 100644
--- /dev/null
+++ b/src/Lang/Crucible/Utils/Seconds.hs
@@ -0,0 +1,18 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
+module Lang.Crucible.Utils.Seconds
+  ( Seconds
+  , secondsToInt
+  , secondsFromInt
+  , secondsToMicroseconds
+  ) where
+
+newtype Seconds = Seconds { secondsToInt :: Int }
+  deriving (Eq, Num, Ord, Show)
+
+-- | Inverse of 'secondsToInt'
+secondsFromInt :: Int -> Seconds
+secondsFromInt = Seconds
+
+secondsToMicroseconds :: Seconds -> Int
+secondsToMicroseconds = (* 1000000) . secondsToInt
diff --git a/src/Lang/Crucible/Utils/Timeout.hs b/src/Lang/Crucible/Utils/Timeout.hs
new file mode 100644
--- /dev/null
+++ b/src/Lang/Crucible/Utils/Timeout.hs
@@ -0,0 +1,38 @@
+module Lang.Crucible.Utils.Timeout
+  ( Timeout(..)
+  , TimedOut(..)
+  , withTimeout
+  ) where
+
+import qualified Control.Concurrent as CC
+import qualified Control.Concurrent.Async as CCA
+
+import qualified Lang.Crucible.Utils.Seconds as Secs
+
+-- | A timeout, in seconds.
+newtype Timeout = Timeout { getTimeout :: Secs.Seconds }
+  deriving (Eq, Ord, Show)
+
+-- Private, not exported
+timeoutToMicros :: Timeout -> Int
+timeoutToMicros = Secs.secondsToMicroseconds . getTimeout
+
+-- | A task timed out.
+data TimedOut = TimedOut
+  deriving Show
+
+-- | Execute a task with a timeout.
+--
+-- Implemented via 'CCA.race', so re-throws exceptions that occur during the
+-- task (if it completes before the timeout).
+withTimeout ::
+  -- | Timeout duration (seconds)
+  Timeout ->
+  -- | Task to attempt
+  IO a ->
+  IO (Either TimedOut a)
+withTimeout to task = do
+  let timeout = do
+        CC.threadDelay (timeoutToMicros to)
+        pure TimedOut
+  CCA.race timeout task