From c146d10e828eb90afe1a6a32ca9ae87692000a7a Mon Sep 17 00:00:00 2001
From: Shilpi Goel <shigoel@gmail.com>
Date: Fri, 30 Jan 2026 14:19:10 -0600
Subject: [PATCH 1/3] Checkpoint

---
 Strata/DL/Imperative/CmdEval.lean             |   8 +-
 Strata/DL/Imperative/EvalContext.lean         |   2 +
 Strata/DL/Imperative/SMTUtils.lean            |   3 +-
 Strata/DL/SMT/Solver.lean                     |   4 +-
 Strata/Languages/B3/Verifier/Diagnosis.lean   |   3 +-
 Strata/Languages/B3/Verifier/State.lean       |   6 +-
 Strata/Languages/Core/Env.lean                |   2 +-
 Strata/Languages/Core/Options.lean            |   2 +
 Strata/Languages/Core/SMTEncoder.lean         |  16 +-
 Strata/Languages/Core/StatementEval.lean      |  17 +-
 Strata/Languages/Core/Verifier.lean           | 326 ++++++++++++------
 StrataTest/Languages/Core/Examples/Cover.lean |  18 +-
 .../Languages/Core/Examples/TypeDecl.lean     |   2 +-
 StrataTest/Languages/Core/ExprEvalTest.lean   |   4 +-
 14 files changed, 284 insertions(+), 129 deletions(-)

diff --git a/Strata/DL/Imperative/CmdEval.lean b/Strata/DL/Imperative/CmdEval.lean
index 538ecc978..08a1f1c3a 100644
--- a/Strata/DL/Imperative/CmdEval.lean
+++ b/Strata/DL/Imperative/CmdEval.lean
@@ -58,14 +58,14 @@ def Cmd.eval [EC : EvalContext P S] (σ : S) (c : Cmd P) : Cmd P × S :=
       let c' := .assert label e md
       match EC.denoteBool e with
       | some true => -- Proved via evaluation.
