diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,21 @@
+# 0.7.2 -- 2025-03-21
+
+* Add support for the Bitwuzla SMT solver.
+* Add `--debug` option for starting the Crucible debugger.
+* For the sake of the `--debug` flag, Crux now depends on the
+  `crucible-{debug,syntax}` packages.
+
+# 0.7.1 -- 2024-08-30
+
+* Add support for GHC 9.8
+
+# 0.7 -- 2024-02-05
+
+* Add a `Crux.Overrides` module, which defines common functionality for defining
+  overrides, which are shared among several Crux backends.
+
+# 0.6
+
+* Corresponds to the 0.6 release of `crux-llvm` and `crux-mir`.
+* `SimulatorCallbacks` now returns `SimulatorHooks`, a new data type that
+  allows hooking into the simulation process at various steps.
diff --git a/crux.cabal b/crux.cabal
--- a/crux.cabal
+++ b/crux.cabal
@@ -1,6 +1,6 @@
 Cabal-version: 2.2
 Name:          crux
-Version:       0.7.1
+Version:       0.7.2
 Copyright:     (c) Galois, Inc. 2018-2022
 Author:        sweirich@galois.com
 Maintainer:    rscott@galois.com, kquick@galois.com, langston@galois.com
@@ -17,6 +17,8 @@
   verification, usually by embedding verification specifications in
   the source language.
 
+extra-doc-files:  CHANGELOG.md
+
 source-repository head
   type:     git
   location: https://github.com/GaloisInc/crucible
@@ -34,6 +36,8 @@
     containers,
     contravariant >= 1.5 && < 1.6,
     crucible,
+    crucible-debug,
+    crucible-syntax,
     directory,
     filepath,
     generic-lens,
diff --git a/src/Crux.hs b/src/Crux.hs
--- a/src/Crux.hs
+++ b/src/Crux.hs
@@ -28,6 +28,7 @@
   , module Crux.Log
   ) where
 
+import qualified Control.Applicative as Applicative
 import qualified Control.Exception as Ex
 import           Control.Lens
 import           Control.Monad ( unless, void, when )
@@ -53,6 +54,7 @@
 import           System.IO ( Handle, hPutStr, stdout, stderr )
 
 import           Data.Parameterized.Classes
+import qualified Data.Parameterized.Map as MapF
 import           Data.Parameterized.Nonce (newIONonceGenerator, NonceGenerator)
 import           Data.Parameterized.Some ( Some(..) )
 
@@ -60,6 +62,7 @@
 import           Lang.Crucible.Backend.Online
 import qualified Lang.Crucible.Backend.Simple as CBS
 import           Lang.Crucible.CFG.Extension
+import qualified Lang.Crucible.Debug as Debug
 import           Lang.Crucible.Simulator
 import           Lang.Crucible.Simulator.BoundedExec
 import           Lang.Crucible.Simulator.BoundedRecursion
@@ -67,6 +70,7 @@
 import           Lang.Crucible.Simulator.PathSplitting
 import           Lang.Crucible.Simulator.PositionTracking
 import           Lang.Crucible.Simulator.Profiling
+import qualified Lang.Crucible.Syntax.Concrete as Syn
 import           Lang.Crucible.Types
 
 
@@ -76,6 +80,7 @@
 import           What4.Interface (IsExprBuilder, getConfiguration)
 import           What4.Protocol.Online (OnlineSolver)
 import qualified What4.Solver as WS
+import           What4.Solver.Bitwuzla (bitwuzlaTimeout)
 import           What4.Solver.CVC4 (cvc4Timeout)
 import           What4.Solver.CVC5 (cvc5Timeout)
 import           What4.Solver.Yices (yicesEnableMCSat, yicesGoalTimeout)
@@ -364,6 +369,7 @@
         CCS.CVC5 -> withOnlineBackendFM WE.FloatRealRepr
         CCS.STP -> withOnlineBackendFM WE.FloatRealRepr
         CCS.Z3 -> withOnlineBackendFM WE.FloatIEEERepr
+        CCS.Bitwuzla -> withOnlineBackendFM WE.FloatIEEERepr
     fm -> fail ("Unknown floating point mode: " ++ fm ++ "; expected one of [real|ieee|uninterpreted|default]")
 
   where
@@ -415,6 +421,11 @@
          Just s -> symCfg sym z3Timeout (floor (s * 1000))
          Nothing -> return ()
        k bak
+     CCS.Bitwuzla -> withBitwuzlaOnlineBackend sym unsatCoreFeat extraFeatures $ \bak -> do
+       case goalTimeout cruxOpts of
+         Just s -> symCfg sym bitwuzlaTimeout (floor (s * 1000))
+         Nothing -> return ()
+       k bak
      CCS.STP -> do
        -- We don't have a timeout option for STP
        case goalTimeout cruxOpts of
@@ -556,6 +567,7 @@
     CCS.SolverOnline CCS.STP -> k WS.stpAdapter
     CCS.SolverOnline CCS.Yices -> k WS.yicesAdapter
     CCS.SolverOnline CCS.Z3 -> k WS.z3Adapter
+    CCS.SolverOnline CCS.Bitwuzla -> k WS.bitwuzlaAdapter
 
 withSolverAdapters :: [CCS.SolverOffline] -> ([WS.SolverAdapter st] -> a) -> a
 withSolverAdapters solverOffs k =
@@ -667,14 +679,38 @@
     RunnableStateWithExtensions initSt exts <- setup bak monline
     explainFailure <- onError bak
 
