diff --git a/src/SAWScript/Crucible/LLVM/Builtins.hs b/src/SAWScript/Crucible/LLVM/Builtins.hs
index 909f6ef01d..a2042501b3 100644
--- a/src/SAWScript/Crucible/LLVM/Builtins.hs
+++ b/src/SAWScript/Crucible/LLVM/Builtins.hs
@@ -80,6 +80,7 @@ module SAWScript.Crucible.LLVM.Builtins
     , findDecl
     , findDefMaybeStatic
     , setupLLVMCrucibleContext
+    , setupPrestateConditions
     , checkSpecReturnType
     , verifyPrestate
     , verifyPoststate
diff --git a/src/SAWScript/Crucible/LLVM/X86.hs b/src/SAWScript/Crucible/LLVM/X86.hs
index 568c85759c..81518c9dde 100644
--- a/src/SAWScript/Crucible/LLVM/X86.hs
+++ b/src/SAWScript/Crucible/LLVM/X86.hs
@@ -474,12 +474,24 @@ llvm_verify_x86_common (Some (llvmModule :: LLVMModule x)) path nm globsyms chec
               , C._cruciblePersonality = Macaw.MacawSimulatorState
               , C._profilingMetrics = Map.empty
               }
-        globals = C.insertGlobal mvar (preState ^. x86Mem) C.emptyGlobals
+
+      (globals, assumes) <-
+          do let globals0 = C.insertGlobal mvar (preState ^. x86Mem) C.emptyGlobals
+             liftIO $ setupPrestateConditions methodSpec cc (preState ^. x86Mem) env globals0
+                       (methodSpec ^. MS.csPreState . MS.csConditions)
+
+      let
         macawStructRepr = C.StructRepr $ Macaw.crucArchRegTypes Macaw.x86_64MacawSymbolicFns
         initial = C.InitialState ctx globals C.defaultAbortHandler macawStructRepr
                   $ C.runOverrideSim macawStructRepr
                   $ Macaw.crucGenArchConstraints Macaw.x86_64MacawSymbolicFns
                   $ do
+          liftIO $
+            forM_ assumes $ \(C.LabeledPred p (md, reason)) ->
+              do expr <- resolveSAWPred cc p
+                 let loc = MS.conditionLoc md
+                 C.addAssumption bak
+                   (C.GenericAssumption loc reason expr)
           r <- C.callCFG cfg . C.RegMap . singleton . C.RegEntry macawStructRepr $ preState ^. x86Regs
           globals' <- C.readGlobals
           mem' <- C.readGlobal mvar
@@ -1083,9 +1095,6 @@ assertPost globals env premem preregs mdMap = do
   pointsToMatches <- forM (ms ^. MS.csPostState . MS.csPointsTos)
     $ assertPointsTo env tyenv nameEnv
 
-  let setupConditionMatchesPre = fmap -- assume preconditions
-        (LO.executeSetupCondition opts sc cc ms)
-        $ ms ^. MS.csPreState . MS.csConditions
   let setupConditionMatchesPost = fmap -- assert postconditions
         (LO.learnSetupCondition opts sc cc ms MS.PostState)
         $ ms ^. MS.csPostState . MS.csConditions
@@ -1105,15 +1114,12 @@ assertPost globals env premem preregs mdMap = do
     . sequence_ $ mconcat
     [ returnMatches
     , pointsToMatches
-    , setupConditionMatchesPre
     , setupConditionMatchesPost
     , [LO.assertTermEqualities sc cc]
     ]
   st <- case result of
     Left err -> throwX86 $ show err
     Right (_, st) -> pure st
-  liftIO . forM_ (view O.osAssumes st) $ \(_md, asum) ->
-    C.addAssumption bak $ C.GenericAssumption (st ^. O.osLocation) "precondition" asum
   liftIO . forM_ (view LO.osAsserts st) $ \(md, W4.LabeledPred p r) ->
        do (ann,p') <- W4.annotateTerm sym p
           modifyIORef mdMap (Map.insert ann md)