diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs
index eb77483e70..9f271ffb77 100644
--- a/src/SAWScript/Crucible/LLVM/Builtins.hs
+++ b/src/SAWScript/Crucible/LLVM/Builtins.hs
@@ -1044,6 +1044,7 @@ setupLLVMCrucibleContext bic opts lm@(LLVMModule _ llvm_mod mtrans) action = do
                             , _ccBackend = sym
                             , _ccLLVMSimContext = lsimctx
                             , _ccLLVMGlobals = lglobals
+                            , _ccBasicSS = biBasicSS bic
                             }
       )
 
diff --git a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs
index 3d94067db6..e9eb7c59cc 100644
--- a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs
+++ b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs
@@ -64,6 +64,7 @@ import qualified SAWScript.Crucible.Common.Setup.Type as Setup
 
 import qualified SAWScript.Crucible.LLVM.CrucibleLLVM as CL
 
+import           Verifier.SAW.Rewriter (Simpset)
 import           Verifier.SAW.SharedTerm
 import           Verifier.SAW.TypedTerm
 
@@ -211,6 +212,7 @@ data LLVMCrucibleContext arch =
   , _ccBackend         :: Sym
   , _ccLLVMSimContext  :: Crucible.SimContext (Crucible.SAWCruciblePersonality Sym) Sym (CL.LLVM arch)
   , _ccLLVMGlobals     :: Crucible.SymGlobalState Sym
+  , _ccBasicSS         :: Simpset
   }
 
 makeLenses ''LLVMCrucibleContext
diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
index 1f1b15119c..f792ac9ab1 100644
--- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
+++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
@@ -369,7 +369,7 @@ resolveSAWTerm cc tp tm =
           Just (Some w)
             | Just LeqProof <- isPosNat w ->
               do sc <- Crucible.saw_ctx <$> readIORef (W4.sbStateManager sym)
-                 ss <- basic_ss sc
+                 let ss = cc^.ccBasicSS
                  tm' <- rewriteSharedTerm sc ss tm
                  mx <- case getAllExts tm' of
                          [] -> do