diff --git a/deps/crucible b/deps/crucible
index 0a7c3aff..847bd2d1 160000
--- a/deps/crucible
+++ b/deps/crucible
@@ -1 +1 @@
-Subproject commit 0a7c3afff84b3c34555c0812f15308bc5bf04c55
+Subproject commit 847bd2d1cd792f9dfa21a6fa58b7be50d7e46c19
diff --git a/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs b/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs
index 6df43d46..590602e7 100644
--- a/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs
+++ b/macaw-ppc-symbolic/src/Data/Macaw/PPC/Symbolic.hs
@@ -247,31 +247,31 @@ archUpdateReg regEntry reg val =
     Nothing -> error $ "unexpected register: " ++ show (MC.prettyF reg)
 
 
-ppcGenFn :: forall ids h s tp v ppc
+ppcGenFn :: forall ids s tp v ppc
           . ( ppc ~ MP.AnyPPC v )
          => MP.PPCPrimFn ppc (MC.Value ppc ids) tp
-         -> MSB.CrucGen ppc ids h s (C.Atom s (MS.ToCrucibleType tp))
+         -> MSB.CrucGen ppc ids s (C.Atom s (MS.ToCrucibleType tp))
 ppcGenFn fn = do
-  let f :: MC.Value ppc ids a -> MSB.CrucGen ppc ids h s (A.AtomWrapper (C.Atom s) a)
+  let f :: MC.Value ppc ids a -> MSB.CrucGen ppc ids s (A.AtomWrapper (C.Atom s) a)
       f x = A.AtomWrapper <$> MSB.valueToCrucible x
   r <- FC.traverseFC f fn
   MSB.evalArchStmt (PPCPrimFn r)
 
-ppcGenStmt :: forall v ids h s ppc
+ppcGenStmt :: forall v ids s ppc
             . ( ppc ~ MP.AnyPPC v )
            => MP.PPCStmt ppc (MC.Value ppc ids)
-           -> MSB.CrucGen ppc ids h s ()
+           -> MSB.CrucGen ppc ids s ()
 ppcGenStmt s = do