-        (c', EC.deferObligation σ (ProofObligation.mk label .assert assumptions e md))
+        (c', EC.deferObligation σ (ProofObligation.mk label .assert false assumptions e md))
       | some false =>
         if assumptions.isEmpty then
           (c', EC.updateError σ (.AssertFail label e))
         else
-          (c', EC.deferObligation σ (ProofObligation.mk label .assert assumptions e md))
+          (c', EC.deferObligation σ (ProofObligation.mk label .assert false assumptions e md))
       | none =>
-        (c', EC.deferObligation σ (ProofObligation.mk label .assert assumptions e md))
+        (c', EC.deferObligation σ (ProofObligation.mk label .assert false assumptions e md))
 
     | .assume label e md =>
       let (e, σ) := EC.preprocess σ c e
@@ -85,7 +85,7 @@ def Cmd.eval [EC : EvalContext P S] (σ : S) (c : Cmd P) : Cmd P × S :=
       let e := EC.eval σ e
       let assumptions := EC.getPathConditions σ
       let c' := .cover label e md
-      (c', EC.deferObligation σ (ProofObligation.mk label .cover assumptions e md))
+      (c', EC.deferObligation σ (ProofObligation.mk label .cover false assumptions e md))
 
 /--
 Partial evaluator for Imperative's Commands.
diff --git a/Strata/DL/Imperative/EvalContext.lean b/Strata/DL/Imperative/EvalContext.lean
index 218c3bea8..4cdb627bf 100644
--- a/Strata/DL/Imperative/EvalContext.lean
+++ b/Strata/DL/Imperative/EvalContext.lean
@@ -85,6 +85,8 @@ decision procedure or via denotation into Lean.
 structure ProofObligation (P : PureExpr) where
   label : String
   property : PropertyType
+  /-- Check if assumptions are satisfiable. -/
+  checkAssumptionsSat : Bool := false
   assumptions : PathConditions P
   obligation : P.Expr
   metadata : MetaData P
diff --git a/Strata/DL/Imperative/SMTUtils.lean b/Strata/DL/Imperative/SMTUtils.lean
index 89a57819c..2872ce7cb 100644
--- a/Strata/DL/Imperative/SMTUtils.lean
+++ b/Strata/DL/Imperative/SMTUtils.lean
@@ -151,7 +151,8 @@ def dischargeObligation {P : PureExpr} [ToFormat P.Ident]
   let handle ← IO.FS.Handle.mk filename IO.FS.Mode.write
   let solver ← Strata.SMT.Solver.fileWriter handle
   let (ids, estate) ← encodeTerms terms solver
-  let _ ← solver.checkSat ids -- Will return unknown for Solver.fileWriter
+  let _ ← solver.checkSat
+  let _ ← solver.getDecision ids -- Will return unknown for Solver.fileWriter
   let produce_models ←
     if smtsolver.endsWith "z3" then
       -- No need to specify -model because we already have `get-value` in the
diff --git a/Strata/DL/SMT/Solver.lean b/Strata/DL/SMT/Solver.lean
index ca6f3b0b4..d4ac93fe1 100644
--- a/Strata/DL/SMT/Solver.lean
+++ b/Strata/DL/SMT/Solver.lean
@@ -150,8 +150,10 @@ private def readlnD (dflt : String) : SolverM String := do
   | .some stdout => stdout.getLine
   | .none        => pure dflt
 
-def checkSat (vars : List String) : SolverM Decision := do
+def checkSat : SolverM Unit :=
   emitln "(check-sat)"
+
+def getDecision (vars : List String) : SolverM Decision := do
   let result := (← readlnD "unknown").trim
   match result with
   | "sat"     =>
diff --git a/Strata/Languages/B3/Verifier/Diagnosis.lean b/Strata/Languages/B3/Verifier/Diagnosis.lean
index 72d1bed37..2e14b297b 100644
--- a/Strata/Languages/B3/Verifier/Diagnosis.lean
+++ b/Strata/Languages/B3/Verifier/Diagnosis.lean
@@ -91,7 +91,8 @@ partial def diagnoseFailureGeneric
       let _ ← push checkState
       let runCheck : SolverM Decision := do
         Solver.assert (formatTermDirect convResult.term)
-        Solver.checkSat []
+        Solver.checkSat
+        Solver.getDecision []
       let decision ← runCheck.run checkState.smtState.solver
       let _ ← pop checkState
       let isProvablyFalse := decision == .unsat
diff --git a/Strata/Languages/B3/Verifier/State.lean b/Strata/Languages/B3/Verifier/State.lean
index caedc2312..da9477c7b 100644
--- a/Strata/Languages/B3/Verifier/State.lean
+++ b/Strata/Languages/B3/Verifier/State.lean
@@ -138,7 +138,8 @@ def prove (state : B3VerificationState) (term : Term) (ctx : VerificationContext
   let _ ← push state
   let runCheck : SolverM (Decision × Option String) := do
     Solver.assert s!"(not {formatTermDirect term})"
-    let decision ← Solver.checkSat []
+    let _ ← Solver.checkSat
+    let decision ← Solver.getDecision []
     let model := if decision == .sat then some "model available" else none
     return (decision, model)
   let (decision, model) ← runCheck.run state.smtState.solver
@@ -154,7 +155,8 @@ def reach (state : B3VerificationState) (term : Term) (ctx : VerificationContext
   let _ ← push state
   let runCheck : SolverM (Decision × Option String) := do
     Solver.assert (formatTermDirect term)
-    let decision ← Solver.checkSat []
+    let _ ← Solver.checkSat
+    let decision ← Solver.getDecision []
     let model := if decision == .sat then some "reachable" else none
     return (decision, model)
   let (decision, model) ← runCheck.run state.smtState.solver
diff --git a/Strata/Languages/Core/Env.lean b/Strata/Languages/Core/Env.lean
index 598af6a2f..a8b51d064 100644
--- a/Strata/Languages/Core/Env.lean
+++ b/Strata/Languages/Core/Env.lean
@@ -107,7 +107,7 @@ def ProofObligation.create
     dbg_trace f!"{Format.line}Obligation {label} is free!{Format.line}"
     none
   else
-    some (ProofObligation.mk label propertyType assumptions obligation.expr obligation.md)
+    some (ProofObligation.mk label propertyType false assumptions obligation.expr obligation.md)
 
 def ProofObligations.createAssertions
   (assumptions : PathConditions Expression)
diff --git a/Strata/Languages/Core/Options.lean b/Strata/Languages/Core/Options.lean
index bde5e2afc..8eed2dbc2 100644
--- a/Strata/Languages/Core/Options.lean
+++ b/Strata/Languages/Core/Options.lean
@@ -43,6 +43,7 @@ structure Options where
   checkOnly : Bool
   stopOnFirstError : Bool
   removeIrrelevantAxioms : Bool
+  checkAssumptionsSat : Bool
   /-- Solver time limit in seconds -/
   solverTimeout : Nat
   /-- Output results in SARIF format -/
@@ -55,6 +56,7 @@ def Options.default : Options := {
   checkOnly := false,
   stopOnFirstError := false,
   removeIrrelevantAxioms := false,
+  checkAssumptionsSat := false,
   solverTimeout := 10,
   outputSarif := false
 }
diff --git a/Strata/Languages/Core/SMTEncoder.lean b/Strata/Languages/Core/SMTEncoder.lean
index 71878c632..a7156f231 100644
--- a/Strata/Languages/Core/SMTEncoder.lean
+++ b/Strata/Languages/Core/SMTEncoder.lean
@@ -565,6 +565,11 @@ def toSMTTerms (E : Env) (es : List (LExpr CoreLParams.mono)) (ctx : SMT.Context
     let (erestt, ctx) ← toSMTTerms E erest ctx
     .ok ((et :: erestt), ctx)
 
+structure SMT.Obligation where
+  assumptions : List Term
+  obligation : Term
+  checkAssumptionsSat : Bool := false
+
 /--
 Encode a proof obligation -- which may be of type `assert` or `cover` -- into
 SMTLIB.
@@ -587,9 +592,9 @@ Under conditions `P`, `cover(Q)` is encoded into SMTLib as follows:
 If the result is `unsat`, then `P ∧ Q` is unsatisfiable, which means that the
 cover is violated. If the result is `sat`, then the cover succeeds.
 -/
-def ProofObligation.toSMTTerms (E : Env)
-  (d : Imperative.ProofObligation Expression) (ctx : SMT.Context := SMT.Context.default) :
-  Except Format ((List Term) × SMT.Context) := do
+def ProofObligation.toSMTObligation (E : Env)
+    (d : Imperative.ProofObligation Expression) (ctx : SMT.Context := SMT.Context.default) :
+    Except Format (SMT.Obligation × SMT.Context) := do
   let assumptions := d.assumptions.flatten.map (fun a => a.snd)
   let (ctx, distinct_terms) ← E.distinct.foldlM (λ (ctx, tss) es =>
     do let (ts, ctx') ← Core.toSMTTerms E es ctx; pure (ctx', ts :: tss)) (ctx, [])
@@ -602,7 +607,10 @@ def ProofObligation.toSMTTerms (E : Env)
       obligation_pos_term
     else
       Factory.not obligation_pos_term
-  .ok ((distinct_assumptions ++ assumptions_terms ++ [obligation_term]), ctx)
+  .ok ({assumptions := distinct_assumptions ++ assumptions_terms,
+        obligation := obligation_term,
+        checkAssumptionsSat := d.checkAssumptionsSat },
+       ctx)
 
 ---------------------------------------------------------------------
 
diff --git a/Strata/Languages/Core/StatementEval.lean b/Strata/Languages/Core/StatementEval.lean
index 16ed8b5b8..8f601789d 100644
--- a/Strata/Languages/Core/StatementEval.lean
+++ b/Strata/Languages/Core/StatementEval.lean
@@ -262,19 +262,24 @@ def Statements.collectAsserts (ss : Statements) : List (String × Imperative.Met
   termination_by Imperative.Block.sizeOf ss
 end
 
-def createFailingCoverObligations
+private def createUnreachableCoverObligations
     (covers : List (String × Imperative.MetaData Expression)) :
     Imperative.ProofObligations Expression :=
   covers.toArray.map
     (fun (label, md) =>
-      (Imperative.ProofObligation.mk label .cover [] (LExpr.false ()) md))
+      (Imperative.ProofObligation.mk label .cover
+        false
+        [[("unreachable", (LExpr.false ()))]]
+        (LExpr.false ()) md))
 
-def createPassingAssertObligations
+private def createUnreachableAssertObligations
     (asserts : List (String × Imperative.MetaData Expression)) :
     Imperative.ProofObligations Expression :=
   asserts.toArray.map
     (fun (label, md) =>
-      (Imperative.ProofObligation.mk label .assert [] (LExpr.true ()) md))
+      (Imperative.ProofObligation.mk label .assert false
+        [[("unreachable", (LExpr.false ()))]]
+        (LExpr.true ()) md))
 
 abbrev StmtsStack := List Statements
 
@@ -371,8 +376,8 @@ def evalAuxGo (steps : Nat) (old_var_subst : SubstMap) (Ewn : EnvWithNext) (ss :
                 if Statements.containsCovers ss_f || Statements.containsAsserts ss_f then
                   let ss_f_covers := Statements.collectCovers ss_f
                   let ss_f_asserts := Statements.collectAsserts ss_f
-                  let deferred := createFailingCoverObligations ss_f_covers
-                  let deferred := deferred ++ createPassingAssertObligations ss_f_asserts
+                  let deferred := createUnreachableCoverObligations ss_f_covers
+                  let deferred := deferred ++ createUnreachableAssertObligations ss_f_asserts
                   [{ Ewn with env.deferred := Ewn.env.deferred ++ deferred }]
                 else
                   []
diff --git a/Strata/Languages/Core/Verifier.lean b/Strata/Languages/Core/Verifier.lean
index 9bfb83310..3e5f8f6c1 100644
--- a/Strata/Languages/Core/Verifier.lean
+++ b/Strata/Languages/Core/Verifier.lean
@@ -15,34 +15,6 @@ import Strata.DDM.AST
 
 ---------------------------------------------------------------------
 
-namespace Strata.SMT.Encoder
-
-open Strata.SMT.Encoder
-open Strata
-
--- Derived from Strata.SMT.Encoder.encode.
-def encodeCore (ctx : Core.SMT.Context) (prelude : SolverM Unit) (ts : List Term) :
-  SolverM (List String × EncoderState) := do
-  Solver.reset
-  Solver.setLogic "ALL"
-  prelude
-  let _ ← ctx.sorts.mapM (fun s => Solver.declareSort s.name s.arity)
-  ctx.emitDatatypes
-  let (_ufs, estate) ← ctx.ufs.mapM (fun uf => encodeUF uf) |>.run EncoderState.init
-  let (_ifs, estate) ← ctx.ifs.mapM (fun fn => encodeFunction fn.uf fn.body) |>.run estate
-  let (_axms, estate) ← ctx.axms.mapM (fun ax => encodeTerm False ax) |>.run estate
-  for id in _axms do
-    Solver.assert id
-  let (ids, estate) ← ts.mapM (encodeTerm False) |>.run estate
-  for id in ids do
-    Solver.assert id
-  let ids := estate.ufs.values
-  return (ids, estate)
-
-end Strata.SMT.Encoder
-
----------------------------------------------------------------------
-
 namespace Core.SMT
 open Std (ToFormat Format format)
 open Lambda Strata.SMT
@@ -100,7 +72,7 @@ inductive Result where
   | unsat
   | unknown
   | err (msg : String)
-deriving DecidableEq, Repr
+deriving DecidableEq, Repr, Inhabited
 
 def Result.isSat (r : Result) : Bool :=
   match r with | .sat _ => true | _ => false
@@ -132,21 +104,17 @@ def runSolver (solver : String) (args : Array String) : IO IO.Process.Output :=
     cmd := solver
     args := args
   }
-  -- dbg_trace f!"runSolver: exitcode: {repr output.exitCode}\n\
-  --                         stderr: {repr output.stderr}\n\
-  --                         stdout: {repr output.stdout}"
   return output
 
-def solverResult (vars : List (IdentT LMonoTy Visibility)) (output : IO.Process.Output)
-    (ctx : SMT.Context) (E : EncoderState) :
-  Except Format Result := do
-  let stdout := output.stdout
-  let pos := (stdout.find (fun c => c == '\n')).byteIdx
-  let verdict := (stdout.take pos).trim
-  let rest := stdout.drop pos
+-- def readLinesUntilVerdict (lines : List String) : List String × List String :=
+
+
+def parseVerdictWithModel (vars : List (IdentT LMonoTy Visibility))
+    (verdict model : String) (ctx : SMT.Context) (E : EncoderState) :
+    Except Format Result := do
   match verdict with
   | "sat"     =>
-    let rawModel ← getModel rest
+    let rawModel ← getModel model
     -- We suppress any model processing errors.
     -- Likely, these would be because of the suboptimal implementation
     -- of the model parser, which shouldn't hold back useful
@@ -155,8 +123,45 @@ def solverResult (vars : List (IdentT LMonoTy Visibility)) (output : IO.Process.
     | .ok model => .ok (.sat model)
     | .error _model_err => (.ok (.sat []))
   | "unsat"   =>  .ok .unsat
-  | "unknown" =>  .ok .unknown
-  | _     =>  .error s!"stderr:{output.stderr}\nsolver stdout: {output.stdout}\n"
+  | _ =>  .ok .unknown
+
+partial def parseVerdictsWithModel (vars : List (IdentT LMonoTy Visibility))
+    (lines : List String) (ctx : SMT.Context) (E : EncoderState) :
+    Except Format (List Result) := do
+  dbg_trace f!"lines: {lines}"
+  match lines with
+  | [] =>
+    .ok []
+  | verdict :: model :: rest =>
+    if !isVerdict verdict then
+      .error f!"SMT Solver Error! Ill-formed verdict: {verdict}"
+    else
+      let (modelStr, restLines) := if isVerdict model then ("", model :: rest) else (model, rest)
+      let result ← parseVerdictWithModel vars verdict modelStr ctx E
+      let restResult ← parseVerdictsWithModel vars restLines ctx E
+      return (result :: restResult)
+  | verdict :: rest =>
+    if !isVerdict verdict then
+      .error f!"SMT Solver Error! Ill-formed verdict: {verdict}"
+    else
+      let result ← parseVerdictWithModel vars verdict "" ctx E
+      let restResult ← parseVerdictsWithModel vars rest ctx E
+      return (result :: restResult)
+  where isVerdict (s : String) : Bool :=
+    s ∈ ["unsat", "sat", "unknown"]
+
+/--
+Parse SMT solver output from (possibly) multiple `check-sat` calls.
+Returns a list of results in order, where each result corresponds to one
+`check-sat`.
+-/
+def solverResults (vars : List (IdentT LMonoTy Visibility))
+    (output : IO.Process.Output) (ctx : SMT.Context) (E : EncoderState) :
+    Except Format (List Result) := do
+  let lines := (output.stdout.splitOn "\n").map String.trim
+  let lines := lines.filter (fun s => !s.isEmpty)
+  parseVerdictsWithModel vars lines ctx E |>.mapError
+      (fun e => f!"{e}\nStdErr: {output.stderr}\nExit Code: {output.exitCode}")
 
 def getSolverPrelude : String → SolverM Unit
 | "z3" => do
@@ -171,7 +176,9 @@ def getSolverPrelude : String → SolverM Unit
 def getSolverFlags (options : Options) (solver : String) : Array String :=
   let produceModels :=
     match solver with
-    | "cvc5" => #["--produce-models"]
+    -- Running cvc5 with `--incremental` is okay even if we have only one
+    -- check-sat in the SMTLib file.
+    | "cvc5" => #["--incremental", "--produce-models"]
     -- No need to specify -model for Z3 because we already have `get-value`
     -- in the generated SMT file.
     | _ => #[]
@@ -182,22 +189,57 @@ def getSolverFlags (options : Options) (solver : String) : Array String :=
     | _ => #[]
   produceModels ++ setTimeout
 
+open Strata.SMT.Encoder in
+-- Derived from Strata.SMT.Encoder.encode.
+def encodeObligation (ctx : Core.SMT.Context) (prelude : SolverM Unit)
+    (ob : SMT.Obligation) : SolverM EncoderState := do
+  Solver.reset
+  Solver.setLogic "ALL"
+  prelude
+  let _ ← ctx.sorts.mapM (fun s => Solver.declareSort s.name s.arity)
+  ctx.emitDatatypes
+  let (_ufs, estate) ← ctx.ufs.mapM (fun uf => encodeUF uf) |>.run EncoderState.init
+  let (_ifs, estate) ← ctx.ifs.mapM (fun fn => encodeFunction fn.uf fn.body) |>.run estate
+  let (_axms, estate) ← ctx.axms.mapM (fun ax => encodeTerm False ax) |>.run estate
+  for id in _axms do
+    Solver.assert id
+  let estate ←
+    if ob.checkAssumptionsSat then do
+      let (assumption_ids, estate) ← ob.assumptions.mapM (encodeTerm False) |>.run estate
+      for id in assumption_ids do
+        Solver.assert id
+      Solver.checkSat
+      if !estate.ufs.values.isEmpty then Solver.getValue estate.ufs.values
+      let (conclusion_id, estate) ← (encodeTerm False ob.obligation) |>.run estate
+      Solver.assert conclusion_id
+      Solver.checkSat
+      if !estate.ufs.values.isEmpty then Solver.getValue estate.ufs.values
+      pure estate
+    else do
+      let terms := ob.assumptions ++ [ob.obligation]
+      let (ids, estate) ← terms.mapM (encodeTerm False) |>.run estate
+      for id in ids do
+        Solver.assert id
+      Solver.checkSat
+      if !estate.ufs.values.isEmpty then Solver.getValue estate.ufs.values
+      pure estate
+  return estate
+
 def dischargeObligation
   (options : Options)
   (vars : List (IdentT LMonoTy Visibility)) (smtsolver filename : String)
-  (terms : List Term) (ctx : SMT.Context)
-  : IO (Except Format (SMT.Result × EncoderState)) := do
+  (ob : SMT.Obligation) (ctx : SMT.Context)
+  : IO (Except Format (List SMT.Result × EncoderState)) := do
   let handle ← IO.FS.Handle.mk filename IO.FS.Mode.write
   let solver ← Solver.fileWriter handle
   let prelude := getSolverPrelude smtsolver
-  let (ids, estate) ← Strata.SMT.Encoder.encodeCore ctx prelude terms solver
-  let _ ← solver.checkSat ids -- Will return unknown for Solver.fileWriter
+  let estate ← encodeObligation ctx prelude ob solver
   if options.verbose > .normal then IO.println s!"Wrote problem to {filename}."
   let flags := getSolverFlags options smtsolver
   let output ← runSolver smtsolver (#[filename] ++ flags)
-  match SMT.solverResult vars output ctx estate with
+  match SMT.solverResults vars output ctx estate with
   | .error e => return .error e
-  | .ok result => return .ok (result, estate)
+  | .ok results => return .ok (results, estate)
 
 end Core.SMT
 ---------------------------------------------------------------------
@@ -230,26 +272,35 @@ analysis.
 -/
 structure VCResult where
   obligation : Imperative.ProofObligation Expression
-  smtResult : SMT.Result := .unknown
+  -- `.none` when the proof obligation doesn't require assumption sat checks.
+  assumptionsSat : Option Outcome := .none
+  assumptionSatSMTResult : SMT.Result := .unknown
   result : Outcome := .unknown
+  smtResult : SMT.Result := .unknown
   estate : EncoderState := EncoderState.init
   verbose : VerboseMode := .normal
 
 /--
 Map the result from an SMT backend engine to an `Outcome`.
 -/
-def smtResultToOutcome (r : SMT.Result) (isCover : Bool) : Outcome :=
+def smtResultToOutcome (r : SMT.Result) (satIsPass : Bool) : Outcome :=
   match r with
   | .unknown => .unknown
   | .unsat =>
-    if isCover then .fail else .pass
+    if satIsPass then .fail else .pass
   | .sat _ =>
-    if isCover then .pass else .fail
+    if satIsPass then .pass else .fail
   | .err e => .implementationError e
 
 instance : ToFormat VCResult where
-  format r := f!"Obligation: {r.obligation.label}\n\
+  format r :=
+  let assumptionCheckResult :=
+    match r.assumptionsSat with
+    | .none => f!""
+    | some r => f!"Assumptions Sat Check: {r}\n"
+  f!"Obligation: {r.obligation.label}\n\
                  Property: {r.obligation.property}\n\
+                 {assumptionCheckResult}\
                  Result: {r.result}\
                  {r.smtResult.formatModelIfSat true}"
 
@@ -285,51 +336,87 @@ Preprocess a proof obligation before handing it off to a backend engine.
 -/
 def preprocessObligation (obligation : ProofObligation Expression) (p : Program)
     (options : Options) : EIO DiagnosticModel (ProofObligation Expression × Option VCResult) := do
-  match obligation.property with
-  | .cover =>
-    if obligation.obligation.isFalse then
-      -- If PE determines that the consequent is false, then we can immediately
-      -- report a failure.
-      let result := { obligation, result := .fail, verbose :=  options.verbose }
-      return (obligation, some result)
-    else
-      return (obligation, none)
-  | .assert =>
-    if obligation.obligation.isTrue then
-      -- We don't need the SMT solver if PE (partial evaluation) is enough to
-      -- reduce the consequent to true.
-      let result := { obligation, result := .pass, verbose := options.verbose }
-      return (obligation, some result)
-    else if obligation.obligation.isFalse && obligation.assumptions.isEmpty then
-      -- If PE determines that the consequent is false and the path conditions
-      -- are empty, then we can immediately report a verification failure. Note
-      -- that we go to the SMT solver if the path conditions aren't empty --
-      -- after all, the path conditions could imply false, which the PE isn't
-      -- capable enough to infer.
-      let prog := f!"\n\nEvaluated program:\n{p}"
-      dbg_trace f!"\n\nObligation {obligation.label}: failed!\
-                   \n\nResult obtained during partial evaluation.\
-                   {if options.verbose >= .normal then prog else ""}"
-      let result := { obligation, result := .fail, verbose := options.verbose }
-      return (obligation, some result)
-    else if options.removeIrrelevantAxioms then
-      -- We attempt to prune the path conditions by excluding all irrelevant
-      -- axioms w.r.t. the consequent to reduce the size of the proof
-      -- obligation.
-      let cg := Program.toFunctionCG p
-      let fns := obligation.obligation.getOps.map CoreIdent.toPretty
-      let relevant_fns := (fns ++ (CallGraph.getAllCalleesClosure cg fns)).dedup
-      let irrelevant_axs := Program.getIrrelevantAxioms p relevant_fns
-      let new_assumptions := Imperative.PathConditions.removeByNames obligation.assumptions irrelevant_axs
-      return ({ obligation with assumptions := new_assumptions }, none)
-    else
-      return (obligation, none)
+  -- First, we check whether we can return a result immediately based on
+  -- satisfiability of assumptions alone.
+  let checkAssumptionsStatus :=
+    match obligation.checkAssumptionsSat with
+    | true =>
+      if obligation.assumptions.isEmpty then
+        -- No assumptions to check; can process consequent next.
+        some Outcome.pass
+      else if obligation.assumptions.flatten.any (fun (_, e) => e.isFalse) then
+        -- Unsat assumptions; can exit early.
+        some Outcome.fail
+      else -- Exit to use a backend solver.
+        some Outcome.unknown
+    | false =>
+      -- Assumption satisfiability check not requested.
+      -- Can process consequent next.
+      .none
+  match checkAssumptionsStatus with
+  | some .fail => -- Exit early.
+    let result := { obligation,
+                    assumptionsSat := checkAssumptionsStatus,
+                    result := (match obligation.property with
+                              | .assert => .pass
+                              | .cover => .fail),
+                    verbose := options.verbose }
+    return (obligation, some result)
+  | .some .unknown =>
+    -- Exit early. We need a backend solver for further processing.
+    return (obligation, none)
+  | _ => -- Continue preprocessing.
+    match obligation.property with
+    | .cover =>
+      if obligation.obligation.isFalse then
+        -- If PE determines that the consequent is false, then the cover fails.
+        let result := { obligation,
+                        assumptionsSat := checkAssumptionsStatus,
+                        result := .fail, verbose := options.verbose }
+        return (obligation, some result)
+      else
+        return (obligation, none)
+    | .assert =>
+      if obligation.obligation.isTrue then
+        -- We don't need the SMT solver if PE (partial evaluation) is enough to
+        -- reduce the consequent to true.
+        let result := { obligation,
+                        assumptionsSat := checkAssumptionsStatus,
+                        result := .pass, verbose := options.verbose }
+        return (obligation, some result)
+      else if obligation.obligation.isFalse && obligation.assumptions.isEmpty then
+        -- If PE determines that the consequent is false and the path conditions
+        -- are empty (i.e., satisfiable), then we can immediately report a
+        -- verification failure. Note that we go to the SMT solver if the path
+        -- conditions aren't empty -- after all, the path conditions could imply
+        -- false, which the PE isn't capable enough to infer.
+        let prog := f!"\n\nEvaluated program:\n{p}"
+        dbg_trace f!"\n\nObligation {obligation.label}: failed!\
+                     \n\nResult obtained during partial evaluation.\
+                     {if options.verbose >= .normal then prog else ""}"
+        let result := { obligation,
+                        assumptionsSat := checkAssumptionsStatus,
+                        result := .fail,
+                        verbose := options.verbose }
+        return (obligation, some result)
+      else if options.removeIrrelevantAxioms then
+        -- We attempt to prune the path conditions by excluding all irrelevant
+        -- axioms w.r.t. the consequent to reduce the size of the proof
+        -- obligation.
+        let cg := Program.toFunctionCG p
+        let fns := obligation.obligation.getOps.map CoreIdent.toPretty
+        let relevant_fns := (fns ++ (CallGraph.getAllCalleesClosure cg fns)).dedup
+        let irrelevant_axs := Program.getIrrelevantAxioms p relevant_fns
+        let new_assumptions := Imperative.PathConditions.removeByNames obligation.assumptions irrelevant_axs
+        return ({ obligation with assumptions := new_assumptions }, none)
+      else
+        return (obligation, none)
 
 /--
 Invoke a backend engine and get the analysis result for a
 given proof obligation.
 -/
-def getObligationResult (terms : List Term) (ctx : SMT.Context)
+def getObligationResult (ob : SMT.Obligation) (ctx : SMT.Context)
     (obligation : ProofObligation Expression) (p : Program)
     (smtsolver : String) (options : Options) (counter : IO.Ref Nat)
     (tempDir : System.FilePath) : EIO DiagnosticModel VCResult := do
@@ -343,17 +430,43 @@ def getObligationResult (terms : List Term) (ctx : SMT.Context)
         (SMT.dischargeObligation options
           (ProofObligation.getVars obligation) smtsolver
             filename.toString
-          terms ctx)
+          ob ctx)
   match ans with
   | .error e =>
     dbg_trace f!"\n\nObligation {obligation.label}: SMT Solver Invocation Error!\
                  \n\nError: {e}\
                  {if options.verbose >= .normal then prog else ""}"
     .error <| DiagnosticModel.fromFormat e
-  | .ok (smt_result, estate) =>
+  | .ok (smt_results, estate) =>
+
+    let (assumptions_sat_res, assumptions_solver_res, obligation_res) ←
+      if ob.checkAssumptionsSat then
+        if h1 : smt_results.length == 2 then
+          .ok (some (smtResultToOutcome (smt_results[0]'(by grind)) true),
+               smt_results[0]'(by grind),
+               smt_results[1]'(by grind))
+        else
+          let f :=
+            f!"🚨 SMT Solver Implementation Error! Expected 2 results \
+                (assumptions sat check and main obligation check), \
+                but got {smt_results.length} results instead."
+          dbg_trace f!"\n\nObligation {obligation.label}: {f}\
+                       {if options.verbose >= .normal then prog else ""}"
+          .error <| DiagnosticModel.fromFormat f
+      else if h2 : smt_results.length == 1 then
+        .ok (none, .unknown, smt_results[0]'(by grind))
+      else
+        let f :=
+          f!"🚨 SMT Solver Implementation Error! Expected 1 result (main obligation check), \
+              but got {smt_results.length} results instead."
+        dbg_trace f!"\n\nObligation {obligation.label}: {f}\
+                     {if options.verbose >= .normal then prog else ""}"
+        .error <| DiagnosticModel.fromFormat f
     let result :=  { obligation,
-                     result := smtResultToOutcome smt_result (obligation.property == .cover)
-                     smtResult := smt_result,
+                     assumptionsSat := assumptions_sat_res
+                     assumptionSatSMTResult := assumptions_solver_res,
+                     result := smtResultToOutcome obligation_res (obligation.property == .cover)
+                     smtResult := obligation_res,
                      estate,
                      verbose := options.verbose }
     return result
@@ -361,6 +474,7 @@ def getObligationResult (terms : List Term) (ctx : SMT.Context)
 def verifySingleEnv (smtsolver : String) (pE : Program × Env) (options : Options)
     (counter : IO.Ref Nat) (tempDir : System.FilePath) :
     EIO DiagnosticModel VCResults := do
+  dbg_trace f!"Verify single env: {pE.snd.deferred}\n"
   let (p, E) := pE
   match E.error with
   | some err =>
@@ -370,6 +484,12 @@ def verifySingleEnv (smtsolver : String) (pE : Program × Env) (options : Option
   | _ =>
     let mut results := (#[] : VCResults)
     for obligation in E.deferred do
+      -- `options.checkAssumptionsSat := true` is a global setting that overrides
+      -- per-obligation assumption satisfiability setting (`false` by default).
+      let obligation := if options.checkAssumptionsSat then
+        { obligation with checkAssumptionsSat := true }
+      else
+        obligation
       let (obligation, maybeResult) ← preprocessObligation obligation p options
       if h : maybeResult.isSome then
         let result := Option.get maybeResult h
@@ -383,8 +503,8 @@ def verifySingleEnv (smtsolver : String) (pE : Program × Env) (options : Option
             dbg_trace f!"\n\nResult: {result}\n{prog}"
           if options.stopOnFirstError then break else continue
       -- For `unknown` results, we appeal to the SMT backend below.
-      let maybeTerms := ProofObligation.toSMTTerms E obligation
-      match maybeTerms with
+      let maybeOb := ProofObligation.toSMTObligation E obligation
+      match maybeOb with
       | .error err =>
         let err := f!"SMT Encoding Error! " ++ err
         let result := { obligation,
@@ -395,8 +515,8 @@ def verifySingleEnv (smtsolver : String) (pE : Program × Env) (options : Option
           dbg_trace f!"\n\nResult: {result}\n{prog}"
         results := results.push result
         if options.stopOnFirstError then break
-      | .ok (terms, ctx) =>
-        let result ← getObligationResult terms ctx obligation p smtsolver options
+      | .ok (ob, ctx) =>
+        let result ← getObligationResult ob ctx obligation p smtsolver options
                       counter tempDir
         results := results.push result
         if result.isNotSuccess then
@@ -413,7 +533,7 @@ def verify (smtsolver : String) (program : Program)
     : EIO DiagnosticModel VCResults := do
   match Core.typeCheckAndPartialEval options program moreFns with
   | .error err =>
-    .error { err with message := s!"❌ Type checking error.\n{err.message}" }
+    .error { err with message := s!"❌ Error.\n{err.message}" }
   | .ok pEs =>
     let counter ← IO.toEIO (fun e => DiagnosticModel.fromFormat f!"{e}") (IO.mkRef 0)
     let VCss ← if options.checkOnly then
diff --git a/StrataTest/Languages/Core/Examples/Cover.lean b/StrataTest/Languages/Core/Examples/Cover.lean
index 445cd3d07..71036c95d 100644
--- a/StrataTest/Languages/Core/Examples/Cover.lean
+++ b/StrataTest/Languages/Core/Examples/Cover.lean
@@ -25,41 +25,49 @@ procedure Test() returns ()
     cover [reachable_cover]: (true);
     cover [unsatisfiable_cover]: (x == -1);
     assert [reachable_assert]: (true);
+
   }
 };
 #end
 
-
 /--
 info:
 Obligation: unreachable_cover1
 Property: cover
+Assumptions Sat Check: ❌ fail
 Result: ❌ fail
 
 Obligation: unreachable_cover2
 Property: cover
+Assumptions Sat Check: ❌ fail
 Result: ❌ fail
 
 Obligation: unreachable_assert
 Property: assert
+Assumptions Sat Check: ❌ fail
 Result: ✅ pass
 
 Obligation: reachable_cover
 Property: cover
+Assumptions Sat Check: ✅ pass
 Result: ✅ pass
 Model:
 (init_x_0, 0)
 
 Obligation: unsatisfiable_cover
 Property: cover
+Assumptions Sat Check: ✅ pass
 Result: ❌ fail
 
 Obligation: reachable_assert
 Property: assert
+Assumptions Sat Check: ✅ pass
 Result: ✅ pass
 -/
 #guard_msgs in
-#eval verify "z3" coverPgm1 (options := Options.quiet)
+#eval verify "z3" coverPgm1
+          (options := {Options.quiet with solverTimeout := 1,
+                                          checkAssumptionsSat := true})
 
 ---------------------------------------------------------------------
 
@@ -84,19 +92,23 @@ spec {
 info:
 Obligation: ctest1
 Property: cover
+Assumptions Sat Check: ❌ fail
 Result: ❌ fail
 
 Obligation: ctest2
 Property: cover
+Assumptions Sat Check: ✅ pass
 Result: ✅ pass
 Model:
 ($__x0, 3)
 
 Obligation: atest2
 Property: assert
+Assumptions Sat Check: ✅ pass
 Result: ✅ pass
 -/
 #guard_msgs in
-#eval verify "z3" coverPgm2 (options := Options.quiet)
+#eval verify "z3" coverPgm2
+      (options := {Options.quiet with checkAssumptionsSat := true})
 
 ---------------------------------------------------------------------
diff --git a/StrataTest/Languages/Core/Examples/TypeDecl.lean b/StrataTest/Languages/Core/Examples/TypeDecl.lean
index f724bda66..b85661b50 100644
--- a/StrataTest/Languages/Core/Examples/TypeDecl.lean
+++ b/StrataTest/Languages/Core/Examples/TypeDecl.lean
@@ -123,7 +123,7 @@ type int := bool;
 #end
 
 /--
-error: (0,(0-0)) ❌ Type checking error.
+error: (0,(0-0)) ❌ Error.
 This type declaration's name is reserved!
 int := bool
 KnownTypes' names:
diff --git a/StrataTest/Languages/Core/ExprEvalTest.lean b/StrataTest/Languages/Core/ExprEvalTest.lean
index 22bad0114..fe61e480c 100644
--- a/StrataTest/Languages/Core/ExprEvalTest.lean
+++ b/StrataTest/Languages/Core/ExprEvalTest.lean
@@ -70,9 +70,9 @@ def checkValid (e:LExpr CoreLParams.mono): IO Bool := do
       let ans ← Core.SMT.dischargeObligation
         { Options.default with verbose := .quiet }
         (LExpr.freeVars e) "z3" filename.toString
-        [smt_term] ctx
+        {assumptions := [], obligation := smt_term} ctx
       match ans with
-      | .ok (.sat _,_) => return true
+      | .ok ([.sat _],_) => return true
       | _ =>
         IO.println s!"Test failed on {e}"
         IO.println s!"The query: {repr smt_term}"

From 44079159743cf02848fa4cf8630cc0eecb6726f6 Mon Sep 17 00:00:00 2001
From: Shilpi Goel <shigoel@gmail.com>
Date: Fri, 30 Jan 2026 14:33:55 -0600
Subject: [PATCH 2/3] Fix parsing of SMT solver output

---
 .../expected/ProcedureTypeError.core.expected |  2 +-
 Examples/expected/TypeError.core.expected     |  2 +-
 Strata/Languages/Core/Verifier.lean           | 28 +++++++++----------
 3 files changed, 16 insertions(+), 16 deletions(-)

diff --git a/Examples/expected/ProcedureTypeError.core.expected b/Examples/expected/ProcedureTypeError.core.expected
index 35379b046..34f7b6c62 100644
--- a/Examples/expected/ProcedureTypeError.core.expected
+++ b/Examples/expected/ProcedureTypeError.core.expected
@@ -1,3 +1,3 @@
 Successfully parsed.
-ProcedureTypeError.core.st(21,(4-32)) ❌ Type checking error.
+ProcedureTypeError.core.st(21,(4-32)) ❌ Error.
 [SumPositive:precond2]: Cannot find this fvar in the context! c
diff --git a/Examples/expected/TypeError.core.expected b/Examples/expected/TypeError.core.expected
index cd712e24b..366e7b5fd 100644
--- a/Examples/expected/TypeError.core.expected
+++ b/Examples/expected/TypeError.core.expected
@@ -1,4 +1,4 @@
 Successfully parsed.
-TypeError.core.st(25,(2-18)) ❌ Type checking error.
+TypeError.core.st(25,(2-18)) ❌ Error.
 Impossible to unify (Map int (Map bool bool)) with (Map int int).
 First mismatch: (Map bool bool) with int.
diff --git a/Strata/Languages/Core/Verifier.lean b/Strata/Languages/Core/Verifier.lean
index 3e5f8f6c1..6c34c2ce5 100644
--- a/Strata/Languages/Core/Verifier.lean
+++ b/Strata/Languages/Core/Verifier.lean
@@ -106,8 +106,18 @@ def runSolver (solver : String) (args : Array String) : IO IO.Process.Output :=
   }
   return output
 
--- def readLinesUntilVerdict (lines : List String) : List String × List String :=
+def isVerdict (s : String) : Bool :=
+  s ∈ ["unsat", "sat", "unknown"]
 
+def readLinesUntilVerdict (lines : List String) : List String × List String :=
+  match lines with
+  | [] => ([], [])
+  | head :: tail =>
+    if isVerdict head then
+      ([], lines)
+    else
+      let (pfx, rest) := readLinesUntilVerdict tail
+      (head :: pfx, rest)
 
 def parseVerdictWithModel (vars : List (IdentT LMonoTy Visibility))
     (verdict model : String) (ctx : SMT.Context) (E : EncoderState) :
@@ -128,27 +138,18 @@ def parseVerdictWithModel (vars : List (IdentT LMonoTy Visibility))
 partial def parseVerdictsWithModel (vars : List (IdentT LMonoTy Visibility))
     (lines : List String) (ctx : SMT.Context) (E : EncoderState) :
     Except Format (List Result) := do
-  dbg_trace f!"lines: {lines}"
   match lines with
   | [] =>
     .ok []
-  | verdict :: model :: rest =>
+  | verdict :: rest =>
     if !isVerdict verdict then
       .error f!"SMT Solver Error! Ill-formed verdict: {verdict}"
     else
-      let (modelStr, restLines) := if isVerdict model then ("", model :: rest) else (model, rest)
+      let (modelLines, restLines) := readLinesUntilVerdict rest
+      let modelStr := String.intercalate "\n" modelLines
       let result ← parseVerdictWithModel vars verdict modelStr ctx E
       let restResult ← parseVerdictsWithModel vars restLines ctx E
       return (result :: restResult)
-  | verdict :: rest =>
-    if !isVerdict verdict then
-      .error f!"SMT Solver Error! Ill-formed verdict: {verdict}"
-    else
-      let result ← parseVerdictWithModel vars verdict "" ctx E
-      let restResult ← parseVerdictsWithModel vars rest ctx E
-      return (result :: restResult)
-  where isVerdict (s : String) : Bool :=
-    s ∈ ["unsat", "sat", "unknown"]
 
 /--
 Parse SMT solver output from (possibly) multiple `check-sat` calls.
@@ -474,7 +475,6 @@ def getObligationResult (ob : SMT.Obligation) (ctx : SMT.Context)
 def verifySingleEnv (smtsolver : String) (pE : Program × Env) (options : Options)
     (counter : IO.Ref Nat) (tempDir : System.FilePath) :
     EIO DiagnosticModel VCResults := do
-  dbg_trace f!"Verify single env: {pE.snd.deferred}\n"
   let (p, E) := pE
   match E.error with
   | some err =>

From adeb2d362c6b96a47a74c50c1ba723c12fdbb6be Mon Sep 17 00:00:00 2001
From: Shilpi Goel <shigoel@gmail.com>
Date: Fri, 30 Jan 2026 18:03:42 -0600
Subject: [PATCH 3/3] Add finer grained control of reachability checks

---
 Strata/DL/Imperative/CmdEval.lean             |  20 ++-
 Strata/DL/Imperative/EvalContext.lean         |   8 +-
 Strata/DL/Imperative/MetaData.lean            |  18 ++-
 Strata/Languages/Core/DDMTransform/Parse.lean |   8 +-
 .../Core/DDMTransform/Translate.lean          |  25 ++-
 Strata/Languages/Core/Env.lean                |  26 ---
 Strata/Languages/Core/Options.lean            |   4 +-
 Strata/Languages/Core/SMTEncoder.lean         |  11 +-
 Strata/Languages/Core/SarifOutput.lean        |   4 +-
 Strata/Languages/Core/StatementEval.lean      |  35 ++++-
 Strata/Languages/Core/Verifier.lean           | 148 ++++++++++--------
 StrataMain.lean                               |   2 +-
 .../Core/DatatypeVerificationTests.lean       |   6 +-
 StrataTest/Languages/Core/Examples/Cover.lean |  19 +--
 StrataTest/Languages/Core/ExprEvalTest.lean   |   2 +-
 .../Languages/Core/SarifOutputTests.lean      |   5 +-
 StrataVerify.lean                             |   2 +-
 17 files changed, 215 insertions(+), 128 deletions(-)

diff --git a/Strata/DL/Imperative/CmdEval.lean b/Strata/DL/Imperative/CmdEval.lean
index 08a1f1c3a..486d8d406 100644
--- a/Strata/DL/Imperative/CmdEval.lean
+++ b/Strata/DL/Imperative/CmdEval.lean
@@ -14,10 +14,16 @@ open Std (ToFormat Format format)
 
 --------------------------------------------------------------------
 
+def checkAssumptionsSatMode [BEq P.Ident] (md : MetaData P) :
+    Imperative.AssumptionSatCheckMode :=
+  match Imperative.MetaData.getCheckAssumptionsSat md with
+    | none => .globalDefault
+    | some b => if b then .check else .noCheck
+
 /--
 Partial evaluator for an Imperative Command.
 -/
-def Cmd.eval [EC : EvalContext P S] (σ : S) (c : Cmd P) : Cmd P × S :=
+def Cmd.eval [EC : EvalContext P S] [BEq P.Ident] (σ : S) (c : Cmd P) : Cmd P × S :=
   match EC.lookupError σ with
   | some _ => (c, σ)
   | none =>
@@ -56,16 +62,17 @@ def Cmd.eval [EC : EvalContext P S] (σ : S) (c : Cmd P) : Cmd P × S :=
       let e := EC.eval σ e
       let assumptions := EC.getPathConditions σ
       let c' := .assert label e md
+      let checkAssum := checkAssumptionsSatMode md
       match EC.denoteBool e with
       | some true => -- Proved via evaluation.
-        (c', EC.deferObligation σ (ProofObligation.mk label .assert false assumptions e md))
+        (c', EC.deferObligation σ (ProofObligation.mk label .assert checkAssum assumptions e md))
       | some false =>
         if assumptions.isEmpty then
           (c', EC.updateError σ (.AssertFail label e))
         else
-          (c', EC.deferObligation σ (ProofObligation.mk label .assert false assumptions e md))
+          (c', EC.deferObligation σ (ProofObligation.mk label .assert checkAssum assumptions e md))
       | none =>
-        (c', EC.deferObligation σ (ProofObligation.mk label .assert false assumptions e md))
+        (c', EC.deferObligation σ (ProofObligation.mk label .assert checkAssum assumptions e md))
 
     | .assume label e md =>
       let (e, σ) := EC.preprocess σ c e
@@ -85,12 +92,13 @@ def Cmd.eval [EC : EvalContext P S] (σ : S) (c : Cmd P) : Cmd P × S :=
       let e := EC.eval σ e
       let assumptions := EC.getPathConditions σ
       let c' := .cover label e md
-      (c', EC.deferObligation σ (ProofObligation.mk label .cover false assumptions e md))
+      let checkAssum := checkAssumptionsSatMode md
+      (c', EC.deferObligation σ (ProofObligation.mk label .cover checkAssum assumptions e md))
 
 /--
 Partial evaluator for Imperative's Commands.
 -/
-def Cmds.eval [EvalContext P S] (σ : S) (cs : Cmds P) : Cmds P × S :=
+def Cmds.eval [EvalContext P S] [BEq P.Ident] (σ : S) (cs : Cmds P) : Cmds P × S :=
   match cs with
   | [] => ([], σ)
   | c :: crest =>
diff --git a/Strata/DL/Imperative/EvalContext.lean b/Strata/DL/Imperative/EvalContext.lean
index 4cdb627bf..eb01b0a9c 100644
--- a/Strata/DL/Imperative/EvalContext.lean
+++ b/Strata/DL/Imperative/EvalContext.lean
@@ -73,6 +73,12 @@ inductive PropertyType where
   | assert
   deriving Repr, DecidableEq
 
+inductive AssumptionSatCheckMode where
+  | check
+  | noCheck
+  | globalDefault
+  deriving Repr, DecidableEq
+
 instance : ToFormat PropertyType where
   format p := match p with
     | .cover => "cover"
@@ -86,7 +92,7 @@ structure ProofObligation (P : PureExpr) where
   label : String
   property : PropertyType
   /-- Check if assumptions are satisfiable. -/
-  checkAssumptionsSat : Bool := false
+  checkAssumptionsSat : AssumptionSatCheckMode := .globalDefault
   assumptions : PathConditions P
   obligation : P.Expr
   metadata : MetaData P
diff --git a/Strata/DL/Imperative/MetaData.lean b/Strata/DL/Imperative/MetaData.lean
index ce1b84ca0..486d7d20d 100644
--- a/Strata/DL/Imperative/MetaData.lean
+++ b/Strata/DL/Imperative/MetaData.lean
@@ -75,12 +75,15 @@ inductive MetaDataElem.Value (P : PureExpr) where
   | msg (s : String)
   /-- Metadata value in the form of a fileRange. -/
   | fileRange (r: FileRange)
+  /-- Metadata value in the form of a boolean switch. -/
+  | switch (b : Bool)
 
 instance [ToFormat P.Expr] : ToFormat (MetaDataElem.Value P) where
   format f := match f with
               | .expr e => f!"{e}"
               | .msg s => f!"{s}"
               | .fileRange r => f!"{r}"
+              | .switch a => f!"{a}"
 
 instance [Repr P.Expr] : Repr (MetaDataElem.Value P) where
   reprPrec v prec :=
@@ -89,6 +92,7 @@ instance [Repr P.Expr] : Repr (MetaDataElem.Value P) where
       | .expr e => f!".expr {reprPrec e prec}"
       | .msg s => f!".msg {s}"
       | .fileRange fr => f!".fileRange {fr}"
+      | .switch a => f!".switch {a}"
     Repr.addAppParen res prec
 
 def MetaDataElem.Value.beq [BEq P.Expr] (v1 v2 : MetaDataElem.Value P) :=
@@ -96,6 +100,7 @@ def MetaDataElem.Value.beq [BEq P.Expr] (v1 v2 : MetaDataElem.Value P) :=
   | .expr e1, .expr e2 => e1 == e2
   | .msg m1, .msg m2 => m1 == m2
   | .fileRange r1, .fileRange r2 => r1 == r2
+  | .switch r1, .switch r2 => r1 == r2
   | _, _ => false
 
 instance [BEq P.Expr] : BEq (MetaDataElem.Value P) where
@@ -172,7 +177,7 @@ instance [Repr P.Expr] [Repr P.Ident] : Repr (MetaDataElem P) where
 def MetaData.fileRange : MetaDataElem.Field P := .label "fileRange"
 
 def getFileRange {P : PureExpr} [BEq P.Ident] (md: MetaData P) : Option FileRange := do
-  let fileRangeElement <- md.findElem Imperative.MetaData.fileRange
+  let fileRangeElement ← md.findElem Imperative.MetaData.fileRange
   match fileRangeElement.value with
     | .fileRange fileRange =>
       some fileRange
@@ -192,11 +197,20 @@ def MetaData.toDiagnosticF {P : PureExpr} [BEq P.Ident] (md : MetaData P) (msg :
 /-- Get the file range from metadata as a DiagnosticModel (for formatting).
     This is a compatibility function that formats the file range using byte offsets.
     For proper line/column display, use toDiagnostic and format with a FileMap at the top level. -/
-def MetaData.formatFileRangeD {P : PureExpr} [BEq P.Ident] (md : MetaData P) (fileMap : Option Lean.FileMap := none) (includeEnd? : Bool := false) : Format :=
+def MetaData.formatFileRangeD {P : PureExpr} [BEq P.Ident] (md : MetaData P)
+    (fileMap : Option Lean.FileMap := none) (includeEnd? : Bool := false) : Format :=
   match getFileRange md with
   | some fr => fr.format fileMap includeEnd?
   | none => f!""
 
+def MetaData.checkAssumptionsSat : MetaDataElem.Field P := .label "checkAssumptionsSat"
+
+def MetaData.getCheckAssumptionsSat {P : PureExpr} [BEq P.Ident] (md: MetaData P) : Option Bool := do
+  let elem ← md.findElem Imperative.MetaData.checkAssumptionsSat
+  match elem.value with
+    | .switch b => some b
+    | _ => none
+
 ---------------------------------------------------------------------
 
 end Imperative
diff --git a/Strata/Languages/Core/DDMTransform/Parse.lean b/Strata/Languages/Core/DDMTransform/Parse.lean
index 690d7de27..fc1f1fe67 100644
--- a/Strata/Languages/Core/DDMTransform/Parse.lean
+++ b/Strata/Languages/Core/DDMTransform/Parse.lean
@@ -187,14 +187,18 @@ category Label;
 
 op label (l : Ident) : Label => "[" l "]:";
 
+category CheckAssumptionsSat;
+op checkAssumOn : CheckAssumptionsSat => "@[" "checkAssumptionsSat" ":" "true" "]";
+op checkAssumOff : CheckAssumptionsSat => "@[" "checkAssumptionsSat" ":" "false" "]";
+
 @[scope(dl)]
 op varStatement (dl : DeclList) : Statement => "var " dl ";\n";
 @[declare(v, tp)]
 op initStatement (tp : Type, v : Ident, e : tp) : Statement => "var " v " : " tp " := " e ";\n";
 op assign (tp : Type, v : Lhs, e : tp) : Statement => v " := " e ";\n";
 op assume (label : Option Label, c : bool) : Statement => "assume " label c ";\n";
-op assert (label : Option Label, c : bool) : Statement => "assert " label c ";\n";
-op cover (label : Option Label, c : bool) : Statement => "cover " label c ";\n";
+op assert (checkAssum? : Option CheckAssumptionsSat, label : Option Label, c : bool) : Statement => checkAssum? "assert " label c ";\n";
+op cover (checkAssum? : Option CheckAssumptionsSat, label : Option Label, c : bool) : Statement => checkAssum? "cover " label c ";\n";
 op if_statement (c : bool, t : Block, f : Else) : Statement => "if" "(" c ")" t f;
 op else0 () : Else =>;
 op else1 (f : Block) : Else => "else" f;
diff --git a/Strata/Languages/Core/DDMTransform/Translate.lean b/Strata/Languages/Core/DDMTransform/Translate.lean
index 6d8b5b326..e0b846052 100644
--- a/Strata/Languages/Core/DDMTransform/Translate.lean
+++ b/Strata/Languages/Core/DDMTransform/Translate.lean
@@ -133,6 +133,19 @@ def translateReal (arg : Arg) : TransM Decimal := do
     | TransM.error s!"translateReal expects decimal lit"
   return d
 
+def translateOptionCheckAssum (arg : Arg) : TransM (Option Bool) := do
+  translateOption
+    (fun maybe_arg => do
+        match maybe_arg with
+        | none => return default
+        | some c =>
+          let .op op := c | TransM.error s!"translateLhs expected op {repr arg}"
+          match op.name with
+          | q`Core.checkAssumOn => return (some true)
+          | q`Core.checkAssumOff => return (some false)
+          | _ => return .none)
+    arg
+
 ---------------------------------------------------------------------
 
 inductive GenKind where
@@ -976,19 +989,27 @@ partial def translateStmt (p : Program) (bindings : TransBindings) (arg : Arg) :
     let id ← translateIdent CoreIdent ida
     let md ← getOpMetaData op
     return ([.havoc id md], bindings)
-  | q`Core.assert, #[la, ca] =>
+  | q`Core.assert, #[checkAssum, la, ca] =>
     let c ← translateExpr p bindings ca
     let default_name := s!"assert_{bindings.gen.assert_def}"
     let bindings := incrNum .assert_def bindings
     let l ← translateOptionLabel default_name la
+    let checkAssumMode ← translateOptionCheckAssum checkAssum
     let md ← getOpMetaData op
+    let md := if h: checkAssumMode.isSome then
+                md.pushElem Imperative.MetaData.checkAssumptionsSat (.switch (checkAssumMode.get h))
+              else md
     return ([.assert l c md], bindings)
-  | q`Core.cover, #[la, ca] =>
+  | q`Core.cover, #[checkAssum, la, ca] =>
     let c ← translateExpr p bindings ca
     let default_name := s!"cover_{bindings.gen.assert_def}"
     let bindings := incrNum .cover_def bindings
     let l ← translateOptionLabel default_name la
+    let checkAssumMode ← translateOptionCheckAssum checkAssum
     let md ← getOpMetaData op
+    let md := if h: checkAssumMode.isSome then
+                md.pushElem Imperative.MetaData.checkAssumptionsSat (.switch (checkAssumMode.get h))
+              else md
     return ([.cover l c md], bindings)
   | q`Core.assume, #[la, ca] =>
     let c ← translateExpr p bindings ca
diff --git a/Strata/Languages/Core/Env.lean b/Strata/Languages/Core/Env.lean
index a8b51d064..1bef0d55e 100644
--- a/Strata/Languages/Core/Env.lean
+++ b/Strata/Languages/Core/Env.lean
@@ -97,32 +97,6 @@ instance : ToFormat (ProofObligation Expression) where
 instance : ToFormat (ProofObligations Expression) where
   format os := Std.Format.joinSep (Array.map format os).toList Format.line
 
--- (FIXME) Parameterize by EvalContext typeclass.
-def ProofObligation.create
-  (label : String) (propertyType : PropertyType)
-  (assumptions : PathConditions Expression) (obligation : Procedure.Check):
-  Option (ProofObligation Expression) :=
-  open Lambda.LExpr.SyntaxMono in
-  if obligation.attr == .Free then
-    dbg_trace f!"{Format.line}Obligation {label} is free!{Format.line}"
-    none
-  else
-    some (ProofObligation.mk label propertyType false assumptions obligation.expr obligation.md)
-
-def ProofObligations.createAssertions
-  (assumptions : PathConditions Expression)
-  (obligations : ListMap String Procedure.Check)
-  : ProofObligations Expression :=
-  match obligations with
-  | [] => #[]
-  | o :: orest =>
-    let orest' := ProofObligations.createAssertions assumptions orest
-    let o' :=
-      match (ProofObligation.create o.fst .assert assumptions o.snd) with
-      | none => #[]
-      | some o' => #[o']
-    o' ++ orest'
-
 /--
 A substitution map from variable identifiers to expressions.
 -/
diff --git a/Strata/Languages/Core/Options.lean b/Strata/Languages/Core/Options.lean
index 8eed2dbc2..290b32f66 100644
--- a/Strata/Languages/Core/Options.lean
+++ b/Strata/Languages/Core/Options.lean
@@ -43,7 +43,9 @@ structure Options where
   checkOnly : Bool
   stopOnFirstError : Bool
   removeIrrelevantAxioms : Bool
-  checkAssumptionsSat : Bool
+  /-- Check if assumptions are satisfiable; global setting can be overridden by
+    obligation-specific setting. -/
+  checkAssumptionsSat : Bool := false
   /-- Solver time limit in seconds -/
   solverTimeout : Nat
   /-- Output results in SARIF format -/
diff --git a/Strata/Languages/Core/SMTEncoder.lean b/Strata/Languages/Core/SMTEncoder.lean
index a7156f231..5151f7b9a 100644
--- a/Strata/Languages/Core/SMTEncoder.lean
+++ b/Strata/Languages/Core/SMTEncoder.lean
@@ -568,7 +568,7 @@ def toSMTTerms (E : Env) (es : List (LExpr CoreLParams.mono)) (ctx : SMT.Context
 structure SMT.Obligation where
   assumptions : List Term
   obligation : Term
-  checkAssumptionsSat : Bool := false
+  checkAssumptionsSat : Bool
 
 /--
 Encode a proof obligation -- which may be of type `assert` or `cover` -- into
@@ -595,6 +595,13 @@ cover is violated. If the result is `sat`, then the cover succeeds.
 def ProofObligation.toSMTObligation (E : Env)
     (d : Imperative.ProofObligation Expression) (ctx : SMT.Context := SMT.Context.default) :
     Except Format (SMT.Obligation × SMT.Context) := do
+  let checkAssumptionsSat ← match d.checkAssumptionsSat with
+    | .check => .ok true
+    | .noCheck => .ok false
+    | .globalDefault =>
+      .error "Implementation Error in ProofObligation.toSMTObligation: \
+              Global default for checking satisfiability of assumptions \
+              not supported in this context."
   let assumptions := d.assumptions.flatten.map (fun a => a.snd)
   let (ctx, distinct_terms) ← E.distinct.foldlM (λ (ctx, tss) es =>
     do let (ts, ctx') ← Core.toSMTTerms E es ctx; pure (ctx', ts :: tss)) (ctx, [])
@@ -609,7 +616,7 @@ def ProofObligation.toSMTObligation (E : Env)
       Factory.not obligation_pos_term
   .ok ({assumptions := distinct_assumptions ++ assumptions_terms,
         obligation := obligation_term,
-        checkAssumptionsSat := d.checkAssumptionsSat },
+        checkAssumptionsSat := checkAssumptionsSat },
        ctx)
 
 ---------------------------------------------------------------------
diff --git a/Strata/Languages/Core/SarifOutput.lean b/Strata/Languages/Core/SarifOutput.lean
index 8f071ca95..c341cf93a 100644
--- a/Strata/Languages/Core/SarifOutput.lean
+++ b/Strata/Languages/Core/SarifOutput.lean
@@ -56,8 +56,8 @@ def extractLocation (files : Map Strata.Uri Lean.FileMap) (md : Imperative.MetaD
 /-- Convert a VCResult to a SARIF Result -/
 def vcResultToSarifResult (files : Map Strata.Uri Lean.FileMap) (vcr : VCResult) : Strata.Sarif.Result :=
   let ruleId := vcr.obligation.label
-  let level := outcomeToLevel vcr.result
-  let messageText := outcomeToMessage vcr.result vcr.smtResult
+  let level := outcomeToLevel vcr.result.result
+  let messageText := outcomeToMessage vcr.result.result vcr.result.solverResult
   let message : Strata.Sarif.Message := { text := messageText }
 
   let locations := match extractLocation files vcr.obligation.metadata with
diff --git a/Strata/Languages/Core/StatementEval.lean b/Strata/Languages/Core/StatementEval.lean
index 8f601789d..bd76d701f 100644
--- a/Strata/Languages/Core/StatementEval.lean
+++ b/Strata/Languages/Core/StatementEval.lean
@@ -111,6 +111,36 @@ Get current values of global variables for old expression substitution.
 private def getCurrentGlobals (E : Env) : VarSubst :=
   E.exprEnv.state.oldest.map (fun (id, ty, e) => ((id.name, ty), e))
 
+open Imperative in
+private def ProofObligation.create
+  (label : String) (propertyType : PropertyType)
+  (assumptions : PathConditions Expression) (obligation : Procedure.Check)
+  (assumptionSatCheckMode : AssumptionSatCheckMode) :
+  Option (ProofObligation Expression) :=
+  open Lambda.LExpr.SyntaxMono in
+  if obligation.attr == .Free then
+    dbg_trace f!"{Format.line}Obligation {label} is free!{Format.line}"
+    none
+  else
+    some (ProofObligation.mk label propertyType assumptionSatCheckMode assumptions obligation.expr obligation.md)
+
+open Imperative in
+private def ProofObligations.createAssertions
+  (assumptions : PathConditions Expression)
+  (obligations : ListMap String Procedure.Check)
+  : ProofObligations Expression :=
+  match obligations with
+  | [] => #[]
+  | o :: orest =>
+    let orest' := ProofObligations.createAssertions assumptions orest
+    let o' :=
+      -- TODO: Assumption sat checking is hardcoded to `.noCheck` here; we
+      -- don't yet have syntax to specify it per-contract yet.
+      match (ProofObligation.create o.fst .assert assumptions o.snd .noCheck) with
+      | none => #[]
+      | some o' => #[o']
+    o' ++ orest'
+
 /--
 Evaluate a procedure call `lhs := pname(args)`.
 -/
@@ -268,7 +298,7 @@ private def createUnreachableCoverObligations
   covers.toArray.map
     (fun (label, md) =>
       (Imperative.ProofObligation.mk label .cover
-        false
+        (Imperative.checkAssumptionsSatMode md)
         [[("unreachable", (LExpr.false ()))]]
         (LExpr.false ()) md))
 
@@ -277,7 +307,8 @@ private def createUnreachableAssertObligations
     Imperative.ProofObligations Expression :=
   asserts.toArray.map
     (fun (label, md) =>
-      (Imperative.ProofObligation.mk label .assert false
+      (Imperative.ProofObligation.mk label .assert
+        (Imperative.checkAssumptionsSatMode md)
         [[("unreachable", (LExpr.false ()))]]
         (LExpr.true ()) md))
 
diff --git a/Strata/Languages/Core/Verifier.lean b/Strata/Languages/Core/Verifier.lean
index 6c34c2ce5..ffdcacad4 100644
--- a/Strata/Languages/Core/Verifier.lean
+++ b/Strata/Languages/Core/Verifier.lean
@@ -267,17 +267,34 @@ instance : ToFormat Outcome where
     | .unknown => "🟡 unknown"
     | .implementationError e => s!"🚨 Implementation Error! {e}"
 
+/--
+All results from analyzing a proof obligation.
+-/
+structure ObligationResult where
+  -- `.none` when the proof obligation doesn't require assumption sat checks.
+  assumptionsSat : Option Outcome := .none
+  assumptionSatSolverResult : SMT.Result := .unknown
+  result : Outcome := .unknown
+  solverResult : SMT.Result := .unknown
+  deriving Repr, Inhabited
+
+instance : ToFormat ObligationResult where
+  format r :=
+  let obResult := f!"{r.result}{r.solverResult.formatModelIfSat true}"
+  let finalResult :=
+    match r.assumptionsSat with
+    | .none => f!"Result: {obResult}"
+    | some r => f!"Assumptions Sat Check: {r}\n\
+                   Result: {obResult}"
+  finalResult
+
 /--
 A collection of all information relevant to a verification condition's
 analysis.
 -/
 structure VCResult where
   obligation : Imperative.ProofObligation Expression
-  -- `.none` when the proof obligation doesn't require assumption sat checks.
-  assumptionsSat : Option Outcome := .none
-  assumptionSatSMTResult : SMT.Result := .unknown
-  result : Outcome := .unknown
-  smtResult : SMT.Result := .unknown
+  result : ObligationResult
   estate : EncoderState := EncoderState.init
   verbose : VerboseMode := .normal
 
@@ -295,27 +312,21 @@ def smtResultToOutcome (r : SMT.Result) (satIsPass : Bool) : Outcome :=
 
 instance : ToFormat VCResult where
   format r :=
-  let assumptionCheckResult :=
-    match r.assumptionsSat with
-    | .none => f!""
-    | some r => f!"Assumptions Sat Check: {r}\n"
   f!"Obligation: {r.obligation.label}\n\
                  Property: {r.obligation.property}\n\
-                 {assumptionCheckResult}\
-                 Result: {r.result}\
-                 {r.smtResult.formatModelIfSat true}"
+                 {r.result}"
 
 def VCResult.isSuccess (vr : VCResult) : Bool :=
-  match vr.result with | .pass => true | _ => false
+  match vr.result.result with | .pass => true | _ => false
 
 def VCResult.isFailure (vr : VCResult) : Bool :=
-  match vr.result with | .fail => true | _ => false
+  match vr.result.result with | .fail => true | _ => false
 
 def VCResult.isUnknown (vr : VCResult) : Bool :=
-  match vr.result with | .unknown => true | _ => false
+  match vr.result.result with | .unknown => true | _ => false
 
 def VCResult.isImplementationError (vr : VCResult) : Bool :=
-  match vr.result with | .implementationError _ => true | _ => false
+  match vr.result.result with | .implementationError _ => true | _ => false
 
 def VCResult.isNotSuccess (vcResult : Core.VCResult) :=
   !Core.VCResult.isSuccess vcResult
@@ -341,7 +352,7 @@ def preprocessObligation (obligation : ProofObligation Expression) (p : Program)
   -- satisfiability of assumptions alone.
   let checkAssumptionsStatus :=
     match obligation.checkAssumptionsSat with
-    | true =>
+    | .check =>
       if obligation.assumptions.isEmpty then
         -- No assumptions to check; can process consequent next.
         some Outcome.pass
@@ -350,17 +361,19 @@ def preprocessObligation (obligation : ProofObligation Expression) (p : Program)
         some Outcome.fail
       else -- Exit to use a backend solver.
         some Outcome.unknown
-    | false =>
+    | _ =>
       -- Assumption satisfiability check not requested.
       -- Can process consequent next.
       .none
   match checkAssumptionsStatus with
   | some .fail => -- Exit early.
     let result := { obligation,
-                    assumptionsSat := checkAssumptionsStatus,
-                    result := (match obligation.property with
-                              | .assert => .pass
-                              | .cover => .fail),
+                    result := {
+                        assumptionsSat := checkAssumptionsStatus,
+                        result := (match obligation.property with
+                                    | .assert => .pass
+                                    | .cover => .fail),
+                    }
                     verbose := options.verbose }
     return (obligation, some result)
   | .some .unknown =>
@@ -372,8 +385,10 @@ def preprocessObligation (obligation : ProofObligation Expression) (p : Program)
       if obligation.obligation.isFalse then
         -- If PE determines that the consequent is false, then the cover fails.
         let result := { obligation,
-                        assumptionsSat := checkAssumptionsStatus,
-                        result := .fail, verbose := options.verbose }
+                        result := {
+                          assumptionsSat := checkAssumptionsStatus,
+                          result := .fail },
+                        verbose := options.verbose }
         return (obligation, some result)
       else
         return (obligation, none)
@@ -382,8 +397,9 @@ def preprocessObligation (obligation : ProofObligation Expression) (p : Program)
         -- We don't need the SMT solver if PE (partial evaluation) is enough to
         -- reduce the consequent to true.
         let result := { obligation,
-                        assumptionsSat := checkAssumptionsStatus,
-                        result := .pass, verbose := options.verbose }
+                        result := {assumptionsSat := checkAssumptionsStatus,
+                                   result := .pass},
+                        verbose := options.verbose }
         return (obligation, some result)
       else if obligation.obligation.isFalse && obligation.assumptions.isEmpty then
         -- If PE determines that the consequent is false and the path conditions
@@ -396,8 +412,8 @@ def preprocessObligation (obligation : ProofObligation Expression) (p : Program)
                      \n\nResult obtained during partial evaluation.\
                      {if options.verbose >= .normal then prog else ""}"
         let result := { obligation,
-                        assumptionsSat := checkAssumptionsStatus,
-                        result := .fail,
+                        result := { assumptionsSat := checkAssumptionsStatus,
+                                    result := .fail },
                         verbose := options.verbose }
         return (obligation, some result)
       else if options.removeIrrelevantAxioms then
@@ -413,6 +429,35 @@ def preprocessObligation (obligation : ProofObligation Expression) (p : Program)
       else
         return (obligation, none)
 
+def smtResultsToObligationResult (name : String) (property : PropertyType)
+    (checkAssumptionsSat : Bool) (smt_results : List SMT.Result) :
+    Except Format ObligationResult := do
+  let (assumptions_sat_res, assumptions_solver_res, obligation_res) ←
+    if checkAssumptionsSat then
+      if h1 : smt_results.length == 2 then
+        .ok (some (smtResultToOutcome (smt_results[0]'(by grind)) true),
+             smt_results[0]'(by grind),
+             smt_results[1]'(by grind))
+      else
+        let f :=
+          f!"🚨 \n\nObligation {name}: SMT Solver Implementation Error! \
+              Expected 2 results \
+              (assumptions sat check and main obligation check), \
+              but got {smt_results.length} results instead."
+        .error f
+    else if h2 : smt_results.length == 1 then
+      .ok (none, .unknown, smt_results[0]'(by grind))
+    else
+      let f :=
+        f!"🚨 \n\nObligation {name}: SMT Solver Implementation Error! \
+            Expected 1 result (main obligation check), \
+            but got {smt_results.length} results instead."
+      .error f
+  return { assumptionsSat := assumptions_sat_res
+           assumptionSatSolverResult := assumptions_solver_res,
+           result := smtResultToOutcome obligation_res (property == .cover)
+           solverResult := obligation_res }
+
 /--
 Invoke a backend engine and get the analysis result for a
 given proof obligation.
@@ -439,35 +484,12 @@ def getObligationResult (ob : SMT.Obligation) (ctx : SMT.Context)
                  {if options.verbose >= .normal then prog else ""}"
     .error <| DiagnosticModel.fromFormat e
   | .ok (smt_results, estate) =>
-
-    let (assumptions_sat_res, assumptions_solver_res, obligation_res) ←
-      if ob.checkAssumptionsSat then
-        if h1 : smt_results.length == 2 then
-          .ok (some (smtResultToOutcome (smt_results[0]'(by grind)) true),
-               smt_results[0]'(by grind),
-               smt_results[1]'(by grind))
-        else
-          let f :=
-            f!"🚨 SMT Solver Implementation Error! Expected 2 results \
-                (assumptions sat check and main obligation check), \
-                but got {smt_results.length} results instead."
-          dbg_trace f!"\n\nObligation {obligation.label}: {f}\
-                       {if options.verbose >= .normal then prog else ""}"
-          .error <| DiagnosticModel.fromFormat f
-      else if h2 : smt_results.length == 1 then
-        .ok (none, .unknown, smt_results[0]'(by grind))
-      else
-        let f :=
-          f!"🚨 SMT Solver Implementation Error! Expected 1 result (main obligation check), \
-              but got {smt_results.length} results instead."
-        dbg_trace f!"\n\nObligation {obligation.label}: {f}\
-                     {if options.verbose >= .normal then prog else ""}"
-        .error <| DiagnosticModel.fromFormat f
+    let obresult ←
+      match smtResultsToObligationResult obligation.label obligation.property ob.checkAssumptionsSat smt_results with
+      | .ok result => pure result
+      | .error fmt => throw (DiagnosticModel.fromFormat fmt)
     let result :=  { obligation,
-                     assumptionsSat := assumptions_sat_res
-                     assumptionSatSMTResult := assumptions_solver_res,
-                     result := smtResultToOutcome obligation_res (obligation.property == .cover)
-                     smtResult := obligation_res,
+                     result := obresult
                      estate,
                      verbose := options.verbose }
     return result
@@ -484,10 +506,12 @@ def verifySingleEnv (smtsolver : String) (pE : Program × Env) (options : Option
   | _ =>
     let mut results := (#[] : VCResults)
     for obligation in E.deferred do
-      -- `options.checkAssumptionsSat := true` is a global setting that overrides
-      -- per-obligation assumption satisfiability setting (`false` by default).
-      let obligation := if options.checkAssumptionsSat then
-        { obligation with checkAssumptionsSat := true }
+      let obligation :=
+        -- Set the obligation's assumption satisfiability check mode to the
+        -- global setting, unless the local setting overrides it.
+        if obligation.checkAssumptionsSat == .globalDefault then
+          { obligation with checkAssumptionsSat :=
+              if options.checkAssumptionsSat then .check else .noCheck }
       else
         obligation
       let (obligation, maybeResult) ← preprocessObligation obligation p options
@@ -508,7 +532,7 @@ def verifySingleEnv (smtsolver : String) (pE : Program × Env) (options : Option
       | .error err =>
         let err := f!"SMT Encoding Error! " ++ err
         let result := { obligation,
-                        result := .implementationError (toString err),
+                        result := { result := .implementationError (toString err) },
                         verbose := options.verbose }
         if options.verbose >= .normal then
           let prog := f!"\n\nEvaluated program:\n{p}"
@@ -588,7 +612,7 @@ def verify
     panic! s!"DDM Transform Error: {repr errors}"
 
 def toDiagnosticModel (vcr : Core.VCResult) : Option DiagnosticModel := do
-  match vcr.result with
+  match vcr.result.result with
   | .pass => none  -- Verification succeeded, no diagnostic
   | result =>
     let fileRangeElem ← vcr.obligation.metadata.findElem Imperative.MetaData.fileRange
diff --git a/StrataMain.lean b/StrataMain.lean
index 2a70578f4..2cc16618d 100644
--- a/StrataMain.lean
+++ b/StrataMain.lean
@@ -226,7 +226,7 @@ def pyAnalyzeCommand : Command where
                                       (moreFns := Strata.Python.ReFactory)))
       let mut s := ""
       for vcResult in vcResults do
-        s := s ++ s!"\n{vcResult.obligation.label}: {Std.format vcResult.result}\n"
+        s := s ++ s!"\n{vcResult.obligation.label}: {Std.format vcResult.result.result}\n"
       IO.println s
 
 def javaGenCommand : Command where
diff --git a/StrataTest/Languages/Core/DatatypeVerificationTests.lean b/StrataTest/Languages/Core/DatatypeVerificationTests.lean
index 50d8bb03f..9dba511b6 100644
--- a/StrataTest/Languages/Core/DatatypeVerificationTests.lean
+++ b/StrataTest/Languages/Core/DatatypeVerificationTests.lean
@@ -115,9 +115,9 @@ def runVerificationTest (testName : String) (program : Program) : IO String := d
     | .ok results =>
       let mut output := s!"{testName}: PASSED\n"
       output := output ++ s!"  Verified {results.size} obligation(s)\n"
-      for result in results do
-        if result.result != .pass then
-          output := output ++ s!"  WARNING: {result.obligation.label}: {Std.format result.result}\n"
+      for r in results do
+        if r.result.result != .pass then
+          output := output ++ s!"  WARNING: {r.obligation.label}: {Std.format r.result}\n"
       return output
   catch e =>
     return s!"{testName}: FAILED (exception)\n  Error: {e}"
diff --git a/StrataTest/Languages/Core/Examples/Cover.lean b/StrataTest/Languages/Core/Examples/Cover.lean
index 71036c95d..666aea9ee 100644
--- a/StrataTest/Languages/Core/Examples/Cover.lean
+++ b/StrataTest/Languages/Core/Examples/Cover.lean
@@ -18,13 +18,13 @@ procedure Test() returns ()
   assume (x >= 0);
 
   if (false) {
-    cover [unreachable_cover1]: (true);
-    cover [unreachable_cover2]: (false);
-    assert [unreachable_assert]: (false);
+    @[checkAssumptionsSat:true] cover [unreachable_cover1]: (true);
+    @[checkAssumptionsSat:false] cover [unreachable_cover2]: (false);
+     assert [unreachable_assert]: (false);
   } else {
     cover [reachable_cover]: (true);
-    cover [unsatisfiable_cover]: (x == -1);
-    assert [reachable_assert]: (true);
+    @[checkAssumptionsSat:true] cover [unsatisfiable_cover]: (x == -1);
+    @[checkAssumptionsSat:false] assert [reachable_assert]: (true);
 
   }
 };
@@ -39,7 +39,6 @@ Result: ❌ fail
 
 Obligation: unreachable_cover2
 Property: cover
-Assumptions Sat Check: ❌ fail
 Result: ❌ fail
 
 Obligation: unreachable_assert
@@ -61,7 +60,6 @@ Result: ❌ fail
 
 Obligation: reachable_assert
 Property: assert
-Assumptions Sat Check: ✅ pass
 Result: ✅ pass
 -/
 #guard_msgs in
@@ -80,10 +78,10 @@ spec {
 }
 {
   if (x <= 1) {
-    cover [ctest1]: (true);
+    @[checkAssumptionsSat:true] cover [ctest1]: (true);
   } else {
     cover [ctest2]: (x > 2);
-    assert [atest2]: (x > 1);
+    @[checkAssumptionsSat:true] assert [atest2]: (x > 1);
   }
 };
 #end
@@ -97,7 +95,6 @@ Result: ❌ fail
 
 Obligation: ctest2
 Property: cover
-Assumptions Sat Check: ✅ pass
 Result: ✅ pass
 Model:
 ($__x0, 3)
@@ -109,6 +106,6 @@ Result: ✅ pass
 -/
 #guard_msgs in
 #eval verify "z3" coverPgm2
-      (options := {Options.quiet with checkAssumptionsSat := true})
+      (options := {Options.quiet with checkAssumptionsSat := false})
 
 ---------------------------------------------------------------------
diff --git a/StrataTest/Languages/Core/ExprEvalTest.lean b/StrataTest/Languages/Core/ExprEvalTest.lean
index fe61e480c..bcad978e3 100644
--- a/StrataTest/Languages/Core/ExprEvalTest.lean
+++ b/StrataTest/Languages/Core/ExprEvalTest.lean
@@ -70,7 +70,7 @@ def checkValid (e:LExpr CoreLParams.mono): IO Bool := do
       let ans ← Core.SMT.dischargeObligation
         { Options.default with verbose := .quiet }
         (LExpr.freeVars e) "z3" filename.toString
-        {assumptions := [], obligation := smt_term} ctx
+        {assumptions := [], obligation := smt_term, checkAssumptionsSat := false} ctx
       match ans with
       | .ok ([.sat _],_) => return true
       | _ =>
diff --git a/StrataTest/Languages/Core/SarifOutputTests.lean b/StrataTest/Languages/Core/SarifOutputTests.lean
index 3802db9f3..2f62b4436 100644
--- a/StrataTest/Languages/Core/SarifOutputTests.lean
+++ b/StrataTest/Languages/Core/SarifOutputTests.lean
@@ -54,10 +54,9 @@ def makeObligation (label : String) (md : MetaData Expression := #[]) : ProofObl
     metadata := md }
 
 /-- Create a VCResult for testing -/
-def makeVCResult (label : String) (outcome : Outcome) (smtResult : Result := .unknown) (md : MetaData Expression := #[]) : VCResult :=
+def makeVCResult (label : String) (outcome : Outcome) (solverResult : Result := .unknown) (md : MetaData Expression := #[]) : VCResult :=
   { obligation := makeObligation label md
-    smtResult := smtResult
-    result := outcome
+    result := { solverResult := solverResult, result := outcome }
     verbose := .normal }
 
 /-! ## Level Conversion Tests -/
diff --git a/StrataVerify.lean b/StrataVerify.lean
index 7bfafadba..f3be413f3 100644
--- a/StrataVerify.lean
+++ b/StrataVerify.lean
@@ -132,7 +132,7 @@ def main (args : List String) : IO UInt32 := do
         -- Also output standard format
         for vcResult in vcResults do
           let posStr := Imperative.MetaData.formatFileRangeD vcResult.obligation.metadata (some inputCtx.fileMap)
-          println! f!"{posStr} [{vcResult.obligation.label}]: {vcResult.result}"
+          println! f!"{posStr} [{vcResult.obligation.label}]: {vcResult.result.result}"
         let success := vcResults.all Core.VCResult.isSuccess
         if success && !opts.checkOnly then
           println! f!"All {vcResults.size} goals passed."