diff --git a/deps/crucible b/deps/crucible
index 9a5d6cc32c..ac948b4363 160000
--- a/deps/crucible
+++ b/deps/crucible
@@ -1 +1 @@
-Subproject commit 9a5d6cc32c8351722ab8b489a634b78f62337805
+Subproject commit ac948b4363745e10e2226c843339bad16bf198fa
diff --git a/deps/cryptol-specs b/deps/cryptol-specs
index 423fd3f381..4066cc0637 160000
--- a/deps/cryptol-specs
+++ b/deps/cryptol-specs
@@ -1 +1 @@
-Subproject commit 423fd3f381b3337c9d9ac52760019bf03f4314ae
+Subproject commit 4066cc0637c23c7d880dd0330c332821dc805f2c
diff --git a/deps/what4 b/deps/what4
index e46dff4209..8c9401b5d2 160000
--- a/deps/what4
+++ b/deps/what4
@@ -1 +1 @@
-Subproject commit e46dff42096550d860d210bd9cf6e435d8cd7ce5
+Subproject commit 8c9401b5d21d20451d224d4834bd611fc83b850b
diff --git a/examples/aes/aes.saw b/examples/aes/aes.saw
index 4ad6a9e578..59dd0d4fb6 100644
--- a/examples/aes/aes.saw
+++ b/examples/aes/aes.saw
@@ -5,20 +5,22 @@ print "Proving encrypt_lemma...";
 encrypt_lemma <-
   time (prove_print (unint_z3 ["AESRound"])
   (rewrite (cryptol_ss())
-  {{ \(state0 : State) (ks : [9]RoundKey) ->
+  {{ \(state0 : State) (ks : [13]RoundKey) ->
       (rounds where rounds = [state0] # [ AESRound (rk, s) | rk <- ks | s <- rounds ]) ! 0 ==
-        AESRound(ks@8,AESRound(ks@7,AESRound(ks@6,AESRound(ks@5,AESRound(ks@4,
-          AESRound(ks@3,AESRound(ks@2,AESRound(ks@1,AESRound(ks@0,state0)))))))))
+        AESRound(ks@12,AESRound(ks@11,AESRound(ks@10,AESRound(ks@9,
+          AESRound(ks@8,AESRound(ks@7,AESRound(ks@6,AESRound(ks@5,AESRound(ks@4,
+            AESRound(ks@3,AESRound(ks@2,AESRound(ks@1,AESRound(ks@0,state0)))))))))))))
   }}));
 
 print "Proving decrypt_lemma...";
 decrypt_lemma <-
   time (prove_print (unint_z3 ["AESInvRound"])
   (rewrite (cryptol_ss())
-  {{ \(state0 : State) (ks : [9]RoundKey) ->
+  {{ \(state0 : State) (ks : [13]RoundKey) ->
       (rounds where rounds = [state0] # [ AESInvRound (rk, s) | rk <- reverse ks | s <- rounds ]) ! 0 ==
         AESInvRound(ks@0,AESInvRound(ks@1,AESInvRound(ks@2,AESInvRound(ks@3,AESInvRound(ks@4,
-          AESInvRound(ks@5,AESInvRound(ks@6,AESInvRound(ks@7,AESInvRound(ks@8,state0)))))))))
+          AESInvRound(ks@5,AESInvRound(ks@6,AESInvRound(ks@7,AESInvRound(ks@8,
+            AESInvRound(ks@9,AESInvRound(ks@10,AESInvRound(ks@11,AESInvRound(ks@12,state0)))))))))))))
   }}));
 
 print "Proving msgToState_stateToMsg(rme)...";
@@ -65,7 +67,7 @@ InvMixColumns_MixColumns <-
 print "Proving aesDecrypt_aesEncrypt(rewriting)...";
 dec_enc <-
   time (prove_print do {
-    unfolding ["aesEncrypt", "aesDecrypt"];
+    unfolding ["aesEncrypt", "aesEncryptWithKeySchedule", "aesDecrypt"];
     simplify (addsimps [encrypt_lemma,
                         decrypt_lemma]
               (cryptol_ss()));
@@ -112,7 +114,7 @@ MixColumns_InvMixColumns <-
 print "Proving aesEncrypt_aesDecrypt(rewriting)...";
 enc_dec <-
   time (prove_print do {
-    unfolding ["aesEncrypt", "aesDecrypt"];
+    unfolding ["aesEncrypt", "aesEncryptWithKeySchedule", "aesDecrypt"];
     simplify (addsimps [encrypt_lemma,
                         decrypt_lemma]
               (cryptol_ss()));
diff --git a/intTests/test_smt_array_load_concrete_size/Makefile b/intTests/test_smt_array_load_concrete_size/Makefile
new file mode 100644
index 0000000000..dffb75bb76
--- /dev/null
+++ b/intTests/test_smt_array_load_concrete_size/Makefile
@@ -0,0 +1,11 @@
+CC = clang
+CFLAGS = -g -emit-llvm -frecord-command-line -O1
+
+all: test.bc
+
+test.bc: test.c
+	$(CC) $(CFLAGS) -c $< -o $@
+
+.PHONY: clean
+clean:
+	rm -f test.bc
diff --git a/intTests/test_smt_array_load_concrete_size/Mix.cry b/intTests/test_smt_array_load_concrete_size/Mix.cry
new file mode 100644
index 0000000000..2b51da1e58
--- /dev/null
+++ b/intTests/test_smt_array_load_concrete_size/Mix.cry
@@ -0,0 +1,8 @@
+module Mix where
+
+import Array
+
+type ByteArray = Array[64][8]
+
+mix : {l} (width l <= 64) => ByteArray -> [64] -> [l][8] -> ByteArray
+mix block n data = arrayCopy block n (arrayRangeUpdate (arrayConstant 0) 0 data) 0 `(l)
diff --git a/intTests/test_smt_array_load_concrete_size/test.bc b/intTests/test_smt_array_load_concrete_size/test.bc
new file mode 100644
index 0000000000..6e20929297
Binary files /dev/null and b/intTests/test_smt_array_load_concrete_size/test.bc differ
diff --git a/intTests/test_smt_array_load_concrete_size/test.c b/intTests/test_smt_array_load_concrete_size/test.c
new file mode 100644
index 0000000000..14e059ae58
--- /dev/null
+++ b/intTests/test_smt_array_load_concrete_size/test.c
@@ -0,0 +1,13 @@
+#include <stdint.h>
+#include <string.h>
+
+int mix(uint8_t block[128], uint32_t n, uint8_t *data, size_t len) {
+  size_t left = 128 - n;
+
+  if (len < left) {
+    memcpy(block + n, data, len);
+  } else {
+    memcpy(block + n, data, left);
+  }
+  return 1;
+}
diff --git a/intTests/test_smt_array_load_concrete_size/test.saw b/intTests/test_smt_array_load_concrete_size/test.saw
new file mode 100644
index 0000000000..1cf9dc6343
--- /dev/null
+++ b/intTests/test_smt_array_load_concrete_size/test.saw
@@ -0,0 +1,66 @@
+enable_experimental;
+
+import "Mix.cry";
+let arrayRangeEq = parse_core "arrayRangeEq 64 (Vec 8 Bool)";
+
+m <- llvm_load_module "test.bc";
+
+let i8 = llvm_int 8;
+let i32 = llvm_int 32;
+
+let alloc_init_readonly ty v = do {
+  p <- llvm_alloc_readonly ty;
+  llvm_points_to p v;
+  return p;
+};
+
+let ptr_to_fresh_readonly n ty = do {
+  x <- llvm_fresh_var n ty;
+  p <- alloc_init_readonly ty (llvm_term x);
+  return (x, p);
+};
+
+let mix_spec len res_block_len range_eq_len = do {
+  block <- llvm_fresh_cryptol_var "block" {| ByteArray |};
+  block_ptr <- llvm_symbolic_alloc false 1 {{ 128:[64] }};
+  llvm_points_to_array_prefix block_ptr block {{ 128:[64] }};
+
+  (data, data_ptr) <- ptr_to_fresh_readonly "data" (llvm_array len i8);
+
+  n <- llvm_fresh_var "n" i32;
+  llvm_precond({{ n < 128 }});
+
+  llvm_execute_func [block_ptr, (llvm_term n), data_ptr, (llvm_term {{ `len : [64] }})];
+
+  let res = {{ mix block (0 # n) data }};
+  res_block <- llvm_fresh_cryptol_var "res_block" {| ByteArray |};
+  llvm_points_to_array_prefix block_ptr res_block {{ `res_block_len:[64] }};
+  llvm_postcond {{ arrayRangeEq res_block 0 res 0 `range_eq_len }};
+
+  llvm_return (llvm_term {{ 1 : [32]}});
+};
+
+llvm_verify m "mix"
+  []
+  true
+  (mix_spec 1 128 128)
+  (do {
+    w4_unint_z3 [];
+  });
+
+llvm_verify m "mix"
+  []
+  true
+  (mix_spec 1 0 0)
+  (do {
+    w4_unint_z3 [];
+  });
+
+fails (llvm_verify m "mix"
+  []
+  true
+  (mix_spec 1 129 0)
+  (do {
+    w4_unint_z3 [];
+  }));
+
diff --git a/intTests/test_smt_array_load_concrete_size/test.sh b/intTests/test_smt_array_load_concrete_size/test.sh
new file mode 100755
index 0000000000..d5f2c8ea02
--- /dev/null
+++ b/intTests/test_smt_array_load_concrete_size/test.sh
@@ -0,0 +1,6 @@
+#!/usr/bin/env bash
+
+set -e
+
+$SAW test.saw
+
diff --git a/saw-remote-api/src/SAWServer.hs b/saw-remote-api/src/SAWServer.hs
index 76a5600590..41863eb001 100644
--- a/saw-remote-api/src/SAWServer.hs
+++ b/saw-remote-api/src/SAWServer.hs
@@ -270,6 +270,8 @@ initialState readFileFn =
                 , rwProofs = []
                 , rwPreservedRegs = []
                 , rwAllocSymInitCheck = True
+                , rwWhat4PushMuxOps = False
+                , rwNoSatisfyingWriteFreshConstant = True
                 , rwCrucibleTimeout = CC.defaultSAWCoreBackendTimeout
                 , rwPathSatSolver = CC.PathSat_Z3
                 , rwSkipSafetyProofs = False
diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
index f262c70629..1e5816455d 100644
--- a/src/SAWScript/Builtins.hs
+++ b/src/SAWScript/Builtins.hs
@@ -717,7 +717,8 @@ goal_eval unints =
   execTactic $ tacticChange $ \goal ->
   do sc <- getSharedContext
      unintSet <- resolveNames unints
-     sqt' <- traverseSequentWithFocus (io . evalProp sc unintSet) (goalSequent goal)
+     what4PushMuxOps <- gets rwWhat4PushMuxOps
+     sqt' <- traverseSequentWithFocus (io . evalProp sc what4PushMuxOps unintSet) (goalSequent goal)
      return (sqt', EvalEvidence unintSet)
 
 extract_uninterp ::
@@ -2097,7 +2098,8 @@ specialize_theorem thm ts =
   do sc <- getSharedContext
      db <- SV.getTheoremDB
      pos <- SV.getPosition
-     (thm', db') <- io (specializeTheorem sc db pos "specialize_theorem" thm (map ttTerm ts))
+     what4PushMuxOps <- gets rwWhat4PushMuxOps
+     (thm', db') <- io (specializeTheorem sc what4PushMuxOps db pos "specialize_theorem" thm (map ttTerm ts))
      SV.putTheoremDB db'
      SV.returnProof thm'
 
diff --git a/src/SAWScript/Crucible/Common.hs b/src/SAWScript/Crucible/Common.hs
index 4d27e816e4..6c353abae4 100644
--- a/src/SAWScript/Crucible/Common.hs
+++ b/src/SAWScript/Crucible/Common.hs
@@ -38,12 +38,14 @@ import           Lang.Crucible.Backend
 import           Lang.Crucible.Backend.Online (OnlineBackend, newOnlineBackend)
 import qualified Data.Parameterized.Nonce as Nonce
 import           What4.Protocol.Online (OnlineSolver(..))
+import qualified What4.Solver.CVC5 as CVC5
 import qualified What4.Solver.Z3 as Z3
 import qualified What4.Solver.Yices as Yices
 import qualified What4.Protocol.SMTLib2 as SMT2
 
 import qualified What4.Config as W4
 import qualified What4.Expr as W4
+import qualified What4.Expr.Builder as W4
 import qualified What4.Interface as W4
 import qualified What4.ProgramLoc as W4 (plSourceLoc)
 
@@ -67,7 +69,7 @@ type Sym = W4.ExprBuilder Nonce.GlobalNonceGenerator SAWCoreState (W4.Flags W4.F
 type Backend solver = OnlineBackend solver Nonce.GlobalNonceGenerator SAWCoreState (W4.Flags W4.FloatReal)
 
 data SomeOnlineBackend =
-  forall solver. OnlineSolver solver => 
+  forall solver. OnlineSolver solver =>
     SomeOnlineBackend (Backend solver)
 
 data SAWCruciblePersonality sym = SAWCruciblePersonality
@@ -75,10 +77,13 @@ data SAWCruciblePersonality sym = SAWCruciblePersonality
 sawCoreState :: Sym -> IO (SAWCoreState Nonce.GlobalNonceGenerator)
 sawCoreState sym = pure (sym ^. W4.userState)
 
-newSAWCoreExprBuilder :: SC.SharedContext -> IO Sym
-newSAWCoreExprBuilder sc =
+newSAWCoreExprBuilder :: SC.SharedContext -> Bool -> IO Sym
+newSAWCoreExprBuilder sc what4PushMuxOps =
   do st <- newSAWCoreState sc
-     W4.newExprBuilder W4.FloatRealRepr st Nonce.globalNonceGenerator
+     sym <- W4.newExprBuilder W4.FloatRealRepr st Nonce.globalNonceGenerator
+     pushMuxOpsSetting <- W4.getOptionSetting W4.pushMuxOpsOption $ W4.getConfiguration sym
+     _ <- W4.setOpt pushMuxOpsSetting what4PushMuxOps
+     pure sym
 
 defaultSAWCoreBackendTimeout :: Integer
 defaultSAWCoreBackendTimeout = 10000
@@ -89,7 +94,9 @@ newSAWCoreBackend pss sym = newSAWCoreBackendWithTimeout pss sym 0
 newSAWCoreBackendWithTimeout :: PathSatSolver -> Sym -> Integer -> IO SomeOnlineBackend
 newSAWCoreBackendWithTimeout PathSat_Yices sym timeout =
   do bak <- newOnlineBackend sym Yices.yicesDefaultFeatures
+     W4.extendConfig Z3.z3Options (W4.getConfiguration sym)
      W4.extendConfig Yices.yicesOptions (W4.getConfiguration sym)
+     W4.extendConfig CVC5.cvc5Options (W4.getConfiguration sym)
      yicesTimeoutSetting <- W4.getOptionSetting Yices.yicesGoalTimeout (W4.getConfiguration sym)
      _ <- W4.setOpt yicesTimeoutSetting timeout
      return (SomeOnlineBackend (bak :: Backend Yices.Connection))
@@ -97,6 +104,8 @@ newSAWCoreBackendWithTimeout PathSat_Yices sym timeout =
 newSAWCoreBackendWithTimeout PathSat_Z3 sym timeout =
   do bak <- newOnlineBackend sym (SMT2.defaultFeatures Z3.Z3)
      W4.extendConfig Z3.z3Options (W4.getConfiguration sym)
+     W4.extendConfig Yices.yicesOptions (W4.getConfiguration sym)
+     W4.extendConfig CVC5.cvc5Options (W4.getConfiguration sym)
      z3TimeoutSetting <- W4.getOptionSetting Z3.z3Timeout (W4.getConfiguration sym)
      _ <- W4.setOpt z3TimeoutSetting timeout
      return (SomeOnlineBackend (bak :: Backend (SMT2.Writer Z3.Z3)))
diff --git a/src/SAWScript/Crucible/JVM/Builtins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs
index f2a55d93b4..53d5f1c1d5 100644
--- a/src/SAWScript/Crucible/JVM/Builtins.hs
+++ b/src/SAWScript/Crucible/JVM/Builtins.hs
@@ -841,7 +841,7 @@ setupCrucibleContext jclass =
      cb <- getJavaCodebase
      sc <- getSharedContext
      pathSatSolver <- gets rwPathSatSolver
-     sym <- io $ newSAWCoreExprBuilder sc
+     sym <- io $ newSAWCoreExprBuilder sc False
      bak <- io $ newSAWCoreBackend pathSatSolver sym
      opts <- getOptions
      io $ CJ.setSimulatorVerbosity (simVerbose opts) sym
diff --git a/src/SAWScript/Crucible/JVM/BuiltinsJVM.hs b/src/SAWScript/Crucible/JVM/BuiltinsJVM.hs
index 0ea687e26f..4ed6096231 100644
--- a/src/SAWScript/Crucible/JVM/BuiltinsJVM.hs
+++ b/src/SAWScript/Crucible/JVM/BuiltinsJVM.hs
@@ -159,7 +159,7 @@ jvm_extract c mname = do
   ctx <- getJVMTrans
 
   io $ do -- only the IO monad, nothing else
-          sym <- newSAWCoreExprBuilder sc
+          sym <- newSAWCoreExprBuilder sc False
           SomeOnlineBackend bak <- newSAWCoreBackend pathSatSolver sym
           st  <- sawCoreState sym
           CJ.setSimulatorVerbosity verbosity sym
diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs
index ca4ae24655..cb38394fa2 100644
--- a/src/SAWScript/Crucible/LLVM/Builtins.hs
+++ b/src/SAWScript/Crucible/LLVM/Builtins.hs
@@ -131,6 +131,8 @@ import qualified Control.Monad.Trans.Maybe as MaybeT
 
 -- parameterized-utils
 import           Data.Parameterized.Classes
+import           Data.Parameterized.Map (MapF)
+import qualified Data.Parameterized.Map as MapF
 import           Data.Parameterized.NatRepr
 import           Data.Parameterized.Some
 import qualified Data.Parameterized.Context as Ctx
@@ -165,6 +167,7 @@ import qualified Lang.Crucible.Simulator.PathSatisfiability as Crucible
 import qualified Lang.Crucible.LLVM.ArraySizeProfile as Crucible
 import qualified Lang.Crucible.LLVM.DataLayout as Crucible
 import qualified Lang.Crucible.LLVM.Bytes as Crucible
+import qualified Lang.Crucible.LLVM.Functions as Crucible
 import qualified Lang.Crucible.LLVM.Intrinsics as Crucible
 import qualified Lang.Crucible.LLVM.MemModel as Crucible
 import qualified Lang.Crucible.LLVM.MemType as Crucible
@@ -645,14 +648,15 @@ verifyMethodSpec cc methodSpec lemmas checkSat tactic asp =
      printOutLnTop Info $
        unwords ["Simulating", (methodSpec ^. csName) , "..."]
      top_loc <- toW4Loc "llvm_verify" <$> getPosition
-     (ret, globals3) <-
-       io $ verifySimulate opts cc pfs methodSpec args assumes top_loc lemmas globals2 checkSat asp mdMap
+     (ret, globals3, invSubst) <-
+       verifySimulate opts cc pfs methodSpec args assumes top_loc lemmas globals2 checkSat asp mdMap
 
      -- collect the proof obligations
      (asserts, post_override_state) <-
        verifyPoststate cc
        methodSpec env globals3 ret
        mdMap
+       invSubst
 
      -- restore previous assumption state
      _ <- io $ Crucible.popAssumptionFrame bak frameIdent
@@ -752,6 +756,7 @@ refineMethodSpec cc methodSpec lemmas tactic =
        verifyPoststate cc
        methodSpec env globals3 ret
        mdMap
+       MapF.empty
 
      -- restore previous assumption state
      _ <- io $ Crucible.popAssumptionFrame bak frameIdent
@@ -1431,11 +1436,10 @@ verifySimulate ::
   Bool ->
   Maybe (IORef (Map Text.Text [Crucible.FunctionProfile])) ->
   IORef MetadataMap ->
-  IO (Maybe (Crucible.MemType, LLVMVal), Crucible.SymGlobalState Sym)
+  TopLevel (Maybe (Crucible.MemType, LLVMVal), Crucible.SymGlobalState Sym, MapF (W4.SymFnWrapper Sym) (W4.SymFnWrapper Sym))
 verifySimulate opts cc pfs mspec args assumes top_loc lemmas globals checkSat asp mdMap =
-  withCfgAndBlockId opts cc mspec $ \cfg entryId ->
-  ccWithBackend cc $ \bak ->
-  do let sym = cc^.ccSym
+  io $ withCfgAndBlockId opts cc mspec $ \cfg entryId -> ccWithBackend cc $ \bak -> do
+     let sym = cc^.ccSym
      let argTys = Crucible.blockInputs $
            Crucible.getBlock entryId $ Crucible.cfgBlockMap cfg
      let retTy = Crucible.handleReturnType $ Crucible.cfgHandle cfg
@@ -1503,7 +1507,7 @@ verifySimulate opts cc pfs mspec args assumes top_loc lemmas globals checkSat as
                             (Crucible.regType  retval)
                             (Crucible.regValue retval)
                      return (Just (ret_mt, v))
-            return (retval', globals1)
+            return (retval', globals1, MapF.empty)
 
        Crucible.TimeoutResult _ -> fail $ "Symbolic execution timed out"
 
@@ -1627,9 +1631,10 @@ verifyPoststate ::
   Crucible.SymGlobalState Sym {- ^ global variables -} ->
   Maybe (Crucible.MemType, LLVMVal) {- ^ optional return value -} ->
   IORef MetadataMap {- ^ metadata map -} ->
+  MapF (W4.SymFnWrapper Sym) (W4.SymFnWrapper Sym) {- ^ invariant substitution -} ->
   TopLevel ([(String, MS.ConditionMetadata, Term)], OverrideState (LLVM arch))
     {- ^ generated labels and verification conditions -}
-verifyPoststate cc mspec env0 globals ret mdMap =
+verifyPoststate cc mspec env0 globals ret mdMap invSubst =
   ccWithBackend cc $ \bak ->
   do poststateLoc <- toW4Loc "_SAW_verify_poststate" <$> getPosition
      sc <- getSharedContext
@@ -1670,7 +1675,7 @@ verifyPoststate cc mspec env0 globals ret mdMap =
           modifyIORef mdMap (Map.insert ann md)
           Crucible.addAssertion bak (Crucible.LabeledPred p' r)
 
-     sc_obligations <- io $ getPoststateObligations sc bak mdMap
+     sc_obligations <- io $ getPoststateObligations sc bak mdMap invSubst
      return (sc_obligations, st)
 
   where
@@ -1692,14 +1697,16 @@ verifyPoststate cc mspec env0 globals ret mdMap =
 
 -- | Translate the proof obligations from the Crucible backend into SAWCore
 -- terms. For each proof oblication, return a triple consisting of the error
--- message, the metadata, and the SAWCore.
+-- message, the metadata, and the SAWCore. For each proof obligation, substitute
+-- the uninterpreted invariants with their definitions.
 getPoststateObligations ::
   Crucible.IsSymBackend Sym bak =>
   SharedContext ->
   bak ->
   IORef MetadataMap ->
+  MapF (W4.SymFnWrapper Sym) (W4.SymFnWrapper Sym) {- ^ invariant substitution -} ->
   IO [(String, MS.ConditionMetadata, Term)]
-getPoststateObligations sc bak mdMap =
+getPoststateObligations sc bak mdMap invSubst =
   do obligations <- maybe [] Crucible.goalsToList <$> Crucible.getProofObligations bak
      Crucible.clearProofObligations bak
 
@@ -1711,8 +1718,8 @@ getPoststateObligations sc bak mdMap =
 
     verifyObligation finalMdMap (Crucible.ProofGoal hyps (Crucible.LabeledPred concl err@(Crucible.SimError loc _))) =
       do st <- Common.sawCoreState sym
-         hypTerm <- toSC sym st =<< Crucible.assumptionsPred sym hyps
-         conclTerm <- toSC sym st concl
+         hypTerm <- toSC sym st =<< W4.substituteSymFns sym invSubst =<< Crucible.assumptionsPred sym hyps
+         conclTerm <- toSC sym st =<< W4.substituteSymFns sym invSubst concl
          obligation <- scImplies sc hypTerm conclTerm
          let defaultMd = MS.ConditionMetadata
                          { MS.conditionLoc = loc
@@ -1744,8 +1751,10 @@ setupLLVMCrucibleContext pathSat lm action =
      smt_array_memory_model_enabled <- gets rwSMTArrayMemoryModel
      crucible_assert_then_assume_enabled <- gets rwCrucibleAssertThenAssume
      what4HashConsing <- gets rwWhat4HashConsing
+     what4PushMuxOps <- gets rwWhat4PushMuxOps
      laxPointerOrdering <- gets rwLaxPointerOrdering
      laxLoadsAndStores <- gets rwLaxLoadsAndStores
+     noSatisfyingWriteFreshConstant <- gets rwNoSatisfyingWriteFreshConstant
      pathSatSolver <- gets rwPathSatSolver
      what4Eval <- gets rwWhat4Eval
      allocSymInitCheck <- gets rwAllocSymInitCheck
@@ -1756,6 +1765,7 @@ setupLLVMCrucibleContext pathSat lm action =
           let ?memOpts = Crucible.defaultMemOptions
                           { Crucible.laxPointerOrdering = laxPointerOrdering
                           , Crucible.laxLoadsAndStores = laxLoadsAndStores
+                          , Crucible.noSatisfyingWriteFreshConstant = noSatisfyingWriteFreshConstant
                           }
           let ?intrinsicsOpts = Crucible.defaultIntrinsicsOptions
           let ?recordLLVMAnnotation = \_ _ _ -> return ()
@@ -1764,7 +1774,7 @@ setupLLVMCrucibleContext pathSat lm action =
           cc <-
             io $
             do let verbosity = simVerbose opts
-               sym <- Common.newSAWCoreExprBuilder sc
+               sym <- Common.newSAWCoreExprBuilder sc False
                Common.SomeOnlineBackend bak <-
                  Common.newSAWCoreBackendWithTimeout pathSatSolver sym crucibleTimeout
 
@@ -1775,6 +1785,9 @@ setupLLVMCrucibleContext pathSat lm action =
                cacheTermsSetting <- W4.getOptionSetting W4.cacheTerms cfg
                _ <- W4.setOpt cacheTermsSetting what4HashConsing
 
+               pushMuxOpsSetting <- W4.getOptionSetting W4.pushMuxOpsOption cfg
+               _ <- W4.setOpt pushMuxOpsSetting what4PushMuxOps
+
                -- enable online solver interactions if path sat checking is on
                enableOnlineSetting <- W4.getOptionSetting Crucible.enableOnlineBackend cfg
                _ <- W4.setOpt enableOnlineSetting pathSat
@@ -1808,7 +1821,9 @@ setupLLVMCrucibleContext pathSat lm action =
                      do -- register all the functions defined in the LLVM module
                         Crucible.registerLazyModule (handleTranslationWarning opts) mtrans
                         -- register the callable override functions
-                        Crucible.register_llvm_overrides llvm_mod saw_llvm_overrides saw_llvm_overrides ctx
+                        _ <- Crucible.register_llvm_overrides llvm_mod saw_llvm_overrides saw_llvm_overrides ctx
+
+                        pure ()
 
                let initExecState =
                      Crucible.InitialState simctx globals Crucible.defaultAbortHandler Crucible.UnitRepr $
@@ -1844,19 +1859,20 @@ handleTranslationWarning opts (Crucible.LLVMTranslationWarning s p msg) =
 
 saw_llvm_overrides ::
   ( Crucible.IsSymInterface sym, Crucible.HasLLVMAnn sym, Crucible.HasPtrWidth wptr ) =>
-  [Crucible.OverrideTemplate p sym arch rtp l a]
+  [Crucible.OverrideTemplate p sym ext arch]
 saw_llvm_overrides =
   [ Crucible.basic_llvm_override saw_assert_override
   ]
 
 saw_assert_override ::
   ( Crucible.IsSymInterface sym, Crucible.HasLLVMAnn sym, Crucible.HasPtrWidth wptr ) =>
-  Crucible.LLVMOverride p sym
+  Crucible.LLVMOverride p sym ext
     (Crucible.EmptyCtx Crucible.::> Crucible.BVType 32)
     Crucible.UnitType
 saw_assert_override =
   [llvmOvr| void @saw_assert( i32 ) |]
-  (\_memOps bak (Ctx.Empty Ctx.:> p) ->
+  (\_memOps (Ctx.Empty Ctx.:> p) ->
+     Crucible.ovrWithBackend $ \bak ->
      do let sym = Crucible.backendGetSym bak
         let msg = Crucible.GenericSimError "saw_assert"
         liftIO $
diff --git a/src/SAWScript/Crucible/LLVM/Override.hs b/src/SAWScript/Crucible/LLVM/Override.hs
index bcf62131e9..da3a14a2fb 100644
--- a/src/SAWScript/Crucible/LLVM/Override.hs
+++ b/src/SAWScript/Crucible/LLVM/Override.hs
@@ -119,6 +119,7 @@ import qualified Data.BitVector.Sized as BV
 import           Verifier.SAW.SharedTerm
 import           Verifier.SAW.Recognizer
 import           Verifier.SAW.TypedTerm
+import           Verifier.SAW.Simulator.TermModel
 import           Verifier.SAW.Simulator.What4.ReturnTrip (SAWCoreState(..), toSC, bindSAWTerm)
 
 import           SAWScript.Crucible.Common
@@ -1487,7 +1488,34 @@ matchPointsToValue opts sc cc spec prepost md maybe_cond ptr val =
 
                    return Nothing
 
-              _ -> return $ Just errMsg
+              _ ->
+                do sub <- OM (use termSub)
+                   modmap <- liftIO $ scGetModuleMap sc
+                   instantiated_expected_sz_tm <- liftIO $ scInstantiateExt sc sub $ ttTerm expected_sz_tm
+                   normalized_expected_sz_tm <- liftIO $
+                     normalizeSharedTerm sc modmap mempty mempty mempty instantiated_expected_sz_tm
+                   case asUnsignedConcreteBv normalized_expected_sz_tm of
+                     Just sz_nat ->
+                       do sz_bv <- liftIO $
+                            W4.bvLit sym Crucible.PtrWidth $ BV.mkBV Crucible.PtrWidth $ fromIntegral sz_nat
+                          maybe_matching_array <- liftIO $
+                            Crucible.asMemMatchingArrayStore sym Crucible.PtrWidth ptr sz_bv (Crucible.memImplHeap mem)
+                          res <- case maybe_matching_array of
+                            Just (ok, arr) -> return $ Right (ok, arr)
+                            Nothing -> liftIO $ Crucible.loadArrayConcreteSizeRaw sym mem ptr sz_nat alignment
+
+                          case res of
+                            Right (ok, arr) ->
+                              do addAssert ok md $ Crucible.SimError loc $ Crucible.GenericSimError $ show errMsg
+                                 st <- liftIO (sawCoreState sym)
+                                 arr_tm <- liftIO $ toSC sym st arr
+                                 instantiateExtMatchTerm sc md prepost arr_tm $ ttTerm expected_arr_tm
+                                 return Nothing
+
+                            Left{} -> return $ Just errMsg
+
+                     Nothing -> return $ Just errMsg
+
 
 -- | Like 'matchPointsToValue', but specifically geared towards the needs
 -- of fields within bitfields. In particular, this performs all of the
diff --git a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
index 2ce7d9113e..93a0b2718f 100644
--- a/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
+++ b/src/SAWScript/Crucible/LLVM/ResolveSetupValue.hs
@@ -754,7 +754,7 @@ resolveSAWPred cc tm = do
      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
+                      let v = Concrete.evalSharedTerm modmap mempty mempty tm'
                       pure (Just (Concrete.toBool v))
              _ -> return Nothing
      case mx of
diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs
index 26aca27d81..57fdf0277b 100644
--- a/src/SAWScript/Crucible/LLVM/X86.hs
+++ b/src/SAWScript/Crucible/LLVM/X86.hs
@@ -27,13 +27,14 @@ Stability   : provisional
 module SAWScript.Crucible.LLVM.X86
   ( llvm_verify_x86
   , llvm_verify_fixpoint_x86
+  , llvm_verify_fixpoint_chc_x86
   , llvm_verify_x86_with_invariant
   , defaultStackBaseAlign
   ) where
 
 import Control.Lens.TH (makeLenses)
 
-import System.IO (stdout)
+import System.IO
 import Control.Exception (throw)
 import Control.Lens (Getter, to, view, use, (&), (^.), (.~), (%~), (.=))
 import Control.Monad (forM, forM_, unless, when, zipWithM)
@@ -62,6 +63,7 @@ import Data.Maybe
 import qualified Text.LLVM.AST as LLVM
 
 import Data.Parameterized.Some
+import Data.Parameterized.Map (MapF)
 import qualified Data.Parameterized.Map as MapF
 import Data.Parameterized.NatRepr
 import Data.Parameterized.Nonce (GlobalNonceGenerator)
@@ -130,6 +132,7 @@ import qualified Lang.Crucible.LLVM.Intrinsics as C.LLVM
 import qualified Lang.Crucible.LLVM.MemModel as C.LLVM
 import qualified Lang.Crucible.LLVM.MemType as C.LLVM
 import qualified Lang.Crucible.LLVM.SimpleLoopFixpoint as Crucible.LLVM.Fixpoint
+import qualified Lang.Crucible.LLVM.SimpleLoopFixpointCHC as Crucible.LLVM.FixpointCHC
 import qualified Lang.Crucible.LLVM.SimpleLoopInvariant as SimpleInvariant
 import qualified Lang.Crucible.LLVM.Translation as C.LLVM
 import qualified Lang.Crucible.LLVM.TypeContext as C.LLVM
@@ -272,9 +275,10 @@ llvmPointerOffset = snd . C.LLVM.llvmPointerView
 -- the unsigned comparison between pointer1 and pointer2 is equivalent with the
 -- unsigned comparison between offset1 + 4096 and offset2 + 4096.
 doPtrCmp ::
+  FixpointSelect ->
   (sym -> W4.SymBV sym w -> W4.SymBV sym w -> IO (W4.Pred sym)) ->
   Macaw.PtrOp sym w (C.RegValue sym C.BoolType)
-doPtrCmp f = Macaw.ptrOp $ \bak mem w xPtr xBits yPtr yBits x y -> do
+doPtrCmp fixpointSelect f = Macaw.ptrOp $ \bak mem w xPtr xBits yPtr yBits x y -> do
   let sym = backendGetSym bak
   let ptr_as_bv_for_cmp ptr = do
         page_size <- W4.bvLit sym (W4.bvWidth $ llvmPointerOffset ptr) $
@@ -286,6 +290,8 @@ doPtrCmp f = Macaw.ptrOp $ \bak mem w xPtr xBits yPtr yBits x y -> do
         ok <- W4.orPred sym is_valid
           =<< W4.andPred sym is_negative_offset is_not_overflow
         return (ptr_as_bv, ok)
+        -- is_valid <- Macaw.isValidPtr sym mem w ptr
+        -- return (llvmPointerOffset ptr, is_valid)
   both_bits <- W4.andPred sym xBits yBits
   both_ptrs <- W4.andPred sym xPtr yPtr
   same_region <- W4.natEq sym (llvmPointerBlock x) (llvmPointerBlock y)
@@ -296,9 +302,20 @@ doPtrCmp f = Macaw.ptrOp $ \bak mem w xPtr xBits yPtr yBits x y -> do
     =<< W4.andPred sym ok_x ok_y
   res_both_bits <- f sym (llvmPointerOffset x) (llvmPointerOffset y)
   res_both_ptrs <- f sym x_ptr_as_bv y_ptr_as_bv
-  undef <- Macaw.mkUndefinedBool sym "ptr_cmp"
-  W4.itePred sym both_bits res_both_bits
-    =<< W4.itePred sym ok_both_ptrs res_both_ptrs undef
+  let ptrCmpDefault = do
+        undef <- Macaw.mkUndefinedBool sym "ptr_cmp"
+        W4.itePred sym both_bits res_both_bits
+          =<< W4.itePred sym ok_both_ptrs res_both_ptrs undef
+  case fixpointSelect of
+    SimpleFixpointCHC{} ->
+      if | Just True <- W4.asConstantPred both_bits ->
+           return res_both_bits
+         | Just True <- W4.asConstantPred both_ptrs -> do
+           C.assert bak ok_both_ptrs $ C.AssertFailureSimError "" ""
+           return res_both_ptrs
+         | otherwise ->
+           ptrCmpDefault
+    _ -> ptrCmpDefault
 
 -------------------------------------------------------------------------------
 -- ** Entrypoint
@@ -334,6 +351,26 @@ llvm_verify_fixpoint_x86 ::
 llvm_verify_fixpoint_x86 llvmModule path nm globsyms checkSat f =
   llvm_verify_x86_common llvmModule path nm globsyms checkSat (SimpleFixpoint f)
 
+-- | Verify that an x86_64 function (following the System V AMD64 ABI) conforms
+-- to an LLVM specification. This allows for compositional verification of LLVM
+-- functions that call x86_64 functions (but not the other way around).
+--
+-- This differs from 'llvm_verify_fixpoint_x86' in that it leverages Z3's
+-- constrained horn-clause (CHC) functionality to synthesize some of the loop's
+-- properties.
+llvm_verify_fixpoint_chc_x86 ::
+  Some LLVMModule {- ^ Module to associate with method spec -} ->
+  FilePath {- ^ Path to ELF file -} ->
+  String {- ^ Function's symbol in ELF file -} ->
+  [(String, Integer)] {- ^ Global variable symbol names and sizes (in bytes) -} ->
+  Bool {- ^ Whether to enable path satisfiability checking -} ->
+  TypedTerm {- ^ Function specifying the loop -} ->
+  LLVMCrucibleSetupM () {- ^ Specification to verify against -} ->
+  ProofScript () {- ^ Tactic used to use when discharging goals -} ->
+  TopLevel (SomeLLVM MS.ProvedSpec)
+llvm_verify_fixpoint_chc_x86 llvmModule path nm globsyms checkSat f =
+  llvm_verify_x86_common llvmModule path nm globsyms checkSat (SimpleFixpointCHC f)
+
 -- | Verify that an x86_64 function (following the System V AMD64 ABI) conforms
 -- to an LLVM specification. This allows for compositional verification of LLVM
 -- functions that call x86_64 functions (but not the other way around).
@@ -354,6 +391,7 @@ llvm_verify_x86_with_invariant llvmModule path nm globsyms checkSat (loopName,lo
 data FixpointSelect
  = NoFixpoint
  | SimpleFixpoint TypedTerm
+ | SimpleFixpointCHC TypedTerm
  | SimpleInvariant String Integer TypedTerm
 
 llvm_verify_x86_common ::
@@ -371,29 +409,34 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec
                  $ modTrans llvmModule ^. C.LLVM.transContext = do
       start <- io getCurrentTime
       laxLoadsAndStores <- gets rwLaxLoadsAndStores
+      noSatisfyingWriteFreshConstant <- gets rwNoSatisfyingWriteFreshConstant
       pathSatSolver <- gets rwPathSatSolver
       let ?ptrWidth = knownNat @64
       let ?memOpts = C.LLVM.defaultMemOptions
                        { C.LLVM.laxLoadsAndStores = laxLoadsAndStores
+                       , C.LLVM.noSatisfyingWriteFreshConstant = noSatisfyingWriteFreshConstant
                        }
       let ?recordLLVMAnnotation = \_ _ _ -> return ()
       sc <- getSharedContext
       opts <- getOptions
       basic_ss <- getBasicSS
       rw <- getTopLevelRW
-      sym <- liftIO $ newSAWCoreExprBuilder sc
+      sym <- liftIO $ newSAWCoreExprBuilder sc False
       mdMap <- liftIO $ newIORef mempty
       SomeOnlineBackend bak <- liftIO $
         newSAWCoreBackendWithTimeout pathSatSolver sym $ rwCrucibleTimeout rw
-      cacheTermsSetting <- liftIO $ W4.getOptionSetting W4.B.cacheTerms $ W4.getConfiguration sym
+      let config = W4.getConfiguration sym
+      cacheTermsSetting <- liftIO $ W4.getOptionSetting W4.B.cacheTerms config
       _ <- liftIO $ W4.setOpt cacheTermsSetting $ rwWhat4HashConsingX86 rw
+      pushMuxOpsSetting <- liftIO $ W4.getOptionSetting W4.B.pushMuxOpsOption config
+      _ <- liftIO $ W4.setOpt pushMuxOpsSetting $ rwWhat4PushMuxOps rw
       liftIO $ W4.extendConfig
         [ W4.opt
             LO.enableSMTArrayMemoryModel
             (W4.ConcreteBool $ rwSMTArrayMemoryModel rw)
             ("Enable SMT array memory model" :: Text)
         ]
-        (W4.getConfiguration sym)
+        config
       let ?w4EvalTactic = W4EvalTactic { doW4Eval = rwWhat4Eval rw }
       sawst <- liftIO $ sawCoreState sym
       halloc <- getHandleAlloc
@@ -493,8 +536,8 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec
           archEvalFns mvar mmConf
         sawMacawExtensions = defaultMacawExtensions_x86_64
           { C.extensionExec = \s0 st -> case s0 of
-              Macaw.PtrLt w x y -> doPtrCmp W4.bvUlt st mvar w x y
-              Macaw.PtrLeq w x y -> doPtrCmp W4.bvUle st mvar w x y
+              Macaw.PtrLt w x y -> doPtrCmp fixpointSelect W4.bvUlt st mvar w x y
+              Macaw.PtrLeq w x y -> doPtrCmp fixpointSelect W4.bvUle st mvar w x y
               _ -> (C.extensionExec defaultMacawExtensions_x86_64) s0 st
           }
         ctx :: C.SimContext (Macaw.MacawSimulatorState Sym) Sym (Macaw.MacawExt Macaw.X86_64)
@@ -539,12 +582,20 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec
          else
            pure []
 
-      simpleLoopFixpointFeature <-
+      -- rw_ref <- liftIO . newIORef =<< getTopLevelRW
+      (simpleLoopFixpointFeature, maybe_ref) <-
         case fixpointSelect of
-          NoFixpoint -> return []
+          NoFixpoint -> return ([], Nothing)
           SimpleFixpoint func ->
-            do f <- liftIO (setupSimpleLoopFixpointFeature sym sc sawst cfg mvar func)
-               return [f]
+            do f <- liftIO $ setupSimpleLoopFixpointFeature sym sc sawst cfg mvar func
+               return ([f], Nothing)
+          SimpleFixpointCHC func ->
+            do let ?ptrWidth = knownNat @64
+              --  (f, ref) <- liftIO $ Crucible.LLVM.Fixpoint.simpleLoopFixpoint sym cfg mvar Nothing
+              --  (f, ref) <- liftIO $ Crucible.LLVM.Fixpoint.simpleLoopFixpoint sym cfg mvar $
+              --    Just $ simpleLoopFixpointFunction sc sym rw_ref $ methodSpec ^. csName
+               (f, ref) <- liftIO $ setupSimpleLoopFixpointCHCFeature sym sc sawst cfg mvar func
+               return ([f], Just ref)
           SimpleInvariant loopFixpointSymbol loopNum func ->
             do (loopaddr :: Macaw.MemSegmentOff 64) <-
                  case findSymbols (symMap relf) . encodeUtf8 $ Text.pack loopFixpointSymbol of
@@ -556,7 +607,7 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec
                    do let printFn = printOutLn opts Info
                       f <- liftIO (setupSimpleLoopInvariantFeature sym printFn loopNum
                                                                    sc sawst mdMap loopcfg mvar func)
-                      return [f]
+                      return ([f], Nothing)
 
       let execFeatures = simpleLoopFixpointFeature ++ psatf
 
@@ -578,12 +629,22 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec
                          ]
         C.TimeoutResult{} -> fail "Execution timed out"
 
+      (invSubst, loopFunEquivConds) <- liftIO $ case maybe_ref of
+        Just fixpoint_state_ref -> do
+          uninterp_inv_fns <- Crucible.LLVM.FixpointCHC.executionFeatureContextInvPreds <$> readIORef fixpoint_state_ref
+          subst <- C.runCHC bak uninterp_inv_fns
+          loop_fun_equiv_conds <- Crucible.LLVM.FixpointCHC.executionFeatureContextLoopFunEquivConds <$> readIORef fixpoint_state_ref
+          return (subst, loop_fun_equiv_conds)
+        Nothing -> return (MapF.empty, [])
+
       liftIO $ printOutLn opts Info
         "Examining specification to determine postconditions"
       liftIO $ void $ runX86Sim finalState $
         assertPost env (preState ^. x86Mem) (preState ^. x86Regs) mdMap
 
-      (stats,vcstats) <- checkGoals bak opts nm sc tactic mdMap
+      (stats,vcstats) <- checkGoals bak opts nm (methodSpec ^. MS.csLoc) sc tactic mdMap invSubst loopFunEquivConds
+
+      -- putTopLevelRW =<< liftIO (readIORef rw_ref)
 
       end <- io getCurrentTime
       let diff = diffUTCTime end start
@@ -592,8 +653,6 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec
 
   | otherwise = fail "LLVM module must be 64-bit"
 
-
-
 setupSimpleLoopFixpointFeature ::
   ( sym ~ W4.B.ExprBuilder n st fs
   , C.IsSymInterface sym
@@ -665,6 +724,80 @@ setupSimpleLoopFixpointFeature sym sc sawst cfg mvar func =
 
        return (result_substitution, result_condition)
 
+setupSimpleLoopFixpointCHCFeature ::
+  ( sym ~ W4.B.ExprBuilder n st fs
+  , C.IsSymInterface sym
+  , ?memOpts::C.LLVM.MemOptions
+  , C.LLVM.HasLLVMAnn sym
+  , C.IsSyntaxExtension ext
+  ) =>
+  sym ->
+  SharedContext ->
+  SAWCoreState n ->
+  C.CFG ext blocks init ret ->
+  C.GlobalVar C.LLVM.Mem ->
+  TypedTerm ->
+  IO (C.ExecutionFeature p sym ext rtp, IORef (Crucible.LLVM.FixpointCHC.ExecutionFeatureContext sym 64 ext))
+
+setupSimpleLoopFixpointCHCFeature sym sc sawst cfg mvar func = do
+  let ?ptrWidth = knownNat @64
+  Crucible.LLVM.FixpointCHC.simpleLoopFixpoint sym cfg mvar $ Just fixpoint_func
+
+ where
+  fixpoint_func fixpoint_substitution condition =
+    do let fixpoint_substitution_as_list = reverse $ MapF.toList fixpoint_substitution
+       let header_exprs = map (mapSome $ Crucible.LLVM.FixpointCHC.headerValue) (MapF.elems fixpoint_substitution)
+       let body_exprs = map (mapSome $ Crucible.LLVM.FixpointCHC.bodyValue) (MapF.elems fixpoint_substitution)
+       let uninterpreted_constants = foldMap
+             (viewSome $ Set.map (mapSome $ W4.varExpr sym) . W4.exprUninterpConstants sym)
+             (Some condition : body_exprs ++ header_exprs)
+       let filtered_uninterpreted_constants = Set.toList $ Set.filter
+             (\(Some variable) ->
+               not (List.isPrefixOf "cindex_var" $ show $ W4.printSymExpr variable)
+               && not (List.isPrefixOf "creg_join_var" $ show $ W4.printSymExpr variable)
+               && not (List.isPrefixOf "cmem_join_var" $ show $ W4.printSymExpr variable)
+               && not (List.isPrefixOf "cundefined" $ show $ W4.printSymExpr variable)
+               && not (List.isPrefixOf "calign_amount" $ show $ W4.printSymExpr variable))
+             uninterpreted_constants
+       tms <- mapM (viewSome $ toSC sym sawst) filtered_uninterpreted_constants
+       implicit_parameters <- mapM (scExtCns sc) $ Set.toList $ foldMap getAllExtSet tms
+       arguments <- forM fixpoint_substitution_as_list $ \(MapF.Pair _ fixpoint_entry) ->
+         toSC sym sawst $ Crucible.LLVM.FixpointCHC.headerValue fixpoint_entry
+       arguments_tuple <- scTuple sc arguments
+       applied_func <- scApplyAll sc (ttTerm func) $ implicit_parameters ++ [arguments_tuple]
+       applied_func_selectors <- forM [1 .. (length fixpoint_substitution_as_list)] $ \i ->
+         scTupleSelector sc applied_func i (length fixpoint_substitution_as_list)
+       result_substitution <- MapF.fromList <$> zipWithM
+         (\(MapF.Pair variable _) applied_func_selector ->
+           MapF.Pair variable <$> bindSAWTerm sym sawst (W4.exprType variable) applied_func_selector)
+         fixpoint_substitution_as_list
+         applied_func_selectors
+
+       explicit_parameters <- forM fixpoint_substitution_as_list $ \(MapF.Pair variable _) ->
+         toSC sym sawst variable
+       explicit_parameters_tuple <- scTuple sc explicit_parameters
+
+       inner_func <- case asConstant (ttTerm func) of
+         Just (_, Just (asApplyAll -> (isGlobalDef "Prelude.fix" -> Just (), [_, inner_func]))) ->
+           return inner_func
+         _ -> fail $ "not Prelude.fix: " ++ showTerm (ttTerm func)
+       func_body <- betaNormalize sc
+         =<< scApplyAll sc inner_func ((ttTerm func) : (implicit_parameters ++ [explicit_parameters_tuple]))
+
+       step_arguments <- forM fixpoint_substitution_as_list $ \(MapF.Pair _ fixpoint_entry) ->
+         toSC sym sawst $ Crucible.LLVM.FixpointCHC.bodyValue fixpoint_entry
+       step_arguments_tuple <- scTuple sc step_arguments
+       tail_applied_func <- scApplyAll sc (ttTerm func) $ implicit_parameters ++ [step_arguments_tuple]
+
+       loop_condition <- toSC sym sawst condition
+       output_tuple_type <- scTupleType sc =<< mapM (scTypeOf sc) explicit_parameters
+       loop_body <- scIte sc output_tuple_type loop_condition tail_applied_func explicit_parameters_tuple
+
+       induction_step_condition <- scEq sc loop_body func_body
+       result_condition <- bindSAWTerm sym sawst W4.BaseBoolRepr induction_step_condition
+
+       return (result_substitution, Just result_condition)
+
 
 -- | This procedure sets up the simple loop fixpoint feature.
 --   Its main task is to massage the user-provided invariant
@@ -1384,12 +1517,28 @@ checkGoals ::
   bak ->
   Options ->
   String ->
+  W4.ProgramLoc ->
   SharedContext ->
   ProofScript () ->
   IORef MetadataMap {- ^ metadata map -} ->
+  MapF (W4.SymFnWrapper Sym) (W4.SymFnWrapper Sym) ->
+  [W4.Pred Sym] ->
   TopLevel (SolverStats, [MS.VCStats])
-checkGoals bak opts nm sc tactic mdMap = do
-  gs <- liftIO $ getPoststateObligations sc bak mdMap
+checkGoals bak opts nm loc sc tactic mdMap invSubst loopFunEquivConds = do
+  poststate_gs <- liftIO $ getPoststateObligations sc bak mdMap invSubst
+  loop_gs <- liftIO $ forM loopFunEquivConds $ \cond -> do
+    let sym = C.backendGetSym bak
+    st <- Common.sawCoreState sym
+    condTerm <- toSC sym st =<< W4.substituteSymFns sym invSubst cond
+    let defaultMd = MS.ConditionMetadata
+          { MS.conditionLoc = loc
+          , MS.conditionTags = mempty
+          , MS.conditionType = "loop function equivalence"
+          , MS.conditionContext = ""
+          }
+    return ("", defaultMd, condTerm)
+  let gs = poststate_gs ++ loop_gs
+
   liftIO . printOutLn opts Info $ mconcat
     [ "Simulation finished, running solver on "
     , show $ length gs
diff --git a/src/SAWScript/Crucible/MIR/Builtins.hs b/src/SAWScript/Crucible/MIR/Builtins.hs
index 9fe85bd382..adc2462658 100644
--- a/src/SAWScript/Crucible/MIR/Builtins.hs
+++ b/src/SAWScript/Crucible/MIR/Builtins.hs
@@ -1395,7 +1395,7 @@ setupCrucibleContext rm =
   do halloc <- getHandleAlloc
      sc <- getSharedContext
      pathSatSolver <- gets rwPathSatSolver
-     sym <- io $ newSAWCoreExprBuilder sc
+     sym <- io $ newSAWCoreExprBuilder sc False
      someBak@(SomeOnlineBackend bak) <- io $ newSAWCoreBackend pathSatSolver sym
      let cs     = rm ^. Mir.rmCS
      let col    = cs ^. Mir.collection
diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
index 59be4c6e0f..0ccc981bde 100644
--- a/src/SAWScript/Interpreter.hs
+++ b/src/SAWScript/Interpreter.hs
@@ -515,6 +515,8 @@ buildTopLevelEnv proxy opts =
                    , rwPreservedRegs = []
                    , rwStackBaseAlign = defaultStackBaseAlign
                    , rwAllocSymInitCheck = True
+                   , rwWhat4PushMuxOps = False
+                   , rwNoSatisfyingWriteFreshConstant = True
                    , rwCrucibleTimeout = CC.defaultSAWCoreBackendTimeout
                    , rwPathSatSolver = CC.PathSat_Z3
                    , rwSkipSafetyProofs = False
@@ -737,6 +739,26 @@ disable_alloc_sym_init_check = do
   rw <- getTopLevelRW
   putTopLevelRW rw { rwAllocSymInitCheck = False }
 
+enable_no_satisfying_write_fresh_constant :: TopLevel ()
+enable_no_satisfying_write_fresh_constant = do
+  rw <- getTopLevelRW
+  putTopLevelRW rw { rwNoSatisfyingWriteFreshConstant = True }
+
+disable_no_satisfying_write_fresh_constant :: TopLevel ()
+disable_no_satisfying_write_fresh_constant = do
+  rw <- getTopLevelRW
+  putTopLevelRW rw { rwNoSatisfyingWriteFreshConstant = False }
+
+enable_what4_push_mux_ops :: TopLevel ()
+enable_what4_push_mux_ops = do
+  rw <- getTopLevelRW
+  putTopLevelRW rw { rwWhat4PushMuxOps = True }
+
+disable_what4_push_mux_ops :: TopLevel ()
+disable_what4_push_mux_ops = do
+  rw <- getTopLevelRW
+  putTopLevelRW rw { rwWhat4PushMuxOps = False }
+
 set_crucible_timeout :: Integer -> TopLevel ()
 set_crucible_timeout t = do
   rw <- getTopLevelRW
@@ -3377,6 +3399,19 @@ primitives = Map.fromList
     , "the live variables in the loop evolve as the loop computes."
     ]
 
+  , prim "llvm_verify_fixpoint_chc_x86"
+    "LLVMModule -> String -> String -> [(String, Int)] -> Bool -> Term -> LLVMSetup () -> ProofScript () -> TopLevel LLVMSpec"
+    (pureVal llvm_verify_fixpoint_chc_x86)
+    Experimental
+    [ "An experimental variant of 'llvm_verify_x86'. This variant can prove some properties"
+    , "involving simple loops with the help of a user-provided term that describes how"
+    , "the live variables in the loop evolve as the loop computes."
+    , ""
+    , "This differs from 'llvm_verify_fixpoint_x86' in that it leverages Z3's"
+    , "constrained horn-clause (CHC) functionality to synthesize some of the"
+    , "loop's properties."
+    ]
+
   , prim "llvm_verify_x86_with_invariant"
     "LLVMModule -> String -> String -> [(String, Int)] -> Bool -> (String, Int, Term) -> LLVMSetup () -> ProofScript () -> TopLevel LLVMSpec"
     (pureVal llvm_verify_x86_with_invariant)
@@ -3466,6 +3501,37 @@ primitives = Map.fromList
     , "This makes the implicit assumption that there is some unspecified byte at any valid memory address."
     ]
 
+  , prim "enable_no_satisfying_write_fresh_constant" "TopLevel ()"
+    (pureVal enable_no_satisfying_write_fresh_constant)
+    Experimental
+    [ "When simulating LLVM code that performs an invalid write, make a fresh"
+    , "constant as a proof obligation. This constant will always fail, but it"
+    , "will also not be constant-folded away."
+    ]
+
+  , prim "disable_no_satisfying_write_fresh_constant" "TopLevel ()"
+    (pureVal disable_no_satisfying_write_fresh_constant)
+    Experimental
+    [ "When simulating LLVM code that performs an invalid write, return 'false'"
+    , "as a proof obligation."
+    ]
+
+  , prim "enable_what4_push_mux_ops" "TopLevel ()"
+    (pureVal enable_what4_push_mux_ops)
+    Experimental
+    [ "Push certain What4 operations (e.g., 'zext') down to the branches of"
+    , "'ite' expressions as much as possible. In some (but not all) circumstances,"
+    , "this can result in operations that are easier for SMT solvers to reason"
+    , "about."
+    ]
+
+  , prim "disable_what4_push_mux_ops" "TopLevel ()"
+    (pureVal disable_what4_push_mux_ops)
+    Experimental
+    [ "Do not push certain What4 operations (e.g., 'zext') down to the branches"
+    , "of 'ite' expressions as much as possible."
+    ]
+
   , prim "set_crucible_timeout" "Int -> TopLevel ()"
     (pureVal set_crucible_timeout)
     Experimental
diff --git a/src/SAWScript/Proof.hs b/src/SAWScript/Proof.hs
index cb685c2889..65a9e25547 100644
--- a/src/SAWScript/Proof.hs
+++ b/src/SAWScript/Proof.hs
@@ -466,15 +466,15 @@ unbindAndFreshenProp sc (Prop p0) = loop [] [] p0
 -- | Evaluate the given proposition by round-tripping
 --   through the What4 formula representation.  This will
 --   perform a variety of simplifications and rewrites.
-evalProp :: SharedContext -> Set VarIndex -> Prop -> IO Prop
-evalProp sc unints p =
+evalProp :: SharedContext -> Bool -> Set VarIndex -> Prop -> IO Prop
+evalProp sc what4PushMuxOps unints p =
   do (ecs, body) <- unbindAndFreshenProp sc p
      body' <-
        case asEqTrue body of
          Just t -> pure t
          Nothing -> fail ("goal_eval: expected EqTrue\n" ++ scPrettyTerm defaultPPOpts (unProp p))
 
-     sym <- Common.newSAWCoreExprBuilder sc
+     sym <- Common.newSAWCoreExprBuilder sc what4PushMuxOps
      st <- Common.sawCoreState sym
      (_names, (_mlabels, p')) <- W4Sim.w4Eval sym st sc mempty unints body'
      t1 <- W4Sim.toSC sym st p'
@@ -949,11 +949,11 @@ reachableTheorems db roots = Set.foldl' (loop (theoremMap db)) mempty roots
 --   does not totally guarantee the theorem is true, as it does
 --   not verify any solver-provided proofs, and it accepts admitted
 --   propositions and quickchecked propositions as valid.
-validateTheorem :: SharedContext -> TheoremDB -> Theorem -> IO ()
+validateTheorem :: SharedContext -> Bool -> TheoremDB -> Theorem -> IO ()
 
-validateTheorem sc db Theorem{ _thmProp = p, _thmEvidence = e, _thmDepends = thmDep } =
+validateTheorem sc what4PushMuxOps db Theorem{ _thmProp = p, _thmEvidence = e, _thmDepends = thmDep } =
    do let hyps = Map.keysSet (theoremMap db)
-      (deps,_) <- checkEvidence sc e p
+      (deps,_) <- checkEvidence sc what4PushMuxOps e p
       unless (Set.isSubsetOf deps thmDep && Set.isSubsetOf thmDep hyps)
              (fail $ unlines ["Theorem failed to declare its dependencies correctly"
                              , show deps, show thmDep ])
@@ -1188,6 +1188,7 @@ proofByTerm sc db prf loc rsn =
 --   error will be raised.
 constructTheorem ::
   SharedContext ->
+  Bool ->
   TheoremDB ->
   Prop ->
   Evidence ->
@@ -1196,8 +1197,8 @@ constructTheorem ::
   Text ->
   NominalDiffTime ->
   IO (Theorem, TheoremDB)
-constructTheorem sc db p e loc ploc rsn elapsed =
-  do (deps,sy) <- checkEvidence sc e p
+constructTheorem sc what4PushMuxOps db p e loc ploc rsn elapsed =
+  do (deps,sy) <- checkEvidence sc what4PushMuxOps e p
      n  <- freshNonce globalNonceGenerator
      let thm =
           Theorem
@@ -1220,14 +1221,14 @@ constructTheorem sc db p e loc ploc rsn elapsed =
 --   specializes the leading quantifiers with the given terms.
 --   This will fail if the given terms to not match the quantifier structure
 --   of the given theorem.
-specializeTheorem :: SharedContext -> TheoremDB -> Pos -> Text -> Theorem -> [Term] -> IO (Theorem, TheoremDB)
-specializeTheorem _sc db _loc _rsn thm [] = return (thm, db)
-specializeTheorem sc db loc rsn thm ts =
+specializeTheorem :: SharedContext -> Bool -> TheoremDB -> Pos -> Text -> Theorem -> [Term] -> IO (Theorem, TheoremDB)
+specializeTheorem _sc _what4PushMuxOps db _loc _rsn thm [] = return (thm, db)
+specializeTheorem sc what4PushMuxOps db loc rsn thm ts =
   do res <- specializeProp sc (_thmProp thm) ts
      case res of
        Left err -> fail (unlines (["specialize_theorem: failed to specialize"] ++ TC.prettyTCError err))
        Right p' ->
-         constructTheorem sc db p' (ApplyEvidence thm (map Left ts)) loc Nothing rsn 0
+         constructTheorem sc what4PushMuxOps db p' (ApplyEvidence thm (map Left ts)) loc Nothing rsn 0
 
 specializeProp :: SharedContext -> Prop -> [Term] -> IO (Either TC.TCError Prop)
 specializeProp sc (Prop p0) ts0 = TC.runTCM (loop p0 ts0) sc Nothing []
@@ -1528,8 +1529,9 @@ normalizeConclBoolCommit sc b =
 
 -- | Verify that the given evidence in fact supports the given proposition.
 --   Returns the identifiers of all the theorems depended on while checking evidence.
-checkEvidence :: SharedContext -> Evidence -> Prop -> IO (Set TheoremNonce, TheoremSummary)
-checkEvidence sc = \e p -> do nenv <- scGetNamingEnv sc
+checkEvidence :: SharedContext -> Bool -> Evidence -> Prop -> IO (Set TheoremNonce, TheoremSummary)
+checkEvidence sc what4PushMuxOps = \e p -> do
+                              nenv <- scGetNamingEnv sc
                               check nenv e (propToSequent p)
 
   where
@@ -1683,7 +1685,7 @@ checkEvidence sc = \e p -> do nenv <- scGetNamingEnv sc
            check nenv e' sqt'
 
       EvalEvidence vars e' ->
-        do sqt' <- traverseSequentWithFocus (evalProp sc vars) sqt
+        do sqt' <- traverseSequentWithFocus (evalProp sc what4PushMuxOps vars) sqt
            check nenv e' sqt'
 
       ConversionEvidence sqt' e' ->
@@ -1814,17 +1816,19 @@ finishProof ::
   ProofState ->
   Bool {- ^ should we record the theorem in the database? -} ->
   Bool {- ^ do we need to normalize the sequent to match the final goal ? -} ->
+  Bool {- ^ If 'True', push certain @ExprBuilder@ operations (e.g., @zext@) down
+            to the branches of @ite@ expressions -} ->
   IO (ProofResult, TheoremDB)
 finishProof sc db conclProp
     ps@(ProofState gs (concl,loc,ploc,rsn) stats _ checkEv start)
-    recordThm useSequentGoals =
+    recordThm useSequentGoals what4PushMuxOps =
   case gs of
     [] ->
       do e <- checkEv []
          let e' = if useSequentGoals
                    then NormalizeSequentEvidence concl e
                    else e
-         (deps,sy) <- checkEvidence sc e' conclProp
+         (deps,sy) <- checkEvidence sc what4PushMuxOps e' conclProp
          n <- freshNonce globalNonceGenerator
          end <- getCurrentTime
          let theorem =
diff --git a/src/SAWScript/Prover/Exporter.hs b/src/SAWScript/Prover/Exporter.hs
index 12c4ed2293..951446c3cb 100644
--- a/src/SAWScript/Prover/Exporter.hs
+++ b/src/SAWScript/Prover/Exporter.hs
@@ -49,6 +49,7 @@ import Data.Foldable(toList)
 
 import Control.Monad (unless)
 import Control.Monad.Except (runExceptT)
+import Control.Monad.State (gets)
 import qualified Data.AIG as AIG
 import qualified Data.ByteString as BS
 import Data.Maybe (mapMaybe)
@@ -103,7 +104,7 @@ import SAWScript.Value
 
 import qualified What4.Interface as W4
 import qualified What4.Expr.Builder as W4
-import What4.Config (extendConfig)
+import What4.Config (extendConfig, getOptionSetting, setOpt)
 import What4.Interface (getConfiguration, IsSymExprBuilder)
 import What4.Protocol.SMTLib2 (writeDefaultSMT2)
 import What4.Protocol.SMTLib2.Response (smtParseOptions)
@@ -312,11 +313,16 @@ writeSMTLib2 f satq = getSharedContext >>= \sc -> io $
 -- | Write a SAT query an SMT-Lib version 2 file.
 -- This version uses What4 instead of SBV.
 writeSMTLib2What4 :: FilePath -> SATQuery -> TopLevel ()
-writeSMTLib2What4 f satq = getSharedContext >>= \sc -> io $
-  do sym <- W4.newExprBuilder W4.FloatRealRepr St globalNonceGenerator
+writeSMTLib2What4 f satq = do
+  sc <- getSharedContext
+  what4PushMuxOps <- gets rwWhat4PushMuxOps
+  io $ do
+     sym <- W4.newExprBuilder W4.FloatRealRepr St globalNonceGenerator
      (_varMap, lits) <- W.w4Solve sym sc satq
      let cfg = getConfiguration sym
      extendConfig smtParseOptions cfg
+     pushMuxOpsSetting <- getOptionSetting W4.pushMuxOpsOption cfg
+     _ <- setOpt pushMuxOpsSetting what4PushMuxOps
      withFile f WriteMode $ \h ->
        writeDefaultSMT2 () "Offline SMTLib2" defaultWriteSMTLIB2Features Nothing sym h lits
 
@@ -328,7 +334,7 @@ write_verilog sc path t = io $ writeVerilog sc path t
 
 writeVerilogSAT :: FilePath -> SATQuery -> TopLevel [(ExtCns Term, FiniteType)]
 writeVerilogSAT path satq = getSharedContext >>= \sc -> io $
-  do sym <- newSAWCoreExprBuilder sc
+  do sym <- newSAWCoreExprBuilder sc False
      -- For SAT checking, we don't care what order the variables are in,
      -- but only that we can correctly keep track of the connection
      -- between inputs and assignments.
@@ -380,7 +386,7 @@ flattenSValue _ sval = fail $ "write_verilog: unsupported result type: " ++ show
 
 writeVerilog :: SharedContext -> FilePath -> Term -> IO ()
 writeVerilog sc path t = do
-  sym <- newSAWCoreExprBuilder sc
+  sym <- newSAWCoreExprBuilder sc False
   st  <- sawCoreState sym
   -- For writing Verilog in the general case, it's convenient for any
   -- lambda-bound inputs to appear first in the module input list, in
diff --git a/src/SAWScript/Prover/What4.hs b/src/SAWScript/Prover/What4.hs
index 52de3e941e..69f289d6c8 100644
--- a/src/SAWScript/Prover/What4.hs
+++ b/src/SAWScript/Prover/What4.hs
@@ -9,6 +9,7 @@ module SAWScript.Prover.What4 where
 
 
 import           Control.Lens ((^.))
+import           Control.Monad.State (gets)
 import           Data.List (nub)
 import           Data.Set (Set)
 import qualified Data.Map as Map
@@ -20,7 +21,7 @@ import Verifier.SAW.FiniteValue
 import Verifier.SAW.SATQuery (SATQuery(..))
 
 import           SAWScript.Proof(Sequent, sequentToSATQuery, CEX)
-import           SAWScript.Value (TopLevel, io, getSharedContext)
+import           SAWScript.Value (TopLevel, io, getSharedContext, rwWhat4PushMuxOps)
 
 import           Data.Parameterized.Nonce
 
@@ -41,15 +42,21 @@ import qualified What4.Expr.Builder as B
 -- trivial state
 data St t = St
 
-setupWhat4_sym :: Bool -> IO (B.ExprBuilder
-                              GlobalNonceGenerator
-                              St
-                              (B.Flags B.FloatReal))
-setupWhat4_sym hashConsing =
+setupWhat4_sym ::
+  Bool ->
+  Bool ->
+  IO (B.ExprBuilder
+      GlobalNonceGenerator
+      St
+      (B.Flags B.FloatReal))
+setupWhat4_sym hashConsing what4PushMuxOps =
   do -- TODO: get rid of GlobalNonceGenerator ???
      sym <- B.newExprBuilder B.FloatRealRepr St globalNonceGenerator
-     cacheTermsSetting <- getOptionSetting B.cacheTerms $ getConfiguration sym
+     let cfg = getConfiguration sym
+     cacheTermsSetting <- getOptionSetting B.cacheTerms cfg
      _ <- setOpt cacheTermsSetting hashConsing
+     pushMuxOpsSetting <- getOptionSetting B.pushMuxOpsOption cfg
+     _ <- setOpt pushMuxOpsSetting what4PushMuxOps
      return sym
 
 what4Theories ::
@@ -57,9 +64,11 @@ what4Theories ::
   Bool ->
   Sequent ->
   TopLevel [String]
-what4Theories unintSet hashConsing goal =
-  getSharedContext >>= \sc -> io $
-  do sym <- setupWhat4_sym hashConsing
+what4Theories unintSet hashConsing goal = do
+  sc <- getSharedContext
+  what4PushMuxOps <- gets rwWhat4PushMuxOps
+  io $ do
+     sym <- setupWhat4_sym hashConsing what4PushMuxOps
      satq <- sequentToSATQuery sc unintSet goal
      (_varMap, lits) <- W.w4Solve sym sc satq
      let pf lit = (predicateVarInfo lit)^.problemFeatures
@@ -86,9 +95,11 @@ proveWhat4_sym ::
   Bool ->
   SATQuery ->
   TopLevel (Maybe CEX, String)
-proveWhat4_sym solver hashConsing satq =
-  getSharedContext >>= \sc -> io $
-  do sym <- setupWhat4_sym hashConsing
+proveWhat4_sym solver hashConsing satq = do
+  sc <- getSharedContext
+  what4PushMuxOps <- gets rwWhat4PushMuxOps
+  io $ do
+     sym <- setupWhat4_sym hashConsing what4PushMuxOps
      proveWhat4_solver solver sym sc satq (return ())
 
 proveExportWhat4_sym ::
@@ -97,9 +108,11 @@ proveExportWhat4_sym ::
   FilePath ->
   SATQuery ->
   TopLevel (Maybe CEX, String)
-proveExportWhat4_sym solver hashConsing outFilePath satq =
-  getSharedContext >>= \sc -> io $
-  do sym <- setupWhat4_sym hashConsing
+proveExportWhat4_sym solver hashConsing outFilePath satq = do
+  sc <- getSharedContext
+  what4PushMuxOps <- gets rwWhat4PushMuxOps
+  io $ do
+     sym <- setupWhat4_sym hashConsing what4PushMuxOps
 
      -- Write smt out
      (_, _, lits, solver_name) <- setupWhat4_solver solver sym sc satq
@@ -131,9 +144,11 @@ proveWhat4_z3_using ::
   Bool          {- ^ Hash-consing of What4 terms -}->
   SATQuery      {- ^ The query to be proved -} ->
   TopLevel (Maybe CEX, String)
-proveWhat4_z3_using tactic hashConsing satq =
-  getSharedContext >>= \sc -> io $
-  do sym <- setupWhat4_sym hashConsing
+proveWhat4_z3_using tactic hashConsing satq = do
+  sc <- getSharedContext
+  what4PushMuxOps <- gets rwWhat4PushMuxOps
+  io $ do
+     sym <- setupWhat4_sym hashConsing what4PushMuxOps
      proveWhat4_solver z3Adapter sym sc satq $
        do z3TacticSetting <- getOptionSetting z3Tactic $ getConfiguration sym
           _ <- setOpt z3TacticSetting $ Text.pack tactic
diff --git a/src/SAWScript/Value.hs b/src/SAWScript/Value.hs
index 709b422a58..282ba109f6 100644
--- a/src/SAWScript/Value.hs
+++ b/src/SAWScript/Value.hs
@@ -333,7 +333,7 @@ showRefnset opts ss =
     ppFunAssumpRHS ctx (OpaqueFunAssump f args) =
       ppTermAppInCtx opts' ctx (funNameTerm f) args
     ppFunAssumpRHS ctx (RewriteFunAssump rhs) =
-      SAWCorePP.ppTermInCtx opts' (map fst $ mrVarCtxInnerToOuter ctx) rhs 
+      SAWCorePP.ppTermInCtx opts' (map fst $ mrVarCtxInnerToOuter ctx) rhs
     opts' = sawPPOpts opts
 
 showsPrecValue :: PPOpts -> SAWNamingEnv -> Int -> Value -> ShowS
@@ -587,6 +587,9 @@ data TopLevelRW =
 
   , rwAllocSymInitCheck :: Bool
 
+  , rwWhat4PushMuxOps :: Bool
+  , rwNoSatisfyingWriteFreshConstant :: Bool
+
   , rwCrucibleTimeout :: Integer
 
   , rwPathSatSolver :: Common.PathSatSolver
@@ -952,7 +955,8 @@ runProofScript (ProofScript m) concl gl ploc rsn recordThm useSequentGoals =
        Right _ ->
          do sc <- getSharedContext
             db <- getTheoremDB
-            (thmResult, db') <- io (finishProof sc db concl pstate recordThm useSequentGoals)
+            what4PushMuxOps <- gets rwWhat4PushMuxOps
+            (thmResult, db') <- io (finishProof sc db concl pstate recordThm useSequentGoals what4PushMuxOps)
             putTheoremDB db'
             pure thmResult
 
diff --git a/src/SAWScript/X86.hs b/src/SAWScript/X86.hs
index e61a44b0dd..c3ef53d37e 100644
--- a/src/SAWScript/X86.hs
+++ b/src/SAWScript/X86.hs
@@ -209,7 +209,7 @@ proof fileReader pss archi file mbCry globs fun =
      halloc  <- newHandleAllocator
      scLoadPreludeModule sc
      scLoadCryptolModule sc
-     sym <- newSAWCoreExprBuilder sc
+     sym <- newSAWCoreExprBuilder sc False
      SomeOnlineBackend bak <- newSAWCoreBackend pss sym
      let ?fileReader = fileReader
      cenv <- loadCry sym mbCry
diff --git a/src/SAWScript/Yosys.hs b/src/SAWScript/Yosys.hs
index fbcd657886..2cc2d18667 100644
--- a/src/SAWScript/Yosys.hs
+++ b/src/SAWScript/Yosys.hs
@@ -252,5 +252,5 @@ yosys_verify_sequential_sally ::
   TopLevel ()
 yosys_verify_sequential_sally s path q fixed = do
   sc <- getSharedContext
-  sym <- liftIO $ Common.newSAWCoreExprBuilder sc
+  sym <- liftIO $ Common.newSAWCoreExprBuilder sc False
   queryModelChecker sym sc s path q . Set.fromList $ Text.pack <$> fixed