diff --git a/deps/saw-core b/deps/saw-core
index c8316b86c3..fd9df6c4bb 160000
--- a/deps/saw-core
+++ b/deps/saw-core
@@ -1 +1 @@
-Subproject commit c8316b86c384e45a592ae866ed5a2186a92fd137
+Subproject commit fd9df6c4bb45371c89ff2f4466deae47f100ce16
diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
index 57b6972925..535eec3959 100644
--- a/src/SAWScript/Builtins.hs
+++ b/src/SAWScript/Builtins.hs
@@ -1127,6 +1127,15 @@ beta_reduce_term (TypedTerm schema t) = do
   t' <- io $ betaNormalize sc t
   return (TypedTerm schema t')
 
+term_eval :: [String] -> TypedTerm -> TopLevel TypedTerm
+term_eval unints (TypedTerm schema t0) =
+  do sc <- getSharedContext
+     unintSet <- resolveNames unints
+     let gen = globalNonceGenerator
+     sym <- liftIO $ Crucible.newSAWCoreBackend FloatRealRepr sc gen
+     t1 <- liftIO $ W4Sim.w4EvalTerm sym sc Map.empty unintSet t0
+     pure (TypedTerm schema t1)
+
 addsimp :: Theorem -> Simpset -> TopLevel Simpset
 addsimp (Theorem (Prop t) _stats) ss =
   case ruleOfProp t of
diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
index 45f87bda04..9f86ae4b92 100644
--- a/src/SAWScript/Interpreter.hs
+++ b/src/SAWScript/Interpreter.hs
@@ -1566,6 +1566,17 @@ primitives = Map.fromList
     Current
     [ "Reduce the given term to beta-normal form." ]
 
+  , prim "term_eval"           "Term -> Term"
+    (funVal1 (term_eval []))
+    Current
+    [ "Evaluate the term to a first-order combination of primitives." ]
+
+  , prim "term_eval_unint"     "[String] -> Term -> Term"
+    (funVal2 term_eval)
+    Current
+    [ "Evaluate the term to a first-order combination of primitives."
+    , "Leave the given names, as defined with 'define', as uninterpreted." ]
+
   , prim "cryptol_load"        "String -> TopLevel CryptolModule"
     (pureVal (cryptol_load BS.readFile))
     Current