From e1c00c2d2680d44138d31294733685c94fb89fe8 Mon Sep 17 00:00:00 2001
From: "Iavor S. Diatchki" <diatchki@galois.com>
Date: Tue, 7 Oct 2025 10:04:25 -0700
Subject: [PATCH 01/19] Add a way do declare that names should be kept opaque
 during LLVM symbolic simulation

Fixes #2674
---
 .../src/SAWCentral/Crucible/LLVM/Builtins.hs  | 33 +++++++++++++++----
 .../Crucible/LLVM/ResolveSetupValue.hs        | 28 ++++++++--------
 .../SAWCentral/Crucible/LLVM/Setup/Value.hs   |  4 ++-
 .../src/SAWCentral/Crucible/LLVM/X86.hs       |  1 +
 saw-core/src/SAWCore/SharedTerm.hs            | 22 +++++++++++++
 saw-script/src/SAWScript/Interpreter.hs       |  7 ++++
 6 files changed, 73 insertions(+), 22 deletions(-)

diff --git a/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs b/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs
index d75765c656..332b7a17e7 100644
--- a/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs
+++ b/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs
@@ -31,6 +31,7 @@ module SAWCentral.Crucible.LLVM.Builtins
     , llvm_return
     , llvm_precond
     , llvm_postcond
+    , llvm_unint
     , llvm_assert
     , llvm_cfg
     , llvm_extract
@@ -169,7 +170,7 @@ import qualified SAWCentral.Crucible.LLVM.CrucibleLLVM as Crucible
 
 -- saw-core
 import SAWCore.FiniteValue (ppFirstOrderValue)
-import SAWCore.Name (ecShortName)
+import SAWCore.Name (ecShortName, nameIndex)
 import SAWCore.SharedTerm
 import SAWCore.Recognizer
 import SAWCore.Term.Pretty (showTerm)
@@ -205,6 +206,7 @@ import qualified SAWCentral.Crucible.Common.Vacuity as Vacuity
 import SAWCentral.Crucible.LLVM.Override
 import SAWCentral.Crucible.LLVM.ResolveSetupValue
 import SAWCentral.Crucible.LLVM.MethodSpecIR
+import SAWCentral.Crucible.LLVM.Setup.Value(ccUninterp)
 import SAWCentral.Panic (panic)
 
 type AssumptionReason = (MS.ConditionMetadata, String)
@@ -580,17 +582,18 @@ withMethodSpec pathSat lm nm setup action =
               -- execute commands of the method spec
               io $ W4.setCurrentProgramLoc sym setupLoc
 
-              methodSpec <-
-                view Setup.csMethodSpec <$>
+              
+              setupState  <-
                 (execStateT
                    (runReaderT (runLLVMCrucibleSetupM setup)
                                (Setup.makeCrucibleSetupRO))
                      st0)
+              let methodSpec = setupState ^. Setup.csMethodSpec
+                  cc1        = setupState ^. Setup.csCrucibleContext
+              io $ checkSpecArgumentTypes cc1 methodSpec
+              io $ checkSpecReturnType cc1 methodSpec
 
-              io $ checkSpecArgumentTypes cc methodSpec
-              io $ checkSpecReturnType cc methodSpec
-
-              action cc methodSpec
+              action cc1 methodSpec
 
 verifyMethodSpec ::
   ( ?lc :: Crucible.TypeContext
@@ -1777,6 +1780,7 @@ setupLLVMCrucibleContext pathSat lm action =
                                      , _ccLLVMSimContext = lsimctx
                                      , _ccLLVMGlobals = lglobals
                                      , _ccBasicSS = basic_ss
+                                     , _ccUninterp = Set.empty
                                      }
           action cc
 
@@ -2006,6 +2010,21 @@ llvm_postcond term =
   do loc <- getW4Position "llvm_postcond"
      Setup.crucible_postcond loc term
 
+llvm_unint :: TypedTerm -> LLVMCrucibleSetupM ()
+llvm_unint term =
+  LLVMCrucibleSetupM $
+    do
+      prePost <- use Setup.csPrePost
+      case prePost of
+        PreState ->
+          case asConstant (ttTerm term) of
+            Nothing -> fail "The argument to `llvm_unint` should be a name."
+            Just n ->
+              do 
+                 Setup.csCrucibleContext . ccUninterp . contains (nameIndex n) .= True
+        PostState -> fail "`llvm_unint` works only int the pre-condition of a specification."
+          
+
 llvm_return ::
   AllLLVM MS.SetupValue ->
   LLVMCrucibleSetupM ()
diff --git a/saw-central/src/SAWCentral/Crucible/LLVM/ResolveSetupValue.hs b/saw-central/src/SAWCentral/Crucible/LLVM/ResolveSetupValue.hs
index bf949bed48..deded8fbaf 100644
--- a/saw-central/src/SAWCentral/Crucible/LLVM/ResolveSetupValue.hs
+++ b/saw-central/src/SAWCentral/Crucible/LLVM/ResolveSetupValue.hs
@@ -46,7 +46,6 @@ import Data.Void (absurd)
 import qualified Data.Dwarf as Dwarf
 import           Data.Map (Map)
 import qualified Data.Map as Map
-import qualified Data.Set as Set
 import           Data.Text (Text)
 import qualified Data.Text as Text
 import qualified Data.Vector as V
