diff --git a/.gitignore b/.gitignore
index 3776616d98..9f5babd9ab 100644
--- a/.gitignore
+++ b/.gitignore
@@ -12,4 +12,5 @@ vcs/*.smt2
 *.py.ion
 *.py.ion.core.st
 
-Strata.code-workspace
\ No newline at end of file
+Strata.code-workspace
+Build/
\ No newline at end of file
diff --git a/Strata/DDM/Format.lean b/Strata/DDM/Format.lean
index 613a726135..4d97f30839 100644
--- a/Strata/DDM/Format.lean
+++ b/Strata/DDM/Format.lean
@@ -453,7 +453,7 @@ private partial def ArgF.mformatM {α} : ArgF α → FormatM PrecFormat
     if z : entries.size = 0 then
       pure (.atom .nil)
     else do
-      let f i q s := return s ++ "; " ++ (← entries[i].mformatM).format
+      let f i q s := return s ++ ";\n" ++ (← entries[i].mformatM).format
       let a := (← entries[0].mformatM).format
       .atom <$> entries.size.foldlM f (start := 1) a
 
diff --git a/Strata/Languages/Laurel/ConstrainedTypeElim.lean b/Strata/Languages/Laurel/ConstrainedTypeElim.lean
index 7e86c374a1..dce1a2eef3 100644
--- a/Strata/Languages/Laurel/ConstrainedTypeElim.lean
+++ b/Strata/Languages/Laurel/ConstrainedTypeElim.lean
@@ -224,7 +224,7 @@ private def mkWitnessProc (ptMap : ConstrainedTypeMap) (ct : ConstrainedType) :
   { name := mkId s!"$witness_{ct.name.text}"
     inputs := []
     outputs := []
-    body := .Transparent ⟨.Block [witnessInit, assert] none, src⟩
+    body := .Opaque [] (some ⟨.Block [witnessInit, assert] none, src⟩) []
     preconditions := []
     isFunctional := false
     decreases := none }
diff --git a/Strata/Languages/Laurel/ContractPass.lean b/Strata/Languages/Laurel/ContractPass.lean
new file mode 100644
index 0000000000..914192d108
--- /dev/null
+++ b/Strata/Languages/Laurel/ContractPass.lean
@@ -0,0 +1,343 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+public import Strata.Languages.Laurel.MapStmtExpr
+
+/-!
+## Contract Pass (Laurel → Laurel)
+
+Removes pre- and postconditions from all procedures and replaces them with
+explicit precondition/postcondition helper procedures, assumptions, and
+assertions.
+
+For each procedure with contracts:
+- Generate a precondition procedure (`foo$pre`) returning the conjunction of preconditions.
+- Generate a postcondition procedure (`foo$post`) that takes all inputs and all
+  outputs as parameters and returns the conjunction of postconditions. It is
+  marked as functional and does not call the original procedure.
+- Insert `assume foo$pre(inputs)` at the start of the body.
+- Insert `assert foo$post(inputs, outputs)` at the end of the body.
+
+For each call to a contracted procedure:
+- Assign all input arguments to temporary variables before the call.
+- Insert `assert foo$pre(temps)` before the call (precondition check).
+- After the call, insert `assume foo$post(temps, outputs)` (postcondition assumption).
+-/
+
+namespace Strata.Laurel
+
+public section
+
+private def mkMd (e : StmtExpr) : StmtExprMd := { val := e, source := none }
+private def mkVarMd (v : Variable) : VariableMd := { val := v, source := none }
+
+/-- Build a conjunction of expressions. Returns `LiteralBool true` for an empty list. -/
+private def conjoin (exprs : List StmtExprMd) : StmtExprMd :=
+  match exprs with
+  | [] => mkMd (.LiteralBool true)
+  | [e] => e
+  | e :: rest => rest.foldl (fun acc x =>
+      mkMd (.PrimitiveOp .And [acc, x])) e
+
+/-- Name for the precondition helper procedure. -/
+def preCondProcName (procName : String) : String := s!"{procName}$pre"
+
+/-- Name for the postcondition helper procedure. -/
+def postCondProcName (procName : String) : String := s!"{procName}$post"
+
+/-- Get postconditions from a procedure body. -/
+private def getPostconditions (body : Body) : List Condition :=
+  match body with
+  | .Opaque postconds _ _ => postconds
+  | .Abstract postconds => postconds
+  | _ => []
+
+/-- Build a call expression. -/
+private def mkCall (callee : String) (args : List StmtExprMd) : StmtExprMd :=
+  mkMd (.StaticCall (mkId callee) args)
+
+/-- Convert parameters to identifier expressions. -/
+private def paramsToArgs (params : List Parameter) : List StmtExprMd :=
+  params.map fun p => mkMd (.Var (.Local p.name))
+
+/-- Build a helper function that returns the conjunction of the given conditions. -/
+private def mkConditionProc (name : String) (params : List Parameter)
+    (conditions : List Condition) : Procedure :=
+  { name := mkId name
+    inputs := params
+    outputs := [⟨mkId "$result", { val := .TBool, source := none }⟩]
+    preconditions := []
+    decreases := none
+    isFunctional := true
+    body := .Transparent (conjoin (conditions.map (·.condition))) }
+
+/-- Build a postcondition function that takes all inputs and all outputs as
+    parameters and returns the conjunction of postconditions. The function is
+    marked as functional and does not call the original procedure.
+
+    For a procedure `foo(a, b) returns (x, y)` with postcondition `P(a, b, x, y)`,
+    generates:
+    ```
+    function foo$post(a, b, x, y) returns ($result : bool) {
+      P(a, b, x, y)
+    }
+    ```
+-/
+private def mkPostConditionProc (name : String)
+    (inputParams : List Parameter) (outputParams : List Parameter)
+    (conditions : List Condition) : Procedure :=
+  let allParams := inputParams ++ outputParams
+  { name := mkId name
+    inputs := allParams
+    outputs := [⟨mkId "$result", { val := .TBool, source := none }⟩]
+    preconditions := []
+    decreases := none
+    isFunctional := true
+    body := .Transparent (conjoin (conditions.map (·.condition))) }
+
+/-- Extract a combined summary from a list of conditions. -/
+private def combinedSummary (clauses : List Condition) : Option String :=
+  let summaries := clauses.filterMap (·.summary)
+  match summaries with
+  | [] => none
+  | [s] => some s
+  | ss => some (String.intercalate ", " ss)
+
+/-- Information about a procedure's contracts. -/
+private structure ContractInfo where
+  hasPreCondition : Bool
+  hasPostCondition : Bool
+  preName : String
+  postName : String
+  preSummary : Option String
+  postSummary : Option String
+  inputParams : List Parameter
+  outputParams : List Parameter
+
+/-- Collect contract info for all procedures with contracts. -/
+private def collectContractInfo (procs : List Procedure) : Std.HashMap String ContractInfo :=
+  procs.foldl (fun m proc =>
+    let postconds := getPostconditions proc.body
+    let hasPre := !proc.preconditions.isEmpty
+    let hasPost := !postconds.isEmpty
+    if hasPre || hasPost then
+      m.insert proc.name.text {
+        hasPreCondition := hasPre
+        hasPostCondition := hasPost
+        preName := preCondProcName proc.name.text
+        postName := postCondProcName proc.name.text
+        preSummary := combinedSummary proc.preconditions
+        postSummary := combinedSummary postconds
+        inputParams := proc.inputs
+        outputParams := proc.outputs
+      }
+    else m) {}
+
+/-- Transform a procedure body to add assume/assert for its own contracts. -/
+private def transformProcBody (proc : Procedure) (info : ContractInfo) : Body :=
+  let inputArgs := paramsToArgs proc.inputs
+  let postconds := getPostconditions proc.body
+  let preAssume : List StmtExprMd :=
+    if info.hasPreCondition then
+      let preSrc := match proc.preconditions.head? with
+        | some pc => pc.condition.source
+        | none => none
+      [⟨.Assume (mkCall info.preName inputArgs), preSrc⟩]
+    else []
+  let postAssert : List StmtExprMd :=
+    if info.hasPostCondition then
+      postconds.map fun pc =>
+        let summary := pc.summary.getD "postcondition"
+        ⟨.Assert { condition := pc.condition, summary := some summary }, pc.condition.source⟩
+    else []
+  match proc.body with
+  | .Transparent body =>
+    .Transparent ⟨.Block (preAssume ++ [body] ++ postAssert) none, body.source⟩
+  | .Opaque _ (some impl) _ =>
+    .Opaque [] (some ⟨.Block (preAssume ++ [impl] ++ postAssert) none, impl.source⟩) []
+  | .Opaque _ none mods =>
+    .Opaque [] none mods
+  | .Abstract _ =>
+    .Abstract []
+  | b => b
+
+/-- Generate temporary variable assignments for input arguments at a call site.
+    Returns (temp declarations+assignments, temp variable references).
+    Uses the parameter types from the procedure's contract info so that
+    resolution can type-check the generated temporaries.
+    `callIdx` distinguishes multiple calls to the same procedure. -/
+private def mkTempAssignments (args : List StmtExprMd) (calleeName : String)
+    (inputParams : List Parameter) (callIdx : Nat) (src : Option FileRange)
+    : List StmtExprMd × List StmtExprMd :=
+  let indexed := args.zipIdx
+  let decls := indexed.map fun (arg, i) =>
+    let tempName := s!"${calleeName}${callIdx}$arg{i}"
+    let paramType := match inputParams[i]? with
+      | some p => p.type
+      | none => { val := .Unknown, source := none }
+    let param : Parameter := { name := mkId tempName, type := paramType }
+    ⟨StmtExpr.Assign [mkVarMd (.Declare param)] arg, src⟩
+  let refs := indexed.map fun (_, i) =>
+    let tempName := s!"${calleeName}${callIdx}$arg{i}"
+    mkMd (.Var (.Local (mkId tempName)))
+  (decls, refs)
+
+/-- Rewrite a single statement that may be a call to a contracted procedure.
+    Returns a list of statements (the original plus any inserted assert/assume).
+    Takes and returns a call counter for generating unique temp variable names.
+    When `isFunctional` is true, precondition checks use `assume` instead of
+    `assert` since asserts are not supported in functions during Core translation.
+
+    At call sites:
+    1. Assign input arguments to temporary variables.
+    2. Assert precondition using temps.
+    3. Execute the call using temps as arguments.
+    4. Assume postcondition using temps + output variables. -/
+private def rewriteStmt (contractInfoMap : Std.HashMap String ContractInfo)
+    (isFunctional : Bool) (callCounter : Nat) (e : StmtExprMd) : List StmtExprMd × Nat :=
+  let src := e.source
+  let mkWithSrc (se : StmtExpr) : StmtExprMd := ⟨se, src⟩
+  match e.val with
+  | .Assign targets (.mk (.StaticCall callee args) callSrc) =>
+    match contractInfoMap.get? callee.text with
+    | some info =>
+      let (tempDecls, tempRefs) := mkTempAssignments args callee.text info.inputParams callCounter src
+      let callWithTemps : StmtExprMd := ⟨.Assign targets ⟨.StaticCall callee tempRefs, callSrc⟩, src⟩
+      let preCheck := if info.hasPreCondition then
+        if isFunctional then
+          [mkWithSrc (.Assume (mkCall info.preName tempRefs))]
+        else
+          [mkWithSrc (.Assert { condition := mkCall info.preName tempRefs, summary := some (info.preSummary.getD "precondition") })]
+        else []
+      -- After the call, assume postcondition with temps (inputs) + output variables
+      let outputArgs := targets.filterMap fun t =>
+        match t.val with
+        | .Local name => some (mkMd (.Var (.Local name)))
+        | .Declare param => some (mkMd (.Var (.Local param.name)))
+        | _ => none
+      let postAssume := if info.hasPostCondition
+        then [mkWithSrc (.Assume (mkCall info.postName (tempRefs ++ outputArgs)))] else []
+      (tempDecls ++ preCheck ++ [callWithTemps] ++ postAssume, callCounter + 1)
+    | none => ([e], callCounter)
+  | .StaticCall callee args =>
+    match contractInfoMap.get? callee.text with
+    | some info =>
+      let (tempDecls, tempRefs) := mkTempAssignments args callee.text info.inputParams callCounter src
+      let preCheck := if info.hasPreCondition then
+        if isFunctional then
+          [mkWithSrc (.Assume (mkCall info.preName tempRefs))]
+        else
+          [mkWithSrc (.Assert { condition := mkCall info.preName tempRefs, summary := some (info.preSummary.getD "precondition") })]
+        else []
+      -- For bare calls with postconditions, capture outputs in temp variables
+      -- so we can pass them to the $post function.
+      let (callStmt, postAssume) :=
+        if info.hasPostCondition && !info.outputParams.isEmpty then
+          let outputTempDecls := info.outputParams.zipIdx.map fun (p, i) =>
+            let tempName := s!"${callee.text}${callCounter}$out{i}"
+            mkVarMd (.Declare { name := mkId tempName, type := p.type })
+          let callWithOutputs : StmtExprMd :=
+            ⟨.Assign outputTempDecls ⟨.StaticCall callee tempRefs, src⟩, src⟩
+          let outputRefs := info.outputParams.zipIdx.map fun (_, i) =>
+            let tempName := s!"${callee.text}${callCounter}$out{i}"
+            mkMd (.Var (.Local (mkId tempName)))
+          let assume := [mkWithSrc (.Assume (mkCall info.postName (tempRefs ++ outputRefs)))]
+          (callWithOutputs, assume)
+        else
+          (mkWithSrc (.StaticCall callee tempRefs), [])
+      (tempDecls ++ preCheck ++ [callStmt] ++ postAssume, callCounter + 1)
+    | none => ([e], callCounter)
+  | _ => ([e], callCounter)
+
+/-- Rewrite call sites in a statement/expression tree. Processes Block children
+    at the statement level to avoid interfering with expression-level calls. -/
+private def rewriteCallSites (contractInfoMap : Std.HashMap String ContractInfo)
+    (isFunctional : Bool) (expr : StmtExprMd) : StmtExprMd :=
+  let (result, _) := StateT.run (s := (0 : Nat)) <|
+    mapStmtExprM (m := StateM Nat) (fun e => do
+      match e.val with
+      | .Block stmts label =>
+        let mut newStmts : List StmtExprMd := []
+        let mut counter ← get
+        for stmt in stmts do
+          let (expanded, counter') := rewriteStmt contractInfoMap isFunctional counter stmt
+          newStmts := newStmts ++ expanded
+          counter := counter'
+        set counter
+        if newStmts.length == stmts.length then return e
+        else return ⟨.Block newStmts label, e.source⟩
+      | _ => return e) expr
+  -- Handle top-level non-Block statements (e.g., bare Assign or StaticCall)
+  let (expanded, _) := rewriteStmt contractInfoMap isFunctional 0 result
+  match expanded with
+  | [single] => single
+  | many => mkMd (.Block many none)
+
+/-- Rewrite call sites in all bodies of a procedure. -/
+private def rewriteCallSitesInProc (contractInfoMap : Std.HashMap String ContractInfo)
+    (proc : Procedure) : Procedure :=
+  let rw := rewriteCallSites contractInfoMap proc.isFunctional
+  match proc.body with
+  | .Transparent body =>
+    { proc with body := .Transparent (rw body) }
+  | .Opaque posts impl mods =>
+    let body := Body.Opaque (posts.map (·.mapCondition rw)) (impl.map rw) (mods.map rw)
+    { proc with body := body }
+  | _ => proc
+
+/-- Build an axiom expression from `invokeOn` trigger and ensures clauses.
+    Produces `∀ p1, ∀ p2, ..., ∀ pn :: { trigger } (ensures1 && ensures2 && ...)`.
+    The trigger controls when the SMT solver instantiates the axiom. -/
+private def mkInvokeOnAxiom (params : List Parameter) (trigger : StmtExprMd)
+    (postconds : List Condition) : StmtExprMd :=
+  let body := conjoin (postconds.map (·.condition))
+  -- Wrap in nested Forall from last param (innermost) to first (outermost).
+  -- The trigger is placed on the innermost quantifier.
+  params.foldr (init := (body, true)) (fun p (acc, isInnermost) =>
+    let trig := if isInnermost then some trigger else none
+    (mkMd (.Quantifier .Forall p trig acc), false)) |>.1
+
+/-- Run the contract pass on a Laurel program.
+    All procedures with contracts are transformed. -/
+def contractPass (program : Program) : Program :=
+  let contractInfoMap := collectContractInfo program.staticProcedures
+
+  -- Generate helper procedures for all procedures with contracts
+  let helperProcs := program.staticProcedures.flatMap fun proc =>
+    let postconds := getPostconditions proc.body
+    let preProc :=
+      if proc.preconditions.isEmpty then []
+      else [mkConditionProc (preCondProcName proc.name.text) proc.inputs proc.preconditions]
+    let postProc :=
+      if postconds.isEmpty then []
+      else [mkPostConditionProc (postCondProcName proc.name.text)
+              proc.inputs proc.outputs postconds]
+    preProc ++ postProc
+
+  -- Transform procedures: strip contracts, add assume/assert, rewrite call sites
+  let transformedProcs := program.staticProcedures.map fun proc =>
+    let proc := match proc.invokeOn with
+      | some trigger =>
+        let postconds := getPostconditions proc.body
+        if postconds.isEmpty then { proc with invokeOn := none }
+        else { proc with
+          axioms := [mkInvokeOnAxiom proc.inputs trigger postconds]
+          invokeOn := none }
+      | none => proc
+    let proc := match contractInfoMap.get? proc.name.text with
+      | some info =>
+        { proc with
+          preconditions := []
+          body := transformProcBody proc info }
+      | none => proc
+    -- Rewrite call sites in the procedure body
+    rewriteCallSitesInProc contractInfoMap proc
+
+  { program with staticProcedures := helperProcs ++ transformedProcs }
+
+end -- public section
+end Strata.Laurel
diff --git a/Strata/Languages/Laurel/EliminateReturnStatements.lean b/Strata/Languages/Laurel/EliminateReturnStatements.lean
new file mode 100644
index 0000000000..de8494a2ba
--- /dev/null
+++ b/Strata/Languages/Laurel/EliminateReturnStatements.lean
@@ -0,0 +1,62 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+public import Strata.Languages.Laurel.MapStmtExpr
+
+/-!
+# Eliminate Return Statements
+
+Replaces `return` statements in imperative procedure bodies with assignments
+to the output parameters followed by an `exit` to a labelled block that wraps
+the entire body. This ensures that code placed after the body block (e.g.,
+postcondition assertions inserted by the contract pass) is always reached.
+
+This pass should run after `EliminateReturnsInExpression` (which handles
+functional/expression-position returns) and before the contract pass.
+-/
+
+namespace Strata.Laurel
+
+public section
+
+private def returnLabel : String := "$return"
+
+/-- Replace `Return val` with `output := val; exit "$return"` (or just `exit`
+    for valueless returns). Uses `mapStmtExpr` for bottom-up traversal. -/
+private def replaceReturn (source: Option FileRange) (outputs : List Parameter) (expr : StmtExprMd) : StmtExprMd :=
+  mapStmtExpr (fun e =>
+    match e.val with
+    | .Return (some val) =>
+      match outputs with
+      | [out] =>
+        let assign := ⟨ .Assign [⟨ .Local out.name, source⟩ ] val, source⟩
+        let exit := ⟨ .Exit returnLabel, source⟩
+        ⟨.Block [assign, exit] none, e.source⟩
+      | _ => ⟨ .Exit returnLabel, source⟩
+    | .Return none => ⟨ .Exit returnLabel, source⟩
+    | _ => e) expr
+
+/-- Transform a single procedure: wrap body in a labelled block and replace returns. -/
+private def eliminateReturnStmts (proc : Procedure) : Procedure :=
+  match proc.body with
+  | .Opaque postconds (some impl) mods =>
+    let impl' := (replaceReturn proc.name.source) proc.outputs impl
+    let wrapped : StmtExprMd := { val := .Block [impl'] (some returnLabel), source := impl.source }
+    { proc with body := .Opaque postconds (some wrapped) mods }
+  | .Transparent body =>
+    let body' := (replaceReturn proc.name.source) proc.outputs body
+    let wrapped : StmtExprMd := { val := .Block [body'] (some returnLabel), source := body.source }
+    { proc with body := .Transparent wrapped }
+  | _ => proc
+
+/-- Transform a program by eliminating return statements in all procedure bodies. -/
+def eliminateReturnStatements (program : Program) : Program :=
+  { program with staticProcedures := program.staticProcedures.map eliminateReturnStmts }
+
+end -- public section
+
+end Strata.Laurel
diff --git a/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean
index 1ed8e93828..76e4d1a2aa 100644
--- a/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean
+++ b/Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean
@@ -238,6 +238,7 @@ private def procedureToOp (proc : Procedure) : Strata.Operation :=
   let requiresArgs := proc.preconditions.map requiresClauseToArg |>.toArray
   let invokeOnArg := optionArg (proc.invokeOn.map fun e =>
     laurelOp "invokeOnClause" #[stmtExprToArg e])
+  let axiomsArgs := proc.axioms.map (fun ax => laurelOp "axiomClause" #[stmtExprToArg ax]) |>.toArray
   let (opaqueSpecArg, bodyArg) := match proc.body with
     | .Transparent body =>
       (optionArg none, optionArg (some (laurelOp "body" #[stmtExprToArg body])))
@@ -260,6 +261,7 @@ private def procedureToOp (proc : Procedure) : Strata.Operation :=
       returnParamsArg,
       seqArg requiresArgs,
       invokeOnArg,
+      seqArg axiomsArgs,
       opaqueSpecArg,
       bodyArg
     ] }
diff --git a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
index 8d3dcdc460..2caa173e0e 100644
--- a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
+++ b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
@@ -465,9 +465,9 @@ def parseProcedure (arg : Arg) : TransM Procedure := do
 
   match op.name, op.args with
   | q`Laurel.procedure, #[nameArg, paramArg, returnTypeArg, returnParamsArg,
-      requiresArg, invokeOnArg, opaqueSpecArg, bodyArg]
+      requiresArg, invokeOnArg, axiomsArg, opaqueSpecArg, bodyArg]
   | q`Laurel.function, #[nameArg, paramArg, returnTypeArg, returnParamsArg,
-      requiresArg, invokeOnArg, opaqueSpecArg, bodyArg] =>
+      requiresArg, invokeOnArg, axiomsArg, opaqueSpecArg, bodyArg] =>
     let name ← translateIdent nameArg
     let parameters ← translateParameters paramArg
     -- Either returnTypeArg or returnParamsArg may have a value, not both
@@ -497,6 +497,15 @@ def parseProcedure (arg : Arg) : TransM Procedure := do
         | _, _ => TransM.error s!"Expected invokeOnClause operation, got {repr invokeOnOp.name}"
       | .option _ none => pure none
       | _ => pure none
+    -- Parse axiom clauses (zero or more)
+    let axioms ← match axiomsArg with
+      | .seq _ _ args => args.toList.mapM fun clauseArg => do
+        match clauseArg with
+        | .op clauseOp => match clauseOp.name, clauseOp.args with
+          | q`Laurel.axiomClause, #[exprArg] => translateStmtExpr exprArg
+          | _, _ => TransM.error s!"Expected axiomClause operation, got {repr clauseOp.name}"
+        | _ => TransM.error s!"Expected axiomClause operation in axioms sequence"
+      | _ => pure []
     -- Parse optional opaqueSpec (contains ensures and modifies)
     let (isOpaque, postconditions, modifies) ← match opaqueSpecArg with
       | .option _ (some (.op opaqueSpecOp)) => match opaqueSpecOp.name, opaqueSpecOp.args with
@@ -535,11 +544,12 @@ def parseProcedure (arg : Arg) : TransM Procedure := do
       decreases := none
       isFunctional := op.name == q`Laurel.function
       invokeOn := invokeOn
+      axioms := axioms
       body := procBody
     }
   | q`Laurel.procedure, args
   | q`Laurel.function, args =>
-    TransM.error s!"parseProcedure expects 8 arguments, got {args.size}"
+    TransM.error s!"parseProcedure expects 9 arguments, got {args.size}"
   | _, _ =>
     TransM.error s!"parseProcedure expects procedure or function, got {repr op.name}"
 
diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
index 02e2159643..d3f77fe15f 100644
--- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
+++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
@@ -9,7 +9,7 @@ module
 -- Laurel dialect definition, loaded from LaurelGrammar.st
 -- NOTE: Changes to LaurelGrammar.st are not automatically tracked by the build system.
 -- Update this file (e.g. this comment) to trigger a recompile after modifying LaurelGrammar.st.
--- Last grammar change: multiAssign supports field access targets, added opaque keyword.
+-- Last grammar change: added axiom clause to procedure/function definitions.
 public import Strata.DDM.Integration.Lean
 public meta import Strata.DDM.Integration.Lean
 
diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
index b81b0d8b11..8a20d1be14 100644
--- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
+++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
@@ -106,8 +106,8 @@ op ifThenElse (cond: StmtExpr, thenBranch: StmtExpr, elseBranch: Option ElseBran
 op assert (cond : StmtExpr, errorMessage: Option ErrorSummary) : StmtExpr => @[prec(0)] "assert " cond:0 errorMessage:0;
 op assume (cond : StmtExpr) : StmtExpr => @[prec(0)] "assume " cond:0;
 op return (value : StmtExpr) : StmtExpr => @[prec(0)] "return " value:0;
-op block (stmts : SemicolonSepBy StmtExpr) : StmtExpr => @[prec(1000)] "{ " stmts " }";
-op labelledBlock (stmts : SemicolonSepBy StmtExpr, label : Ident) : StmtExpr => @[prec(1000)] "{ " stmts " }" label;
+op block (stmts : SemicolonSepBy StmtExpr) : StmtExpr => @[prec(1000)] "{\n  " indent(2, stmts) "\n}";
+op labelledBlock (stmts : SemicolonSepBy StmtExpr, label : Ident) : StmtExpr => @[prec(1000)] "{\n  " indent(2, stmts) "\n}" label;
 op exit (label : Ident) : StmtExpr => @[prec(0)] "exit " label;
 
 // While loops
@@ -159,6 +159,9 @@ op returnType(returnType: LaurelType): ReturnType => ": " returnType;
 category InvokeOnClause;
 op invokeOnClause(trigger: StmtExpr): InvokeOnClause => "\n  invokeOn " trigger:0;
 
+category AxiomClause;
+op axiomClause(cond: StmtExpr): AxiomClause => "\n  axiom " cond:0;
+
 category RequiresClause;
 op requiresClause(cond: StmtExpr, errorMessage: Option ErrorSummary): RequiresClause => "\n  requires " cond:0 errorMessage;
 
@@ -186,18 +189,20 @@ op procedure (name : Ident, parameters: CommaSepBy Parameter,
   returnParameters: Option ReturnParameters,
   requires: Seq RequiresClause,
   invokeOn: Option InvokeOnClause,
+  axioms: Seq AxiomClause,
   opaqueSpec: Option OpaqueSpec,
   body : Option Body) : Procedure =>
-  "procedure " name "(" parameters ")" returnType returnParameters requires invokeOn opaqueSpec body ";";
+  "procedure " name "(" parameters ")" returnType returnParameters requires invokeOn axioms opaqueSpec body ";";
 
 op function (name : Ident, parameters: CommaSepBy Parameter,
   returnType: Option ReturnType,
   returnParameters: Option ReturnParameters,
   requires: Seq RequiresClause,
   invokeOn: Option InvokeOnClause,
+  axioms: Seq AxiomClause,
   opaqueSpec: Option OpaqueSpec,
   body : Option Body) : Procedure =>
-  "function " name "(" parameters ")" returnType returnParameters requires invokeOn opaqueSpec body ";";
+  "function " name "(" parameters ")" returnType returnParameters requires invokeOn axioms opaqueSpec body ";";
 
 op composite (name: Ident, extending: Option Extends, fields: Seq Field, procedures: Seq Procedure): Composite => "composite " name extending " {" fields procedures " }";
 
diff --git a/Strata/Languages/Laurel/HeapParameterization.lean b/Strata/Languages/Laurel/HeapParameterization.lean
index fecaf5350c..f68b93c031 100644
--- a/Strata/Languages/Laurel/HeapParameterization.lean
+++ b/Strata/Languages/Laurel/HeapParameterization.lean
@@ -315,7 +315,11 @@ where
               let isLast := idx == n - 1
               let s' ← recurse s (isLast && valueUsed)
               let rest' ← processStmts (idx + 1) rest
-              pure (s' :: rest')
+              -- Flatten blocks created by recurse so that
+              -- Declare targets remain in the enclosing scope.
+              match s'.val with
+              | .Block innerStmts (some "$inlineMe") => pure (innerStmts ++ rest')
+              | _ => pure (s' :: rest')
           termination_by sizeOf remaining
         let stmts' ← processStmts 0 stmts
         return ⟨ .Block stmts' label, source ⟩
@@ -389,7 +393,7 @@ where
 
       -- Create a block if necessary
       if suffixes.length > 0 then
-        return ⟨ StmtExpr.Block (newAssign :: suffixes) none, source ⟩
+        return ⟨ StmtExpr.Block (newAssign :: suffixes) (some "$inlineMe"), source ⟩
       else
         return newAssign
 
diff --git a/Strata/Languages/Laurel/Laurel.lean b/Strata/Languages/Laurel/Laurel.lean
index a5cd11439c..e0de8628eb 100644
--- a/Strata/Languages/Laurel/Laurel.lean
+++ b/Strata/Languages/Laurel/Laurel.lean
@@ -200,6 +200,9 @@ structure Procedure : Type where
       whose body is the ensures clause universally quantified over the procedure's inputs,
       with this expression as the SMT trigger. -/
   invokeOn : Option (AstNode StmtExpr) := none
+  /-- Axioms to emit alongside this procedure. Populated by the contract pass from
+      `invokeOn` and ensures clauses. -/
+  axioms : List (AstNode StmtExpr) := []
 
 /--
 A typed parameter for a procedure.
@@ -459,6 +462,11 @@ def Body.isTransparent : Body → Bool
   | .Transparent _ => true
   | _ => false
 
+def Body.hasPostconditions : Body → Bool
+  | .Opaque posts _ _ => !posts.isEmpty
+  | .Abstract posts => !posts.isEmpty
+  | _ => false
+
 def HighTypeMd.isBool (t : HighTypeMd) : Bool := t.val.isBool
 
 /--
diff --git a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
index c6984120fe..a2c60847c2 100644
--- a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
+++ b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
@@ -8,8 +8,11 @@ module
 public import Strata.Languages.Laurel.LaurelToCoreTranslator
 import Strata.Languages.Laurel.DesugarShortCircuit
 import Strata.Languages.Laurel.EliminateReturnsInExpression
+import Strata.Languages.Laurel.EliminateReturnStatements
 import Strata.Languages.Laurel.EliminateValueReturns
 import Strata.Languages.Laurel.ConstrainedTypeElim
+import Strata.Languages.Laurel.ContractPass
+import Strata.Languages.Laurel.RemoveFunctionAssumptions
 import Strata.Languages.Laurel.TypeAliasElim
 import Strata.Languages.Core.Verifier
 import Strata.Util.Profile
@@ -180,10 +183,32 @@ private def runLaurelPasses (options : LaurelTranslateOptions) (program : Progra
     -- Run resolve after the pass if needed
     if pass.needsResolves then
       let result := resolve program (some model)
+      let newErrors := result.errors.filter fun e => !resolutionErrors.contains e
+      if !newErrors.isEmpty then
+        let newDiags := newErrors.toList.map fun d =>
+          { d with message :=
+              s!"Internal error: resolution after '{pass.name}' introduced this diagnostic: {d.message}" }
+        emit pass.name "laurel.st" program
+        return (program, model, allDiags ++ newDiags, allStats)
       program := result.program
       model := result.model
     emit pass.name "laurel.st" program
 
+  program := eliminateReturnStatements program
+  emit "EliminateReturnStatements" "laurel.st" program
+
+  program := contractPass program
+  emit "ContractPass" "laurel.st" program
+
+  program := removeFunctionAssumptions program
+  emit "RemoveFunctionAssumptions" "laurel.st" program
+
+  -- Re-resolve after contractPass so the model includes the generated
+  -- helper procedures ($pre, $post) and their isFunctional status.
+  let contractResult := resolve program (some model)
+  program := contractResult.program
+  model := contractResult.model
+
   return (program, model, allDiags, allStats)
 
 /--
@@ -211,8 +236,13 @@ def translateWithLaurel (options : LaurelTranslateOptions) (program : Program)
     if let some coreProgram := coreProgramOption then
       emit "CoreProgram" "core.st" coreProgram
     let mut allDiagnostics := passDiags ++ translateState.diagnostics
+
+    if translateState.coreDiagnostics.length > 0 && allDiagnostics.isEmpty then
+      -- The program was suppressed but no diagnostics explain why — report the core diagnostics.
+      allDiagnostics := allDiagnostics ++ translateState.coreDiagnostics
+
     let coreProgramOption :=
-      if translateState.coreProgramHasSuperfluousErrors then none else coreProgramOption
+      if !translateState.coreDiagnostics.isEmpty then none else coreProgramOption
     return (coreProgramOption, allDiagnostics, program, stats)
 
 /--
diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean
index cccf8ab011..d504483f2c 100644
--- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean
+++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean
@@ -32,7 +32,7 @@ import Strata.Languages.Laurel.ConstrainedTypeElim
 import Strata.Util.Tactics
 
 open Core (VCResult VCResults VerifyOptions)
-open Core (intAddOp intSubOp intMulOp intSafeDivOp intSafeModOp intSafeDivTOp intSafeModTOp intNegOp intLtOp intLeOp intGtOp intGeOp boolAndOp boolOrOp boolNotOp boolImpliesOp strConcatOp)
+open Core (intAddOp intSubOp intMulOp intDivOp intSafeDivOp intModOp intSafeModOp intDivTOp intSafeDivTOp intModTOp intSafeModTOp intNegOp intLtOp intLeOp intGtOp intGeOp boolAndOp boolOrOp boolNotOp boolImpliesOp strConcatOp)
 open Core (realAddOp realSubOp realMulOp realDivOp realNegOp realLtOp realLeOp realGtOp realGeOp)
 
 namespace Strata.Laurel
@@ -62,8 +62,16 @@ structure TranslateState where
   model : SemanticModel
   /-- Overflow check configuration -/
   overflowChecks : Core.OverflowChecks := {}
-  /-- Do not process the produces Core program, since it has superfluous errors -/
-  coreProgramHasSuperfluousErrors: Bool := false
+  /-- Diagnostics that indicate the Core program should not be processed further.
+      When non-empty, the produced Core program is suppressed. Each entry records
+      why the program was deemed invalid so that if no other diagnostics explain
+      the suppression, these can be surfaced to the user. -/
+  coreDiagnostics : List DiagnosticModel := []
+  /-- When `true`, use safe division (`intSafeDivOp`) and safe datatype selectors
+      (with preconditions). When `false`, use unsafe division (`intDivOp`) and
+      unsafe datatype selectors (without preconditions).
+      Set to `true` for proof procedures and `false` for functions. -/
+  proof : Bool := false
 
 /-- The translation monad: state over Except, allowing both accumulated diagnostics and hard failures -/
 @[expose] abbrev TranslateM := OptionT (StateM TranslateState)
@@ -72,8 +80,28 @@ structure TranslateState where
 def emitDiagnostic (d : DiagnosticModel) : TranslateM Unit :=
   modify fun s => { s with diagnostics := s.diagnostics ++ [d] }
 
-private def invalidCoreType : TranslateM LMonoTy := do
-  modify fun s => { s with coreProgramHasSuperfluousErrors := true }
+/-- Adjust a datatype selector (destructor) name based on the `proof` flag.
+    Destructor names contain `..` (e.g. `IntList..head`, `IntList..head!`).
+    Tester names also contain `..` but start with `is` after the separator.
+    - `proof = true` → use safe selectors (strip `!` suffix)
+    - `proof = false` → use unsafe selectors (add `!` suffix) -/
+private def adjustSelectorName (name : String) (proof : Bool) : String :=
+  -- Only adjust destructor names (contain ".." but are not testers)
+  match name.splitOn ".." with
+  | [_, suffix] =>
+    if suffix.startsWith "is" then name  -- tester, leave unchanged
+    else if proof then
+      name
+      -- Safe: strip trailing "!"
+      -- if name.endsWith "!" then (name.dropEnd 1).toString else name
+    else
+      -- Unsafe: add trailing "!" if not already present
+      if name.endsWith "!" then name else name ++ "!"
+  | _ => name  -- not a destructor name, leave unchanged
+
+private def invalidCoreType (source : Option FileRange := none) (reason : String := "Type could not be translated to Core (resolution error placeholder)") : TranslateM LMonoTy := do
+  modify fun s => { s with coreDiagnostics := s.coreDiagnostics ++
+    [diagnosticFromSource source reason DiagnosticType.StrataBug] }
   return .tcons s!"LaurelResolutionErrorPlaceholder" []
 
 /-
@@ -97,14 +125,16 @@ def translateType (ty : HighTypeMd) : TranslateM LMonoTy := do
     | some (.datatypeDefinition dt) => return .tcons dt.name.text []
     | some (.datatypeConstructor typeName _) => return .tcons typeName.text []
     | _ => do -- resolution should have already emitted a diagnostic
-      modify fun s => { s with coreProgramHasSuperfluousErrors := true }
+      modify fun s => { s with coreDiagnostics := s.coreDiagnostics ++
+        [diagnosticFromSource ty.source s!"UserDefined type could not be resolved to a composite or datatype" DiagnosticType.StrataBug] }
       return .tcons "Composite" []
   | .TCore s => return .tcons s []
   | .TReal => return LMonoTy.real
+  | .MultiValuedExpr _ => invalidCoreType
   | .Unknown => invalidCoreType
   | _ => do
     emitDiagnostic (diagnosticFromSource ty.source "cannot translate type to Core: not supported yet" DiagnosticType.StrataBug)
-    invalidCoreType
+    invalidCoreType ty.source s!"cannot translate type to Core: not supported yet"
 
 termination_by ty.val
 decreasing_by all_goals (first | (cases elementType; term_by_mem) | (cases keyType; term_by_mem) | (cases valueType; term_by_mem))
@@ -129,7 +159,7 @@ private def freshId : TranslateM Nat := do
 /-- Throw a hard diagnostic error, aborting the current translation -/
 def throwExprDiagnostic (d : DiagnosticModel): TranslateM Core.Expression.Expr := do
   emitDiagnostic d
-  modify fun s => { s with coreProgramHasSuperfluousErrors := true }
+  modify fun s => { s with coreDiagnostics := s.coreDiagnostics ++ [d] }
   let id ← freshId
   return LExpr.fvar () (⟨s!"DUMMY_VAR_{id}", ()⟩) none
 
@@ -152,6 +182,7 @@ def translateExpr (expr : StmtExprMd)
   let s ← get
   let model := s.model
   let md := astNodeToCoreMd expr
+  let proof := (← get).proof
   let disallowed (source : Option FileRange) (msg : String) : TranslateM Core.Expression.Expr := do
     if isPureContext then
       throwExprDiagnostic $ diagnosticFromSource source msg
@@ -208,10 +239,10 @@ def translateExpr (expr : StmtExprMd)
     | .Add => return binOp (if isReal then realAddOp else intAddOp)
     | .Sub => return binOp (if isReal then realSubOp else intSubOp)
     | .Mul => return binOp (if isReal then realMulOp else intMulOp)
-    | .Div => return binOp (if isReal then realDivOp else intSafeDivOp)
-    | .Mod => return binOp intSafeModOp
-    | .DivT => return binOp intSafeDivTOp
-    | .ModT => return binOp intSafeModTOp
+    | .Div => return binOp (if isReal then realDivOp else if proof then intSafeDivOp else intDivOp)
+    | .Mod => return binOp (if (← get).proof then intSafeModOp else intModOp)
+    | .DivT => return binOp (if (← get).proof then intSafeDivTOp else intDivTOp)
+    | .ModT => return binOp (if (← get).proof then intSafeModTOp else intModTOp)
     | .Lt => return binOp (if isReal then realLtOp else intLtOp)
     | .Leq => return binOp (if isReal then realLeOp else intLeOp)
     | .Gt => return binOp (if isReal then realGtOp else intGtOp)
@@ -238,7 +269,8 @@ def translateExpr (expr : StmtExprMd)
       if isPureContext && !model.isFunction callee then
         disallowed expr.source "calls to procedures are not supported in functions or contracts"
       else
-        let fnOp : Core.Expression.Expr := .op () ⟨callee.text, ()⟩ none
+        let calleeName := adjustSelectorName callee.text (← get).proof
+        let fnOp : Core.Expression.Expr := .op () ⟨calleeName, ()⟩ none
         args.attach.foldlM (fun acc ⟨arg, _⟩ => do
           let re ← translateExpr arg boundVars isPureContext
           return .app () acc re) fnOp
@@ -345,7 +377,7 @@ private def exprAsUnusedInit (expr : StmtExprMd) (md : Imperative.MetaData Core.
 
 def throwStmtDiagnostic (d : DiagnosticModel): TranslateM (List Core.Statement) := do
   emitDiagnostic d
-  modify fun s => { s with coreProgramHasSuperfluousErrors := true }
+  modify fun s => { s with coreDiagnostics := s.coreDiagnostics ++ [d] }
   return []
 
 /--
@@ -493,8 +525,9 @@ def translateStmt (stmt : StmtExprMd)
       | none =>
           return [.exit (some "$body") md]
       | some _ =>
-          emitDiagnostic $ md.toDiagnostic "Return statement with value should have been eliminated by EliminateValueReturns pass" DiagnosticType.StrataBug
-          modify fun s => { s with coreProgramHasSuperfluousErrors := true }
+          let d := md.toDiagnostic "Return statement with value should have been eliminated by EliminateValueReturns pass" DiagnosticType.StrataBug
+          emitDiagnostic d
+          modify fun s => { s with coreDiagnostics := s.coreDiagnostics ++ [d] }
           return [.exit (some "$body") md]
   | .While cond invariants decreasesExpr body =>
       let condExpr ← translateExpr cond
@@ -547,6 +580,7 @@ Diagnostics from disallowed constructs in preconditions, postconditions, and bod
 are emitted into the monad state.
 -/
 def translateProcedure (proc : Procedure) : TranslateM Core.Procedure := do
+  modify fun s => { s with proof := true }
   let inputPairs ← proc.inputs.mapM translateParameterToCore
   let inputs := inputPairs
   let outputs ← proc.outputs.mapM translateParameterToCore
@@ -638,6 +672,7 @@ Translate a Laurel Procedure to a Core Function (when applicable) using `Transla
 Diagnostics for disallowed constructs in the function body are emitted into the monad state.
 -/
 def translateProcedureToFunction (options: LaurelTranslateOptions) (isRecursive: Bool) (proc : Procedure) : TranslateM Core.Decl := do
+  modify fun s => { s with proof := false }
   let inputs ← proc.inputs.mapM translateParameterToCore
   let outputTy ← match proc.outputs.head? with
     | some p => translateType p.type
@@ -670,7 +705,7 @@ def translateProcedureToFunction (options: LaurelTranslateOptions) (isRecursive:
   let body ← match proc.body with
     | .Transparent bodyExpr => some <$> translateExpr bodyExpr [] (isPureContext := true)
     | .Opaque _ (some bodyExpr) _ =>
-      emitDiagnostic (diagnosticFromSource proc.name.source "functions with postconditions are not yet supported")
+      emitDiagnostic (diagnosticFromSource proc.name.source s!"opaque function '{proc.name}' is not yet supported")
       some <$> translateExpr bodyExpr [] (isPureContext := true)
     | _ => pure none
   let f : Core.Function := {
@@ -733,12 +768,11 @@ def translateLaurelToCore (options: LaurelTranslateOptions) (program : Program)
       else
         let procDecls ← procs.flatMapM fun proc => do
           let procDecl ← translateProcedure proc
-          -- Turn free postconditions into axioms placed right behind the related procedure
-          let axiomDecls : List Core.Decl ← match proc.invokeOn with
-            | none => pure []
-            | some trigger => do
-              let axDecl? ← translateInvokeOnAxiom proc trigger
-              pure axDecl?.toList
+          -- Translate axioms (populated by the contract pass from invokeOn + ensures)
+          -- Axioms are emitted after the procedure that introduces them.
+          let axiomDecls ← proc.axioms.mapM fun ax => do
+            let coreExpr ← translateExpr ax [] (isPureContext := true)
+            return Core.Decl.ax { name := s!"invokeOn_{proc.name.text}", e := coreExpr } (identifierToCoreMd proc.name)
           return [Core.Decl.proc procDecl (identifierToCoreMd proc.name)] ++ axiomDecls
         return procDecls
     | .datatypes dts => do
diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean
index 65af0996d5..7c63b6870f 100644
--- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean
+++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean
@@ -157,45 +157,48 @@ private def computeType (expr : StmtExprMd) : LiftM HighTypeMd := do
   let s ← get
   return computeExprType s.model expr
 
-/-- Check if an expression contains any assignments or imperative calls (recursively). -/
-def containsAssignmentOrImperativeCall (model: SemanticModel) (expr : StmtExprMd) : Bool :=
+/-- Check if an expression contains any assignments (recursively). -/
+def containsAssignment (expr : StmtExprMd) : Bool :=
   match expr with
   | AstNode.mk val _ =>
   match val with
   | .Assign .. => true
-  | .StaticCall name args1 =>
-    (match model.get name with
-    | .staticProcedure proc => !proc.isFunctional
-    | _ => false) ||
-      args1.attach.any (fun x => containsAssignmentOrImperativeCall model x.val)
-  | .PrimitiveOp _ args2 => args2.attach.any (fun x => containsAssignmentOrImperativeCall model x.val)
-  | .Block stmts _ => stmts.attach.any (fun x => containsAssignmentOrImperativeCall model x.val)
+  | .StaticCall _ args => args.attach.any (fun x => containsAssignment x.val)
+  | .PrimitiveOp _ args => args.attach.any (fun x => containsAssignment x.val)
+  | .Block stmts _ => stmts.attach.any (fun x => containsAssignment x.val)
   | .IfThenElse cond th el =>
-      containsAssignmentOrImperativeCall model cond ||
-      containsAssignmentOrImperativeCall model th ||
-      match el with | some e => containsAssignmentOrImperativeCall model e | none => false
+      containsAssignment cond || containsAssignment th ||
+      match el with | some e => containsAssignment e | none => false
   | _ => false
   termination_by expr
   decreasing_by
     all_goals ((try cases x); simp_all; try term_by_mem)
 
-/-- Check if an expression contains any nondeterministic holes (recursively). -/
-private def containsNondetHole (expr : StmtExprMd) : Bool :=
+/-- Check if an expression contains any non-functional procedure calls (recursively). -/
+def containsImperativeCall (model : SemanticModel) (expr : StmtExprMd) : Bool :=
   match expr with
   | AstNode.mk val _ =>
   match val with
-  | .Hole false _ => true
-  | .PrimitiveOp _ args => args.attach.any (fun x => containsNondetHole x.val)
-  | .StaticCall _ args => args.attach.any (fun x => containsNondetHole x.val)
-  | .Block stmts _ => stmts.attach.any (fun x => containsNondetHole x.val)
+  | .StaticCall name args =>
+    (match model.get name with
+    | .staticProcedure proc => !proc.isFunctional
+    | _ => false) ||
+      args.attach.any (fun x => containsImperativeCall model x.val)
+  | .PrimitiveOp _ args => args.attach.any (fun x => containsImperativeCall model x.val)
+  | .Block stmts _ => stmts.attach.any (fun x => containsImperativeCall model x.val)
   | .IfThenElse cond th el =>
-      containsNondetHole cond || containsNondetHole th ||
-      match el with | some e => containsNondetHole e | none => false
+      containsImperativeCall model cond ||
+      containsImperativeCall model th ||
+      match el with | some e => containsImperativeCall model e | none => false
   | _ => false
   termination_by expr
   decreasing_by
     all_goals ((try cases x); simp_all; try term_by_mem)
 
+/-- Check if an expression contains any assignments or non-functional procedure calls (recursively). -/
+def containsAssignmentOrImperativeCall (model : SemanticModel) (expr : StmtExprMd) : Bool :=
+  containsAssignment expr || containsImperativeCall model expr
+
 /--
 Shared logic for lifting an assignment in expression position:
 prepends the assignment, creates before-snapshots for all targets,
@@ -274,12 +277,22 @@ def transformExpr (expr : StmtExprMd) : LiftM StmtExprMd := do
     if model.isFunction callee then
       return seqCall
     else
-      -- Imperative call in expression position: lift it like an assignment
+      -- Imperative call in expression position: lift to an assignment.
+      -- Only valid for single-output procedures (or unresolved ones where we
+      -- fall back to a single target). Multi-output procedures in expression
+      -- position are a bug in the upstream translation — Resolution should
+      -- emit a diagnostic for that case.
+      let outputs := match model.get callee with
+        | .staticProcedure proc => proc.outputs
+        | .instanceProcedure _ proc => proc.outputs
+        | _ => []
       let callResultVar ← freshCondVar
-      let callResultType ← computeType expr
+      let callResultType ← match outputs with
+        | [single] => pure single.type
+        | _ => computeType expr
       let liftedCall := [
-        ⟨ (.Var (.Declare ⟨callResultVar, callResultType⟩)), source ⟩,
-        ⟨.Assign [⟨ .Local callResultVar, source⟩] seqCall, source⟩
+        ⟨.Var (.Declare ⟨callResultVar, callResultType⟩), source⟩,
+        ⟨.Assign [⟨.Local callResultVar, source⟩] seqCall, source⟩
       ]
       modify fun s => { s with prependedStmts := s.prependedStmts ++ liftedCall}
       return bare (.Var (.Local callResultVar))
@@ -360,8 +373,8 @@ def transformStmt (stmt : StmtExprMd) : LiftM (List StmtExprMd) := do
   match val with
   | .Assert cond =>
       -- Do not transform assert conditions with assignments — they must be rejected.
-      -- But nondeterministic holes need to be lifted.
-      if containsNondetHole cond.condition && !containsAssignmentOrImperativeCall (← get).model cond.condition then
+      -- But nondeterministic holes and imperative calls need to be lifted.
+      if !containsAssignment cond.condition then
         let seqCond ← transformExpr cond.condition
         let prepends ← takePrepends
         modify fun s => { s with subst := [] }
@@ -370,7 +383,9 @@ def transformStmt (stmt : StmtExprMd) : LiftM (List StmtExprMd) := do
         return [stmt]
 
   | .Assume cond =>
-      if containsNondetHole cond && !containsAssignmentOrImperativeCall (← get).model cond then
+      -- Do not transform assume conditions with assignments — they must be rejected.
+      -- But nondeterministic holes and imperative calls need to be lifted.
+      if !containsAssignment cond then
         let seqCond ← transformExpr cond
         let prepends ← takePrepends
         modify fun s => { s with subst := [] }
diff --git a/Strata/Languages/Laurel/RemoveFunctionAssumptions.lean b/Strata/Languages/Laurel/RemoveFunctionAssumptions.lean
new file mode 100644
index 0000000000..b5f3ba4e3f
--- /dev/null
+++ b/Strata/Languages/Laurel/RemoveFunctionAssumptions.lean
@@ -0,0 +1,53 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+
+public import Strata.Languages.Laurel.MapStmtExpr
+
+/-!
+## Remove Function Assumptions (Laurel → Laurel)
+
+Removes `assume` statements from the bodies of functional procedures.
+Functions (procedures with `isFunctional = true`) should not contain
+assumptions since they are pure and their bodies are inlined at call sites.
+Assumptions left over from the contract pass would incorrectly constrain
+the function's evaluation context.
+-/
+
+namespace Strata.Laurel
+
+public section
+
+/-- Remove all `Assume` nodes from a statement/expression tree. -/
+private def removeAssumes (expr : StmtExprMd) : StmtExprMd :=
+  mapStmtExpr (fun e =>
+    match e.val with
+    | .Block stmts label =>
+      let filtered := stmts.filter fun s =>
+        match s.val with
+        | .Assume _ => false
+        | _ => true
+      if filtered.length == stmts.length then e
+      else ⟨.Block filtered label, e.source⟩
+    | _ => e) expr
+
+/-- Remove assumptions from the body of a single functional procedure. -/
+private def removeFunctionAssumptionsProc (proc : Procedure) : Procedure :=
+  if !proc.isFunctional then proc
+  else
+    match proc.body with
+    | .Transparent body =>
+      { proc with body := .Transparent (removeAssumes body) }
+    | .Opaque posts (some impl) mods =>
+      { proc with body := .Opaque posts (some (removeAssumes impl)) mods }
+    | _ => proc
+
+/-- Remove assumptions from all functional procedures in a program. -/
+def removeFunctionAssumptions (program : Program) : Program :=
+  { program with staticProcedures := program.staticProcedures.map removeFunctionAssumptionsProc }
+
+end -- public section
+end Strata.Laurel
diff --git a/Strata/Languages/Laurel/Resolution.lean b/Strata/Languages/Laurel/Resolution.lean
index 16bcf1333f..ee5d0afa44 100644
--- a/Strata/Languages/Laurel/Resolution.lean
+++ b/Strata/Languages/Laurel/Resolution.lean
@@ -223,7 +223,6 @@ private def freshId : ResolveM Nat := do
   set { s with nextId := id + 1 }
   return id
 
-
 /-- Like `defineName`, but reports a diagnostic if the name already exists in the current scope.
     Inserts an `.unresolved` node so subsequent references still resolve without cascading errors. -/
 def defineNameCheckDup (iden : Identifier) (node : ResolvedNode) (overrideResolutionName: Option String := none) : ResolveM Identifier := do
@@ -540,11 +539,16 @@ def resolveProcedure (proc : Procedure) : ResolveM Procedure := do
       let diag := diagnosticFromSource proc.name.source
         s!"transparent procedures are not yet supported. Add 'opaque' to make the procedure opaque"
       modify fun s => { s with errors := s.errors.push diag }
+    if proc.isFunctional && body'.hasPostconditions then
+      let diag := diagnosticFromSource proc.name.source
+        s!"functions with postconditions are not yet supported"
+      modify fun s => { s with errors := s.errors.push diag }
     let invokeOn' ← proc.invokeOn.mapM resolveStmtExpr
     return { name := procName', inputs := inputs', outputs := outputs',
              isFunctional := proc.isFunctional,
              preconditions := pres', decreases := dec',
              invokeOn := invokeOn',
+             axioms := proc.axioms,
              body := body' }
 
 /-- Resolve a field: define its name under the qualified key (OwnerType.fieldName) and resolve its type. -/
@@ -573,12 +577,17 @@ def resolveInstanceProcedure (typeName : Identifier) (proc : Procedure) : Resolv
       let diag := diagnosticFromSource proc.name.source
         s!"transparent procedures are not yet supported. Add 'opaque' to make the procedure opaque"
       modify fun s => { s with errors := s.errors.push diag }
+    if proc.isFunctional && body'.hasPostconditions then
+      let diag := diagnosticFromSource proc.name.source
+        s!"functions with postconditions are not yet supported"
+      modify fun s => { s with errors := s.errors.push diag }
     let invokeOn' ← proc.invokeOn.mapM resolveStmtExpr
     modify fun s => { s with instanceTypeName := savedInstType }
     return { name := procName', inputs := inputs', outputs := outputs',
              isFunctional := proc.isFunctional,
              preconditions := pres', decreases := dec',
              invokeOn := invokeOn',
+             axioms := proc.axioms,
              body := body' }
 
 /-- Resolve a type definition. -/
diff --git a/StrataTest/Languages/Laurel/AbstractToConcreteTreeTranslatorTest.lean b/StrataTest/Languages/Laurel/AbstractToConcreteTreeTranslatorTest.lean
index 701405b362..5134de4f39 100644
--- a/StrataTest/Languages/Laurel/AbstractToConcreteTreeTranslatorTest.lean
+++ b/StrataTest/Languages/Laurel/AbstractToConcreteTreeTranslatorTest.lean
@@ -58,21 +58,30 @@ private def roundtrip (input : String) : IO String := do
 
 /--
 info: procedure foo()
-{ assert true; assert false };
+  opaque
+{
+  assert true;
+  assert false
+};
 -/
 #guard_msgs in
-#eval do IO.println (← roundtrip r"procedure foo() { assert true; assert false };")
+#eval do IO.println (← roundtrip r"procedure foo() opaque { assert true; assert false };")
 
 /--
 info: procedure add(x: int, y: int): int
-{ x + y };
+  opaque
+{
+  x + y
+};
 -/
 #guard_msgs in
-#eval do IO.println (← roundtrip r"procedure add(x: int, y: int): int { x + y };")
+#eval do IO.println (← roundtrip r"procedure add(x: int, y: int): int opaque { x + y };")
 
 /--
 info: function aFunction(x: int): int
-{ x };
+{
+  x
+};
 -/
 #guard_msgs in
 #eval do IO.println (← roundtrip r"function aFunction(x: int): int { x };")
@@ -90,17 +99,22 @@ composite Point {
 
 /--
 info: procedure test(x: int): int
-{ if x > 0 then x else 0 - x };
+  opaque
+{
+  if x > 0 then x else 0 - x
+};
 -/
 #guard_msgs in
-#eval do IO.println (← roundtrip r"procedure test(x: int): int { if x > 0 then x else 0 - x };")
+#eval do IO.println (← roundtrip r"procedure test(x: int): int opaque { if x > 0 then x else 0 - x };")
 
 /--
 info: procedure divide(x: int, y: int): int
   requires y != 0
   opaque
   ensures result >= 0
-{ x / y };
+{
+  x / y
+};
 -/
 #guard_msgs in
 #eval do IO.println (← roundtrip r"
@@ -113,11 +127,15 @@ procedure divide(x: int, y: int): int
 
 /--
 info: procedure test()
-{ assert forall(x: int) => x == x; assert exists(y: int) => y > 0 };
+  opaque
+{
+  assert forall(x: int) => x == x;
+  assert exists(y: int) => y > 0
+};
 -/
 #guard_msgs in
 #eval do IO.println (← roundtrip r"
-procedure test() {
+procedure test() opaque {
     assert forall(x: int) => x == x;
     assert exists(y: int) => y > 0
 };
@@ -127,7 +145,12 @@ procedure test() {
 info: composite Point { var x: int var y: int }
 
 procedure test(): int
-{ var p: Point := new Point; p#x := 5; p#x };
+  opaque
+{
+  var p: Point := new Point;
+  p#x := 5;
+  p#x
+};
 -/
 #guard_msgs in
 #eval do IO.println (← roundtrip r"
@@ -135,7 +158,7 @@ composite Point {
   var x: int
   var y: int
 }
-procedure test(): int {
+procedure test(): int opaque {
     var p: Point := new Point;
     p#x := 5;
     p#x
@@ -160,25 +183,34 @@ info: composite Animal { }
 composite Dog extends Animal { }
 
 procedure test(a: Animal): bool
-{ a is Dog };
+  opaque
+{
+  a is Dog
+};
 -/
 #guard_msgs in
 #eval do IO.println (← roundtrip r"
 composite Animal {}
 composite Dog extends Animal {}
-procedure test(a: Animal): bool { a is Dog };
+procedure test(a: Animal): bool opaque { a is Dog };
 ")
 
 -- Additional coverage: while loops
 
 /--
 info: procedure test()
-{ var x: int := 0; while(x < 10)
-  invariant x >= 0 { x := x + 1 } };
+  opaque
+{
+  var x: int := 0;
+  while(x < 10)
+    invariant x >= 0 {
+    x := x + 1
+  }
+};
 -/
 #guard_msgs in
 #eval do IO.println (← roundtrip r"
-procedure test() {
+procedure test() opaque {
     var x: int := 0;
     while(x < 10)
       invariant x >= 0
@@ -203,7 +235,10 @@ procedure modify(c: Container)
   opaque
   ensures true
   modifies c
-{ c#value := c#value + 1; true };
+{
+  c#value := c#value + 1;
+  true
+};
 -/
 #guard_msgs in
 #eval do IO.println (← roundtrip r"
@@ -219,9 +254,12 @@ procedure modify(c: Container)
 
 /--
 info: procedure test(): int
-{ <??> };
+  opaque
+{
+  <??>
+};
 -/
 #guard_msgs in
-#eval do IO.println (← roundtrip r"procedure test(): int { <??> };")
+#eval do IO.println (← roundtrip r"procedure test(): int opaque { <??> };")
 
 end Strata.Laurel
diff --git a/StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean b/StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean
index 86ce51e683..8a293059d5 100644
--- a/StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean
+++ b/StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean
@@ -44,15 +44,26 @@ def parseLaurelAndElim (input : String) : IO Program := do
 
 /--
 info: function nat$constraint(x: int): bool
-{ x >= 0 };
+{
+  x >= 0
+};
 procedure test(n: int)
   returns (r: int)
   requires nat$constraint(n)
   opaque
   ensures nat$constraint(r)
-{ assert r >= 0; var y: int := n; assert nat$constraint(y); return y };
+{
+  assert r >= 0;
+  var y: int := n;
+  assert nat$constraint(y);
+  return y
+};
 procedure $witness_nat()
-{ var $witness: int := 0; assert nat$constraint($witness) };
+  opaque
+{
+  var $witness: int := 0;
+  assert nat$constraint($witness)
+};
 -/
 #guard_msgs in
 #eval! do
@@ -76,11 +87,26 @@ procedure test(b: bool) {
 
 /--
 info: function pos$constraint(v: int): bool
-{ v > 0 };
+{
+  v > 0
+};
 procedure test(b: bool)
-{ if b then { var x: int := 1; assert pos$constraint(x) }; { var x: int := -5; x := -10 } };
+{
+  if b then {
+    var x: int := 1;
+    assert pos$constraint(x)
+  };
+  {
+    var x: int := -5;
+    x := -10
+  }
+};
 procedure $witness_pos()
-{ var $witness: int := 1; assert pos$constraint($witness) };
+  opaque
+{
+  var $witness: int := 1;
+  assert pos$constraint($witness)
+};
 -/
 #guard_msgs in
 #eval! do
@@ -92,7 +118,7 @@ procedure $witness_pos()
 -- The variable has no known value, only the type constraint is assumed.
 def uninitProgram : String := r"
 constrained posint = x: int where x > 0 witness 1
-procedure f() {
+procedure f() opaque {
   var x: posint;
   assert x == 1
 };
@@ -100,11 +126,22 @@ procedure f() {
 
 /--
 info: function posint$constraint(x: int): bool
-{ x > 0 };
+{
+  x > 0
+};
 procedure f()
-{ var x: int; assume posint$constraint(x); assert x == 1 };
+  opaque
+{
+  var x: int;
+  assume posint$constraint(x);
+  assert x == 1
+};
 procedure $witness_posint()
-{ var $witness: int := 1; assert posint$constraint($witness) };
+  opaque
+{
+  var $witness: int := 1;
+  assert posint$constraint($witness)
+};
 -/
 #guard_msgs in
 #eval! do
diff --git a/StrataTest/Languages/Laurel/DivisionByZeroCheckTest.lean b/StrataTest/Languages/Laurel/DivisionByZeroCheckTest.lean
index 40e8a9112d..7623f946c8 100644
--- a/StrataTest/Languages/Laurel/DivisionByZeroCheckTest.lean
+++ b/StrataTest/Languages/Laurel/DivisionByZeroCheckTest.lean
@@ -37,8 +37,9 @@ procedure unsafeDivision(x: int)
 // Error ranges are too wide because Core does not use expression locations
 };
 
-function pureDiv(x: int, y: int): int
+procedure pureDiv(x: int, y: int): int
   requires y != 0
+  opaque
 {
   x / y
 };
@@ -46,20 +47,21 @@ function pureDiv(x: int, y: int): int
 procedure callPureDivSafe()
   opaque
 {
-  var z: int := pureDiv(10, 2);
-  assert z == 5
+  var z: int := pureDiv(10, 2)
+  // TODO remove assumes from functions, so pureDiv can be a function
+  // assert z == 5
 };
 
 procedure callPureDivUnsafe(x: int)
   opaque
 {
   var z: int := pureDiv(10, x)
-//^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
+//^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: precondition does not hold
 // Error ranges are too wide because Core does not use expression locations
 };
 "
 
-#guard_msgs(drop info, error) in
-#eval testInputWithOffset "DivByZeroE2E" e2eProgram 22 processLaurelFile
+#guard_msgs (drop info, error) in
+#eval testInputWithOffset "DivByZeroE2E" e2eProgram 20 processLaurelFile
 
 end Laurel
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypes.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypes.lean
index 80d21eb4d6..c7ae8b9782 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypes.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T10_ConstrainedTypes.lean
@@ -32,7 +32,7 @@ procedure outputValid(): nat
 
 // Output constraint — invalid return fails
 procedure outputInvalid(): nat
-//                         ^^^ error: assertion does not hold
+//                         ^^^ error: postcondition does not hold
   opaque
 {
   return -1
@@ -196,7 +196,7 @@ procedure captureTest(y: haslarger)
 };
 "
 
-#guard_msgs(drop info, error) in
+#guard_msgs (drop info, error) in
 #eval testInputWithOffset "ConstrainedTypes" program 14 processLaurelFile
 
 end Laurel
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T15_ShortCircuit.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T15_ShortCircuit.lean
index 2e5b46a8ab..019eaf4ba9 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T15_ShortCircuit.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T15_ShortCircuit.lean
@@ -14,7 +14,7 @@ namespace Laurel
 
 def shortCircuitProgram := r"
 function mustNotCallFunc(x: int): int
-  requires false
+   requires false
 { x };
 
 procedure mustNotCallProc(): int
@@ -91,7 +91,7 @@ procedure testImpliesProc()
 };
 "
 
-#guard_msgs(drop info) in
+#guard_msgs (drop info) in
 #eval testInputWithOffset "ShortCircuit" shortCircuitProgram 15 processLaurelFile
 
 end Laurel
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_InvokeOn.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_InvokeOn.lean
index a5eb37f347..0f6eb2ae09 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_InvokeOn.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_InvokeOn.lean
@@ -17,8 +17,10 @@ function P(x: int): bool;
 function Q(x: int): bool;
 
 function assertP(x: int): int requires P(x);
-function needsPAndQsInvoke1(): int {
+
+procedure needsPAndQsInvoke1(): int opaque {
   assertP(3)
+//^^^^^^^^^^ error: precondition does not hold
 };
 
 procedure PAndQ(x: int)
@@ -26,7 +28,7 @@ procedure PAndQ(x: int)
   opaque
   ensures P(x) && Q(x);
 
-function needsPAndQsInvoke2(): int {
+procedure needsPAndQsInvoke2(): int opaque {
   assertP(3)
 };
 
@@ -69,7 +71,7 @@ procedure badPostcondition(x: int)
   invokeOn R(x)
   opaque
   ensures R(x)
-//        ^^^^ error: assertion could not be proved
+//        ^^^^ error: postcondition could not be proved
 {
 };
 
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean
index 57e5a61ddd..2b3767391c 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsError.lean
@@ -44,7 +44,6 @@ procedure impureContractIsNotLegal1(x: int)
   opaque
 {
   assert impure() == 1
-//       ^^^^^^^^ error: calls to procedures are not supported in functions or contracts
 };
 
 procedure impureContractIsNotLegal2(x: int)
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean
index 3ebe4eb4cf..5d8b9a9cee 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean
@@ -18,7 +18,6 @@ function assertAndAssumeInFunctions(a: int) returns (r: int)
   assert 2 == 3;
 //^^^^^^^^^^^^^ error: asserts are not YET supported in functions or contracts
   assume true;
-//^^^^^^^^^^^ error: assumes are not YET supported in functions or contracts
   a
 };
 
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean
index c7f1742a88..0387a6af7b 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T6_Preconditions.lean
@@ -44,7 +44,7 @@ procedure aFunctionWithPreconditionCaller()
   opaque
 {
   var x: int := aFunctionWithPrecondition(0)
-//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
+//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: precondition does not hold
 // Error ranges are too wide because Core does not use expression locations
 };
 
@@ -76,7 +76,7 @@ procedure funcMultipleRequiresCaller()
 {
   var a: int := funcMultipleRequires(1, 2);
   var b: int := funcMultipleRequires(1, -1)
-//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
+//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: precondition does not hold
 };
 "
 
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean
index 526a03dd92..1f081b0560 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean
@@ -27,13 +27,13 @@ procedure callerOfOpaqueProcedure()
   var x: int := opaqueBody(3);
   assert x > 0;
   assert x == 3
-//^^^^^^^^^^^^^ error: assertion could not be proved
+//^^^^^^^^^^^^^ error: assertion does not hold
 };
 
 procedure invalidPostcondition(x: int)
     opaque
     ensures false
-//          ^^^^^ error: assertion does not hold
+//          ^^^^^ error: postcondition does not hold
 {
 };
 "
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_PostconditionsErrors.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_PostconditionsErrors.lean
index d61c5849da..8228f5aebe 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_PostconditionsErrors.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_PostconditionsErrors.lean
@@ -16,11 +16,9 @@ def program := r"
 
 function opaqueFunction(x: int) returns (r: int)
 //       ^^^^^^^^^^^^^^ error: functions with postconditions are not yet supported
-// The above limitation is because Core does not yet support functions with postconditions
   requires x > 0
   opaque
   ensures r > 0
-// The above limitation is because functions in Core do not support postconditions
 {
   x
 };
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8b_EarlyReturnPostconditions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8b_EarlyReturnPostconditions.lean
index 964fc7dfb0..f8f4b8089b 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8b_EarlyReturnPostconditions.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8b_EarlyReturnPostconditions.lean
@@ -26,7 +26,7 @@ procedure earlyReturnCorrect(x: int) returns (r: int)
 procedure earlyReturnBuggy(x: int) returns (r: int)
   opaque
   ensures r >= 0
-//        ^^^^^^ error: assertion does not hold
+//        ^^^^^^ error: postcondition does not hold
 {
   if x < 0 then {
     return x
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8d_HeapMutatingValueReturn.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8d_HeapMutatingValueReturn.lean
index 0a8321d945..7fa1e0aba2 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8d_HeapMutatingValueReturn.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8d_HeapMutatingValueReturn.lean
@@ -29,7 +29,7 @@ procedure setAndReturn(c: Container, x: int) returns (r: int)
 procedure setAndReturnBuggy(c: Container, x: int) returns (r: int)
   opaque
   ensures r == x + 1
-//        ^^^^^^^^^^ error: assertion does not hold
+//        ^^^^^^^^^^ error: postcondition does not hold
   modifies c
 {
   c#value := x;
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean b/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean
index 7dbf35022d..e46f03ef99 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean
@@ -199,5 +199,5 @@ procedure fieldTargetInMultiAssign()
 };
 "#
 
-#guard_msgs(drop info, error) in
+#guard_msgs (drop info, error) in
 #eval testInputWithOffset "MutableFields" program 14 processLaurelFile
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T7_InstanceProcedures.lean b/StrataTest/Languages/Laurel/Examples/Objects/T7_InstanceProcedures.lean
index ec05fcfd3d..189295102d 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T7_InstanceProcedures.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T7_InstanceProcedures.lean
@@ -15,8 +15,8 @@ namespace Strata.Laurel
 def instanceProcedureProgram := r"
 composite Counter {
   var count: int
-  procedure increment(self: Counter)
-//          ^^^^^^^^^ error: Instance procedure 'increment' on composite type 'Counter' is not yet supported
+  procedure self_increment(self: Counter)
+//          ^^^^^^^^^^^^^^ error: Instance procedure 'self_increment' on composite type 'Counter' is not yet supported
     opaque
   {
     self#count := self#count + 1
diff --git a/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean b/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean
index f3a3acbd6f..98e1706a3f 100644
--- a/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean
+++ b/StrataTest/Languages/Laurel/LiftExpressionAssignmentsTest.lean
@@ -23,6 +23,7 @@ namespace Strata.Laurel
 
 def blockStmtLiftingProgram : String := r"
 procedure assertInBlockExpr()
+  opaque
 {
   var x: int := 0;
   var y: int := { assert x == 0; x := 1; x };
@@ -44,7 +45,17 @@ def parseLaurelAndLift (input : String) : IO Program := do
 
 /--
 info: procedure assertInBlockExpr()
-{ var x: int := 0; assert x == 0; var $x_0: int := x; x := 1; var y: int := { x }; assert y == 1 };
+  opaque
+{
+  var x: int := 0;
+  assert x == 0;
+  var $x_0: int := x;
+  x := 1;
+  var y: int := {
+    x
+  };
+  assert y == 1
+};
 -/
 #guard_msgs in
 #eval! do
diff --git a/StrataTest/Languages/Laurel/LiftHolesTest.lean b/StrataTest/Languages/Laurel/LiftHolesTest.lean
index 14d25a4416..08966a3321 100644
--- a/StrataTest/Languages/Laurel/LiftHolesTest.lean
+++ b/StrataTest/Languages/Laurel/LiftHolesTest.lean
@@ -46,11 +46,14 @@ info: function $hole_0()
   returns ($result: int)
   opaque;
 procedure test()
-{ var x: int := 1 + $hole_0() };
+  opaque
+{
+  var x: int := 1 + $hole_0()
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { var x: int := 1 + <?> };
+procedure test() opaque { var x: int := 1 + <?> };
 "
 
 -- Bare Hole as Assign Declare initializer → replaced with call (no longer preserved as havoc).
@@ -59,11 +62,14 @@ info: function $hole_0()
   returns ($result: int)
   opaque;
 procedure test()
-{ var x: int := $hole_0() };
+  opaque
+{
+  var x: int := $hole_0()
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { var x: int := <?> };
+procedure test() opaque { var x: int := <?> };
 "
 
 -- Hole in comparison arg inside assert → int (inferred from sibling literal).
@@ -72,11 +78,14 @@ info: function $hole_0()
   returns ($result: int)
   opaque;
 procedure test()
-{ assert $hole_0() > 0 };
+  opaque
+{
+  assert $hole_0() > 0
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { assert <?> > 0 };
+procedure test() opaque { assert <?> > 0 };
 "
 
 -- Hole directly as assert condition → bool.
@@ -85,11 +94,14 @@ info: function $hole_0()
   returns ($result: bool)
   opaque;
 procedure test()
-{ assert $hole_0() };
+  opaque
+{
+  assert $hole_0()
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { assert <?> };
+procedure test() opaque { assert <?> };
 "
 
 -- Hole directly as assume condition → bool.
@@ -98,11 +110,14 @@ info: function $hole_0()
   returns ($result: bool)
   opaque;
 procedure test()
-{ assume $hole_0() };
+  opaque
+{
+  assume $hole_0()
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { assume <?> };
+procedure test() opaque { assume <?> };
 "
 
 -- Hole as if-then-else condition → bool.
@@ -111,11 +126,16 @@ info: function $hole_0()
   returns ($result: bool)
   opaque;
 procedure test()
-{ if $hole_0() then { assert true } };
+  opaque
+{
+  if $hole_0() then {
+    assert true
+  }
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { if <?> then { assert true } };
+procedure test() opaque { if <?> then { assert true } };
 "
 
 -- Hole in then-branch of if-then-else inside typed local variable → int.
@@ -124,11 +144,14 @@ info: function $hole_0()
   returns ($result: int)
   opaque;
 procedure test()
-{ var x: int := if true then $hole_0() else 0 };
+  opaque
+{
+  var x: int := if true then $hole_0() else 0
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { var x: int := if true then <?> else 0 };
+procedure test() opaque { var x: int := if true then <?> else 0 };
 "
 
 -- Hole as while-loop condition → bool.
@@ -137,11 +160,16 @@ info: function $hole_0()
   returns ($result: bool)
   opaque;
 procedure test()
-{ while($hole_0()) {  } };
+  opaque
+{
+  while($hole_0()) {
+    ⏎
+  }
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { while(<?>) {} };
+procedure test() opaque { while(<?>) {} };
 "
 
 -- Hole as while-loop invariant → bool.
@@ -150,12 +178,17 @@ info: function $hole_0()
   returns ($result: bool)
   opaque;
 procedure test()
-{ while(true)
-  invariant $hole_0() {  } };
+  opaque
+{
+  while(true)
+    invariant $hole_0() {
+    ⏎
+  }
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { while(true) invariant <?> {} };
+procedure test() opaque { while(true) invariant <?> {} };
 "
 
 /-! ## Operators -/
@@ -166,11 +199,14 @@ info: function $hole_0()
   returns ($result: bool)
   opaque;
 procedure test()
-{ assert true && $hole_0() };
+  opaque
+{
+  assert true && $hole_0()
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { assert true && <?> };
+procedure test() opaque { assert true && <?> };
 "
 
 -- Hole in Neg inside typed local variable → int.
@@ -179,11 +215,14 @@ info: function $hole_0()
   returns ($result: int)
   opaque;
 procedure test()
-{ var x: int := -$hole_0() };
+  opaque
+{
+  var x: int := -$hole_0()
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { var x: int := -<?> };
+procedure test() opaque { var x: int := -<?> };
 "
 
 -- Hole in StrConcat inside typed local variable → string.
@@ -192,11 +231,14 @@ info: function $hole_0()
   returns ($result: string)
   opaque;
 procedure test()
-{ var s: string := "hello" ++ $hole_0() };
+  opaque
+{
+  var s: string := "hello" ++ $hole_0()
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint
-  "procedure test() { var s: string := \"hello\" ++ <?> };"
+  "procedure test() opaque { var s: string := \"hello\" ++ <?> };"
 
 /-! ## Multiple holes -/
 
@@ -209,11 +251,14 @@ function $hole_1()
   returns ($result: int)
   opaque;
 procedure test()
-{ var x: int := $hole_0() + $hole_1() };
+  opaque
+{
+  var x: int := $hole_0() + $hole_1()
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { var x: int := <?> + <?> };
+procedure test() opaque { var x: int := <?> + <?> };
 "
 
 -- Holes across statements: Mul arg (int) then assert condition (bool).
@@ -225,11 +270,15 @@ function $hole_1()
   returns ($result: bool)
   opaque;
 procedure test()
-{ var x: int := 2 * $hole_0(); assert $hole_1() };
+  opaque
+{
+  var x: int := 2 * $hole_0();
+  assert $hole_1()
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { var x: int := 2 * <?>; assert <?> };
+procedure test() opaque { var x: int := 2 * <?>; assert <?> };
 "
 
 /-! ## Combinations: holes in nested contexts -/
@@ -240,11 +289,16 @@ info: function $hole_0()
   returns ($result: int)
   opaque;
 procedure test()
-{ if 1 + $hole_0() > 0 then { assert true } };
+  opaque
+{
+  if 1 + $hole_0() > 0 then {
+    assert true
+  }
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { if 1 + <?> > 0 then { assert true } };
+procedure test() opaque { if 1 + <?> > 0 then { assert true } };
 "
 
 -- Hole in Implies inside while invariant → bool.
@@ -253,12 +307,18 @@ info: function $hole_0()
   returns ($result: bool)
   opaque;
 procedure test()
-{ var p: bool; while(true)
-  invariant p ==> $hole_0() {  } };
+  opaque
+{
+  var p: bool;
+  while(true)
+    invariant p ==> $hole_0() {
+    ⏎
+  }
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { var p: bool; while(true) invariant p ==> <?> {} };
+procedure test() opaque { var p: bool; while(true) invariant p ==> <?> {} };
 "
 
 -- Hole in Mul inside typed local variable with real type → real.
@@ -267,11 +327,14 @@ info: function $hole_0()
   returns ($result: real)
   opaque;
 procedure test()
-{ var r: real := 3.14 * $hole_0() };
+  opaque
+{
+  var r: real := 3.14 * $hole_0()
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { var r: real := 3.14 * <?> };
+procedure test() opaque { var r: real := 3.14 * <?> };
 "
 
 /-! ## Call argument and return type inference -/
@@ -282,11 +345,14 @@ info: function $hole_0(n: int)
   returns ($result: int)
   opaque;
 procedure test(n: int)
-{ assert n > $hole_0(n) };
+  opaque
+{
+  assert n > $hole_0(n)
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test(n: int) { assert n > <?> };
+procedure test(n: int) opaque { assert n > <?> };
 "
 
 /-! ## Holes in functions -/
@@ -297,11 +363,14 @@ info: function $hole_0(x: int)
   returns ($result: int)
   opaque;
 function test(x: int): int
-{ $hole_0(x) };
+  opaque
+{
+  $hole_0(x)
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-function test(x: int): int { <?> };
+function test(x: int): int opaque { <?> };
 "
 
 /-! ## Nondeterministic holes (<??>) -/
@@ -309,11 +378,14 @@ function test(x: int): int { <?> };
 -- Nondet hole in procedure → preserved after eliminateHoles (lifted by liftExpressionAssignments).
 /--
 info: procedure test()
-{ assert <??> };
+  opaque
+{
+  assert <??>
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { assert <??> };
+procedure test() opaque { assert <??> };
 "
 
 -- Mixed: det hole eliminated, nondet hole preserved.
@@ -322,11 +394,15 @@ info: function $hole_0()
   returns ($result: int)
   opaque;
 procedure test()
-{ var x: int := $hole_0(); assert <??> };
+  opaque
+{
+  var x: int := $hole_0();
+  assert <??>
+};
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { var x: int := <?>; assert <??> };
+procedure test() opaque { var x: int := <?>; assert <??> };
 "
 
 -- Nondet hole in function → should be rejected (not tested here since
diff --git a/StrataTest/Languages/Laurel/LiftImperativeCallsInAssertTest.lean b/StrataTest/Languages/Laurel/LiftImperativeCallsInAssertTest.lean
new file mode 100644
index 0000000000..f44067848c
--- /dev/null
+++ b/StrataTest/Languages/Laurel/LiftImperativeCallsInAssertTest.lean
@@ -0,0 +1,143 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+/-
+Tests that the expression lifter correctly hoists imperative procedure calls
+out of assert and assume conditions, while leaving assignments untouched
+(so they are rejected downstream).
+-/
+
+import Strata.DDM.Elab
+import Strata.DDM.BuiltinDialects.Init
+import Strata.Languages.Laurel.Grammar.LaurelGrammar
+import Strata.Languages.Laurel.Grammar.ConcreteToAbstractTreeTranslator
+import Strata.Languages.Laurel.LaurelToCoreTranslator
+
+open Strata
+open Strata.Elab (parseStrataProgramFromDialect)
+
+namespace Strata.Laurel
+
+private def parseLaurelAndLift (input : String) : IO Program := do
+  let inputCtx := Strata.Parser.stringInputContext "test" input
+  let dialects := Strata.Elab.LoadedDialects.ofDialects! #[initDialect, Laurel]
+  let strataProgram ← parseStrataProgramFromDialect dialects Laurel.name inputCtx
+  let uri := Strata.Uri.file "test"
+  match Laurel.TransM.run uri (Laurel.parseProgram strataProgram) with
+  | .error e => throw (IO.userError s!"Translation errors: {e}")
+  | .ok program =>
+    let result := resolve program
+    let (program, model) := (result.program, result.model)
+    pure (liftExpressionAssignments model program)
+
+private def printLifted (input : String) : IO Unit := do
+  let program ← parseLaurelAndLift input
+  for proc in program.staticProcedures do
+    IO.println (toString (Std.Format.pretty (Std.ToFormat.format proc)))
+
+/-! ## Imperative calls in assert are lifted -/
+
+/--
+info: procedure impure(): int
+{
+  var x: int := 0;
+  x := x + 1;
+  x
+};
+procedure test()
+{
+  var $c_0: int;
+  $c_0 := impure();
+  assert $c_0 == 1
+};
+-/
+#guard_msgs in
+#eval! printLifted r"
+procedure impure(): int {
+  var x: int := 0;
+  x := x + 1;
+  x
+};
+procedure test() {
+  assert impure() == 1
+};
+"
+
+/-! ## Assignments in assert are NOT lifted (rejected downstream) -/
+
+/--
+info: procedure test()
+{
+  var x: int := 0;
+  assert (x := 2) == 2
+};
+-/
+#guard_msgs in
+#eval! printLifted r"
+procedure test() {
+  var x: int := 0;
+  assert (x := 2) == 2
+};
+"
+
+/-! ## Imperative calls in assume are lifted -/
+
+/--
+info: procedure impure(): int
+{
+  var x: int := 0;
+  x := x + 1;
+  x
+};
+procedure test()
+{
+  var $c_0: int;
+  $c_0 := impure();
+  assume $c_0 == 1
+};
+-/
+#guard_msgs in
+#eval! printLifted r"
+procedure impure(): int {
+  var x: int := 0;
+  x := x + 1;
+  x
+};
+procedure test() {
+  assume impure() == 1
+};
+"
+
+/-! ## Multi-output calls in expression position produce a single (broken) target.
+    This is intentional — multi-output calls should not appear in expression position.
+    Resolution should emit a diagnostic for this case. -/
+
+/--
+info: procedure multi_out(x: int)
+  returns (r: int, extra: int)
+{
+  r := x + 1;
+  extra := x + 2
+};
+procedure test()
+{
+  var $c_0: BUG_MultiValuedExpr;
+  $c_0 := multi_out(5);
+  assert $c_0 == 6
+};
+-/
+#guard_msgs in
+#eval! printLifted r"
+procedure multi_out(x: int) returns (r: int, extra: int) {
+  r := x + 1;
+  extra := x + 2
+};
+procedure test() {
+  assert multi_out(5) == 6
+};
+"
+
+end Laurel
diff --git a/StrataTest/Languages/Laurel/TestExamples.lean b/StrataTest/Languages/Laurel/TestExamples.lean
index 5affbb2813..781cc366fd 100644
--- a/StrataTest/Languages/Laurel/TestExamples.lean
+++ b/StrataTest/Languages/Laurel/TestExamples.lean
@@ -36,4 +36,14 @@ def processLaurelFileWithOptions (options : LaurelVerifyOptions) (input : InputC
 def processLaurelFile (input : InputContext) : IO (Array Diagnostic) :=
   processLaurelFileWithOptions default input
 
+/-- Project-root-relative path to the `Build/` directory for intermediate files.
+    Resolved from the current working directory so it works on any machine. -/
+def buildDir : IO String := do
+  let cwd ← IO.currentDir
+  return s!"{cwd}/Build/"
+
+def processLaurelFileKeepIntermediates (input : InputContext) : IO (Array Diagnostic) := do
+  let dir ← buildDir
+  processLaurelFileWithOptions { translateOptions := { keepAllFilesPrefix := dir}} input
+
 end Laurel
diff --git a/StrataTest/Languages/Python/PySpecArgTypeTest.lean b/StrataTest/Languages/Python/PySpecArgTypeTest.lean
index d921aaab9c..ff30813ef9 100644
--- a/StrataTest/Languages/Python/PySpecArgTypeTest.lean
+++ b/StrataTest/Languages/Python/PySpecArgTypeTest.lean
@@ -97,7 +97,12 @@ preconditions redundant. -/
 info: procedure typed_func(x: Any, y: Any): Any
   opaque
   modifies *
-{ result := <??>; assert Any..isfrom_int(x); assert Any..isfrom_str(y); assume Any..isfrom_float(result) };
+{
+  result := <??>;
+  assert Any..isfrom_int(x);
+  assert Any..isfrom_str(y);
+  assume Any..isfrom_float(result)
+};
 -/
 #guard_msgs in
 #eval! do
diff --git a/StrataTest/Languages/Python/expected_laurel/test_any_dict.expected b/StrataTest/Languages/Python/expected_laurel/test_any_dict.expected
index 56fc49687d..ff85154acb 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_any_dict.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_any_dict.expected
@@ -1,4 +1,3 @@
-test_any_dict.py(5, 4): ✅ pass - assert_assert(71)_calls_Any_get_0
 test_any_dict.py(5, 4): ✅ pass - Any holds dict
-DETAIL: 2 passed, 0 failed, 0 inconclusive
+DETAIL: 1 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_any_list.expected b/StrataTest/Languages/Python/expected_laurel/test_any_list.expected
index af813bcfcd..eab3cafe96 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_any_list.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_any_list.expected
@@ -1,4 +1,3 @@
-test_any_list.py(5, 4): ✅ pass - assert_assert(72)_calls_Any_get_0
 test_any_list.py(5, 4): ✅ pass - Any holds list
-DETAIL: 2 passed, 0 failed, 0 inconclusive
+DETAIL: 1 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_arithmetic.expected b/StrataTest/Languages/Python/expected_laurel/test_arithmetic.expected
index 5d2aac95de..bc4993a6ac 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_arithmetic.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_arithmetic.expected
@@ -14,20 +14,17 @@ test_arithmetic.py(16, 4): ✅ pass - addition implemented incorrectly
 test_arithmetic.py(19, 16): ✅ pass - Check PSub exception
 test_arithmetic.py(19, 4): ✅ pass - assert(436)
 test_arithmetic.py(20, 4): ✅ pass - subtraction implemented incorrectly
-test_arithmetic.py(23, 16): ✅ pass - assert_assert(556)_calls_PFloorDiv_0
 test_arithmetic.py(23, 16): ✅ pass - Check PFloorDiv exception
-test_arithmetic.py(23, 4): ✅ pass - set_quot_calls_PFloorDiv_0
+test_arithmetic.py(23, 4): ✅ pass - precondition
 test_arithmetic.py(23, 4): ✅ pass - assert(544)
 test_arithmetic.py(24, 4): ✅ pass - floor division implemented incorrectly
-test_arithmetic.py(27, 15): ✅ pass - assert_assert(652)_calls_PMod_0
 test_arithmetic.py(27, 15): ✅ pass - Check PMod exception
-test_arithmetic.py(27, 4): ✅ pass - set_rem_calls_PMod_0
+test_arithmetic.py(27, 4): ✅ pass - precondition
 test_arithmetic.py(27, 4): ✅ pass - assert(641)
 test_arithmetic.py(28, 4): ✅ pass - mod implemented incorrectly
-test_arithmetic.py(31, 20): ✅ pass - assert_assert(749)_calls_PMod_0
 test_arithmetic.py(31, 20): ✅ pass - Check PMod exception
-test_arithmetic.py(31, 4): ✅ pass - set_neg_rem1_calls_PMod_0
+test_arithmetic.py(31, 4): ✅ pass - precondition
 test_arithmetic.py(31, 4): ✅ pass - assert(733)
 test_arithmetic.py(32, 4): ✅ pass - negative mod should follow Python floored semantics
-DETAIL: 31 passed, 0 failed, 0 inconclusive
+DETAIL: 28 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_augadd_list.expected b/StrataTest/Languages/Python/expected_laurel/test_augadd_list.expected
index b9ee61e68b..f07cc66721 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_augadd_list.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_augadd_list.expected
@@ -1,7 +1,5 @@
 test_augadd_list.py(3, 4): ✅ pass - Check PAdd exception
-test_augadd_list.py(4, 4): ✅ pass - assert_assert(61)_calls_Any_get_0
 test_augadd_list.py(4, 4): ✅ pass - augmented add list
-test_augadd_list.py(5, 4): ✅ pass - assert_assert(105)_calls_Any_get_0
 test_augadd_list.py(5, 4): ✅ pass - augmented add list last
-DETAIL: 5 passed, 0 failed, 0 inconclusive
+DETAIL: 3 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_augfloordiv.expected b/StrataTest/Languages/Python/expected_laurel/test_augfloordiv.expected
index a5f20ce182..bd3fdc807e 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_augfloordiv.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_augfloordiv.expected
@@ -1,7 +1,6 @@
 test_augfloordiv.py(2, 4): ✅ pass - assert(28)
-test_augfloordiv.py(3, 4): ✅ pass - assert_assert(44)_calls_PFloorDiv_0
 test_augfloordiv.py(3, 4): ✅ pass - Check PFloorDiv exception
-test_augfloordiv.py(3, 4): ✅ pass - set_x_calls_PFloorDiv_0
+test_augfloordiv.py(3, 4): ✅ pass - precondition
 test_augfloordiv.py(4, 4): ✅ pass - augmented floordiv
-DETAIL: 5 passed, 0 failed, 0 inconclusive
+DETAIL: 4 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_augmented_assign.expected b/StrataTest/Languages/Python/expected_laurel/test_augmented_assign.expected
index ad80803bf1..32755f38b8 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_augmented_assign.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_augmented_assign.expected
@@ -4,10 +4,7 @@ test_augmented_assign.py(6, 4): ✅ pass - Check PSub exception
 test_augmented_assign.py(7, 4): ✅ pass - 8 - 2 == 6
 test_augmented_assign.py(8, 4): ✅ pass - Check PMul exception
 test_augmented_assign.py(9, 4): ✅ pass - 6 * 2 == 12
-test_augmented_assign.py(11, 4): ✅ pass - assert_assert(219)_calls_Any_get_0
 test_augmented_assign.py(11, 4): ✅ pass - Check Any_sets! exception
-test_augmented_assign.py(11, 4): ✅ pass - set_l_calls_Any_get_0
-test_augmented_assign.py(12, 4): ✅ pass - assert_assert(233)_calls_Any_get_0
 test_augmented_assign.py(12, 4): ✅ pass - list element modified
-DETAIL: 11 passed, 0 failed, 0 inconclusive
+DETAIL: 8 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_augmod.expected b/StrataTest/Languages/Python/expected_laurel/test_augmod.expected
index c785c8575b..610fb8eb52 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_augmod.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_augmod.expected
@@ -1,7 +1,6 @@
 test_augmod.py(2, 4): ✅ pass - assert(23)
-test_augmod.py(3, 4): ✅ pass - assert_assert(39)_calls_PMod_0
 test_augmod.py(3, 4): ✅ pass - Check PMod exception
-test_augmod.py(3, 4): ✅ pass - set_x_calls_PMod_0
+test_augmod.py(3, 4): ✅ pass - precondition
 test_augmod.py(4, 4): ✅ pass - augmented mod
-DETAIL: 5 passed, 0 failed, 0 inconclusive
+DETAIL: 4 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_bool_shortcircuit_and.expected b/StrataTest/Languages/Python/expected_laurel/test_bool_shortcircuit_and.expected
new file mode 100644
index 0000000000..9e1ce10b80
--- /dev/null
+++ b/StrataTest/Languages/Python/expected_laurel/test_bool_shortcircuit_and.expected
@@ -0,0 +1,7 @@
+test_bool_shortcircuit_and.py(2, 4): ✅ pass - assert(38)
+test_bool_shortcircuit_and.py(3, 14): ✅ pass - Check PAnd exception
+test_bool_shortcircuit_and.py(3, 4): ✅ pass - assert(53)
+test_bool_shortcircuit_and.py(4, 11): ✅ pass - Check PNot exception
+test_bool_shortcircuit_and.py(4, 4): ✅ pass - short circuit and
+DETAIL: 5 passed, 0 failed, 0 inconclusive
+RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_bool_shortcircuit_or.expected b/StrataTest/Languages/Python/expected_laurel/test_bool_shortcircuit_or.expected
new file mode 100644
index 0000000000..6478e617c4
--- /dev/null
+++ b/StrataTest/Languages/Python/expected_laurel/test_bool_shortcircuit_or.expected
@@ -0,0 +1,6 @@
+test_bool_shortcircuit_or.py(2, 4): ✅ pass - assert(37)
+test_bool_shortcircuit_or.py(3, 14): ✅ pass - Check POr exception
+test_bool_shortcircuit_or.py(3, 4): ✅ pass - assert(52)
+test_bool_shortcircuit_or.py(4, 4): ✅ pass - short circuit or
+DETAIL: 4 passed, 0 failed, 0 inconclusive
+RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_break_continue.expected b/StrataTest/Languages/Python/expected_laurel/test_break_continue.expected
index 1cb5222c41..346c4a6d03 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_break_continue.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_break_continue.expected
@@ -4,9 +4,7 @@ test_break_continue.py(1, 26): ✅ pass - (test_while_break ensures) Return type
 test_break_continue.py(7, 4): ✅ pass - assert(129)
 test_break_continue.py(8, 10): ✅ pass - Check PNot exception
 test_break_continue.py(6, 29): ✅ pass - (test_while_continue ensures) Return type constraint
-test_break_continue.py(14, 4): ✅ pass - assume_assume(267)_calls_PIn_0
 test_break_continue.py(12, 24): ✅ pass - (test_for_break ensures) Return type constraint
-test_break_continue.py(19, 4): ✅ pass - assume_assume(362)_calls_PIn_0
 test_break_continue.py(17, 27): ✅ pass - (test_for_continue ensures) Return type constraint
-DETAIL: 10 passed, 0 failed, 0 inconclusive
+DETAIL: 8 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_bubble_sort_step.expected b/StrataTest/Languages/Python/expected_laurel/test_bubble_sort_step.expected
index f3de7b0866..fa612873ae 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_bubble_sort_step.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_bubble_sort_step.expected
@@ -1,41 +1,20 @@
-test_bubble_sort_step.py(12, 8): ✅ pass - set_t3_calls_Any_get_0
+test_bubble_sort_step.py(12, 8): ✅ pass - precondition
 test_bubble_sort_step.py(12, 8): ✅ pass - assert(250)
-test_bubble_sort_step.py(13, 8): ✅ pass - assert_assert(274)_calls_Any_get_0
 test_bubble_sort_step.py(13, 8): ✅ pass - Check Any_sets! exception
-test_bubble_sort_step.py(13, 8): ✅ pass - set_xs_calls_Any_get_0
 test_bubble_sort_step.py(14, 8): ✅ pass - Check Any_sets! exception
-test_bubble_sort_step.py(3, 7): ✅ pass - assert_assert(55)_calls_Any_get_0
-test_bubble_sort_step.py(3, 7): ✅ pass - assert_assert(55)_calls_Any_get_1
 test_bubble_sort_step.py(3, 7): ✅ pass - Check PGt exception
-test_bubble_sort_step.py(3, 4): ✅ pass - ite_cond_calls_Any_get_0
-test_bubble_sort_step.py(3, 4): ✅ pass - ite_cond_calls_Any_get_1
-test_bubble_sort_step.py(4, 8): ✅ pass - set_t_calls_Any_get_0
+test_bubble_sort_step.py(4, 8): ✅ pass - precondition
 test_bubble_sort_step.py(4, 8): ✅ pass - assert(78)
-test_bubble_sort_step.py(5, 8): ✅ pass - assert_assert(101)_calls_Any_get_0
 test_bubble_sort_step.py(5, 8): ✅ pass - Check Any_sets! exception
-test_bubble_sort_step.py(5, 8): ✅ pass - set_xs_calls_Any_get_0
 test_bubble_sort_step.py(6, 8): ✅ pass - Check Any_sets! exception
-test_bubble_sort_step.py(7, 7): ✅ pass - assert_assert(140)_calls_Any_get_0
-test_bubble_sort_step.py(7, 7): ✅ pass - assert_assert(140)_calls_Any_get_1
 test_bubble_sort_step.py(7, 7): ✅ pass - Check PGt exception
-test_bubble_sort_step.py(7, 4): ✅ pass - ite_cond_calls_Any_get_0
-test_bubble_sort_step.py(7, 4): ✅ pass - ite_cond_calls_Any_get_1
-test_bubble_sort_step.py(8, 8): ✅ pass - set_t2_calls_Any_get_0
+test_bubble_sort_step.py(8, 8): ✅ pass - precondition
 test_bubble_sort_step.py(8, 8): ✅ pass - assert(163)
-test_bubble_sort_step.py(9, 8): ✅ pass - assert_assert(187)_calls_Any_get_0
 test_bubble_sort_step.py(9, 8): ✅ pass - Check Any_sets! exception
-test_bubble_sort_step.py(9, 8): ✅ pass - set_xs_calls_Any_get_0
 test_bubble_sort_step.py(10, 8): ✅ pass - Check Any_sets! exception
-test_bubble_sort_step.py(11, 7): ✅ pass - assert_assert(227)_calls_Any_get_0
-test_bubble_sort_step.py(11, 7): ✅ pass - assert_assert(227)_calls_Any_get_1
 test_bubble_sort_step.py(11, 7): ✅ pass - Check PGt exception
-test_bubble_sort_step.py(11, 4): ✅ pass - ite_cond_calls_Any_get_0
-test_bubble_sort_step.py(11, 4): ✅ pass - ite_cond_calls_Any_get_1
-test_bubble_sort_step.py(15, 4): ✅ pass - assert_assert(311)_calls_Any_get_0
 test_bubble_sort_step.py(15, 4): ✅ pass - sorted first
-test_bubble_sort_step.py(16, 4): ✅ pass - assert_assert(349)_calls_Any_get_0
 test_bubble_sort_step.py(16, 4): ✅ pass - sorted second
-test_bubble_sort_step.py(17, 4): ✅ pass - assert_assert(388)_calls_Any_get_0
 test_bubble_sort_step.py(17, 4): ✅ pass - sorted third
-DETAIL: 39 passed, 0 failed, 0 inconclusive
+DETAIL: 18 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_empty.expected b/StrataTest/Languages/Python/expected_laurel/test_class_empty.expected
index aab04f3a0d..7f98693936 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_empty.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_empty.expected
@@ -1,4 +1,4 @@
-test_class_empty.py(5, 4): ✅ pass - callElimAssert_requires_4
+test_class_empty.py(5, 4): ✅ pass - precondition
 test_class_empty.py(6, 4): ✅ pass - empty class instantiated
 DETAIL: 2 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_field_init.expected b/StrataTest/Languages/Python/expected_laurel/test_class_field_init.expected
index 7cb1e2fc89..0ff29bd94b 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_field_init.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_field_init.expected
@@ -1,2 +1,3 @@
-DETAIL: 0 passed, 0 failed, 0 inconclusive
+test_class_field_init.py(20, 4): ✔️ always true if reached - (CircularBuffer@__init__ requires) Type constraint of size, (CircularBuffer@__init__ requires) Type constraint of name
+DETAIL: 1 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_field_use.expected b/StrataTest/Languages/Python/expected_laurel/test_class_field_use.expected
index 0caaf75c9f..29a689ea2c 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_field_use.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_field_use.expected
@@ -1,5 +1,6 @@
+test_class_field_use.py(13, 4): ✔️ always true if reached - (CircularBuffer@__init__ requires) Type constraint of n
 test_class_field_use.py(14, 4): ✔️ always true if reached - Check PMul exception
 test_class_field_use.py(14, 4): ✔️ always true if reached - assert(302)
 test_class_field_use.py(15, 4): ✔️ always true if reached - Doubling of buffer did not work
-DETAIL: 3 passed, 0 failed, 0 inconclusive
+DETAIL: 4 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_method_call_from_main.expected b/StrataTest/Languages/Python/expected_laurel/test_class_method_call_from_main.expected
index 0047be2edb..15fd5c1889 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_method_call_from_main.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_method_call_from_main.expected
@@ -1,6 +1,5 @@
 test_class_method_call_from_main.py(10, 8): ❓ unknown - name must not be empty
-test_class_method_call_from_main.py(9, 23): ❓ unknown - (Greeter@greet ensures) Return type constraint
 test_class_method_call_from_main.py(14, 4): ✅ pass - (Greeter@__init__ requires) Type constraint of name
 test_class_method_call_from_main.py(15, 4): ✅ pass - assert(415)
-DETAIL: 2 passed, 0 failed, 2 inconclusive
+DETAIL: 2 passed, 0 failed, 1 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_methods.expected b/StrataTest/Languages/Python/expected_laurel/test_class_methods.expected
index 36c53a8361..8c55563f01 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_methods.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_methods.expected
@@ -1,11 +1,16 @@
-test_class_methods.py(34, 4): ✔️ always true if reached - main_assert(471)_13
+test_class_methods.py(34, 4): ✔️ always true if reached - (Account@__init__ requires) Type constraint of owner, (Account@__init__ requires) Type constraint of balance
+test_class_methods.py(34, 4): ✔️ always true if reached - main_assert(471)_31
 test_class_methods.py(34, 4): ✔️ always true if reached - get_owner should return Alice
-test_class_methods.py(34, 4): ✔️ always true if reached - main_assert(564)_15
+test_class_methods.py(34, 4): ✔️ always true if reached - main_assert(564)_34
 test_class_methods.py(34, 4): ✔️ always true if reached - get_balance should return 100
-test_class_methods.py(34, 4): ✔️ always true if reached - main_assert(678)_17
+test_class_methods.py(34, 4): ✔️ always true if reached - (Account@set_balance requires) Type constraint of amount
+test_class_methods.py(27, 4): ✔️ always true if reached - (Account@set_balance ensures) Return type constraint
+test_class_methods.py(34, 4): ✔️ always true if reached - main_assert(678)_39
 test_class_methods.py(34, 4): ✔️ always true if reached - set_balance should update balance
+test_class_methods.py(34, 4): ✔️ always true if reached - (Origin_test_helper_procedure_Requires)req_name_is_foo, (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str, (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar
 test_class_methods.py(31, 4): ✔️ always true if reached - assert_name_is_foo
 test_class_methods.py(31, 4): ✔️ always true if reached - assert_opt_name_none_or_str
 test_class_methods.py(31, 4): ✔️ always true if reached - assert_opt_name_none_or_bar
-DETAIL: 9 passed, 0 failed, 0 inconclusive
+test_class_methods.py(31, 4): ✔️ always true if reached - ensures_maybe_except_none
+DETAIL: 14 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_mixed_init.expected b/StrataTest/Languages/Python/expected_laurel/test_class_mixed_init.expected
index 766329f9a4..ee2f8ef831 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_mixed_init.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_mixed_init.expected
@@ -1,4 +1,6 @@
+test_class_mixed_init.py(19, 0): ✔️ always true if reached - (WithInit@__init__ requires) Type constraint of x
 test_class_mixed_init.py(19, 0): ✔️ always true if reached - class with init
+test_class_mixed_init.py(19, 0): ✔️ always true if reached - precondition
 test_class_mixed_init.py(19, 0): ❓ unknown - class with init
-DETAIL: 1 passed, 0 failed, 1 inconclusive
+DETAIL: 3 passed, 0 failed, 1 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_no_init.expected b/StrataTest/Languages/Python/expected_laurel/test_class_no_init.expected
index 7228247375..a55c76cfe4 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_no_init.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_no_init.expected
@@ -1,4 +1,4 @@
-test_class_no_init.py(5, 4): ✅ pass - callElimAssert_requires_4
+test_class_no_init.py(5, 4): ✅ pass - precondition
 test_class_no_init.py(6, 4): ❓ unknown - class without __init__
 DETAIL: 1 passed, 0 failed, 1 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_no_init_multi_field.expected b/StrataTest/Languages/Python/expected_laurel/test_class_no_init_multi_field.expected
index 3dbe40b3b6..13ba7f459b 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_no_init_multi_field.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_no_init_multi_field.expected
@@ -1,4 +1,4 @@
-test_class_no_init_multi_field.py(7, 4): ✅ pass - callElimAssert_requires_4
+test_class_no_init_multi_field.py(7, 4): ✅ pass - precondition
 test_class_no_init_multi_field.py(8, 4): ✅ pass - class with multiple annotated fields no init
 DETAIL: 2 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_no_init_with_method.expected b/StrataTest/Languages/Python/expected_laurel/test_class_no_init_with_method.expected
index 29b6682a29..82dccbedf2 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_no_init_with_method.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_no_init_with_method.expected
@@ -1,5 +1,4 @@
-test_class_no_init_with_method.py(4, 23): ❓ unknown - (WithMethod@get_x ensures) Return type constraint
-test_class_no_init_with_method.py(8, 4): ✅ pass - callElimAssert_requires_4
+test_class_no_init_with_method.py(8, 4): ✅ pass - precondition
 test_class_no_init_with_method.py(9, 4): ✅ pass - class with method but no __init__
-DETAIL: 2 passed, 0 failed, 1 inconclusive
-RESULT: Inconclusive
+DETAIL: 2 passed, 0 failed, 0 inconclusive
+RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_with_methods.expected b/StrataTest/Languages/Python/expected_laurel/test_class_with_methods.expected
index 1085e02e58..c98dfdd1e0 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_with_methods.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_with_methods.expected
@@ -1,9 +1,16 @@
-test_class_with_methods.py(32, 4): ✔️ always true if reached - main_assert(484)_12
+test_class_with_methods.py(32, 4): ✔️ always true if reached - (DataStore@__init__ requires) Type constraint of name
+test_class_with_methods.py(32, 4): ✔️ always true if reached - (DataStore@add requires) Type constraint of amount
+test_class_with_methods.py(20, 4): ✔️ always true if reached - (DataStore@add ensures) Return type constraint
+test_class_with_methods.py(32, 4): ✔️ always true if reached - (DataStore@add requires) Type constraint of amount
+test_class_with_methods.py(21, 4): ✔️ always true if reached - (DataStore@add ensures) Return type constraint
+test_class_with_methods.py(32, 4): ✔️ always true if reached - main_assert(484)_34
 test_class_with_methods.py(32, 4): ✔️ always true if reached - get_count should return 30
-test_class_with_methods.py(32, 4): ✔️ always true if reached - main_assert(569)_14
+test_class_with_methods.py(32, 4): ✔️ always true if reached - main_assert(569)_37
 test_class_with_methods.py(32, 4): ✔️ always true if reached - get_name should return mystore
+test_class_with_methods.py(32, 4): ✔️ always true if reached - (Origin_test_helper_procedure_Requires)req_name_is_foo, (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str, (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar
 test_class_with_methods.py(29, 4): ✔️ always true if reached - assert_name_is_foo
 test_class_with_methods.py(29, 4): ✔️ always true if reached - assert_opt_name_none_or_str
 test_class_with_methods.py(29, 4): ✔️ always true if reached - assert_opt_name_none_or_bar
-DETAIL: 7 passed, 0 failed, 0 inconclusive
+test_class_with_methods.py(29, 4): ✔️ always true if reached - ensures_maybe_except_none
+DETAIL: 14 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_coerce_int_in_any_list.expected b/StrataTest/Languages/Python/expected_laurel/test_coerce_int_in_any_list.expected
index 26134635da..eb8eb43cbf 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_coerce_int_in_any_list.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_coerce_int_in_any_list.expected
@@ -1,6 +1,4 @@
-test_coerce_int_in_any_list.py(5, 4): ✅ pass - assert_assert(103)_calls_Any_get_0
 test_coerce_int_in_any_list.py(5, 4): ✅ pass - int in Any list
-test_coerce_int_in_any_list.py(6, 4): ✅ pass - assert_assert(144)_calls_Any_get_0
 test_coerce_int_in_any_list.py(6, 4): ✅ pass - str in Any list
-DETAIL: 4 passed, 0 failed, 0 inconclusive
+DETAIL: 2 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_datetime.expected b/StrataTest/Languages/Python/expected_laurel/test_datetime.expected
index f627b50117..475cfe68af 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_datetime.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_datetime.expected
@@ -1,8 +1,5 @@
 test_datetime.py(13, 0): ✅ pass - (Origin_datetime_date_Requires)d_type
-test_datetime.py(14, 0): ✅ pass - (Origin_timedelta_Requires)
-test_datetime.py(14, 0): ✅ pass - (Origin_timedelta_Requires)hours_type
-test_datetime.py(14, 0): ✅ pass - (Origin_timedelta_Requires)days_pos
-test_datetime.py(14, 0): ✅ pass - (Origin_timedelta_Requires)hours_pos
+test_datetime.py(14, 0): ✅ pass - (Origin_timedelta_Requires), (Origin_timedelta_Requires)hours_type, (Origin_timedelta_Requires)days_pos, (Origin_timedelta_Requires)hours_pos
 test_datetime.py(15, 19): ✅ pass - Check PSub exception
 test_datetime.py(21, 7): ✅ pass - Check PLe exception
 test_datetime.py(21, 0): ✅ pass - assert(554)
@@ -10,5 +7,5 @@ test_datetime.py(25, 0): ✅ pass - assert(673)
 test_datetime.py(27, 0): ✅ pass - assert(758)
 test_datetime.py(30, 7): ✅ pass - Check PLe exception
 test_datetime.py(30, 0): ✅ pass - assert(859)
-DETAIL: 12 passed, 0 failed, 0 inconclusive
+DETAIL: 9 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_datetime_now_tz.expected b/StrataTest/Languages/Python/expected_laurel/test_datetime_now_tz.expected
index 4ef6e80e7b..50f1fb5f5e 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_datetime_now_tz.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_datetime_now_tz.expected
@@ -1,9 +1,6 @@
-test_datetime_now_tz.py(4, 0): ✅ pass - (Origin_timedelta_Requires)
-test_datetime_now_tz.py(4, 0): ✅ pass - (Origin_timedelta_Requires)hours_type
-test_datetime_now_tz.py(4, 0): ✅ pass - (Origin_timedelta_Requires)days_pos
-test_datetime_now_tz.py(4, 0): ✅ pass - (Origin_timedelta_Requires)hours_pos
+test_datetime_now_tz.py(4, 0): ✅ pass - (Origin_timedelta_Requires), (Origin_timedelta_Requires)hours_type, (Origin_timedelta_Requires)days_pos, (Origin_timedelta_Requires)hours_pos
 test_datetime_now_tz.py(5, 18): ✅ pass - Check PSub exception
 test_datetime_now_tz.py(6, 7): ✅ pass - Check PLe exception
 test_datetime_now_tz.py(6, 0): ✅ pass - assert(162)
-DETAIL: 7 passed, 0 failed, 0 inconclusive
+DETAIL: 4 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_deep_inline.expected b/StrataTest/Languages/Python/expected_laurel/test_deep_inline.expected
index eac560309d..40951a6720 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_deep_inline.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_deep_inline.expected
@@ -1,11 +1,15 @@
+test_deep_inline.py(21, 4): ✔️ always true if reached - (triple_apply requires) Type constraint of x
+test_deep_inline.py(15, 4): ✔️ always true if reached - (double_inc requires) Type constraint of x
+test_deep_inline.py(10, 4): ✔️ always true if reached - (inc requires) Type constraint of x
 test_deep_inline.py(6, 4): ✔️ always true if reached - Check PAdd exception
-test_deep_inline.py(10, 4): ✔️ always true if reached - double_inc_assert(135)_35
+test_deep_inline.py(10, 4): ✔️ always true if reached - double_inc_assert(135)_56
 test_deep_inline.py(10, 4): ✔️ always true if reached - Check PMul exception
-test_deep_inline.py(15, 4): ✔️ always true if reached - triple_apply_assert(206)_17
+test_deep_inline.py(15, 4): ✔️ always true if reached - triple_apply_assert(206)_27
+test_deep_inline.py(15, 4): ✔️ always true if reached - (inc requires) Type constraint of x
 test_deep_inline.py(11, 4): ✔️ always true if reached - Check PAdd exception
-test_deep_inline.py(15, 4): ✔️ always true if reached - triple_apply_assert(233)_18
-test_deep_inline.py(21, 4): ✔️ always true if reached - main_assert(279)_5
+test_deep_inline.py(15, 4): ✔️ always true if reached - triple_apply_assert(233)_30
+test_deep_inline.py(21, 4): ✔️ always true if reached - main_assert(279)_9
 test_deep_inline.py(21, 4): ✔️ always true if reached - triple_apply(3) should be 9
 test_deep_inline.py(21, 4): ✖️ always false if reached - triple_apply(3) should not be 10
-DETAIL: 8 passed, 1 failed, 0 inconclusive
+DETAIL: 12 passed, 1 failed, 0 inconclusive
 RESULT: Failures found
diff --git a/StrataTest/Languages/Python/expected_laurel/test_deeply_nested_list.expected b/StrataTest/Languages/Python/expected_laurel/test_deeply_nested_list.expected
index 1cc971115e..a5254648f8 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_deeply_nested_list.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_deeply_nested_list.expected
@@ -1,6 +1,3 @@
-test_deeply_nested_list.py(3, 4): ✅ pass - assert_assert(33)_calls_Any_get_0
-test_deeply_nested_list.py(3, 4): ✅ pass - assert_assert(33)_calls_Any_get_1
-test_deeply_nested_list.py(3, 4): ✅ pass - assert_assert(33)_calls_Any_get_2
 test_deeply_nested_list.py(3, 4): ✅ pass - triple nested list
-DETAIL: 4 passed, 0 failed, 0 inconclusive
+DETAIL: 1 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_default_params.expected b/StrataTest/Languages/Python/expected_laurel/test_default_params.expected
index 395575a21c..15898dab3f 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_default_params.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_default_params.expected
@@ -1,27 +1,21 @@
 test_default_params.py(2, 18): ✅ pass - Check PAdd exception
 test_default_params.py(2, 4): ✅ pass - assert(58)
-test_default_params.py(1, 49): ✅ pass - (greet ensures) Return type constraint
 test_default_params.py(6, 4): ✅ pass - assert(160)
 test_default_params.py(7, 4): ✅ pass - assert(180)
 test_default_params.py(8, 10): ✅ pass - Check PLt exception
 test_default_params.py(9, 17): ❓ unknown - Check PMul exception
 test_default_params.py(10, 12): ❓ unknown - Check PAdd exception
-test_default_params.py(5, 38): ❓ unknown - (power ensures) Return type constraint
-test_default_params.py(14, 4): ✅ pass - (greet requires) Type constraint of name
-test_default_params.py(14, 4): ✅ pass - (greet requires) Type constraint of greeting
+test_default_params.py(14, 4): ✅ pass - (greet requires) Type constraint of name, (greet requires) Type constraint of greeting
 test_default_params.py(14, 4): ✅ pass - assert(294)
 test_default_params.py(15, 4): ❓ unknown - default greeting failed
-test_default_params.py(17, 4): ✅ pass - (greet requires) Type constraint of name
-test_default_params.py(17, 4): ✅ pass - (greet requires) Type constraint of greeting
+test_default_params.py(17, 4): ✅ pass - (greet requires) Type constraint of name, (greet requires) Type constraint of greeting
 test_default_params.py(17, 4): ✅ pass - assert(386)
 test_default_params.py(18, 4): ❓ unknown - explicit greeting failed
-test_default_params.py(20, 4): ✅ pass - (power requires) Type constraint of base
-test_default_params.py(20, 4): ✅ pass - (power requires) Type constraint of exp
+test_default_params.py(20, 4): ✅ pass - (power requires) Type constraint of base, (power requires) Type constraint of exp
 test_default_params.py(20, 4): ✅ pass - assert(478)
 test_default_params.py(21, 4): ❓ unknown - default power failed
-test_default_params.py(23, 4): ✅ pass - (power requires) Type constraint of base
-test_default_params.py(23, 4): ✅ pass - (power requires) Type constraint of exp
+test_default_params.py(23, 4): ✅ pass - (power requires) Type constraint of base, (power requires) Type constraint of exp
 test_default_params.py(23, 4): ✅ pass - assert(545)
 test_default_params.py(24, 4): ❓ unknown - explicit power failed
-DETAIL: 18 passed, 0 failed, 7 inconclusive
+DETAIL: 13 passed, 0 failed, 6 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_dict_add_key.expected b/StrataTest/Languages/Python/expected_laurel/test_dict_add_key.expected
index fe764d0f3f..02d7caccf7 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_dict_add_key.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_dict_add_key.expected
@@ -1,5 +1,4 @@
 test_dict_add_key.py(3, 4): ✅ pass - Check Any_sets! exception
-test_dict_add_key.py(4, 4): ✅ pass - assert_assert(56)_calls_Any_get_0
 test_dict_add_key.py(4, 4): ✅ pass - dict add key
-DETAIL: 3 passed, 0 failed, 0 inconclusive
+DETAIL: 2 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_dict_assign.expected b/StrataTest/Languages/Python/expected_laurel/test_dict_assign.expected
index 3c6fafeb0a..ea52fc6ed8 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_dict_assign.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_dict_assign.expected
@@ -1,5 +1,4 @@
 test_dict_assign.py(3, 4): ✅ pass - Check Any_sets! exception
-test_dict_assign.py(4, 4): ✅ pass - assert_assert(62)_calls_Any_get_0
 test_dict_assign.py(4, 4): ✅ pass - dict update
-DETAIL: 3 passed, 0 failed, 0 inconclusive
+DETAIL: 2 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_dict_create.expected b/StrataTest/Languages/Python/expected_laurel/test_dict_create.expected
index 5613842891..7c8bf156fc 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_dict_create.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_dict_create.expected
@@ -1,6 +1,4 @@
-test_dict_create.py(3, 4): ✅ pass - assert_assert(53)_calls_Any_get_0
 test_dict_create.py(3, 4): ✅ pass - dict access
-test_dict_create.py(4, 4): ✅ pass - assert_assert(91)_calls_Any_get_0
 test_dict_create.py(4, 4): ✅ pass - dict access b
-DETAIL: 4 passed, 0 failed, 0 inconclusive
+DETAIL: 2 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_dict_empty.expected b/StrataTest/Languages/Python/expected_laurel/test_dict_empty.expected
new file mode 100644
index 0000000000..cb184bdea0
--- /dev/null
+++ b/StrataTest/Languages/Python/expected_laurel/test_dict_empty.expected
@@ -0,0 +1,5 @@
+test_dict_empty.py(3, 4): ✅ pass - assert(38)
+test_dict_empty.py(5, 16): ✅ pass - Check PAdd exception
+test_dict_empty.py(6, 4): ✅ pass - empty dict
+DETAIL: 3 passed, 0 failed, 0 inconclusive
+RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_dict_in.expected b/StrataTest/Languages/Python/expected_laurel/test_dict_in.expected
index 57ab802313..b3d9fea177 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_dict_in.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_dict_in.expected
@@ -1,6 +1,4 @@
-test_dict_in.py(3, 4): ✅ pass - assert_assert(49)_calls_PIn_0
 test_dict_in.py(3, 4): ✅ pass - key in dict
-test_dict_in.py(4, 4): ✅ pass - assert_assert(84)_calls_PNotIn_0
 test_dict_in.py(4, 4): ✅ pass - key not in dict
-DETAIL: 4 passed, 0 failed, 0 inconclusive
+DETAIL: 2 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_dict_of_list.expected b/StrataTest/Languages/Python/expected_laurel/test_dict_of_list.expected
index 7fc8fa186e..453effc4a2 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_dict_of_list.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_dict_of_list.expected
@@ -1,5 +1,3 @@
-test_dict_of_list.py(5, 4): ✅ pass - assert_assert(91)_calls_Any_get_0
-test_dict_of_list.py(5, 4): ✅ pass - assert_assert(91)_calls_Any_get_1
 test_dict_of_list.py(5, 4): ✅ pass - dict of list
-DETAIL: 3 passed, 0 failed, 0 inconclusive
+DETAIL: 1 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_dict_operations.expected b/StrataTest/Languages/Python/expected_laurel/test_dict_operations.expected
index 98c3037b20..5c7b7c9d26 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_dict_operations.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_dict_operations.expected
@@ -1,26 +1,12 @@
-test_dict_operations.py(7, 0): ✅ pass - assert_assert(81)_calls_Any_get_0
 test_dict_operations.py(7, 0): ✅ pass - assert(81)
-test_dict_operations.py(8, 0): ✅ pass - assert_assert(118)_calls_Any_get_0
 test_dict_operations.py(8, 0): ✅ pass - assert(118)
 test_dict_operations.py(10, 0): ✅ pass - Check Any_sets! exception
-test_dict_operations.py(11, 0): ✅ pass - assert_assert(172)_calls_Any_get_0
 test_dict_operations.py(11, 0): ✅ pass - assert(172)
-test_dict_operations.py(13, 0): ✅ pass - assert_assert(204)_calls_PIn_0
 test_dict_operations.py(13, 0): ✅ pass - assert(204)
-test_dict_operations.py(14, 0): ✅ pass - assert_assert(228)_calls_PNotIn_0
 test_dict_operations.py(14, 0): ✅ pass - assert(228)
-test_dict_operations.py(23, 0): ✅ pass - assert_assert(403)_calls_Any_get_0
-test_dict_operations.py(23, 0): ✅ pass - assert_assert(403)_calls_Any_get_1
-test_dict_operations.py(23, 0): ✅ pass - assert_assert(403)_calls_Any_get_2
 test_dict_operations.py(23, 0): ✅ pass - assert(403)
-test_dict_operations.py(24, 0): ✅ pass - assert_assert(457)_calls_Any_get_0
-test_dict_operations.py(24, 0): ✅ pass - assert_assert(457)_calls_Any_get_1
-test_dict_operations.py(24, 0): ✅ pass - assert_assert(457)_calls_Any_get_2
 test_dict_operations.py(24, 0): ✅ pass - assert(457)
 test_dict_operations.py(26, 0): ✅ pass - Check Any_sets! exception
-test_dict_operations.py(27, 0): ✅ pass - assert_assert(557)_calls_Any_get_0
-test_dict_operations.py(27, 0): ✅ pass - assert_assert(557)_calls_Any_get_1
-test_dict_operations.py(27, 0): ✅ pass - assert_assert(557)_calls_Any_get_2
 test_dict_operations.py(27, 0): ✅ pass - assert(557)
-DETAIL: 24 passed, 0 failed, 0 inconclusive
+DETAIL: 10 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_dict_overwrite.expected b/StrataTest/Languages/Python/expected_laurel/test_dict_overwrite.expected
index a326876db0..4dea1038c4 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_dict_overwrite.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_dict_overwrite.expected
@@ -1,6 +1,5 @@
 test_dict_overwrite.py(3, 4): ✅ pass - Check Any_sets! exception
 test_dict_overwrite.py(4, 4): ✅ pass - Check Any_sets! exception
-test_dict_overwrite.py(5, 4): ✅ pass - assert_assert(78)_calls_Any_get_0
 test_dict_overwrite.py(5, 4): ✅ pass - dict overwrite
-DETAIL: 4 passed, 0 failed, 0 inconclusive
+DETAIL: 3 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_empty_dict_access.expected b/StrataTest/Languages/Python/expected_laurel/test_empty_dict_access.expected
index cb7f5dfa7d..9b0952a928 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_empty_dict_access.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_empty_dict_access.expected
@@ -1,8 +1,7 @@
-test_empty_dict_access.py(5, 8): ✅ pass - set_r_calls_Any_get_0
+test_empty_dict_access.py(5, 8): ✅ pass - precondition
 test_empty_dict_access.py(3, 4): ✅ pass - assert(33)
-test_empty_dict_access.py(4, 4): ✅ pass - ite_cond_calls_PIn_0
 test_empty_dict_access.py(7, 12): ✅ pass - Check PNeg exception
 test_empty_dict_access.py(8, 16): ✅ pass - Check PNeg exception
 test_empty_dict_access.py(8, 4): ✅ pass - missing key guarded
-DETAIL: 6 passed, 0 failed, 0 inconclusive
+DETAIL: 5 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_flag_pattern.expected b/StrataTest/Languages/Python/expected_laurel/test_flag_pattern.expected
index 1ae36f0f29..5afe4ea920 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_flag_pattern.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_flag_pattern.expected
@@ -1,9 +1,6 @@
 test_flag_pattern.py(3, 4): ✅ pass - assert(54)
-test_flag_pattern.py(4, 4): ✅ pass - assume_assume(81)_calls_PIn_0
-test_flag_pattern.py(5, 11): ✅ pass - assert_assert(108)_calls_PMod_0
 test_flag_pattern.py(5, 11): ✅ pass - Check PMod exception
-test_flag_pattern.py(5, 8): ✅ pass - ite_cond_calls_PMod_0
 test_flag_pattern.py(7, 11): ❓ unknown - Check PNot exception
 test_flag_pattern.py(7, 4): ❓ unknown - no even numbers
-DETAIL: 5 passed, 0 failed, 2 inconclusive
+DETAIL: 2 passed, 0 failed, 2 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_foo_client_folder.expected b/StrataTest/Languages/Python/expected_laurel/test_foo_client_folder.expected
new file mode 100644
index 0000000000..9762ca4aaf
--- /dev/null
+++ b/StrataTest/Languages/Python/expected_laurel/test_foo_client_folder.expected
@@ -0,0 +1,12 @@
+test_foo_client_folder.py(8, 0): ✅ pass - assert(204)
+test_foo_client_folder.py(9, 0): ✅ pass - assert(250)
+test_foo_client_folder.py(11, 0): ✅ pass - assert(273)
+test_foo_client_folder.py(12, 24): ✅ pass - Check PMul exception
+test_foo_client_folder.py(12, 0): ✅ pass - assert(303)
+test_foo_client_folder.py(13, 0): ✅ pass - assert(336)
+test_foo_client_folder.py(14, 0): ✅ pass - assert(379)
+test_foo_client_folder.py(15, 0): ✅ pass - assert(427)
+test_foo_client_folder.py(16, 0): ✅ pass - assert(477)
+test_foo_client_folder.py(17, 0): ✅ pass - assert(529)
+DETAIL: 10 passed, 0 failed, 0 inconclusive
+RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_for_else_break.expected b/StrataTest/Languages/Python/expected_laurel/test_for_else_break.expected
index 5d1dcabdd9..159cba6937 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_for_else_break.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_for_else_break.expected
@@ -1,5 +1,4 @@
 test_for_else_break.py(2, 4): ✅ pass - assert(31)
-test_for_else_break.py(3, 4): ✅ pass - assume_assume(46)_calls_PIn_0
 test_for_else_break.py(8, 4): ✅ pass - for else skipped on break
-DETAIL: 3 passed, 0 failed, 0 inconclusive
+DETAIL: 2 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_for_loop.expected b/StrataTest/Languages/Python/expected_laurel/test_for_loop.expected
index 77a760ea8f..6d5e1e9f35 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_for_loop.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_for_loop.expected
@@ -1,14 +1,11 @@
 test_for_loop.py(3, 4): ✅ pass - assert(64)
-test_for_loop.py(4, 4): ✅ pass - assume_assume(83)_calls_PIn_0
 test_for_loop.py(5, 16): ❓ unknown - Check PAdd exception
 test_for_loop.py(6, 4): ❓ unknown - sum of list should be 15
 test_for_loop.py(11, 4): ✅ pass - assert(274)
-test_for_loop.py(12, 4): ✅ pass - assume_assume(293)_calls_PIn_0
 test_for_loop.py(13, 11): ✅ pass - Check PGt exception
 test_for_loop.py(14, 20): ❓ unknown - Check PAdd exception
 test_for_loop.py(15, 4): ❓ unknown - should count 3 items greater than 3
 test_for_loop.py(20, 4): ✅ pass - assert(512)
-test_for_loop.py(21, 4): ✅ pass - assume_assume(531)_calls_PIn_0
 test_for_loop.py(25, 4): ❓ unknown (pass on 1 path, unknown on 2 paths) - should have found 30
-DETAIL: 7 passed, 0 failed, 5 inconclusive
+DETAIL: 4 passed, 0 failed, 5 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_for_range.expected b/StrataTest/Languages/Python/expected_laurel/test_for_range.expected
index 03b0272495..18338bf176 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_for_range.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_for_range.expected
@@ -1,13 +1,11 @@
-test_for_range.py(10, 0): ✅ pass - set_i_calls_range_0
-test_for_range.py(3, 0): ✅ pass - set_i_calls_range_0
 test_for_range.py(4, 11): ✅ pass - Check PLt exception
 test_for_range.py(4, 4): ✅ pass - assert(46)
 test_for_range.py(5, 11): ✅ pass - Check PGe exception
 test_for_range.py(5, 4): ✅ pass - assert(63)
-test_for_range.py(6, 4): ✅ pass - set_j_calls_Any_get_0
+test_for_range.py(6, 4): ✅ pass - precondition
 test_for_range.py(7, 11): ✅ pass - Check PLt exception
 test_for_range.py(7, 4): ✅ pass - assert(101)
 test_for_range.py(10, 15): ✅ pass - Check PNeg exception
 test_for_range.py(13, 0): ✅ pass - assert(156)
-DETAIL: 11 passed, 0 failed, 0 inconclusive
+DETAIL: 9 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected b/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected
index 014be579f7..16460b41a6 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_func_input_type_constraints.expected
@@ -1,16 +1,8 @@
 test_func_input_type_constraints.py(4, 11): ✅ pass - Check PMul exception
-test_func_input_type_constraints.py(3, 48): ✅ pass - (Mul ensures) Return type constraint
-test_func_input_type_constraints.py(6, 62): ✅ pass - (Sum ensures) Return type constraint
 test_func_input_type_constraints.py(9, 11): ✅ pass - Check PAdd exception
-test_func_input_type_constraints.py(12, 4): ❓ unknown - set_LaurelResult_calls_Any_get_0
-test_func_input_type_constraints.py(12, 4): ❓ unknown - set_LaurelResult_calls_Any_get_1
-test_func_input_type_constraints.py(11, 65): ❓ unknown - (List_Dict_index ensures) Return type constraint
-test_func_input_type_constraints.py(15, 0): ✅ pass - (Mul requires) Type constraint of x
-test_func_input_type_constraints.py(15, 0): ✅ pass - (Mul requires) Type constraint of y
-test_func_input_type_constraints.py(16, 0): ✅ pass - (Sum requires) Type constraint of x
-test_func_input_type_constraints.py(16, 0): ✅ pass - (Sum requires) Type constraint of y
-test_func_input_type_constraints.py(17, 0): ✅ pass - (List_Dict_index requires) Type constraint of l
-test_func_input_type_constraints.py(17, 0): ✅ pass - (List_Dict_index requires) Type constraint of i
-test_func_input_type_constraints.py(17, 0): ✅ pass - (List_Dict_index requires) Type constraint of s
-DETAIL: 11 passed, 0 failed, 3 inconclusive
+test_func_input_type_constraints.py(12, 4): ❓ unknown - precondition
+test_func_input_type_constraints.py(15, 0): ✅ pass - (Mul requires) Type constraint of x, (Mul requires) Type constraint of y
+test_func_input_type_constraints.py(16, 0): ✅ pass - (Sum requires) Type constraint of x, (Sum requires) Type constraint of y
+test_func_input_type_constraints.py(17, 0): ✅ pass - (List_Dict_index requires) Type constraint of l, (List_Dict_index requires) Type constraint of i, (List_Dict_index requires) Type constraint of s
+DETAIL: 5 passed, 0 failed, 1 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected b/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected
index 62499427b9..8e006bfe41 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected
@@ -1,6 +1,4 @@
-test_function_def_calls.py(6, 4): ❓ unknown - (Origin_test_helper_procedure_Requires)req_name_is_foo
-test_function_def_calls.py(6, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str
-test_function_def_calls.py(6, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar
+test_function_def_calls.py(6, 4): ❓ unknown - (Origin_test_helper_procedure_Requires)req_name_is_foo, (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str, (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar
 test_function_def_calls.py(9, 4): ✅ pass - (my_f requires) Type constraint of s
-DETAIL: 3 passed, 0 failed, 1 inconclusive
+DETAIL: 1 passed, 0 failed, 1 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_havoc_callee_after_hole_call.expected b/StrataTest/Languages/Python/expected_laurel/test_havoc_callee_after_hole_call.expected
index 9a320c707c..71a4c3013b 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_havoc_callee_after_hole_call.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_havoc_callee_after_hole_call.expected
@@ -2,9 +2,9 @@ test_havoc_callee_after_hole_call.py(8, 0): ❓ unknown - expected unknown becau
 test_havoc_callee_after_hole_call.py(12, 0): ❓ unknown - expected unknown because xs should be havocked
 test_havoc_callee_after_hole_call.py(16, 0): ✔️ always true if reached - chained call: receiver not havocked (chained attribute is not a Name)
 test_havoc_callee_after_hole_call.py(20, 0): ✔️ always true if reached - unrelated variable: nothing should be havocked
+test_havoc_callee_after_hole_call.py(22, 0): ✔️ always true if reached - (MyClass@__init__ requires) Type constraint of n
 test_havoc_callee_after_hole_call.py(25, 0): ✔️ always true if reached - composite arg: heap not havocked (out of scope)
 test_havoc_callee_after_hole_call.py(30, 0): ❓ unknown - expected unknown because argument locals should be havocked
-test_havoc_callee_after_hole_call.py(36, 0): ❓ unknown - assume_assume(1193)_calls_PIn_0
 test_havoc_callee_after_hole_call.py(37, 4): ✔️ always true if reached - for-loop over unmodeled iterator should not crash
-DETAIL: 4 passed, 0 failed, 4 inconclusive
+DETAIL: 5 passed, 0 failed, 3 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected b/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected
index 2c4b59ca73..18cd9da09a 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_if_elif.expected
@@ -1,5 +1,4 @@
 test_if_elif.py(2, 7): ✅ pass - Check PLt exception
-test_if_elif.py(1, 24): ✅ pass - (classify ensures) Return type constraint
 test_if_elif.py(6, 9): ✅ pass - Check PLt exception
 test_if_elif.py(12, 23): ✅ pass - Check PNeg exception
 test_if_elif.py(12, 4): ✅ pass - (classify requires) Type constraint of x
@@ -14,5 +13,5 @@ test_if_elif.py(19, 4): ❓ unknown - should be small
 test_if_elif.py(21, 4): ✅ pass - (classify requires) Type constraint of x
 test_if_elif.py(21, 4): ✅ pass - assert(416)
 test_if_elif.py(22, 4): ❓ unknown - should be large
-DETAIL: 12 passed, 0 failed, 4 inconclusive
+DETAIL: 11 passed, 0 failed, 4 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_int_floordiv.expected b/StrataTest/Languages/Python/expected_laurel/test_int_floordiv.expected
index a62d7083eb..dbaf2cfc25 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_int_floordiv.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_int_floordiv.expected
@@ -1,9 +1,8 @@
 test_int_floordiv.py(2, 4): ✅ pass - assert(29)
 test_int_floordiv.py(3, 4): ✅ pass - assert(45)
-test_int_floordiv.py(4, 13): ✅ pass - assert_assert(69)_calls_PFloorDiv_0
 test_int_floordiv.py(4, 13): ✅ pass - Check PFloorDiv exception
-test_int_floordiv.py(4, 4): ✅ pass - set_c_calls_PFloorDiv_0
+test_int_floordiv.py(4, 4): ✅ pass - precondition
 test_int_floordiv.py(4, 4): ✅ pass - assert(60)
 test_int_floordiv.py(5, 4): ✅ pass - int floor division
-DETAIL: 7 passed, 0 failed, 0 inconclusive
+DETAIL: 6 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_int_mod.expected b/StrataTest/Languages/Python/expected_laurel/test_int_mod.expected
index 1a2a0276e6..14a2c6f1fa 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_int_mod.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_int_mod.expected
@@ -1,9 +1,8 @@
 test_int_mod.py(2, 4): ✅ pass - assert(24)
 test_int_mod.py(3, 4): ✅ pass - assert(40)
-test_int_mod.py(4, 13): ✅ pass - assert_assert(64)_calls_PMod_0
 test_int_mod.py(4, 13): ✅ pass - Check PMod exception
-test_int_mod.py(4, 4): ✅ pass - set_c_calls_PMod_0
+test_int_mod.py(4, 4): ✅ pass - precondition
 test_int_mod.py(4, 4): ✅ pass - assert(55)
 test_int_mod.py(5, 4): ✅ pass - int modulo
-DETAIL: 7 passed, 0 failed, 0 inconclusive
+DETAIL: 6 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_int_negative_floordiv.expected b/StrataTest/Languages/Python/expected_laurel/test_int_negative_floordiv.expected
index 527ca97690..8c48e74acc 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_int_negative_floordiv.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_int_negative_floordiv.expected
@@ -1,7 +1,5 @@
-test_int_negative_floordiv.py(2, 11): ✅ pass - assert_assert(45)_calls_PFloorDiv_0
 test_int_negative_floordiv.py(2, 11): ✅ pass - Check PFloorDiv exception
 test_int_negative_floordiv.py(2, 24): ✅ pass - Check PNeg exception
-test_int_negative_floordiv.py(2, 4): ✅ pass - assert_assert(38)_calls_PFloorDiv_0
 test_int_negative_floordiv.py(2, 4): ✅ pass - floor division rounds toward negative infinity
-DETAIL: 5 passed, 0 failed, 0 inconclusive
+DETAIL: 3 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_int_negative_mod.expected b/StrataTest/Languages/Python/expected_laurel/test_int_negative_mod.expected
index 6f8a8fbc25..584acd0181 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_int_negative_mod.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_int_negative_mod.expected
@@ -1,6 +1,4 @@
-test_int_negative_mod.py(2, 11): ✅ pass - assert_assert(40)_calls_PMod_0
 test_int_negative_mod.py(2, 11): ✅ pass - Check PMod exception
-test_int_negative_mod.py(2, 4): ✅ pass - assert_assert(33)_calls_PMod_0
 test_int_negative_mod.py(2, 4): ✅ pass - python mod is always non-negative for positive divisor
-DETAIL: 4 passed, 0 failed, 0 inconclusive
+DETAIL: 2 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_list.expected b/StrataTest/Languages/Python/expected_laurel/test_list.expected
index f86f7b60d6..373b608e6d 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_list.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_list.expected
@@ -1,23 +1,14 @@
-test_list.py(3, 0): ✅ pass - assert_assert(32)_calls_PIn_0
 test_list.py(3, 0): ✅ pass - assert(32)
-test_list.py(5, 0): ✅ pass - set_n_calls_Any_get_0
+test_list.py(5, 0): ✅ pass - precondition
 test_list.py(7, 0): ✅ pass - assert(71)
-test_list.py(9, 0): ✅ pass - assert_assert(87)_calls_Any_get_0
 test_list.py(9, 0): ✅ pass - assert(87)
-test_list.py(11, 0): ✅ pass - assert_assert(113)_calls_Any_get_0
 test_list.py(11, 0): ✅ pass - assert(113)
 test_list.py(13, 0): ✅ pass - Check Any_sets! exception
-test_list.py(15, 0): ✅ pass - assert_assert(158)_calls_Any_get_0
 test_list.py(15, 0): ✅ pass - assert(158)
 test_list.py(19, 10): ✅ pass - Check PAdd exception
-test_list.py(21, 0): ✅ pass - assert_assert(250)_calls_Any_get_0
 test_list.py(21, 0): ✅ pass - assert(250)
 test_list.py(23, 0): ✅ pass - Check Any_sets! exception
-test_list.py(25, 7): ✅ pass - assert_assert(305)_calls_Any_get_0
-test_list.py(25, 7): ✅ pass - assert_assert(305)_calls_Any_get_1
 test_list.py(25, 7): ✅ pass - Check PAdd exception
-test_list.py(25, 0): ✅ pass - assert_assert(298)_calls_Any_get_0
-test_list.py(25, 0): ✅ pass - assert_assert(298)_calls_Any_get_1
 test_list.py(25, 0): ✅ pass - assert(298)
-DETAIL: 21 passed, 0 failed, 0 inconclusive
+DETAIL: 12 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_list_assign.expected b/StrataTest/Languages/Python/expected_laurel/test_list_assign.expected
index 032ca9ce08..68789afc86 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_list_assign.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_list_assign.expected
@@ -1,5 +1,4 @@
 test_list_assign.py(3, 4): ✅ pass - Check Any_sets! exception
-test_list_assign.py(4, 4): ✅ pass - assert_assert(62)_calls_Any_get_0
 test_list_assign.py(4, 4): ✅ pass - list element assignment
-DETAIL: 3 passed, 0 failed, 0 inconclusive
+DETAIL: 2 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_list_concat.expected b/StrataTest/Languages/Python/expected_laurel/test_list_concat.expected
index bfcfa2f91d..7f0f1e6dbb 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_list_concat.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_list_concat.expected
@@ -1,7 +1,5 @@
 test_list_concat.py(4, 8): ✅ pass - Check PAdd exception
-test_list_concat.py(5, 4): ✅ pass - assert_assert(72)_calls_Any_get_0
 test_list_concat.py(5, 4): ✅ pass - first
-test_list_concat.py(6, 4): ✅ pass - assert_assert(102)_calls_Any_get_0
 test_list_concat.py(6, 4): ✅ pass - last
-DETAIL: 5 passed, 0 failed, 0 inconclusive
+DETAIL: 3 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_list_create.expected b/StrataTest/Languages/Python/expected_laurel/test_list_create.expected
index 5ff4e591a6..58910edb15 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_list_create.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_list_create.expected
@@ -1,6 +1,4 @@
-test_list_create.py(3, 4): ✅ pass - assert_assert(47)_calls_Any_get_0
 test_list_create.py(3, 4): ✅ pass - first element
-test_list_create.py(4, 4): ✅ pass - assert_assert(86)_calls_Any_get_0
 test_list_create.py(4, 4): ✅ pass - last element
-DETAIL: 4 passed, 0 failed, 0 inconclusive
+DETAIL: 2 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_list_empty.expected b/StrataTest/Languages/Python/expected_laurel/test_list_empty.expected
index 3c2df0a452..503486c3c8 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_list_empty.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_list_empty.expected
@@ -1,6 +1,5 @@
 test_list_empty.py(3, 4): ✅ pass - assert(39)
-test_list_empty.py(4, 4): ✅ pass - assume_assume(58)_calls_PIn_0
 test_list_empty.py(5, 16): ✅ pass - Check PAdd exception
 test_list_empty.py(6, 4): ✅ pass - empty list
-DETAIL: 4 passed, 0 failed, 0 inconclusive
+DETAIL: 3 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_list_in.expected b/StrataTest/Languages/Python/expected_laurel/test_list_in.expected
index de531eb5d5..5efc327bc5 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_list_in.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_list_in.expected
@@ -1,6 +1,4 @@
-test_list_in.py(3, 4): ✅ pass - assert_assert(49)_calls_PIn_0
 test_list_in.py(3, 4): ✅ pass - element in list
-test_list_in.py(4, 4): ✅ pass - assert_assert(87)_calls_PNotIn_0
 test_list_in.py(4, 4): ✅ pass - element not in list
-DETAIL: 4 passed, 0 failed, 0 inconclusive
+DETAIL: 2 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_list_negative_index.expected b/StrataTest/Languages/Python/expected_laurel/test_list_negative_index.expected
index 7e1291e401..0c386b0cbb 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_list_negative_index.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_list_negative_index.expected
@@ -1,4 +1,3 @@
-test_list_negative_index.py(3, 4): ✅ pass - assert_assert(58)_calls_Any_get_0
 test_list_negative_index.py(3, 4): ✅ pass - negative index
-DETAIL: 2 passed, 0 failed, 0 inconclusive
+DETAIL: 1 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_list_of_list.expected b/StrataTest/Languages/Python/expected_laurel/test_list_of_list.expected
index 2a613b7d1b..1564c05b62 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_list_of_list.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_list_of_list.expected
@@ -1,5 +1,3 @@
-test_list_of_list.py(5, 4): ✅ pass - assert_assert(84)_calls_Any_get_0
-test_list_of_list.py(5, 4): ✅ pass - assert_assert(84)_calls_Any_get_1
 test_list_of_list.py(5, 4): ✅ pass - list of list
-DETAIL: 3 passed, 0 failed, 0 inconclusive
+DETAIL: 1 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_list_slice.expected b/StrataTest/Languages/Python/expected_laurel/test_list_slice.expected
index ce237e95f1..4f449765c7 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_list_slice.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_list_slice.expected
@@ -1,22 +1,13 @@
-test_list_slice.py(3, 0): ✅ pass - assert_assert(32)_calls_Any_get_slice_0
-test_list_slice.py(3, 0): ✅ pass - assert_assert(32)_calls_Any_get_1
 test_list_slice.py(3, 0): ✅ pass - assert(32)
-test_list_slice.py(7, 0): ✅ pass - assert_assert(145)_calls_Any_get_slice_0
-test_list_slice.py(7, 0): ✅ pass - assert_assert(145)_calls_Any_get_1
-test_list_slice.py(7, 0): ✅ pass - assert_assert(145)_calls_Any_get_2
 test_list_slice.py(7, 0): ✅ pass - assert(145)
-test_list_slice.py(9, 0): ✅ pass - assert_assert(187)_calls_Any_get_slice_0
 test_list_slice.py(9, 0): ✅ pass - assert(187)
 test_list_slice.py(11, 16): ✅ pass - Check PNeg exception
 test_list_slice.py(11, 19): ✅ pass - Check PNeg exception
-test_list_slice.py(11, 0): ✅ pass - assert_assert(220)_calls_Any_get_slice_0
 test_list_slice.py(11, 0): ✅ pass - assert(220)
 test_list_slice.py(13, 16): ✅ pass - Check PNeg exception
 test_list_slice.py(13, 21): ✅ pass - Check PNeg exception
-test_list_slice.py(13, 0): ✅ pass - assert_assert(260)_calls_Any_get_slice_0
 test_list_slice.py(13, 0): ✅ pass - assert(260)
 test_list_slice.py(15, 18): ✅ pass - Check PNeg exception
-test_list_slice.py(15, 0): ✅ pass - assert_assert(307)_calls_Any_get_slice_0
 test_list_slice.py(15, 0): ✅ pass - assert(307)
-DETAIL: 20 passed, 0 failed, 0 inconclusive
+DETAIL: 11 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_loops.expected b/StrataTest/Languages/Python/expected_laurel/test_loops.expected
index 4adb7f6b70..0139b2727f 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_loops.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_loops.expected
@@ -1,19 +1,14 @@
 test_loops.py(3, 4): ✅ pass - assert(38)
-test_loops.py(4, 4): ✅ pass - assume_assume(53)_calls_PIn_0
 test_loops.py(5, 12): ❓ unknown - Check PAdd exception
 test_loops.py(6, 11): ❓ unknown - Check PGt exception
 test_loops.py(6, 4): ❓ unknown - simple loop incremented
 test_loops.py(9, 4): ✅ pass - assert(174)
-test_loops.py(10, 4): ❓ unknown - set_a_calls_Any_get_0
-test_loops.py(10, 4): ❓ unknown - set_b_calls_Any_get_0
+test_loops.py(10, 4): ❓ unknown - precondition
 test_loops.py(11, 13): ❓ unknown - Check PSub exception
 test_loops.py(12, 11): ❓ unknown - Check PLt exception
 test_loops.py(12, 4): ❓ unknown - tuple unpacking decremented
 test_loops.py(15, 4): ✅ pass - assert(337)
-test_loops.py(16, 4): ❓ unknown - set_x_calls_Any_get_0
-test_loops.py(16, 4): ❓ unknown - set_tuple_360_calls_Any_get_0
-test_loops.py(16, 4): ❓ unknown - set_y_calls_Any_get_0
-test_loops.py(16, 4): ❓ unknown - set_z_calls_Any_get_0
+test_loops.py(16, 4): ❓ unknown - precondition
 test_loops.py(17, 13): ❓ unknown - Check PAdd exception
 test_loops.py(18, 11): ❓ unknown - Check PGt exception
 test_loops.py(18, 4): ❓ unknown - nested unpacking incremented
@@ -22,5 +17,5 @@ test_loops.py(22, 10): ✅ pass - Check PGt exception
 test_loops.py(23, 13): ❓ unknown - Check PSub exception
 test_loops.py(24, 11): ❓ unknown - Check PLe exception
 test_loops.py(24, 4): ❓ unknown - while loop did not increase n4
-DETAIL: 6 passed, 0 failed, 18 inconclusive
+DETAIL: 5 passed, 0 failed, 14 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_method_call_with_kwargs.expected b/StrataTest/Languages/Python/expected_laurel/test_method_call_with_kwargs.expected
index 315f62f13d..2503bcbd16 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_method_call_with_kwargs.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_method_call_with_kwargs.expected
@@ -1,9 +1,4 @@
-test_method_call_with_kwargs.py(5, 82): ✅ pass - (MyClass@some_method ensures) Return type constraint
-test_method_call_with_kwargs.py(8, 0): ✅ pass - (MyClass@__init__ requires) Type constraint of ip1
-test_method_call_with_kwargs.py(8, 0): ✅ pass - (MyClass@__init__ requires) Type constraint of ip2
-test_method_call_with_kwargs.py(8, 0): ✅ pass - (MyClass@__init__ requires) Type constraint of ip3
-test_method_call_with_kwargs.py(9, 0): ✅ pass - (MyClass@some_method requires) Type constraint of ip1
-test_method_call_with_kwargs.py(9, 0): ✅ pass - (MyClass@some_method requires) Type constraint of ip2
-test_method_call_with_kwargs.py(9, 0): ✅ pass - (MyClass@some_method requires) Type constraint of ip3
-DETAIL: 7 passed, 0 failed, 0 inconclusive
+test_method_call_with_kwargs.py(8, 0): ✅ pass - (MyClass@__init__ requires) Type constraint of ip1, (MyClass@__init__ requires) Type constraint of ip2, (MyClass@__init__ requires) Type constraint of ip3
+test_method_call_with_kwargs.py(9, 0): ✅ pass - (MyClass@some_method requires) Type constraint of ip1, (MyClass@some_method requires) Type constraint of ip2, (MyClass@some_method requires) Type constraint of ip3
+DETAIL: 2 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_method_kwargs_no_hierarchy.expected b/StrataTest/Languages/Python/expected_laurel/test_method_kwargs_no_hierarchy.expected
index 56de827e26..37ed3dac07 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_method_kwargs_no_hierarchy.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_method_kwargs_no_hierarchy.expected
@@ -1,12 +1,8 @@
-test_method_kwargs_no_hierarchy.py(5, 41): ❓ unknown - (Calculator@add ensures) Return type constraint
 test_method_kwargs_no_hierarchy.py(9, 4): ✅ pass - (Calculator@__init__ requires) Type constraint of base
-unknown location: ✅ pass - assert_assert(0)_calls_Any_get_or_none_0
 unknown location: ✅ pass - assert(0)
-test_method_kwargs_no_hierarchy.py(11, 18): ✅ pass - init_calls_Any_get_or_none_0
-test_method_kwargs_no_hierarchy.py(11, 18): ✅ pass - (Calculator@add requires) Type constraint of x
-test_method_kwargs_no_hierarchy.py(11, 18): ✅ pass - (Calculator@add requires) Type constraint of y
+test_method_kwargs_no_hierarchy.py(11, 18): ✅ pass - (Calculator@add requires) Type constraint of x, (Calculator@add requires) Type constraint of y
 test_method_kwargs_no_hierarchy.py(11, 4): ✅ pass - assert(254)
 test_method_kwargs_no_hierarchy.py(12, 4): ❓ unknown - assert(286)
 test_method_kwargs_no_hierarchy.py(8, 14): ✅ pass - (main ensures) Return type constraint
-DETAIL: 8 passed, 0 failed, 2 inconclusive
+DETAIL: 5 passed, 0 failed, 1 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_missing_models.expected b/StrataTest/Languages/Python/expected_laurel/test_missing_models.expected
index e0c6cdcdc4..dcf01d30af 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_missing_models.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_missing_models.expected
@@ -1,13 +1,5 @@
-test_missing_models.py(12, 4): ❓ unknown (pass on 2 paths, unknown on 1 path) - (Origin_test_helper_procedure_Requires)req_name_is_foo
-test_missing_models.py(12, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str
-test_missing_models.py(12, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar
-test_missing_models.py(15, 4): ❓ unknown (pass on 2 paths, unknown on 1 path) - (Origin_test_helper_procedure_Requires)req_name_is_foo
-test_missing_models.py(15, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str
-test_missing_models.py(15, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar
-test_missing_models.py(8, 4): ❓ unknown - init_calls_Any_get_0
-test_missing_models.py(8, 4): ❓ unknown - init_calls_Any_get_1
-test_missing_models.py(9, 4): ❓ unknown - (Origin_test_helper_procedure_Requires)req_name_is_foo
-test_missing_models.py(9, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str
-test_missing_models.py(9, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar
-DETAIL: 6 passed, 0 failed, 5 inconclusive
+test_missing_models.py(12, 4): ❓ unknown (pass on 2 paths, unknown on 1 path) - (Origin_test_helper_procedure_Requires)req_name_is_foo, (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str, (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar
+test_missing_models.py(15, 4): ❓ unknown (pass on 2 paths, unknown on 1 path) - (Origin_test_helper_procedure_Requires)req_name_is_foo, (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str, (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar
+test_missing_models.py(9, 4): ❓ unknown - (Origin_test_helper_procedure_Requires)req_name_is_foo, (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str, (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar
+DETAIL: 0 passed, 0 failed, 3 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_mixed_types_list.expected b/StrataTest/Languages/Python/expected_laurel/test_mixed_types_list.expected
index 6ea1964407..19a65113f5 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_mixed_types_list.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_mixed_types_list.expected
@@ -1,6 +1,4 @@
-test_mixed_types_list.py(3, 4): ✅ pass - assert_assert(56)_calls_Any_get_0
 test_mixed_types_list.py(3, 4): ✅ pass - int element
-test_mixed_types_list.py(4, 4): ✅ pass - assert_assert(93)_calls_Any_get_0
 test_mixed_types_list.py(4, 4): ✅ pass - str element
-DETAIL: 4 passed, 0 failed, 0 inconclusive
+DETAIL: 2 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_module_level.expected b/StrataTest/Languages/Python/expected_laurel/test_module_level.expected
index d6bc9a6556..4f7f991788 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_module_level.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_module_level.expected
@@ -1,13 +1,8 @@
-test_module_level.py(9, 0): ✅ pass - assert_assert(115)_calls_Any_get_0
 test_module_level.py(9, 0): ✅ pass - assert(115)
-test_module_level.py(10, 0): ✅ pass - assert_assert(145)_calls_Any_get_0
 test_module_level.py(10, 0): ✅ pass - assert(145)
 test_module_level.py(12, 0): ✅ pass - Check Any_sets! exception
-test_module_level.py(13, 0): ✅ pass - assert_assert(201)_calls_Any_get_0
 test_module_level.py(13, 0): ✅ pass - assert(201)
-test_module_level.py(14, 0): ✅ pass - assert_assert(236)_calls_PIn_0
 test_module_level.py(14, 0): ✅ pass - assert(236)
-test_module_level.py(15, 0): ✅ pass - assert_assert(258)_calls_PNotIn_0
 test_module_level.py(15, 0): ✅ pass - assert(258)
-DETAIL: 11 passed, 0 failed, 0 inconclusive
+DETAIL: 6 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected b/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected
index 1408f7cb98..9eb18e44b5 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected
@@ -1,18 +1,10 @@
-test_multi_function.py(4, 44): ✅ pass - (create_config ensures) Return type constraint
-test_multi_function.py(9, 4): ✅ pass - ite_cond_calls_PNotIn_0
-test_multi_function.py(8, 47): ✅ pass - (validate_config ensures) Return type constraint
-test_multi_function.py(11, 4): ✅ pass - ite_cond_calls_PNotIn_0
-test_multi_function.py(16, 4): ✅ pass - (create_config requires) Type constraint of name
-test_multi_function.py(16, 4): ✅ pass - (create_config requires) Type constraint of value
+test_multi_function.py(16, 4): ✅ pass - (create_config requires) Type constraint of name, (create_config requires) Type constraint of value
 test_multi_function.py(17, 4): ✅ pass - (validate_config requires) Type constraint of config
 test_multi_function.py(17, 4): ✅ pass - assert(485)
 test_multi_function.py(18, 7): ✅ pass - Check PNot exception
-test_multi_function.py(20, 4): ❓ unknown - set_LaurelResult_calls_Any_get_0
-test_multi_function.py(23, 4): ✅ pass - (process_config requires) Type constraint of name
-test_multi_function.py(23, 4): ✅ pass - (process_config requires) Type constraint of value
+test_multi_function.py(20, 4): ❓ unknown - precondition
+test_multi_function.py(23, 4): ✅ pass - (process_config requires) Type constraint of name, (process_config requires) Type constraint of value
 test_multi_function.py(24, 4): ❓ unknown - process_config should return value
-test_multi_function.py(26, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_name_is_foo
-test_multi_function.py(26, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str
-test_multi_function.py(26, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar
-DETAIL: 14 passed, 0 failed, 2 inconclusive
+test_multi_function.py(26, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_name_is_foo, (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str, (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar
+DETAIL: 6 passed, 0 failed, 2 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_nested_calls.expected b/StrataTest/Languages/Python/expected_laurel/test_nested_calls.expected
index 0f4bb96d26..bc29103fab 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_nested_calls.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_nested_calls.expected
@@ -1,7 +1,5 @@
 test_nested_calls.py(2, 11): ✅ pass - Check PMul exception
-test_nested_calls.py(1, 22): ✅ pass - (double ensures) Return type constraint
 test_nested_calls.py(5, 11): ✅ pass - Check PAdd exception
-test_nested_calls.py(4, 23): ✅ pass - (add_one ensures) Return type constraint
 test_nested_calls.py(8, 4): ✅ pass - (double requires) Type constraint of x
 test_nested_calls.py(8, 4): ✅ pass - assert(107)
 test_nested_calls.py(9, 4): ✅ pass - (double requires) Type constraint of x
@@ -17,5 +15,5 @@ test_nested_calls.py(16, 4): ✅ pass - assert(309)
 test_nested_calls.py(17, 4): ✅ pass - (double requires) Type constraint of x
 test_nested_calls.py(17, 4): ✅ pass - assert(333)
 test_nested_calls.py(18, 4): ❓ unknown - double(add_one(4)) should be 10
-DETAIL: 16 passed, 0 failed, 3 inconclusive
+DETAIL: 14 passed, 0 failed, 3 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_nested_dict.expected b/StrataTest/Languages/Python/expected_laurel/test_nested_dict.expected
index df550fc4b1..28591de58c 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_nested_dict.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_nested_dict.expected
@@ -1,6 +1,3 @@
-test_nested_dict.py(3, 4): ✅ pass - assert_assert(48)_calls_Any_get_0
-test_nested_dict.py(3, 4): ✅ pass - assert_assert(48)_calls_Any_get_1
-test_nested_dict.py(3, 4): ✅ pass - assert_assert(48)_calls_Any_get_2
 test_nested_dict.py(3, 4): ✅ pass - nested dict
-DETAIL: 4 passed, 0 failed, 0 inconclusive
+DETAIL: 1 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_nested_list.expected b/StrataTest/Languages/Python/expected_laurel/test_nested_list.expected
index 9920d7a1ef..60ce4e55cb 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_nested_list.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_nested_list.expected
@@ -1,8 +1,4 @@
-test_nested_list.py(3, 4): ✅ pass - assert_assert(54)_calls_Any_get_0
-test_nested_list.py(3, 4): ✅ pass - assert_assert(54)_calls_Any_get_1
 test_nested_list.py(3, 4): ✅ pass - nested access 0,0
-test_nested_list.py(4, 4): ✅ pass - assert_assert(100)_calls_Any_get_0
-test_nested_list.py(4, 4): ✅ pass - assert_assert(100)_calls_Any_get_1
 test_nested_list.py(4, 4): ✅ pass - nested access 1,1
-DETAIL: 6 passed, 0 failed, 0 inconclusive
+DETAIL: 2 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_nested_optional.expected b/StrataTest/Languages/Python/expected_laurel/test_nested_optional.expected
index e32ca89fd6..d687e3d9e8 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_nested_optional.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_nested_optional.expected
@@ -1,4 +1,3 @@
-test_nested_optional.py(5, 4): ✅ pass - assert_assert(90)_calls_Any_get_0
 test_nested_optional.py(5, 4): ✅ pass - nested optional list
-DETAIL: 2 passed, 0 failed, 0 inconclusive
+DETAIL: 1 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_none_in_list.expected b/StrataTest/Languages/Python/expected_laurel/test_none_in_list.expected
index 11f44bb821..a4af287ee6 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_none_in_list.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_none_in_list.expected
@@ -1,4 +1,3 @@
-test_none_in_list.py(3, 4): ✅ pass - assert_assert(38)_calls_Any_get_0
 test_none_in_list.py(3, 4): ✅ pass - None in list
-DETAIL: 2 passed, 0 failed, 0 inconclusive
+DETAIL: 1 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_param_reassign.expected b/StrataTest/Languages/Python/expected_laurel/test_param_reassign.expected
index 57dfaf7a9e..286d5bc701 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_param_reassign.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_param_reassign.expected
@@ -1,33 +1,25 @@
 test_param_reassign.py(2, 8): ✅ pass - Check PAdd exception
-test_param_reassign.py(1, 37): ✅ pass - (single_param_reassign ensures) Return type constraint
 test_param_reassign.py(6, 8): ✅ pass - Check PAdd exception
 test_param_reassign.py(7, 8): ✅ pass - Check PMul exception
 test_param_reassign.py(8, 11): ✅ pass - Check PAdd exception
-test_param_reassign.py(5, 44): ✅ pass - (multi_param_reassign ensures) Return type constraint
 test_param_reassign.py(11, 11): ✅ pass - Check PAdd exception
-test_param_reassign.py(10, 41): ✅ pass - (no_param_reassign ensures) Return type constraint
 test_param_reassign.py(14, 8): ✅ pass - Check PAdd exception
-test_param_reassign.py(13, 46): ✅ pass - (partial_param_reassign ensures) Return type constraint
 test_param_reassign.py(18, 8): ✅ pass - Check PAdd exception
 test_param_reassign.py(19, 8): ✅ pass - Check PMul exception
-test_param_reassign.py(17, 36): ✅ pass - (param_reassign_twice ensures) Return type constraint
 test_param_reassign.py(23, 4): ✅ pass - (single_param_reassign requires) Type constraint of x
 test_param_reassign.py(23, 4): ✅ pass - assert(422)
 test_param_reassign.py(24, 4): ❓ unknown - single reassign
-test_param_reassign.py(26, 4): ✅ pass - (multi_param_reassign requires) Type constraint of a
-test_param_reassign.py(26, 4): ✅ pass - (multi_param_reassign requires) Type constraint of b
+test_param_reassign.py(26, 4): ✅ pass - (multi_param_reassign requires) Type constraint of a, (multi_param_reassign requires) Type constraint of b
 test_param_reassign.py(26, 4): ✅ pass - assert(500)
 test_param_reassign.py(27, 4): ❓ unknown - multi reassign
-test_param_reassign.py(29, 4): ✅ pass - (no_param_reassign requires) Type constraint of x
-test_param_reassign.py(29, 4): ✅ pass - (no_param_reassign requires) Type constraint of y
+test_param_reassign.py(29, 4): ✅ pass - (no_param_reassign requires) Type constraint of x, (no_param_reassign requires) Type constraint of y
 test_param_reassign.py(29, 4): ✅ pass - assert(580)
 test_param_reassign.py(30, 4): ❓ unknown - no reassign
-test_param_reassign.py(32, 4): ✅ pass - (partial_param_reassign requires) Type constraint of x
-test_param_reassign.py(32, 4): ✅ pass - (partial_param_reassign requires) Type constraint of y
+test_param_reassign.py(32, 4): ✅ pass - (partial_param_reassign requires) Type constraint of x, (partial_param_reassign requires) Type constraint of y
 test_param_reassign.py(32, 4): ✅ pass - assert(653)
 test_param_reassign.py(33, 4): ❓ unknown - partial reassign
 test_param_reassign.py(35, 4): ✅ pass - (param_reassign_twice requires) Type constraint of x
 test_param_reassign.py(35, 4): ✅ pass - assert(738)
 test_param_reassign.py(36, 4): ❓ unknown - reassign twice
-DETAIL: 26 passed, 0 failed, 5 inconclusive
+DETAIL: 18 passed, 0 failed, 5 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_param_reassign_kwargs.expected b/StrataTest/Languages/Python/expected_laurel/test_param_reassign_kwargs.expected
index 330fc8092f..996c36bc2f 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_param_reassign_kwargs.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_param_reassign_kwargs.expected
@@ -1,8 +1,6 @@
 test_param_reassign_kwargs.py(2, 11): ✅ pass - Check PAdd exception
-test_param_reassign_kwargs.py(1, 59): ✅ pass - (greet ensures) Return type constraint
-test_param_reassign_kwargs.py(6, 4): ✅ pass - (greet requires) Type constraint of name
-test_param_reassign_kwargs.py(6, 4): ✅ pass - (greet requires) Type constraint of greeting
+test_param_reassign_kwargs.py(6, 4): ✅ pass - (greet requires) Type constraint of name, (greet requires) Type constraint of greeting
 test_param_reassign_kwargs.py(6, 4): ✅ pass - assert(137)
 test_param_reassign_kwargs.py(7, 4): ❓ unknown - kwargs call
-DETAIL: 5 passed, 0 failed, 1 inconclusive
+DETAIL: 3 passed, 0 failed, 1 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_pin_any.expected b/StrataTest/Languages/Python/expected_laurel/test_pin_any.expected
index 8088956821..e32e5bd379 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_pin_any.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_pin_any.expected
@@ -1,5 +1,4 @@
-test_pin_any.py(4, 8): ❓ unknown - assert_assert(124)_calls_PIn_0
 test_pin_any.py(4, 8): ❓ unknown - key could be in results
 test_pin_any.py(2, 36): ✔️ always true if reached - (test_in_on_any ensures) Return type constraint
-DETAIL: 1 passed, 0 failed, 2 inconclusive
+DETAIL: 1 passed, 0 failed, 1 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_precondition_verification.expected b/StrataTest/Languages/Python/expected_laurel/test_precondition_verification.expected
index 30acce18e1..97ff1a49a1 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_precondition_verification.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_precondition_verification.expected
@@ -1,14 +1,6 @@
-test_precondition_verification.py(8, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_name_is_foo
-test_precondition_verification.py(8, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str
-test_precondition_verification.py(8, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar
-test_precondition_verification.py(11, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_name_is_foo
-test_precondition_verification.py(11, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str
-test_precondition_verification.py(11, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar
-test_precondition_verification.py(14, 4): ❓ unknown - (Origin_test_helper_procedure_Requires)req_name_is_foo
-test_precondition_verification.py(14, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str
-test_precondition_verification.py(14, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar
-test_precondition_verification.py(17, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_name_is_foo
-test_precondition_verification.py(17, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str
-test_precondition_verification.py(17, 4): ❓ unknown - (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar
-DETAIL: 10 passed, 0 failed, 2 inconclusive
+test_precondition_verification.py(8, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_name_is_foo, (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str, (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar
+test_precondition_verification.py(11, 4): ✅ pass - (Origin_test_helper_procedure_Requires)req_name_is_foo, (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str, (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar
+test_precondition_verification.py(14, 4): ❓ unknown - (Origin_test_helper_procedure_Requires)req_name_is_foo, (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str, (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar
+test_precondition_verification.py(17, 4): ❓ unknown - (Origin_test_helper_procedure_Requires)req_name_is_foo, (Origin_test_helper_procedure_Requires)req_opt_name_none_or_str, (Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar
+DETAIL: 2 passed, 0 failed, 2 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_procedure_in_assert.expected b/StrataTest/Languages/Python/expected_laurel/test_procedure_in_assert.expected
new file mode 100644
index 0000000000..3c6575c742
--- /dev/null
+++ b/StrataTest/Languages/Python/expected_laurel/test_procedure_in_assert.expected
@@ -0,0 +1,6 @@
+test_procedure_in_assert.py(8, 4): ✅ pass - assert(311)
+test_procedure_in_assert.py(9, 4): ✅ pass - (Origin_timedelta_Requires), (Origin_timedelta_Requires)hours_type, (Origin_timedelta_Requires)days_pos, (Origin_timedelta_Requires)hours_pos
+test_procedure_in_assert.py(10, 4): ✅ pass - assert(361)
+test_procedure_in_assert.py(11, 4): ✅ pass - should pass
+DETAIL: 4 passed, 0 failed, 0 inconclusive
+RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_regex_negative.expected b/StrataTest/Languages/Python/expected_laurel/test_regex_negative.expected
index 2d85b2d64a..ffc6566e42 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_regex_negative.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_regex_negative.expected
@@ -1,51 +1,51 @@
-test_regex_negative.py(9, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_negative.py(9, 4): ✅ pass - precondition
 test_regex_negative.py(10, 4): ❓ unknown - EXPECTED_FAIL: fullmatch a on b
-test_regex_negative.py(12, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_negative.py(12, 4): ✅ pass - precondition
 test_regex_negative.py(13, 4): ❓ unknown - EXPECTED_FAIL: fullmatch abc on abd
-test_regex_negative.py(15, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_negative.py(15, 4): ✅ pass - precondition
 test_regex_negative.py(16, 4): ❓ unknown - EXPECTED_FAIL: fullmatch [a-z]+ on ABC
-test_regex_negative.py(19, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_negative.py(19, 4): ✅ pass - precondition
 test_regex_negative.py(20, 4): ❓ unknown - EXPECTED_FAIL: fullmatch ^abc$ on abcd
-test_regex_negative.py(22, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_negative.py(22, 4): ✅ pass - precondition
 test_regex_negative.py(23, 4): ❓ unknown - EXPECTED_FAIL: search ^abc in xabc
-test_regex_negative.py(25, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_negative.py(25, 4): ✅ pass - precondition
 test_regex_negative.py(26, 4): ❓ unknown - EXPECTED_FAIL: search abc$ in abcx
-test_regex_negative.py(28, 4): ✅ pass - set_m_calls_re_match_0
+test_regex_negative.py(28, 4): ✅ pass - precondition
 test_regex_negative.py(29, 4): ❓ unknown - EXPECTED_FAIL: match ^a$ in ab
-test_regex_negative.py(32, 4): ✅ pass - set_p_calls_re_compile_0
-test_regex_negative.py(33, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_negative.py(32, 4): ✅ pass - precondition
+test_regex_negative.py(33, 4): ✅ pass - precondition
 test_regex_negative.py(34, 4): ❓ unknown - EXPECTED_FAIL: compiled ^abc$ search xabc
-test_regex_negative.py(36, 4): ✅ pass - set_m_calls_re_match_0
+test_regex_negative.py(36, 4): ✅ pass - precondition
 test_regex_negative.py(37, 4): ❓ unknown - EXPECTED_FAIL: compiled ^abc$ match abcx
-test_regex_negative.py(44, 8): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_negative.py(44, 8): ✅ pass - precondition
 test_regex_negative.py(47, 4): ❓ unknown - malformed: unmatched paren should raise
-test_regex_negative.py(51, 8): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_negative.py(51, 8): ✅ pass - precondition
 test_regex_negative.py(54, 4): ❓ unknown - malformed: nothing to repeat should raise
-test_regex_negative.py(58, 8): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_negative.py(58, 8): ✅ pass - precondition
 test_regex_negative.py(61, 4): ❓ unknown - malformed: bad bounds should raise
-test_regex_negative.py(65, 8): ✅ pass - set_m_calls_re_search_0
+test_regex_negative.py(65, 8): ✅ pass - precondition
 test_regex_negative.py(68, 4): ❓ unknown - malformed: search with bad pattern should raise
-test_regex_negative.py(72, 8): ✅ pass - set_m_calls_re_match_0
+test_regex_negative.py(72, 8): ✅ pass - precondition
 test_regex_negative.py(75, 4): ❓ unknown - malformed: match with bad pattern should raise
-test_regex_negative.py(83, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_negative.py(83, 4): ✅ pass - precondition
 test_regex_negative.py(84, 4): ❓ unknown - unsupported: search \S+ should match non-empty non-whitespace
-test_regex_negative.py(86, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_negative.py(86, 4): ✅ pass - precondition
 test_regex_negative.py(87, 4): ❓ unknown - unsupported: fullmatch \d+ on digit string
-test_regex_negative.py(89, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_negative.py(89, 4): ✅ pass - precondition
 test_regex_negative.py(90, 4): ❓ unknown - unsupported: fullmatch \w+ on word string
-test_regex_negative.py(92, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_negative.py(92, 4): ✅ pass - precondition
 test_regex_negative.py(93, 4): ❓ unknown - unsupported: search \s+ finds whitespace
-test_regex_negative.py(96, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_negative.py(96, 4): ✅ pass - precondition
 test_regex_negative.py(97, 4): ❓ unknown - unsupported: fullmatch [a-z\d]+ on alphanumeric
-test_regex_negative.py(99, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_negative.py(99, 4): ✅ pass - precondition
 test_regex_negative.py(100, 4): ❓ unknown - unsupported: fullmatch [\w\-]+ on word with dash
-test_regex_negative.py(103, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_negative.py(103, 4): ✅ pass - precondition
 test_regex_negative.py(104, 4): ❓ unknown - unsupported: search \t+ on tab string
-test_regex_negative.py(106, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_negative.py(106, 4): ✅ pass - precondition
 test_regex_negative.py(107, 4): ❓ unknown - unsupported: fullmatch [^\n]+ on non-newline string
-test_regex_negative.py(110, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_negative.py(110, 4): ✅ pass - precondition
 test_regex_negative.py(111, 4): ❓ unknown - unsupported: non-greedy .*? quantifier
-test_regex_negative.py(113, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_negative.py(113, 4): ✅ pass - precondition
 test_regex_negative.py(114, 4): ❓ unknown - unsupported: positive lookahead (?=foo)
 DETAIL: 25 passed, 0 failed, 24 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_regex_positive.expected b/StrataTest/Languages/Python/expected_laurel/test_regex_positive.expected
index 58993070b1..bdafa7fb98 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_regex_positive.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_regex_positive.expected
@@ -1,284 +1,284 @@
-test_regex_positive.py(7, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(7, 4): ✅ pass - precondition
 test_regex_positive.py(8, 4): ✅ pass - fullmatch literal should match
-test_regex_positive.py(10, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(10, 4): ✅ pass - precondition
 test_regex_positive.py(11, 4): ✅ pass - fullmatch literal should reject extra chars
-test_regex_positive.py(14, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(14, 4): ✅ pass - precondition
 test_regex_positive.py(15, 4): ✅ pass - fullmatch char class should match
-test_regex_positive.py(17, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(17, 4): ✅ pass - precondition
 test_regex_positive.py(18, 4): ✅ pass - fullmatch char class should reject uppercase
-test_regex_positive.py(21, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(21, 4): ✅ pass - precondition
 test_regex_positive.py(22, 4): ✅ pass - fullmatch negated class should match non-digits
-test_regex_positive.py(24, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(24, 4): ✅ pass - precondition
 test_regex_positive.py(25, 4): ✅ pass - fullmatch negated class should reject digits
-test_regex_positive.py(28, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(28, 4): ✅ pass - precondition
 test_regex_positive.py(29, 4): ✅ pass - fullmatch dot-plus should match non-empty
-test_regex_positive.py(31, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(31, 4): ✅ pass - precondition
 test_regex_positive.py(32, 4): ✅ pass - fullmatch single dot should reject two chars
-test_regex_positive.py(35, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(35, 4): ✅ pass - precondition
 test_regex_positive.py(36, 4): ✅ pass - fullmatch a* should match empty
-test_regex_positive.py(38, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(38, 4): ✅ pass - precondition
 test_regex_positive.py(39, 4): ✅ pass - fullmatch a* should match repeated
-test_regex_positive.py(41, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(41, 4): ✅ pass - precondition
 test_regex_positive.py(42, 4): ✅ pass - fullmatch a* should reject non-a
-test_regex_positive.py(45, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(45, 4): ✅ pass - precondition
 test_regex_positive.py(46, 4): ✅ pass - fullmatch a+ should reject empty
-test_regex_positive.py(48, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(48, 4): ✅ pass - precondition
 test_regex_positive.py(49, 4): ✅ pass - fullmatch a+ should match one-or-more
-test_regex_positive.py(52, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(52, 4): ✅ pass - precondition
 test_regex_positive.py(53, 4): ✅ pass - fullmatch ab?c should match without b
-test_regex_positive.py(55, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(55, 4): ✅ pass - precondition
 test_regex_positive.py(56, 4): ✅ pass - fullmatch ab?c should match with b
-test_regex_positive.py(58, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(58, 4): ✅ pass - precondition
 test_regex_positive.py(59, 4): ✅ pass - fullmatch ab?c should reject two b's
-test_regex_positive.py(62, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(62, 4): ✅ pass - precondition
 test_regex_positive.py(63, 4): ✅ pass - fullmatch alternation should match first
-test_regex_positive.py(65, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(65, 4): ✅ pass - precondition
 test_regex_positive.py(66, 4): ✅ pass - fullmatch alternation should match second
-test_regex_positive.py(68, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(68, 4): ✅ pass - precondition
 test_regex_positive.py(69, 4): ✅ pass - fullmatch alternation should reject other
-test_regex_positive.py(72, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(72, 4): ✅ pass - precondition
 test_regex_positive.py(73, 4): ✅ pass - fullmatch concat should match
-test_regex_positive.py(75, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(75, 4): ✅ pass - precondition
 test_regex_positive.py(76, 4): ✅ pass - fullmatch concat should reject wrong order
-test_regex_positive.py(80, 4): ✅ pass - set_m_calls_re_match_0
+test_regex_positive.py(80, 4): ✅ pass - precondition
 test_regex_positive.py(81, 4): ✅ pass - match should match at start
-test_regex_positive.py(83, 4): ✅ pass - set_m_calls_re_match_0
+test_regex_positive.py(83, 4): ✅ pass - precondition
 test_regex_positive.py(84, 4): ✅ pass - match should reject when not at start
-test_regex_positive.py(86, 4): ✅ pass - set_m_calls_re_match_0
+test_regex_positive.py(86, 4): ✅ pass - precondition
 test_regex_positive.py(87, 4): ✅ pass - match should match prefix
-test_regex_positive.py(89, 4): ✅ pass - set_m_calls_re_match_0
+test_regex_positive.py(89, 4): ✅ pass - precondition
 test_regex_positive.py(90, 4): ✅ pass - match should reject non-prefix
-test_regex_positive.py(94, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(94, 4): ✅ pass - precondition
 test_regex_positive.py(95, 4): ✅ pass - search should find digits in middle
-test_regex_positive.py(97, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(97, 4): ✅ pass - precondition
 test_regex_positive.py(98, 4): ✅ pass - search should reject when no digits
-test_regex_positive.py(100, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(100, 4): ✅ pass - precondition
 test_regex_positive.py(101, 4): ✅ pass - search should find substring
-test_regex_positive.py(103, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(103, 4): ✅ pass - precondition
 test_regex_positive.py(104, 4): ✅ pass - search should reject missing substring
-test_regex_positive.py(108, 4): ✅ pass - set_p_calls_re_compile_0
-test_regex_positive.py(110, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(108, 4): ✅ pass - precondition
+test_regex_positive.py(110, 4): ✅ pass - precondition
 test_regex_positive.py(111, 4): ✅ pass - compiled fullmatch should match
-test_regex_positive.py(113, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(113, 4): ✅ pass - precondition
 test_regex_positive.py(114, 4): ✅ pass - compiled fullmatch should reject uppercase
-test_regex_positive.py(116, 4): ✅ pass - set_m_calls_re_match_0
+test_regex_positive.py(116, 4): ✅ pass - precondition
 test_regex_positive.py(117, 4): ✅ pass - compiled match should match prefix
-test_regex_positive.py(119, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(119, 4): ✅ pass - precondition
 test_regex_positive.py(120, 4): ✅ pass - compiled search should find in middle
-test_regex_positive.py(125, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(125, 4): ✅ pass - precondition
 test_regex_positive.py(126, 4): ✅ pass - fullmatch empty pattern on empty string
-test_regex_positive.py(128, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(128, 4): ✅ pass - precondition
 test_regex_positive.py(129, 4): ✅ pass - fullmatch empty pattern on non-empty string
-test_regex_positive.py(132, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(132, 4): ✅ pass - precondition
 test_regex_positive.py(133, 4): ✅ pass - fullmatch single char
-test_regex_positive.py(135, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(135, 4): ✅ pass - precondition
 test_regex_positive.py(136, 4): ✅ pass - fullmatch single char mismatch
-test_regex_positive.py(139, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(139, 4): ✅ pass - precondition
 test_regex_positive.py(140, 4): ✅ pass - fullmatch nested group-plus
-test_regex_positive.py(142, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(142, 4): ✅ pass - precondition
 test_regex_positive.py(143, 4): ✅ pass - fullmatch nested group-plus mismatch
-test_regex_positive.py(146, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(146, 4): ✅ pass - precondition
 test_regex_positive.py(147, 4): ✅ pass - fullmatch loop min
-test_regex_positive.py(149, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(149, 4): ✅ pass - precondition
 test_regex_positive.py(150, 4): ✅ pass - fullmatch loop max
-test_regex_positive.py(152, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(152, 4): ✅ pass - precondition
 test_regex_positive.py(153, 4): ✅ pass - fullmatch loop below min
-test_regex_positive.py(155, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(155, 4): ✅ pass - precondition
 test_regex_positive.py(156, 4): ✅ pass - fullmatch loop above max
-test_regex_positive.py(159, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(159, 4): ✅ pass - precondition
 test_regex_positive.py(160, 4): ✅ pass - fullmatch group loop match
-test_regex_positive.py(162, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(162, 4): ✅ pass - precondition
 test_regex_positive.py(163, 4): ✅ pass - fullmatch group loop too few
-test_regex_positive.py(165, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(165, 4): ✅ pass - precondition
 test_regex_positive.py(166, 4): ✅ pass - fullmatch group loop 3 reps
-test_regex_positive.py(168, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(168, 4): ✅ pass - precondition
 test_regex_positive.py(169, 4): ✅ pass - fullmatch group loop 1 rep
-test_regex_positive.py(174, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(174, 4): ✅ pass - precondition
 test_regex_positive.py(175, 4): ✅ pass - fullmatch ^a match
-test_regex_positive.py(177, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(177, 4): ✅ pass - precondition
 test_regex_positive.py(178, 4): ✅ pass - fullmatch ^a reject
-test_regex_positive.py(180, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(180, 4): ✅ pass - precondition
 test_regex_positive.py(181, 4): ✅ pass - fullmatch a$ match
-test_regex_positive.py(183, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(183, 4): ✅ pass - precondition
 test_regex_positive.py(184, 4): ✅ pass - fullmatch a$ reject
-test_regex_positive.py(186, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(186, 4): ✅ pass - precondition
 test_regex_positive.py(187, 4): ✅ pass - fullmatch ^a$ match
-test_regex_positive.py(189, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(189, 4): ✅ pass - precondition
 test_regex_positive.py(190, 4): ✅ pass - fullmatch ^a$ reject trailing
-test_regex_positive.py(192, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(192, 4): ✅ pass - precondition
 test_regex_positive.py(193, 4): ✅ pass - fullmatch ^a$ reject leading
-test_regex_positive.py(196, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(196, 4): ✅ pass - precondition
 test_regex_positive.py(197, 4): ✅ pass - fullmatch ^$ on empty
-test_regex_positive.py(199, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(199, 4): ✅ pass - precondition
 test_regex_positive.py(200, 4): ✅ pass - fullmatch ^$ on non-empty
-test_regex_positive.py(202, 4): ✅ pass - set_m_calls_re_match_0
+test_regex_positive.py(202, 4): ✅ pass - precondition
 test_regex_positive.py(203, 4): ✅ pass - match ^$ on empty
-test_regex_positive.py(205, 4): ✅ pass - set_m_calls_re_match_0
+test_regex_positive.py(205, 4): ✅ pass - precondition
 test_regex_positive.py(206, 4): ✅ pass - match ^$ on non-empty
-test_regex_positive.py(208, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(208, 4): ✅ pass - precondition
 test_regex_positive.py(209, 4): ✅ pass - search ^$ on empty
-test_regex_positive.py(211, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(211, 4): ✅ pass - precondition
 test_regex_positive.py(212, 4): ✅ pass - search ^$ on non-empty
-test_regex_positive.py(217, 4): ✅ pass - set_m_calls_re_match_0
+test_regex_positive.py(217, 4): ✅ pass - precondition
 test_regex_positive.py(218, 4): ✅ pass - match ^a
-test_regex_positive.py(220, 4): ✅ pass - set_m_calls_re_match_0
+test_regex_positive.py(220, 4): ✅ pass - precondition
 test_regex_positive.py(221, 4): ✅ pass - match ^a trailing ok
-test_regex_positive.py(223, 4): ✅ pass - set_m_calls_re_match_0
+test_regex_positive.py(223, 4): ✅ pass - precondition
 test_regex_positive.py(224, 4): ✅ pass - match ^a reject
-test_regex_positive.py(227, 4): ✅ pass - set_m_calls_re_match_0
+test_regex_positive.py(227, 4): ✅ pass - precondition
 test_regex_positive.py(228, 4): ✅ pass - match ^a$ exact
-test_regex_positive.py(230, 4): ✅ pass - set_m_calls_re_match_0
+test_regex_positive.py(230, 4): ✅ pass - precondition
 test_regex_positive.py(231, 4): ✅ pass - match ^a$ reject trailing
-test_regex_positive.py(233, 4): ✅ pass - set_m_calls_re_match_0
+test_regex_positive.py(233, 4): ✅ pass - precondition
 test_regex_positive.py(234, 4): ✅ pass - match a$ exact
-test_regex_positive.py(236, 4): ✅ pass - set_m_calls_re_match_0
+test_regex_positive.py(236, 4): ✅ pass - precondition
 test_regex_positive.py(237, 4): ✅ pass - match a$ reject trailing
-test_regex_positive.py(239, 4): ✅ pass - set_m_calls_re_match_0
+test_regex_positive.py(239, 4): ✅ pass - precondition
 test_regex_positive.py(240, 4): ✅ pass - match a.*$ accepts
-test_regex_positive.py(242, 4): ✅ pass - set_m_calls_re_match_0
+test_regex_positive.py(242, 4): ✅ pass - precondition
 test_regex_positive.py(243, 4): ✅ pass - match a.*$ rejects
-test_regex_positive.py(248, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(248, 4): ✅ pass - precondition
 test_regex_positive.py(249, 4): ✅ pass - search a in middle
-test_regex_positive.py(251, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(251, 4): ✅ pass - precondition
 test_regex_positive.py(252, 4): ✅ pass - search a not found
-test_regex_positive.py(255, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(255, 4): ✅ pass - precondition
 test_regex_positive.py(256, 4): ✅ pass - search ^a at start
-test_regex_positive.py(258, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(258, 4): ✅ pass - precondition
 test_regex_positive.py(259, 4): ✅ pass - search ^a reject non-start
-test_regex_positive.py(261, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(261, 4): ✅ pass - precondition
 test_regex_positive.py(262, 4): ✅ pass - search ^a exact
-test_regex_positive.py(265, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(265, 4): ✅ pass - precondition
 test_regex_positive.py(266, 4): ✅ pass - search a$ at end
-test_regex_positive.py(268, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(268, 4): ✅ pass - precondition
 test_regex_positive.py(269, 4): ✅ pass - search a$ reject non-end
-test_regex_positive.py(271, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(271, 4): ✅ pass - precondition
 test_regex_positive.py(272, 4): ✅ pass - search a$ deep end
-test_regex_positive.py(274, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(274, 4): ✅ pass - precondition
 test_regex_positive.py(275, 4): ✅ pass - search a$ reject trailing
-test_regex_positive.py(278, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(278, 4): ✅ pass - precondition
 test_regex_positive.py(279, 4): ✅ pass - search ^a$ exact
-test_regex_positive.py(281, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(281, 4): ✅ pass - precondition
 test_regex_positive.py(282, 4): ✅ pass - search ^a$ reject prefix
-test_regex_positive.py(284, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(284, 4): ✅ pass - precondition
 test_regex_positive.py(285, 4): ✅ pass - search ^a$ reject suffix
-test_regex_positive.py(289, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(289, 4): ✅ pass - precondition
 test_regex_positive.py(290, 4): ✅ pass - search ^abc at start
-test_regex_positive.py(292, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(292, 4): ✅ pass - precondition
 test_regex_positive.py(293, 4): ✅ pass - search ^abc reject non-start
-test_regex_positive.py(295, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(295, 4): ✅ pass - precondition
 test_regex_positive.py(296, 4): ✅ pass - search abc$ at end
-test_regex_positive.py(298, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(298, 4): ✅ pass - precondition
 test_regex_positive.py(299, 4): ✅ pass - search abc$ reject non-end
-test_regex_positive.py(301, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(301, 4): ✅ pass - precondition
 test_regex_positive.py(302, 4): ✅ pass - search ^abc$ exact
-test_regex_positive.py(304, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(304, 4): ✅ pass - precondition
 test_regex_positive.py(305, 4): ✅ pass - search ^abc$ reject prefix
-test_regex_positive.py(307, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(307, 4): ✅ pass - precondition
 test_regex_positive.py(308, 4): ✅ pass - search ^abc$ reject suffix
-test_regex_positive.py(312, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(312, 4): ✅ pass - precondition
 test_regex_positive.py(313, 4): ✅ pass - fullmatch ^a{3}$ match
-test_regex_positive.py(315, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(315, 4): ✅ pass - precondition
 test_regex_positive.py(316, 4): ✅ pass - fullmatch ^a{3}$ too few
-test_regex_positive.py(318, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(318, 4): ✅ pass - precondition
 test_regex_positive.py(319, 4): ✅ pass - fullmatch ^a{3}$ too many
-test_regex_positive.py(321, 4): ✅ pass - set_m_calls_re_match_0
+test_regex_positive.py(321, 4): ✅ pass - precondition
 test_regex_positive.py(322, 4): ✅ pass - match ^a{3}$ exact
-test_regex_positive.py(324, 4): ✅ pass - set_m_calls_re_match_0
+test_regex_positive.py(324, 4): ✅ pass - precondition
 test_regex_positive.py(325, 4): ✅ pass - match ^a{3}$ reject trailing
-test_regex_positive.py(327, 4): ✅ pass - set_m_calls_re_match_0
+test_regex_positive.py(327, 4): ✅ pass - precondition
 test_regex_positive.py(328, 4): ✅ pass - match a{3} trailing ok
-test_regex_positive.py(332, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(332, 4): ✅ pass - precondition
 test_regex_positive.py(333, 4): ✅ pass - escaped dot matches literal
-test_regex_positive.py(335, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(335, 4): ✅ pass - precondition
 test_regex_positive.py(336, 4): ✅ pass - escaped dot rejects non-dot
-test_regex_positive.py(338, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(338, 4): ✅ pass - precondition
 test_regex_positive.py(339, 4): ✅ pass - escaped plus matches literal
-test_regex_positive.py(341, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(341, 4): ✅ pass - precondition
 test_regex_positive.py(342, 4): ✅ pass - escaped plus rejects
-test_regex_positive.py(344, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(344, 4): ✅ pass - precondition
 test_regex_positive.py(345, 4): ✅ pass - escaped star matches literal
-test_regex_positive.py(347, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(347, 4): ✅ pass - precondition
 test_regex_positive.py(348, 4): ✅ pass - escaped star rejects
-test_regex_positive.py(350, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(350, 4): ✅ pass - precondition
 test_regex_positive.py(351, 4): ✅ pass - escaped question matches literal
-test_regex_positive.py(353, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(353, 4): ✅ pass - precondition
 test_regex_positive.py(354, 4): ✅ pass - escaped question rejects
-test_regex_positive.py(356, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(356, 4): ✅ pass - precondition
 test_regex_positive.py(357, 4): ✅ pass - escaped parens match literal
-test_regex_positive.py(359, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(359, 4): ✅ pass - precondition
 test_regex_positive.py(360, 4): ✅ pass - escaped parens reject
-test_regex_positive.py(362, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(362, 4): ✅ pass - precondition
 test_regex_positive.py(363, 4): ✅ pass - escaped backslash matches literal
-test_regex_positive.py(365, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(365, 4): ✅ pass - precondition
 test_regex_positive.py(366, 4): ✅ pass - escaped backslash rejects
-test_regex_positive.py(369, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(369, 4): ✅ pass - precondition
 test_regex_positive.py(370, 4): ✅ pass - search escaped dot
-test_regex_positive.py(372, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(372, 4): ✅ pass - precondition
 test_regex_positive.py(373, 4): ✅ pass - search escaped backslash
-test_regex_positive.py(375, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(375, 4): ✅ pass - precondition
 test_regex_positive.py(376, 4): ✅ pass - search escaped backslash reject
-test_regex_positive.py(380, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(380, 4): ✅ pass - precondition
 test_regex_positive.py(381, 4): ✅ pass - colon literal match
-test_regex_positive.py(383, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(383, 4): ✅ pass - precondition
 test_regex_positive.py(384, 4): ✅ pass - colon literal reject
-test_regex_positive.py(386, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(386, 4): ✅ pass - precondition
 test_regex_positive.py(387, 4): ✅ pass - colon class match
-test_regex_positive.py(389, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(389, 4): ✅ pass - precondition
 test_regex_positive.py(390, 4): ✅ pass - colon class reject
-test_regex_positive.py(392, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(392, 4): ✅ pass - precondition
 test_regex_positive.py(393, 4): ✅ pass - search colon class
-test_regex_positive.py(395, 4): ✅ pass - set_m_calls_re_match_0
+test_regex_positive.py(395, 4): ✅ pass - precondition
 test_regex_positive.py(396, 4): ✅ pass - match anchored colon
-test_regex_positive.py(398, 4): ✅ pass - set_m_calls_re_match_0
+test_regex_positive.py(398, 4): ✅ pass - precondition
 test_regex_positive.py(399, 4): ✅ pass - match anchored colon reject trailing
-test_regex_positive.py(403, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(403, 4): ✅ pass - precondition
 test_regex_positive.py(404, 4): ✅ pass - wildcard empty middle
-test_regex_positive.py(406, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(406, 4): ✅ pass - precondition
 test_regex_positive.py(407, 4): ✅ pass - wildcard non-empty middle
-test_regex_positive.py(409, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(409, 4): ✅ pass - precondition
 test_regex_positive.py(410, 4): ✅ pass - wildcard wrong ending
-test_regex_positive.py(412, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(412, 4): ✅ pass - precondition
 test_regex_positive.py(413, 4): ✅ pass - search wildcard
-test_regex_positive.py(416, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(416, 4): ✅ pass - precondition
 test_regex_positive.py(417, 4): ✅ pass - multi-char alt first
-test_regex_positive.py(419, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(419, 4): ✅ pass - precondition
 test_regex_positive.py(420, 4): ✅ pass - multi-char alt second
-test_regex_positive.py(422, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(422, 4): ✅ pass - precondition
 test_regex_positive.py(423, 4): ✅ pass - multi-char alt reject concat
-test_regex_positive.py(425, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(425, 4): ✅ pass - precondition
 test_regex_positive.py(426, 4): ✅ pass - search multi-char alt
-test_regex_positive.py(430, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(430, 4): ✅ pass - precondition
 test_regex_positive.py(431, 4): ✅ pass - fullmatch ^a|b$ first branch
-test_regex_positive.py(433, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(433, 4): ✅ pass - precondition
 test_regex_positive.py(434, 4): ✅ pass - fullmatch ^a|b$ second branch
-test_regex_positive.py(436, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(436, 4): ✅ pass - precondition
 test_regex_positive.py(437, 4): ✅ pass - fullmatch ^a|b$ reject
-test_regex_positive.py(439, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(439, 4): ✅ pass - precondition
 test_regex_positive.py(440, 4): ✅ pass - search ^a|b$ start anchor
-test_regex_positive.py(442, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(442, 4): ✅ pass - precondition
 test_regex_positive.py(443, 4): ✅ pass - search ^a|b$ end anchor
-test_regex_positive.py(445, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(445, 4): ✅ pass - precondition
 test_regex_positive.py(446, 4): ✅ pass - search ^a|b$ neither
-test_regex_positive.py(450, 4): ✅ pass - set_p_calls_re_compile_0
-test_regex_positive.py(452, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(450, 4): ✅ pass - precondition
+test_regex_positive.py(452, 4): ✅ pass - precondition
 test_regex_positive.py(453, 4): ✅ pass - compiled ^abc$ fullmatch
-test_regex_positive.py(455, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(455, 4): ✅ pass - precondition
 test_regex_positive.py(456, 4): ✅ pass - compiled ^abc$ search exact
-test_regex_positive.py(458, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(458, 4): ✅ pass - precondition
 test_regex_positive.py(459, 4): ✅ pass - compiled ^abc$ search reject prefix
-test_regex_positive.py(461, 4): ✅ pass - set_m_calls_re_match_0
+test_regex_positive.py(461, 4): ✅ pass - precondition
 test_regex_positive.py(462, 4): ✅ pass - compiled ^abc$ match exact
-test_regex_positive.py(464, 4): ✅ pass - set_m_calls_re_match_0
+test_regex_positive.py(464, 4): ✅ pass - precondition
 test_regex_positive.py(465, 4): ✅ pass - compiled ^abc$ match reject trailing
-test_regex_positive.py(472, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(472, 4): ✅ pass - precondition
 test_regex_positive.py(473, 4): ✅ pass - malformed: unmatched paren is exception, not None
-test_regex_positive.py(475, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(475, 4): ✅ pass - precondition
 test_regex_positive.py(476, 4): ✅ pass - malformed: nothing to repeat is exception, not None
-test_regex_positive.py(478, 4): ✅ pass - set_m_calls_re_fullmatch_0
+test_regex_positive.py(478, 4): ✅ pass - precondition
 test_regex_positive.py(479, 4): ✅ pass - malformed: bad bounds is exception, not None
-test_regex_positive.py(481, 4): ✅ pass - set_m_calls_re_search_0
+test_regex_positive.py(481, 4): ✅ pass - precondition
 test_regex_positive.py(482, 4): ✅ pass - malformed: search with bad pattern is exception, not None
-test_regex_positive.py(484, 4): ✅ pass - set_m_calls_re_match_0
+test_regex_positive.py(484, 4): ✅ pass - precondition
 test_regex_positive.py(485, 4): ✅ pass - malformed: match with bad pattern is exception, not None
 DETAIL: 282 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_return_types.expected b/StrataTest/Languages/Python/expected_laurel/test_return_types.expected
index ba027981f3..95def4a888 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_return_types.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_return_types.expected
@@ -1,20 +1,14 @@
-test_return_types.py(1, 20): ✅ pass - (get_number ensures) Return type constraint
-test_return_types.py(4, 22): ✅ pass - (get_greeting ensures) Return type constraint
-test_return_types.py(7, 18): ✅ pass - (get_flag ensures) Return type constraint
 test_return_types.py(11, 4): ✅ pass - assert(159)
-test_return_types.py(10, 21): ✅ pass - (get_nothing ensures) Return type constraint
 test_return_types.py(15, 18): ✅ pass - Check PAdd exception
 test_return_types.py(15, 4): ✅ pass - assert(223)
-test_return_types.py(14, 27): ✅ pass - (add ensures) Return type constraint
 test_return_types.py(19, 4): ✅ pass - assert(278)
 test_return_types.py(20, 4): ❓ unknown - get_number returned wrong value
 test_return_types.py(22, 4): ✅ pass - assert(359)
 test_return_types.py(23, 4): ❓ unknown - get_greeting returned wrong value
 test_return_types.py(25, 4): ✅ pass - assert(449)
 test_return_types.py(26, 4): ❓ unknown - get_flag returned wrong value
-test_return_types.py(28, 4): ✅ pass - (add requires) Type constraint of a
-test_return_types.py(28, 4): ✅ pass - (add requires) Type constraint of b
+test_return_types.py(28, 4): ✅ pass - (add requires) Type constraint of a, (add requires) Type constraint of b
 test_return_types.py(28, 4): ✅ pass - assert(529)
 test_return_types.py(29, 4): ❓ unknown - add returned wrong value
-DETAIL: 14 passed, 0 failed, 4 inconclusive
+DETAIL: 8 passed, 0 failed, 4 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_subscription.expected b/StrataTest/Languages/Python/expected_laurel/test_subscription.expected
index a2764b2a02..7e53afca0d 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_subscription.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_subscription.expected
@@ -1,16 +1,7 @@
 test_subscription.py(12, 0): ✅ pass - Check Any_sets! exception
 test_subscription.py(14, 0): ✅ pass - Check Any_sets! exception
-test_subscription.py(16, 0): ✅ pass - assert_assert(421)_calls_Any_get_0
-test_subscription.py(16, 0): ✅ pass - assert_assert(421)_calls_Any_get_1
-test_subscription.py(16, 0): ✅ pass - assert_assert(421)_calls_Any_get_2
-test_subscription.py(16, 0): ✅ pass - assert_assert(421)_calls_Any_get_3
 test_subscription.py(16, 0): ✅ pass - assert(421)
-test_subscription.py(18, 0): ✅ pass - assert_assert(489)_calls_Any_get_0
-test_subscription.py(18, 0): ✅ pass - assert_assert(489)_calls_Any_get_1
-test_subscription.py(18, 0): ✅ pass - assert_assert(489)_calls_Any_get_2
-test_subscription.py(18, 0): ✅ pass - assert_assert(489)_calls_PIn_3
 test_subscription.py(18, 0): ✅ pass - assert(489)
-test_subscription.py(20, 0): ✅ pass - assert_assert(554)_calls_PIn_0
 test_subscription.py(20, 0): ✅ pass - assert(554)
-DETAIL: 14 passed, 0 failed, 0 inconclusive
+DETAIL: 5 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_timedelta_expr.expected b/StrataTest/Languages/Python/expected_laurel/test_timedelta_expr.expected
index 270b1ae3c0..396109c554 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_timedelta_expr.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_timedelta_expr.expected
@@ -1,9 +1,6 @@
-test_timedelta_expr.py(4, 0): ✅ pass - (Origin_timedelta_Requires)
-test_timedelta_expr.py(4, 0): ✅ pass - (Origin_timedelta_Requires)hours_type
-test_timedelta_expr.py(4, 0): ✅ pass - (Origin_timedelta_Requires)days_pos
-test_timedelta_expr.py(4, 0): ✅ pass - (Origin_timedelta_Requires)hours_pos
+test_timedelta_expr.py(4, 0): ✅ pass - (Origin_timedelta_Requires), (Origin_timedelta_Requires)hours_type, (Origin_timedelta_Requires)days_pos, (Origin_timedelta_Requires)hours_pos
 test_timedelta_expr.py(5, 18): ✅ pass - Check PSub exception
 test_timedelta_expr.py(6, 7): ✅ pass - Check PLe exception
 test_timedelta_expr.py(6, 0): ✅ pass - assert(140)
-DETAIL: 7 passed, 0 failed, 0 inconclusive
+DETAIL: 4 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_tuple_create.expected b/StrataTest/Languages/Python/expected_laurel/test_tuple_create.expected
index eb841a55ce..a6dfe49f01 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_tuple_create.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_tuple_create.expected
@@ -1,6 +1,4 @@
-test_tuple_create.py(3, 4): ✅ pass - assert_assert(47)_calls_Any_get_0
 test_tuple_create.py(3, 4): ✅ pass - tuple first
-test_tuple_create.py(4, 4): ✅ pass - assert_assert(83)_calls_Any_get_0
 test_tuple_create.py(4, 4): ✅ pass - tuple last
-DETAIL: 4 passed, 0 failed, 0 inconclusive
+DETAIL: 2 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_tuple_swap.expected b/StrataTest/Languages/Python/expected_laurel/test_tuple_swap.expected
index bce7234e3f..10317bc474 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_tuple_swap.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_tuple_swap.expected
@@ -1,8 +1,7 @@
 test_tuple_swap.py(2, 4): ✅ pass - assert(27)
 test_tuple_swap.py(3, 4): ✅ pass - assert(42)
-test_tuple_swap.py(4, 4): ✅ pass - set_a_calls_Any_get_0
-test_tuple_swap.py(4, 4): ✅ pass - set_b_calls_Any_get_0
+test_tuple_swap.py(4, 4): ✅ pass - precondition
 test_tuple_swap.py(5, 11): ✅ pass - Check PAnd exception
 test_tuple_swap.py(5, 4): ✅ pass - tuple swap
-DETAIL: 6 passed, 0 failed, 0 inconclusive
+DETAIL: 5 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_tuple_type.expected b/StrataTest/Languages/Python/expected_laurel/test_tuple_type.expected
index 211a0b9df0..8ac41bf5ea 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_tuple_type.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_tuple_type.expected
@@ -1,4 +1,3 @@
-test_tuple_type.py(5, 4): ✅ pass - assert_assert(80)_calls_Any_get_0
 test_tuple_type.py(5, 4): ✅ pass - typed tuple
-DETAIL: 2 passed, 0 failed, 0 inconclusive
+DETAIL: 1 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_tuple_unpack.expected b/StrataTest/Languages/Python/expected_laurel/test_tuple_unpack.expected
index 2e58c8bb13..5a47e1ae13 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_tuple_unpack.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_tuple_unpack.expected
@@ -1,6 +1,5 @@
-test_tuple_unpack.py(3, 4): ✅ pass - set_a_calls_Any_get_0
-test_tuple_unpack.py(3, 4): ✅ pass - set_b_calls_Any_get_0
+test_tuple_unpack.py(3, 4): ✅ pass - precondition
 test_tuple_unpack.py(4, 4): ✅ pass - unpack first
 test_tuple_unpack.py(5, 4): ✅ pass - unpack second
-DETAIL: 4 passed, 0 failed, 0 inconclusive
+DETAIL: 3 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_type_dict_annotation.expected b/StrataTest/Languages/Python/expected_laurel/test_type_dict_annotation.expected
index 2b25064dde..007113295d 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_type_dict_annotation.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_type_dict_annotation.expected
@@ -1,4 +1,3 @@
-test_type_dict_annotation.py(5, 4): ✅ pass - assert_assert(95)_calls_Any_get_0
 test_type_dict_annotation.py(5, 4): ✅ pass - typed dict
-DETAIL: 2 passed, 0 failed, 0 inconclusive
+DETAIL: 1 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_type_list_annotation.expected b/StrataTest/Languages/Python/expected_laurel/test_type_list_annotation.expected
index db7eb8de67..52172b4968 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_type_list_annotation.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_type_list_annotation.expected
@@ -1,4 +1,3 @@
-test_type_list_annotation.py(5, 4): ✅ pass - assert_assert(92)_calls_Any_get_0
 test_type_list_annotation.py(5, 4): ✅ pass - typed list
-DETAIL: 2 passed, 0 failed, 0 inconclusive
+DETAIL: 1 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/expected_laurel/test_var_shadow_func.expected b/StrataTest/Languages/Python/expected_laurel/test_var_shadow_func.expected
index 7aee788a67..601f7f9897 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_var_shadow_func.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_var_shadow_func.expected
@@ -1,9 +1,8 @@
 test_var_shadow_func.py(2, 8): ✅ pass - Check PAdd exception
-test_var_shadow_func.py(1, 17): ✅ pass - (f ensures) Return type constraint
 test_var_shadow_func.py(6, 4): ✅ pass - assert(83)
 test_var_shadow_func.py(7, 4): ✅ pass - (f requires) Type constraint of x
 test_var_shadow_func.py(7, 4): ✅ pass - assert(98)
 test_var_shadow_func.py(8, 4): ❓ unknown - param modified inside
 test_var_shadow_func.py(9, 4): ✅ pass - original unchanged
-DETAIL: 6 passed, 0 failed, 1 inconclusive
+DETAIL: 5 passed, 0 failed, 1 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_while_loop.expected b/StrataTest/Languages/Python/expected_laurel/test_while_loop.expected
index 18aceeb417..038870f888 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_while_loop.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_while_loop.expected
@@ -4,17 +4,14 @@ test_while_loop.py(4, 10): ✅ pass - Check PGt exception
 test_while_loop.py(5, 16): ❓ unknown - Check PAdd exception
 test_while_loop.py(6, 12): ❓ unknown - Check PSub exception
 test_while_loop.py(7, 4): ❓ unknown - countdown sum should be 15
-test_while_loop.py(1, 30): ❓ unknown - (test_while_countdown ensures) Return type constraint
 test_while_loop.py(11, 4): ✅ pass - assert(241)
 test_while_loop.py(13, 16): ❓ unknown - Check PAdd exception
 test_while_loop.py(16, 4): ✅ pass - should have counted to 10
-test_while_loop.py(10, 31): ❓ unknown (pass on 1 path, unknown on 1 path) - (test_while_true_break ensures) Return type constraint
 test_while_loop.py(20, 4): ✅ pass - assert(453)
 test_while_loop.py(21, 4): ✅ pass - assert(468)
 test_while_loop.py(22, 10): ✅ pass - Check PLt exception
 test_while_loop.py(23, 12): ❓ unknown - Check PAdd exception
 test_while_loop.py(27, 4): ❓ unknown - sum excluding 5 should be 50
-test_while_loop.py(19, 34): ❓ unknown - (test_while_with_continue ensures) Return type constraint
 test_while_loop.py(26, 16): ❓ unknown - Check PAdd exception
-DETAIL: 8 passed, 0 failed, 10 inconclusive
+DETAIL: 8 passed, 0 failed, 7 inconclusive
 RESULT: Inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_with_statement.expected b/StrataTest/Languages/Python/expected_laurel/test_with_statement.expected
index c73e76d8cb..8948ea9e4e 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_with_statement.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_with_statement.expected
@@ -1,9 +1,13 @@
+test_with_statement.py(16, 4): ✔️ always true if reached - (Resource@__init__ requires) Type constraint of n
 test_with_statement.py(17, 4): ✔️ always true if reached - assert(364)
 test_with_statement.py(20, 4): ✔️ always true if reached - assert(426)
+test_with_statement.py(23, 4): ✔️ always true if reached - (Resource@__init__ requires) Type constraint of n
 test_with_statement.py(25, 8): ✔️ always true if reached - assert(525)
 test_with_statement.py(26, 8): ✔️ always true if reached - assert(558)
+test_with_statement.py(29, 4): ✔️ always true if reached - (Resource@__init__ requires) Type constraint of n
+test_with_statement.py(30, 4): ✔️ always true if reached - (Resource@__init__ requires) Type constraint of n
 test_with_statement.py(32, 21): ✔️ always true if reached - Check PAdd exception
 test_with_statement.py(32, 8): ✔️ always true if reached - assert(697)
 test_with_statement.py(33, 8): ✔️ always true if reached - assert(724)
-DETAIL: 7 passed, 0 failed, 0 inconclusive
+DETAIL: 11 passed, 0 failed, 0 inconclusive
 RESULT: Analysis success
diff --git a/StrataTest/Languages/Python/tests/pending/test_bool_shortcircuit_and.py b/StrataTest/Languages/Python/tests/test_bool_shortcircuit_and.py
similarity index 100%
rename from StrataTest/Languages/Python/tests/pending/test_bool_shortcircuit_and.py
rename to StrataTest/Languages/Python/tests/test_bool_shortcircuit_and.py
diff --git a/StrataTest/Languages/Python/tests/pending/test_bool_shortcircuit_or.py b/StrataTest/Languages/Python/tests/test_bool_shortcircuit_or.py
similarity index 100%
rename from StrataTest/Languages/Python/tests/pending/test_bool_shortcircuit_or.py
rename to StrataTest/Languages/Python/tests/test_bool_shortcircuit_or.py
diff --git a/StrataTest/Languages/Python/tests/pending/test_dict_empty.py b/StrataTest/Languages/Python/tests/test_dict_empty.py
similarity index 100%
rename from StrataTest/Languages/Python/tests/pending/test_dict_empty.py
rename to StrataTest/Languages/Python/tests/test_dict_empty.py
diff --git a/StrataTest/Languages/Python/tests/pending/test_foo_client_folder.py b/StrataTest/Languages/Python/tests/test_foo_client_folder.py
similarity index 100%
rename from StrataTest/Languages/Python/tests/pending/test_foo_client_folder.py
rename to StrataTest/Languages/Python/tests/test_foo_client_folder.py
diff --git a/StrataTest/Languages/Python/tests/test_procedure_in_assert.py b/StrataTest/Languages/Python/tests/test_procedure_in_assert.py
new file mode 100644
index 0000000000..6fb2a194a2
--- /dev/null
+++ b/StrataTest/Languages/Python/tests/test_procedure_in_assert.py
@@ -0,0 +1,15 @@
+from datetime import timedelta
+
+def main() -> int:
+    # Test that a procedure call (timedelta_func) can appear in an
+    # assignment whose result is then used in an assert.
+    # The call is in assignment position (not expression position),
+    # which is the correct pattern for multi-output procedures.
+    base: int = 100
+    delta = timedelta(days=7)
+    result: int = 1
+    assert result == 1, "should pass"
+    return result
+
+if __name__ == "__main__":
+    main()