-  let f :: MC.Value ppc ids a -> MSB.CrucGen ppc ids h s (A.AtomWrapper (C.Atom s) a)
+  let f :: MC.Value ppc ids a -> MSB.CrucGen ppc ids s (A.AtomWrapper (C.Atom s) a)
       f x = A.AtomWrapper <$> MSB.valueToCrucible x
   s' <- TF.traverseF f s
   void (MSB.evalArchStmt (PPCPrimStmt s'))
 
-ppcGenTermStmt :: forall v ids h s ppc
+ppcGenTermStmt :: forall v ids s ppc
                 . ( ppc ~ MP.AnyPPC v )
                => MP.PPCTermStmt ids
                -> MC.RegState (MP.PPCReg ppc) (MC.Value ppc ids)
-               -> MSB.CrucGen ppc ids h s ()
+               -> MSB.CrucGen ppc ids s ()
 ppcGenTermStmt ts _rs =
   void (MSB.evalArchStmt (PPCPrimTerm ts))
 
diff --git a/symbolic/src/Data/Macaw/Symbolic.hs b/symbolic/src/Data/Macaw/Symbolic.hs
index b2efc59a..ce22fffd 100644
--- a/symbolic/src/Data/Macaw/Symbolic.hs
+++ b/symbolic/src/Data/Macaw/Symbolic.hs
@@ -111,13 +111,12 @@ import           GHC.TypeLits
 import           Control.Lens ((^.))
 import           Control.Monad
 import           Control.Monad.IO.Class
-import           Control.Monad.ST (ST, RealWorld, stToIO)
 import           Data.Foldable
 import qualified Data.Map.Strict as Map
 import           Data.Maybe
 import           Data.Parameterized.Context (EmptyCtx, (::>), pattern Empty, pattern (:>))
 import qualified Data.Parameterized.Context as Ctx
-import           Data.Parameterized.Nonce ( NonceGenerator, newSTNonceGenerator )
+import           Data.Parameterized.Nonce ( NonceGenerator, newIONonceGenerator )
 import           Data.Parameterized.Some ( Some(Some) )
 import qualified Data.Parameterized.TraversableFC as FC
 import qualified Data.Vector as V
@@ -225,22 +224,22 @@ type SymArchConstraints arch =
 -- Useful as an alternative to 'mkCrucCFG' if post-processing is
 -- desired (as this is easier to do with the registerized form); use
 -- 'toCoreCFG' to finish.
-mkCrucRegCFG :: forall h arch ids
+mkCrucRegCFG :: forall arch ids
             .  MacawSymbolicArchFunctions arch
                -- ^ Crucible architecture-specific functions.
-            -> C.HandleAllocator h
+            -> C.HandleAllocator
                -- ^ Handle allocator to make function handles
             -> C.FunctionName
                -- ^ Name of function for pretty print purposes.
-            -> (forall s. MacawMonad arch ids h s (CR.Label s, [CR.Block (MacawExt arch) s (MacawFunctionResult arch)]))
+            -> (forall s. MacawMonad arch ids s (CR.Label s, [CR.Block (MacawExt arch) s (MacawFunctionResult arch)]))
                 -- ^ Action to run
-            -> ST h (CR.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
+            -> IO (CR.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
 mkCrucRegCFG archFns halloc nm action = do
   let crucRegTypes = crucArchRegTypes archFns
   let macawStructRepr = C.StructRepr crucRegTypes
   let argTypes = Empty :> macawStructRepr
   h <- C.mkHandle' halloc nm argTypes macawStructRepr
-  Some (ng :: NonceGenerator (ST h) s) <- newSTNonceGenerator
+  Some (ng :: NonceGenerator IO s) <- newIONonceGenerator
   let ps0 = initCrucPersistentState ng
   blockRes <- runMacawMonad ps0 action
   (entry, blks) <-
@@ -257,7 +256,7 @@ mkCrucRegCFG archFns halloc nm action = do
   pure $ CR.SomeCFG rg
 
 -- | Create a Crucible CFG from a list of blocks
-addBlocksCFG :: forall h s arch ids
+addBlocksCFG :: forall s arch ids
              .  MacawSymbolicArchFunctions arch
              -- ^ Crucible specific functions.
              -> MemSegmentMap (M.ArchAddrWidth arch)
@@ -268,7 +267,7 @@ addBlocksCFG :: forall h s arch ids
              -- ^ Function that maps offsets from start of block to Crucible position.
              -> M.Block arch ids
              -- ^ Macaw block for this region.
-             -> MacawMonad arch ids h s (CR.Label s, [CR.Block (MacawExt arch) s (MacawFunctionResult arch)])
+             -> MacawMonad arch ids s (CR.Label s, [CR.Block (MacawExt arch) s (MacawFunctionResult arch)])
 addBlocksCFG archFns baseAddrMap addr posFn macawBlock = do
   crucGenArchConstraints archFns $ do
    -- Map block map to Crucible CFG
@@ -285,10 +284,10 @@ addBlocksCFG archFns baseAddrMap addr posFn macawBlock = do
 --
 -- Also note that any 'M.FetchAndExecute' terminators are turned into Crucible
 -- return statements.
-mkBlocksRegCFG :: forall s arch ids
+mkBlocksRegCFG :: forall arch ids
             .  MacawSymbolicArchFunctions arch
                -- ^ Crucible specific functions.
-            -> C.HandleAllocator s
+            -> C.HandleAllocator
                -- ^ Handle allocator to make the blocks
             -> MemSegmentMap (M.ArchAddrWidth arch)
                -- ^ Map from region indices to their address
@@ -300,7 +299,7 @@ mkBlocksRegCFG :: forall s arch ids
             -- ^ Function that maps offsets from start of block to Crucible position.
             -> M.Block arch ids
             -- ^ List of blocks for this region.
-            -> ST s (CR.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
+            -> IO (CR.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
 mkBlocksRegCFG archFns halloc memBaseVarMap nm addr posFn macawBlock = do
   mkCrucRegCFG archFns halloc nm $ do
     addBlocksCFG archFns memBaseVarMap addr posFn macawBlock
@@ -314,10 +313,10 @@ mkBlocksRegCFG archFns halloc memBaseVarMap nm addr posFn macawBlock = do
 --
 -- Also note that any 'M.FetchAndExecute' terminators are turned into Crucible
 -- return statements.
-mkBlocksCFG :: forall s arch ids
+mkBlocksCFG :: forall arch ids
             .  MacawSymbolicArchFunctions arch
                -- ^ Crucible specific functions.
-            -> C.HandleAllocator s
+            -> C.HandleAllocator
                -- ^ Handle allocator to make the blocks
             -> MemSegmentMap (M.ArchAddrWidth arch)
                -- ^ Map from region indices to their address
@@ -329,15 +328,15 @@ mkBlocksCFG :: forall s arch ids
             -- ^ Function that maps offsets from start of block to Crucible position.
             -> M.Block arch ids
             -- ^ List of blocks for this region.
-            -> ST s (C.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
+            -> IO (C.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
 mkBlocksCFG archFns halloc memBaseVarMap nm addr posFn macawBlock =
   toCoreCFG archFns <$>
   mkBlocksRegCFG archFns halloc memBaseVarMap nm addr posFn macawBlock
 
 -- | Create a map from Macaw @(address, index)@ pairs to Crucible labels
-mkBlockLabelMap :: [M.ParsedBlock arch ids] -> MacawMonad arch ids h s (BlockLabelMap arch s)
+mkBlockLabelMap :: [M.ParsedBlock arch ids] -> MacawMonad arch ids s (BlockLabelMap arch s)
 mkBlockLabelMap blks = foldM insBlock Map.empty blks
- where insBlock :: BlockLabelMap arch s -> M.ParsedBlock arch ids -> MacawMonad arch ids h s (BlockLabelMap arch s)
+ where insBlock :: BlockLabelMap arch s -> M.ParsedBlock arch ids -> MacawMonad arch ids s (BlockLabelMap arch s)
        insBlock m b = do
          let base = M.pblockAddr b
          n <- mmFreshNonce
@@ -388,10 +387,10 @@ termStmtToJump tm0 addr =
 -- This is useful as an alternative to 'mkParsedBlockCFG' if post-processing is
 -- desired (as this is easier on the registerized form). Use 'toCoreCFG' to
 -- finish by translating the registerized CFG to SSA.
-mkParsedBlockRegCFG :: forall h arch ids
+mkParsedBlockRegCFG :: forall arch ids
                  .  MacawSymbolicArchFunctions arch
                  -- ^ Architecture specific functions.
-                 -> C.HandleAllocator h
+                 -> C.HandleAllocator
                  -- ^ Handle allocator to make the blocks
                  -> MemSegmentMap (M.ArchAddrWidth arch)
                  -- ^ Map from region indices to their address
@@ -399,7 +398,7 @@ mkParsedBlockRegCFG :: forall h arch ids
                  -- ^ Function that maps function address to Crucible position
                  -> M.ParsedBlock arch ids
                  -- ^ Block to translate
-                 -> ST h (CR.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
+                 -> IO (CR.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
 mkParsedBlockRegCFG archFns halloc memBaseVarMap posFn b = crucGenArchConstraints archFns $ do
   mkCrucRegCFG archFns halloc "" $ do
     let strippedBlock = b { M.pblockTermStmt = termStmtToReturn (M.pblockTermStmt b) }
@@ -454,10 +453,10 @@ mkParsedBlockRegCFG archFns halloc memBaseVarMap posFn b = crucGenArchConstraint
 --
 -- Note that this function takes 'M.ParsedBlock's, which are the blocks
 -- available in the 'M.DiscoveryFunInfo'.
-mkParsedBlockCFG :: forall s arch ids
+mkParsedBlockCFG :: forall arch ids
                  .  MacawSymbolicArchFunctions arch
                  -- ^ Architecture specific functions.
-                 -> C.HandleAllocator s
+                 -> C.HandleAllocator
                  -- ^ Handle allocator to make the blocks
                  -> MemSegmentMap (M.ArchAddrWidth arch)
                  -- ^ Map from region indices to their address
@@ -465,15 +464,15 @@ mkParsedBlockCFG :: forall s arch ids
                  -- ^ Function that maps function address to Crucible position
                  -> M.ParsedBlock arch ids
                  -- ^ Block to translate
-                 -> ST s (C.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
+                 -> IO (C.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
 mkParsedBlockCFG archFns halloc memBaseVarMap posFn b =
   toCoreCFG archFns <$> mkParsedBlockRegCFG archFns halloc memBaseVarMap posFn b
 
 mkBlockPathRegCFG
-  :: forall h arch ids
+  :: forall arch ids
    . MacawSymbolicArchFunctions arch
   -- ^ Architecture specific functions.
-  -> C.HandleAllocator h
+  -> C.HandleAllocator
   -- ^ Handle allocator to make the blocks
   -> MemSegmentMap (M.ArchAddrWidth arch)
   -- ^ Map from region indices to their address
@@ -481,7 +480,7 @@ mkBlockPathRegCFG
   -- ^ Function that maps function address to Crucible position
   -> [M.ParsedBlock arch ids]
   -- ^ Bloc path to translate
-  -> ST h (CR.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
+  -> IO (CR.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
 mkBlockPathRegCFG arch_fns halloc mem_base_var_map pos_fn blocks =
   crucGenArchConstraints arch_fns $ mkCrucRegCFG arch_fns halloc "" $ do
     let entry_addr = M.pblockAddr $ head blocks
@@ -555,10 +554,10 @@ mkBlockPathRegCFG arch_fns halloc mem_base_var_map pos_fn blocks =
                          init_extra_crucible_blocks ++ concat crucible_blocks)
 
 mkBlockPathCFG
-  :: forall s arch ids
+  :: forall arch ids
    . MacawSymbolicArchFunctions arch
   -- ^ Architecture specific functions.
-  -> C.HandleAllocator s
+  -> C.HandleAllocator
   -- ^ Handle allocator to make the blocks
   -> MemSegmentMap (M.ArchAddrWidth arch)
   -- ^ Map from region indices to their address
@@ -566,7 +565,7 @@ mkBlockPathCFG
   -- ^ Function that maps function address to Crucible position
   -> [M.ParsedBlock arch ids]
   -- ^ Block to translate
-  -> ST s (C.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
+  -> IO (C.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
 mkBlockPathCFG arch_fns halloc mem_base_var_map pos_fn blocks =
   toCoreCFG arch_fns <$>
     mkBlockPathRegCFG arch_fns halloc mem_base_var_map pos_fn blocks
@@ -577,10 +576,10 @@ mkBlockPathCFG arch_fns halloc mem_base_var_map pos_fn blocks =
 -- This is provided as an alternative to 'mkFunCFG' to allow for post-processing
 -- of the CFG (e.g., instrumentation) prior to the SSA conversion (which can be
 -- done using 'toCoreCFG').
-mkFunRegCFG :: forall h arch ids
+mkFunRegCFG :: forall arch ids
          .  MacawSymbolicArchFunctions arch
             -- ^ Architecture specific functions.
-         -> C.HandleAllocator h
+         -> C.HandleAllocator
             -- ^ Handle allocator to make the blocks
          -> MemSegmentMap (M.ArchAddrWidth arch)
             -- ^ Map from region indices to their address
@@ -590,7 +589,7 @@ mkFunRegCFG :: forall h arch ids
             -- ^ Function that maps function address to Crucible position
          -> M.DiscoveryFunInfo arch ids
          -- ^ List of blocks for this region.
-         -> ST h (CR.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
+         -> IO (CR.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
 mkFunRegCFG archFns halloc memBaseVarMap nm posFn fn = crucGenArchConstraints archFns $ do
   mkCrucRegCFG archFns halloc nm $ do
     -- Get entry point address for function
@@ -636,10 +635,10 @@ mkFunRegCFG archFns halloc memBaseVarMap nm posFn fn = crucGenArchConstraints ar
                         initExtraCrucibleBlocks ++ concat restCrucibleBlocks)
 
 -- | Translate a macaw function (passed as a 'M.DiscoveryFunInfo') into a Crucible 'C.CFG' (in SSA form)
-mkFunCFG :: forall s arch ids
+mkFunCFG :: forall arch ids
          .  MacawSymbolicArchFunctions arch
             -- ^ Architecture specific functions.
-         -> C.HandleAllocator s
+         -> C.HandleAllocator
             -- ^ Handle allocator to make the blocks
          -> MemSegmentMap (M.ArchAddrWidth arch)
             -- ^ Map from region indices to their address
@@ -649,7 +648,7 @@ mkFunCFG :: forall s arch ids
             -- ^ Function that maps function address to Crucible position
          -> M.DiscoveryFunInfo arch ids
             -- ^ List of blocks for this region.
-         -> ST s (C.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
+         -> IO (C.SomeCFG (MacawExt arch) (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch))
 mkFunCFG archFns halloc memBaseVarMap nm posFn fn =
   toCoreCFG archFns <$> mkFunRegCFG archFns halloc memBaseVarMap nm posFn fn
 
@@ -879,7 +878,7 @@ runCodeBlock
   -> MacawSymbolicArchFunctions arch
   -- ^ Translation functions
   -> SB.MacawArchEvalFn sym arch
-  -> C.HandleAllocator RealWorld
+  -> C.HandleAllocator
   -> (MM.MemImpl sym, GlobalMap sym (M.ArchAddrWidth arch))
   -> LookupFunctionHandle sym arch
   -> C.CFG (MacawExt arch) blocks (EmptyCtx ::> ArchRegStruct arch) (ArchRegStruct arch)
@@ -892,7 +891,7 @@ runCodeBlock
           (MacawExt arch)
           (C.RegEntry sym (ArchRegStruct arch)))
 runCodeBlock sym archFns archEval halloc (initMem,globs) lookupH g regStruct = do
-  mvar <- stToIO (MM.mkMemVar halloc)
+  mvar <- MM.mkMemVar halloc
   let crucRegTypes = crucArchRegTypes archFns
   let macawStructRepr = C.StructRepr crucRegTypes
 
diff --git a/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs b/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs
index f658317d..d59b7ba9 100644
--- a/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs
+++ b/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs
@@ -80,7 +80,6 @@ module Data.Macaw.Symbolic.CrucGen
 import           Control.Lens hiding (Empty, (:>))
 import           Control.Monad ( foldM )
 import           Control.Monad.Except
-import           Control.Monad.ST
 import           Control.Monad.State.Strict
 import           Data.Bits
 import qualified Data.Kind as K
@@ -194,17 +193,17 @@ data MacawSymbolicArchFunctions arch
     -- LOT of memory---TypeReprs were dominating the heap).
   , crucGenArchRegName :: !(forall tp . M.ArchReg arch tp -> C.SolverSymbol)
     -- ^ Provides a solver name to use for referring to register.
-  , crucGenArchFn :: !(forall ids h s tp
+  , crucGenArchFn :: !(forall ids s tp
                          . M.ArchFn arch (M.Value arch ids) tp
-                         -> CrucGen arch ids h s (CR.Atom s (ToCrucibleType tp)))
+                         -> CrucGen arch ids s (CR.Atom s (ToCrucibleType tp)))
      -- ^ Generate crucible for architecture-specific function.
   , crucGenArchStmt
-    :: !(forall ids h s . M.ArchStmt arch (M.Value arch ids) -> CrucGen arch ids h s ())
+    :: !(forall ids s . M.ArchStmt arch (M.Value arch ids) -> CrucGen arch ids s ())
      -- ^ Generate crucible for architecture-specific statement.
-  , crucGenArchTermStmt :: !(forall ids h s
+  , crucGenArchTermStmt :: !(forall ids s
                                . M.ArchTermStmt arch ids
                                -> M.RegState (M.ArchReg arch) (M.Value arch ids)
-                               -> CrucGen arch ids h s ())
+                               -> CrucGen arch ids s ())
      -- ^ Generate crucible for architecture-specific terminal statement.
   }
 
@@ -570,14 +569,14 @@ instance MacawArchConstraints arch
 type MemSegmentMap w = Map M.RegionIndex (CR.GlobalVar (C.BVType w))
 
 -- | State used for generating blocks
-data CrucGenState arch ids h s
+data CrucGenState arch ids s
    = CrucGenState
    { translateFns       :: !(MacawSymbolicArchFunctions arch)
    , crucMemBaseAddrMap :: !(MemSegmentMap (M.ArchAddrWidth arch))
      -- ^ Map from memory region to base address
    , crucRegIndexMap :: !(RegIndexMap arch)
      -- ^ Map from architecture register to Crucible/Macaw index pair.
-   , crucPState      :: !(CrucPersistentState ids h s)
+   , crucPState      :: !(CrucPersistentState ids s)
      -- ^ State that persists across blocks.
    , crucRegisterReg :: !(CR.Reg s (ArchRegStruct arch))
    , macawPositionFn :: !(M.ArchAddrWord arch -> C.Position)
@@ -623,43 +622,43 @@ instance OrdF (BVAtom s) where
       GTF -> GTF
 
 crucPStateLens ::
-  Simple Lens (CrucGenState arch ids h s) (CrucPersistentState ids h s)
+  Simple Lens (CrucGenState arch ids s) (CrucPersistentState ids s)
 crucPStateLens = lens crucPState (\s v -> s { crucPState = v })
 
 toBitsCacheLens ::
-  Simple Lens (CrucGenState arch ids h s) (MapF (PtrAtom s) (BVAtom s))
+  Simple Lens (CrucGenState arch ids s) (MapF (PtrAtom s) (BVAtom s))
 toBitsCacheLens = lens toBitsCache (\s v -> s { toBitsCache = v })
 
 fromBitsCacheLens ::
-  Simple Lens (CrucGenState arch ids h s) (MapF (BVAtom s) (PtrAtom s))
+  Simple Lens (CrucGenState arch ids s) (MapF (BVAtom s) (PtrAtom s))
 fromBitsCacheLens = lens fromBitsCache (\s v -> s { fromBitsCache = v })
 
 assignValueMapLens ::
-  Simple Lens (CrucPersistentState ids h s)
+  Simple Lens (CrucPersistentState ids s)
               (MapF (M.AssignId ids) (MacawCrucibleValue (CR.Atom s)))
 assignValueMapLens = lens assignValueMap (\s v -> s { assignValueMap = v })
 
-type CrucGenRet arch ids h s = (CrucGenState arch ids h s, CR.TermStmt s (MacawFunctionResult arch))
+type CrucGenRet arch ids s = (CrucGenState arch ids s, CR.TermStmt s (MacawFunctionResult arch))
 
 -- | The Crucible generator monad
 --
 -- This monad provides an environment for constructing Crucible blocks from
 -- Macaw blocks, including the translation of values while preserving sharing
 -- and the construction of a control flow graph.
-newtype CrucGen arch ids h s r
+newtype CrucGen arch ids s r
    = CrucGen { unCrucGen
-               :: CrucGenState arch ids h s
-                  -> (CrucGenState arch ids h s
+               :: CrucGenState arch ids s
+                  -> (CrucGenState arch ids s
                       -> r
-                      -> ST h (CrucGenRet arch ids h s))
-                  -> ST h (CrucGenRet arch ids h s)
+                      -> IO (CrucGenRet arch ids s))
+                  -> IO (CrucGenRet arch ids s)
              }
 
-instance Functor (CrucGen arch ids h s) where
+instance Functor (CrucGen arch ids s) where
   {-# INLINE fmap #-}
   fmap f m = CrucGen $ \s0 cont -> unCrucGen m s0 $ \s1 v -> cont s1 (f v)
 
-instance Applicative (CrucGen arch ids h s) where
+instance Applicative (CrucGen arch ids s) where
   {-# INLINE pure #-}
   pure !r = CrucGen $ \s cont -> cont s r
   {-# INLINE (<*>) #-}
@@ -667,26 +666,26 @@ instance Applicative (CrucGen arch ids h s) where
                       $ \s1 f -> unCrucGen ma s1
                       $ \s2 a -> cont s2 (f a)
 
-instance Monad (CrucGen arch ids h s) where
+instance Monad (CrucGen arch ids s) where
   {-# INLINE (>>=) #-}
   m >>= h = CrucGen $ \s0 cont -> unCrucGen m s0 $ \s1 r -> unCrucGen (h r) s1 cont
 
-instance MonadState (CrucGenState arch ids h s) (CrucGen arch ids h s) where
+instance MonadState (CrucGenState arch ids s) (CrucGen arch ids s) where
   get = CrucGen $ \s cont -> cont s s
   put s = CrucGen $ \_ cont -> cont s ()
 
-cgExecST :: ST h a -> CrucGen arch ids h s a
+cgExecST :: IO a -> CrucGen arch ids s a
 cgExecST m = CrucGen $ \s cont -> m >>= cont s
 
 -- | A NatRepr corresponding to the architecture width.
-archAddrWidth :: CrucGen arch ids h s (ArchAddrWidthRepr arch)
+archAddrWidth :: CrucGen arch ids s (ArchAddrWidthRepr arch)
 archAddrWidth = crucGenAddrWidth . translateFns <$> get
 
 -- | Get current position
-getPos :: CrucGen arch ids h s C.Position
+getPos :: CrucGen arch ids s C.Position
 getPos = gets codePos
 
-addStmt :: CR.Stmt (MacawExt arch) s -> CrucGen arch ids h s ()
+addStmt :: CR.Stmt (MacawExt arch) s -> CrucGen arch ids s ()
 addStmt stmt = seq stmt $ do
   p <- getPos
   s <- get
@@ -696,7 +695,7 @@ addStmt stmt = seq stmt $ do
   put $! s { prevStmts = pstmt : prev }
 
 addTermStmt :: CR.TermStmt s (MacawFunctionResult arch)
-            -> CrucGen arch ids h s a
+            -> CrucGen arch ids s a
 addTermStmt tstmt = do
   CrucGen $ \s _ -> pure (s, tstmt)
 {-
@@ -714,27 +713,27 @@ addTermStmt tstmt = do
 -- Support a friendlier API such as that of Crucible's Generator
 -- monad.)
 addExtraBlock :: CR.Block (MacawExt arch) s (MacawFunctionResult arch)
-              -> CrucGen arch ids h s ()
+              -> CrucGen arch ids s ()
 addExtraBlock blk =
   modify' $ \s@(CrucGenState { extraBlocks = blks }) ->
               s { extraBlocks = blk : blks }
 
-freshValueIndex :: CrucGen arch ids h s (Nonce s tp)
+freshValueIndex :: CrucGen arch ids s (Nonce s tp)
 freshValueIndex = do
   s <- get
   let ps = crucPState s
   let ng = nonceGen ps
   cgExecST $ freshNonce ng
 
-mmNonceGenerator :: MacawMonad arch ids h s (NonceGenerator (ST h) s)
+mmNonceGenerator :: MacawMonad arch ids s (NonceGenerator IO s)
 mmNonceGenerator = gets nonceGen
 
-mmFreshNonce :: MacawMonad arch ids h s (Nonce s tp)
+mmFreshNonce :: MacawMonad arch ids s (Nonce s tp)
 mmFreshNonce = do
   ng <- gets nonceGen
   mmExecST $ freshNonce ng
 
-mkAtom :: C.TypeRepr ctp -> CrucGen arch ids h s (CR.Atom s ctp)
+mkAtom :: C.TypeRepr ctp -> CrucGen arch ids s (CR.Atom s ctp)
 mkAtom tp = do
   archFns <- gets translateFns
   crucGenArchConstraints archFns $ do
@@ -749,7 +748,7 @@ mkAtom tp = do
   pure $! atom
 
 -- | Evaluate the crucible app and return a reference to the result.
-evalAtom :: CR.AtomValue (MacawExt arch) s ctp -> CrucGen arch ids h s (CR.Atom s ctp)
+evalAtom :: CR.AtomValue (MacawExt arch) s ctp -> CrucGen arch ids s (CR.Atom s ctp)
 evalAtom av = do
   archFns <- gets translateFns
   crucGenArchConstraints archFns $ do
@@ -758,11 +757,11 @@ evalAtom av = do
   pure atom
 
 -- | Evaluate the crucible app and return a reference to the result.
-crucibleValue :: C.App (MacawExt arch) (CR.Atom s) ctp -> CrucGen arch ids h s (CR.Atom s ctp)
+crucibleValue :: C.App (MacawExt arch) (CR.Atom s) ctp -> CrucGen arch ids s (CR.Atom s ctp)
 crucibleValue = evalAtom . CR.EvalApp
 
 -- | Evaluate a Macaw expression extension
-evalMacawExt :: MacawExprExtension arch (CR.Atom s) tp -> CrucGen arch ids h s (CR.Atom s tp)
+evalMacawExt :: MacawExprExtension arch (CR.Atom s) tp -> CrucGen arch ids s (CR.Atom s tp)
 evalMacawExt = crucibleValue . C.ExtensionApp
 
 -- | Treat a register value as a bit-vector.
@@ -770,7 +769,7 @@ toBits ::
   (1 <= w) =>
   NatRepr w ->
   CR.Atom s (MM.LLVMPointerType w) ->
-  CrucGen arch ids h s (CR.Atom s (C.BVType w))
+  CrucGen arch ids s (CR.Atom s (C.BVType w))
 toBits w x =
   use (toBitsCacheLens . atF (PtrAtom x)) >>= \case
     Just (BVAtom x') ->
@@ -786,7 +785,7 @@ fromBits ::
   (1 <= w) =>
   NatRepr w ->
   CR.Atom s (C.BVType w) ->
-  CrucGen arch ids h s (CR.Atom s (MM.LLVMPointerType w))
+  CrucGen arch ids s (CR.Atom s (MM.LLVMPointerType w))
 fromBits w x =
   use (fromBitsCacheLens . atF (BVAtom x)) >>= \case
     Just (PtrAtom x') ->
@@ -797,12 +796,12 @@ fromBits w x =
       assign (toBitsCacheLens . atF (PtrAtom x')) (Just (BVAtom x))
       return x'
 
-getRegs :: CrucGen arch ids h s (CR.Atom s (ArchRegStruct arch))
+getRegs :: CrucGen arch ids s (CR.Atom s (ArchRegStruct arch))
 getRegs = gets crucRegisterReg >>= evalAtom . CR.ReadReg
 
 -- | Return the value associated with the given register
 getRegValue :: M.ArchReg arch tp
-            -> CrucGen arch ids h s (CR.Atom s (ToCrucibleType tp))
+            -> CrucGen arch ids s (CR.Atom s (ToCrucibleType tp))
 getRegValue r = do
   archFns <- gets translateFns
   idxMap  <- gets crucRegIndexMap
@@ -816,25 +815,25 @@ getRegValue r = do
       crucibleValue (C.GetStruct regStruct (crucibleIndex idx) tp)
 
 v2c :: M.Value arch ids tp
-    -> CrucGen arch ids h s (CR.Atom s (ToCrucibleType tp))
+    -> CrucGen arch ids s (CR.Atom s (ToCrucibleType tp))
 v2c = valueToCrucible
 
 v2c' :: (1 <= w) =>
        NatRepr w ->
        M.Value arch ids (M.BVType w) ->
-       CrucGen arch ids h s (CR.Atom s (C.BVType w))
+       CrucGen arch ids s (CR.Atom s (C.BVType w))
 v2c' w x = toBits w =<< valueToCrucible x
 
 -- | Evaluate the crucible app and return a reference to the result.
 appAtom :: C.App (MacawExt arch) (CR.Atom s) ctp ->
-            CrucGen arch ids h s (CR.Atom s ctp)
+            CrucGen arch ids s (CR.Atom s ctp)
 appAtom app = evalAtom (CR.EvalApp app)
 
 appBVAtom ::
   (1 <= w) =>
   NatRepr w ->
   C.App (MacawExt arch) (CR.Atom s) (C.BVType w) ->
-  CrucGen arch ids h s (CR.Atom s (MM.LLVMPointerType w))
+  CrucGen arch ids s (CR.Atom s (MM.LLVMPointerType w))
 appBVAtom w app = fromBits w =<< appAtom app
 
 addLemma :: (1 <= x, x + 1 <= y) => NatRepr x -> q y -> LeqProof 1 y
@@ -848,7 +847,7 @@ addLemma x y =
 
 
 -- | Create a crucible value for a bitvector literal.
-bvLit :: (1 <= w) => NatRepr w -> Integer -> CrucGen arch ids h s (CR.Atom s (C.BVType w))
+bvLit :: (1 <= w) => NatRepr w -> Integer -> CrucGen arch ids s (CR.Atom s (C.BVType w))
 bvLit w i = crucibleValue (C.BVLit w (i .&. maxUnsigned w))
 
 bitOp2 :: (1 <= w)
@@ -858,14 +857,14 @@ bitOp2 :: (1 <= w)
            -> C.App (MacawExt arch) (CR.Atom s) (C.BVType w))
        -> M.Value arch ids (M.BVType w)
        -> M.Value arch ids (M.BVType w)
-       -> CrucGen arch ids h s (CR.Atom s (MM.LLVMPointerType w))
+       -> CrucGen arch ids s (CR.Atom s (MM.LLVMPointerType w))
 bitOp2 w f x y = fromBits w =<< appAtom =<< f <$> v2c' w x <*> v2c' w y
 
 
 appToCrucible
-  :: forall arch ids h s tp
+  :: forall arch ids s tp
   . M.App (M.Value arch ids) tp
-  -> CrucGen arch ids h s (CR.Atom s (ToCrucibleType tp))
+  -> CrucGen arch ids s (CR.Atom s (ToCrucibleType tp))
 appToCrucible app = do
   archFns <- gets translateFns
   crucGenArchConstraints archFns $ do
@@ -1050,7 +1049,7 @@ appToCrucible app = do
         let bvBit
               :: (1 <= i, i <= n)
               => NatRepr i
-              -> CrucGen arch ids h s (CR.Atom s (C.BVType n))
+              -> CrucGen arch ids s (CR.Atom s (C.BVType n))
             bvBit i | Refl <- minusPlusCancel i (knownNat @1) = do
               b <- appAtom $
                 C.BVSelect (subNat i (knownNat @1)) (knownNat @1) w x'
@@ -1094,7 +1093,7 @@ countZeros :: (1 <= w) =>
   NatRepr w ->
   (NatRepr w -> CR.Atom s (C.BVType w) -> CR.Atom s (C.BVType w) -> C.App (MacawExt arch) (CR.Atom s) (C.BVType w)) ->
   M.Value arch ids (M.BVType w) ->
-  CrucGen arch ids h s (CR.Atom s (MM.LLVMPointerType w))
+  CrucGen arch ids s (CR.Atom s (MM.LLVMPointerType w))
 countZeros w f vx = do
   cx <- v2c vx >>= toBits w
   isZeros <- forM [0..intValue w-1] $ \i -> do
@@ -1111,7 +1110,7 @@ countZeros w f vx = do
 --
 -- This is in the 'CrucGen' monad so that it can preserve sharing in terms.
 valueToCrucible :: M.Value arch ids tp
-                -> CrucGen arch ids h s (CR.Atom s (ToCrucibleType tp))
+                -> CrucGen arch ids s (CR.Atom s (ToCrucibleType tp))
 valueToCrucible v = do
  archFns <- gets translateFns
  crucGenArchConstraints archFns $ do
@@ -1138,21 +1137,21 @@ valueToCrucible v = do
 
 -- | Create a fresh symbolic value of the given type.
 freshSymbolic :: M.TypeRepr tp
-              -> CrucGen arch ids h s (CR.Atom s (ToCrucibleType tp))
+              -> CrucGen arch ids s (CR.Atom s (ToCrucibleType tp))
 freshSymbolic repr = evalMacawStmt (MacawFreshSymbolic repr)
 
 evalMacawStmt :: MacawStmtExtension arch (CR.Atom s) tp ->
-                  CrucGen arch ids h s (CR.Atom s tp)
+                  CrucGen arch ids s (CR.Atom s tp)
 evalMacawStmt = evalAtom . CR.EvalExt
 
 -- | Embed an architecture-specific Macaw statement into a Crucible program
 --
 -- All architecture-specific statements return values (which can be unit).
-evalArchStmt :: MacawArchStmtExtension arch (CR.Atom s) tp -> CrucGen arch ids h s (CR.Atom s tp)
+evalArchStmt :: MacawArchStmtExtension arch (CR.Atom s) tp -> CrucGen arch ids s (CR.Atom s tp)
 evalArchStmt = evalMacawStmt . MacawArchStmtExtension
 
 assignRhsToCrucible :: M.AssignRhs arch (M.Value arch ids) tp
-                    -> CrucGen arch ids h s (CR.Atom s (ToCrucibleType tp))
+                    -> CrucGen arch ids s (CR.Atom s (ToCrucibleType tp))
 assignRhsToCrucible rhs =
  gets translateFns >>= \archFns ->
  crucGenArchConstraints archFns $
@@ -1173,7 +1172,7 @@ assignRhsToCrucible rhs =
       fns <- translateFns <$> get
       crucGenArchFn fns f
 
-addMacawStmt :: forall arch ids h s . M.ArchSegmentOff arch -> M.Stmt arch ids -> CrucGen arch ids h s ()
+addMacawStmt :: forall arch ids s . M.ArchSegmentOff arch -> M.Stmt arch ids -> CrucGen arch ids s ()
 addMacawStmt baddr stmt =
   gets translateFns >>= \archFns ->
   crucGenArchConstraints archFns $
@@ -1213,9 +1212,9 @@ addMacawStmt baddr stmt =
       void $ evalMacawStmt crucStmt
 
 -- | Create a crucible struct for registers from a register state.
-createRegStruct :: forall arch ids h s
+createRegStruct :: forall arch ids s
                 .  M.RegState (M.ArchReg arch) (M.Value arch ids)
-                -> CrucGen arch ids h s (CR.Atom s (ArchRegStruct arch))
+                -> CrucGen arch ids s (CR.Atom s (ArchRegStruct arch))
 createRegStruct regs = do
   archFns <- gets translateFns
 
@@ -1233,9 +1232,9 @@ createRegStruct regs = do
   updates <- createRegUpdates regs
   foldM addUpdate startingVals updates
 
-createRegUpdates :: forall arch ids h s
+createRegUpdates :: forall arch ids s
                  .  M.RegState (M.ArchReg arch) (M.Value arch ids)
-                 -> CrucGen arch ids h s
+                 -> CrucGen arch ids s
                       [Pair (Ctx.Index (MacawCrucibleRegTypes arch)) (CR.Atom s)]
 createRegUpdates regs = do
   archFns <- gets translateFns
@@ -1249,7 +1248,7 @@ createRegUpdates regs = do
           Just idx -> Just . Pair (crucibleIndex idx) <$> valueToCrucible val
 
 addMacawTermStmt :: M.TermStmt arch ids
-                 -> CrucGen arch ids h s ()
+                 -> CrucGen arch ids s ()
 addMacawTermStmt tstmt =
   case tstmt of
     M.FetchAndExecute regs -> do
@@ -1265,24 +1264,24 @@ addMacawTermStmt tstmt =
 -----------------
 
 -- | Monad for adding new blocks to a state.
-newtype MacawMonad arch ids h s a
-  = MacawMonad ( ExceptT String (StateT (CrucPersistentState ids h s) (ST h)) a)
+newtype MacawMonad arch ids s a
+  = MacawMonad ( ExceptT String (StateT (CrucPersistentState ids s) IO) a)
   deriving ( Functor
            , Applicative
            , Monad
            , MonadError String
-           , MonadState (CrucPersistentState ids h s)
+           , MonadState (CrucPersistentState ids s)
            )
 
-runMacawMonad :: CrucPersistentState ids h s
-              -> MacawMonad arch ids h s a
-              -> ST h (Either String a, CrucPersistentState ids h s)
+runMacawMonad :: CrucPersistentState ids s
+              -> MacawMonad arch ids s a
+              -> IO (Either String a, CrucPersistentState ids s)
 runMacawMonad s (MacawMonad m) = runStateT (runExceptT m) s
 
-mmExecST :: ST h a -> MacawMonad arch ids h s a
+mmExecST :: IO a -> MacawMonad arch ids s a
 mmExecST = MacawMonad . lift . lift
 
-runCrucGen :: forall arch ids h s
+runCrucGen :: forall arch ids s
            .  MacawSymbolicArchFunctions arch
            -> MemSegmentMap (M.ArchAddrWidth arch)
               -- ^ Base address map
@@ -1292,8 +1291,8 @@ runCrucGen :: forall arch ids h s
               -- ^ Label for this block
            -> CR.Reg s (ArchRegStruct arch)
               -- ^ Crucible register for struct containing all Macaw registers.
-           -> CrucGen arch ids h s ()
-           -> MacawMonad arch ids h s
+           -> CrucGen arch ids s ()
+           -> MacawMonad arch ids s
                 ( CR.Block (MacawExt arch ) s (MacawFunctionResult arch)
                     -- Block created
                 , [CR.Block (MacawExt arch) s (MacawFunctionResult arch)]
@@ -1338,7 +1337,7 @@ addMacawBlock :: M.MemWidth (M.ArchAddrWidth arch)
               -> (M.ArchAddrWord arch -> C.Position)
                  -- ^ Function for generating position from offset from start of this block.
               -> M.Block arch ids
-              -> MacawMonad arch ids h s
+              -> MacawMonad arch ids s
                    ( CR.Block (MacawExt arch) s (MacawFunctionResult arch)
                    , [CR.Block (MacawExt arch) s (MacawFunctionResult arch)]
                    )
@@ -1372,7 +1371,7 @@ parsedBlockLabel blockLabelMap addr =
 
 -- | DO NOT CALL THIS FROM USER CODE.  We count on the registers not
 -- changing until the end of the block.
-setMachineRegs :: CR.Atom s (ArchRegStruct arch) -> CrucGen arch ids h s ()
+setMachineRegs :: CR.Atom s (ArchRegStruct arch) -> CrucGen arch ids s ()
 setMachineRegs newRegs = do
   regReg <- gets crucRegisterReg
   addStmt $ CR.SetReg regReg newRegs
@@ -1385,7 +1384,7 @@ addMacawParsedTermStmt :: BlockLabelMap arch s
                        -> M.ArchSegmentOff arch
                           -- ^ Address of this block
                        -> M.ParsedTermStmt arch ids
-                       -> CrucGen arch ids h s ()
+                       -> CrucGen arch ids s ()
 addMacawParsedTermStmt blockLabelMap thisAddr tstmt = do
  archFns <- translateFns <$> get
  crucGenArchConstraints archFns $ do
@@ -1435,11 +1434,11 @@ addMacawParsedTermStmt blockLabelMap thisAddr tstmt = do
       msgVal <- crucibleValue $ C.TextLit $ Text.pack $ "Could not identify block at " ++ show thisAddr
       addTermStmt $ CR.ErrorStmt msgVal
 
-addSwitch :: forall arch s ids h
+addSwitch :: forall arch s ids
            . BlockLabelMap arch s
           -> M.ArchAddrValue arch ids
           -> Vec.Vector (M.ArchSegmentOff arch)
-          -> CrucGen arch ids h s ()
+          -> CrucGen arch ids s ()
 addSwitch blockLabelMap idx possibleAddrs = do
   archFns <- translateFns <$> get
   crucGenArchConstraints archFns $ do
@@ -1468,7 +1467,7 @@ addSwitch blockLabelMap idx possibleAddrs = do
                , CR.TermStmt s (MacawFunctionResult arch) )
             -> ( Int
                , M.ArchSegmentOff arch )
-            -> CrucGen arch ids h s
+            -> CrucGen arch ids s
                  ( [CR.Stmt (MacawExt arch) s]
                  , CR.TermStmt s (MacawFunctionResult arch) )
       chain (elsStmts, elsTerm) (thnIdx, thnAddr) = do
@@ -1524,7 +1523,7 @@ addSwitch blockLabelMap idx possibleAddrs = do
   mapM_ addStmt stmts
   addTermStmt termStmt
 
-addParsedBlock :: forall arch ids h s
+addParsedBlock :: forall arch ids s
                .  MacawSymbolicArchFunctions arch
                -> MemSegmentMap (M.ArchAddrWidth arch)
                -- ^ Base address map
@@ -1535,7 +1534,7 @@ addParsedBlock :: forall arch ids h s
                -> CR.Reg s (ArchRegStruct arch)
                     -- ^ Register that stores Macaw registers
                -> M.ParsedBlock arch ids
-               -> MacawMonad arch ids h s [CR.Block (MacawExt arch) s (MacawFunctionResult arch)]
+               -> MacawMonad arch ids s [CR.Block (MacawExt arch) s (MacawFunctionResult arch)]
 addParsedBlock archFns memSegMap blockLabelMap posFn regReg macawBlock = do
   crucGenArchConstraints archFns $ do
   let base = M.pblockAddr macawBlock
diff --git a/symbolic/src/Data/Macaw/Symbolic/PersistentState.hs b/symbolic/src/Data/Macaw/Symbolic/PersistentState.hs
index 5c422f58..3b81d10d 100644
--- a/symbolic/src/Data/Macaw/Symbolic/PersistentState.hs
+++ b/symbolic/src/Data/Macaw/Symbolic/PersistentState.hs
@@ -44,7 +44,6 @@ module Data.Macaw.Symbolic.PersistentState
   ) where
 
 
-import           Control.Monad.ST (ST)
 import qualified Data.Kind as K
 import qualified Data.Macaw.CFG as M
 import qualified Data.Macaw.Types as M
@@ -227,9 +226,9 @@ instance TraversableFC MacawCrucibleValue where
 -- CrucPersistentState
 
 -- | State that needs to be persisted across block translations
-data CrucPersistentState ids h s
+data CrucPersistentState ids s
    = CrucPersistentState
-   { nonceGen :: NonceGenerator (ST h) s
+   { nonceGen :: NonceGenerator IO s
      -- ^ Generator used to get fresh ids for Crucible atoms.
    , assignValueMap ::
       !(MapF (M.AssignId ids) (MacawCrucibleValue (CR.Atom s)))
@@ -237,8 +236,8 @@ data CrucPersistentState ids h s
    }
 
 -- | Initial crucible persistent state
-initCrucPersistentState :: NonceGenerator (ST h) s
-                        -> CrucPersistentState ids h s
+initCrucPersistentState :: NonceGenerator IO s
+                        -> CrucPersistentState ids s
 initCrucPersistentState ng =
   CrucPersistentState
       { nonceGen       = ng
diff --git a/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs b/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs
index 2d1747a5..a4fb8baf 100644
--- a/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs
+++ b/x86_symbolic/src/Data/Macaw/X86/Symbolic.hs
@@ -276,27 +276,27 @@ instance TraversableFC X86StmtExtension where
 type instance MacawArchStmtExtension M.X86_64 = X86StmtExtension
 
 
-crucGenX86Fn :: forall ids h s tp. M.X86PrimFn (M.Value M.X86_64 ids) tp
-             -> CrucGen M.X86_64 ids h s (C.Atom s (ToCrucibleType tp))
+crucGenX86Fn :: forall ids s tp. M.X86PrimFn (M.Value M.X86_64 ids) tp
+             -> CrucGen M.X86_64 ids s (C.Atom s (ToCrucibleType tp))
 crucGenX86Fn fn = do
-  let f ::  M.Value arch ids a -> CrucGen arch ids h s (AtomWrapper (C.Atom s) a)
+  let f ::  M.Value arch ids a -> CrucGen arch ids s (AtomWrapper (C.Atom s) a)
       f x = AtomWrapper <$> valueToCrucible x
   r <- traverseFC f fn
   evalArchStmt (X86PrimFn r)
 
 
-crucGenX86Stmt :: forall ids h s
+crucGenX86Stmt :: forall ids s
                 . M.X86Stmt (M.Value M.X86_64 ids)
-               -> CrucGen M.X86_64 ids h s ()
+               -> CrucGen M.X86_64 ids s ()
 crucGenX86Stmt stmt = do
-  let f :: M.Value M.X86_64 ids a -> CrucGen M.X86_64 ids h s (AtomWrapper (C.Atom s) a)
+  let f :: M.Value M.X86_64 ids a -> CrucGen M.X86_64 ids s (AtomWrapper (C.Atom s) a)
       f x = AtomWrapper <$> valueToCrucible x
   stmt' <- traverseF f stmt
   void (evalArchStmt (X86PrimStmt stmt'))
 
 crucGenX86TermStmt :: M.X86TermStmt ids
                    -> M.RegState M.X86Reg (M.Value M.X86_64 ids)
-                   -> CrucGen M.X86_64 ids h s ()
+                   -> CrucGen M.X86_64 ids s ()
 crucGenX86TermStmt tstmt _regs =
   void (evalArchStmt (X86PrimTerm tstmt))
 
diff --git a/x86_symbolic/tests/Main.hs b/x86_symbolic/tests/Main.hs
index 37ffce72..2bebf26b 100644
--- a/x86_symbolic/tests/Main.hs
+++ b/x86_symbolic/tests/Main.hs
@@ -95,7 +95,7 @@ main = do
       [] -> fail "Could not find add function"
       _ -> fail "Found multiple add functions"
 
-  memBaseVar <- stToIO $ C.freshGlobalVar halloc "add_mem_base" C.knownRepr
+  memBaseVar <- C.freshGlobalVar halloc "add_mem_base" C.knownRepr
 
   let memBaseVarMap :: MS.MemSegmentMap 64
       memBaseVarMap = Map.singleton 1 memBaseVar
@@ -113,7 +113,7 @@ main = do
         putStrLn $ "Analyzing " ++ show addr
 
   (_, Some funInfo) <- stToIO $ M.analyzeFunction logFn addAddr M.UserRequest ds0
-  C.SomeCFG g <- stToIO $ MS.mkFunCFG x86ArchFns halloc memBaseVarMap "add" posFn funInfo
+  C.SomeCFG g <- MS.mkFunCFG x86ArchFns halloc memBaseVarMap "add" posFn funInfo
 
   regs <- MS.macawAssignToCrucM (mkReg x86ArchFns sym) (MS.crucGenRegAssignment x86ArchFns)