@@ -88,7 +87,7 @@ import           SAWCentral.Crucible.Common.MethodSpec (AllocIndex(..), SetupVal
 import           SAWCentral.Crucible.Common.ResolveSetupValue (checkBooleanType)
 
 import SAWCentral.Crucible.LLVM.MethodSpecIR
-import SAWCentral.Crucible.LLVM.Setup.Value (LLVMPtr)
+import SAWCentral.Crucible.LLVM.Setup.Value (LLVMPtr, ccUninterp)
 import qualified SAWCentral.Proof as SP
 
 type LLVMVal = Crucible.LLVMVal Sym
@@ -757,16 +756,16 @@ resolveSAWPred cc tm = do
      st <- sawCoreState sym
      let sc = saw_ctx st
      let ss = cc^.ccBasicSS
+         unint = cc ^. ccUninterp
      (_,tm') <- rewriteSharedTerm sc ss tm
 
      checkBooleanType sc tm'
 
-     mx <- case getAllExts tm' of
+     mx <- if not (isConstFoldTerm unint tm') then pure Nothing else
              -- concretely evaluate if it is a closed term
-             [] -> do modmap <- scGetModuleMap sc
-                      let v = Concrete.evalSharedTerm modmap mempty mempty tm'
-                      pure (Just (Concrete.toBool v))
-             _ -> return Nothing
+             do modmap <- scGetModuleMap sc
+                let v = Concrete.evalSharedTerm modmap mempty mempty tm'
+                pure (Just (Concrete.toBool v))
      case mx of
        Just x  -> return $ W4.backendPred sym x
        Nothing
@@ -775,7 +774,7 @@ resolveSAWPred cc tm = do
               (_,tm'') <- rewriteSharedTerm sc cryptol_ss tm'
               (_,tm''') <- rewriteSharedTerm sc ss tm''
               if all isPreludeName (Map.elems $ getConstantSet tm''') then
-                do (_names, (_mlabels, p)) <- w4Eval sym st sc mempty Set.empty tm'''
+                do (_names, (_mlabels, p)) <- w4Eval sym st sc mempty unint tm'''
                    return p
               else bindSAWTerm sym st W4.BaseBoolRepr tm'
          | otherwise ->
@@ -791,12 +790,13 @@ resolveSAWSymBV cc w tm =
   do let sym = cc^.ccSym
      st <- sawCoreState sym
      let sc = saw_ctx st
-     mx <- case getAllExts tm of
+         unint = cc ^. ccUninterp
+     mx <- if not (isConstFoldTerm unint tm) then pure Nothing else
              -- concretely evaluate if it is a closed term
-             [] -> do modmap <- scGetModuleMap sc
-                      let v = Concrete.evalSharedTerm modmap mempty mempty tm
-                      pure (Just (Prim.unsigned (Concrete.toWord v)))
-             _ -> return Nothing
+             do modmap <- scGetModuleMap sc
+                let v = Concrete.evalSharedTerm modmap mempty mempty tm
+                pure (Just (Prim.unsigned (Concrete.toWord v)))
+            
      case mx of
        Just x  -> W4.bvLit sym w (BV.mkBV w x)
        Nothing
@@ -807,7 +807,7 @@ resolveSAWSymBV cc w tm =
               (_,tm'') <- rewriteSharedTerm sc cryptol_ss tm'
               (_,tm''') <- rewriteSharedTerm sc ss tm''
               if all isPreludeName (Map.elems $ getConstantSet tm''') then
-                do (_names, _, _, x) <- w4EvalAny sym st sc mempty Set.empty tm'''
+                do (_names, _, _, x) <- w4EvalAny sym st sc mempty unint tm'''
                    case valueToSymExpr x of
                      Just (Some y)
                        | Just Refl <- testEquality (W4.BaseBVRepr w) (W4.exprType y) ->
diff --git a/saw-central/src/SAWCentral/Crucible/LLVM/Setup/Value.hs b/saw-central/src/SAWCentral/Crucible/LLVM/Setup/Value.hs
index 967a42da37..e2d863b281 100644
--- a/saw-central/src/SAWCentral/Crucible/LLVM/Setup/Value.hs
+++ b/saw-central/src/SAWCentral/Crucible/LLVM/Setup/Value.hs
@@ -64,6 +64,7 @@ module SAWCentral.Crucible.LLVM.Setup.Value
   , ccLLVMGlobals
   , ccBasicSS
   , ccBackend
+  , ccUninterp
     -- * PointsTo
   , LLVMPointsTo(..)
   , LLVMPointsToValue(..)
@@ -90,6 +91,7 @@ import           Data.Text (Text)
 import qualified Data.Text as Text
 import           Data.Type.Equality (TestEquality(..))
 import           Data.Void (Void)
+import           Data.Set(Set)
 import qualified Prettyprinter as PPL
 import qualified Text.LLVM.AST as L
 import qualified Text.LLVM.PP as L
@@ -270,7 +272,6 @@ showLLVMModule (LLVMModule name m _) =
 -- ** CrucibleContext
 
 type instance Setup.CrucibleContext (LLVM arch) = LLVMCrucibleContext arch
-
 data LLVMCrucibleContext arch =
   LLVMCrucibleContext
   { _ccLLVMModule      :: LLVMModule arch
@@ -278,6 +279,7 @@ data LLVMCrucibleContext arch =
   , _ccLLVMSimContext  :: Crucible.SimContext (SAWCruciblePersonality Sym) Sym CL.LLVM
   , _ccLLVMGlobals     :: Crucible.SymGlobalState Sym
   , _ccBasicSS         :: Simpset TheoremNonce
+  , _ccUninterp        :: !(Set VarIndex)
   }
 
 makeLenses ''LLVMCrucibleContext
diff --git a/saw-central/src/SAWCentral/Crucible/LLVM/X86.hs b/saw-central/src/SAWCentral/Crucible/LLVM/X86.hs
index 13cb5f6da9..4a1f49ccac 100644
--- a/saw-central/src/SAWCentral/Crucible/LLVM/X86.hs
+++ b/saw-central/src/SAWCentral/Crucible/LLVM/X86.hs
@@ -486,6 +486,7 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec
           { _ccLLVMModule = llvmModule
           , _ccBackend = SomeOnlineBackend bak
           , _ccBasicSS = basic_ss
+          , _ccUninterp = Set.empty
 
           -- It's unpleasant that we need to do this to use resolveSetupVal.
           , _ccLLVMSimContext = error "Attempted to access ccLLVMSimContext"
diff --git a/saw-core/src/SAWCore/SharedTerm.hs b/saw-core/src/SAWCore/SharedTerm.hs
index 1b40c5250a..cc1d5dec24 100644
--- a/saw-core/src/SAWCore/SharedTerm.hs
+++ b/saw-core/src/SAWCore/SharedTerm.hs
@@ -248,6 +248,7 @@ module SAWCore.SharedTerm
   , instantiateVar
   , instantiateVarList
   , betaNormalize
+  , isConstFoldTerm
   , getAllExts
   , getAllExtSet
   , getConstantSet
@@ -2731,6 +2732,27 @@ whenModified b f m = ChangeT $ do
     Original{} -> return (Original b)
     Modified a -> Modified <$> f a
 
+-- | Can this term be evaluated to a constant?
+-- The parameter is a set of names which should be considered opaque---if
+-- we encounter any of these then the term is not considered to evaluate to
+-- a constant.
+isConstFoldTerm :: Set VarIndex -> Term -> Bool
+isConstFoldTerm unint t = isJust (go mempty t)
+    where
+    go !vis term =
+      case term of
+        STApp { stAppIndex = idx, stAppTermF = termF }
+          | IntSet.member idx vis -> Just vis
+          | otherwise -> goF (IntSet.insert idx vis) termF
+        Unshared termF -> goF vis termF
+    goF vis tf =
+      case tf of
+        Variable {} -> Nothing
+        Constant c
+          | nameIndex c `Set.member` unint -> Nothing
+          | otherwise -> Just vis
+        _ -> foldM go vis tf
+
 -- | Return a list of all ExtCns subterms in the given term, sorted by
 -- index. Does not traverse the unfoldings of @Constant@ terms.
 getAllExts :: Term -> [ExtCns Term]
diff --git a/saw-script/src/SAWScript/Interpreter.hs b/saw-script/src/SAWScript/Interpreter.hs
index 12520ea369..a5588f5890 100644
--- a/saw-script/src/SAWScript/Interpreter.hs
+++ b/saw-script/src/SAWScript/Interpreter.hs
@@ -4979,6 +4979,13 @@ primitives = Map.fromList
     Current
     [ "Legacy alternative name for `llvm_execute_func`." ]
 
+  , prim "llvm_unint" "Term -> LLVMSetup ()"
+    (pureVal llvm_unint)
+    Current
+    [ "Keep the given name opaque during symbolic simulation."
+    , "The input term should be a name."
+    ] 
+
   , prim "llvm_return" "SetupValue -> LLVMSetup ()"
     (pureVal llvm_return)
     Current

From 7f1b4d710be869ffe7150489b6eda2ec068d774d Mon Sep 17 00:00:00 2001
From: "Iavor S. Diatchki" <diatchki@galois.com>
Date: Wed, 8 Oct 2025 15:55:07 -0700
Subject: [PATCH 02/19] Factor common code and add `*_unint` commands to
 backends

---
 .../src/Mir/Compositional/State.hs            |  11 +-
 .../Crucible/Common/ResolveSetupValue.hs      | 158 ++++++++++++++----
 .../Crucible/Common/Setup/Builtins.hs         |  25 ++-
 .../src/SAWCentral/Crucible/JVM/Builtins.hs   |   6 +
 .../src/SAWCentral/Crucible/JVM/Override.hs   |   6 +-
 .../Crucible/JVM/ResolveSetupValue.hs         |  48 +-----
 .../SAWCentral/Crucible/JVM/Setup/Value.hs    |   4 +
 .../src/SAWCentral/Crucible/LLVM/Builtins.hs  |  18 +-
 .../Crucible/LLVM/ResolveSetupValue.hs        |  86 ++--------
 .../src/SAWCentral/Crucible/MIR/Builtins.hs   |   6 +
 .../src/SAWCentral/Crucible/MIR/Override.hs   |   7 +-
 .../Crucible/MIR/ResolveSetupValue.hs         |  37 +---
 .../SAWCentral/Crucible/MIR/Setup/Value.hs    |   4 +
 saw-script/src/SAWScript/Interpreter.hs       |  14 ++
 14 files changed, 233 insertions(+), 197 deletions(-)

diff --git a/crucible-mir-comp/src/Mir/Compositional/State.hs b/crucible-mir-comp/src/Mir/Compositional/State.hs
index b2cdfd92e8..8af1233d9a 100644
--- a/crucible-mir-comp/src/Mir/Compositional/State.hs
+++ b/crucible-mir-comp/src/Mir/Compositional/State.hs
@@ -29,8 +29,15 @@ data MirState t = MirState {
   -- ^ Inforamtion about what terms are loaded
 
   mirKeepUninterp     :: IORef (Set Text),
-  -- ^ Set of names we'd like to keep uninterpreted;
-  -- we use `_cryEnv` to compute what they refer to.
+  {- ^ Set of names we'd like to keep uninterpreted;
+    we use `_cryEnv` to compute what they refer to.
+    Note that in SAW, the MIRContext has a similar field,
+    of type `Set VarIndex`. We can't do the same here, instead we keep the
+    actual `Text` names.  The reason is because `crux-mir-comp` load Cryptol
+    code lazily, only when a function is first called.  As a result we can't
+    resolve the names early, because the Cryptol code would not yet have been
+    loaded.
+  -}
 
   mirSAWCoreState :: SAW.SAWCoreState t
 }
diff --git a/saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs b/saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs
index f9a2497916..19d2e951f7 100644
--- a/saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs
+++ b/saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs
@@ -1,49 +1,147 @@
 -- | Utilities for resolving 'SetupValue's that are used across language
 -- backends.
+{-# Language DataKinds, TypeOperators, GADTs, TypeApplications #-}
+{-# Language ImplicitParams #-}
 module SAWCentral.Crucible.Common.ResolveSetupValue ( 
-  resolveBoolTerm,
-  checkBooleanType
+  resolveBoolTerm, resolveBoolTerm',
+  resolveBitvectorTerm, resolveBitvectorTerm',
+  ResolveRewrite(..),
   ) where
 
+import qualified Data.Map as Map
+import           Data.Set(Set)
+import qualified Data.BitVector.Sized as BV
+import           Data.Parameterized.Some (Some(..))
+import           Data.Parameterized.NatRepr
+
 import qualified What4.BaseTypes as W4
 import qualified What4.Interface as W4
 
+
 import SAWCore.SharedTerm
+import SAWCore.Name
+import qualified SAWCore.Prim as Prim
 
 import qualified SAWCore.Simulator.Concrete as Concrete
+import qualified Lang.Crucible.Types as Crucible
+import qualified Lang.Crucible.Simulator.RegValue as Crucible
 
 import SAWCoreWhat4.ReturnTrip
 
 import SAWCentral.Crucible.Common
 
-import Cryptol.TypeCheck.Type (tIsBit)
+import SAWCentral.Proof (TheoremNonce)
+import SAWCore.Rewriter (Simpset, rewriteSharedTerm)
+import qualified CryptolSAWCore.Simpset as Cryptol
+import SAWCoreWhat4.What4(w4EvalAny, valueToSymExpr)
+
+import Cryptol.TypeCheck.Type (tIsBit, tIsSeq, tIsNum)
 import CryptolSAWCore.TypedTerm (mkTypedTerm, ttType, ttIsMono)
 import qualified Cryptol.Utils.PP as PP
 
--- | Resolve a SAWCore 'Term' into a What4 'W4.Pred'.
-resolveBoolTerm :: Sym -> Term -> IO (W4.Pred Sym)
-resolveBoolTerm sym tm =
-  do st <- sawCoreState sym
-     let sc = saw_ctx st
-     mx <- case getAllExts tm of
-             -- concretely evaluate if it is a closed term
-             [] ->
-               do modmap <- scGetModuleMap sc
-                  let v = Concrete.evalSharedTerm modmap mempty mempty tm
-                  pure (Just (Concrete.toBool v))
-             _ -> return Nothing
-     case mx of
-       Just x  -> return (W4.backendPred sym x)
-       Nothing -> bindSAWTerm sym st W4.BaseBoolRepr tm
-
--- | Ensure that the term has Cryptol type @Bit@.
-checkBooleanType :: SharedContext -> Term -> IO ()
-checkBooleanType sc tm = do
-  tt <- mkTypedTerm sc tm
-  case ttIsMono (ttType tt) of
-    Just ty | tIsBit ty -> pure ()
-            | otherwise -> fail $ unlines
-                 [ "Expected type: Bit"
-                 , "Actual type:   " ++ show (PP.pp ty)
-                 ]
-    Nothing -> fail "Expected monomorphic Cryptol type, got polymorphic or unrecognized type"
+
+-- | Optional rewrites to do when resolving a term
+data ResolveRewrite = ResolveRewrite {
+  rrBasicSS :: Maybe (Simpset TheoremNonce),
+  -- ^ Rewrite terms using these rewrites
+
+  rrWhat4Eval :: Bool
+  -- ^ Also simplify terms using What4 evaluation
+}
+
+-- | Don't do any rewriting
+noResolveRewrite :: ResolveRewrite
+noResolveRewrite = ResolveRewrite { rrBasicSS = Nothing, rrWhat4Eval = False }
+
+-- Convert a term to a What4 expression, trying to simplify it in the process.
+resolveTerm ::
+  Sym {- ^ Backend state -} ->
+  Set VarIndex {- ^ Keep these opaque -} ->
+  W4.BaseTypeRepr t  {- ^ Type of term -} ->
+  ResolveRewrite {- ^ Optional rewrites to do on the term -} ->
+  Term {- ^ Term to process -} ->
+  IO (Crucible.RegValue Sym (Crucible.BaseToType t))
+resolveTerm sym unint bt rr tm =
+  do
+    st       <- sawCoreState sym
+    tm'      <- basicRewrite st tm
+    case () of
+      _ | isConstFoldTerm unint tm' ->
+          do -- Evaluate as constant
+            modmap <- scGetModuleMap (saw_ctx st)
+            let v = Concrete.evalSharedTerm modmap mempty mempty tm'
+            case bt of
+              W4.BaseBoolRepr -> pure (W4.backendPred sym (Concrete.toBool v))
+              W4.BaseBVRepr w -> W4.bvLit sym w (BV.mkBV w (Prim.unsigned (Concrete.toWord v)))
+              _ -> fail "resolveTerm: expected `Bool` or bit-vector"
+
+        | rrWhat4Eval rr ->
+          do -- Try to use rewrites to simplify the term
+            let sc = saw_ctx st
+            cryptol_ss <- Cryptol.mkCryptolSimpset @TheoremNonce sc
+            tm''       <- snd <$> rewriteSharedTerm sc cryptol_ss tm'
+            tm'''      <- basicRewrite st tm''
+            if all isPreludeName (Map.elems (getConstantSet tm''')) then
+              do
+                (_, _, _, p) <- w4EvalAny sym st sc mempty unint tm'''
+                case valueToSymExpr p of
+                  Just (Some y)
+                    | Just Refl <- testEquality bt ty -> pure y
+                    | otherwise -> typeError (show ty)
+                    where ty = W4.exprType y
+                  _ -> fail ("resolveTem: unexpected w4Eval result " ++ show p)
+              else
+                doBind st tm'''
+
+          -- Just bind the term
+        | otherwise -> doBind st tm'
+
+  where
+  basicRewrite st =
+    case rrBasicSS rr of
+      Nothing -> pure
+      Just ss -> \t -> snd <$> rewriteSharedTerm (saw_ctx st) ss t
+
+  isPreludeName nm =
+    case nm of
+      ModuleIdentifier ident -> identModule ident == preludeName
+      _ -> False
+
+  doBind st te =
+    do
+      tt <- mkTypedTerm (saw_ctx st) tm
+      case ttIsMono (ttType tt) of
+          Just ty
+            | tIsBit ty, W4.BaseBoolRepr <- bt -> pure ()
+            | Just (n,el) <- (tIsSeq ty)
+            , tIsBit el, Just i <- tIsNum n, W4.BaseBVRepr w <- bt
+            , intValue w == i -> pure ()
+            | otherwise -> typeError (show (PP.pp ty)) :: IO ()
+          Nothing -> fail "Expected monomorphic Cryptol type, got polymorphic or unrecognized type"
+
+      bindSAWTerm sym st bt te
+
+  typeError :: String -> IO a
+  typeError t = fail $ unlines [
+    "Expected type: " ++ show bt,
+    "Actual type: " ++ t
+    ]
+
+-- 'resolveTerm' specialized to booleans.
+resolveBoolTerm' :: Sym -> Set VarIndex -> ResolveRewrite -> Term -> IO (W4.Pred Sym)
+resolveBoolTerm' sym unint = resolveTerm sym unint W4.BaseBoolRepr
+
+-- 'resolveTerm' specialized to booleans, without rewriting.
+resolveBoolTerm :: Sym -> Set VarIndex -> Term -> IO (W4.Pred Sym)
+resolveBoolTerm sym unint = resolveBoolTerm' sym unint noResolveRewrite
+
+-- 'resolveTerm' specialized to bit-vectors.
+resolveBitvectorTerm' ::
+  (1 W4.<= w) => Sym -> Set VarIndex -> W4.NatRepr w -> ResolveRewrite -> Term -> IO (W4.SymBV Sym w)
+resolveBitvectorTerm' sym unint w = resolveTerm sym unint (W4.BaseBVRepr w)
+                  
+-- 'resolveTerm' specialized to bit-vectors, without rewriting.
+resolveBitvectorTerm :: 
+  (1 W4.<= w) => Sym -> Set VarIndex -> W4.NatRepr w -> Term -> IO (W4.SymBV Sym w)
+resolveBitvectorTerm sym unint w = resolveBitvectorTerm' sym unint w noResolveRewrite
+
diff --git a/saw-central/src/SAWCentral/Crucible/Common/Setup/Builtins.hs b/saw-central/src/SAWCentral/Crucible/Common/Setup/Builtins.hs
index ce36af8e0e..e755e4ea35 100644
--- a/saw-central/src/SAWCentral/Crucible/Common/Setup/Builtins.hs
+++ b/saw-central/src/SAWCentral/Crucible/Common/Setup/Builtins.hs
@@ -8,6 +8,7 @@ Stability   : provisional
 
 {-# LANGUAGE DeriveTraversable #-}
 {-# LANGUAGE ParallelListComp #-}
+{-# LANGUAGE RankNTypes #-}
 
 module SAWCentral.Crucible.Common.Setup.Builtins
   ( crucible_precond
@@ -15,6 +16,7 @@ module SAWCentral.Crucible.Common.Setup.Builtins
   , crucible_return
   , crucible_execute_func
   , crucible_equal
+  , declare_unint
   , CheckPointsToType(..)
   ) where
 
@@ -22,10 +24,13 @@ import           Control.Lens
 import           Control.Monad (when)
 import           Control.Monad.State (get)
 import qualified Data.Map as Map
+import           Data.Set(Set)
 
 import qualified What4.ProgramLoc as W4
 
-import           CryptolSAWCore.TypedTerm (TypedTerm)
+import           SAWCore.Recognizer(asConstant)
+import           SAWCore.Name(VarIndex, nameIndex)
+import           CryptolSAWCore.TypedTerm (TypedTerm, ttTerm)
 
 import           SAWCentral.Value
 
@@ -37,6 +42,24 @@ import           SAWCentral.Crucible.Common.Setup.Type
 
 -- TODO: crucible_fresh_var?
 
+-- | Declare a particular name as opaque
+declare_unint ::
+  String {- ^ Name of command for error messages -} ->
+  Setter' (MS.CrucibleContext ext) (Set VarIndex) {-^ Keep uninterpreted names here -} ->
+  TypedTerm {- ^ Term corresponding to the name -} ->
+  CrucibleSetup ext ()
+declare_unint cmd unintF term =
+  do
+    prePost <- use csPrePost
+    case prePost of
+      MS.PreState ->
+        case asConstant (ttTerm term) of
+          Nothing -> fail ("The argument to `" ++ cmd ++ "` should be a name.")
+          Just n  -> csCrucibleContext . unintF . contains (nameIndex n) .= True
+      MS.PostState ->
+        fail ("`" ++ cmd ++ "` works only int the pre-condition of a specification.")
+     
+
 crucible_precond ::
   W4.ProgramLoc ->
   TypedTerm ->
diff --git a/saw-central/src/SAWCentral/Crucible/JVM/Builtins.hs b/saw-central/src/SAWCentral/Crucible/JVM/Builtins.hs
index ad5fdbf226..4621260904 100644
--- a/saw-central/src/SAWCentral/Crucible/JVM/Builtins.hs
+++ b/saw-central/src/SAWCentral/Crucible/JVM/Builtins.hs
@@ -46,6 +46,7 @@ module SAWCentral.Crucible.JVM.Builtins
     , jvm_setup_with_tag
     , jvm_ghost_value
     , jvm_equal
+    , jvm_unint
     ) where
 
 import           Control.Lens
@@ -139,6 +140,7 @@ import qualified SAWCentral.Crucible.Common.Vacuity as Vacuity
 import qualified SAWCentral.Crucible.Common.MethodSpec as MS
 import qualified SAWCentral.Crucible.Common.Setup.Type as Setup
 import qualified SAWCentral.Crucible.Common.Setup.Builtins as Setup
+import SAWCentral.Crucible.JVM.Setup.Value(jccUninterp)
 import SAWCentral.Crucible.JVM.MethodSpecIR
 import SAWCentral.Crucible.JVM.Override
 import SAWCentral.Crucible.JVM.ResolveSetupValue
@@ -862,6 +864,7 @@ setupCrucibleContext jclass =
                                , _jccBackend = bak
                                , _jccJVMContext = jc
                                , _jccHandleAllocator = halloc
+                               , _jccUninterp = mempty
                                }
 
 --------------------------------------------------------------------------------
@@ -1474,6 +1477,9 @@ jvm_equal val1 val2 =
        ]
      Setup.crucible_equal loc val1 val2
 
+jvm_unint :: TypedTerm -> JVMSetupM ()
+jvm_unint term = JVMSetupM (Setup.declare_unint "jvm_unint" jccUninterp term)
+
 --------------------------------------------------------------------------------
 
 -- | Sort a list of things and group them into equivalence classes.
diff --git a/saw-central/src/SAWCentral/Crucible/JVM/Override.hs b/saw-central/src/SAWCentral/Crucible/JVM/Override.hs
index 8c572bf87a..8b51337a8f 100644
--- a/saw-central/src/SAWCentral/Crucible/JVM/Override.hs
+++ b/saw-central/src/SAWCentral/Crucible/JVM/Override.hs
@@ -111,7 +111,7 @@ import qualified SAWCentral.Crucible.Common.Override as Ov (getSymInterface)
 import qualified SAWCentral.Crucible.Common.MethodSpec as MS
 import           SAWCentral.Crucible.JVM.MethodSpecIR
 import           SAWCentral.Crucible.JVM.ResolveSetupValue
-import           SAWCentral.Crucible.JVM.Setup.Value ()
+import           SAWCentral.Crucible.JVM.Setup.Value (jccUninterp)
 import           SAWCentral.Options
 import           SAWCentral.Panic
 import           SAWCentral.Utils (handleException)
@@ -730,7 +730,7 @@ learnPred ::
 learnPred sc cc md prepost t =
   do s <- OM (use termSub)
      u <- liftIO $ scInstantiateExt sc s t
-     p <- liftIO $ resolveBoolTerm (cc ^. jccSym) u
+     p <- liftIO $ resolveBoolTerm (cc ^. jccSym) (cc ^. jccUninterp) u
      let loc = MS.conditionLoc md
      addAssert p md (Crucible.SimError loc (Crucible.AssertFailureSimError (MS.stateCond prepost) ""))
 
@@ -918,7 +918,7 @@ executePred ::
 executePred sc cc md tt =
   do s <- OM (use termSub)
      t <- liftIO $ scInstantiateExt sc s (ttTerm tt)
-     p <- liftIO $ resolveBoolTerm (cc ^. jccSym) t
+     p <- liftIO $ resolveBoolTerm (cc ^. jccSym) (cc ^. jccUninterp) t
      addAssume p md
 
 ------------------------------------------------------------------------
diff --git a/saw-central/src/SAWCentral/Crucible/JVM/ResolveSetupValue.hs b/saw-central/src/SAWCentral/Crucible/JVM/ResolveSetupValue.hs
index 729147735e..968d44d21d 100644
--- a/saw-central/src/SAWCentral/Crucible/JVM/ResolveSetupValue.hs
+++ b/saw-central/src/SAWCentral/Crucible/JVM/ResolveSetupValue.hs
@@ -47,11 +47,6 @@ import qualified What4.Interface as W4
 import SAWCore.SharedTerm
 import CryptolSAWCore.TypedTerm
 
-import qualified SAWCore.Prim as Prim
-import qualified SAWCore.Simulator.Concrete as Concrete
-
-import SAWCoreWhat4.ReturnTrip
-
 -- crucible
 
 import qualified Lang.Crucible.Simulator as Crucible (RegValue)
@@ -70,9 +65,9 @@ import SAWCentral.Crucible.Common.MethodSpec (AllocIndex(..))
 
 import SAWCentral.Panic
 import SAWCentral.Crucible.JVM.MethodSpecIR
-import SAWCentral.Crucible.JVM.Setup.Value (JVMRefVal)
+import SAWCentral.Crucible.JVM.Setup.Value (JVMRefVal, jccUninterp)
 import qualified SAWCentral.Crucible.Common.MethodSpec as MS
-import SAWCentral.Crucible.Common.ResolveSetupValue ( resolveBoolTerm, checkBooleanType )
+import SAWCentral.Crucible.Common.ResolveSetupValue (resolveBoolTerm, resolveBitvectorTerm)
 
 
 data JVMVal
@@ -214,12 +209,7 @@ resolveSAWPred ::
   JVMCrucibleContext ->
   Term ->
   IO (W4.Pred Sym)
-resolveSAWPred cc tm =
-  do let sym = cc^.jccSym
-     st <- sawCoreState sym
-     let sc = saw_ctx st
-     checkBooleanType sc tm
-     bindSAWTerm sym st W4.BaseBoolRepr tm
+resolveSAWPred cc = resolveBoolTerm (cc ^. jccSym) (cc ^. jccUninterp)
 
 resolveSAWTerm ::
   JVMCrucibleContext ->
@@ -229,7 +219,7 @@ resolveSAWTerm ::
 resolveSAWTerm cc tp tm =
   case tp of
     Cryptol.TVBit ->
-      do b <- resolveBoolTerm sym tm
+      do b <- resolveBoolTerm sym (cc ^. jccUninterp) tm
          x0 <- W4.bvLit sym W4.knownNat (BV.zero W4.knownNat)
          x1 <- W4.bvLit sym W4.knownNat (BV.one  W4.knownNat)
          x <- W4.bvIte sym b x1 x0
@@ -245,13 +235,14 @@ resolveSAWTerm cc tp tm =
     Cryptol.TVRational ->
       fail "resolveSAWTerm: unimplemented type Rational (FIXME)"
     Cryptol.TVSeq sz Cryptol.TVBit ->
+      let unint = cc ^. jccUninterp in
       case sz of
-        8  -> do x <- resolveBitvectorTerm sym (W4.knownNat @8) tm
+        8  -> do x <- resolveBitvectorTerm sym unint (W4.knownNat @8) tm
                  IVal <$> W4.bvSext sym W4.knownNat x
-        16 -> do x <- resolveBitvectorTerm sym (W4.knownNat @16) tm
+        16 -> do x <- resolveBitvectorTerm sym unint (W4.knownNat @16) tm
                  IVal <$> W4.bvSext sym W4.knownNat x
-        32 -> IVal <$> resolveBitvectorTerm sym W4.knownNat tm
-        64 -> LVal <$> resolveBitvectorTerm sym W4.knownNat tm
+        32 -> IVal <$> resolveBitvectorTerm sym unint W4.knownNat tm
+        64 -> LVal <$> resolveBitvectorTerm sym unint W4.knownNat tm
         _  -> fail ("Invalid bitvector width: " ++ show sz)
     Cryptol.TVSeq _sz _tp' ->
       fail "resolveSAWTerm: unimplemented sequence type"
@@ -268,27 +259,6 @@ resolveSAWTerm cc tp tm =
   where
     sym = cc^.jccSym
 
-resolveBitvectorTerm ::
-  forall w.
-  (1 W4.<= w) =>
-  Sym ->
-  W4.NatRepr w ->
-  Term ->
-  IO (W4.SymBV Sym w)
-resolveBitvectorTerm sym w tm =
-  do st <- sawCoreState sym
-     let sc = saw_ctx st
-     mx <- case getAllExts tm of
-             -- concretely evaluate if it is a closed term
-             [] ->
-               do modmap <- scGetModuleMap sc
-                  let v = Concrete.evalSharedTerm modmap mempty mempty tm
-                  pure (Just (Prim.unsigned (Concrete.toWord v)))
-             _ -> return Nothing
-     case mx of
-       Just x  -> W4.bvLit sym w (BV.mkBV w x)
-       Nothing -> bindSAWTerm sym st (W4.BaseBVRepr w) tm
-
 toJVMType :: Cryptol.TValue -> Maybe J.Type
 toJVMType tp =
   case tp of
diff --git a/saw-central/src/SAWCentral/Crucible/JVM/Setup/Value.hs b/saw-central/src/SAWCentral/Crucible/JVM/Setup/Value.hs
index dabc7ad152..de60220379 100644
--- a/saw-central/src/SAWCentral/Crucible/JVM/Setup/Value.hs
+++ b/saw-central/src/SAWCentral/Crucible/JVM/Setup/Value.hs
@@ -49,11 +49,13 @@ module SAWCentral.Crucible.JVM.Setup.Value
   , jccJVMContext
   , jccBackend
   , jccHandleAllocator
+  , jccUninterp
 
   , JVMRefVal
   ) where
 
 import           Control.Lens
+import           Data.Set(Set)
 import           Data.Void (Void)
 import qualified Prettyprinter as PPL
 
@@ -70,6 +72,7 @@ import qualified Language.JVM.Parser as J
 -- cryptol-saw-core
 import           CryptolSAWCore.TypedTerm (TypedTerm)
 
+import           SAWCore.Name(VarIndex)
 import           SAWCentral.Crucible.Common
 import qualified SAWCentral.Crucible.Common.Setup.Value as MS
 
@@ -150,6 +153,7 @@ data JVMCrucibleContext =
   , _jccJVMContext     :: CJ.JVMContext
   , _jccBackend        :: SomeOnlineBackend
   , _jccHandleAllocator :: Crucible.HandleAllocator
+  , _jccUninterp       :: Set VarIndex
   }
 
 makeLenses ''JVMCrucibleContext
diff --git a/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs b/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs
index 332b7a17e7..a8c6f5686a 100644
--- a/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs
+++ b/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs
@@ -170,7 +170,7 @@ import qualified SAWCentral.Crucible.LLVM.CrucibleLLVM as Crucible
 
 -- saw-core
 import SAWCore.FiniteValue (ppFirstOrderValue)
-import SAWCore.Name (ecShortName, nameIndex)
+import SAWCore.Name (ecShortName)
 import SAWCore.SharedTerm
 import SAWCore.Recognizer
 import SAWCore.Term.Pretty (showTerm)
@@ -205,8 +205,8 @@ import qualified SAWCentral.Crucible.Common.Vacuity as Vacuity
 
 import SAWCentral.Crucible.LLVM.Override
 import SAWCentral.Crucible.LLVM.ResolveSetupValue
-import SAWCentral.Crucible.LLVM.MethodSpecIR
 import SAWCentral.Crucible.LLVM.Setup.Value(ccUninterp)
+import SAWCentral.Crucible.LLVM.MethodSpecIR
 import SAWCentral.Panic (panic)
 
 type AssumptionReason = (MS.ConditionMetadata, String)
@@ -1780,7 +1780,7 @@ setupLLVMCrucibleContext pathSat lm action =
                                      , _ccLLVMSimContext = lsimctx
                                      , _ccLLVMGlobals = lglobals
                                      , _ccBasicSS = basic_ss
-                                     , _ccUninterp = Set.empty
+                                     , _ccUninterp = mempty
                                      }
           action cc
 
@@ -2012,17 +2012,7 @@ llvm_postcond term =
 
 llvm_unint :: TypedTerm -> LLVMCrucibleSetupM ()
 llvm_unint term =
-  LLVMCrucibleSetupM $
-    do
-      prePost <- use Setup.csPrePost
-      case prePost of
-        PreState ->
-          case asConstant (ttTerm term) of
-            Nothing -> fail "The argument to `llvm_unint` should be a name."
-            Just n ->
-              do 
-                 Setup.csCrucibleContext . ccUninterp . contains (nameIndex n) .= True
-        PostState -> fail "`llvm_unint` works only int the pre-condition of a specification."
+  LLVMCrucibleSetupM (Setup.declare_unint "llvm_unint" ccUninterp term)
           
 
 llvm_return ::
diff --git a/saw-central/src/SAWCentral/Crucible/LLVM/ResolveSetupValue.hs b/saw-central/src/SAWCentral/Crucible/LLVM/ResolveSetupValue.hs
index deded8fbaf..ad7a03e2d5 100644
--- a/saw-central/src/SAWCentral/Crucible/LLVM/ResolveSetupValue.hs
+++ b/saw-central/src/SAWCentral/Crucible/LLVM/ResolveSetupValue.hs
@@ -39,7 +39,6 @@ import Control.Lens ( (^.), view )
 import Control.Monad
 import Control.Monad.Except
 import Control.Monad.State
-import qualified Data.BitVector.Sized as BV
 import Data.Maybe (fromMaybe, fromJust)
 import Data.Void (absurd)
 
@@ -56,12 +55,10 @@ import qualified Text.LLVM.AST as L
 
 import qualified Cryptol.Eval.Type as Cryptol (TValue(..), tValTy, evalValType)
 import qualified Cryptol.TypeCheck.AST as Cryptol (Schema(..))
-import qualified CryptolSAWCore.Simpset as Cryptol
 
 import           Data.Parameterized.Some (Some(..))
 import           Data.Parameterized.NatRepr
 
-import qualified What4.BaseTypes    as W4
 import qualified What4.Interface    as W4
 
 import qualified Lang.Crucible.LLVM.Bytes       as Crucible
@@ -70,25 +67,19 @@ import qualified Lang.Crucible.LLVM.MemType     as Crucible
 import qualified Lang.Crucible.LLVM.Translation as Crucible
 import qualified SAWCentral.Crucible.LLVM.CrucibleLLVM as Crucible
 
-import SAWCore.Rewriter
 import SAWCore.SharedTerm
-import qualified SAWCore.Prim as Prim
-import qualified SAWCore.Simulator.Concrete as Concrete
 
 import CryptolSAWCore.Cryptol (importType, emptyEnv)
-import SAWCore.Name
 import CryptolSAWCore.TypedTerm
-import SAWCoreWhat4.What4
 import SAWCoreWhat4.ReturnTrip
 import qualified Text.LLVM.DebugUtils as L
 
 import           SAWCentral.Crucible.Common (Sym, sawCoreState, HasSymInterface(..))
 import           SAWCentral.Crucible.Common.MethodSpec (AllocIndex(..), SetupValue(..))
-import           SAWCentral.Crucible.Common.ResolveSetupValue (checkBooleanType)
+import qualified SAWCentral.Crucible.Common.ResolveSetupValue as Common
 
 import SAWCentral.Crucible.LLVM.MethodSpecIR
 import SAWCentral.Crucible.LLVM.Setup.Value (LLVMPtr, ccUninterp)
-import qualified SAWCentral.Proof as SP
 
 type LLVMVal = Crucible.LLVMVal Sym
 
@@ -751,34 +742,12 @@ resolveSAWPred ::
   LLVMCrucibleContext arch ->
   Term ->
   IO (W4.Pred Sym)
-resolveSAWPred cc tm = do
-  do let sym = cc^.ccSym
-     st <- sawCoreState sym
-     let sc = saw_ctx st
-     let ss = cc^.ccBasicSS
-         unint = cc ^. ccUninterp
-     (_,tm') <- rewriteSharedTerm sc ss tm
-
-     checkBooleanType sc tm'
-
-     mx <- if not (isConstFoldTerm unint tm') then pure Nothing else
-             -- concretely evaluate if it is a closed term
-             do modmap <- scGetModuleMap sc
-                let v = Concrete.evalSharedTerm modmap mempty mempty tm'
-                pure (Just (Concrete.toBool v))
-     case mx of
-       Just x  -> return $ W4.backendPred sym x
-       Nothing
-         | doW4Eval ?w4EvalTactic ->
-           do cryptol_ss <- Cryptol.mkCryptolSimpset @SP.TheoremNonce sc
-              (_,tm'') <- rewriteSharedTerm sc cryptol_ss tm'
-              (_,tm''') <- rewriteSharedTerm sc ss tm''
-              if all isPreludeName (Map.elems $ getConstantSet tm''') then
-                do (_names, (_mlabels, p)) <- w4Eval sym st sc mempty unint tm'''
-                   return p
-              else bindSAWTerm sym st W4.BaseBoolRepr tm'
-         | otherwise ->
-           bindSAWTerm sym st W4.BaseBoolRepr tm'
+resolveSAWPred cc =
+  Common.resolveBoolTerm' (cc ^. ccSym) (cc ^. ccUninterp)
+  Common.ResolveRewrite {
+    Common.rrBasicSS = Just (cc ^. ccBasicSS),
+    Common.rrWhat4Eval = doW4Eval ?w4EvalTactic
+  }
 
 resolveSAWSymBV ::
   (?w4EvalTactic :: W4EvalTactic, 1 <= w) =>
@@ -786,41 +755,12 @@ resolveSAWSymBV ::
   NatRepr w ->
   Term ->
   IO (W4.SymBV Sym w)
-resolveSAWSymBV cc w tm =
-  do let sym = cc^.ccSym
-     st <- sawCoreState sym
-     let sc = saw_ctx st
-         unint = cc ^. ccUninterp
-     mx <- if not (isConstFoldTerm unint tm) then pure Nothing else
-             -- concretely evaluate if it is a closed term
-             do modmap <- scGetModuleMap sc
-                let v = Concrete.evalSharedTerm modmap mempty mempty tm
-                pure (Just (Prim.unsigned (Concrete.toWord v)))
-            
-     case mx of
-       Just x  -> W4.bvLit sym w (BV.mkBV w x)
-       Nothing
-         | doW4Eval ?w4EvalTactic ->
-           do let ss = cc^.ccBasicSS
-              (_,tm') <- rewriteSharedTerm sc ss tm
-              cryptol_ss <- Cryptol.mkCryptolSimpset @SP.TheoremNonce sc
-              (_,tm'') <- rewriteSharedTerm sc cryptol_ss tm'
-              (_,tm''') <- rewriteSharedTerm sc ss tm''
-              if all isPreludeName (Map.elems $ getConstantSet tm''') then
-                do (_names, _, _, x) <- w4EvalAny sym st sc mempty unint tm'''
-                   case valueToSymExpr x of
-                     Just (Some y)
-                       | Just Refl <- testEquality (W4.BaseBVRepr w) (W4.exprType y) ->
-                         return y
-                     _ -> fail $ "resolveSAWSymBV: unexpected w4Eval result " ++ show x
-              else bindSAWTerm sym st (W4.BaseBVRepr w) tm
-         | otherwise ->
-           bindSAWTerm sym st (W4.BaseBVRepr w) tm
-
-isPreludeName :: NameInfo -> Bool
-isPreludeName = \case
-  ModuleIdentifier ident -> identModule ident == preludeName
-  _ -> False
+resolveSAWSymBV cc w =
+  Common.resolveBitvectorTerm' (cc ^. ccSym) (cc ^. ccUninterp) w
+  Common.ResolveRewrite {
+    Common.rrBasicSS = Just (cc ^. ccBasicSS),
+    Common.rrWhat4Eval = doW4Eval ?w4EvalTactic
+  }
 
 resolveSAWTerm ::
   (?w4EvalTactic :: W4EvalTactic, Crucible.HasPtrWidth (Crucible.ArchWidth arch)) =>
diff --git a/saw-central/src/SAWCentral/Crucible/MIR/Builtins.hs b/saw-central/src/SAWCentral/Crucible/MIR/Builtins.hs
index 9b9170059c..9f15581dcf 100644
--- a/saw-central/src/SAWCentral/Crucible/MIR/Builtins.hs
+++ b/saw-central/src/SAWCentral/Crucible/MIR/Builtins.hs
@@ -37,6 +37,7 @@ module SAWCentral.Crucible.MIR.Builtins
   , mir_return
   , mir_unsafe_assume_spec
   , mir_verify
+  , mir_unint
     -- ** MIR enums
   , mir_enum_value
     -- ** MIR slices
@@ -174,6 +175,7 @@ import SAWCentral.Proof
 import SAWCentral.Prover.SolverStats
 import SAWCentral.Utils (neGroupOn)
 import SAWCentral.Value
+import SAWCentral.Crucible.MIR.Setup.Value(mccUninterp)
 
 type AssumptionReason = (MS.ConditionMetadata, String)
 type SetupValue = MS.SetupValue MIR
@@ -786,6 +788,9 @@ mir_points_to_internal mode ref val =
            , "  Value type:    " ++ show (PP.pretty valTy)
            ]
 
+mir_unint :: TypedTerm -> MIRSetupM ()
+mir_unint term = MIRSetupM (Setup.declare_unint "mir_unint" mccUninterp term)
+
 -- | Perform a set of validity checks on the LHS reference or pointer value in a
 -- 'mir_points_to' or 'mir_points_to_multi' command. In particular:
 --
@@ -2097,6 +2102,7 @@ setupCrucibleContext rm =
                                , _mccSimContext = simctx1
                                , _mccSymGlobalState = globalsImmutStaticsOnly
                                , _mccStaticInitializerMap = staticInitializerMap
+                               , _mccUninterp = mempty
                                }
 
 -- | Create a result value of the appropriate type, suitable for use in an
diff --git a/saw-central/src/SAWCentral/Crucible/MIR/Override.hs b/saw-central/src/SAWCentral/Crucible/MIR/Override.hs
index b70a4a6207..ac71246100 100644
--- a/saw-central/src/SAWCentral/Crucible/MIR/Override.hs
+++ b/saw-central/src/SAWCentral/Crucible/MIR/Override.hs
@@ -84,6 +84,7 @@ import qualified SAWCentral.Crucible.Common.MethodSpec as MS
 import SAWCentral.Crucible.Common.MethodSpec (AllocIndex(..))
 import qualified SAWCentral.Crucible.Common.Override as Ov (getSymInterface)
 import SAWCentral.Crucible.Common.Override hiding (getSymInterface)
+import SAWCentral.Crucible.MIR.Setup.Value(mccUninterp)
 import SAWCentral.Crucible.MIR.MethodSpecIR
 import SAWCentral.Crucible.MIR.ResolveSetupValue
 import SAWCentral.Crucible.MIR.TypeShape
@@ -632,7 +633,7 @@ executePred ::
 executePred sc cc md tt =
   do s <- OM (use termSub)
      t <- liftIO $ scInstantiateExt sc s (ttTerm tt)
-     p <- liftIO $ resolveBoolTerm (cc ^. mccSym) t
+     p <- liftIO $ resolveBoolTerm (cc ^. mccSym) (cc ^. mccUninterp) t
      addAssume p md
 
 -- | Update the simulator state based on the postconditions from the
@@ -1051,7 +1052,7 @@ learnPred ::
 learnPred sc cc md prepost t =
   do s <- OM (use termSub)
      u <- liftIO $ scInstantiateExt sc s t
-     p <- liftIO $ resolveBoolTerm (cc ^. mccSym) u
+     p <- liftIO $ resolveBoolTerm (cc ^. mccSym) (cc ^. mccUninterp) u
      let loc = MS.conditionLoc md
      addAssert p md (Crucible.SimError loc (Crucible.AssertFailureSimError (MS.stateCond prepost) ""))
 
@@ -1433,7 +1434,7 @@ matchArg opts sc cc cs prepost md = go False []
                 addAssert pred_ md =<< notEq
             _ -> fail_
         (_, _, MS.SetupMux () c t f) -> do
-          cPred <- liftIO $ resolveBoolTerm sym (ttTerm c)
+          cPred <- liftIO $ resolveBoolTerm sym (cc ^. mccUninterp) (ttTerm c)
           withConditionalPred cPred $
             go inCast projStack actual t
           cNegPred <- liftIO $ W4.notPred sym cPred
diff --git a/saw-central/src/SAWCentral/Crucible/MIR/ResolveSetupValue.hs b/saw-central/src/SAWCentral/Crucible/MIR/ResolveSetupValue.hs
index 939228ee2e..4b43209327 100644
--- a/saw-central/src/SAWCentral/Crucible/MIR/ResolveSetupValue.hs
+++ b/saw-central/src/SAWCentral/Crucible/MIR/ResolveSetupValue.hs
@@ -103,15 +103,14 @@ import qualified What4.Partial as W4
 
 import CryptolSAWCore.Cryptol (importType, emptyEnv)
 import SAWCore.SharedTerm
-import qualified SAWCore.Prim as Prim
-import qualified SAWCore.Simulator.Concrete as Concrete
 import SAWCoreWhat4.ReturnTrip
 import CryptolSAWCore.TypedTerm
 
 import SAWCentral.Crucible.Common
 import qualified SAWCentral.Crucible.Common.MethodSpec as MS
 import SAWCentral.Crucible.Common.MethodSpec (AllocIndex(..))
-import SAWCentral.Crucible.Common.ResolveSetupValue (resolveBoolTerm, checkBooleanType)
+import SAWCentral.Crucible.Common.ResolveSetupValue (resolveBoolTerm, resolveBitvectorTerm)
+import SAWCentral.Crucible.MIR.Setup.Value(mccUninterp)
 import SAWCentral.Crucible.MIR.MethodSpecIR
 import SAWCentral.Crucible.MIR.TypeShape
 import SAWCentral.Panic
@@ -987,12 +986,7 @@ resolveSAWPred ::
   MIRCrucibleContext ->
   Term ->
   IO (W4.Pred Sym)
-resolveSAWPred cc tm =
-  do let sym = cc^.mccSym
-     st <- sawCoreState sym
-     let sc = saw_ctx st
-     checkBooleanType sc tm
-     bindSAWTerm sym st W4.BaseBoolRepr tm
+resolveSAWPred cc = resolveBoolTerm (cc ^. mccSym) (cc ^. mccUninterp)
 
 resolveSAWTerm ::
   MIRCrucibleContext ->
@@ -1002,7 +996,7 @@ resolveSAWTerm ::
 resolveSAWTerm mcc tp tm =
   case tp of
     Cryptol.TVBit ->
-      do b <- resolveBoolTerm sym tm
+      do b <- resolveBoolTerm sym (mcc ^. mccUninterp) tm
          pure $ MIRVal (PrimShape Mir.TyBool W4.BaseBoolRepr) b
     Cryptol.TVInteger ->
       fail "resolveSAWTerm: unimplemented type Integer (FIXME)"
@@ -1027,7 +1021,7 @@ resolveSAWTerm mcc tp tm =
                 => Mir.BaseSize -> W4.NatRepr w -> IO MIRVal
         bv_term b n =
          MIRVal (PrimShape (Mir.TyUint b) (W4.BaseBVRepr n)) <$>
-         resolveBitvectorTerm sym n tm
+         resolveBitvectorTerm sym (mcc ^. mccUninterp) n tm
     Cryptol.TVSeq sz tp' -> do
       doIndex <- indexSeqTerm sym (sz, tp') tm
       case toMIRType tp' of
@@ -1077,27 +1071,6 @@ resolveSAWTerm mcc tp tm =
     sym = mcc ^. mccSym
     col = mcc ^. mccRustModule ^. Mir.rmCS ^. Mir.collection
 
-resolveBitvectorTerm ::
-  forall w.
-  (1 W4.<= w) =>
-  Sym ->
-  W4.NatRepr w ->
-  Term ->
-  IO (W4.SymBV Sym w)
-resolveBitvectorTerm sym w tm =
-  do st <- sawCoreState sym
-     let sc = saw_ctx st
-     mx <- case getAllExts tm of
-             -- concretely evaluate if it is a closed term
-             [] ->
-               do modmap <- scGetModuleMap sc
-                  let v = Concrete.evalSharedTerm modmap mempty mempty tm
-                  pure (Just (Prim.unsigned (Concrete.toWord v)))
-             _ -> return Nothing
-     case mx of
-       Just x  -> W4.bvLit sym w (BV.mkBV w x)
-       Nothing -> bindSAWTerm sym st (W4.BaseBVRepr w) tm
-
 data ToMIRTypeErr = NotYetSupported String | Impossible String
 
 toMIRTypeErrToString :: ToMIRTypeErr -> String
diff --git a/saw-central/src/SAWCentral/Crucible/MIR/Setup/Value.hs b/saw-central/src/SAWCentral/Crucible/MIR/Setup/Value.hs
index 09476f1c10..599a5193f4 100644
--- a/saw-central/src/SAWCentral/Crucible/MIR/Setup/Value.hs
+++ b/saw-central/src/SAWCentral/Crucible/MIR/Setup/Value.hs
@@ -29,6 +29,7 @@ module SAWCentral.Crucible.MIR.Setup.Value
   , mccSimContext
   , mccSymGlobalState
   , mccStaticInitializerMap
+  , mccUninterp
 
     -- * @MirStaticInitializerMap@
   , MirStaticInitializerMap
@@ -72,6 +73,7 @@ import Control.Lens (makeLenses)
 import Data.Parameterized.Classes
 import Data.Parameterized.Map (MapF)
 import Data.Parameterized.Some
+import Data.Set(Set)
 import Data.Text (Text)
 import Data.Void (Void)
 
@@ -82,6 +84,7 @@ import Mir.Generator
 import Mir.Intrinsics
 import qualified Mir.Mir as M
 
+import           SAWCore.Name(VarIndex)
 import           SAWCentral.Crucible.Common
 import qualified SAWCentral.Crucible.Common.Setup.Value as MS
 
@@ -119,6 +122,7 @@ data MIRCrucibleContext =
   , _mccSimContext           :: SimContext (SAWCruciblePersonality Sym) Sym MIR
   , _mccSymGlobalState       :: SymGlobalState Sym
   , _mccStaticInitializerMap :: MirStaticInitializerMap
+  , _mccUninterp             :: Set VarIndex
   }
 
 type instance MS.CrucibleContext MIR = MIRCrucibleContext
diff --git a/saw-script/src/SAWScript/Interpreter.hs b/saw-script/src/SAWScript/Interpreter.hs
index a5588f5890..7db7200b70 100644
--- a/saw-script/src/SAWScript/Interpreter.hs
+++ b/saw-script/src/SAWScript/Interpreter.hs
@@ -4984,6 +4984,20 @@ primitives = Map.fromList
     Current
     [ "Keep the given name opaque during symbolic simulation."
     , "The input term should be a name."
+    ]
+
+  , prim "jvm_unint" "Term -> JVMSetup ()"
+    (pureVal jvm_unint)
+    Current
+    [ "Keep the given name opaque during symbolic simulation."
+    , "The input term should be a name."
+    ] 
+
+  , prim "mir_unint" "Term -> MIRSetup ()"
+    (pureVal mir_unint)
+    Current
+    [ "Keep the given name opaque during symbolic simulation."
+    , "The input term should be a name."
     ] 
 
   , prim "llvm_return" "SetupValue -> LLVMSetup ()"

From 354f34f6d05dc5d9d93f18678aafe3fe145b3dae Mon Sep 17 00:00:00 2001
From: "Iavor S. Diatchki" <iavor.diatchki@gmail.com>
Date: Thu, 9 Oct 2025 09:11:24 -0700
Subject: [PATCH 03/19] Update
 saw-central/src/SAWCentral/Crucible/Common/Setup/Builtins.hs

Co-authored-by: Ryan Scott <rscott@galois.com>
---
 saw-central/src/SAWCentral/Crucible/Common/Setup/Builtins.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/saw-central/src/SAWCentral/Crucible/Common/Setup/Builtins.hs b/saw-central/src/SAWCentral/Crucible/Common/Setup/Builtins.hs
index e755e4ea35..66a99fd03a 100644
--- a/saw-central/src/SAWCentral/Crucible/Common/Setup/Builtins.hs
+++ b/saw-central/src/SAWCentral/Crucible/Common/Setup/Builtins.hs
@@ -57,7 +57,7 @@ declare_unint cmd unintF term =
           Nothing -> fail ("The argument to `" ++ cmd ++ "` should be a name.")
           Just n  -> csCrucibleContext . unintF . contains (nameIndex n) .= True
       MS.PostState ->
-        fail ("`" ++ cmd ++ "` works only int the pre-condition of a specification.")
+        fail ("`" ++ cmd ++ "` works only in the pre-condition of a specification.")
      
 
 crucible_precond ::

From 719e44cd7242c64029e4f5349f8a3f2a812fc0a6 Mon Sep 17 00:00:00 2001
From: "Iavor S. Diatchki" <iavor.diatchki@gmail.com>
Date: Thu, 9 Oct 2025 09:11:37 -0700
Subject: [PATCH 04/19] Update crucible-mir-comp/src/Mir/Compositional/State.hs

Co-authored-by: Ryan Scott <rscott@galois.com>
---
 crucible-mir-comp/src/Mir/Compositional/State.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/crucible-mir-comp/src/Mir/Compositional/State.hs b/crucible-mir-comp/src/Mir/Compositional/State.hs
index 8af1233d9a..92a65f5b7f 100644
--- a/crucible-mir-comp/src/Mir/Compositional/State.hs
+++ b/crucible-mir-comp/src/Mir/Compositional/State.hs
@@ -33,7 +33,7 @@ data MirState t = MirState {
     we use `_cryEnv` to compute what they refer to.
     Note that in SAW, the MIRContext has a similar field,
     of type `Set VarIndex`. We can't do the same here, instead we keep the
-    actual `Text` names.  The reason is because `crux-mir-comp` load Cryptol
+    actual `Text` names.  The reason is because `crux-mir-comp` loads Cryptol
     code lazily, only when a function is first called.  As a result we can't
     resolve the names early, because the Cryptol code would not yet have been
     loaded.

From fbb39a66ea9254cd51f927b64964aa62f16ec11e Mon Sep 17 00:00:00 2001
From: "Iavor S. Diatchki" <iavor.diatchki@gmail.com>
Date: Thu, 9 Oct 2025 09:12:14 -0700
Subject: [PATCH 05/19] Update
 saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs

Co-authored-by: Ryan Scott <rscott@galois.com>
---
 saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs b/saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs
index 19d2e951f7..f60bc8c4db 100644
--- a/saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs
+++ b/saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs
@@ -89,7 +89,7 @@ resolveTerm sym unint bt rr tm =
                     | Just Refl <- testEquality bt ty -> pure y
                     | otherwise -> typeError (show ty)
                     where ty = W4.exprType y
-                  _ -> fail ("resolveTem: unexpected w4Eval result " ++ show p)
+                  _ -> fail ("resolveTerm: unexpected w4Eval result " ++ show p)
               else
                 doBind st tm'''
 

From 442ba92c4ac8c3b81afaf5a1e74751c1eeba583d Mon Sep 17 00:00:00 2001
From: "Iavor S. Diatchki" <iavor.diatchki@gmail.com>
Date: Thu, 9 Oct 2025 09:14:12 -0700
Subject: [PATCH 06/19] Update
 saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs

Co-authored-by: Ryan Scott <rscott@galois.com>
---
 saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs b/saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs
index f60bc8c4db..85bab48cee 100644
--- a/saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs
+++ b/saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs
@@ -117,7 +117,7 @@ resolveTerm sym unint bt rr tm =
             , tIsBit el, Just i <- tIsNum n, W4.BaseBVRepr w <- bt
             , intValue w == i -> pure ()
             | otherwise -> typeError (show (PP.pp ty)) :: IO ()
-          Nothing -> fail "Expected monomorphic Cryptol type, got polymorphic or unrecognized type"
+          Nothing -> fail "resolveTerm: Expected monomorphic Cryptol type, got polymorphic or unrecognized type"
 
       bindSAWTerm sym st bt te
 

From 9615c4e818de9c11bdc1477b27b37ffe18040393 Mon Sep 17 00:00:00 2001
From: "Iavor S. Diatchki" <diatchki@galois.com>
Date: Thu, 9 Oct 2025 09:16:37 -0700
Subject: [PATCH 07/19] Document function precondition

---
 .../src/SAWCentral/Crucible/Common/ResolveSetupValue.hs        | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs b/saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs
index 85bab48cee..d8b4d9ff39 100644
--- a/saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs
+++ b/saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs
@@ -54,6 +54,9 @@ noResolveRewrite :: ResolveRewrite
 noResolveRewrite = ResolveRewrite { rrBasicSS = Nothing, rrWhat4Eval = False }
 
 -- Convert a term to a What4 expression, trying to simplify it in the process.
+-- Currently this expects the terms to be wither boolean or bit-vectors, as
+-- that's all we use it for.   It should be fairly straightforward to generalize
+-- if need be.
 resolveTerm ::
   Sym {- ^ Backend state -} ->
   Set VarIndex {- ^ Keep these opaque -} ->

From d292b8fe70fa2fe242c75e9b7dbe947a6d748973 Mon Sep 17 00:00:00 2001
From: "Iavor S. Diatchki" <diatchki@galois.com>
Date: Thu, 9 Oct 2025 11:17:59 -0700
Subject: [PATCH 08/19] Make the `*_unint` functions take `[String]` instead of
 `Term`

---
 .../Crucible/Common/Setup/Builtins.hs         | 19 ++++++++++---------
 .../src/SAWCentral/Crucible/JVM/Builtins.hs   |  2 +-
 .../src/SAWCentral/Crucible/LLVM/Builtins.hs  |  2 +-
 .../src/SAWCentral/Crucible/MIR/Builtins.hs   |  2 +-
 saw-central/src/SAWCentral/Value.hs           |  4 ++++
 saw-script/src/SAWScript/Interpreter.hs       | 18 ++++++------------
 6 files changed, 23 insertions(+), 24 deletions(-)

diff --git a/saw-central/src/SAWCentral/Crucible/Common/Setup/Builtins.hs b/saw-central/src/SAWCentral/Crucible/Common/Setup/Builtins.hs
index 66a99fd03a..fc9b960379 100644
--- a/saw-central/src/SAWCentral/Crucible/Common/Setup/Builtins.hs
+++ b/saw-central/src/SAWCentral/Crucible/Common/Setup/Builtins.hs
@@ -25,17 +25,19 @@ import           Control.Monad (when)
 import           Control.Monad.State (get)
 import qualified Data.Map as Map
 import           Data.Set(Set)
+import qualified Data.Set as Set
+import           Data.Text(Text)
 
 import qualified What4.ProgramLoc as W4
 
-import           SAWCore.Recognizer(asConstant)
-import           SAWCore.Name(VarIndex, nameIndex)
-import           CryptolSAWCore.TypedTerm (TypedTerm, ttTerm)
+import           SAWCore.Name(VarIndex)
+import           CryptolSAWCore.TypedTerm (TypedTerm)
 
 import           SAWCentral.Value
 
 import qualified SAWCentral.Crucible.Common.MethodSpec as MS
 import           SAWCentral.Crucible.Common.Setup.Type
+import           SAWCentral.Builtins(resolveNames)
 
 --------------------------------------------------------------------------------
 -- ** Builtins
@@ -46,19 +48,18 @@ import           SAWCentral.Crucible.Common.Setup.Type
 declare_unint ::
   String {- ^ Name of command for error messages -} ->
   Setter' (MS.CrucibleContext ext) (Set VarIndex) {-^ Keep uninterpreted names here -} ->
-  TypedTerm {- ^ Term corresponding to the name -} ->
+  [Text] {- ^ Names for the things to be left uninterpreted -} ->
   CrucibleSetup ext ()
-declare_unint cmd unintF term =
+declare_unint cmd unintF names = 
   do
     prePost <- use csPrePost
     case prePost of
       MS.PreState ->
-        case asConstant (ttTerm term) of
-          Nothing -> fail ("The argument to `" ++ cmd ++ "` should be a name.")
-          Just n  -> csCrucibleContext . unintF . contains (nameIndex n) .= True
+        do
+          ns <- crucibleSetupTopLevel (resolveNames names)
+          csCrucibleContext . unintF %= Set.union ns
       MS.PostState ->
         fail ("`" ++ cmd ++ "` works only in the pre-condition of a specification.")
-     
 
 crucible_precond ::
   W4.ProgramLoc ->
diff --git a/saw-central/src/SAWCentral/Crucible/JVM/Builtins.hs b/saw-central/src/SAWCentral/Crucible/JVM/Builtins.hs
index 4621260904..d0a7bea38b 100644
--- a/saw-central/src/SAWCentral/Crucible/JVM/Builtins.hs
+++ b/saw-central/src/SAWCentral/Crucible/JVM/Builtins.hs
@@ -1477,7 +1477,7 @@ jvm_equal val1 val2 =
        ]
      Setup.crucible_equal loc val1 val2
 
-jvm_unint :: TypedTerm -> JVMSetupM ()
+jvm_unint :: [Text] -> JVMSetupM ()
 jvm_unint term = JVMSetupM (Setup.declare_unint "jvm_unint" jccUninterp term)
 
 --------------------------------------------------------------------------------
diff --git a/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs b/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs
index a8c6f5686a..596cad1476 100644
--- a/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs
+++ b/saw-central/src/SAWCentral/Crucible/LLVM/Builtins.hs
@@ -2010,7 +2010,7 @@ llvm_postcond term =
   do loc <- getW4Position "llvm_postcond"
      Setup.crucible_postcond loc term
 
-llvm_unint :: TypedTerm -> LLVMCrucibleSetupM ()
+llvm_unint :: [Text] -> LLVMCrucibleSetupM ()
 llvm_unint term =
   LLVMCrucibleSetupM (Setup.declare_unint "llvm_unint" ccUninterp term)
           
diff --git a/saw-central/src/SAWCentral/Crucible/MIR/Builtins.hs b/saw-central/src/SAWCentral/Crucible/MIR/Builtins.hs
index 9f15581dcf..2abad13b96 100644
--- a/saw-central/src/SAWCentral/Crucible/MIR/Builtins.hs
+++ b/saw-central/src/SAWCentral/Crucible/MIR/Builtins.hs
@@ -788,7 +788,7 @@ mir_points_to_internal mode ref val =
            , "  Value type:    " ++ show (PP.pretty valTy)
            ]
 
-mir_unint :: TypedTerm -> MIRSetupM ()
+mir_unint :: [Text] -> MIRSetupM ()
 mir_unint term = MIRSetupM (Setup.declare_unint "mir_unint" mccUninterp term)
 
 -- | Perform a set of validity checks on the LHS reference or pointer value in a
diff --git a/saw-central/src/SAWCentral/Value.hs b/saw-central/src/SAWCentral/Value.hs
index 2beb60f9e6..2090b76b59 100644
--- a/saw-central/src/SAWCentral/Value.hs
+++ b/saw-central/src/SAWCentral/Value.hs
@@ -176,6 +176,7 @@ module SAWCentral.Value (
     llvmTopLevel,
     jvmTopLevel,
     mirTopLevel,
+    crucibleSetupTopLevel,
     -- used in SAWScript.Interpreter
     -- XXX: probably belongs in SAWSupport
     underStateT,
@@ -1288,6 +1289,9 @@ runProofScript (ProofScript m) concl gl ploc rsn recordThm useSequentGoals =
             pure thmResult
 
 
+crucibleSetupTopLevel :: TopLevel a -> CrucibleSetup ext a
+crucibleSetupTopLevel m = lift (lift m)
+
 scriptTopLevel :: TopLevel a -> ProofScript a
 scriptTopLevel m = ProofScript (lift (lift m))
 
diff --git a/saw-script/src/SAWScript/Interpreter.hs b/saw-script/src/SAWScript/Interpreter.hs
index 7db7200b70..0b248bad50 100644
--- a/saw-script/src/SAWScript/Interpreter.hs
+++ b/saw-script/src/SAWScript/Interpreter.hs
@@ -4979,26 +4979,20 @@ primitives = Map.fromList
     Current
     [ "Legacy alternative name for `llvm_execute_func`." ]
 
-  , prim "llvm_unint" "Term -> LLVMSetup ()"
+  , prim "llvm_unint" "[String] -> LLVMSetup ()"
     (pureVal llvm_unint)
     Current
-    [ "Keep the given name opaque during symbolic simulation."
-    , "The input term should be a name."
-    ]
+    [ "Keep the given names opaque during symbolic simulation." ]
 
-  , prim "jvm_unint" "Term -> JVMSetup ()"
+  , prim "jvm_unint" "[String] -> JVMSetup ()"
     (pureVal jvm_unint)
     Current
-    [ "Keep the given name opaque during symbolic simulation."
-    , "The input term should be a name."
-    ] 
+    [ "Keep the given names opaque during symbolic simulation." ] 
 
-  , prim "mir_unint" "Term -> MIRSetup ()"
+  , prim "mir_unint" "[String] -> MIRSetup ()"
     (pureVal mir_unint)
     Current
-    [ "Keep the given name opaque during symbolic simulation."
-    , "The input term should be a name."
-    ] 
+    [ "Keep the given names opaque during symbolic simulation." ] 
 
   , prim "llvm_return" "SetupValue -> LLVMSetup ()"
     (pureVal llvm_return)

From 75805bcc2182a67bdc97d4347a7ae1cbf5485e81 Mon Sep 17 00:00:00 2001
From: "Iavor S. Diatchki" <diatchki@galois.com>
Date: Thu, 9 Oct 2025 13:37:09 -0700
Subject: [PATCH 09/19] Check types early.  Fix up error message

---
 .../Crucible/Common/ResolveSetupValue.hs      | 25 +++++++++++--------
 1 file changed, 14 insertions(+), 11 deletions(-)

diff --git a/saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs b/saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs
index d8b4d9ff39..9e38ca24a7 100644
--- a/saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs
+++ b/saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs
@@ -36,7 +36,7 @@ import qualified CryptolSAWCore.Simpset as Cryptol
 import SAWCoreWhat4.What4(w4EvalAny, valueToSymExpr)
 
 import Cryptol.TypeCheck.Type (tIsBit, tIsSeq, tIsNum)
-import CryptolSAWCore.TypedTerm (mkTypedTerm, ttType, ttIsMono)
+import CryptolSAWCore.TypedTerm (mkTypedTerm, ttType, ttIsMono, ppTypedTermType)
 import qualified Cryptol.Utils.PP as PP
 
 
@@ -67,6 +67,7 @@ resolveTerm ::
 resolveTerm sym unint bt rr tm =
   do
     st       <- sawCoreState sym
+    checkType st
     tm'      <- basicRewrite st tm
     case () of
       _ | isConstFoldTerm unint tm' ->
@@ -94,10 +95,10 @@ resolveTerm sym unint bt rr tm =
                     where ty = W4.exprType y
                   _ -> fail ("resolveTerm: unexpected w4Eval result " ++ show p)
               else
-                doBind st tm'''
+                bindSAWTerm sym st bt tm'''
 
           -- Just bind the term
-        | otherwise -> doBind st tm'
+        | otherwise -> bindSAWTerm sym st bt tm'
 
   where
   basicRewrite st =
@@ -110,24 +111,26 @@ resolveTerm sym unint bt rr tm =
       ModuleIdentifier ident -> identModule ident == preludeName
       _ -> False
 
-  doBind st te =
+  checkType st =
     do
-      tt <- mkTypedTerm (saw_ctx st) tm
-      case ttIsMono (ttType tt) of
+      sc <- ttType <$> mkTypedTerm (saw_ctx st) tm
+      case ttIsMono sc of
           Just ty
             | tIsBit ty, W4.BaseBoolRepr <- bt -> pure ()
             | Just (n,el) <- (tIsSeq ty)
             , tIsBit el, Just i <- tIsNum n, W4.BaseBVRepr w <- bt
             , intValue w == i -> pure ()
             | otherwise -> typeError (show (PP.pp ty)) :: IO ()
-          Nothing -> fail "resolveTerm: Expected monomorphic Cryptol type, got polymorphic or unrecognized type"
-
-      bindSAWTerm sym st bt te
+          Nothing -> typeError (show (ppTypedTermType sc))
 
   typeError :: String -> IO a
   typeError t = fail $ unlines [
-    "Expected type: " ++ show bt,
-    "Actual type: " ++ t
+    "Expected type: " ++ (
+      case bt of
+        BaseBoolRepr  -> "Bit"
+        BaseBVRepr w  -> "[" ++ show w ++ "]"
+        _             -> show bt),
+    "Actual type:   " ++ t
     ]
 
 -- 'resolveTerm' specialized to booleans.

From b418141fab0bfb8a8b3bcf2cefd0321932533148 Mon Sep 17 00:00:00 2001
From: "Iavor S. Diatchki" <diatchki@galois.com>
Date: Thu, 9 Oct 2025 14:12:26 -0700
Subject: [PATCH 10/19] Make it build

---
 .../src/SAWCentral/Crucible/Common/ResolveSetupValue.hs       | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs b/saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs
index 9e38ca24a7..a63ea2952f 100644
--- a/saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs
+++ b/saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs
@@ -127,8 +127,8 @@ resolveTerm sym unint bt rr tm =
   typeError t = fail $ unlines [
     "Expected type: " ++ (
       case bt of
-        BaseBoolRepr  -> "Bit"
-        BaseBVRepr w  -> "[" ++ show w ++ "]"
+        W4.BaseBoolRepr  -> "Bit"
+        W4.BaseBVRepr w  -> "[" ++ show w ++ "]"
         _             -> show bt),
     "Actual type:   " ++ t
     ]

From 9ef43918b5948edcfceafb1d15e1165eba8950d8 Mon Sep 17 00:00:00 2001
From: "Iavor S. Diatchki" <diatchki@galois.com>
Date: Thu, 9 Oct 2025 14:15:14 -0700
Subject: [PATCH 11/19] Reuse `crucibleSetupTopLevel`

---
 saw-central/src/SAWCentral/Value.hs | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/saw-central/src/SAWCentral/Value.hs b/saw-central/src/SAWCentral/Value.hs
index 2090b76b59..d4f0c52570 100644
--- a/saw-central/src/SAWCentral/Value.hs
+++ b/saw-central/src/SAWCentral/Value.hs
@@ -1296,13 +1296,13 @@ scriptTopLevel :: TopLevel a -> ProofScript a
 scriptTopLevel m = ProofScript (lift (lift m))
 
 llvmTopLevel :: TopLevel a -> LLVMCrucibleSetupM a
-llvmTopLevel m = LLVMCrucibleSetupM (lift (lift m))
+llvmTopLevel m = LLVMCrucibleSetupM (crucibleSetupTopLevel m)
 
 jvmTopLevel :: TopLevel a -> JVMSetupM a
-jvmTopLevel m = JVMSetupM (lift (lift m))
+jvmTopLevel m = JVMSetupM (crucibleSetupTopLevel m)
 
 mirTopLevel :: TopLevel a -> MIRSetupM a
-mirTopLevel m = MIRSetupM (lift (lift m))
+mirTopLevel m = MIRSetupM (crucibleSetupTopLevel m)
 
 instance MonadIO ProofScript where
   liftIO m = ProofScript (liftIO m)

From b2decc892e5f9ecda2f253ad2e2c15a148b6d1b6 Mon Sep 17 00:00:00 2001
From: "Iavor S. Diatchki" <diatchki@galois.com>
Date: Thu, 9 Oct 2025 14:15:57 -0700
Subject: [PATCH 12/19] Fix typo

---
 saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs b/saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs
index a63ea2952f..61f503ef58 100644
--- a/saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs
+++ b/saw-central/src/SAWCentral/Crucible/Common/ResolveSetupValue.hs
@@ -54,7 +54,7 @@ noResolveRewrite :: ResolveRewrite
 noResolveRewrite = ResolveRewrite { rrBasicSS = Nothing, rrWhat4Eval = False }
 
 -- Convert a term to a What4 expression, trying to simplify it in the process.
--- Currently this expects the terms to be wither boolean or bit-vectors, as
+-- Currently this expects the terms to be either boolean or bit-vectors, as
 -- that's all we use it for.   It should be fairly straightforward to generalize
 -- if need be.
 resolveTerm ::

From 44668293f8d7ba12f0465c2d51df909b75db95ff Mon Sep 17 00:00:00 2001
From: "Iavor S. Diatchki" <diatchki@galois.com>
Date: Thu, 9 Oct 2025 14:28:32 -0700
Subject: [PATCH 13/19] Update CHANGES

---
 CHANGES.md | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/CHANGES.md b/CHANGES.md
index cb39d493b6..9f72af1339 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -86,6 +86,10 @@ This release supports [version
 
 ## New Features
 
+* We have new commands `llvm_unit: [String] -> LLVMSetup ()` and
+  and analagous commands for JVM and MIR, which can be used to declare that some
+  Cryptol names should be kept opaque during symbolic simulation.
+
 * The Cryptol import syntax has been extended.
   - You can now import Cryptol module names, including qualified module
     names (which are resolved via the Cryptol load path) as well as

From 2a41a1e1066435475e98cb79c81cf8382038d782 Mon Sep 17 00:00:00 2001
From: "Iavor S. Diatchki" <diatchki@galois.com>
Date: Thu, 9 Oct 2025 14:36:35 -0700
Subject: [PATCH 14/19] Add a test case for 2674

---
 intTests/test2674/Example.cry |   7 +++++++
 intTests/test2674/example.bc  | Bin 0 -> 2672 bytes
 intTests/test2674/example.c   |   2 ++
 intTests/test2674/test.saw    |  35 ++++++++++++++++++++++++++++++++++
 intTests/test2674/test.sh     |   2 ++
 5 files changed, 46 insertions(+)
 create mode 100644 intTests/test2674/Example.cry
 create mode 100644 intTests/test2674/example.bc
 create mode 100644 intTests/test2674/example.c
 create mode 100644 intTests/test2674/test.saw
 create mode 100644 intTests/test2674/test.sh

diff --git a/intTests/test2674/Example.cry b/intTests/test2674/Example.cry
new file mode 100644
index 0000000000..c30e27da30
--- /dev/null
+++ b/intTests/test2674/Example.cry
@@ -0,0 +1,7 @@
+module Example where
+
+cry_ID : [8] -> [8]
+cry_ID x = x
+
+cry_FIVE : [8] -> [8]
+cry_FIVE y = cry_ID 5 + y
diff --git a/intTests/test2674/example.bc b/intTests/test2674/example.bc
new file mode 100644
index 0000000000000000000000000000000000000000..19b4c962908cbb80047a40611a196dde4528c462
GIT binary patch
literal 2672
zcmYjTe@q+K9e;<xXTY3ILKj=PyW9m5xl&<=$%q|;W@DN<DwCWas+g1s9|TIakQhUZ
z?XK$?lOA2&$wX|js!X!mZ0i1V*8Gt_(h1wlajBKjtV*p6A-gfeiD-gWwnbW{?fdLx
z-P65apZ9&=`@Zk5_tuy8G$JT1P){`=^dBgF_NDb706+pZtQOjS{hQza?q6TN^~qna
zzxD5nPrm$Ndp}{UgEd}_(2r^mYOLWAbVv`C47M)VvbD#QTBG?gF{eIIr_!^v?+#1q
zmuvbiH};*;8e2>%-Kz~o<GjPY%(wRMlEYft<(e~D)wLGResrGulrS3S2C2vb-yez3
zeo&)Nlb^kyH-^Ipw9Jv|EJE*a2*Iz>{;^u^ANyuM)t-PRGMREZ8tM<)Gj)B&gDUF%
zR_iY#>e^hhWNUEO0yRR%bqKu={a)|Er}&(N8`T>W*2Waa<!o#!&aA|n3Pt8lk}1dO
z65*C-+;X=|_Nd4yq?+-`-7(UyB7KrP?Utv;LtYgbu#ys6inA*OSFo|`HX1l=2HBKI
z-zA=28q$%|gR(y+Uwm2zO#C-sBPm76fJ&Yml)EL;?;`^Sc`_!?MC5L*91zGU1L+?R
z`5ok&1`=t|ESs{ix8rm<-jpHOM+E*m={3mR<FW~<0>INGdt!38fQ1ZvMEVV~AKm5X
z6_L%mno>cgoMd)HdMns;*GiXp2EdF+X9>ItgF8Wb8<t%3dYmZ)ne8O=C|;qlu^GT6
zAi$K_B2y;VQjy65xJ2i9`gVmZN3i!ex)f)&2n~?I^s6N*2TK*QLXchOnY9XsT%64Z
znJNKLej&1%BD0pn%=03<g6WwRKwyBt5Nw&iVidp%N&4P%ycDOiHnw`S5>Iaev6Th2
zU{S4Xwj$D|jfRbz1e3B+&jw<302@J6*u|E3CR34WQ)HJ#ECa~D#!)FO2D`n~RN^ob
z47$Dp%l`vo&%p`;>b-{r*q5>GlbYrrViHMRjnslV(J}Bh92dLaw(1V5QfPO=9g)2W
z#gXxlTOxhnS=fo>NuTUrBFzcKVF|ua)0mT*Sfv8n)I@~xTFHQmoL*Hv)RG>F3{={Q
z0yV`w!#}Pfu7<|~>4`O`BK4C*?qltrgsU|w0!i@qYLU>}r{;Ksw9f&gm6nyk4^D!B
zKjsip0d8cYT7C0CBwT;+l}xRDxY>DY*CA=J=8{vpfwx_Q^Q58gQc3i3ksfOydgtw?
zxpcU%;>uIeN%bbue66K+B&ti@$EK1D`0kicS0M}S%_(}b_TI3fH|GmOB)kFc>yX`U
zGT>HteX^UA^|@whD?$|o&3Qp{f1BENQeE0*W}OG0V^ShJCcI<08M3U}&DRw@H$y#h
z3QKOg#p@#97$*;pgF4B>k_<X_yC6tN@6$S9J0r<MpktlviOT+H@TJGw)Z+s6k0okL
zPz-0m!{T(V(yod03QsQwnH5oaH)1zu?dE8uy^%I8+D-Ec%VPTb@Y8Q+Eng@siM0CG
zS=l`(d)%Svacs<Koje_r^|w!I9wW`)om448-M4Cr9JK|f;0)N^A(-#*G=#)jfrfB;
zM6hGJ<EDiD$d!;K=WKg+5SKjTBYn~113M87)&Toc?7I-X>q+Jp5QiWz&uojzQ<p-f
zT-uVb_ku#cP4$%QmU)<_!+&molgcw74<rQx>4^qU-`7%GOVoyw`bKC?-myV2@5vXL
zbr8Uzw<JQn*F$^f(x$N8oJ;rINSd>0IAc%FaeY!nf>e{0gr)ymhT3vzzAh-YIn9Qk
z+2Az)bW-QF)O~@1={E)C!va-uQcs1}ueL-QvQNIaXNzYxd1jesz=CCd-x&8>%T0Ul
z4TX6zWX=uV1na|LA&~_fINRz!dq6!AG{pk-(5iVDgTJH+#neY6oMk8qu7Wi@y$Yrb
z&e_a`G^nl@ES0k^#~^nzI0Yx^v9=L`Dq{O;fXRkn=R+5D<dj1mipf8hVDGg>q9>g0
zSxlQ&?MJ|!a-cD_gMXn<WI@#1N#;bbWo+PefqKGeo)nZ%oSGfXirOeBH#tpl6%PBM
zHRK(~mjUu~2$>-!JgkGW&#U$I9;1V64TcvMKJSld4QF~fjeWn0@E?wIW%TZ4`n|nC
zd$Rvk?zK_R)Y%K?XGX?F&(PG_z^L<>of{bSj-I<XGc69E8y)kA6Qk|!3un(yk9urw
z_qkDS<eYf^b<SJe$#ov?5IO|TP(j-}4+}y^S4XG0qw~d9)toTvRJW>XJ7=veFoTZn
zQokbQgtl2@I-$O$R@mFR)B_7St<JbB8Vl$1TlY@iThBhqubj^1Q@1ydz8KB;W2Y+k
zo$Sh5`Dp!q^aqIlc96fZ!DE29A_If&DA*F4!MvKD-J~<|rZQZlNo?|}zkct~eHZn>
z31Ofq;b71_a8f%7DTr?>9Hl-PJPiBjp!-VNbe*tV4fQUjYkr0=nYALl2G@&-+j8Yn
zU4<K<>R4iu(CmOQz%~-qIA1kz-Cs;#&O8Kd8r;hQ-VC`WtFVB`=yOPXO6bX4&()CS
z3IwyFHx}xFz>cH|z(o!r{HEDmn;hu3YU9E=Yi%ELMwVa^uQgTHY%k&biRl+lKpt!+
zY;&mu(X1wfVW)~yDO3B;EX8<Up`-}a8EpaRCOL!@&>Jc3{yFqXt<E|CGlWLr0doNQ
zU5Z5m=7(wE`Bjk-Q($ZmDlWLk_sBe+K*2JADUbnbJ=E&!=DT%(D)hMTgo@9F3#P;G
z9@K_VH;nQ74r5p^&v6){pMY$;p$FOC#PgA%WBnsTM~}Vsa@FTV&qVj3b`kqz`-C`h
cVajLh#=bb}6DI)c7#YGlput-(ga0f41v##rm;e9(

literal 0
HcmV?d00001

diff --git a/intTests/test2674/example.c b/intTests/test2674/example.c
new file mode 100644
index 0000000000..8f33d7fefe
--- /dev/null
+++ b/intTests/test2674/example.c
@@ -0,0 +1,2 @@
+unsigned char c_ID(unsigned char x) { return x; }
+unsigned char c_FIVE(unsigned char y) { return c_ID(5)+y; }
diff --git a/intTests/test2674/test.saw b/intTests/test2674/test.saw
new file mode 100644
index 0000000000..b6867f9831
--- /dev/null
+++ b/intTests/test2674/test.saw
@@ -0,0 +1,35 @@
+m <- llvm_load_module "example.bc";
+
+import "Example.cry";
+
+thm_id <- llvm_verify
+  m "c_ID" [] false
+  do {
+    X <- llvm_fresh_var "X" (llvm_int 8);
+    llvm_execute_func [llvm_term X];
+    llvm_return (llvm_term {{ cry_ID X }} );
+  }
+  rme;
+
+fails (llvm_verify
+  m "c_FIVE" [thm_id] false
+  do {
+    Y <- llvm_fresh_var "Y" (llvm_int 8);
+    llvm_execute_func [llvm_term Y];
+    llvm_return (llvm_term {{ cry_FIVE Y }});
+  }
+  do {
+    w4_unint_rme ["cry_ID"];
+  });
+
+thm_five <- llvm_verify
+  m "c_FIVE" [thm_id] false
+  do {
+    llvm_unint ["cry_ID"];
+    Y <- llvm_fresh_var "Y" (llvm_int 8);
+    llvm_execute_func [llvm_term Y];
+    llvm_return (llvm_term {{ cry_FIVE Y }});
+  }
+  do {
+    w4_unint_rme ["cry_ID"];
+  };
\ No newline at end of file
diff --git a/intTests/test2674/test.sh b/intTests/test2674/test.sh
new file mode 100644
index 0000000000..1ceccb9b79
--- /dev/null
+++ b/intTests/test2674/test.sh
@@ -0,0 +1,2 @@
+set -e
+$SAW test.saw
\ No newline at end of file

From 03cca1b87f552c2d6a83e7a28682026f085db17c Mon Sep 17 00:00:00 2001
From: "Iavor S. Diatchki" <diatchki@galois.com>
Date: Thu, 9 Oct 2025 15:22:55 -0700
Subject: [PATCH 15/19] Fix tests

---
 intTests/test_search/search00.log.good | 1 +
 intTests/test_search/search01.log.good | 1 +
 2 files changed, 2 insertions(+)

diff --git a/intTests/test_search/search00.log.good b/intTests/test_search/search00.log.good
index f0013799fc..8b31f7b5ff 100644
--- a/intTests/test_search/search00.log.good
+++ b/intTests/test_search/search00.log.good
@@ -42,6 +42,7 @@ llvm_points_to_untyped : SetupValue -> SetupValue -> LLVMSetup ()
 llvm_postcond : Term -> LLVMSetup ()
 llvm_precond : Term -> LLVMSetup ()
 llvm_return : SetupValue -> LLVMSetup ()
+llvm_unint : [String] -> LLVMSetup ()
 llvm_unsafe_assume_spec : LLVMModule -> String -> LLVMSetup () -> TopLevel LLVMSpec
 llvm_verify : LLVMModule -> String -> [LLVMSpec] -> Bool -> LLVMSetup () -> ProofScript () -> TopLevel LLVMSpec
 19 more matches tagged experimental; use enable_experimental to see them
diff --git a/intTests/test_search/search01.log.good b/intTests/test_search/search01.log.good
index 8e46f926f7..e8e0ba60d7 100644
--- a/intTests/test_search/search01.log.good
+++ b/intTests/test_search/search01.log.good
@@ -27,6 +27,7 @@ jvm_postcond : Term -> JVMSetup ()
 jvm_precond : Term -> JVMSetup ()
 jvm_return : JVMValue -> JVMSetup ()
 jvm_static_field_is : String -> JVMValue -> JVMSetup ()
+jvm_unint : [String] -> JVMSetup ()
 jvm_unsafe_assume_spec : JavaClass -> String -> JVMSetup () -> TopLevel JVMSpec
 jvm_verify : JavaClass -> String -> [JVMSpec] -> Bool -> JVMSetup () -> ProofScript () -> TopLevel JVMSpec
 2 more matches tagged experimental; use enable_experimental to see them

From 7ec95c1ebfca128d030348d3d28d2a7e9a569d39 Mon Sep 17 00:00:00 2001
From: "Iavor S. Diatchki" <diatchki@galois.com>
Date: Fri, 10 Oct 2025 09:03:42 -0700
Subject: [PATCH 16/19] Typos

---
 CHANGES.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/CHANGES.md b/CHANGES.md
index 9f72af1339..ef09c72007 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -86,8 +86,8 @@ This release supports [version
 
 ## New Features
 
-* We have new commands `llvm_unit: [String] -> LLVMSetup ()` and
-  and analagous commands for JVM and MIR, which can be used to declare that some
+* SAW new commands `llvm_unint: [String] -> LLVMSetup ()` and
+  and analogous commands for JVM and MIR, which can be used to declare that some
   Cryptol names should be kept opaque during symbolic simulation.
 
 * The Cryptol import syntax has been extended.

From 3e88aeb6a831b7cf7cf1724b1663d33b1448b594 Mon Sep 17 00:00:00 2001
From: "Iavor S. Diatchki" <diatchki@galois.com>
Date: Fri, 10 Oct 2025 09:04:26 -0700
Subject: [PATCH 17/19] Update help for `*_unint` commands

---
 saw-script/src/SAWScript/Interpreter.hs | 32 ++++++++++++++-----------
 1 file changed, 18 insertions(+), 14 deletions(-)

diff --git a/saw-script/src/SAWScript/Interpreter.hs b/saw-script/src/SAWScript/Interpreter.hs
index 0b248bad50..2d966ea29a 100644
--- a/saw-script/src/SAWScript/Interpreter.hs
+++ b/saw-script/src/SAWScript/Interpreter.hs
@@ -2402,7 +2402,7 @@ primTypes = Map.fromList
 
 
 primitives :: Map SS.LName Primitive
-primitives = Map.fromList
+primitives = Map.fromList $
   [ prim "return"              "{m, a} a -> m a"
     (pureVal (\v -> VReturn atRestPos [] v))
     Current
@@ -4978,23 +4978,27 @@ primitives = Map.fromList
     (pureVal llvm_execute_func)
     Current
     [ "Legacy alternative name for `llvm_execute_func`." ]
-
-  , prim "llvm_unint" "[String] -> LLVMSetup ()"
-    (pureVal llvm_unint)
-    Current
-    [ "Keep the given names opaque during symbolic simulation." ]
+  ] ++
+    let unint_help =
+         [ "Keep the given Cryptol/SAWCore names opaque during symbolic simulation."
+         , "The command should be used before symbolic execution begins"
+         , "(i.e., in the pre-condition of the specification)."
+         , "This command does not affect the ProofScript---to keep names"
+         , "opaque while discharging goals, you still need to provide them"
+         , "as explicit arguments to the relevant proof tactics."
+         ]
+    in
+  [ prim "llvm_unint" "[String] -> LLVMSetup ()"
+    (pureVal llvm_unint) Current unint_help
 
   , prim "jvm_unint" "[String] -> JVMSetup ()"
-    (pureVal jvm_unint)
-    Current
-    [ "Keep the given names opaque during symbolic simulation." ] 
+    (pureVal jvm_unint) Current unint_help
 
   , prim "mir_unint" "[String] -> MIRSetup ()"
-    (pureVal mir_unint)
-    Current
-    [ "Keep the given names opaque during symbolic simulation." ] 
-
-  , prim "llvm_return" "SetupValue -> LLVMSetup ()"
+    (pureVal mir_unint) Current unint_help
+  ]
+  ++
+  [ prim "llvm_return" "SetupValue -> LLVMSetup ()"
     (pureVal llvm_return)
     Current
     [ "Specify the given value as the return value of the function. A"

From eae0ed9293e69ca2e370514a1cfef80d97dc1d40 Mon Sep 17 00:00:00 2001
From: "Iavor S. Diatchki" <diatchki@galois.com>
Date: Fri, 10 Oct 2025 09:06:56 -0700
Subject: [PATCH 18/19] Test for no `*_uninterp` in post-condition

---
 intTests/test2674/test.saw | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/intTests/test2674/test.saw b/intTests/test2674/test.saw
index b6867f9831..5603c6b669 100644
--- a/intTests/test2674/test.saw
+++ b/intTests/test2674/test.saw
@@ -22,6 +22,19 @@ fails (llvm_verify
     w4_unint_rme ["cry_ID"];
   });
 
+
+fails (llvm_verify
+  m "c_FIVE" [thm_id] false
+  do {
+    Y <- llvm_fresh_var "Y" (llvm_int 8);
+    llvm_execute_func [llvm_term Y];
+    llvm_unint ["cry_ID"];
+    llvm_return (llvm_term {{ cry_FIVE Y }});
+  }
+  do {
+    w4_unint_rme [];
+  });
+
 thm_five <- llvm_verify
   m "c_FIVE" [thm_id] false
   do {

From 073c51b16004961b007dfb6c5726b60dca37cc00 Mon Sep 17 00:00:00 2001
From: "Iavor S. Diatchki" <iavor.diatchki@gmail.com>
Date: Fri, 10 Oct 2025 09:32:17 -0700
Subject: [PATCH 19/19] Update CHANGES.md

Co-authored-by: Ryan Scott <rscott@galois.com>
---
 CHANGES.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CHANGES.md b/CHANGES.md
index ef09c72007..360e03309e 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -86,7 +86,7 @@ This release supports [version
 
 ## New Features
 
-* SAW new commands `llvm_unint: [String] -> LLVMSetup ()` and
+* SAW has new commands `llvm_unint: [String] -> LLVMSetup ()` and
   and analogous commands for JVM and MIR, which can be used to declare that some
   Cryptol names should be kept opaque during symbolic simulation.