diff --git a/deps/crucible b/deps/crucible
index 6fad4300..459e8db3 160000
--- a/deps/crucible
+++ b/deps/crucible
@@ -1 +1 @@
-Subproject commit 6fad4300d50c15ad926eedab7a98109bb36caa90
+Subproject commit 459e8db323b164ad48f52fb232a6a3331e99be69
diff --git a/symbolic-syntax/src/Data/Macaw/Symbolic/Syntax.hs b/symbolic-syntax/src/Data/Macaw/Symbolic/Syntax.hs
index 83b97c01..4ef22415 100644
--- a/symbolic-syntax/src/Data/Macaw/Symbolic/Syntax.hs
+++ b/symbolic-syntax/src/Data/Macaw/Symbolic/Syntax.hs
@@ -42,7 +42,7 @@ import qualified Lang.Crucible.CFG.Reg as LCCR
 import qualified Lang.Crucible.LLVM.MemModel as LCLM
 import qualified Lang.Crucible.Syntax.Atoms as LCSA
 import qualified Lang.Crucible.Syntax.Concrete as LCSC
-import qualified Lang.Crucible.Syntax.ExprParse as LCSE
+import qualified Lang.Crucible.Syntax.Monad as LCSM
 import qualified Lang.Crucible.Types as LCT
 import qualified Lang.Crucible.LLVM.Syntax as LCLS
 
@@ -50,7 +50,7 @@ import qualified What4.Interface as WI
 import qualified What4.ProgramLoc as WP
 
 -- | The constraints on the abstract parser monad
-type ExtensionParser m ext s = ( LCSE.MonadSyntax LCSA.Atomic m
+type ExtensionParser m ext s = ( LCSM.MonadSyntax LCSA.Atomic m
                                , MonadWriter [WP.Posd (LCCR.Stmt ext s)] m
                                , MonadState (LCSC.SyntaxState s) m
                                , MonadIO m
@@ -169,14 +169,14 @@ extensionParser :: forall s m ext arch w
                 -- ^ A pair containing a result type and an atom of that type
 extensionParser wrappers hooks =
   let ?parserHooks = hooks in
-  LCSE.depCons LCSC.atomName $ \name ->
+  LCSM.depCons LCSC.atomName $ \name ->
     case name of
       LCSA.AtomName "pointer-read" -> do
         -- Pointer reads are a special case because we must parse the type of
         -- the value to read as well as the endianness of the read before
         -- parsing the additional arguments as Atoms.
-        LCSE.depCons LCSC.isType $ \(Some tp) ->
-          LCSE.depCons LCSC.atomName $ \endiannessName ->
+        LCSM.depCons LCSC.isType $ \(Some tp) ->
+          LCSM.depCons LCSC.atomName $ \endiannessName ->
             case endiannessFromAtomName endiannessName of
               Just endianness ->
                 let readWrapper =
@@ -187,8 +187,8 @@ extensionParser wrappers hooks =
         -- Pointer writes are a special case because we must parse the type of
         -- the value to write out as well as the endianness of the write before
         -- parsing the additional arguments as Atoms.
-        LCSE.depCons LCSC.isType $ \(Some tp) ->
-          LCSE.depCons LCSC.atomName $ \endiannessName ->
+        LCSM.depCons LCSC.isType $ \(Some tp) ->
+          LCSM.depCons LCSC.atomName $ \endiannessName ->
             case endiannessFromAtomName endiannessName of
               Just endianness ->
                 let writeWrapper =
@@ -199,7 +199,7 @@ extensionParser wrappers hooks =
         -- Bitvector literals with a type argument are a special case.  We must
         -- parse the type argument separately before parsing the remaining
         -- argument as an Atom.
-        LCSE.depCons LCSC.isType $ \(Some tp) ->
+        LCSM.depCons LCSC.isType $ \(Some tp) ->
           case tp of
             LCT.BVRepr{} ->
               go (SomeExtensionWrapper (buildBvTypedLitWrapper tp))
@@ -213,7 +213,7 @@ extensionParser wrappers hooks =
        => SomeExtensionWrapper arch
        -> m (Some (LCCR.Atom s))
     go (SomeExtensionWrapper wrapper) = do
-      loc <- LCSE.position
+      loc <- LCSM.position
       -- Generate atoms for the arguments to this extension
       operandAtoms <- LCSC.operands (extArgTypes wrapper)
       -- Pass these atoms to the extension wrapper and return an atom for the
@@ -518,8 +518,8 @@ extensionWrappers = Map.fromList
   , (LCSA.AtomName "pointer-make-null", SomeExtensionWrapper wrapMakeNull)
   ]
 
-ptrTypeParser :: LCSE.MonadSyntax LCSA.Atomic m => m (Some LCT.TypeRepr)
-ptrTypeParser = LCSE.describe "Pointer type" $ do
+ptrTypeParser :: LCSM.MonadSyntax LCSA.Atomic m => m (Some LCT.TypeRepr)
+ptrTypeParser = LCSM.describe "Pointer type" $ do
   LCSC.BoundedNat n <- LCLS.pointerTypeParser
   pure (Some (LCLM.LLVMPointerRepr n))
 
@@ -534,10 +534,10 @@ machineCodeParserHooks
 machineCodeParserHooks proxy hooks =
   LCSC.ParserHooks
   { LCSC.extensionTypeParser =
-      LCSE.describe "Macaw type" $
-        LCSE.call (ptrTypeParser <|> LCSC.extensionTypeParser hooks)
+      LCSM.describe "Macaw type" $
+        LCSM.call (ptrTypeParser <|> LCSC.extensionTypeParser hooks)
   , LCSC.extensionParser =
-      LCSE.describe "Macaw operation" $ do
+      LCSM.describe "Macaw operation" $ do
         let extParser = extensionParser extensionWrappers (machineCodeParserHooks proxy hooks)
-        LCSE.call (extParser <|> LCSC.extensionParser hooks)
+        LCSM.call (extParser <|> LCSC.extensionParser hooks)
   }