diff --git a/deps/crucible b/deps/crucible
index 6fdb562aa0..8f7db760a8 160000
--- a/deps/crucible
+++ b/deps/crucible
@@ -1 +1 @@
-Subproject commit 6fdb562aa0cd915ea45eb3f14bb6af467dd5d00f
+Subproject commit 8f7db760a89915133e6b623ceed05f34f64f3e42
diff --git a/deps/saw-core b/deps/saw-core
index 52d8d43d79..82d1666d13 160000
--- a/deps/saw-core
+++ b/deps/saw-core
@@ -1 +1 @@
-Subproject commit 52d8d43d7913e62c7e3f50a9835de2a7a4da27c9
+Subproject commit 82d1666d139b413f573f2ec86a389c5fd5c310a2
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/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs
index 6412edf0c0..e4e8776397 100644
--- a/src/SAWScript/Crucible/LLVM/Override.hs
+++ b/src/SAWScript/Crucible/LLVM/Override.hs
@@ -683,8 +683,8 @@ refreshTerms sc ss =
   where
     freshenTerm tt =
       case asExtCns (ttTerm tt) of
-        Just ec -> do new <- liftIO (mkTypedTerm sc =<< scFreshGlobal sc (ecName ec) (ecType ec))
-                      return (termId (ttTerm tt), ttTerm new)
+        Just ec -> do new <- liftIO (scFreshGlobal sc (ecName ec) (ecType ec))
+                      return (termId (ttTerm tt), new)
         Nothing -> error "refreshTerms: not a variable"
 
 ------------------------------------------------------------------------
diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
index 1f1b15119c..df154a8cf6 100644
--- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
+++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
@@ -71,7 +71,6 @@ import qualified Data.SBV.Dynamic as SBV (svAsInteger)
 import           SAWScript.Crucible.Common (Sym)
 import           SAWScript.Crucible.Common.MethodSpec (AllocIndex(..), SetupValue(..))
 
-import SAWScript.Prover.Rewrite
 import SAWScript.Crucible.LLVM.MethodSpecIR
 
 --import qualified SAWScript.LLVMBuiltins as LB
@@ -369,7 +368,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