diff --git a/crucible-mir-comp/src/Mir/Compositional/Builder.hs b/crucible-mir-comp/src/Mir/Compositional/Builder.hs
index d55f48b024..cd3ab2ec70 100644
--- a/crucible-mir-comp/src/Mir/Compositional/Builder.hs
+++ b/crucible-mir-comp/src/Mir/Compositional/Builder.hs
@@ -714,6 +714,8 @@ regToSetup bak p eval shp rv = go shp rv
         alloc <- refToAlloc bak p mutbl ty' tpr startRef len
         let offsetSv idx sv = if idx == 0 then sv else MS.SetupElem () sv idx
         return $ offsetSv idx $ MS.SetupVar alloc
+    go (FnPtrShape _ _ _) _ =
+        error "Function pointers not currently supported in overrides"
 
     goFields :: forall ctx. Assignment FieldShape ctx -> Assignment (RegValue' sym) ctx ->
         BuilderT sym t (OverrideSim p sym MIR rtp args ret) [MS.SetupValue MIR]
diff --git a/crucible-mir-comp/src/Mir/Compositional/Clobber.hs b/crucible-mir-comp/src/Mir/Compositional/Clobber.hs
index 2686c4a25d..458d09daac 100644
--- a/crucible-mir-comp/src/Mir/Compositional/Clobber.hs
+++ b/crucible-mir-comp/src/Mir/Compositional/Clobber.hs
@@ -59,6 +59,8 @@ clobberSymbolic sym loc nameStr shp rv = go shp rv
         ", but got Any wrapping " ++ show tpr
       where shpTpr = StructRepr $ fmapFC fieldShapeType flds
     go (TransparentShape _ shp) rv = go shp rv
+    go (FnPtrShape _ _ _) _rv =
+        error "Function pointers not currently supported in overrides"
     go shp _rv = error $ "clobberSymbolic: " ++ show (shapeType shp) ++ " NYI"
 
     goField :: forall tp. FieldShape tp -> RegValue' sym tp ->
@@ -105,6 +107,8 @@ clobberImmutSymbolic sym loc nameStr shp rv = go shp rv
     -- Since this ref is in immutable memory, whatever behavior we're
     -- approximating with this clobber can't possibly modify it.
     go (RefShape _ _ _tpr) rv = return rv
+    go (FnPtrShape _ _ _) _rv =
+        error "Function pointers not currently supported in overrides"
 
     goField :: forall tp. FieldShape tp -> RegValue' sym tp ->
         OverrideSim (p sym) sym MIR rtp args ret (RegValue' sym tp)
@@ -133,6 +137,8 @@ freshSymbolic sym loc nameStr shp = go shp
         return expr
     go (ArrayShape (M.TyArray _ len) _ shp) =
         MirVector_Vector <$> V.replicateM len (go shp)
+    go (FnPtrShape _ _ _) =
+        error "Function pointers not currently supported in overrides"
     go shp = error $ "freshSymbolic: " ++ show (shapeType shp) ++ " NYI"
 
 
diff --git a/crucible-mir-comp/src/Mir/Compositional/Convert.hs b/crucible-mir-comp/src/Mir/Compositional/Convert.hs
index 3b9cbe24a3..157639bf39 100644
--- a/crucible-mir-comp/src/Mir/Compositional/Convert.hs
+++ b/crucible-mir-comp/src/Mir/Compositional/Convert.hs
@@ -49,7 +49,8 @@ import qualified Verifier.SAW.Simulator.What4.ReturnTrip as SAW (baseSCType)
 
 import Mir.Intrinsics
 import qualified Mir.Mir as M
-import Mir.TransTy (tyToRepr, canInitialize, isUnsized, reprTransparentFieldTy)
+import Mir.TransTy ( tyListToCtx, tyToRepr, tyToReprCont, canInitialize
+                   , isUnsized, reprTransparentFieldTy )
 
 
 -- | TypeShape is used to classify MIR `Ty`s and their corresponding
@@ -75,6 +76,11 @@ data TypeShape (tp :: CrucibleType) where
     -- a TypeShape.  None of our operations need to recurse inside pointers,
     -- and also this saves us from some infinite recursion.
     RefShape :: M.Ty -> M.Ty -> TypeRepr tp -> TypeShape (MirReferenceType tp)
+    -- | Note that 'FnPtrShape' contains only 'TypeRepr's for the argument and
+    -- result types, not 'TypeShape's, as none of our operations need to recurse
+    -- inside them.
+    FnPtrShape :: M.Ty -> CtxRepr args -> TypeRepr ret
+               -> TypeShape (FunctionHandleType args ret)
 
 -- | The TypeShape of a struct field, which might have a MaybeType wrapper to
 -- allow for partial initialization.
@@ -108,6 +114,7 @@ tyToShape col ty = go ty
             Nothing -> error $ "tyToShape: bad adt: " ++ show ty
         M.TyRef ty' mutbl -> goRef ty ty' mutbl
         M.TyRawPtr ty' mutbl -> goRef ty ty' mutbl
+        M.TyFnPtr sig -> goFnPtr ty sig
         _ -> error $ "tyToShape: " ++ show ty ++ " NYI"
 
     goPrim :: M.Ty -> Some TypeShape
@@ -139,10 +146,19 @@ tyToShape col ty = go ty
         False -> Some $ OptField shp
 
     goRef :: M.Ty -> M.Ty -> M.Mutability -> Some TypeShape
-    goRef ty (M.TySlice ty') mutbl | Some tpr <- tyToRepr col ty' = Some $
+    goRef ty ty' mutbl
+      | M.TySlice slicedTy <- ty'
+      , Some tpr <- tyToRepr col slicedTy
+      = Some $
+         TupleShape ty [refTy, usizeTy]
+             (Empty
+                :> ReqField (RefShape refTy slicedTy tpr)
+                :> ReqField (PrimShape usizeTy BaseUsizeRepr))
+      | M.TyStr <- ty'
+      = Some $
         TupleShape ty [refTy, usizeTy]
             (Empty
-                :> ReqField (RefShape refTy ty' tpr)
+                :> ReqField (RefShape refTy (M.TyUint M.B8) (BVRepr (knownNat @8)))
                 :> ReqField (PrimShape usizeTy BaseUsizeRepr))
       where
         -- We use a ref (of the same mutability as `ty`) when possible, to
@@ -155,6 +171,12 @@ tyToShape col ty = go ty
         "tyToShape: fat pointer " ++ show ty ++ " NYI"
     goRef ty ty' _ | Some tpr <- tyToRepr col ty' = Some $ RefShape ty ty' tpr
 
+    goFnPtr :: M.Ty -> M.FnSig -> Some TypeShape
+    goFnPtr ty (M.FnSig args ret _abi _spread) =
+        tyListToCtx col args $ \argsr  ->
+        tyToReprCont col ret $ \retr ->
+           Some (FnPtrShape ty argsr retr)
+
 -- | Given a `Ty` and the result of `tyToRepr ty`, produce a `TypeShape` with
 -- the same index `tp`.  Raises an `error` if the `TypeRepr` doesn't match
 -- `tyToRepr ty`.
@@ -177,6 +199,7 @@ shapeType shp = go shp
     go (StructShape _ _ _flds) = AnyRepr
     go (TransparentShape _ shp) = go shp
     go (RefShape _ _ tpr) = MirReferenceRepr tpr
+    go (FnPtrShape _ args ret) = FunctionHandleRepr args ret
 
 fieldShapeType :: FieldShape tp -> TypeRepr tp
 fieldShapeType (ReqField shp) = shapeType shp
@@ -190,6 +213,7 @@ shapeMirTy (ArrayShape ty _ _) = ty
 shapeMirTy (StructShape ty _ _) = ty
 shapeMirTy (TransparentShape ty _) = ty
 shapeMirTy (RefShape ty _ _) = ty
+shapeMirTy (FnPtrShape ty _ _) = ty
 
 fieldShapeMirTy :: FieldShape tp -> M.Ty
 fieldShapeMirTy (ReqField shp) = shapeMirTy shp
@@ -536,7 +560,7 @@ shapeToTerm sc shp = go shp
     go :: forall tp. TypeShape tp -> m SAW.Term
     go (UnitShape _) = liftIO $ SAW.scUnitType sc
     go (PrimShape _ BaseBoolRepr) = liftIO $ SAW.scBoolType sc
-    go (PrimShape _ (BaseBVRepr w)) = liftIO $ SAW.scBitvector sc (natValue w) 
+    go (PrimShape _ (BaseBVRepr w)) = liftIO $ SAW.scBitvector sc (natValue w)
     go (TupleShape _ _ flds) = do
         tys <- toListFC getConst <$> traverseFC (\x -> Const <$> goField x) flds
         liftIO $ SAW.scTupleType sc tys
diff --git a/crucible-mir-comp/src/Mir/Compositional/Override.hs b/crucible-mir-comp/src/Mir/Compositional/Override.hs
index 2936d30e90..0553c28baf 100644
--- a/crucible-mir-comp/src/Mir/Compositional/Override.hs
+++ b/crucible-mir-comp/src/Mir/Compositional/Override.hs
@@ -407,6 +407,8 @@ matchArg sym sc eval allocSpecs md shp rv sv = go shp rv sv
         goRef refTy tpr ref alloc 0
     go (RefShape refTy _ tpr) ref (MS.SetupElem () (MS.SetupVar alloc) idx) =
         goRef refTy tpr ref alloc idx
+    go (FnPtrShape _ _ _) _ _ =
+        error "Function pointers not currently supported in overrides"
     go shp _ sv = error $ "matchArg: type error: bad SetupValue " ++
         show (MS.ppSetupValue sv) ++ " for " ++ show (shapeType shp)
 
@@ -528,6 +530,8 @@ setupToReg sym sc termSub regMap allocMap shp sv = go shp sv
             Nothing -> error $ "setupToReg: type error: bad reference type for " ++ show alloc ++
                 ": got " ++ show (ptr ^. mpType) ++ " but expected " ++ show tpr
         Nothing -> error $ "setupToReg: no definition for " ++ show alloc
+    go (FnPtrShape _ _ _) _ =
+        error "Function pointers not currently supported in overrides"
     go shp sv = error $ "setupToReg: type error: bad SetupValue for " ++ show (shapeType shp) ++
         ": " ++ show (MS.ppSetupValue sv)
 
diff --git a/crux-mir-comp/DESIGN.md b/crux-mir-comp/DESIGN.md
index 86414e3974..195bb60dde 100644
--- a/crux-mir-comp/DESIGN.md
+++ b/crux-mir-comp/DESIGN.md
@@ -19,7 +19,7 @@ fn f(x: (u8, u8)) -> (u8, u8) {
     (x.1, x.0)
 }
 
-#[crux_test]
+#[crux::test]
 fn f_test() {
     let x = <(u8, u8)>::symbolic("x");
     crucible_assume!(x.0 > 0);
@@ -45,7 +45,7 @@ fn f_spec() -> MethodSpec {
     msb.finish()
 }
 
-#[crux_test]
+#[crux::test]
 fn use_f() {
     f_spec().enable();
 
diff --git a/crux-mir-comp/crux-mir-comp.cabal b/crux-mir-comp/crux-mir-comp.cabal
index ce6056da60..199b7c991d 100644
--- a/crux-mir-comp/crux-mir-comp.cabal
+++ b/crux-mir-comp/crux-mir-comp.cabal
@@ -21,6 +21,7 @@ library
   default-language: Haskell2010
   build-depends: base >= 4.9 && < 5,
                  text,
+                 extra,
                  crucible,
                  parameterized-utils >= 1.0.8,
                  containers,
@@ -39,6 +40,7 @@ library
   hs-source-dirs: src
   exposed-modules: Mir.Compositional
                    Mir.Cryptol
+  other-modules:   Mir.Compositional.DefId
 
   ghc-options: -Wall -Wno-name-shadowing
 
@@ -104,6 +106,8 @@ test-suite test
                 config-schema,
                 config-value,
                 bytestring,
+                regex-base,
+                regex-posix,
                 utf8-string
 
   default-language: Haskell2010
diff --git a/crux-mir-comp/src/Mir/Compositional.hs b/crux-mir-comp/src/Mir/Compositional.hs
index 774c8c7220..ad7ef253d3 100644
--- a/crux-mir-comp/src/Mir/Compositional.hs
+++ b/crux-mir-comp/src/Mir/Compositional.hs
@@ -12,7 +12,6 @@ where
 import Data.Parameterized.Context (pattern Empty, pattern (:>))
 import Data.Parameterized.NatRepr
 import Data.Text (Text)
-import qualified Data.Text as Text
 
 import Lang.Crucible.Backend
 import Lang.Crucible.CFG.Core
@@ -28,6 +27,7 @@ import Mir.Intrinsics
 
 import Mir.Compositional.Builder (builderNew)
 import Mir.Compositional.Clobber (clobberGlobalsOverride)
+import Mir.Compositional.DefId (hasInstPrefix)
 
 
 compositionalOverrides ::
@@ -40,7 +40,7 @@ compositionalOverrides ::
     Maybe (OverrideSim (p sym) sym MIR rtp a r ())
 compositionalOverrides _symOnline cs name cfg
 
-  | (normDefId "crucible::method_spec::raw::builder_new" <> "::_inst") `Text.isPrefixOf` name
+  | hasInstPrefix ["crucible", "method_spec", "raw", "builder_new"] explodedName
   , Empty <- cfgArgTypes cfg
   , MethodSpecBuilderRepr <- cfgReturnType cfg
   = Just $ bindFnHandle (cfgHandle cfg) $ UseOverride $
@@ -48,7 +48,7 @@ compositionalOverrides _symOnline cs name cfg
         msb <- builderNew cs (textId name)
         return $ MethodSpecBuilder msb
 
-  | (normDefId "crucible::method_spec::raw::builder_add_arg" <> "::_inst") `Text.isPrefixOf` name
+  | hasInstPrefix ["crucible", "method_spec", "raw", "builder_add_arg"] explodedName
   , Empty :> MethodSpecBuilderRepr :> MirReferenceRepr _tpr <- cfgArgTypes cfg
   , MethodSpecBuilderRepr <- cfgReturnType cfg
   = Just $ bindFnHandle (cfgHandle cfg) $ UseOverride $
@@ -58,7 +58,7 @@ compositionalOverrides _symOnline cs name cfg
         msb' <- msbAddArg tpr argRef msb
         return $ MethodSpecBuilder msb'
 
-  | (normDefId "crucible::method_spec::raw::builder_set_return" <> "::_inst") `Text.isPrefixOf` name
+  | hasInstPrefix ["crucible", "method_spec", "raw", "builder_set_return"] explodedName
   , Empty :> MethodSpecBuilderRepr :> MirReferenceRepr _tpr <- cfgArgTypes cfg
   , MethodSpecBuilderRepr <- cfgReturnType cfg
   = Just $ bindFnHandle (cfgHandle cfg) $ UseOverride $
@@ -68,7 +68,7 @@ compositionalOverrides _symOnline cs name cfg
         msb' <- msbSetReturn tpr argRef msb
         return $ MethodSpecBuilder msb'
 
-  | normDefId "crucible::method_spec::raw::builder_gather_assumes" == name
+  | ["crucible", "method_spec", "raw", "builder_gather_assumes"] == explodedName
   , Empty :> MethodSpecBuilderRepr <- cfgArgTypes cfg
   , MethodSpecBuilderRepr <- cfgReturnType cfg
   = Just $ bindFnHandle (cfgHandle cfg) $ UseOverride $
@@ -77,7 +77,7 @@ compositionalOverrides _symOnline cs name cfg
         msb' <- msbGatherAssumes msb
         return $ MethodSpecBuilder msb'
 
-  | normDefId "crucible::method_spec::raw::builder_gather_asserts" == name
+  | ["crucible", "method_spec", "raw", "builder_gather_asserts"] == explodedName
   , Empty :> MethodSpecBuilderRepr <- cfgArgTypes cfg
   , MethodSpecBuilderRepr <- cfgReturnType cfg
   = Just $ bindFnHandle (cfgHandle cfg) $ UseOverride $
@@ -86,7 +86,7 @@ compositionalOverrides _symOnline cs name cfg
         msb' <- msbGatherAsserts msb
         return $ MethodSpecBuilder msb'
 
-  | normDefId "crucible::method_spec::raw::builder_finish" == name
+  | ["crucible", "method_spec", "raw", "builder_finish"] == explodedName
   , Empty :> MethodSpecBuilderRepr <- cfgArgTypes cfg
   , MethodSpecRepr <- cfgReturnType cfg
   = Just $ bindFnHandle (cfgHandle cfg) $ UseOverride $
@@ -95,7 +95,7 @@ compositionalOverrides _symOnline cs name cfg
         msbFinish msb
 
 
-  | normDefId "crucible::method_spec::raw::clobber_globals" == name
+  | ["crucible", "method_spec", "raw", "clobber_globals"] == explodedName
   , Empty <- cfgArgTypes cfg
   , UnitRepr <- cfgReturnType cfg
   = Just $ bindFnHandle (cfgHandle cfg) $ UseOverride $
@@ -103,7 +103,7 @@ compositionalOverrides _symOnline cs name cfg
         clobberGlobalsOverride cs
 
 
-  | normDefId "crucible::method_spec::raw::spec_pretty_print" == name
+  | ["crucible", "method_spec", "raw", "spec_pretty_print"] == explodedName
   , Empty :> MethodSpecRepr <- cfgArgTypes cfg
   , MirSliceRepr (BVRepr w) <- cfgReturnType cfg
   , Just Refl <- testEquality w (knownNat @8)
@@ -112,7 +112,7 @@ compositionalOverrides _symOnline cs name cfg
         RegMap (Empty :> RegEntry _tpr (MethodSpec ms _)) <- getOverrideArgs
         msPrettyPrint ms
 
-  | normDefId "crucible::method_spec::raw::spec_enable" == name
+  | ["crucible", "method_spec", "raw", "spec_enable"] == explodedName
   , Empty :> MethodSpecRepr <- cfgArgTypes cfg
   , UnitRepr <- cfgReturnType cfg
   = Just $ bindFnHandle (cfgHandle cfg) $ UseOverride $
@@ -122,4 +122,5 @@ compositionalOverrides _symOnline cs name cfg
 
 
   | otherwise = Nothing
-
+  where
+    explodedName = textIdKey name
diff --git a/crux-mir-comp/src/Mir/Compositional/DefId.hs b/crux-mir-comp/src/Mir/Compositional/DefId.hs
new file mode 100644
index 0000000000..36a7334238
--- /dev/null
+++ b/crux-mir-comp/src/Mir/Compositional/DefId.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE OverloadedStrings #-}
+module Mir.Compositional.DefId
+  ( hasInstPrefix
+  ) where
+
+import Data.List.Extra (unsnoc)
+import qualified Data.Text as Text
+import Data.Text (Text)
+
+import Mir.DefId
+
+-- | Check if @edid@ has the same path as @pfxInit@, plus a final path
+-- component that begins with the name @_inst@.
+hasInstPrefix :: [Text] -> ExplodedDefId -> Bool
+hasInstPrefix pfxInit edid =
+  case unsnoc edid of
+    Nothing -> False
+    Just (edidInit, edidLast) ->
+      pfxInit == edidInit &&
+      "_inst" `Text.isPrefixOf` edidLast
diff --git a/crux-mir-comp/src/Mir/Cryptol.hs b/crux-mir-comp/src/Mir/Cryptol.hs
index ffb3e00747..17bc207a59 100644
--- a/crux-mir-comp/src/Mir/Cryptol.hs
+++ b/crux-mir-comp/src/Mir/Cryptol.hs
@@ -62,6 +62,7 @@ import qualified Verifier.SAW.Recognizer as SAW (asExtCns)
 import qualified Verifier.SAW.TypedTerm as SAW
 
 import Mir.Compositional.Convert
+import Mir.Compositional.DefId (hasInstPrefix)
 
 
 cryptolOverrides ::
@@ -74,7 +75,7 @@ cryptolOverrides ::
     Maybe (OverrideSim (p sym) sym MIR rtp a r ())
 cryptolOverrides _symOnline cs name cfg
 
-  | (normDefId "crucible::cryptol::load" <> "::_inst") `Text.isPrefixOf` name
+  | hasInstPrefix ["crucible", "cryptol", "load"] explodedName
   , Empty
       :> MirSliceRepr (BVRepr (testEquality (knownNat @8) -> Just Refl))
       :> MirSliceRepr (BVRepr (testEquality (knownNat @8) -> Just Refl))
@@ -90,7 +91,7 @@ cryptolOverrides _symOnline cs name cfg
         RegMap (Empty :> RegEntry _tpr modulePathStr :> RegEntry _tpr' nameStr) <- getOverrideArgs
         cryptolLoad (cs ^. collection) sig (cfgReturnType cfg) modulePathStr nameStr
 
-  | (normDefId "crucible::cryptol::override_" <> "::_inst") `Text.isPrefixOf` name
+  | hasInstPrefix ["crucible", "cryptol", "override_"] explodedName
   , Empty
       :> UnitRepr
       :> MirSliceRepr (BVRepr (testEquality (knownNat @8) -> Just Refl))
@@ -114,7 +115,7 @@ cryptolOverrides _symOnline cs name cfg
           :> RegEntry _tpr' nameStr) <- getOverrideArgs
         cryptolOverride (cs ^. collection) mh modulePathStr nameStr
 
-  | (normDefId "crucible::cryptol::munge" <> "::_inst") `Text.isPrefixOf` name
+  | hasInstPrefix ["crucible", "cryptol", "munge"] explodedName
   , Empty :> tpr <- cfgArgTypes cfg
   , tpr' <- cfgReturnType cfg
   , Just Refl <- testEquality tpr tpr'
@@ -131,7 +132,8 @@ cryptolOverrides _symOnline cs name cfg
         liftIO $ munge sym shp rv
 
   | otherwise = Nothing
-
+  where
+    explodedName = textIdKey name
 
 cryptolLoad ::
     forall sym p t st fs rtp a r tp .
@@ -333,6 +335,8 @@ munge sym shp rv = do
                 AnyValue tpr <$> goFields flds rvs
             | otherwise = error $  "munge: StructShape AnyValue with NYI TypeRepr " ++ show tpr
         go (TransparentShape _ shp) rv = go shp rv
+        go (FnPtrShape _ _ _) _ =
+            error "Function pointers not currently supported in overrides"
         -- TODO: RefShape
         go shp _ = error $ "munge: " ++ show (shapeType shp) ++ " NYI"
 
diff --git a/crux-mir-comp/test/Test.hs b/crux-mir-comp/test/Test.hs
index d84d870684..93e0b5573c 100644
--- a/crux-mir-comp/test/Test.hs
+++ b/crux-mir-comp/test/Test.hs
@@ -2,6 +2,7 @@
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE ImplicitParams #-}
 {-# Language OverloadedStrings #-}
+{-# Language ScopedTypeVariables #-}
 {-# OPTIONS_GHC -Wall -fno-warn-unused-top-binds #-}
 
 import qualified Data.ByteString as BS
@@ -24,6 +25,8 @@ import           Test.Tasty.HUnit (Assertion, testCaseSteps, assertBool, assertF
 import           Test.Tasty.Golden (findByExtension)
 import           Test.Tasty.Golden.Advanced (goldenTest)
 import           Test.Tasty.ExpectedFailure (expectFailBecause)
+import           Text.Regex.Base ( makeRegex, matchM )
+import           Text.Regex.Posix.ByteString.Lazy ( Regex )
 
 import qualified Mir.Language as Mir
 
@@ -117,7 +120,7 @@ cruxOracleTest dir name step = do
   step ("Oracle output: " ++ orOut)
 
   let rustFile = dir </> name <.> "rs"
-  
+
   cruxOut <- withSystemTempFile name $ \tempName h -> do
     runCrux rustFile h RcmConcrete
     hClose h
@@ -137,8 +140,9 @@ symbTest dir =
      return $
        testGroup "Output testing"
          [ doGoldenTest (takeBaseName rustFile) goodFile outFile $
-           withFile outFile WriteMode $ \h ->
-           runCrux rustFile h RcmSymbolic
+           do withFile outFile WriteMode $ \h ->
+                runCrux rustFile h RcmSymbolic
+              sanitizeGoldenOutputFile outFile
          | rustFile <- rustFiles
          -- Skip hidden files, such as editor swap files
          , not $ "." `isPrefixOf` takeFileName rustFile
@@ -181,6 +185,40 @@ doGoldenTest rustFile goodFile outFile act = goldenTest (takeBaseName rustFile)
         goodFile ++ " contains:\n" ++ BS8.toString out)
     (\out -> BS.writeFile goodFile out)
 
+-- | Sanitize the golden output in a file.
+sanitizeGoldenOutputFile :: FilePath -> IO ()
+sanitizeGoldenOutputFile file = do
+  out <- BS.readFile file
+  BS.writeFile file $ sanitizeGoldenTestOutput out
+
+-- | Replace occurrences of crate disambiguators (which are highly sensitive to
+-- the contents of crates' source code) with more stable output to reduce churn
+-- in the golden tests.
+sanitizeGoldenTestOutput :: BS.ByteString -> BS.ByteString
+sanitizeGoldenTestOutput = go
+  where
+    go :: BS.ByteString -> BS.ByteString
+    go out
+      | Just (before, _matched :: BS.ByteString, after, [preDisamb])
+          <- matchM disambRE out
+      = before <> preDisamb <> "<DISAMB>::" <> go after
+      | otherwise
+      = out
+
+    disambRE :: Regex
+    disambRE = makeRegex disambBS
+
+    -- A disambiguator looks something like foo/a1b4j89a, i.e., an alphanumeric
+    -- string that starts with an alphabetic character, followed by a forward
+    -- slash, followed by eight alphanumeric characters. To reduce the rate of
+    -- false positives, we also match two trailing colons, which would be
+    -- present when printing out a full DefId (e.g., foo/a1b4j89a::Bar::Baz).
+    disambBS :: BS.ByteString
+    disambBS = "([A-Za-z_]" <> alphaNum <> "*/)" <> mconcat (replicate 8 alphaNum) <> "::"
+
+    alphaNum :: BS.ByteString
+    alphaNum = "[A-Za-z0-9_]"
+
 main :: IO ()
 main = defaultMain =<< suite
 
@@ -189,7 +227,7 @@ suite = do
   let ?debug = 0 :: Int
   let ?assertFalseOnError = True
   let ?printCrucible = False
-  trees <- sequence 
+  trees <- sequence
            [ testGroup "crux concrete" <$> sequence [ testDir cruxOracleTest "test/conc_eval/" ]
            , testGroup "crux symbolic" <$> sequence [ symbTest "test/symb_eval" ]
            , testGroup "crux coverage" <$> sequence [ coverageTests "test/coverage" ]
diff --git a/crux-mir-comp/test/symb_eval/comp/alias_array_bad.good b/crux-mir-comp/test/symb_eval/comp/alias_array_bad.good
index 8f21a5ca50..c65ed7d995 100644
--- a/crux-mir-comp/test/symb_eval/comp/alias_array_bad.good
+++ b/crux-mir-comp/test/symb_eval/comp/alias_array_bad.good
@@ -1,18 +1,18 @@
-test alias_array_bad/3a1fbbbh::f_test[0]: ok
-test alias_array_bad/3a1fbbbh::use_f[0]: FAILED
+test alias_array_bad/<DISAMB>::f_test[0]: ok
+test alias_array_bad/<DISAMB>::use_f[0]: FAILED
 
 failures:
 
----- alias_array_bad/3a1fbbbh::use_f[0] counterexamples ----
+---- alias_array_bad/<DISAMB>::use_f[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   test/symb_eval/comp/alias_array_bad.rs:45:14: 45:16: error: in alias_array_bad/3a1fbbbh::use_f[0]
+[Crux]   test/symb_eval/comp/alias_array_bad.rs:45:14: 45:16: error: in alias_array_bad/<DISAMB>::use_f[0]
 [Crux]   references AllocIndex 0 and AllocIndex 1 must not overlap
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/alias_array_bad.rs:46:5: 46:38: error: in alias_array_bad/3a1fbbbh::use_f[0]
+[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/alias_array_bad.rs:46:5: 46:37: error: in alias_array_bad/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/alias_array_bad.rs:46:5:
 [Crux]   	0 < b[0].get()
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/alias_array_bad.rs:47:5: 47:39: error: in alias_array_bad/3a1fbbbh::use_f[0]
+[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/alias_array_bad.rs:47:5: 47:38: error: in alias_array_bad/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/alias_array_bad.rs:47:5:
 [Crux]   	b[0].get() < 10
 
diff --git a/crux-mir-comp/test/symb_eval/comp/alias_array_bad.rs b/crux-mir-comp/test/symb_eval/comp/alias_array_bad.rs
index da23bdcaf4..7ca679ec8c 100644
--- a/crux-mir-comp/test/symb_eval/comp/alias_array_bad.rs
+++ b/crux-mir-comp/test/symb_eval/comp/alias_array_bad.rs
@@ -8,7 +8,7 @@ fn f(x: &Cell<u8>, y: &[Cell<u8>; 2]) {
     x.swap(&y[0]);
 }
 
-#[crux_test]
+#[crux::test]
 fn f_test() {
     clobber_globals();
     let x = Cell::new(u8::symbolic("x"));
@@ -36,7 +36,7 @@ fn f_spec() -> MethodSpec {
     msb.finish()
 }
 
-#[crux_test]
+#[crux::test]
 fn use_f() {
     f_spec().enable();
 
diff --git a/crux-mir-comp/test/symb_eval/comp/alias_array_bad2.good b/crux-mir-comp/test/symb_eval/comp/alias_array_bad2.good
index 174eaca698..313b675559 100644
--- a/crux-mir-comp/test/symb_eval/comp/alias_array_bad2.good
+++ b/crux-mir-comp/test/symb_eval/comp/alias_array_bad2.good
@@ -1,14 +1,14 @@
-test alias_array_bad2/3a1fbbbh::f_test[0]: ok
-test alias_array_bad2/3a1fbbbh::use_f[0]: FAILED
+test alias_array_bad2/<DISAMB>::f_test[0]: ok
+test alias_array_bad2/<DISAMB>::use_f[0]: FAILED
 
 failures:
 
----- alias_array_bad2/3a1fbbbh::use_f[0] counterexamples ----
+---- alias_array_bad2/<DISAMB>::use_f[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   test/symb_eval/comp/alias_array_bad2.rs:45:14: 45:16: error: in alias_array_bad2/3a1fbbbh::use_f[0]
+[Crux]   test/symb_eval/comp/alias_array_bad2.rs:45:14: 45:16: error: in alias_array_bad2/<DISAMB>::use_f[0]
 [Crux]   references AllocIndex 0 and AllocIndex 1 must not overlap
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/alias_array_bad2.rs:47:5: 47:39: error: in alias_array_bad2/3a1fbbbh::use_f[0]
+[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/alias_array_bad2.rs:47:5: 47:38: error: in alias_array_bad2/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/alias_array_bad2.rs:47:5:
 [Crux]   	b[0].get() < 10
 
diff --git a/crux-mir-comp/test/symb_eval/comp/alias_array_bad2.rs b/crux-mir-comp/test/symb_eval/comp/alias_array_bad2.rs
index bb0f79af58..605ee1caae 100644
--- a/crux-mir-comp/test/symb_eval/comp/alias_array_bad2.rs
+++ b/crux-mir-comp/test/symb_eval/comp/alias_array_bad2.rs
@@ -8,7 +8,7 @@ fn f(x: &Cell<u8>, y: &[Cell<u8>; 2]) {
     x.swap(&y[0]);
 }
 
-#[crux_test]
+#[crux::test]
 fn f_test() {
     clobber_globals();
     let x = Cell::new(u8::symbolic("x"));
@@ -36,7 +36,7 @@ fn f_spec() -> MethodSpec {
     msb.finish()
 }
 
-#[crux_test]
+#[crux::test]
 fn use_f() {
     f_spec().enable();
 
diff --git a/crux-mir-comp/test/symb_eval/comp/alias_array_ok.good b/crux-mir-comp/test/symb_eval/comp/alias_array_ok.good
index b7b511b522..bfe8c997e2 100644
--- a/crux-mir-comp/test/symb_eval/comp/alias_array_ok.good
+++ b/crux-mir-comp/test/symb_eval/comp/alias_array_ok.good
@@ -1,11 +1,11 @@
-test alias_array_ok/3a1fbbbh::f_test[0]: ok
-test alias_array_ok/3a1fbbbh::use_f[0]: FAILED
+test alias_array_ok/<DISAMB>::f_test[0]: ok
+test alias_array_ok/<DISAMB>::use_f[0]: FAILED
 
 failures:
 
----- alias_array_ok/3a1fbbbh::use_f[0] counterexamples ----
+---- alias_array_ok/<DISAMB>::use_f[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/alias_array_ok.rs:48:5: 48:39: error: in alias_array_ok/3a1fbbbh::use_f[0]
+[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/alias_array_ok.rs:48:5: 48:38: error: in alias_array_ok/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/alias_array_ok.rs:48:5:
 [Crux]   	b[0].get() < 10
 
diff --git a/crux-mir-comp/test/symb_eval/comp/alias_array_ok.rs b/crux-mir-comp/test/symb_eval/comp/alias_array_ok.rs
index 9b13abf078..d13cabad31 100644
--- a/crux-mir-comp/test/symb_eval/comp/alias_array_ok.rs
+++ b/crux-mir-comp/test/symb_eval/comp/alias_array_ok.rs
@@ -8,7 +8,7 @@ fn f(x: &Cell<u8>, y: &[Cell<u8>; 2]) {
     x.swap(&y[0]);
 }
 
-#[crux_test]
+#[crux::test]
 fn f_test() {
     clobber_globals();
     let x = Cell::new(u8::symbolic("x"));
@@ -36,7 +36,7 @@ fn f_spec() -> MethodSpec {
     msb.finish()
 }
 
-#[crux_test]
+#[crux::test]
 fn use_f() {
     f_spec().enable();
 
diff --git a/crux-mir-comp/test/symb_eval/comp/alias_bad.good b/crux-mir-comp/test/symb_eval/comp/alias_bad.good
index c573524a28..d66b6d234f 100644
--- a/crux-mir-comp/test/symb_eval/comp/alias_bad.good
+++ b/crux-mir-comp/test/symb_eval/comp/alias_bad.good
@@ -1,18 +1,18 @@
-test alias_bad/3a1fbbbh::f_test[0]: ok
-test alias_bad/3a1fbbbh::use_f[0]: FAILED
+test alias_bad/<DISAMB>::f_test[0]: ok
+test alias_bad/<DISAMB>::use_f[0]: FAILED
 
 failures:
 
----- alias_bad/3a1fbbbh::use_f[0] counterexamples ----
+---- alias_bad/<DISAMB>::use_f[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   test/symb_eval/comp/alias_bad.rs:45:11: 45:13: error: in alias_bad/3a1fbbbh::use_f[0]
+[Crux]   test/symb_eval/comp/alias_bad.rs:45:11: 45:13: error: in alias_bad/<DISAMB>::use_f[0]
 [Crux]   references AllocIndex 0 and AllocIndex 1 must not overlap
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/alias_bad.rs:46:5: 46:35: error: in alias_bad/3a1fbbbh::use_f[0]
+[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/alias_bad.rs:46:5: 46:34: error: in alias_bad/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/alias_bad.rs:46:5:
 [Crux]   	0 < b.get()
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/alias_bad.rs:47:5: 47:36: error: in alias_bad/3a1fbbbh::use_f[0]
+[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/alias_bad.rs:47:5: 47:35: error: in alias_bad/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/alias_bad.rs:47:5:
 [Crux]   	b.get() < 10
 
diff --git a/crux-mir-comp/test/symb_eval/comp/alias_bad.rs b/crux-mir-comp/test/symb_eval/comp/alias_bad.rs
index 749cc4c169..d486b3a9fd 100644
--- a/crux-mir-comp/test/symb_eval/comp/alias_bad.rs
+++ b/crux-mir-comp/test/symb_eval/comp/alias_bad.rs
@@ -8,7 +8,7 @@ fn f(x: &Cell<u8>, y: &Cell<u8>) {
     x.swap(y);
 }
 
-#[crux_test]
+#[crux::test]
 fn f_test() {
     clobber_globals();
     let x = Cell::new(u8::symbolic("x"));
@@ -36,7 +36,7 @@ fn f_spec() -> MethodSpec {
     msb.finish()
 }
 
-#[crux_test]
+#[crux::test]
 fn use_f() {
     f_spec().enable();
 
diff --git a/crux-mir-comp/test/symb_eval/comp/alias_ok.good b/crux-mir-comp/test/symb_eval/comp/alias_ok.good
index bbb9fcc0ab..3db9b9ca3d 100644
--- a/crux-mir-comp/test/symb_eval/comp/alias_ok.good
+++ b/crux-mir-comp/test/symb_eval/comp/alias_ok.good
@@ -1,11 +1,11 @@
-test alias_ok/3a1fbbbh::f_test[0]: ok
-test alias_ok/3a1fbbbh::use_f[0]: FAILED
+test alias_ok/<DISAMB>::f_test[0]: ok
+test alias_ok/<DISAMB>::use_f[0]: FAILED
 
 failures:
 
----- alias_ok/3a1fbbbh::use_f[0] counterexamples ----
+---- alias_ok/<DISAMB>::use_f[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/alias_ok.rs:49:5: 49:36: error: in alias_ok/3a1fbbbh::use_f[0]
+[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/alias_ok.rs:49:5: 49:35: error: in alias_ok/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/alias_ok.rs:49:5:
 [Crux]   	b.get() < 10
 
diff --git a/crux-mir-comp/test/symb_eval/comp/alias_ok.rs b/crux-mir-comp/test/symb_eval/comp/alias_ok.rs
index 986909124b..ba2a3d5d89 100644
--- a/crux-mir-comp/test/symb_eval/comp/alias_ok.rs
+++ b/crux-mir-comp/test/symb_eval/comp/alias_ok.rs
@@ -8,7 +8,7 @@ fn f(x: &Cell<u8>, y: &Cell<u8>) {
     x.swap(y);
 }
 
-#[crux_test]
+#[crux::test]
 fn f_test() {
     clobber_globals();
     let x = Cell::new(u8::symbolic("x"));
@@ -36,7 +36,7 @@ fn f_spec() -> MethodSpec {
     msb.finish()
 }
 
-#[crux_test]
+#[crux::test]
 fn use_f() {
     f_spec().enable();
 
diff --git a/crux-mir-comp/test/symb_eval/comp/clobber_globals.good b/crux-mir-comp/test/symb_eval/comp/clobber_globals.good
index 213876df76..07ec5680d6 100644
--- a/crux-mir-comp/test/symb_eval/comp/clobber_globals.good
+++ b/crux-mir-comp/test/symb_eval/comp/clobber_globals.good
@@ -1,17 +1,17 @@
-test clobber_globals/3a1fbbbh::f_test[0]: FAILED
-test clobber_globals/3a1fbbbh::use_f[0]: FAILED
+test clobber_globals/<DISAMB>::f_test[0]: FAILED
+test clobber_globals/<DISAMB>::use_f[0]: FAILED
 
 failures:
 
----- clobber_globals/3a1fbbbh::f_test[0] counterexamples ----
+---- clobber_globals/<DISAMB>::f_test[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   test/symb_eval/comp/clobber_globals.rs:16:9: 16:70: error: in clobber_globals/3a1fbbbh::f_test[0]
+[Crux]   test/symb_eval/comp/clobber_globals.rs:16:9: 16:70: error: in clobber_globals/<DISAMB>::f_test[0]
 [Crux]   MIR assertion at test/symb_eval/comp/clobber_globals.rs:15:5:
 [Crux]   	expected failure; ATOMIC was clobbered by clobber_globals()
 
----- clobber_globals/3a1fbbbh::use_f[0] counterexamples ----
+---- clobber_globals/<DISAMB>::use_f[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   test/symb_eval/comp/clobber_globals.rs:38:9: 38:61: error: in clobber_globals/3a1fbbbh::use_f[0]
+[Crux]   test/symb_eval/comp/clobber_globals.rs:38:9: 38:61: error: in clobber_globals/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/clobber_globals.rs:37:5:
 [Crux]   	expected failure; ATOMIC was clobbered by f's spec
 
diff --git a/crux-mir-comp/test/symb_eval/comp/clobber_globals.rs b/crux-mir-comp/test/symb_eval/comp/clobber_globals.rs
index 21e0b9db94..afbb8b1ce8 100644
--- a/crux-mir-comp/test/symb_eval/comp/clobber_globals.rs
+++ b/crux-mir-comp/test/symb_eval/comp/clobber_globals.rs
@@ -8,7 +8,7 @@ static ATOMIC: AtomicUsize = AtomicUsize::new(123);
 fn f() {
 }
 
-#[crux_test]
+#[crux::test]
 fn f_test() {
     clobber_globals();
     f();
@@ -27,7 +27,7 @@ fn f_spec() -> MethodSpec {
     msb.finish()
 }
 
-#[crux_test]
+#[crux::test]
 fn use_f() {
     f_spec().enable();
 
diff --git a/crux-mir-comp/test/symb_eval/comp/munge_struct.good b/crux-mir-comp/test/symb_eval/comp/munge_struct.good
index 6ee4dd3406..870b0f63de 100644
--- a/crux-mir-comp/test/symb_eval/comp/munge_struct.good
+++ b/crux-mir-comp/test/symb_eval/comp/munge_struct.good
@@ -1,3 +1,3 @@
-test munge_struct/3a1fbbbh::munge_struct_equiv_test[0]: ok
+test munge_struct/<DISAMB>::munge_struct_equiv_test[0]: ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir-comp/test/symb_eval/comp/munge_struct.rs b/crux-mir-comp/test/symb_eval/comp/munge_struct.rs
index 25cdd7c669..9a02b7e33b 100644
--- a/crux-mir-comp/test/symb_eval/comp/munge_struct.rs
+++ b/crux-mir-comp/test/symb_eval/comp/munge_struct.rs
@@ -12,7 +12,7 @@ fn reflect(p: Point) -> Point {
     Point{x: p.y, y: p.x}
 }
 
-#[crux_test]
+#[crux::test]
 fn munge_struct_equiv_test() {
     let (x, y) = <(u32, u32)>::symbolic("p");
     let p2 = reflect(munge(Point{x, y}));
diff --git a/crux-mir-comp/test/symb_eval/comp/override_test_indep.good b/crux-mir-comp/test/symb_eval/comp/override_test_indep.good
index bb6bb52b4d..733894aff2 100644
--- a/crux-mir-comp/test/symb_eval/comp/override_test_indep.good
+++ b/crux-mir-comp/test/symb_eval/comp/override_test_indep.good
@@ -1,13 +1,13 @@
-test override_test_indep/3a1fbbbh::f_test[0]: ok
-test override_test_indep/3a1fbbbh::use_f1[0]: ok
-test override_test_indep/3a1fbbbh::use_f2[0]: FAILED
-test override_test_indep/3a1fbbbh::use_f3[0]: ok
+test override_test_indep/<DISAMB>::f_test[0]: ok
+test override_test_indep/<DISAMB>::use_f1[0]: ok
+test override_test_indep/<DISAMB>::use_f2[0]: FAILED
+test override_test_indep/<DISAMB>::use_f3[0]: ok
 
 failures:
 
----- override_test_indep/3a1fbbbh::use_f2[0] counterexamples ----
+---- override_test_indep/<DISAMB>::use_f2[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/override_test_indep.rs:57:5: 57:30: error: in override_test_indep/3a1fbbbh::use_f2[0]
+[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/override_test_indep.rs:57:5: 57:29: error: in override_test_indep/<DISAMB>::use_f2[0]
 [Crux]   MIR assertion at test/symb_eval/comp/override_test_indep.rs:57:5:
 [Crux]   	d < 10
 
diff --git a/crux-mir-comp/test/symb_eval/comp/override_test_indep.rs b/crux-mir-comp/test/symb_eval/comp/override_test_indep.rs
index 302478d36e..d623acc513 100644
--- a/crux-mir-comp/test/symb_eval/comp/override_test_indep.rs
+++ b/crux-mir-comp/test/symb_eval/comp/override_test_indep.rs
@@ -8,7 +8,7 @@ fn f(x: (u8, u8)) -> (u8, u8) {
     (x.1, x.0)
 }
 
-#[crux_test]
+#[crux::test]
 fn f_test() {
     clobber_globals();
     let x = <(u8, u8)>::symbolic("x");
@@ -33,7 +33,7 @@ fn f_spec() -> MethodSpec {
     msb.finish()
 }
 
-#[crux_test]
+#[crux::test]
 fn use_f1() {
     let a = u8::symbolic("a");
     let b = u8::symbolic("b");
@@ -44,7 +44,7 @@ fn use_f1() {
     crucible_assert!(d < 10);
 }
 
-#[crux_test]
+#[crux::test]
 fn use_f2() {
     f_spec().enable();
 
@@ -57,7 +57,7 @@ fn use_f2() {
     crucible_assert!(d < 10);
 }
 
-#[crux_test]
+#[crux::test]
 fn use_f3() {
     let a = u8::symbolic("a");
     let b = u8::symbolic("b");
diff --git a/crux-mir-comp/test/symb_eval/comp/ptr_offset.good b/crux-mir-comp/test/symb_eval/comp/ptr_offset.good
index 8a7e2f9843..3a27415cea 100644
--- a/crux-mir-comp/test/symb_eval/comp/ptr_offset.good
+++ b/crux-mir-comp/test/symb_eval/comp/ptr_offset.good
@@ -1,11 +1,11 @@
-test ptr_offset/3a1fbbbh::f_test[0]: ok
-test ptr_offset/3a1fbbbh::use_f[0]: FAILED
+test ptr_offset/<DISAMB>::f_test[0]: ok
+test ptr_offset/<DISAMB>::use_f[0]: FAILED
 
 failures:
 
----- ptr_offset/3a1fbbbh::use_f[0] counterexamples ----
+---- ptr_offset/<DISAMB>::use_f[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/ptr_offset.rs:64:5: 64:31: error: in ptr_offset/3a1fbbbh::use_f[0]
+[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/ptr_offset.rs:64:5: 64:30: error: in ptr_offset/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/ptr_offset.rs:64:5:
 [Crux]   	b2 < 10
 
diff --git a/crux-mir-comp/test/symb_eval/comp/ptr_offset.rs b/crux-mir-comp/test/symb_eval/comp/ptr_offset.rs
index c60dfffa69..7456ba7648 100644
--- a/crux-mir-comp/test/symb_eval/comp/ptr_offset.rs
+++ b/crux-mir-comp/test/symb_eval/comp/ptr_offset.rs
@@ -7,7 +7,7 @@ fn f(ptr: *mut u8) {
     unsafe { ptr::swap(ptr, ptr.add(1)) };
 }
 
-#[crux_test]
+#[crux::test]
 fn f_test() {
     clobber_globals();
     let mut x = <[u8; 2]>::symbolic("x");
@@ -47,7 +47,7 @@ fn f_spec() -> MethodSpec {
 //   - PointsTos: ptr0 -> [y0, y1]
 //   - Postconditions: y1 > 0
 
-#[crux_test]
+#[crux::test]
 fn use_f() {
     f_spec().enable();
 
diff --git a/crux-mir-comp/test/symb_eval/comp/ptr_offset_rev.good b/crux-mir-comp/test/symb_eval/comp/ptr_offset_rev.good
index 3894efcc99..5a3984d46b 100644
--- a/crux-mir-comp/test/symb_eval/comp/ptr_offset_rev.good
+++ b/crux-mir-comp/test/symb_eval/comp/ptr_offset_rev.good
@@ -1,11 +1,11 @@
-test ptr_offset_rev/3a1fbbbh::f_test[0]: ok
-test ptr_offset_rev/3a1fbbbh::use_f[0]: FAILED
+test ptr_offset_rev/<DISAMB>::f_test[0]: ok
+test ptr_offset_rev/<DISAMB>::use_f[0]: FAILED
 
 failures:
 
----- ptr_offset_rev/3a1fbbbh::use_f[0] counterexamples ----
+---- ptr_offset_rev/<DISAMB>::use_f[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/ptr_offset_rev.rs:64:5: 64:31: error: in ptr_offset_rev/3a1fbbbh::use_f[0]
+[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/ptr_offset_rev.rs:64:5: 64:30: error: in ptr_offset_rev/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/ptr_offset_rev.rs:64:5:
 [Crux]   	b2 < 10
 
diff --git a/crux-mir-comp/test/symb_eval/comp/ptr_offset_rev.rs b/crux-mir-comp/test/symb_eval/comp/ptr_offset_rev.rs
index 3561415bc9..b8d0bde467 100644
--- a/crux-mir-comp/test/symb_eval/comp/ptr_offset_rev.rs
+++ b/crux-mir-comp/test/symb_eval/comp/ptr_offset_rev.rs
@@ -7,7 +7,7 @@ fn f(ptr: *mut u8) {
     unsafe { ptr::swap(ptr.sub(1), ptr) };
 }
 
-#[crux_test]
+#[crux::test]
 fn f_test() {
     clobber_globals();
     let mut x = <[u8; 2]>::symbolic("x");
@@ -47,7 +47,7 @@ fn f_spec() -> MethodSpec {
 //   - PointsTos: ptr0 -> [y0, y1]
 //   - Postconditions: y1 > 0
 
-#[crux_test]
+#[crux::test]
 fn use_f() {
     f_spec().enable();
 
diff --git a/crux-mir-comp/test/symb_eval/comp/spec_array.good b/crux-mir-comp/test/symb_eval/comp/spec_array.good
index 33689a3c34..3fd9f86c9e 100644
--- a/crux-mir-comp/test/symb_eval/comp/spec_array.good
+++ b/crux-mir-comp/test/symb_eval/comp/spec_array.good
@@ -1,11 +1,11 @@
-test spec_array/3a1fbbbh::f_test[0]: ok
-test spec_array/3a1fbbbh::use_f[0]: FAILED
+test spec_array/<DISAMB>::f_test[0]: ok
+test spec_array/<DISAMB>::use_f[0]: FAILED
 
 failures:
 
----- spec_array/3a1fbbbh::use_f[0] counterexamples ----
+---- spec_array/<DISAMB>::use_f[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/spec_array.rs:43:5: 43:30: error: in spec_array/3a1fbbbh::use_f[0]
+[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/spec_array.rs:43:5: 43:29: error: in spec_array/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/spec_array.rs:43:5:
 [Crux]   	d < 10
 
diff --git a/crux-mir-comp/test/symb_eval/comp/spec_array.rs b/crux-mir-comp/test/symb_eval/comp/spec_array.rs
index 3fd6ee987e..4626129cd1 100644
--- a/crux-mir-comp/test/symb_eval/comp/spec_array.rs
+++ b/crux-mir-comp/test/symb_eval/comp/spec_array.rs
@@ -6,7 +6,7 @@ fn f(x: [u8; 2]) -> [u8; 2] {
     [x[1], x[0]]
 }
 
-#[crux_test]
+#[crux::test]
 fn f_test() {
     clobber_globals();
     let x = <[u8; 2]>::symbolic("x");
@@ -31,7 +31,7 @@ fn f_spec() -> MethodSpec {
     msb.finish()
 }
 
-#[crux_test]
+#[crux::test]
 fn use_f() {
     f_spec().enable();
 
diff --git a/crux-mir-comp/test/symb_eval/comp/spec_box.good b/crux-mir-comp/test/symb_eval/comp/spec_box.good
index eea72e7978..19b07c9734 100644
--- a/crux-mir-comp/test/symb_eval/comp/spec_box.good
+++ b/crux-mir-comp/test/symb_eval/comp/spec_box.good
@@ -1,11 +1,11 @@
-test spec_box/3a1fbbbh::f_test[0]: ok
-test spec_box/3a1fbbbh::use_f[0]: FAILED
+test spec_box/<DISAMB>::f_test[0]: ok
+test spec_box/<DISAMB>::use_f[0]: FAILED
 
 failures:
 
----- spec_box/3a1fbbbh::use_f[0] counterexamples ----
+---- spec_box/<DISAMB>::use_f[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/spec_box.rs:58:5: 58:30: error: in spec_box/3a1fbbbh::use_f[0]
+[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/spec_box.rs:58:5: 58:29: error: in spec_box/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/spec_box.rs:58:5:
 [Crux]   	d < 10
 
diff --git a/crux-mir-comp/test/symb_eval/comp/spec_box.rs b/crux-mir-comp/test/symb_eval/comp/spec_box.rs
index f0c338ccb0..e53a09252b 100644
--- a/crux-mir-comp/test/symb_eval/comp/spec_box.rs
+++ b/crux-mir-comp/test/symb_eval/comp/spec_box.rs
@@ -6,7 +6,7 @@ fn f(x: &[u8; 2]) -> Box<[u8; 2]> {
     Box::new([x[1], x[0]])
 }
 
-#[crux_test]
+#[crux::test]
 fn f_test() {
     clobber_globals();
     let x = <[u8; 2]>::symbolic("x");
@@ -45,7 +45,7 @@ fn f_spec() -> MethodSpec {
 //   - PointsTos: ptr1 -> (y0, y1)
 //   - Postconditions: y1 > 0
 
-#[crux_test]
+#[crux::test]
 fn use_f() {
     f_spec().enable();
 
diff --git a/crux-mir-comp/test/symb_eval/comp/spec_immut_cell.good b/crux-mir-comp/test/symb_eval/comp/spec_immut_cell.good
index af2bacfa47..44dfed7da9 100644
--- a/crux-mir-comp/test/symb_eval/comp/spec_immut_cell.good
+++ b/crux-mir-comp/test/symb_eval/comp/spec_immut_cell.good
@@ -1,11 +1,11 @@
-test spec_immut_cell/3a1fbbbh::f_test[0]: ok
-test spec_immut_cell/3a1fbbbh::use_f[0]: FAILED
+test spec_immut_cell/<DISAMB>::f_test[0]: ok
+test spec_immut_cell/<DISAMB>::use_f[0]: FAILED
 
 failures:
 
----- spec_immut_cell/3a1fbbbh::use_f[0] counterexamples ----
+---- spec_immut_cell/<DISAMB>::use_f[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/spec_immut_cell.rs:68:5: 68:36: error: in spec_immut_cell/3a1fbbbh::use_f[0]
+[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/spec_immut_cell.rs:68:5: 68:35: error: in spec_immut_cell/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/spec_immut_cell.rs:68:5:
 [Crux]   	d.get() < 10
 
diff --git a/crux-mir-comp/test/symb_eval/comp/spec_immut_cell.rs b/crux-mir-comp/test/symb_eval/comp/spec_immut_cell.rs
index 4f4157e7ab..7bf4d23ce4 100644
--- a/crux-mir-comp/test/symb_eval/comp/spec_immut_cell.rs
+++ b/crux-mir-comp/test/symb_eval/comp/spec_immut_cell.rs
@@ -7,7 +7,7 @@ fn f(x: &[Cell<u8>; 2]) {
     x[0].swap(&x[1])
 }
 
-#[crux_test]
+#[crux::test]
 fn f_test() {
     clobber_globals();
     let mut x = [
@@ -53,7 +53,7 @@ fn f_spec() -> MethodSpec {
 //   - PointsTos: ptr0 -> [y0, y1]
 //   - Postconditions: y1 > 0
 
-#[crux_test]
+#[crux::test]
 fn use_f() {
     f_spec().enable();
 
diff --git a/crux-mir-comp/test/symb_eval/comp/spec_mut.good b/crux-mir-comp/test/symb_eval/comp/spec_mut.good
index 8f84e8592d..e73f68a744 100644
--- a/crux-mir-comp/test/symb_eval/comp/spec_mut.good
+++ b/crux-mir-comp/test/symb_eval/comp/spec_mut.good
@@ -1,11 +1,11 @@
-test spec_mut/3a1fbbbh::f_test[0]: ok
-test spec_mut/3a1fbbbh::use_f[0]: FAILED
+test spec_mut/<DISAMB>::f_test[0]: ok
+test spec_mut/<DISAMB>::use_f[0]: FAILED
 
 failures:
 
----- spec_mut/3a1fbbbh::use_f[0] counterexamples ----
+---- spec_mut/<DISAMB>::use_f[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/spec_mut.rs:61:5: 61:30: error: in spec_mut/3a1fbbbh::use_f[0]
+[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/spec_mut.rs:61:5: 61:29: error: in spec_mut/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/spec_mut.rs:61:5:
 [Crux]   	d < 10
 
diff --git a/crux-mir-comp/test/symb_eval/comp/spec_mut.rs b/crux-mir-comp/test/symb_eval/comp/spec_mut.rs
index ef3d577093..69adf97ff5 100644
--- a/crux-mir-comp/test/symb_eval/comp/spec_mut.rs
+++ b/crux-mir-comp/test/symb_eval/comp/spec_mut.rs
@@ -6,7 +6,7 @@ fn f(x: &mut [u8; 2]) {
     x.swap(0, 1);
 }
 
-#[crux_test]
+#[crux::test]
 fn f_test() {
     clobber_globals();
     let mut x = <[u8; 2]>::symbolic("x");
@@ -46,7 +46,7 @@ fn f_spec() -> MethodSpec {
 //   - PointsTos: ptr0 -> [y0, y1]
 //   - Postconditions: y1 > 0
 
-#[crux_test]
+#[crux::test]
 fn use_f() {
     f_spec().enable();
 
diff --git a/crux-mir-comp/test/symb_eval/comp/spec_mut_slice.good b/crux-mir-comp/test/symb_eval/comp/spec_mut_slice.good
index 79a5647efd..5aab238aff 100644
--- a/crux-mir-comp/test/symb_eval/comp/spec_mut_slice.good
+++ b/crux-mir-comp/test/symb_eval/comp/spec_mut_slice.good
@@ -1,11 +1,11 @@
-test spec_mut_slice/3a1fbbbh::f_test[0]: ok
-test spec_mut_slice/3a1fbbbh::use_f[0]: FAILED
+test spec_mut_slice/<DISAMB>::f_test[0]: ok
+test spec_mut_slice/<DISAMB>::use_f[0]: FAILED
 
 failures:
 
----- spec_mut_slice/3a1fbbbh::use_f[0] counterexamples ----
+---- spec_mut_slice/<DISAMB>::use_f[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/spec_mut_slice.rs:48:5: 48:30: error: in spec_mut_slice/3a1fbbbh::use_f[0]
+[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/spec_mut_slice.rs:48:5: 48:29: error: in spec_mut_slice/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/spec_mut_slice.rs:48:5:
 [Crux]   	d < 10
 
diff --git a/crux-mir-comp/test/symb_eval/comp/spec_mut_slice.rs b/crux-mir-comp/test/symb_eval/comp/spec_mut_slice.rs
index c1395db905..66901b051a 100644
--- a/crux-mir-comp/test/symb_eval/comp/spec_mut_slice.rs
+++ b/crux-mir-comp/test/symb_eval/comp/spec_mut_slice.rs
@@ -6,7 +6,7 @@ fn f(x: &mut [u8]) {
     x.swap(0, 1);
 }
 
-#[crux_test]
+#[crux::test]
 fn f_test() {
     clobber_globals();
     let mut x = <[u8; 2]>::symbolic("x");
@@ -33,7 +33,7 @@ fn f_spec() -> MethodSpec {
     msb.finish()
 }
 
-#[crux_test]
+#[crux::test]
 fn use_f() {
     f_spec().enable();
 
diff --git a/crux-mir-comp/test/symb_eval/comp/spec_struct.good b/crux-mir-comp/test/symb_eval/comp/spec_struct.good
index 75595f1177..682281b49a 100644
--- a/crux-mir-comp/test/symb_eval/comp/spec_struct.good
+++ b/crux-mir-comp/test/symb_eval/comp/spec_struct.good
@@ -1,11 +1,11 @@
-test spec_struct/3a1fbbbh::f_test[0]: ok
-test spec_struct/3a1fbbbh::use_f[0]: FAILED
+test spec_struct/<DISAMB>::f_test[0]: ok
+test spec_struct/<DISAMB>::use_f[0]: FAILED
 
 failures:
 
----- spec_struct/3a1fbbbh::use_f[0] counterexamples ----
+---- spec_struct/<DISAMB>::use_f[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/spec_struct.rs:51:5: 51:30: error: in spec_struct/3a1fbbbh::use_f[0]
+[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/spec_struct.rs:51:5: 51:29: error: in spec_struct/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/spec_struct.rs:51:5:
 [Crux]   	d < 10
 
diff --git a/crux-mir-comp/test/symb_eval/comp/spec_struct.rs b/crux-mir-comp/test/symb_eval/comp/spec_struct.rs
index dcbb154604..eb87d7e5ca 100644
--- a/crux-mir-comp/test/symb_eval/comp/spec_struct.rs
+++ b/crux-mir-comp/test/symb_eval/comp/spec_struct.rs
@@ -14,7 +14,7 @@ fn f(x: S) -> S {
     S(x.1, x.0)
 }
 
-#[crux_test]
+#[crux::test]
 fn f_test() {
     clobber_globals();
     let x = <S>::symbolic("x");
@@ -39,7 +39,7 @@ fn f_spec() -> MethodSpec {
     msb.finish()
 }
 
-#[crux_test]
+#[crux::test]
 fn use_f() {
     f_spec().enable();
 
diff --git a/crux-mir-comp/test/symb_eval/comp/spec_tuple.good b/crux-mir-comp/test/symb_eval/comp/spec_tuple.good
index 7f14b0cbe9..c163f06063 100644
--- a/crux-mir-comp/test/symb_eval/comp/spec_tuple.good
+++ b/crux-mir-comp/test/symb_eval/comp/spec_tuple.good
@@ -1,11 +1,11 @@
-test spec_tuple/3a1fbbbh::f_test[0]: ok
-test spec_tuple/3a1fbbbh::use_f[0]: FAILED
+test spec_tuple/<DISAMB>::f_test[0]: ok
+test spec_tuple/<DISAMB>::use_f[0]: FAILED
 
 failures:
 
----- spec_tuple/3a1fbbbh::use_f[0] counterexamples ----
+---- spec_tuple/<DISAMB>::use_f[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/spec_tuple.rs:55:5: 55:30: error: in spec_tuple/3a1fbbbh::use_f[0]
+[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/spec_tuple.rs:55:5: 55:29: error: in spec_tuple/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/spec_tuple.rs:55:5:
 [Crux]   	d < 10
 
diff --git a/crux-mir-comp/test/symb_eval/comp/spec_tuple.rs b/crux-mir-comp/test/symb_eval/comp/spec_tuple.rs
index 78fe283aed..af46c9eb3d 100644
--- a/crux-mir-comp/test/symb_eval/comp/spec_tuple.rs
+++ b/crux-mir-comp/test/symb_eval/comp/spec_tuple.rs
@@ -6,7 +6,7 @@ fn f(x: (u8, u8)) -> (u8, u8) {
     (x.1, x.0)
 }
 
-#[crux_test]
+#[crux::test]
 fn f_test() {
     clobber_globals();
     let x = <(u8, u8)>::symbolic("x");
@@ -43,7 +43,7 @@ fn f_spec() -> MethodSpec {
 //   - PointsTos: none
 //   - Postconditions: y1 > 0
 
-#[crux_test]
+#[crux::test]
 fn use_f() {
     f_spec().enable();
 
diff --git a/crux-mir-comp/test/symb_eval/comp/subst_basic.good b/crux-mir-comp/test/symb_eval/comp/subst_basic.good
index 9cd6d7b455..0e1b14b938 100644
--- a/crux-mir-comp/test/symb_eval/comp/subst_basic.good
+++ b/crux-mir-comp/test/symb_eval/comp/subst_basic.good
@@ -1,3 +1,3 @@
-test subst_basic/3a1fbbbh::use_f[0]: ok
+test subst_basic/<DISAMB>::use_f[0]: ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir-comp/test/symb_eval/comp/subst_basic.rs b/crux-mir-comp/test/symb_eval/comp/subst_basic.rs
index 21bda37143..97553880f6 100644
--- a/crux-mir-comp/test/symb_eval/comp/subst_basic.rs
+++ b/crux-mir-comp/test/symb_eval/comp/subst_basic.rs
@@ -22,7 +22,7 @@ fn f_spec() -> MethodSpec {
     msb.finish()
 }
 
-#[crux_test]
+#[crux::test]
 fn use_f() {
     f_spec().enable();
 
diff --git a/crux-mir-comp/test/symb_eval/comp/subst_multi.good b/crux-mir-comp/test/symb_eval/comp/subst_multi.good
index 7dfa321a33..b337250396 100644
--- a/crux-mir-comp/test/symb_eval/comp/subst_multi.good
+++ b/crux-mir-comp/test/symb_eval/comp/subst_multi.good
@@ -1,3 +1,3 @@
-test subst_multi/3a1fbbbh::use_f[0]: ok
+test subst_multi/<DISAMB>::use_f[0]: ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir-comp/test/symb_eval/comp/subst_multi.rs b/crux-mir-comp/test/symb_eval/comp/subst_multi.rs
index 930ca1c999..2ec108491e 100644
--- a/crux-mir-comp/test/symb_eval/comp/subst_multi.rs
+++ b/crux-mir-comp/test/symb_eval/comp/subst_multi.rs
@@ -24,7 +24,7 @@ fn f_spec() -> MethodSpec {
     msb.finish()
 }
 
-#[crux_test]
+#[crux::test]
 fn use_f() {
     f_spec().enable();
 
diff --git a/crux-mir-comp/test/symb_eval/comp/subst_multi_rev.good b/crux-mir-comp/test/symb_eval/comp/subst_multi_rev.good
index 47171d146e..d36af39023 100644
--- a/crux-mir-comp/test/symb_eval/comp/subst_multi_rev.good
+++ b/crux-mir-comp/test/symb_eval/comp/subst_multi_rev.good
@@ -1,3 +1,3 @@
-test subst_multi_rev/3a1fbbbh::use_f[0]: ok
+test subst_multi_rev/<DISAMB>::use_f[0]: ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir-comp/test/symb_eval/comp/subst_multi_rev.rs b/crux-mir-comp/test/symb_eval/comp/subst_multi_rev.rs
index 84b0b42798..577ebda780 100644
--- a/crux-mir-comp/test/symb_eval/comp/subst_multi_rev.rs
+++ b/crux-mir-comp/test/symb_eval/comp/subst_multi_rev.rs
@@ -26,7 +26,7 @@ fn f_spec() -> MethodSpec {
     msb.finish()
 }
 
-#[crux_test]
+#[crux::test]
 fn use_f() {
     f_spec().enable();
 
diff --git a/crux-mir-comp/test/symb_eval/comp/subst_output.good b/crux-mir-comp/test/symb_eval/comp/subst_output.good
index 320b522db7..3489730df5 100644
--- a/crux-mir-comp/test/symb_eval/comp/subst_output.good
+++ b/crux-mir-comp/test/symb_eval/comp/subst_output.good
@@ -1,10 +1,10 @@
-test subst_output/3a1fbbbh::use_f[0]: FAILED
+test subst_output/<DISAMB>::use_f[0]: FAILED
 
 failures:
 
----- subst_output/3a1fbbbh::use_f[0] counterexamples ----
+---- subst_output/<DISAMB>::use_f[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   ./lib/crucible/lib.rs:37:41: 37:58 !test/symb_eval/comp/subst_output.rs:32:5: 32:31: error: in subst_output/3a1fbbbh::use_f[0]
+[Crux]   ./lib/crucible/lib.rs:38:41: 38:58 !test/symb_eval/comp/subst_output.rs:32:5: 32:30: error: in subst_output/<DISAMB>::use_f[0]
 [Crux]   MIR assertion at test/symb_eval/comp/subst_output.rs:32:5:
 [Crux]   	b0 == a
 
diff --git a/crux-mir-comp/test/symb_eval/comp/subst_output.rs b/crux-mir-comp/test/symb_eval/comp/subst_output.rs
index 78ffedc307..b6210a0f0f 100644
--- a/crux-mir-comp/test/symb_eval/comp/subst_output.rs
+++ b/crux-mir-comp/test/symb_eval/comp/subst_output.rs
@@ -22,7 +22,7 @@ fn f_spec() -> MethodSpec {
     msb.finish()
 }
 
-#[crux_test]
+#[crux::test]
 fn use_f() {
     f_spec().enable();
 
diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_add.good b/crux-mir-comp/test/symb_eval/cryptol/basic_add.good
index d2dfb839b9..072515d5f6 100644
--- a/crux-mir-comp/test/symb_eval/cryptol/basic_add.good
+++ b/crux-mir-comp/test/symb_eval/cryptol/basic_add.good
@@ -1,3 +1,3 @@
-test basic_add/3a1fbbbh::test[0]: ok
+test basic_add/<DISAMB>::test[0]: ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_add.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_add.rs
index d0fcec41fd..c1a3ff4a7c 100644
--- a/crux-mir-comp/test/symb_eval/cryptol/basic_add.rs
+++ b/crux-mir-comp/test/symb_eval/cryptol/basic_add.rs
@@ -7,7 +7,7 @@ cryptol! {
     fn add_byte(x: u8, y: u8) -> u8 = "addByte";
 }
 
-#[crux_test]
+#[crux::test]
 fn test() {
     let x = u8::symbolic("x");
     let y = u8::symbolic("y");
diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_add_bits.good b/crux-mir-comp/test/symb_eval/cryptol/basic_add_bits.good
index a351fcb99a..e5bb33f209 100644
--- a/crux-mir-comp/test/symb_eval/cryptol/basic_add_bits.good
+++ b/crux-mir-comp/test/symb_eval/cryptol/basic_add_bits.good
@@ -1,3 +1,3 @@
-test basic_add_bits/3a1fbbbh::test[0]: ok
+test basic_add_bits/<DISAMB>::test[0]: ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_add_bits.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_add_bits.rs
index 963d8460d4..c062fc814b 100644
--- a/crux-mir-comp/test/symb_eval/cryptol/basic_add_bits.rs
+++ b/crux-mir-comp/test/symb_eval/cryptol/basic_add_bits.rs
@@ -27,7 +27,7 @@ fn from_bits(x: [bool; 8]) -> u8 {
     ((x[7] as u8) << 0)
 }
 
-#[crux_test]
+#[crux::test]
 fn test() {
     let x = u8::symbolic("x");
     let y = u8::symbolic("y");
diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_array_arg.good b/crux-mir-comp/test/symb_eval/cryptol/basic_array_arg.good
index 4ab83dea7e..122fd6cd1d 100644
--- a/crux-mir-comp/test/symb_eval/cryptol/basic_array_arg.good
+++ b/crux-mir-comp/test/symb_eval/cryptol/basic_array_arg.good
@@ -1,3 +1,3 @@
-test basic_array_arg/3a1fbbbh::test[0]: ok
+test basic_array_arg/<DISAMB>::test[0]: ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_array_arg.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_array_arg.rs
index 01f19918f8..d076077413 100644
--- a/crux-mir-comp/test/symb_eval/cryptol/basic_array_arg.rs
+++ b/crux-mir-comp/test/symb_eval/cryptol/basic_array_arg.rs
@@ -3,7 +3,7 @@ use crucible::*;
 
 const PATH: &str = "test::symb_eval::cryptol::basic";
 
-#[crux_test]
+#[crux::test]
 fn test() {
     let x = u8::symbolic("x");
     let y = u8::symbolic("y");
diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_array_ret.good b/crux-mir-comp/test/symb_eval/cryptol/basic_array_ret.good
index bad259e0e4..33eef78c97 100644
--- a/crux-mir-comp/test/symb_eval/cryptol/basic_array_ret.good
+++ b/crux-mir-comp/test/symb_eval/cryptol/basic_array_ret.good
@@ -1,3 +1,3 @@
-test basic_array_ret/3a1fbbbh::test[0]: ok
+test basic_array_ret/<DISAMB>::test[0]: ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_array_ret.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_array_ret.rs
index 1fd68d3717..02de59d9f1 100644
--- a/crux-mir-comp/test/symb_eval/cryptol/basic_array_ret.rs
+++ b/crux-mir-comp/test/symb_eval/cryptol/basic_array_ret.rs
@@ -3,7 +3,7 @@ use crucible::*;
 
 const PATH: &str = "test::symb_eval::cryptol::basic";
 
-#[crux_test]
+#[crux::test]
 fn test() {
     let x = u8::symbolic("x");
     let y = u8::symbolic("y");
diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_array_size.good b/crux-mir-comp/test/symb_eval/cryptol/basic_err_array_size.good
index f163eda5e2..49936ae292 100644
--- a/crux-mir-comp/test/symb_eval/cryptol/basic_err_array_size.good
+++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_array_size.good
@@ -1,10 +1,10 @@
-test basic_err_array_size/3a1fbbbh::test[0]: FAILED
+test basic_err_array_size/<DISAMB>::test[0]: FAILED
 
 failures:
 
----- basic_err_array_size/3a1fbbbh::test[0] counterexamples ----
+---- basic_err_array_size/<DISAMB>::test[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   test/symb_eval/cryptol/basic_err_array_size.rs:8:52: 8:62: error: in basic_err_array_size/3a1fbbbh::test[0]
+[Crux]   test/symb_eval/cryptol/basic_err_array_size.rs:8:52: 8:62: error: in basic_err_array_size/<DISAMB>::test[0]
 [Crux]   error loading "arrayArg": type mismatch in argument 0: Cryptol type [2][8] does not match Rust type u8: array length 2 does not match 3
 
 [Crux] Overall status: Invalid.
diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_array_size.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_err_array_size.rs
index 0dcdcd4cdc..aad14b77bc 100644
--- a/crux-mir-comp/test/symb_eval/cryptol/basic_err_array_size.rs
+++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_array_size.rs
@@ -3,7 +3,7 @@ use crucible::*;
 
 const PATH: &str = "test::symb_eval::cryptol::basic";
 
-#[crux_test]
+#[crux::test]
 fn test() {
     let f: fn([u8; 3]) -> u8 = cryptol::load(PATH, "arrayArg");
 }
diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_bv_size.good b/crux-mir-comp/test/symb_eval/cryptol/basic_err_bv_size.good
index 8493dc696f..65f18f7de1 100644
--- a/crux-mir-comp/test/symb_eval/cryptol/basic_err_bv_size.good
+++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_bv_size.good
@@ -1,10 +1,10 @@
-test basic_err_bv_size/3a1fbbbh::test[0]: FAILED
+test basic_err_bv_size/<DISAMB>::test[0]: FAILED
 
 failures:
 
----- basic_err_bv_size/3a1fbbbh::test[0] counterexamples ----
+---- basic_err_bv_size/<DISAMB>::test[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   test/symb_eval/cryptol/basic_err_bv_size.rs:8:52: 8:61: error: in basic_err_bv_size/3a1fbbbh::test[0]
+[Crux]   test/symb_eval/cryptol/basic_err_bv_size.rs:8:52: 8:61: error: in basic_err_bv_size/<DISAMB>::test[0]
 [Crux]   error loading "addByte": type mismatch in argument 1: Cryptol type [8] does not match Rust type u16: bitvector width 8 does not match 16
 
 [Crux] Overall status: Invalid.
diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_bv_size.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_err_bv_size.rs
index a4f8e4e71a..852644250b 100644
--- a/crux-mir-comp/test/symb_eval/cryptol/basic_err_bv_size.rs
+++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_bv_size.rs
@@ -3,7 +3,7 @@ use crucible::*;
 
 const PATH: &str = "test::symb_eval::cryptol::basic";
 
-#[crux_test]
+#[crux::test]
 fn test() {
     let f: fn(u8, u16) -> u8 = cryptol::load(PATH, "addByte");
 }
diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_fewer_args.good b/crux-mir-comp/test/symb_eval/cryptol/basic_err_fewer_args.good
index 163b4550e2..49f64aafc6 100644
--- a/crux-mir-comp/test/symb_eval/cryptol/basic_err_fewer_args.good
+++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_fewer_args.good
@@ -1,10 +1,10 @@
-test basic_err_fewer_args/3a1fbbbh::test[0]: FAILED
+test basic_err_fewer_args/<DISAMB>::test[0]: FAILED
 
 failures:
 
----- basic_err_fewer_args/3a1fbbbh::test[0] counterexamples ----
+---- basic_err_fewer_args/<DISAMB>::test[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   test/symb_eval/cryptol/basic_err_fewer_args.rs:8:55: 8:64: error: in basic_err_fewer_args/3a1fbbbh::test[0]
+[Crux]   test/symb_eval/cryptol/basic_err_fewer_args.rs:8:55: 8:64: error: in basic_err_fewer_args/<DISAMB>::test[0]
 [Crux]   error loading "addByte": not enough arguments: Cryptol function signature [8] -> [8] -> [8] has 2 arguments, but Rust signature (u8, u8, u8) -> u8 [RustAbi]  requires 3
 
 [Crux] Overall status: Invalid.
diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_fewer_args.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_err_fewer_args.rs
index 175d2e1c91..c2d5154a26 100644
--- a/crux-mir-comp/test/symb_eval/cryptol/basic_err_fewer_args.rs
+++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_fewer_args.rs
@@ -3,7 +3,7 @@ use crucible::*;
 
 const PATH: &str = "test::symb_eval::cryptol::basic";
 
-#[crux_test]
+#[crux::test]
 fn test() {
     let f: fn(u8, u8, u8) -> u8 = cryptol::load(PATH, "addByte");
 }
diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_mismatch.good b/crux-mir-comp/test/symb_eval/cryptol/basic_err_mismatch.good
index 2889838baa..c0e2e15011 100644
--- a/crux-mir-comp/test/symb_eval/cryptol/basic_err_mismatch.good
+++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_mismatch.good
@@ -1,10 +1,10 @@
-test basic_err_mismatch/3a1fbbbh::test[0]: FAILED
+test basic_err_mismatch/<DISAMB>::test[0]: FAILED
 
 failures:
 
----- basic_err_mismatch/3a1fbbbh::test[0] counterexamples ----
+---- basic_err_mismatch/<DISAMB>::test[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   test/symb_eval/cryptol/basic_err_mismatch.rs:8:51: 8:60: error: in basic_err_mismatch/3a1fbbbh::test[0]
+[Crux]   test/symb_eval/cryptol/basic_err_mismatch.rs:8:51: 8:60: error: in basic_err_mismatch/<DISAMB>::test[0]
 [Crux]   error loading "addByte": type mismatch in argument 1: Cryptol type [8] does not match Rust type ()
 
 [Crux] Overall status: Invalid.
diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_mismatch.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_err_mismatch.rs
index 0bc914122a..9dfdeb319e 100644
--- a/crux-mir-comp/test/symb_eval/cryptol/basic_err_mismatch.rs
+++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_mismatch.rs
@@ -3,7 +3,7 @@ use crucible::*;
 
 const PATH: &str = "test::symb_eval::cryptol::basic";
 
-#[crux_test]
+#[crux::test]
 fn test() {
     let f: fn(u8, ()) -> u8 = cryptol::load(PATH, "addByte");
 }
diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_more_args.good b/crux-mir-comp/test/symb_eval/cryptol/basic_err_more_args.good
index 0f0d469dbf..b40202fece 100644
--- a/crux-mir-comp/test/symb_eval/cryptol/basic_err_more_args.good
+++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_more_args.good
@@ -1,10 +1,10 @@
-test basic_err_more_args/3a1fbbbh::test[0]: FAILED
+test basic_err_more_args/<DISAMB>::test[0]: FAILED
 
 failures:
 
----- basic_err_more_args/3a1fbbbh::test[0] counterexamples ----
+---- basic_err_more_args/<DISAMB>::test[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   test/symb_eval/cryptol/basic_err_more_args.rs:8:47: 8:56: error: in basic_err_more_args/3a1fbbbh::test[0]
+[Crux]   test/symb_eval/cryptol/basic_err_more_args.rs:8:47: 8:56: error: in basic_err_more_args/<DISAMB>::test[0]
 [Crux]   error loading "addByte": type mismatch in return value: Cryptol type [8] -> [8] does not match Rust type u8
 
 [Crux] Overall status: Invalid.
diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_more_args.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_err_more_args.rs
index 882daee8dd..86fa2756d2 100644
--- a/crux-mir-comp/test/symb_eval/cryptol/basic_err_more_args.rs
+++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_more_args.rs
@@ -3,7 +3,7 @@ use crucible::*;
 
 const PATH: &str = "test::symb_eval::cryptol::basic";
 
-#[crux_test]
+#[crux::test]
 fn test() {
     let f: fn(u8) -> u8 = cryptol::load(PATH, "addByte");
 }
diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_tuple_size.good b/crux-mir-comp/test/symb_eval/cryptol/basic_err_tuple_size.good
index c78e6f459c..5522696f98 100644
--- a/crux-mir-comp/test/symb_eval/cryptol/basic_err_tuple_size.good
+++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_tuple_size.good
@@ -1,10 +1,10 @@
-test basic_err_tuple_size/3a1fbbbh::test[0]: FAILED
+test basic_err_tuple_size/<DISAMB>::test[0]: FAILED
 
 failures:
 
----- basic_err_tuple_size/3a1fbbbh::test[0] counterexamples ----
+---- basic_err_tuple_size/<DISAMB>::test[0] counterexamples ----
 [Crux] Found counterexample for verification goal
-[Crux]   test/symb_eval/cryptol/basic_err_tuple_size.rs:8:57: 8:67: error: in basic_err_tuple_size/3a1fbbbh::test[0]
+[Crux]   test/symb_eval/cryptol/basic_err_tuple_size.rs:8:57: 8:67: error: in basic_err_tuple_size/<DISAMB>::test[0]
 [Crux]   error loading "tupleArg": type mismatch in argument 0: Cryptol type ([8], [8]) does not match Rust type (u8, u8, u8): tuple size 2 does not match 3
 
 [Crux] Overall status: Invalid.
diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_err_tuple_size.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_err_tuple_size.rs
index 424ac3ca65..947e00edf1 100644
--- a/crux-mir-comp/test/symb_eval/cryptol/basic_err_tuple_size.rs
+++ b/crux-mir-comp/test/symb_eval/cryptol/basic_err_tuple_size.rs
@@ -3,7 +3,7 @@ use crucible::*;
 
 const PATH: &str = "test::symb_eval::cryptol::basic";
 
-#[crux_test]
+#[crux::test]
 fn test() {
     let f: fn((u8, u8, u8)) -> u8 = cryptol::load(PATH, "tupleArg");
 }
diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_arg.good b/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_arg.good
index d307c9e268..2fd7f366ab 100644
--- a/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_arg.good
+++ b/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_arg.good
@@ -1,3 +1,3 @@
-test basic_tuple_arg/3a1fbbbh::test[0]: ok
+test basic_tuple_arg/<DISAMB>::test[0]: ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_arg.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_arg.rs
index 6f791baeba..a478e08192 100644
--- a/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_arg.rs
+++ b/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_arg.rs
@@ -3,7 +3,7 @@ use crucible::*;
 
 const PATH: &str = "test::symb_eval::cryptol::basic";
 
-#[crux_test]
+#[crux::test]
 fn test() {
     let x = u8::symbolic("x");
     let y = u8::symbolic("y");
diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_ret.good b/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_ret.good
index ec91ffdc8d..7e69e6e51f 100644
--- a/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_ret.good
+++ b/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_ret.good
@@ -1,3 +1,3 @@
-test basic_tuple_ret/3a1fbbbh::test[0]: ok
+test basic_tuple_ret/<DISAMB>::test[0]: ok
 
 [Crux] Overall status: Valid.
diff --git a/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_ret.rs b/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_ret.rs
index 059fdaf7a8..01e0a217ed 100644
--- a/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_ret.rs
+++ b/crux-mir-comp/test/symb_eval/cryptol/basic_tuple_ret.rs
@@ -3,7 +3,7 @@ use crucible::*;
 
 const PATH: &str = "test::symb_eval::cryptol::basic";
 
-#[crux_test]
+#[crux::test]
 fn test() {
     let x = u8::symbolic("x");
     let y = u8::symbolic("y");
diff --git a/deps/crucible b/deps/crucible
index 83ff0b1a76..0515e64ab5 160000
--- a/deps/crucible
+++ b/deps/crucible
@@ -1 +1 @@
-Subproject commit 83ff0b1a766742d561242255f191f856c978fde0
+Subproject commit 0515e64ab5c39036c6577e06bbe4272d39de5656
diff --git a/intTests/test_mir_load_module/test.linked-mir.json b/intTests/test_mir_load_module/test.linked-mir.json
index 5f85cd77c2..3e15cb9659 100644
--- a/intTests/test_mir_load_module/test.linked-mir.json
+++ b/intTests/test_mir_load_module/test.linked-mir.json
@@ -1 +1 @@
-{"fns":[{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::i32"}},"pos":"test.rs:1:23: 1:25","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"int","size":4,"val":"42"},"ty":"ty::i32"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"test.rs:1:27: 1:27"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::i32"}]},"name":"test/3a1fbbbh::foo[0]","return_ty":"ty::i32","spread_arg":null}],"adts":[],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/3a1fbbbh::foo[0]","kind":"Item","substs":[]},"name":"test/3a1fbbbh::foo[0]"}],"tys":[{"name":"ty::i32","ty":{"intkind":{"kind":"I32"},"kind":"Int"}}],"roots":["test/3a1fbbbh::foo[0]"]}
\ No newline at end of file
+{"fns":[{"abi":{"kind":"Rust"},"args":[],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::i32"}},"pos":"test.rs:1:23: 1:25","rhs":{"kind":"Use","usevar":{"data":{"rendered":{"kind":"int","size":4,"val":"42"},"ty":"ty::i32"},"kind":"Constant"}}}],"terminator":{"kind":"Return","pos":"test.rs:1:27: 1:27"}},"blockid":"bb0"}],"vars":[{"is_zst":false,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::i32"}]},"name":"test/54f7b4a0::foo","return_ty":"ty::i32","spread_arg":null}],"adts":[],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/54f7b4a0::foo","kind":"Item","substs":[]},"name":"test/54f7b4a0::foo"}],"tys":[{"name":"ty::i32","ty":{"intkind":{"kind":"I32"},"kind":"Int"}}],"roots":["test/54f7b4a0::foo"]}
\ No newline at end of file