diff --git a/crucible-go/src/Lang/Crucible/Go/Overrides.hs b/crucible-go/src/Lang/Crucible/Go/Overrides.hs
index 1574c66b5..50fe307de 100644
--- a/crucible-go/src/Lang/Crucible/Go/Overrides.hs
+++ b/crucible-go/src/Lang/Crucible/Go/Overrides.hs
@@ -106,9 +106,7 @@ do_assert args = C.ovrWithBackend $ \bak -> do
   let sym = backendGetSym bak
   (Empty :> _mgs :> _file :> C.RV b) <- pure args
   loc <- liftIO $ W4.getCurrentProgramLoc sym
-  liftIO $ addDurableAssertion bak (LabeledPred b
-                                    (C.SimError loc $ C.AssertFailureSimError
-                                     "assertion_failure" ""))
+  Crux.doCrucibleAssert "assertion_failure" b (plSourceLoc loc)
   return Ctx.empty
 
 go_overrides :: (IsSymInterface sym, 1 <= w)
diff --git a/crux-llvm/src/Crux/LLVM/Overrides.hs b/crux-llvm/src/Crux/LLVM/Overrides.hs
index f7f65317c..dbbdf188e 100644
--- a/crux-llvm/src/Crux/LLVM/Overrides.hs
+++ b/crux-llvm/src/Crux/LLVM/Overrides.hs
@@ -21,6 +21,7 @@ module Crux.LLVM.Overrides
 
 import qualified Data.ByteString as BS
 import qualified Data.ByteString.Char8 as BS8
+import qualified Data.Text as Text
 import Control.Monad (when)
 import Control.Monad.IO.Class(liftIO)
 import GHC.Exts ( Proxy# )
@@ -481,11 +482,8 @@ do_assert arch mvar bak (Empty :> p :> pFile :> line) =
      l <- case asBV (regValue line) of
             Just (BV.BV l)  -> return (fromInteger l)
             Nothing -> return 0
-     let pos = SourcePos (T.pack file) l 0
-     loc <- liftIO $ getCurrentProgramLoc sym
-     let loc' = loc{ plSourceLoc = pos }
-     let msg = GenericSimError "crucible_assert"
-     liftIO $ addDurableAssertion bak (LabeledPred cond (SimError loc' msg))
+     let loc = SourcePos (Text.pack file) l 0
+     Crux.doCrucibleAssert "crucible_assert" cond loc
 
 do_print_uint32 ::
   (IsSymBackend sym bak) =>
diff --git a/crux-mir/src/Mir/Overrides.hs b/crux-mir/src/Mir/Overrides.hs
index 1a3e3ded3..b36b49de1 100644
--- a/crux-mir/src/Mir/Overrides.hs
+++ b/crux-mir/src/Mir/Overrides.hs
@@ -42,6 +42,7 @@ import What4.Expr.GroundEval (GroundValue, GroundEvalFn(..), GroundArray(..))
 import What4.FunctionName (FunctionName, functionNameFromText)
 import What4.Interface
 import What4.Partial (PartExpr, pattern PE, pattern Unassigned)
+import qualified What4.ProgramLoc as W4
 import What4.Protocol.Online ( checkWithAssumptionsAndModel )
 import What4.SatResult (SatResult(..))
 
@@ -508,9 +509,10 @@ bindFn _symOnline _cs fn cfg =
                                (BV.asUnsigned <$> asBV (unRV lineArg))
                        col <- maybe (fail "not a constant column number") pure $
                               (BV.asUnsigned <$> asBV (unRV colArg))
+                       let loc = W4.SourcePos file (fromIntegral line) (fromIntegral col)
                        let locStr = Text.unpack file <> ":" <> show line <> ":" <> show col
-                       let reason = AssertFailureSimError ("MIR assertion at " <> locStr <> ":\n\t" <> src) ""
-                       liftIO $ assert bak (unRV c) reason
+                       let msg = "MIR assertion at " <> locStr <> ":\n\t" <> src
+                       Crux.doCrucibleAssert msg (unRV c) loc
                        return ()
                , let argTys = (Empty :> BoolRepr :> strrepr :> strrepr :> u32repr :> u32repr)
                  in override ["crucible", "crucible_assume_impl"] argTys UnitRepr $
diff --git a/crux/src/Crux/Overrides.hs b/crux/src/Crux/Overrides.hs
index 71572209d..3f2124a76 100644
--- a/crux/src/Crux/Overrides.hs
+++ b/crux/src/Crux/Overrides.hs
@@ -8,6 +8,7 @@ module Crux.Overrides
   , mkFreshFloat
   , baseFreshOverride
   , baseFreshOverride'
+  , doCrucibleAssert
   ) where
 
 import qualified Data.Parameterized.Context as Ctx
@@ -15,8 +16,10 @@ import qualified Data.Parameterized.Context as Ctx
 import What4.BaseTypes (BaseTypeRepr)
 import qualified What4.Interface as W4
 import qualified What4.InterpretedFloatingPoint as W4
+import qualified What4.ProgramLoc as W4
 
 import qualified Lang.Crucible.Backend as C
+import qualified Lang.Crucible.Simulator.SimError as C
 import qualified Lang.Crucible.Simulator.RegValue as C
 import qualified Lang.Crucible.Types as C
 import qualified Lang.Crucible.Simulator.OverrideSim as C
@@ -88,3 +91,22 @@ baseFreshOverride' nm bty =
   , C.typedOverrideArgs = Ctx.Empty
   , C.typedOverrideRet = C.baseToType bty
   }
+
+-- | Shared implementation of @crucible_assert@ override
+--
+-- Used in Go, LLVM, and MIR frontends.
+doCrucibleAssert ::
+  -- | Assertion failure message
+  String ->
+  -- | Condition to assert
+  W4.Pred sym ->
+  -- | Source position
+  W4.Position ->
+  C.OverrideSim p sym ext r args ret ()
+doCrucibleAssert msg cond pos =
+  C.ovrWithBackend $ \bak ->
+    do let sym = C.backendGetSym bak
+       loc <- liftIO $ W4.getCurrentProgramLoc sym
+       let loc' = loc { W4.plSourceLoc = pos }
+       let reason = C.AssertFailureSimError msg ""
+       liftIO $ C.addDurableAssertion bak (C.LabeledPred cond (C.SimError loc' reason))