+    -- This can't be initialized with the rest of the execution features,
+    -- because it is not a 'GenericExecutionFeature'.
+    --
+    -- Ideally, we would use language-extension-specific command extensions
+    -- (e.g., LLVM commands for Crux-LLVM) and parser hooks, but that would
+    -- require some refactoring to pass those in...
+    let debugging = debug cruxOpts
+    debugger <-
+      if debugging
+      then do
+        let ?parserHooks = Syn.ParserHooks Applicative.empty Applicative.empty
+        let cExts = Debug.voidExts
+        inps <- Debug.defaultDebuggerInputs cExts
+        dbg <-
+          Debug.debugger
+            cExts
+            Debug.voidImpl
+            (Debug.IntrinsicPrinters MapF.empty)
+            inps
+            Debug.defaultDebuggerOutputs
+            UnitRepr
+        pure [dbg]
+      else pure []
+
     -- execute the simulator
     case pathStrategy cruxOpts of
       AlwaysMergePaths ->
-        do res <- executeCrucible (map genericToExecutionFeature execFeatures ++ exts) initSt
+        do res <- executeCrucible (map genericToExecutionFeature execFeatures ++ exts ++ debugger) initSt
            void $ resultCont compRef glsRef frm explainFailure (Result res)
       SplitAndExploreDepthFirst ->
         do (i,ws) <- executeCrucibleDFSPaths
-                         (map genericToExecutionFeature execFeatures ++ exts)
+                         (map genericToExecutionFeature execFeatures ++ exts ++ debugger)
                          initSt
                          (resultCont compRef glsRef frm explainFailure . Result)
            sayCrux (Log.TotalPathsExplored i)
diff --git a/src/Crux/Config/Common.hs b/src/Crux/Config/Common.hs
--- a/src/Crux/Config/Common.hs
+++ b/src/Crux/Config/Common.hs
@@ -205,6 +205,9 @@
   , outputOptions            :: OutputOptions
     -- ^ Output options grouped together for easy transfer to the logger
 
+  , debug                    :: Bool
+    -- ^ Drop into the Crucible debugger before simulation begins
+
   }
   deriving (Generic)
 
@@ -364,6 +367,10 @@
 
           onlineProblemFeatures <- pure noFeatures
 
+          debug <-
+            section "debug" yesOrNoSpec False
+            "Drop into the Crucible debugger before simulation begins"
+
           pure CruxOptions
             { outputOptions = OutputOptions
               { colorOptions = ColorOptions
@@ -525,6 +532,10 @@
          ++ " i.e. one of [real|ieee|uninterpreted|default]. "
          ++ "Default representation is solver specific: [cvc4|yices]=>real, z3=>ieee.")
         $ ReqArg "FPREP" $ \v opts -> Right opts { floatMode = map toLower v }
+
+      , Option [] ["debug"]
+        "Drop into the Crucible debugger before simulation begins"
+        $ NoArg $ \opts -> Right opts { debug = True }
       ]
   }
 
diff --git a/src/Crux/Config/Solver.hs b/src/Crux/Config/Solver.hs
--- a/src/Crux/Config/Solver.hs
+++ b/src/Crux/Config/Solver.hs
@@ -23,7 +23,7 @@
 
 import qualified Crux.Config.Common as CCC
 
-data SolverOnline = Yices | Z3 | CVC4 | CVC5 | STP
+data SolverOnline = Yices | Z3 | CVC4 | CVC5 | STP | Bitwuzla
   deriving (Eq, Ord, Show)
 data SolverOffline = SolverOnline SolverOnline | Boolector | DReal
   deriving (Eq, Ord, Show)
@@ -43,6 +43,7 @@
       STP -> k WEB.FloatRealRepr
       Yices -> k WEB.FloatRealRepr
       Z3 -> k WEB.FloatIEEERepr
+      Bitwuzla -> k WEB.FloatIEEERepr
 
 instance HasDefaultFloatRepr SolverOffline where
   withDefaultFloatRepr st s k =
@@ -124,11 +125,12 @@
       "cvc4" -> pure (SolverOnline CVC4)
       "cvc5" -> pure (SolverOnline CVC5)
       "stp" -> pure (SolverOnline STP)
-      _ -> invalid (printf "%s is not a valid solver (expected dreal, boolector, z3, yices, cvc4, cvc5, or stp)" s)
+      "bitwuzla" -> pure (SolverOnline Bitwuzla)
+      _ -> invalid (printf "%s is not a valid solver (expected dreal, boolector, z3, yices, cvc4, cvc5, stp, or bitwuzla)" s)
 
 asManyOfflineSolvers :: String -> Validated [SolverOffline]
 asManyOfflineSolvers s
-  | s == "all"         = asManyOfflineSolvers "dreal,boolector,z3,yices,cvc4,cvc5,stp"
+  | s == "all"         = asManyOfflineSolvers "dreal,boolector,z3,yices,cvc4,cvc5,stp,bitwuzla"
   | length solvers > 1 = traverse asAnyOfflineSolver solvers
   | otherwise          = invalid (printf "%s is not a valid solver list (expected 'all' or a comma separated list of solvers)" s)
   where
@@ -143,7 +145,8 @@
     "cvc5" -> pure CVC5
     "z3" -> pure Z3
     "stp" -> pure STP
-    _ -> invalid (printf "%s is not a valid online solver (expected yices, cvc4, cvc5, z3, or stp)" s)
+    "bitwuzla" -> pure Bitwuzla
+    _ -> invalid (printf "%s is not a valid online solver (expected yices, cvc4, cvc5, z3, stp, or bitwuzla)" s)
 
 -- | Examine a 'CCC.CruxOptions' and determine what solver configuration to use for
 -- symbolic execution.  This can fail if an invalid solver configuration is