diff --git a/Strata/DDM/Format.lean b/Strata/DDM/Format.lean
index 26a58af21..b3e590d5a 100644
--- a/Strata/DDM/Format.lean
+++ b/Strata/DDM/Format.lean
@@ -30,9 +30,12 @@ Check if a character is valid for continuing a regular identifier.
 Includes @ and $ which are valid in SMT-LIB 2.6 simple symbols and
 used by the encoder for disambiguated names (e.g. x@1) and generated
 names (e.g. $__bv0).
+Note: `'` (apostrophe) is intentionally excluded. Although SMT-LIB 2.6 allows
+it in simple symbols, both cvc5 and Z3 reject it as an unquoted character.
+Names containing `'` (e.g. Lean's `v'`) will be pipe-quoted instead.
 -/
 private def isIdContinue (c : Char) : Bool :=
-  c.isAlphanum || c == '_' || c == '\'' || c == '.' || c == '?' || c == '!' || c == '@' || c == '$'
+  c.isAlphanum || c == '_' || c == '.' || c == '?' || c == '!' || c == '@' || c == '$'
 
 /--
 Check if a string needs pipe delimiters when formatted as an identifier.
diff --git a/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean b/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean
new file mode 100644
index 000000000..1fef2174e
--- /dev/null
+++ b/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean
@@ -0,0 +1,200 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+module
+public import Strata.Languages.Laurel.Laurel
+import Strata.DL.Lambda.LExpr
+import Strata.DDM.Util.Graph.Tarjan
+
+/-!
+## Grouping and Ordering for Core Translation
+
+Utilities for computing the grouping and topological ordering of Laurel
+declarations before they are emitted as Strata Core declarations.
+
+- `groupDatatypes` — groups mutually recursive datatypes into a single `.data`
+  declaration using Tarjan's SCC algorithm.
+- `computeSccDecls` — builds the procedure call graph, runs Tarjan's SCC
+  algorithm, and returns each SCC as a list of procedures paired with a flag
+  indicating whether the SCC is recursive. The result is in reverse topological
+  order (dependencies before dependents), which is the order required by Core.
+-/
+
+namespace Strata.Laurel
+
+open Lambda (LMonoTy LExpr)
+
+/-- Collect all `UserDefined` type names referenced in a `HighType`, including nested ones. -/
+def collectTypeRefs : HighTypeMd → List String
+  | ⟨.UserDefined name, _⟩ => [name.text]
+  | ⟨.TSet elem, _⟩ => collectTypeRefs elem
+  | ⟨.TMap k v, _⟩ => collectTypeRefs k ++ collectTypeRefs v
+  | ⟨.TTypedField vt, _⟩ => collectTypeRefs vt
+  | ⟨.Applied base args, _⟩ =>
+      collectTypeRefs base ++ args.flatMap collectTypeRefs
+  | ⟨.Pure base, _⟩ => collectTypeRefs base
+  | ⟨.Intersection ts, _⟩ => ts.flatMap collectTypeRefs
+  | ⟨.TCore name, _⟩ => [name]
+  | _ => []
+
+/-- Get all datatype names that a `DatatypeDefinition` references in its constructor args. -/
+def datatypeRefs (dt : DatatypeDefinition) : List String :=
+  dt.constructors.flatMap fun c => c.args.flatMap fun p => collectTypeRefs p.type
+
+/--
+Group `LDatatype Unit` values by strongly connected components of their direct type references.
+Datatypes in the same SCC (mutually recursive) share a single `.data` declaration.
+Non-recursive datatypes each get their own singleton `.data` declaration.
+The returned groups are in topological order: leaves (no dependencies) first, roots last.
+-/
+public def groupDatatypes (dts : List DatatypeDefinition)
+    (ldts : List (Lambda.LDatatype Unit)) : List (List (Lambda.LDatatype Unit)) :=
+  let n := dts.length
+  if n = 0 then [] else
+  let nameToIdx : Std.HashMap String Nat :=
+    dts.foldlIdx (fun m i dt => m.insert dt.name.text i) {}
+  -- dt[i] references dt[j] means i depends on j (j must be declared first).
+  -- tarjan guarantees: if there's a path A→B, B appears after A in the output.
+  -- So we add edge j→i (j has a path to i), ensuring i (the dependent) appears after j (the dependency).
+  let edges : List (Nat × Nat) :=
+    dts.foldlIdx (fun acc i dt =>
+      (datatypeRefs dt).filterMap nameToIdx.get? |>.foldl (fun acc j => (j, i) :: acc) acc) []
+  let g := OutGraph.ofEdges! n edges
+  let ldtMap : Std.HashMap String (Lambda.LDatatype Unit) :=
+    ldts.foldl (fun m ldt => m.insert ldt.name ldt) {}
+  let dtsArr := dts.toArray
+  OutGraph.tarjan g |>.toList.filterMap fun comp =>
+    let members := comp.toList.filterMap fun idx =>
+      dtsArr[idx]? |>.bind fun dt => ldtMap.get? dt.name.text
+    if members.isEmpty then none else some members
+
+/--
+Collect all `StaticCall` callee names referenced anywhere in a `StmtExpr`.
+Used to build the call graph for SCC-based procedure ordering.
+-/
+def collectStaticCallNames (expr : StmtExprMd) : List String :=
+  match expr with
+  | WithMetadata.mk val _ =>
+  match val with
+  | .StaticCall callee args =>
+      callee.text :: args.flatMap (fun a => collectStaticCallNames a)
+  | .PrimitiveOp _ args => args.flatMap (fun a => collectStaticCallNames a)
+  | .IfThenElse cond t e =>
+      collectStaticCallNames cond ++
+      collectStaticCallNames t ++
+      match e with
+      | some eelse => collectStaticCallNames eelse
+      | none => []
+  | .Block stmts _ => stmts.flatMap (fun s => collectStaticCallNames s)
+  | .Assign targets v =>
+      targets.flatMap (fun t => collectStaticCallNames t) ++
+      collectStaticCallNames v
+  | .LocalVariable _ _ initOption =>
+      match initOption with
+      | some init => collectStaticCallNames init
+      | none => []
+  | .Return v =>
+      match v with
+      | some x => collectStaticCallNames x
+      | none => []
+  | .While cond invs dec body =>
+      collectStaticCallNames cond ++
+      invs.flatMap (fun i => collectStaticCallNames i) ++
+      (match dec with
+      | some d => collectStaticCallNames d
+      | none => []) ++
+      collectStaticCallNames body
+  | .Forall _ trig body =>
+      (match trig with
+      | some t => collectStaticCallNames t
+      | none => []) ++
+      collectStaticCallNames body
+  | .Exists _ trig body =>
+      (match trig with
+      | some t => collectStaticCallNames t
+      | none => []) ++
+      collectStaticCallNames body
+  | .FieldSelect t _ => collectStaticCallNames t
+  | .PureFieldUpdate t _ v => collectStaticCallNames t ++ collectStaticCallNames v
+  | .InstanceCall t _ args =>
+      collectStaticCallNames t ++ args.flatMap (fun a => collectStaticCallNames a)
+  | .Old v | .Fresh v | .Assert v | .Assume v => collectStaticCallNames v
+  | .ProveBy v p => collectStaticCallNames v ++ collectStaticCallNames p
+  | .ReferenceEquals l r => collectStaticCallNames l ++ collectStaticCallNames r
+  | .AsType t _ | .IsType t _ => collectStaticCallNames t
+  | .ContractOf _ f => collectStaticCallNames f
+  | .Assigned v => collectStaticCallNames v
+  | _ => []
+termination_by sizeOf expr
+
+/--
+Build the procedure call graph, run Tarjan's SCC algorithm, and return each SCC
+as a list of procedures paired with a flag indicating whether the SCC is recursive.
+Results are in reverse topological order: dependencies before dependents.
+
+Procedures with an `invokeOn` trigger are placed as early as possible — before
+unrelated procedures without one — by stably partitioning them first before building
+the graph. Tarjan then naturally assigns them lower indices, causing them to appear
+earlier in the output.
+
+External procedures are excluded.
+-/
+public def computeSccDecls (program : Program) : List (List Procedure × Bool) :=
+  -- External procedures are completely ignored (not translated to Core).
+  -- Stable partition: procedures with invokeOn come first, preserving relative
+  -- order within each group. Tarjan then places them earlier in the topological output.
+  let (withInvokeOn, withoutInvokeOn) :=
+    (program.staticProcedures.filter (fun p => !p.body.isExternal))
+    |>.partition (fun p => p.invokeOn.isSome)
+  let nonExternal : List Procedure := withInvokeOn ++ withoutInvokeOn
+
+  -- Build a call-graph over all non-external procedures.
+  -- An edge proc → callee means proc's body/contracts contain a StaticCall to callee.
+  let nonExternalArr : Array Procedure := nonExternal.toArray
+  let nameToIdx : Std.HashMap String Nat :=
+    nonExternalArr.foldl (fun (acc : Std.HashMap String Nat × Nat) proc =>
+      (acc.1.insert proc.name.text acc.2, acc.2 + 1)) ({}, 0) |>.1
+
+  -- Collect all callee names from a procedure's body and contracts.
+  let procCallees (proc : Procedure) : List String :=
+    let bodyExprs : List StmtExprMd := match proc.body with
+      | .Transparent b => [b]
+      | .Opaque postconds (some impl) _ => postconds ++ [impl]
+      | .Opaque postconds none _ => postconds
+      | _ => []
+    let contractExprs : List StmtExprMd :=
+      proc.preconditions ++
+      proc.invokeOn.toList
+    (bodyExprs ++ contractExprs).flatMap collectStaticCallNames
+
+  -- Build the OutGraph for Tarjan.
+  let n := nonExternalArr.size
+  let graph : Strata.OutGraph n :=
+    nonExternalArr.foldl (fun (acc : Strata.OutGraph n × Nat) proc =>
+      let callerIdx := acc.2
+      let g := acc.1
+      let callees := procCallees proc
+      let g' := callees.foldl (fun g callee =>
+        match nameToIdx.get? callee with
+        | some calleeIdx => g.addEdge! calleeIdx callerIdx
+        | none => g) g
+      (g', callerIdx + 1)) (Strata.OutGraph.empty n, 0) |>.1
+
+  -- Run Tarjan's SCC algorithm. Results are in reverse topological order
+  -- (a node appears after all nodes that have paths to it).
+  let sccs := Strata.OutGraph.tarjan graph
+
+  sccs.toList.filterMap fun scc =>
+    let procs := scc.toList.filterMap fun idx =>
+      nonExternalArr[idx.val]?
+    if procs.isEmpty then none else
+    let isRecursive := procs.length > 1 ||
+      (match scc.toList.head? with
+        | some node => (graph.nodesOut node).contains node
+        | none => false)
+    some (procs, isRecursive)
+
+end Strata.Laurel
diff --git a/Strata/Languages/Laurel/DatatypeGrouping.lean b/Strata/Languages/Laurel/DatatypeGrouping.lean
deleted file mode 100644
index a3fab9d29..000000000
--- a/Strata/Languages/Laurel/DatatypeGrouping.lean
+++ /dev/null
@@ -1,68 +0,0 @@
-/-
-  Copyright Strata Contributors
-
-  SPDX-License-Identifier: Apache-2.0 OR MIT
--/
-
-module
-public import Strata.Languages.Laurel.Laurel
-import Strata.DL.Lambda.LExpr
-import Strata.DDM.Util.Graph.Tarjan
-
-/-!
-## Datatype Grouping via Tarjan's SCC
-
-Groups `LDatatype Unit` values by strongly connected components of their direct type
-references, so that mutually recursive datatypes share a single `.data` declaration.
-SCCs are emitted in dependency order: dependencies (leaves) before dependents (roots).
--/
-
-namespace Strata.Laurel
-
-open Lambda (LMonoTy LExpr)
-
-/-- Collect all `UserDefined` type names referenced in a `HighType`, including nested ones. -/
-def collectTypeRefs : HighTypeMd → List String
-  | ⟨.UserDefined name, _⟩ => [name.text]
-  | ⟨.TSet elem, _⟩ => collectTypeRefs elem
-  | ⟨.TMap k v, _⟩ => collectTypeRefs k ++ collectTypeRefs v
-  | ⟨.TTypedField vt, _⟩ => collectTypeRefs vt
-  | ⟨.Applied base args, _⟩ =>
-      collectTypeRefs base ++ args.flatMap collectTypeRefs
-  | ⟨.Pure base, _⟩ => collectTypeRefs base
-  | ⟨.Intersection ts, _⟩ => ts.flatMap collectTypeRefs
-  | ⟨.TCore name, _⟩ => [name]
-  | _ => []
-
-/-- Get all datatype names that a `DatatypeDefinition` references in its constructor args. -/
-def datatypeRefs (dt : DatatypeDefinition) : List String :=
-  dt.constructors.flatMap fun c => c.args.flatMap fun p => collectTypeRefs p.type
-
-/--
-Group `LDatatype Unit` values by strongly connected components of their direct type references.
-Datatypes in the same SCC (mutually recursive) share a single `.data` declaration.
-Non-recursive datatypes each get their own singleton `.data` declaration.
-The returned groups are in topological order: leaves (no dependencies) first, roots last.
--/
-public def groupDatatypes (dts : List DatatypeDefinition)
-    (ldts : List (Lambda.LDatatype Unit)) : List (List (Lambda.LDatatype Unit)) :=
-  let n := dts.length
-  if n = 0 then [] else
-  let nameToIdx : Std.HashMap String Nat :=
-    dts.foldlIdx (fun m i dt => m.insert dt.name.text i) {}
-  -- dt[i] references dt[j] means i depends on j (j must be declared first).
-  -- tarjan guarantees: if there's a path A→B, B appears after A in the output.
-  -- So we add edge j→i (j has a path to i), ensuring i (the dependent) appears after j (the dependency).
-  let edges : List (Nat × Nat) :=
-    dts.foldlIdx (fun acc i dt =>
-      (datatypeRefs dt).filterMap nameToIdx.get? |>.foldl (fun acc j => (j, i) :: acc) acc) []
-  let g := OutGraph.ofEdges! n edges
-  let ldtMap : Std.HashMap String (Lambda.LDatatype Unit) :=
-    ldts.foldl (fun m ldt => m.insert ldt.name ldt) {}
-  let dtsArr := dts.toArray
-  OutGraph.tarjan g |>.toList.filterMap fun comp =>
-    let members := comp.toList.filterMap fun idx =>
-      dtsArr[idx]? |>.bind fun dt => ldtMap.get? dt.name.text
-    if members.isEmpty then none else some members
-
-end Strata.Laurel
diff --git a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
index 847878012..fbd42e8b0 100644
--- a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
+++ b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
@@ -77,7 +77,7 @@ def translateBool (arg : Arg) : TransM Bool := do
   | x => TransM.error s!"translateBool expects expression or operation, got {repr x}"
 
 instance : Inhabited Parameter where
-  default := { name := "" , type := ⟨.TVoid, #[]⟩ }
+  default := { name := "" , type := ⟨.Unknown, #[]⟩ }
 
 def mkHighTypeMd (t : HighType) (md : MetaData) : HighTypeMd := ⟨t, md⟩
 def mkStmtExprMd (e : StmtExpr) (md : MetaData) : StmtExprMd := ⟨e, md⟩
@@ -146,6 +146,7 @@ instance : Inhabited Procedure where
     determinism := .deterministic none
     decreases := none
     isFunctional := false
+    invokeOn := none
     body := .Transparent ⟨.LiteralBool true, #[]⟩
     md := .empty
   }
@@ -426,9 +427,9 @@ def parseProcedure (arg : Arg) : TransM Procedure := do
 
   match op.name, op.args with
   | q`Laurel.procedure, #[nameArg, paramArg, returnTypeArg, returnParamsArg,
-      requiresArg, ensuresArg, modifiesArg, bodyArg]
+      requiresArg, invokeOnArg, ensuresArg, modifiesArg, bodyArg]
   | q`Laurel.function, #[nameArg, paramArg, returnTypeArg, returnParamsArg,
-      requiresArg, ensuresArg, modifiesArg, bodyArg] =>
+      requiresArg, invokeOnArg, ensuresArg, modifiesArg, bodyArg] =>
     let name ← translateIdent nameArg
     let nameMd ← getArgMetaData nameArg
     let parameters ← translateParameters paramArg
@@ -451,6 +452,14 @@ def parseProcedure (arg : Arg) : TransM Procedure := do
       | _ => TransM.error s!"Expected optionalReturnType operation, got {repr returnTypeArg}"
     -- Parse preconditions (requires clauses - zero or more)
     let preconditions ← translateRequiresClauses requiresArg
+    -- Parse optional invokeOn clause
+    let invokeOn ← match invokeOnArg with
+      | .option _ (some (.op invokeOnOp)) => match invokeOnOp.name, invokeOnOp.args with
+        | q`Laurel.invokeOnClause, #[triggerExprArg] =>
+          translateStmtExpr triggerExprArg >>= (pure ∘ some)
+        | _, _ => TransM.error s!"Expected invokeOnClause operation, got {repr invokeOnOp.name}"
+      | .option _ none => pure none
+      | _ => pure none
     -- Parse postconditions (ensures clauses - zero or more)
     let postconditions ← translateEnsuresClauses ensuresArg
     -- Parse modifies clauses (zero or more)
@@ -483,12 +492,13 @@ def parseProcedure (arg : Arg) : TransM Procedure := do
       determinism := .deterministic none
       decreases := none
       isFunctional := op.name == q`Laurel.function
+      invokeOn := invokeOn
       body := procBody
       md := nameMd
     }
   | 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 2adb32b74..aae3726f0 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: replaced regexType with general coreType
+-- Last grammar change: added invokeOn clause before ensures in procedure/function ops.
 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 08425d3e4..83a9dbdce 100644
--- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
+++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
@@ -90,7 +90,7 @@ category ElseBranch;
 op elseBranch(stmts : StmtExpr) : ElseBranch => @[prec(0)] "else" stmts;
 
 op ifThenElse (cond: StmtExpr, thenBranch: StmtExpr, elseBranch: Option ElseBranch): StmtExpr =>
-  @[prec(20)] "if (" cond ") " thenBranch:0 elseBranch:0;
+  @[prec(20)] "if " cond " then " thenBranch:0 elseBranch:0;
 
 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;
@@ -145,6 +145,9 @@ op datatype (name: Ident, constructors: DatatypeConstructorList): Datatype => "d
 category ReturnType;
 op returnType(returnType: LaurelType): ReturnType => ":" returnType;
 
+category InvokeOnClause;
+op invokeOnClause(trigger: StmtExpr): InvokeOnClause => "invokeOn" trigger:0;
+
 category RequiresClause;
 op requiresClause(cond: StmtExpr, errorMessage: Option ErrorSummary): RequiresClause => "requires" cond:0 errorMessage;
 
@@ -166,19 +169,21 @@ op procedure (name : Ident, parameters: CommaSepBy Parameter,
   returnType: Option ReturnType,
   returnParameters: Option ReturnParameters,
   requires: Seq RequiresClause,
+  invokeOn: Option InvokeOnClause,
   ensures: Seq EnsuresClause,
   modifies: Seq ModifiesClause,
   body : Option Body) : Procedure =>
-  "procedure " name "(" parameters ")" returnType returnParameters requires ensures modifies body ";";
+  "procedure " name "(" parameters ")" returnType returnParameters requires invokeOn ensures modifies body ";";
 
 op function (name : Ident, parameters: CommaSepBy Parameter,
   returnType: Option ReturnType,
   returnParameters: Option ReturnParameters,
   requires: Seq RequiresClause,
+  invokeOn: Option InvokeOnClause,
   ensures: Seq EnsuresClause,
   modifies: Seq ModifiesClause,
   body : Option Body) : Procedure =>
-  "function " name "(" parameters ")" returnType returnParameters requires ensures modifies body ";";
+  "function " name "(" parameters ")" returnType returnParameters requires invokeOn ensures modifies 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/Laurel.lean b/Strata/Languages/Laurel/Laurel.lean
index be67a015d..92690ef1a 100644
--- a/Strata/Languages/Laurel/Laurel.lean
+++ b/Strata/Languages/Laurel/Laurel.lean
@@ -189,6 +189,10 @@ structure Procedure : Type where
   isFunctional : Bool
   /-- The procedure body: transparent, opaque, or abstract. -/
   body : Body
+  /-- Optional trigger for auto-invocation. When present, the translator also emits an axiom
+      whose body is the ensures clause universally quantified over the procedure's inputs,
+      with this expression as the SMT trigger. -/
+  invokeOn : Option (WithMetadata StmtExpr) := none
   /-- Source-level metadata (locations, annotations). -/
   md : MetaData
 
diff --git a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean
index b612d254d..eb0430ed5 100644
--- a/Strata/Languages/Laurel/LaurelToCoreTranslator.lean
+++ b/Strata/Languages/Laurel/LaurelToCoreTranslator.lean
@@ -21,7 +21,7 @@ public import Strata.Languages.Laurel.TypeHierarchy
 public import Strata.Languages.Laurel.LaurelTypes
 public import Strata.Languages.Laurel.ModifiesClauses
 public import Strata.Languages.Laurel.CoreDefinitionsForLaurel
-import Strata.Languages.Laurel.DatatypeGrouping
+import Strata.Languages.Laurel.CoreGroupingAndOrdering
 import Strata.DDM.Util.DecimalRat
 import Strata.DL.Imperative.Stmt
 import Strata.DL.Imperative.MetaData
@@ -185,9 +185,9 @@ def translateExpr (expr : StmtExprMd)
     | .Neq => return .app () boolNotOp (.eq () re1 re2)
     | .And => return binOp boolAndOp
     | .Or => return binOp boolOrOp
-    | .AndThen => return .ite () re1 re2 (.boolConst () false)
-    | .OrElse => return .ite () re1 (.boolConst () true) re2
-    | .Implies => return .ite () re1 re2 (.boolConst () true)
+    | .AndThen => return binOp boolAndOp
+    | .OrElse => return binOp boolOrOp
+    | .Implies => return binOp boolImpliesOp
     | .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)
@@ -559,11 +559,52 @@ def translateProcedure (proc : Procedure) : TranslateM Core.Procedure := do
   let spec : Core.Procedure.Spec := { modifies, preconditions, postconditions }
   return { header, spec, body }
 
+def translateInvokeOnAxiom (proc : Procedure) (trigger : StmtExprMd)
+    : TranslateM (Option Core.Decl) := do
+  let model := (← get).model
+  let postconds := match proc.body with
+    | .Opaque postconds _ _ => postconds
+    | _ => []
+  if postconds.isEmpty then return none
+  -- All input param names become bound variables.
+  -- buildQuants nests ∀ p1, ∀ p2, ..., ∀ pn :: body, so inside body the innermost
+  -- binder (pn) is de Bruijn index 0, and the outermost (p1) is index n-1.
+  -- translateExpr uses findIdx? on boundVars, so we must list params innermost-first
+  -- (i.e. reversed) so that pn → 0, ..., p1 → n-1.
+  let boundVars := proc.inputs.reverse.map (·.name)
+  -- Translate postconditions and trigger with the full bound-var context
+  let postcondExprs ← postconds.mapM (fun pc => translateExpr pc boundVars (isPureContext := true))
+  let bodyExpr : Core.Expression.Expr := match postcondExprs with
+    | [] => .const () (.boolConst true)
+    | [e] => e
+    | e :: rest => rest.foldl (fun acc x => LExpr.mkApp () boolAndOp [acc, x]) e
+  let triggerExpr ← translateExpr trigger boundVars (isPureContext := true)
+  -- Wrap in ∀ from outermost (first param) to innermost (last param).
+  -- The trigger is placed on the innermost quantifier.
+  let quantified := buildQuants model proc.inputs bodyExpr triggerExpr
+  return some (.ax { name := s!"invokeOn_{proc.name.text}", e := quantified } proc.md)
+where
+  /-- Build `∀ p1 ... pn :: { trigger } body`. The trigger is on the innermost quantifier. -/
+  buildQuants (model : SemanticModel) (params : List Parameter)
+      (body : Core.Expression.Expr) (trigger : Core.Expression.Expr)
+      : Core.Expression.Expr :=
+    match params with
+    | [] => body
+    | [p] =>
+      LExpr.allTr () p.name.text (some (translateType model p.type)) trigger body
+    | p :: rest =>
+      LExpr.all () p.name.text (some (translateType model p.type))
+        (buildQuants model rest body trigger)
+
+structure LaurelTranslateOptions where
+  emitResolutionErrors : Bool := true
+  inlineFunctionsWhenPossible : Bool := false
+
 /--
 Translate a Laurel Procedure to a Core Function (when applicable) using `TranslateM`.
 Diagnostics for disallowed constructs in the function body are emitted into the monad state.
 -/
-def translateProcedureToFunction (proc : Procedure) : TranslateM Core.Decl := do
+def translateProcedureToFunction (options: LaurelTranslateOptions) (isRecursive: Bool) (proc : Procedure) : TranslateM Core.Decl := do
   let model := (← get).model
   let inputs := proc.inputs.map (translateParameterToCore model)
   let outputTy := match proc.outputs.head? with
@@ -574,20 +615,42 @@ def translateProcedureToFunction (proc : Procedure) : TranslateM Core.Decl := do
     let checkExpr ← translateExpr precondition [] true
     return { expr := checkExpr, md := () })
 
+  -- For recursive functions, infer the @[cases] parameter index: the first input
+  -- whose type is a user-defined datatype (has constructors). This is the argument
+  -- the partial evaluator will case-split on to unfold the recursion.
+  -- TODO: Use the decreases of the function to determine where to put @[cases]
+  -- First step should be to only support a decreases clause that is exactly one datatype parameter
+  -- Since that's what Core supports
+  let casesIdx : Option Nat :=
+    if !isRecursive then none
+    else proc.inputs.findIdx? fun p =>
+      match p.type.val with
+      | .UserDefined name => match model.get name with
+        | .datatypeDefinition _ => true
+        | _ => false
+      | _ => false
+  let attr : Array Strata.DL.Util.FuncAttr :=
+    match casesIdx with
+    | some i => #[.inlineIfConstr i]
+    | none => if options.inlineFunctionsWhenPossible then #[.inline] else #[]
+
   let body ← match proc.body with
     | .Transparent bodyExpr => some <$> translateExpr bodyExpr [] (isPureContext := true)
     | .Opaque _ (some bodyExpr) _ =>
       emitDiagnostic (proc.md.toDiagnostic "functions with postconditions are not yet supported")
       some <$> translateExpr bodyExpr [] (isPureContext := true)
     | _ => pure none
-  return .func {
+  let f : Core.Function := {
     name := ⟨proc.name.text, ()⟩
     typeArgs := []
     inputs := inputs
     output := outputTy
     body := body
     preconditions := preconditions
-  } proc.md
+    isRecursive := isRecursive
+    attr := attr
+  }
+  return .func f proc.md
 
 /--
 Translate a Laurel DatatypeDefinition to an `LDatatype Unit`.
@@ -609,9 +672,6 @@ def translateDatatypeDefinition (model : SemanticModel) (dt : DatatypeDefinition
     constrs_ne := by simp [constrs]; grind
   }
 
-structure LaurelTranslateOptions where
-  emitResolutionErrors : Bool := true
-
 abbrev TranslateResult := (Option Core.Program) × (List DiagnosticModel)
 
 /-- Like `translate` but also returns the lowered Laurel program (after all
@@ -626,7 +686,11 @@ def translateWithLaurel (options: LaurelTranslateOptions) (program : Program): T
     staticProcedures := coreDefinitionsForLaurel.staticProcedures ++ program.staticProcedures
   }
 
+  -- dbg_trace "=== Initial Laurel program ==="
+  -- dbg_trace (toString (Std.Format.pretty (Std.ToFormat.format program)))
+  -- dbg_trace "================================="
   let result := resolve program
+  let resolutionErrors: List DiagnosticModel := if options.emitResolutionErrors then result.errors.toList else []
   let (program, model) := (result.program, result.model)
   let diamondErrors := validateDiamondFieldAccesses model program
 
@@ -640,9 +704,6 @@ def translateWithLaurel (options: LaurelTranslateOptions) (program : Program): T
   let (program, modifiesDiags) := modifiesClausesTransform model program
   let result := resolve program (some model)
   let (program, model) := (result.program, result.model)
-  -- dbg_trace "=== Program after heapParameterization + modifiesClausesTransform ==="
-  -- dbg_trace (toString (Std.Format.pretty (Std.ToFormat.format program)))
-  -- dbg_trace "================================="
   let result := resolve program (some model)
   let (program, model) := (result.program, result.model)
   let program := inferHoleTypes model program
@@ -657,9 +718,8 @@ def translateWithLaurel (options: LaurelTranslateOptions) (program : Program): T
   let result := resolve program (some model)
   let (program, model) := (result.program, result.model)
 
-    let initState : TranslateState := {model := model }
-  let (coreProgramOption, translateState) := runTranslateM initState (translateLaurelToCore program)
-  let resolutionErrors: List DiagnosticModel := if options.emitResolutionErrors then result.errors.toList else []
+  let initState : TranslateState := {model := model }
+  let (coreProgramOption, translateState) := runTranslateM initState (translateLaurelToCore options program)
   let allDiagnostics := resolutionErrors ++ diamondErrors ++ modifiesDiags ++ constrainedTypeDiags ++ translateState.diagnostics
   let coreProgramOption := if translateState.coreProgramHasSuperfluousErrors then none else coreProgramOption
   (coreProgramOption, allDiagnostics, program)
@@ -686,17 +746,36 @@ def translateWithLaurel (options: LaurelTranslateOptions) (program : Program): T
     let groups := groupDatatypes laurelDatatypes ldatatypes
     return groups.map fun group => Core.Decl.type (.data group) mdWithUnknownLoc
 
-  translateLaurelToCore (program : Program): TranslateM Core.Program := do
+  translateLaurelToCore (options: LaurelTranslateOptions) (program : Program): TranslateM Core.Program := do
     let model := (← get).model
 
-    -- Procedures marked isFunctional are translated to Core functions; all others become Core procedures.
-    -- External procedures are completely ignored (not translated to Core).
-    let nonExternal := program.staticProcedures.filter (fun p => !p.body.isExternal)
-    let (markedPure, procProcs) := nonExternal.partition (·.isFunctional)
-    -- Try to translate each isFunctional procedure to a Core function, collecting errors for failures
-    let pureFuncDecls ← markedPure.mapM translateProcedureToFunction
-    -- Translate procedures using the monad, collecting diagnostics from the final state
-    let procedures ← procProcs.mapM translateProcedure
+    let sccDecls := computeSccDecls program
+
+    let orderedDecls ← sccDecls.flatMapM (fun (procs, isRecursive) => do
+      -- For each SCC, determine if it is purely functional or contains procedures.
+      -- Procedures can't call functions (only functions can call functions), so an SCC
+      -- either contains only functional procedures or only non-functional procedures.
+      let isFuncSCC := procs.all (·.isFunctional)
+      if isFuncSCC then
+        let funcs ← procs.mapM (translateProcedureToFunction options isRecursive)
+        if isRecursive then
+          -- Wrap all recursive functions (single self-recursive or mutual) in recFuncBlock.
+          let coreFuncs := funcs.filterMap (fun d => match d with
+            | .func f _ => some f
+            | _ => none)
+          return [Core.Decl.recFuncBlock coreFuncs mdWithUnknownLoc]
+        else
+          return funcs
+      else
+        procs.flatMapM fun proc => do
+          let axiomDecls : List Core.Decl ← match proc.invokeOn with
+            | none => pure []
+            | some trigger => do
+              let axDecl? ← translateInvokeOnAxiom proc trigger
+              pure axDecl?.toList
+          let procDecl ← translateProcedure proc
+          return [Core.Decl.proc procDecl proc.md] ++ axiomDecls
+    )
 
     -- Translate Laurel constants to Core function declarations (0-ary functions)
     let constantDecls ← program.constants.mapM fun c => do
@@ -710,16 +789,10 @@ def translateWithLaurel (options: LaurelTranslateOptions) (program : Program): T
         body := body
       } mdWithUnknownLoc
 
-    -- Collect ALL errors from both functions, procedures, and resolution before deciding whether to fail
-    -- let allErrors :=pureErrors ++ procDiags ++ constantsState.diagnostics
-    -- if !allErrors.isEmpty then
-    --   .error allErrors.toArray
-    let procDecls := procedures.map (fun p => Core.Decl.proc p mdWithUnknownLoc)
-
     -- Translate Laurel datatype definitions to Core declarations.
     let groupedDatatypeDecls ← translateTypes program model
     let program := {
-      decls := groupedDatatypeDecls ++ constantDecls ++ pureFuncDecls ++ procDecls
+      decls := groupedDatatypeDecls ++ constantDecls ++ orderedDecls
     }
 
     -- dbg_trace "=== Generated Strata Core Program ==="
@@ -741,7 +814,7 @@ Verify a Laurel program using an SMT solver
 def verifyToVcResults (program : Program)
     (options : VerifyOptions := .default)
     : IO (Option VCResults × List DiagnosticModel) := do
-  let (coreProgramOption, translateDiags) := translate { emitResolutionErrors := true } program
+  let (coreProgramOption, translateDiags) := translate {} program
 
   match coreProgramOption with
   | some coreProgram =>
@@ -756,7 +829,6 @@ def verifyToVcResults (program : Program)
     return (some ioResult, translateDiags)
   | none => return (none, translateDiags)
 
-
 def verifyToDiagnostics (files: Map Strata.Uri Lean.FileMap) (program : Program)
     (options : VerifyOptions := .default): IO (Array Diagnostic) := do
   let results <- verifyToVcResults program options
diff --git a/Strata/Languages/Laurel/Resolution.lean b/Strata/Languages/Laurel/Resolution.lean
index 790f650c0..0c2e8f931 100644
--- a/Strata/Languages/Laurel/Resolution.lean
+++ b/Strata/Languages/Laurel/Resolution.lean
@@ -439,9 +439,11 @@ def resolveProcedure (proc : Procedure) : ResolveM Procedure := do
     let det' ← resolveDeterminism proc.determinism
     let dec' ← proc.decreases.mapM resolveStmtExpr
     let body' ← resolveBody proc.body
+    let invokeOn' ← proc.invokeOn.mapM resolveStmtExpr
     return { name := procName', inputs := inputs', outputs := outputs',
              isFunctional := proc.isFunctional,
              preconditions := pres', determinism := det', decreases := dec',
+             invokeOn := invokeOn',
              body := body', md := proc.md }
 
 /-- Resolve a field: define its name under the qualified key (OwnerType.fieldName) and resolve its type. -/
@@ -463,10 +465,12 @@ def resolveInstanceProcedure (typeName : Identifier) (proc : Procedure) : Resolv
     let det' ← resolveDeterminism proc.determinism
     let dec' ← proc.decreases.mapM resolveStmtExpr
     let body' ← resolveBody proc.body
+    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', determinism := det', decreases := dec',
+             invokeOn := invokeOn',
              body := body', md := proc.md }
 
 /-- Resolve a type definition. -/
@@ -499,9 +503,14 @@ def resolveTypeDefinition (td : TypeDefinition) : ResolveM TypeDefinition := do
   | .Constrained ct =>
     let ctName' ← defineName ct.name (.constrainedType ct)
     let base' ← resolveHighType ct.base
-    let constraint' ← resolveStmtExpr ct.constraint
-    let witness' ← resolveStmtExpr ct.witness
-    return .Constrained { name := ctName', base := base', valueName := ct.valueName,
+    -- The valueName (e.g. `x` in `constrained nat = x: int where x >= 0`) must be
+    -- in scope when resolving the constraint and witness expressions.
+    let (valueName', constraint', witness') ← withScope do
+      let valueName' ← defineName ct.valueName (.quantifierVar ct.valueName base')
+      let constraint' ← resolveStmtExpr ct.constraint
+      let witness' ← resolveStmtExpr ct.witness
+      return (valueName', constraint', witness')
+    return .Constrained { name := ctName', base := base', valueName := valueName',
                           constraint := constraint', witness := witness' }
   | .Datatype dt =>
     let dtName' ← defineName dt.name (.datatypeDefinition dt)
diff --git a/Strata/Languages/Python/PySpecPipeline.lean b/Strata/Languages/Python/PySpecPipeline.lean
index 8471c3b15..c88348cc1 100644
--- a/Strata/Languages/Python/PySpecPipeline.lean
+++ b/Strata/Languages/Python/PySpecPipeline.lean
@@ -296,42 +296,29 @@ public def buildPreludeInfo (result : PySpecLaurelResult) : Python.PreludeInfo :
 /-- Combine PySpec and user Laurel programs into a single program,
     prepending External stubs so the Laurel `resolve` pass can see
     prelude names (e.g. `print`, `from_string`). -/
-public def combinePySpecLaurel (info : Python.PreludeInfo)
+public def combinePySpecLaurel
     (pySpec user : Laurel.Program) : Laurel.Program :=
-  let stubs := Python.preludeStubs info
-  let pySpecNames : Std.HashSet String := pySpec.staticProcedures.foldl (init := {})
-    fun s p => if !p.body.isExternal then s.insert p.name.text else s
-  let filteredStubs := stubs.filter fun p => !pySpecNames.contains p.name.text
-  { staticProcedures := filteredStubs ++ pySpec.staticProcedures ++ user.staticProcedures
+  { staticProcedures := pySpec.staticProcedures ++ user.staticProcedures
     staticFields := pySpec.staticFields ++ user.staticFields
     types := pySpec.types ++ user.types
     constants := pySpec.constants ++ user.constants
   }
 
-/-- Prepend the full Python runtime Core prelude (datatype definitions,
+/-- Append the Core part of the Python runtime (datatype definitions,
     procedure bodies, etc.) to the Core program produced by Laurel
     translation. -/
-private def prependPrelude (coreFromLaurel : Core.Program) : Core.Program :=
-  let (preludeDecls, userDecls) := coreFromLaurel.decls.span (fun d => toString d.name != "FIRST_END_MARKER")
-  -- The Core-only prelude has proper signatures for functions that the
-  -- Laurel→Core translator may have produced as empty-signature stubs.
-  -- Filter stubs from preludeDecls when a proper declaration exists.
-  let coreOnly := Python.coreOnlyFromRuntimeCorePart
-  let coreOnlyNames : Std.HashSet String := coreOnly.foldl (init := {})
-    fun s d => s.insert (toString d.name)
-  let filteredPrelude := preludeDecls.filter
-    fun d => !coreOnlyNames.contains (toString d.name)
-  { decls := filteredPrelude ++ coreOnly ++ userDecls }
+private def appendCorePartOfRuntime (coreFromLaurel : Core.Program) : Core.Program :=
+  { decls := coreFromLaurel.decls ++ Python.coreOnlyFromRuntimeCorePart  }
 
 /-- Split procedure names in a Core program into prelude names
-    (before `FIRST_END_MARKER`) and user names (after it).
-    If `FIRST_END_MARKER` is absent, nothing is considered prelude. -/
+    (no file range or empty file) and user names (all others). -/
 public def splitProcNames (prog : Core.Program)
     : Std.HashSet String × List String :=
-  let (before, rest) := prog.decls.span (fun d => toString d.name != "FIRST_END_MARKER")
-  let (preludeDecls, userDecls) := match rest with
-    | _ :: tl => (before, tl)  -- marker found: before is prelude, after is user
-    | [] => ([], before)       -- no marker: everything is user
+  let isPrelude := fun d =>
+    match Imperative.getFileRange (P := Core.Expression) d.metadata with
+    | none => true
+    | some fr => fr.file == .file ""
+  let (preludeDecls, userDecls) := prog.decls.partition isPrelude
   let preludeNames := preludeDecls.foldl (init := ({} : Std.HashSet String)) fun s d =>
     match d.getProc? with
     | some p => s.insert (Core.CoreIdent.toPretty p.header.name)
@@ -340,24 +327,19 @@ public def splitProcNames (prog : Core.Program)
     d.getProc?.map (Core.CoreIdent.toPretty ·.header.name)
   (preludeNames, userProcNames)
 
-/-- Translate a combined Laurel program to Core and prepend the full
-    runtime prelude.  Resolution errors are suppressed because PySpec
-    Laurel procedures reference names defined in the Core prelude
-    (`from_none`, `from_string`, `NoError`, etc.) which the Laurel
-    resolver cannot see — they are merged after translation. Once the
-    Python Core prelude is ported to Laurel, this suppression can be
-    removed. -/
-public def translateCombinedLaurel (combined : Laurel.Program)
-    : (Option Core.Program × List DiagnosticModel) :=
-  let (coreOption, errors) := Laurel.translate { emitResolutionErrors := false } combined
-  (coreOption.map prependPrelude, errors)
-
 /-- Like `translateCombinedLaurel` but also returns the lowered Laurel program
     (after all Laurel-to-Laurel passes, before translation to Core). -/
 public def translateCombinedLaurelWithLowered (combined : Laurel.Program)
     : (Option Core.Program × List DiagnosticModel × Laurel.Program) :=
-  let (coreOption, errors, lowered) := Laurel.translateWithLaurel { emitResolutionErrors := false } combined
-  (coreOption.map prependPrelude, errors, lowered)
+  let (coreOption, errors, lowered) := Laurel.translateWithLaurel { inlineFunctionsWhenPossible := true } combined
+  (coreOption.map appendCorePartOfRuntime, errors, lowered)
+
+/-- Translate a combined Laurel program to Core and prepend the full
+    runtime prelude. -/
+public def translateCombinedLaurel (combined : Laurel.Program)
+    : (Option Core.Program × List DiagnosticModel) :=
+  let (coreOption, errors, _) := translateCombinedLaurelWithLowered combined
+  (coreOption, errors)
 
 /-- Errors from the pyAnalyzeLaurel pipeline. -/
 public inductive PipelineError where
@@ -413,6 +395,6 @@ public def pyAnalyzeLaurel
     | .error e => throw (.internal s!"Python to Laurel translation failed: {e}")
     | .ok result => pure result
 
-  return combinePySpecLaurel preludeInfo result.laurelProgram laurelProgram
+  return combinePySpecLaurel result.laurelProgram laurelProgram
 
 end Strata
diff --git a/Strata/Languages/Python/PythonLaurelCorePrelude.lean b/Strata/Languages/Python/PythonLaurelCorePrelude.lean
index 952b04f07..3b20cd30b 100644
--- a/Strata/Languages/Python/PythonLaurelCorePrelude.lean
+++ b/Strata/Languages/Python/PythonLaurelCorePrelude.lean
@@ -5,7 +5,6 @@
 -/
 module
 
--- TODO: rename file to PythonRuntimeCorePart
 import Strata.DDM.Elab
 import Strata.DDM.AST
 import Strata.Languages.Core.DDMTransform.Grammar
@@ -30,7 +29,7 @@ are filtered out.
 
 The original `CorePrelude.lean` remains unchanged for the Python-through-Core pipeline.
 -/
-private def pythonRuntimeCorePartDDM :=
+private def PythonLaurelCorePreludeDDM :=
 #strata
 program Core;
 
@@ -101,254 +100,17 @@ datatype DictStrAny () {
   DictStrAny_cons (key: string, val: Any, tail: DictStrAny)
 };
 
-// Forward declaration for re_pattern_error: needed so the inline functions
-// after CoreOnlyDelimiter can reference it during DDM parsing.
-function re_pattern_error(pattern : string) : Error;
-// The _bool variants are also factory functions (not inlined here) so that
-// unsupported patterns leave an uninterpreted Bool UF rather than an
-// uninterpreted RegLan UF.  An uninterpreted Bool UF produces `unknown`
-// gracefully; an uninterpreted RegLan UF causes cvc5 theory-combination errors.
-function re_fullmatch_bool(pattern : string, s : string) : bool;
-function re_match_bool(pattern : string, s : string) : bool;
-function re_search_bool(pattern : string, s : string) : bool;
-
 type CoreOnlyDelimiter;
 
 // =====================================================================
 // Core-only declarations (not expressed in Laurel)
 // =====================================================================
 
-// /////////////////////////////////////////////////////////////////////////////////////
-// Regex support
-//
-// Python signatures:
-//   re.compile(pattern: str) -> re.Pattern
-//   re.match(pattern: str | re.Pattern, string: str) -> re.Match | None
-//   re.search(pattern: str | re.Pattern, string: str) -> re.Match | None
-//   re.fullmatch(pattern: str | re.Pattern, string: str) -> re.Match | None
-//
-// Architecture:
-//
-// re.compile is a semantic no-op — it returns the pattern string unchanged.
-// The mode-specific factory functions re_fullmatch_bool, re_match_bool,
-// re_search_bool each compile a pattern+string pair to a Bool via
-// pythonRegexToCore, so anchors (^/$) are handled correctly per mode.
-// Their concreteEval fires when the pattern is a string literal; on
-// unsupported patterns it returns .none, leaving an uninterpreted Bool UF
-// (which produces `unknown` gracefully rather than a cvc5 theory-combination
-// error).
-//
-// On match, we return a from_ClassInstance wrapping a concrete re_Match
-// with pos=0 and endpos=str.len(s), which is sound for the module-level
-// API (no pos/endpos parameters).
-// /////////////////////////////////////////////////////////////////////////////////////
-
-// Mode-specific factory functions (re_fullmatch_bool, re_match_bool,
-// re_search_bool) are declared via ReFactory (with concreteEval for literal
-// pattern expansion), not as inlines here, to avoid duplicate definitions and
-// to prevent uninterpreted RegLan UFs from reaching the SMT solver.
-
-inline function mk_re_Match(s : string) : Any {
-  from_ClassInstance("re_Match",
-    DictStrAny_cons("re_match_string", from_string(s),
-      DictStrAny_cons("re_match_pos", from_int(0),
-        DictStrAny_cons("re_match_endpos", from_int(str.len(s)),
-          DictStrAny_empty()))))
-}
-
-// re.compile is a no-op: returns the pattern string unchanged.
-inline function re_compile(pattern : Any) : Any
-  requires Any..isfrom_string(pattern);
-{
-  pattern
-}
-
-inline function re_fullmatch(pattern : Any, s : Any) : Any
-  requires Any..isfrom_string(pattern) && Any..isfrom_string(s);
-{
-  if Error..isRePatternError(re_pattern_error(Any..as_string!(pattern)))
-  then exception(re_pattern_error(Any..as_string!(pattern)))
-  else if re_fullmatch_bool(Any..as_string!(pattern), Any..as_string!(s))
-       then mk_re_Match(Any..as_string!(s))
-       else from_none()
-}
-inline function re_match(pattern : Any, s : Any) : Any
-  requires Any..isfrom_string(pattern) && Any..isfrom_string(s);
-{
-  if Error..isRePatternError(re_pattern_error(Any..as_string!(pattern)))
-  then exception(re_pattern_error(Any..as_string!(pattern)))
-  else if re_match_bool(Any..as_string!(pattern), Any..as_string!(s))
-       then mk_re_Match(Any..as_string!(s))
-       else from_none()
-}
-inline function re_search(pattern : Any, s : Any) : Any
-  requires Any..isfrom_string(pattern) && Any..isfrom_string(s);
-{
-  if Error..isRePatternError(re_pattern_error(Any..as_string!(pattern)))
-  then exception(re_pattern_error(Any..as_string!(pattern)))
-  else if re_search_bool(Any..as_string!(pattern), Any..as_string!(s))
-       then mk_re_Match(Any..as_string!(s))
-       else from_none()
-}
-
-// /////////////////////////////////////////////////////////////////////////////////////
-//Functions that we provide to Python user
-//to write assertions/contracts about about types of variables
-
-inline function isBool (v: Any) : Any {
-  from_bool (Any..isfrom_bool(v))
-}
-
-inline function isInt (v: Any) : Any {
-  from_bool (Any..isfrom_int(v))
-}
-
-inline function isFloat (v: Any) : Any {
-  from_bool (Any..isfrom_float(v))
-}
-
-inline function isString (v: Any) : Any {
-  from_bool (Any..isfrom_string(v))
-}
-
-inline function isdatetime (v: Any) : Any {
-  from_bool (Any..isfrom_datetime(v))
-}
-
-inline function isDict (v: Any) : Any {
-  from_bool (Any..isfrom_Dict(v))
-}
-
-inline function isList (v: Any) : Any {
-  from_bool (Any..isfrom_ListAny(v))
-}
-
-inline function isClassInstance (v: Any) : Any {
-  from_bool (Any..isfrom_ClassInstance(v))
-}
-
-inline function isInstance_of_Int (v: Any) : Any {
-  from_bool (Any..isfrom_int(v) || Any..isfrom_bool(v))
-}
-
-inline function isInstance_of_Float (v: Any) : Any {
-  from_bool (Any..isfrom_float(v) || Any..isfrom_int(v) || Any..isfrom_bool(v))
-}
-
-// /////////////////////////////////////////////////////////////////////////////////////
-//Functions that we provide to Python user
-//to write assertions/contracts about about types of errors
-// /////////////////////////////////////////////////////////////////////////////////////
-
-inline function isTypeError (e: Error) : Any {
-  from_bool (Error..isTypeError(e))
-}
-
-inline function isAttributeError (e: Error) : Any {
-  from_bool (Error..isAttributeError(e))
-}
-
-inline function isAssertionError (e: Error) : Any {
-  from_bool (Error..isAssertionError(e))
-}
-
-inline function isUnimplementedError (e: Error) : Any {
-  from_bool (Error..isUnimplementedError(e))
-}
-
-inline function isUndefinedError (e: Error) : Any {
-  from_bool (Error..isUndefinedError(e))
-}
-
-inline function isError (e: Error) : bool {
-  ! Error..isNoError(e)
-}
-
-// /////////////////////////////////////////////////////////////////////////////////////
-//The following function convert Any type to bool
-//based on the Python definition of truthiness for basic types
-// https://docs.python.org/3/library/stdtypes.html
-// /////////////////////////////////////////////////////////////////////////////////////
-
-inline function Any_to_bool (v: Any) : bool
-  requires (Any..isfrom_bool(v) || Any..isfrom_none(v) || Any..isfrom_string(v) || Any..isfrom_int(v) || Any..isfrom_Dict(v) || Any..isfrom_ListAny(v));
-{
-  if (Any..isfrom_bool(v)) then Any..as_bool!(v) else
-  if (Any..isfrom_none(v)) then false else
-  if (Any..isfrom_string(v)) then !(Any..as_string!(v) == "") else
-  if (Any..isfrom_int(v)) then !(Any..as_int!(v) == 0) else
-  if (Any..isfrom_Dict(v)) then !(Any..as_Dict!(v) == DictStrAny_empty) else
-  if (Any..isfrom_ListAny(v)) then !(Any..as_ListAny!(v) == ListAny_nil) else
-  false
-  //WILL BE ADDED
-}
-
 // /////////////////////////////////////////////////////////////////////////////////////
 // ListAny functions
 // /////////////////////////////////////////////////////////////////////////////////////
 
-rec function List_len (@[cases] l : ListAny) : int
-{
-  if ListAny..isListAny_nil(l) then 0 else 1 + List_len(ListAny..tail!(l))
-};
-
-axiom [List_len_pos]: forall l : ListAny :: List_len(l) >= 0;
-
-rec function List_contains (@[cases] l : ListAny, x: Any) : bool
-{
-  if ListAny..isListAny_nil(l) then false else (ListAny..head!(l) == x) || List_contains(ListAny..tail!(l), x)
-};
-
-rec function List_extend (@[cases] l1 : ListAny, l2: ListAny) : ListAny
-{
-  if ListAny..isListAny_nil(l1) then l2
-  else ListAny_cons(ListAny..head!(l1), List_extend(ListAny..tail!(l1), l2))
-};
-
-rec function List_get (@[cases] l : ListAny, i : int) : Any
-  requires i >= 0 && i < List_len(l);
-{
-  if ListAny..isListAny_nil(l) then from_none()
-  else if  i == 0 then ListAny..head!(l)
-  else List_get(ListAny..tail!(l), i - 1)
-};
-
-rec function List_take (@[cases] l : ListAny, i: int) : ListAny
-  requires i >= 0 && i <= List_len(l);
-{
-  if ListAny..isListAny_nil(l) then ListAny_nil()
-  else if  i == 0 then ListAny_nil()
-  else ListAny_cons(ListAny..head!(l), List_take(ListAny..tail!(l), i - 1))
-};
-
-axiom [List_take_len]: forall l : ListAny, i: int :: {List_len(List_take(l,i))}
-  (i >= 0 && i <= List_len(l)) ==> List_len(List_take(l,i)) == i;
-
-rec function List_drop (@[cases] l : ListAny, i: int) : ListAny
-  requires i >= 0 && i <= List_len(l);
-{
-  if ListAny..isListAny_nil(l) then ListAny_nil()
-  else if  i == 0 then l
-  else List_drop(ListAny..tail!(l), i - 1)
-};
-
-axiom [List_drop_len]: forall l : ListAny, i: int :: {List_len(List_drop(l,i))}
-  (i >= 0 && i <= List_len(l)) ==> List_len(List_drop(l,i)) == List_len(l) - i;
-
-inline function List_slice (l : ListAny, start : int, stop: int) : ListAny
-  requires start >= 0 && start < List_len(l) && stop >= 0 && stop <= List_len(l) && start <= stop;
-{
-  List_take (List_drop (l, start), stop - start)
-}
-
-rec function List_set (@[cases] l : ListAny, i : int, v: Any) : ListAny
-  requires i >= 0 && i < List_len(l);
-{
-  if ListAny..isListAny_nil(l) then ListAny_nil()
-  else if  i == 0 then ListAny_cons(v, ListAny..tail!(l))
-  else ListAny_cons(ListAny..head!(l), List_set(ListAny..tail!(l), i - 1, v))
-};
-
+// TODO introduce procedure types in Laurel so we can move this to the Laurel part
 rec function List_map (@[cases] l : ListAny, f: Any -> Any) : ListAny
 {
   if ListAny..isListAny_nil(l) then
@@ -367,582 +129,10 @@ rec function List_filter (@[cases] l : ListAny, f: Any -> bool) : ListAny
     List_filter(ListAny..tail!(l), f)
 };
 
-//Require recursive function on int
-function List_repeat (l: ListAny, n: int): ListAny;
-
-
-// /////////////////////////////////////////////////////////////////////////////////////
-// DictStrAny functions
-// /////////////////////////////////////////////////////////////////////////////////////
-
-rec function DictStrAny_contains (@[cases] d : DictStrAny, key: string) : bool
-{
-  if DictStrAny..isDictStrAny_empty(d) then false
-  else (DictStrAny..key!(d) == key) || DictStrAny_contains(DictStrAny..tail!(d), key)
-};
-
-rec function DictStrAny_get (@[cases] d : DictStrAny, key: string) : Any
-  requires DictStrAny_contains(d, key);
-{
-  if  DictStrAny..isDictStrAny_empty(d) then from_none()
-  else if DictStrAny..key!(d) == key then DictStrAny..val!(d)
-  else DictStrAny_get(DictStrAny..tail!(d), key)
-};
-
-inline function DictStrAny_get_or_none (d : DictStrAny, key: string) : Any
-{
-  if DictStrAny_contains(d, key) then DictStrAny_get(d, key)
-  else from_none()
-}
-
-inline function Any_get_or_none (dict: Any, key: Any) : Any
-  requires Any..isfrom_Dict(dict) && Any..isfrom_string(key);
-{
-  DictStrAny_get_or_none(Any..as_Dict!(dict), Any..as_string!(key))
-}
-
-rec function DictStrAny_insert (@[cases] d : DictStrAny, key: string, val: Any) : DictStrAny
-{
-  if DictStrAny..isDictStrAny_empty(d) then DictStrAny_cons(key, val, DictStrAny_empty())
-  else if DictStrAny..key!(d) == key then DictStrAny_cons(key, val, DictStrAny..tail!(d))
-  else DictStrAny_cons(DictStrAny..key!(d), DictStrAny..val!(d), DictStrAny_insert(DictStrAny..tail!(d), key, val))
-};
-
-inline function Any_get (dictOrList: Any, index: Any): Any
-  requires  (Any..isfrom_Dict(dictOrList) && Any..isfrom_string(index) && DictStrAny_contains(Any..as_Dict!(dictOrList), Any..as_string!(index))) ||
-            (Any..isfrom_ListAny(dictOrList) && Any..isfrom_int(index) && Any..as_int!(index) >= 0 && Any..as_int!(index) < List_len(Any..as_ListAny!(dictOrList)))||
-            (Any..isfrom_ListAny(dictOrList) && Any..isfrom_Slice(index) && Any..start!(index) >= 0 && Any..start!(index) < List_len(Any..as_ListAny!(dictOrList)) &&
-                ((OptionInt..isSome(Any..stop!(index))) &&  OptionInt..unwrap!(Any..stop!(index)) >= 0 && OptionInt..unwrap!(Any..stop!(index)) <= List_len(Any..as_ListAny!(dictOrList)) && Any..start!(index) <= OptionInt..unwrap!(Any..stop!(index))
-                  || (OptionInt..isNone(Any..stop!(index)))));
-{
-  if Any..isfrom_Dict(dictOrList) then
-    DictStrAny_get(Any..as_Dict!(dictOrList), Any..as_string!(index))
-  else if Any..isfrom_ListAny(dictOrList) && Any..isfrom_int(index) then
-    List_get(Any..as_ListAny!(dictOrList), Any..as_int!(index))
-  else if Any..isfrom_ListAny(dictOrList) && Any..isfrom_Slice(index) && OptionInt..isSome(Any..stop!(index)) then
-    from_ListAny(List_slice(Any..as_ListAny!(dictOrList), Any..start!(index), OptionInt..unwrap!(Any..stop!(index))))
-  else
-    from_ListAny(List_drop(Any..as_ListAny!(dictOrList), Any..start!(index)))
-}
-
-inline function Any_get! (dictOrList: Any, index: Any): Any
-{
-  if Any..isexception(dictOrList) then dictOrList
-  else if Any..isexception(index) then index
-  else if !(Any..isfrom_Dict(dictOrList) && Any..isfrom_string(index)) && !(Any..isfrom_ListAny(dictOrList) && Any..isfrom_int(index)) then
-    exception (TypeError("Invalid subscription type"))
-  else if Any..isfrom_Dict(dictOrList) && Any..isfrom_string(index) && DictStrAny_contains(Any..as_Dict!(dictOrList), Any..as_string!(index)) then
-    DictStrAny_get(Any..as_Dict!(dictOrList), Any..as_string!(index))
-  else if Any..isfrom_ListAny(dictOrList) && Any..isfrom_int(index) && Any..as_int!(index) >= 0 && Any..as_int!(index) < List_len(Any..as_ListAny!(dictOrList)) then
-    List_get(Any..as_ListAny!(dictOrList), Any..as_int!(index))
-  else
-    exception (IndexError("Invalid subscription"))
-}
-
-inline function Any_set (dictOrList: Any, index: Any, val: Any): Any
-  requires  (Any..isfrom_Dict(dictOrList) && Any..isfrom_string(index)) ||
-            (Any..isfrom_ListAny(dictOrList) && Any..isfrom_int(index) && Any..as_int!(index) >= 0 && Any..as_int!(index) < List_len(Any..as_ListAny!(dictOrList)));
-{
-  if Any..isfrom_Dict(dictOrList) then
-    from_Dict(DictStrAny_insert(Any..as_Dict!(dictOrList), Any..as_string!(index), val))
-  else
-    from_ListAny(List_set(Any..as_ListAny!(dictOrList), Any..as_int!(index), val))
-}
-
-inline function Any_set! (dictOrList: Any, index: Any, val: Any): Any
-{
-  if Any..isexception(dictOrList) then dictOrList
-  else if Any..isexception(index) then index
-  else if Any..isexception(val) then val
-  else if !(Any..isfrom_Dict(dictOrList) && Any..isfrom_string(index)) && !(Any..isfrom_ListAny(dictOrList) && Any..isfrom_int(index)) then
-    exception (TypeError("Invalid subscription type"))
-  else if Any..isfrom_Dict(dictOrList) && Any..isfrom_string(index) then
-    from_Dict(DictStrAny_insert(Any..as_Dict!(dictOrList), Any..as_string!(index), val))
-  else if Any..isfrom_ListAny(dictOrList) && Any..isfrom_int(index) && Any..as_int!(index) >= 0 && Any..as_int!(index) < List_len(Any..as_ListAny!(dictOrList)) then
-    from_ListAny(List_set(Any..as_ListAny!(dictOrList), Any..as_int!(index), val))
-  else
-    exception (IndexError("Index out of bound"))
-}
-
-rec function Any_sets (dictOrList: Any, @[cases] indices: ListAny, val: Any): Any
-{
-  if ListAny..isListAny_nil(indices) then dictOrList
-  else if ListAny..isListAny_nil(ListAny..tail!(indices)) then Any_set!(dictOrList, ListAny..head!(indices), val)
-  else Any_set!(dictOrList, ListAny..head!(indices),
-    Any_sets(Any_get!(dictOrList, ListAny..head!(indices)), ListAny..tail!(indices), val))
-};
-
-inline function PIn (v: Any, dictOrList: Any) : Any
-  requires (Any..isfrom_Dict(dictOrList) && Any..isfrom_string(v)) || Any..isfrom_ListAny(dictOrList);
-{
-  from_bool(
-    if Any..isfrom_Dict(dictOrList) then
-      DictStrAny_contains(Any..as_Dict!(dictOrList), Any..as_string!(v))
-    else
-      List_contains(Any..as_ListAny!(dictOrList), v)
-  )
-}
-
-inline function PNotIn ( v: Any, dictOrList: Any) : Any
-  requires (Any..isfrom_Dict(dictOrList) && Any..isfrom_string(v)) || Any..isfrom_ListAny(dictOrList);
-{
-  from_bool(
-    if Any..isfrom_Dict(dictOrList) then
-      !DictStrAny_contains(Any..as_Dict!(dictOrList), Any..as_string!(v))
-    else
-      !List_contains(Any..as_ListAny!(dictOrList), v)
-  )
-}
-
-// /////////////////////////////////////////////////////////////////////////////////////
-// Python treats some values of different types to be equivalent
-// This function models that behavior
-// /////////////////////////////////////////////////////////////////////////////////////
-
-function is_IntReal (v: Any) : bool;
-function Any_real_to_int (v: Any) : int;
-
-inline function normalize_any (v : Any) : Any {
-  if v == from_bool(true) then from_int(1)
-  else (if v == from_bool(false) then from_int(0) else
-        if Any..isfrom_float(v) && is_IntReal(v) then from_int(Any_real_to_int(v)) else
-        v)
-}
-
-// /////////////////////////////////////////////////////////////////////////////////////
-// MODELLING PYTHON OPERATIONS
-// Note that there is no official document that define the semantic of Python operations
-// The model of them in this prelude is based on experiments of basic types
-// /////////////////////////////////////////////////////////////////////////////////////
-
-
-// /////////////////////////////////////////////////////////////////////////////////////
-// This function convert an int to a real
-// Need to connect to an SMT function
-function int_to_real (i: int) : real;
-
-// /////////////////////////////////////////////////////////////////////////////////////
-// Converting bool to int or real
-// Used to in Python binary operators' modelling
-inline function bool_to_int (bval: bool) : int {if bval then 1 else 0}
-inline function bool_to_real (b: bool) : real {if b then 1.0 else 0.0}
-
-// /////////////////////////////////////////////////////////////////////////////////////
-// Modelling of Python unary operations
-// /////////////////////////////////////////////////////////////////////////////////////
-
-inline function PNeg (v: Any) : Any
-{
-  if Any..isexception(v) then v
-  else if (Any..isfrom_bool(v)) then
-    from_int(- bool_to_int(Any..as_bool!(v)))
-  else if (Any..isfrom_int(v)) then
-    from_int(- Any..as_int!(v))
-  else if (Any..isfrom_float(v)) then
-    from_float(- Any..as_float!(v))
-  else
-    exception(UndefinedError ("Operand Type is not defined"))
-}
-
-inline function PNot (v: Any) : Any
-{
-  if Any..isexception(v) then v
-  else if (Any..isfrom_bool(v)) then
-    from_bool(!(Any..as_bool!(v)))
-  else if (Any..isfrom_int(v)) then
-    from_bool(!(Any..as_int!(v) == 0))
-  else if (Any..isfrom_float(v)) then
-    from_bool(!(Any..as_float!(v) == 0.0))
-  else if (Any..isfrom_string(v)) then
-    from_bool(!(Any..as_string!(v) == ""))
-  else if (Any..isfrom_ListAny(v)) then
-    from_bool(!(List_len(Any..as_ListAny!(v)) == 0))
-  else
-    exception(UndefinedError ("Operand Type is not defined"))
-}
-
-
-// /////////////////////////////////////////////////////////////////////////////////////
-// Modelling of Python binary operations
-// /////////////////////////////////////////////////////////////////////////////////////
-
-inline function PAdd (v1: Any, v2: Any) : Any
-{
-  if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
-  else if (Any..isfrom_bool(v1) && Any..isfrom_bool(v2)) then
-    from_int(bool_to_int(Any..as_bool!(v1)) + bool_to_int(Any..as_bool!(v2)))
-  else if (Any..isfrom_bool(v1) && Any..isfrom_int(v2)) then
-    from_int(bool_to_int(Any..as_bool!(v1)) + Any..as_int!(v2))
-  else if (Any..isfrom_int(v1) && Any..isfrom_bool(v2)) then
-    from_int(Any..as_int!(v1) + bool_to_int(Any..as_bool!(v2)))
-  else if (Any..isfrom_int(v1) && Any..isfrom_float(v2)) then
-    from_float(int_to_real(Any..as_int!(v1)) + Any..as_float!(v2))
-  else if (Any..isfrom_float(v1) && Any..isfrom_bool(v2)) then
-    from_float(Any..as_float!(v1) + bool_to_real(Any..as_bool!(v2)))
-  else if (Any..isfrom_int(v1) && Any..isfrom_int(v2)) then
-    from_int(Any..as_int!(v1) + Any..as_int!(v2))
-  else if (Any..isfrom_float(v1) && Any..isfrom_int(v2)) then
-    from_float(Any..as_float!(v1) + int_to_real(Any..as_int!(v2)) )
-  else if (Any..isfrom_float(v1) && Any..isfrom_float(v2)) then
-    from_float(Any..as_float!(v1) + Any..as_float!(v2))
-  else if (Any..isfrom_string(v1) && Any..isfrom_string(v2)) then
-    from_string(str.concat(Any..as_string!(v1),Any..as_string!(v2)))
-  else if (Any..isfrom_ListAny(v1) && Any..isfrom_ListAny(v2)) then
-    from_ListAny(List_extend(Any..as_ListAny!(v1),Any..as_ListAny!(v2)))
-  else if (Any..isfrom_datetime(v1) && Any..isfrom_int(v2)) then
-    from_datetime((Any..as_datetime!(v1) + Any..as_int!(v2)))
-  else
-    exception(UndefinedError ("Operand Type is not defined"))
-}
-
-
-inline function PSub (v1: Any, v2: Any) : Any
-{
-  if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
-  else if (Any..isfrom_bool(v1) && Any..isfrom_bool(v2)) then
-    from_int(bool_to_int(Any..as_bool!(v1)) - bool_to_int(Any..as_bool!(v2)))
-  else if (Any..isfrom_bool(v1) && Any..isfrom_int(v2)) then
-    from_int(bool_to_int(Any..as_bool!(v1)) - Any..as_int!(v2))
-  else if (Any..isfrom_int(v1) && Any..isfrom_bool(v2)) then
-    from_int(Any..as_int!(v1) - bool_to_int(Any..as_bool!(v2)))
-  else if (Any..isfrom_bool(v1) && Any..isfrom_float(v2)) then
-    from_float(bool_to_real(Any..as_bool!(v1)) - Any..as_float!(v2))
-  else if (Any..isfrom_float(v1) && Any..isfrom_bool(v2)) then
-    from_float(Any..as_float!(v1) - bool_to_real(Any..as_bool!(v2)))
-  else if (Any..isfrom_int(v1) && Any..isfrom_int(v2)) then
-    from_int(Any..as_int!(v1) - Any..as_int!(v2))
-  else if (Any..isfrom_int(v1) && Any..isfrom_float(v2)) then
-    from_float(int_to_real(Any..as_int!(v1)) - Any..as_float!(v2))
-  else if (Any..isfrom_float(v1) && Any..isfrom_int(v2)) then
-    from_float(Any..as_float!(v1) - int_to_real(Any..as_int!(v2)) )
-  else if (Any..isfrom_float(v1) && Any..isfrom_float(v2)) then
-    from_float(Any..as_float!(v1) - Any..as_float!(v2))
-  else if (Any..isfrom_datetime(v1) && Any..isfrom_int(v2)) then
-    from_datetime(Any..as_datetime!(v1) - Any..as_int!(v2))
-  else if (Any..isfrom_datetime(v1) && Any..isfrom_datetime(v2)) then
-    from_int(Any..as_datetime!(v1) - Any..as_datetime!(v2))
-  else
-    exception(UndefinedError ("Operand Type is not defined"))
-}
-
-
-function string_repeat (s: string, i: int) : string;
-
-inline function PMul (v1: Any, v2: Any) : Any
-{
-  if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
-  else if (Any..isfrom_bool(v1) && Any..isfrom_bool(v2)) then
-    from_int(bool_to_int(Any..as_bool!(v1)) * bool_to_int(Any..as_bool!(v2)))
-  else if (Any..isfrom_bool(v1) && Any..isfrom_int(v2)) then
-    from_int(bool_to_int(Any..as_bool!(v1)) * Any..as_int!(v2))
-  else if (Any..isfrom_int(v1) && Any..isfrom_bool(v2)) then
-    from_int(Any..as_int!(v1) * bool_to_int(Any..as_bool!(v2)))
-  else if (Any..isfrom_bool(v1) && Any..isfrom_float(v2)) then
-    from_float(bool_to_real(Any..as_bool!(v1)) * Any..as_float!(v2))
-  else if (Any..isfrom_float(v1) && Any..isfrom_bool(v2)) then
-    from_float(Any..as_float!(v1) * bool_to_real(Any..as_bool!(v2)))
-  else if (Any..isfrom_bool(v1) && Any..isfrom_string(v2)) then
-    if Any..as_bool!(v1) then v2 else from_string("")
-  else if (Any..isfrom_string(v1) && Any..isfrom_bool(v2)) then
-    if Any..as_bool!(v2) then v1 else from_string("")
-  else if (Any..isfrom_int(v1) && Any..isfrom_int(v2)) then
-    from_int(Any..as_int!(v1) * Any..as_int!(v2))
-  else if (Any..isfrom_int(v1) && Any..isfrom_float(v2)) then
-    from_float(int_to_real(Any..as_int!(v1)) * Any..as_float!(v2))
-  else if (Any..isfrom_float(v1) && Any..isfrom_int(v2)) then
-    from_float(Any..as_float!(v1) * int_to_real(Any..as_int!(v2)) )
-  else if (Any..isfrom_int(v1) && Any..isfrom_string(v2)) then
-    from_string(string_repeat(Any..as_string!(v2), Any..as_int!(v1)))
-  else if (Any..isfrom_string(v1) && Any..isfrom_int(v2)) then
-    from_string(string_repeat(Any..as_string!(v1), Any..as_int!(v2)))
-  else if (Any..isfrom_int(v1) && Any..isfrom_ListAny(v2)) then
-    from_ListAny(List_repeat(Any..as_ListAny!(v2), Any..as_int!(v1)))
-  else if (Any..isfrom_ListAny(v1) && Any..isfrom_int(v2)) then
-    from_ListAny(List_repeat(Any..as_ListAny!(v1), Any..as_int!(v2)))
-  else if (Any..isfrom_float(v1) && Any..isfrom_float(v2)) then
-    from_float(Any..as_float!(v1) * Any..as_float!(v2))
-  else
-    exception(UndefinedError ("Operand Type is not defined"))
-}
-
-inline function PFloorDiv (v1: Any, v2: Any) : Any
-  requires (Any..isfrom_bool(v2)==>Any..as_bool!(v2)) && (Any..isfrom_int(v2)==>Any..as_int!(v2)!=0);
-{
-  if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
-  else if (Any..isfrom_bool(v1) && Any..isfrom_bool(v2)) then
-    from_int( bool_to_int(Any..as_bool!(v1)) / bool_to_int(Any..as_bool!(v2)))
-  else if (Any..isfrom_bool(v1) && Any..isfrom_int(v2)) then
-    from_int(bool_to_int(Any..as_bool!(v1)) / Any..as_int!(v2))
-  else if (Any..isfrom_int(v1) && Any..isfrom_bool(v2)) then
-    from_int(Any..as_int!(v1) / bool_to_int(Any..as_bool!(v2)))
-  else if (Any..isfrom_int(v1) && Any..isfrom_int(v2)) then
-    from_int(Any..as_int!(v1) / Any..as_int!(v2))
-  else
-    exception(UndefinedError ("Operand Type is not defined"))
-}
-
-// /////////////////////////////////////////////////////////////////////////////////////
-// Modelling of Python comparision operations
-// /////////////////////////////////////////////////////////////////////////////////////
-
-function string_lt (s1: string, s2: string) : bool;
-function string_le (s1: string, s2: string) : bool;
-function string_gt (s1: string, s2: string) : bool;
-function string_ge (s1: string, s2: string) : bool;
-function List_lt (l1: ListAny, l2: ListAny): bool;
-function List_le (l1: ListAny, l2: ListAny): bool;
-function List_gt (l1: ListAny, l2: ListAny): bool;
-function List_ge (l1: ListAny, l2: ListAny): bool;
-
-inline function PLt (v1: Any, v2: Any) : Any
-{
-  if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
-  else if (Any..isfrom_bool(v1) && Any..isfrom_bool(v2)) then
-    from_bool(bool_to_int(Any..as_bool!(v1)) < bool_to_int(Any..as_bool!(v2)))
-  else if (Any..isfrom_bool(v1) && Any..isfrom_int(v2)) then
-    from_bool(bool_to_int(Any..as_bool!(v1)) < Any..as_int!(v2))
-  else if (Any..isfrom_int(v1) && Any..isfrom_bool(v2)) then
-    from_bool(Any..as_int!(v1) < bool_to_int(Any..as_bool!(v2)))
-  else if (Any..isfrom_bool(v1) && Any..isfrom_float(v2)) then
-    from_bool(bool_to_real(Any..as_bool!(v1)) < Any..as_float!(v2))
-  else if (Any..isfrom_float(v1) && Any..isfrom_bool(v2)) then
-    from_bool(Any..as_float!(v1) < bool_to_real(Any..as_bool!(v2)))
-  else if (Any..isfrom_int(v1) && Any..isfrom_int(v2)) then
-    from_bool(Any..as_int!(v1) < Any..as_int!(v2))
-  else if (Any..isfrom_int(v1) && Any..isfrom_float(v2)) then
-    from_bool(int_to_real(Any..as_int!(v1)) < Any..as_float!(v2))
-  else if (Any..isfrom_float(v1) && Any..isfrom_int(v2)) then
-    from_bool(Any..as_float!(v1) < int_to_real(Any..as_int!(v2)))
-  else if (Any..isfrom_float(v1) && Any..isfrom_float(v2)) then
-    from_bool(Any..as_float!(v1) < Any..as_float!(v2))
-  else if (Any..isfrom_string(v1) && Any..isfrom_string(v2)) then
-    from_bool(string_lt(Any..as_string!(v1), Any..as_string!(v2)))
-  else if (Any..isfrom_ListAny(v1) && Any..isfrom_ListAny(v2)) then
-    from_bool(List_lt(Any..as_ListAny!(v1),Any..as_ListAny!(v2)))
-  else if (Any..isfrom_datetime(v1) && Any..isfrom_datetime(v2)) then
-    from_bool(Any..as_datetime!(v1) <Any..as_datetime!(v2))
-  else
-    exception(UndefinedError ("Operand Type is not defined"))
-}
-
-inline function PLe (v1: Any, v2: Any) : Any
-{
-  if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
-  else if (Any..isfrom_bool(v1) && Any..isfrom_bool(v2)) then
-    from_bool(bool_to_int(Any..as_bool!(v1)) <= bool_to_int(Any..as_bool!(v2)))
-  else if (Any..isfrom_bool(v1) && Any..isfrom_int(v2)) then
-    from_bool(bool_to_int(Any..as_bool!(v1)) <= Any..as_int!(v2))
-  else if (Any..isfrom_int(v1) && Any..isfrom_bool(v2)) then
-    from_bool(Any..as_int!(v1) <= bool_to_int(Any..as_bool!(v2)))
-  else if (Any..isfrom_bool(v1) && Any..isfrom_float(v2)) then
-    from_bool(bool_to_real(Any..as_bool!(v1)) <= Any..as_float!(v2))
-  else if (Any..isfrom_float(v1) && Any..isfrom_bool(v2)) then
-    from_bool(Any..as_float!(v1) <= bool_to_real(Any..as_bool!(v2)))
-  else if (Any..isfrom_int(v1) && Any..isfrom_int(v2)) then
-    from_bool(Any..as_int!(v1) <= Any..as_int!(v2))
-  else if (Any..isfrom_int(v1) && Any..isfrom_float(v2)) then
-    from_bool(int_to_real(Any..as_int!(v1)) <= Any..as_float!(v2))
-  else if (Any..isfrom_float(v1) && Any..isfrom_int(v2)) then
-    from_bool(Any..as_float!(v1) <= int_to_real(Any..as_int!(v2)))
-  else if (Any..isfrom_float(v1) && Any..isfrom_float(v2)) then
-    from_bool(Any..as_float!(v1) <= Any..as_float!(v2))
-  else if (Any..isfrom_string(v1) && Any..isfrom_string(v2)) then
-    from_bool(string_le(Any..as_string!(v1), Any..as_string!(v2)))
-  else if (Any..isfrom_ListAny(v1) && Any..isfrom_ListAny(v2)) then
-    from_bool(List_le(Any..as_ListAny!(v1),Any..as_ListAny!(v2)))
-  else if (Any..isfrom_datetime(v1) && Any..isfrom_datetime(v2)) then
-    from_bool(Any..as_datetime!(v1) <=Any..as_datetime!(v2))
-  else
-    exception(UndefinedError ("Operand Type is not defined"))
-}
-
-inline function PGt (v1: Any, v2: Any) : Any
-{
-  if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
-  else if (Any..isfrom_bool(v1) && Any..isfrom_bool(v2)) then
-    from_bool(bool_to_int(Any..as_bool!(v1)) > bool_to_int(Any..as_bool!(v2)))
-  else if (Any..isfrom_bool(v1) && Any..isfrom_int(v2)) then
-    from_bool(bool_to_int(Any..as_bool!(v1)) > Any..as_int!(v2))
-  else if (Any..isfrom_int(v1) && Any..isfrom_bool(v2)) then
-    from_bool(Any..as_int!(v1) > bool_to_int(Any..as_bool!(v2)))
-  else if (Any..isfrom_bool(v1) && Any..isfrom_float(v2)) then
-    from_bool(bool_to_real(Any..as_bool!(v1)) > Any..as_float!(v2))
-  else if (Any..isfrom_float(v1) && Any..isfrom_bool(v2)) then
-    from_bool(Any..as_float!(v1) > bool_to_real(Any..as_bool!(v2)))
-  else if (Any..isfrom_int(v1) && Any..isfrom_int(v2)) then
-    from_bool(Any..as_int!(v1) > Any..as_int!(v2))
-  else if (Any..isfrom_int(v1) && Any..isfrom_float(v2)) then
-    from_bool(int_to_real(Any..as_int!(v1)) > Any..as_float!(v2))
-  else if (Any..isfrom_float(v1) && Any..isfrom_int(v2)) then
-    from_bool(Any..as_float!(v1) > int_to_real(Any..as_int!(v2)))
-  else if (Any..isfrom_float(v1) && Any..isfrom_float(v2)) then
-    from_bool(Any..as_float!(v1) > Any..as_float!(v2))
-  else if (Any..isfrom_string(v1) && Any..isfrom_string(v2)) then
-    from_bool(string_gt(Any..as_string!(v1), Any..as_string!(v2)))
-  else if (Any..isfrom_ListAny(v1) && Any..isfrom_ListAny(v2)) then
-    from_bool(List_gt(Any..as_ListAny!(v1),Any..as_ListAny!(v2)))
-  else if (Any..isfrom_datetime(v1) && Any..isfrom_datetime(v2)) then
-    from_bool(Any..as_datetime!(v1) >Any..as_datetime!(v2))
-  else
-    exception(UndefinedError ("Operand Type is not defined"))
-}
-
-inline function PGe (v1: Any, v2: Any) : Any
-{
-  if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
-  else if (Any..isfrom_bool(v1) && Any..isfrom_bool(v2)) then
-    from_bool(bool_to_int(Any..as_bool!(v1)) >= bool_to_int(Any..as_bool!(v2)))
-  else if (Any..isfrom_bool(v1) && Any..isfrom_int(v2)) then
-    from_bool(bool_to_int(Any..as_bool!(v1)) >= Any..as_int!(v2))
-  else if (Any..isfrom_int(v1) && Any..isfrom_bool(v2)) then
-    from_bool(Any..as_int!(v1) >= bool_to_int(Any..as_bool!(v2)))
-  else if (Any..isfrom_bool(v1) && Any..isfrom_float(v2)) then
-    from_bool(bool_to_real(Any..as_bool!(v1)) >= Any..as_float!(v2))
-  else if (Any..isfrom_float(v1) && Any..isfrom_bool(v2)) then
-    from_bool(Any..as_float!(v1) >= bool_to_real(Any..as_bool!(v2)))
-  else if (Any..isfrom_int(v1) && Any..isfrom_int(v2)) then
-    from_bool(Any..as_int!(v1) >= Any..as_int!(v2))
-  else if (Any..isfrom_int(v1) && Any..isfrom_float(v2)) then
-    from_bool(int_to_real(Any..as_int!(v1)) >= Any..as_float!(v2))
-  else if (Any..isfrom_float(v1) && Any..isfrom_int(v2)) then
-    from_bool(Any..as_float!(v1) >= int_to_real(Any..as_int!(v2)))
-  else if (Any..isfrom_float(v1) && Any..isfrom_float(v2)) then
-    from_bool(Any..as_float!(v1) >= Any..as_float!(v2))
-  else if (Any..isfrom_string(v1) && Any..isfrom_string(v2)) then
-    from_bool(string_ge(Any..as_string!(v1), Any..as_string!(v2)))
-  else if (Any..isfrom_ListAny(v1) && Any..isfrom_ListAny(v2)) then
-    from_bool(List_ge(Any..as_ListAny!(v1),Any..as_ListAny!(v2)))
-  else if (Any..isfrom_datetime(v1) && Any..isfrom_datetime(v2)) then
-    from_bool(Any..as_datetime!(v1) >=Any..as_datetime!(v2))
-  else
-    exception(UndefinedError ("Operand Type is not defined"))
-}
-
-inline function PEq (v: Any, v': Any) : Any {
-  from_bool(normalize_any(v) == normalize_any (v'))
-}
-
-inline function PNEq (v: Any, v': Any) : Any {
-  from_bool(normalize_any(v) != normalize_any (v'))
-}
-
-// /////////////////////////////////////////////////////////////////////////////////////
-// Modelling of Python Boolean operations And and Or
-// /////////////////////////////////////////////////////////////////////////////////////
-
-inline function PAnd (v1: Any, v2: Any) : Any
-  requires (Any..isfrom_bool(v1) || Any..isfrom_none(v1) || Any..isfrom_string(v1) || Any..isfrom_int(v1));
-{
-  if ! Any_to_bool (v1) then v1 else v2
-}
-
-inline function POr (v1: Any, v2: Any) : Any
-  requires (Any..isfrom_bool(v1) || Any..isfrom_none(v1) || Any..isfrom_string(v1) || Any..isfrom_int(v1));
-{
-  if Any_to_bool (v1) then v1 else v2
-}
-
-
-// /////////////////////////////////////////////////////////////////////////////////////
-// Modelling of other Python operations, currrently unsupported
-// /////////////////////////////////////////////////////////////////////////////////////
-inline function PPow (v1: Any, v2: Any) : Any
-{
-  exception(UnimplementedError ("Pow operator is not supported"))
-}
-
-inline function PMod (v1: Any, v2: Any) : Any
-{
-  exception(UnimplementedError ("Mod operator is not supported"))
-}
-
-// /////////////////////////////////////////////////////////////////////////////////////
-// Modelling of Python Boolean operations And and Or
-// /////////////////////////////////////////////////////////////////////////////////////
-
-
 // /////////////////////////////////////////////////////////////////////////////////////
 // Modelling some datetime-related Python operations, for testing purpose
 // /////////////////////////////////////////////////////////////////////////////////////
 
-function to_string(a: Any) : string;
-
-function to_string_any(a: Any) : Any {
-  from_string(to_string(a))
-}
-
-function datetime_strptime(dtstring: Any, format: Any) : Any;
-
-axiom [datetime_tostring_cancel]: forall dt: Any ::
-  datetime_strptime(to_string_any(dt), from_string ("%Y-%m-%d")) == dt;
-
-procedure datetime_date(d: Any) returns (ret: Any, error: Error)
-spec {
-  requires [d_type]: Any..isfrom_datetime(d);
-  ensures [ret_type]: Any..isfrom_datetime(ret) && Any..as_datetime!(ret) <= Any..as_datetime!(d);
-}
-{
-  var timedt: int;
-  if (Any..isfrom_datetime(d)) {
-    assume [timedt_le]: timedt <= Any..as_datetime!(d);
-    ret := from_datetime(timedt);
-    error := NoError();
-  }
-  else {
-    ret := from_none();
-    error := TypeError("Input must be datetime");
-  }
-};
-
-procedure datetime_now() returns (ret: Any)
-spec {
-  ensures [ret_type]: Any..isfrom_datetime(ret);
-}
-{
-  var d: int;
-  ret := from_datetime(d);
-};
-
-procedure timedelta_func (days: Any, hours: Any) returns (delta : Any, maybe_except: Error)
-spec{
-  requires [days_type]: Any..isfrom_none(days) || Any..isfrom_int(days);
-  requires [hours_type]: Any..isfrom_none(hours) || Any..isfrom_int(hours);
-  requires [days_pos]: Any..isfrom_int(days) ==> Any..as_int!(days)>=0;
-  requires [hours_pos]: Any..isfrom_int(hours) ==> Any..as_int!(hours)>=0;
-  ensures [ret_pos]: Any..isfrom_int(delta) && Any..as_int!(delta)>=0;
-}
-{
-  var days_i : int := 0;
-  if (Any..isfrom_int(days)) {
-        days_i := Any..as_int!(days);
-  }
-  var hours_i : int := 0;
-  if (Any..isfrom_int(hours)) {
-        hours_i := Any..as_int!(hours);
-  }
-  delta := from_int ((((days_i * 24) + hours_i) * 3600) * 1000000);
-};
-
-// /////////////////////////////////////////////////////////////////////////////////////
-// For testing purpose
-// /////////////////////////////////////////////////////////////////////////////////////
-
-procedure test_helper_procedure(req_name : Any, opt_name : Any) returns (ret: Any, maybe_except: Error)
-spec {
-  requires [req_name_is_foo]: req_name == from_string("foo");
-  requires [req_opt_name_none_or_str]: (Any..isfrom_none(opt_name)) || (Any..isfrom_string(opt_name));
-  requires [req_opt_name_none_or_bar]: (opt_name == from_none()) || (opt_name == from_string("bar"));
-  ensures [ensures_maybe_except_none]: (Error..isNoError(maybe_except));
-}
-{
-  assert [assert_name_is_foo]: req_name == from_string("foo");
-  assert [assert_opt_name_none_or_str]: (Any..isfrom_none(opt_name)) || (Any..isfrom_string(opt_name));
-  assert [assert_opt_name_none_or_bar]: (opt_name == from_none()) || (opt_name == from_string("bar"));
-  assume [assume_maybe_except_none]: (Error..isNoError(maybe_except));
-};
-
-procedure print(msg : Any) returns ();
-
 #end
 
 public section
@@ -952,8 +142,8 @@ These are declarations that cannot be expressed in Laurel grammar.
 The returned program includes forward declarations of types from the
 Laurel prelude; callers should filter out duplicates when merging.
 -/
-def pythonRuntimeCorePart : Core.Program :=
-  Core.getProgram pythonRuntimeCorePartDDM |>.fst
+def PythonLaurelCorePrelude : Core.Program :=
+  Core.getProgram PythonLaurelCorePreludeDDM |>.fst
 
 /--
 Get only the Core-only declarations, dropping the forward declarations
@@ -961,11 +151,11 @@ that precede the `type CoreOnlyDelimiter;` sentinel (and the sentinel itself).
 Everything after the delimiter is a genuine Core-only declaration.
 -/
 def coreOnlyFromRuntimeCorePart : List Core.Decl :=
-  let decls := pythonRuntimeCorePart.decls
+  let decls := PythonLaurelCorePrelude.decls
   -- Drop everything up to and including the CoreOnlyDelimiter sentinel
   match decls.dropWhile (fun d => d.name.name != "CoreOnlyDelimiter") with
   | _ :: rest => rest   -- drop the delimiter itself
-  | [] => dbg_trace "SOUND BUG: CoreOnlyDelimiter sentinel not found in pythonRuntimeCorePart"; []
+  | [] => dbg_trace "SOUND BUG: CoreOnlyDelimiter sentinel not found in PythonLaurelCorePrelude"; []
 
 end -- public section
 
diff --git a/Strata/Languages/Python/PythonRuntimeLaurelPart.lean b/Strata/Languages/Python/PythonRuntimeLaurelPart.lean
index 9de71728c..91afd0e15 100644
--- a/Strata/Languages/Python/PythonRuntimeLaurelPart.lean
+++ b/Strata/Languages/Python/PythonRuntimeLaurelPart.lean
@@ -13,7 +13,7 @@ namespace Python
 
 /--
 Python prelude declarations expressed in Laurel grammar.
-Converted from PythonLaurelCorePrelude.lean (Core dialect) to Laurel dialect.
+Converted from PythonRuntimeCorePart.lean (Core dialect) to Laurel dialect.
 
 Core-specific constructs that Laurel does not support:
 - `inline` keyword: noted in comments
@@ -97,8 +97,8 @@ datatype DictStrAny {
   DictStrAny_cons (key: string, val: Any, tail: DictStrAny)
 }
 
-// /////////////////////////////////////////////////////////////////////////////////////
-// Regex support — re.Match
+
+// Regex support — re.Match and re module functions
 //
 // Models Python's re.Match as a composite (reference) type following the
 // module_Class naming convention (re_Match).
@@ -109,8 +109,7 @@ datatype DictStrAny {
 // or from_ClassInstance wrapping a re_Match).  If the pipeline ever
 // moves to concrete types, these should return re_Match | None directly.
 //
-// Fields that can be determined from the call site are set concretely
-// in the Core-only prelude.  pos and endpos are sound as 0 / str.len
+// pos and endpos are sound as 0 / str.len
 // for the module-level re.match/re.search/re.fullmatch API which does
 // not accept pos/endpos arguments.  If compiled-pattern method calls
 // with explicit pos/endpos are supported later, those values must be
@@ -122,6 +121,31 @@ datatype DictStrAny {
 // over-approximation: the solver treats them as abstract, so
 // verification results involving these will be inconclusive rather
 // than unsound.
+//
+// Python signatures:
+//   re.compile(pattern: str) -> re.Pattern
+//   re.match(pattern: str | re.Pattern, string: str) -> re.Match | None
+//   re.search(pattern: str | re.Pattern, string: str) -> re.Match | None
+//   re.fullmatch(pattern: str | re.Pattern, string: str) -> re.Match | None
+//
+// Architecture:
+//
+// re.compile is a semantic no-op — it returns the pattern string unchanged.
+// The mode-specific factory functions re_fullmatch_bool, re_match_bool,
+// re_search_bool each compile a pattern+string pair to a Bool via
+// pythonRegexToCore, so anchors (^/$) are handled correctly per mode.
+// Their concreteEval fires when the pattern is a string literal; on
+// unsupported patterns it returns .none, leaving an uninterpreted Bool UF
+// (which produces `unknown` gracefully rather than a cvc5 theory-combination
+// error).
+//
+// On match, we return a from_ClassInstance wrapping a concrete re_Match
+// with pos=0 and endpos=str.len(s), which is sound for the module-level
+// API (no pos/endpos parameters).
+//
+// Mode-specific factory functions are declared via ReFactory (with concreteEval
+// for literal pattern expansion), not in this prelude, to avoid duplicate
+// definitions.
 
 composite re_Match {
   var re_match_string : string
@@ -139,7 +163,793 @@ function re_Match_lastindex  (self : re_Match) : int;
 function re_Match_lastgroup  (self : re_Match) : string;
 function re_Match_groups     (self : re_Match) : ListStr;
 
-datatype FIRST_END_MARKER { }
+function re_pattern_error(pattern : string) : Error
+  external;
+
+// The _bool variants are also factory functions (not inlined here) so that
+// unsupported patterns leave an uninterpreted Bool UF rather than an
+// uninterpreted RegLan UF.  An uninterpreted Bool UF produces `unknown`
+// gracefully; an uninterpreted RegLan UF causes cvc5 theory-combination errors.
+function re_fullmatch_bool(pattern : string, s : string) : bool
+  external;
+function re_match_bool(pattern : string, s : string) : bool
+  external;
+function re_search_bool(pattern : string, s : string) : bool
+  external;
+
+function Str.InRegEx(s: string, r: Core regex): bool external;
+function Str.Length(s: string): int external;
+
+// /////////////////////////////////////////////////////////////////////////////////////
+
+
+function mk_re_Match(s : string) : Any {
+  from_ClassInstance("re_Match",
+    DictStrAny_cons("re_match_string", from_string(s),
+      DictStrAny_cons("re_match_pos", from_int(0),
+        DictStrAny_cons("re_match_endpos", from_int(Str.Length(s)),
+          DictStrAny_empty()))))
+};
+
+// re.compile is a no-op: returns the pattern string unchanged.
+function re_compile(pattern : Any) : Any
+  requires Any..isfrom_string(pattern)
+{
+  pattern
+};
+
+function re_fullmatch(pattern : Any, s : Any) : Any
+  requires Any..isfrom_string(pattern) && Any..isfrom_string(s)
+{
+  if Error..isRePatternError(re_pattern_error(Any..as_string!(pattern)))
+  then exception(re_pattern_error(Any..as_string!(pattern)))
+  else if re_fullmatch_bool(Any..as_string!(pattern), Any..as_string!(s))
+       then mk_re_Match(Any..as_string!(s))
+       else from_none()
+};
+function re_match(pattern : Any, s : Any) : Any
+  requires Any..isfrom_string(pattern) && Any..isfrom_string(s)
+{
+  if Error..isRePatternError(re_pattern_error(Any..as_string!(pattern)))
+  then exception(re_pattern_error(Any..as_string!(pattern)))
+  else if re_match_bool(Any..as_string!(pattern), Any..as_string!(s))
+       then mk_re_Match(Any..as_string!(s))
+       else from_none()
+};
+function re_search(pattern : Any, s : Any) : Any
+  requires Any..isfrom_string(pattern) && Any..isfrom_string(s)
+{
+  if Error..isRePatternError(re_pattern_error(Any..as_string!(pattern)))
+  then exception(re_pattern_error(Any..as_string!(pattern)))
+  else if re_search_bool(Any..as_string!(pattern), Any..as_string!(s))
+       then mk_re_Match(Any..as_string!(s))
+       else from_none()
+};
+
+// /////////////////////////////////////////////////////////////////////////////////////
+//Functions that we provide to Python user
+//to write assertions/contracts about about types of variables
+
+function isBool (v: Any) : Any {
+  from_bool (Any..isfrom_bool(v))
+};
+
+function isInt (v: Any) : Any {
+  from_bool (Any..isfrom_int(v))
+};
+
+function isFloat (v: Any) : Any {
+  from_bool (Any..isfrom_float(v))
+};
+
+function isString (v: Any) : Any {
+  from_bool (Any..isfrom_string(v))
+};
+
+function isdatetime (v: Any) : Any {
+  from_bool (Any..isfrom_datetime(v))
+};
+
+function isDict (v: Any) : Any {
+  from_bool (Any..isfrom_Dict(v))
+};
+
+function isList (v: Any) : Any {
+  from_bool (Any..isfrom_ListAny(v))
+};
+
+function isClassInstance (v: Any) : Any {
+  from_bool (Any..isfrom_ClassInstance(v))
+};
+
+function isInstance_of_Int (v: Any) : Any {
+  from_bool (Any..isfrom_int(v) || Any..isfrom_bool(v))
+};
+
+function isInstance_of_Float (v: Any) : Any {
+  from_bool (Any..isfrom_float(v) || Any..isfrom_int(v) || Any..isfrom_bool(v))
+};
+
+// /////////////////////////////////////////////////////////////////////////////////////
+//Functions that we provide to Python user
+//to write assertions/contracts about about types of errors
+// /////////////////////////////////////////////////////////////////////////////////////
+
+function isTypeError (e: Error) : Any {
+  from_bool (Error..isTypeError(e))
+};
+
+function isAttributeError (e: Error) : Any {
+  from_bool (Error..isAttributeError(e))
+};
+
+function isAssertionError (e: Error) : Any {
+  from_bool (Error..isAssertionError(e))
+};
+
+function isUnimplementedError (e: Error) : Any {
+  from_bool (Error..isUnimplementedError(e))
+};
+
+function isUndefinedError (e: Error) : Any {
+  from_bool (Error..isUndefinedError(e))
+};
+
+function isError (e: Error) : bool {
+  ! Error..isNoError(e)
+};
+
+// /////////////////////////////////////////////////////////////////////////////////////
+//The following function convert Any type to bool
+//based on the Python definition of truthiness for basic types
+// https://docs.python.org/3/library/stdtypes.html
+// /////////////////////////////////////////////////////////////////////////////////////
+
+function Any_to_bool (v: Any) : bool
+  requires (Any..isfrom_bool(v) || Any..isfrom_none(v) || Any..isfrom_string(v) || Any..isfrom_int(v) || Any..isfrom_Dict(v) || Any..isfrom_ListAny(v))
+{
+  if (Any..isfrom_bool(v)) then Any..as_bool!(v) else
+  if (Any..isfrom_none(v)) then false else
+  if (Any..isfrom_string(v)) then !(Any..as_string!(v) == "") else
+  if (Any..isfrom_int(v)) then !(Any..as_int!(v) == 0) else
+  if (Any..isfrom_Dict(v)) then !(Any..as_Dict!(v) == DictStrAny_empty()) else
+  if (Any..isfrom_ListAny(v)) then !(Any..as_ListAny!(v) == ListAny_nil()) else
+  false
+  //WILL BE ADDED
+};
+
+// /////////////////////////////////////////////////////////////////////////////////////
+// ListAny functions
+// /////////////////////////////////////////////////////////////////////////////////////
+
+function List_len (l : ListAny) : int
+{
+  if ListAny..isListAny_nil(l) then 0 else 1 + List_len(ListAny..tail!(l))
+};
+
+procedure List_len_pos(l : ListAny)
+  invokeOn List_len(l)
+  ensures List_len(l) >= 0;
+
+function List_contains (l : ListAny, x: Any) : bool
+{
+  if ListAny..isListAny_nil(l) then false else (ListAny..head!(l) == x) || List_contains(ListAny..tail!(l), x)
+};
+
+function List_extend (l1 : ListAny, l2: ListAny) : ListAny
+{
+  if ListAny..isListAny_nil(l1) then l2
+  else ListAny_cons(ListAny..head!(l1), List_extend(ListAny..tail!(l1), l2))
+};
+
+function List_get (l : ListAny, i : int) : Any
+  requires i >= 0 && i < List_len(l)
+{
+  if ListAny..isListAny_nil(l) then from_none()
+  else if  i == 0 then ListAny..head!(l)
+  else List_get(ListAny..tail!(l), i - 1)
+};
+
+function List_take (l : ListAny, i: int) : ListAny
+  requires i >= 0 && i <= List_len(l)
+{
+  if ListAny..isListAny_nil(l) then ListAny_nil()
+  else if  i == 0 then ListAny_nil()
+  else ListAny_cons(ListAny..head!(l), List_take(ListAny..tail!(l), i - 1))
+};
+
+procedure List_take_len(l : ListAny, i: int)
+  invokeOn List_len(List_take(l,i))
+  ensures i >= 0 && i <= List_len(l) ==> List_len(List_take(l,i)) == i;
+
+function List_drop (l : ListAny, i: int) : ListAny
+  requires i >= 0 && i <= List_len(l)
+{
+  if ListAny..isListAny_nil(l) then ListAny_nil()
+  else if  i == 0 then l
+  else List_drop(ListAny..tail!(l), i - 1)
+};
+
+procedure List_drop_len(l : ListAny, i: int)
+  invokeOn List_len(List_drop(l,i))
+  ensures i >= 0 && i <= List_len(l) ==> List_len(List_drop(l,i)) == List_len(l) - i;
+
+function List_slice (l : ListAny, start : int, stop: int) : ListAny
+  requires start >= 0 && start < List_len(l) && stop >= 0 && stop <= List_len(l) && start <= stop
+{
+  List_take (List_drop (l, start), stop - start)
+};
+
+function List_set (l : ListAny, i : int, v: Any) : ListAny
+  requires i >= 0 && i < List_len(l)
+{
+  if ListAny..isListAny_nil(l) then ListAny_nil()
+  else if  i == 0 then ListAny_cons(v, ListAny..tail!(l))
+  else ListAny_cons(ListAny..head!(l), List_set(ListAny..tail!(l), i - 1, v))
+};
+
+//Require recursive function on int
+function List_repeat (l: ListAny, n: int): ListAny;
+
+// /////////////////////////////////////////////////////////////////////////////////////
+// DictStrAny functions
+// /////////////////////////////////////////////////////////////////////////////////////
+
+function DictStrAny_contains (d : DictStrAny, key: string) : bool
+{
+  if DictStrAny..isDictStrAny_empty(d) then false
+  else (DictStrAny..key!(d) == key) || DictStrAny_contains(DictStrAny..tail!(d), key)
+};
+
+function DictStrAny_get (d : DictStrAny, key: string) : Any
+  requires DictStrAny_contains(d, key)
+{
+  if  DictStrAny..isDictStrAny_empty(d) then from_none()
+  else if DictStrAny..key!(d) == key then DictStrAny..val!(d)
+  else DictStrAny_get(DictStrAny..tail!(d), key)
+};
+
+function DictStrAny_get_or_none (d : DictStrAny, key: string) : Any
+{
+  if DictStrAny_contains(d, key) then DictStrAny_get(d, key)
+  else from_none()
+};
+
+function Any_get_or_none (dict: Any, key: Any) : Any
+  requires Any..isfrom_Dict(dict) && Any..isfrom_string(key)
+{
+  DictStrAny_get_or_none(Any..as_Dict!(dict), Any..as_string!(key))
+};
+
+function DictStrAny_insert (d : DictStrAny, key: string, val: Any) : DictStrAny
+{
+  if DictStrAny..isDictStrAny_empty(d) then DictStrAny_cons(key, val, DictStrAny_empty())
+  else if DictStrAny..key!(d) == key then DictStrAny_cons(key, val, DictStrAny..tail!(d))
+  else DictStrAny_cons(DictStrAny..key!(d), DictStrAny..val!(d), DictStrAny_insert(DictStrAny..tail!(d), key, val))
+};
+
+function Any_get (dictOrList: Any, index: Any): Any
+  requires  (Any..isfrom_Dict(dictOrList) && Any..isfrom_string(index) && DictStrAny_contains(Any..as_Dict!(dictOrList), Any..as_string!(index))) ||
+            (Any..isfrom_ListAny(dictOrList) && Any..isfrom_int(index) && Any..as_int!(index) >= 0 && Any..as_int!(index) < List_len(Any..as_ListAny!(dictOrList)))||
+            (Any..isfrom_ListAny(dictOrList) && Any..isfrom_Slice(index) && Any..start!(index) >= 0 && Any..start!(index) < List_len(Any..as_ListAny!(dictOrList)) &&
+                ((OptionInt..isSome(Any..stop!(index))) &&  OptionInt..unwrap!(Any..stop!(index)) >= 0 && OptionInt..unwrap!(Any..stop!(index)) <= List_len(Any..as_ListAny!(dictOrList)) && Any..start!(index) <= OptionInt..unwrap!(Any..stop!(index))
+                  || (OptionInt..isNone(Any..stop!(index)))))
+{
+  if Any..isfrom_Dict(dictOrList) then
+    DictStrAny_get(Any..as_Dict!(dictOrList), Any..as_string!(index))
+  else if Any..isfrom_ListAny(dictOrList) && Any..isfrom_int(index) then
+    List_get(Any..as_ListAny!(dictOrList), Any..as_int!(index))
+  else if Any..isfrom_ListAny(dictOrList) && Any..isfrom_Slice(index) && OptionInt..isSome(Any..stop!(index)) then
+    from_ListAny(List_slice(Any..as_ListAny!(dictOrList), Any..start!(index), OptionInt..unwrap!(Any..stop!(index))))
+  else
+    from_ListAny(List_drop(Any..as_ListAny!(dictOrList), Any..start!(index)))
+};
+
+function Any_get! (dictOrList: Any, index: Any): Any
+{
+  if Any..isexception(dictOrList) then dictOrList
+  else if Any..isexception(index) then index
+  else if !(Any..isfrom_Dict(dictOrList) && Any..isfrom_string(index)) && !(Any..isfrom_ListAny(dictOrList) && Any..isfrom_int(index)) then
+    exception (TypeError("Invalid subscription type"))
+  else if Any..isfrom_Dict(dictOrList) && Any..isfrom_string(index) && DictStrAny_contains(Any..as_Dict!(dictOrList), Any..as_string!(index)) then
+    DictStrAny_get(Any..as_Dict!(dictOrList), Any..as_string!(index))
+  else if Any..isfrom_ListAny(dictOrList) && Any..isfrom_int(index) && Any..as_int!(index) >= 0 && Any..as_int!(index) < List_len(Any..as_ListAny!(dictOrList)) then
+    List_get(Any..as_ListAny!(dictOrList), Any..as_int!(index))
+  else
+    exception (IndexError("Invalid subscription"))
+};
+
+function Any_set (dictOrList: Any, index: Any, val: Any): Any
+  requires  (Any..isfrom_Dict(dictOrList) && Any..isfrom_string(index)) ||
+            (Any..isfrom_ListAny(dictOrList) && Any..isfrom_int(index) && Any..as_int!(index) >= 0 && Any..as_int!(index) < List_len(Any..as_ListAny!(dictOrList)))
+{
+  if Any..isfrom_Dict(dictOrList) then
+    from_Dict(DictStrAny_insert(Any..as_Dict!(dictOrList), Any..as_string!(index), val))
+  else
+    from_ListAny(List_set(Any..as_ListAny!(dictOrList), Any..as_int!(index), val))
+};
+
+function Any_set! (dictOrList: Any, index: Any, val: Any): Any
+{
+  if Any..isexception(dictOrList) then dictOrList
+  else if Any..isexception(index) then index
+  else if Any..isexception(val) then val
+  else if !(Any..isfrom_Dict(dictOrList) && Any..isfrom_string(index)) && !(Any..isfrom_ListAny(dictOrList) && Any..isfrom_int(index)) then
+    exception (TypeError("Invalid subscription type"))
+  else if Any..isfrom_Dict(dictOrList) && Any..isfrom_string(index) then
+    from_Dict(DictStrAny_insert(Any..as_Dict!(dictOrList), Any..as_string!(index), val))
+  else if Any..isfrom_ListAny(dictOrList) && Any..isfrom_int(index) && Any..as_int!(index) >= 0 && Any..as_int!(index) < List_len(Any..as_ListAny!(dictOrList)) then
+    from_ListAny(List_set(Any..as_ListAny!(dictOrList), Any..as_int!(index), val))
+  else
+    exception (IndexError("Index out of bound"))
+};
+
+function Any_sets (indices: ListAny, dictOrList: Any, val: Any): Any
+{
+  if ListAny..isListAny_nil(indices) then dictOrList
+  else if ListAny..isListAny_nil(ListAny..tail!(indices)) then Any_set!(dictOrList, ListAny..head!(indices), val)
+  else Any_set!(dictOrList, ListAny..head!(indices),
+    Any_sets(ListAny..tail!(indices), Any_get!(dictOrList, ListAny..head!(indices)), val))
+};
+
+function PIn (v: Any, dictOrList: Any) : Any
+  requires (Any..isfrom_Dict(dictOrList) && Any..isfrom_string(v)) || Any..isfrom_ListAny(dictOrList)
+{
+  from_bool(
+    if Any..isfrom_Dict(dictOrList) then
+      DictStrAny_contains(Any..as_Dict!(dictOrList), Any..as_string!(v))
+    else
+      List_contains(Any..as_ListAny!(dictOrList), v)
+  )
+};
+
+function PNotIn ( v: Any, dictOrList: Any) : Any
+  requires (Any..isfrom_Dict(dictOrList) && Any..isfrom_string(v)) || Any..isfrom_ListAny(dictOrList)
+{
+  from_bool(
+    if Any..isfrom_Dict(dictOrList) then
+      !DictStrAny_contains(Any..as_Dict!(dictOrList), Any..as_string!(v))
+    else
+      !List_contains(Any..as_ListAny!(dictOrList), v)
+  )
+};
+
+// /////////////////////////////////////////////////////////////////////////////////////
+// Python treats some values of different types to be equivalent
+// This function models that behavior
+// /////////////////////////////////////////////////////////////////////////////////////
+
+function is_IntReal (v: Any) : bool;
+function Any_real_to_int (v: Any) : int;
+
+function normalize_any (v : Any) : Any {
+  if v == from_bool(true) then from_int(1)
+  else (if v == from_bool(false) then from_int(0) else
+        if Any..isfrom_float(v) && is_IntReal(v) then from_int(Any_real_to_int(v)) else
+        v)
+};
+
+
+// /////////////////////////////////////////////////////////////////////////////////////
+// MODELLING PYTHON OPERATIONS
+// Note that there is no official document that define the semantic of Python operations
+// The model of them in this prelude is based on experiments of basic types
+// /////////////////////////////////////////////////////////////////////////////////////
+
+
+// /////////////////////////////////////////////////////////////////////////////////////
+// This function convert an int to a real
+// Need to connect to an SMT function
+function int_to_real (i: int) : real;
+
+// /////////////////////////////////////////////////////////////////////////////////////
+// Converting bool to int or real
+// Used to in Python binary operators' modelling
+function bool_to_int (bval: bool) : int {if bval then 1 else 0};
+function bool_to_real (b: bool) : real {if b then 1.0 else 0.0};
+
+// /////////////////////////////////////////////////////////////////////////////////////
+// Modelling of Python unary operations
+// /////////////////////////////////////////////////////////////////////////////////////
+
+function PNeg (v: Any) : Any
+{
+  if Any..isexception(v) then v
+  else if Any..isfrom_bool(v) then
+    from_int(- bool_to_int(Any..as_bool!(v)))
+  else if Any..isfrom_int(v) then
+    from_int(- Any..as_int!(v))
+  else if Any..isfrom_float(v) then
+    from_float(- Any..as_float!(v))
+  else
+    exception(UndefinedError ("Operand Type is not defined"))
+};
+
+function PNot (v: Any) : Any
+{
+  if Any..isexception(v) then v
+  else if Any..isfrom_bool(v) then
+    from_bool(!(Any..as_bool!(v)))
+  else if Any..isfrom_int(v) then
+    from_bool(!(Any..as_int!(v) == 0))
+  else if Any..isfrom_float(v) then
+    from_bool(!(Any..as_float!(v) == 0.0))
+  else if Any..isfrom_string(v) then
+    from_bool(!(Any..as_string!(v) == ""))
+  else if Any..isfrom_ListAny(v) then
+    from_bool(!(List_len(Any..as_ListAny!(v)) == 0))
+  else
+    exception(UndefinedError ("Operand Type is not defined"))
+};
+
+// /////////////////////////////////////////////////////////////////////////////////////
+// Modelling of Python binary operations
+// /////////////////////////////////////////////////////////////////////////////////////
+
+function Str.Concat(s: string, s2: string): string external;
+
+function PAdd (v1: Any, v2: Any) : Any
+{
+  if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
+  else if Any..isfrom_bool(v1) && Any..isfrom_bool(v2) then
+    from_int(bool_to_int(Any..as_bool!(v1)) + bool_to_int(Any..as_bool!(v2)))
+  else if Any..isfrom_bool(v1) && Any..isfrom_int(v2) then
+    from_int(bool_to_int(Any..as_bool!(v1)) + Any..as_int!(v2))
+  else if Any..isfrom_int(v1) && Any..isfrom_bool(v2) then
+    from_int(Any..as_int!(v1) + bool_to_int(Any..as_bool!(v2)))
+  else if Any..isfrom_int(v1) && Any..isfrom_float(v2) then
+    from_float(int_to_real(Any..as_int!(v1)) + Any..as_float!(v2))
+  else if Any..isfrom_float(v1) && Any..isfrom_bool(v2) then
+    from_float(Any..as_float!(v1) + bool_to_real(Any..as_bool!(v2)))
+  else if Any..isfrom_int(v1) && Any..isfrom_int(v2) then
+    from_int(Any..as_int!(v1) + Any..as_int!(v2))
+  else if Any..isfrom_float(v1) && Any..isfrom_int(v2) then
+    from_float(Any..as_float!(v1) + int_to_real(Any..as_int!(v2)) )
+  else if Any..isfrom_float(v1) && Any..isfrom_float(v2) then
+    from_float(Any..as_float!(v1) + Any..as_float!(v2))
+  else if Any..isfrom_string(v1) && Any..isfrom_string(v2) then
+    from_string(Str.Concat(Any..as_string!(v1),Any..as_string!(v2)))
+  else if Any..isfrom_ListAny(v1) && Any..isfrom_ListAny(v2) then
+    from_ListAny(List_extend(Any..as_ListAny!(v1),Any..as_ListAny!(v2)))
+  else if Any..isfrom_datetime(v1) && Any..isfrom_int(v2) then
+    from_datetime((Any..as_datetime!(v1) + Any..as_int!(v2)))
+  else
+    exception(UndefinedError ("Operand Type is not defined"))
+};
+
+function PSub (v1: Any, v2: Any) : Any
+{
+  if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
+  else if Any..isfrom_bool(v1) && Any..isfrom_bool(v2) then
+    from_int(bool_to_int(Any..as_bool!(v1)) - bool_to_int(Any..as_bool!(v2)))
+  else if Any..isfrom_bool(v1) && Any..isfrom_int(v2) then
+    from_int(bool_to_int(Any..as_bool!(v1)) - Any..as_int!(v2))
+  else if Any..isfrom_int(v1) && Any..isfrom_bool(v2) then
+    from_int(Any..as_int!(v1) - bool_to_int(Any..as_bool!(v2)))
+  else if Any..isfrom_bool(v1) && Any..isfrom_float(v2) then
+    from_float(bool_to_real(Any..as_bool!(v1)) - Any..as_float!(v2))
+  else if Any..isfrom_float(v1) && Any..isfrom_bool(v2) then
+    from_float(Any..as_float!(v1) - bool_to_real(Any..as_bool!(v2)))
+  else if Any..isfrom_int(v1) && Any..isfrom_int(v2) then
+    from_int(Any..as_int!(v1) - Any..as_int!(v2))
+  else if Any..isfrom_int(v1) && Any..isfrom_float(v2) then
+    from_float(int_to_real(Any..as_int!(v1)) - Any..as_float!(v2))
+  else if Any..isfrom_float(v1) && Any..isfrom_int(v2) then
+    from_float(Any..as_float!(v1) - int_to_real(Any..as_int!(v2)) )
+  else if Any..isfrom_float(v1) && Any..isfrom_float(v2) then
+    from_float(Any..as_float!(v1) - Any..as_float!(v2))
+  else if Any..isfrom_datetime(v1) && Any..isfrom_int(v2) then
+    from_datetime(Any..as_datetime!(v1) - Any..as_int!(v2))
+  else if Any..isfrom_datetime(v1) && Any..isfrom_datetime(v2) then
+    from_int(Any..as_datetime!(v1) - Any..as_datetime!(v2))
+  else
+    exception(UndefinedError ("Operand Type is not defined"))
+};
+
+function string_repeat (s: string, i: int) : string;
+
+function PMul (v1: Any, v2: Any) : Any
+{
+  if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
+  else if Any..isfrom_bool(v1) && Any..isfrom_bool(v2) then
+    from_int(bool_to_int(Any..as_bool!(v1)) * bool_to_int(Any..as_bool!(v2)))
+  else if Any..isfrom_bool(v1) && Any..isfrom_int(v2) then
+    from_int(bool_to_int(Any..as_bool!(v1)) * Any..as_int!(v2))
+  else if Any..isfrom_int(v1) && Any..isfrom_bool(v2) then
+    from_int(Any..as_int!(v1) * bool_to_int(Any..as_bool!(v2)))
+  else if Any..isfrom_bool(v1) && Any..isfrom_float(v2) then
+    from_float(bool_to_real(Any..as_bool!(v1)) * Any..as_float!(v2))
+  else if Any..isfrom_float(v1) && Any..isfrom_bool(v2) then
+    from_float(Any..as_float!(v1) * bool_to_real(Any..as_bool!(v2)))
+  else if Any..isfrom_bool(v1) && Any..isfrom_string(v2) then
+    if Any..as_bool!(v1) then v2 else from_string("")
+  else if Any..isfrom_string(v1) && Any..isfrom_bool(v2) then
+    if Any..as_bool!(v2) then v1 else from_string("")
+  else if Any..isfrom_int(v1) && Any..isfrom_int(v2) then
+    from_int(Any..as_int!(v1) * Any..as_int!(v2))
+  else if Any..isfrom_int(v1) && Any..isfrom_float(v2) then
+    from_float(int_to_real(Any..as_int!(v1)) * Any..as_float!(v2))
+  else if Any..isfrom_float(v1) && Any..isfrom_int(v2) then
+    from_float(Any..as_float!(v1) * int_to_real(Any..as_int!(v2)) )
+  else if Any..isfrom_int(v1) && Any..isfrom_string(v2) then
+    from_string(string_repeat(Any..as_string!(v2), Any..as_int!(v1)))
+  else if Any..isfrom_string(v1) && Any..isfrom_int(v2) then
+    from_string(string_repeat(Any..as_string!(v1), Any..as_int!(v2)))
+  else if Any..isfrom_int(v1) && Any..isfrom_ListAny(v2) then
+    from_ListAny(List_repeat(Any..as_ListAny!(v2), Any..as_int!(v1)))
+  else if Any..isfrom_ListAny(v1) && Any..isfrom_int(v2) then
+    from_ListAny(List_repeat(Any..as_ListAny!(v1), Any..as_int!(v2)))
+  else if Any..isfrom_float(v1) && Any..isfrom_float(v2) then
+    from_float(Any..as_float!(v1) * Any..as_float!(v2))
+  else
+    exception(UndefinedError ("Operand Type is not defined"))
+};
+
+function PFloorDiv (v1: Any, v2: Any) : Any
+  requires (Any..isfrom_bool(v2)==>Any..as_bool!(v2)) && (Any..isfrom_int(v2)==>Any..as_int!(v2)!=0)
+{
+  if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
+  else if Any..isfrom_bool(v1) && Any..isfrom_bool(v2) then
+    from_int( bool_to_int(Any..as_bool!(v1)) / bool_to_int(Any..as_bool!(v2)))
+  else if Any..isfrom_bool(v1) && Any..isfrom_int(v2) then
+    from_int(bool_to_int(Any..as_bool!(v1)) / Any..as_int!(v2))
+  else if Any..isfrom_int(v1) && Any..isfrom_bool(v2) then
+    from_int(Any..as_int!(v1) / bool_to_int(Any..as_bool!(v2)))
+  else if Any..isfrom_int(v1) && Any..isfrom_int(v2) then
+    from_int(Any..as_int!(v1) / Any..as_int!(v2))
+  else
+    exception(UndefinedError ("Operand Type is not defined"))
+};
+
+// /////////////////////////////////////////////////////////////////////////////////////
+// Modelling of Python comparision operations
+// /////////////////////////////////////////////////////////////////////////////////////
+
+function string_lt (s1: string, s2: string) : bool;
+function string_le (s1: string, s2: string) : bool;
+function string_gt (s1: string, s2: string) : bool;
+function string_ge (s1: string, s2: string) : bool;
+function List_lt (l1: ListAny, l2: ListAny): bool;
+function List_le (l1: ListAny, l2: ListAny): bool;
+function List_gt (l1: ListAny, l2: ListAny): bool;
+function List_ge (l1: ListAny, l2: ListAny): bool;
+
+function PLt (v1: Any, v2: Any) : Any
+{
+  if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
+  else if Any..isfrom_bool(v1) && Any..isfrom_bool(v2) then
+    from_bool(bool_to_int(Any..as_bool!(v1)) < bool_to_int(Any..as_bool!(v2)))
+  else if Any..isfrom_bool(v1) && Any..isfrom_int(v2) then
+    from_bool(bool_to_int(Any..as_bool!(v1)) < Any..as_int!(v2))
+  else if Any..isfrom_int(v1) && Any..isfrom_bool(v2) then
+    from_bool(Any..as_int!(v1) < bool_to_int(Any..as_bool!(v2)))
+  else if Any..isfrom_bool(v1) && Any..isfrom_float(v2) then
+    from_bool(bool_to_real(Any..as_bool!(v1)) < Any..as_float!(v2))
+  else if Any..isfrom_float(v1) && Any..isfrom_bool(v2) then
+    from_bool(Any..as_float!(v1) < bool_to_real(Any..as_bool!(v2)))
+  else if Any..isfrom_int(v1) && Any..isfrom_int(v2) then
+    from_bool(Any..as_int!(v1) < Any..as_int!(v2))
+  else if Any..isfrom_int(v1) && Any..isfrom_float(v2) then
+    from_bool(int_to_real(Any..as_int!(v1)) < Any..as_float!(v2))
+  else if Any..isfrom_float(v1) && Any..isfrom_int(v2) then
+    from_bool(Any..as_float!(v1) < int_to_real(Any..as_int!(v2)))
+  else if Any..isfrom_float(v1) && Any..isfrom_float(v2) then
+    from_bool(Any..as_float!(v1) < Any..as_float!(v2))
+  else if Any..isfrom_string(v1) && Any..isfrom_string(v2) then
+    from_bool(string_lt(Any..as_string!(v1), Any..as_string!(v2)))
+  else if Any..isfrom_ListAny(v1) && Any..isfrom_ListAny(v2) then
+    from_bool(List_lt(Any..as_ListAny!(v1),Any..as_ListAny!(v2)))
+  else if Any..isfrom_datetime(v1) && Any..isfrom_datetime(v2) then
+    from_bool(Any..as_datetime!(v1) <Any..as_datetime!(v2))
+  else
+    exception(UndefinedError ("Operand Type is not defined"))
+};
+
+function PLe (v1: Any, v2: Any) : Any
+{
+  if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
+  else if Any..isfrom_bool(v1) && Any..isfrom_bool(v2) then
+    from_bool(bool_to_int(Any..as_bool!(v1)) <= bool_to_int(Any..as_bool!(v2)))
+  else if Any..isfrom_bool(v1) && Any..isfrom_int(v2) then
+    from_bool(bool_to_int(Any..as_bool!(v1)) <= Any..as_int!(v2))
+  else if Any..isfrom_int(v1) && Any..isfrom_bool(v2) then
+    from_bool(Any..as_int!(v1) <= bool_to_int(Any..as_bool!(v2)))
+  else if Any..isfrom_bool(v1) && Any..isfrom_float(v2) then
+    from_bool(bool_to_real(Any..as_bool!(v1)) <= Any..as_float!(v2))
+  else if Any..isfrom_float(v1) && Any..isfrom_bool(v2) then
+    from_bool(Any..as_float!(v1) <= bool_to_real(Any..as_bool!(v2)))
+  else if Any..isfrom_int(v1) && Any..isfrom_int(v2) then
+    from_bool(Any..as_int!(v1) <= Any..as_int!(v2))
+  else if Any..isfrom_int(v1) && Any..isfrom_float(v2) then
+    from_bool(int_to_real(Any..as_int!(v1)) <= Any..as_float!(v2))
+  else if Any..isfrom_float(v1) && Any..isfrom_int(v2) then
+    from_bool(Any..as_float!(v1) <= int_to_real(Any..as_int!(v2)))
+  else if Any..isfrom_float(v1) && Any..isfrom_float(v2) then
+    from_bool(Any..as_float!(v1) <= Any..as_float!(v2))
+  else if Any..isfrom_string(v1) && Any..isfrom_string(v2) then
+    from_bool(string_le(Any..as_string!(v1), Any..as_string!(v2)))
+  else if Any..isfrom_ListAny(v1) && Any..isfrom_ListAny(v2) then
+    from_bool(List_le(Any..as_ListAny!(v1),Any..as_ListAny!(v2)))
+  else if Any..isfrom_datetime(v1) && Any..isfrom_datetime(v2) then
+    from_bool(Any..as_datetime!(v1) <=Any..as_datetime!(v2))
+  else
+    exception(UndefinedError ("Operand Type is not defined"))
+};
+
+function PGt (v1: Any, v2: Any) : Any
+{
+  if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
+  else if Any..isfrom_bool(v1) && Any..isfrom_bool(v2) then
+    from_bool(bool_to_int(Any..as_bool!(v1)) > bool_to_int(Any..as_bool!(v2)))
+  else if Any..isfrom_bool(v1) && Any..isfrom_int(v2) then
+    from_bool(bool_to_int(Any..as_bool!(v1)) > Any..as_int!(v2))
+  else if Any..isfrom_int(v1) && Any..isfrom_bool(v2) then
+    from_bool(Any..as_int!(v1) > bool_to_int(Any..as_bool!(v2)))
+  else if Any..isfrom_bool(v1) && Any..isfrom_float(v2) then
+    from_bool(bool_to_real(Any..as_bool!(v1)) > Any..as_float!(v2))
+  else if Any..isfrom_float(v1) && Any..isfrom_bool(v2) then
+    from_bool(Any..as_float!(v1) > bool_to_real(Any..as_bool!(v2)))
+  else if Any..isfrom_int(v1) && Any..isfrom_int(v2) then
+    from_bool(Any..as_int!(v1) > Any..as_int!(v2))
+  else if Any..isfrom_int(v1) && Any..isfrom_float(v2) then
+    from_bool(int_to_real(Any..as_int!(v1)) > Any..as_float!(v2))
+  else if Any..isfrom_float(v1) && Any..isfrom_int(v2) then
+    from_bool(Any..as_float!(v1) > int_to_real(Any..as_int!(v2)))
+  else if Any..isfrom_float(v1) && Any..isfrom_float(v2) then
+    from_bool(Any..as_float!(v1) > Any..as_float!(v2))
+  else if Any..isfrom_string(v1) && Any..isfrom_string(v2) then
+    from_bool(string_gt(Any..as_string!(v1), Any..as_string!(v2)))
+  else if Any..isfrom_ListAny(v1) && Any..isfrom_ListAny(v2) then
+    from_bool(List_gt(Any..as_ListAny!(v1),Any..as_ListAny!(v2)))
+  else if Any..isfrom_datetime(v1) && Any..isfrom_datetime(v2) then
+    from_bool(Any..as_datetime!(v1) >Any..as_datetime!(v2))
+  else
+    exception(UndefinedError ("Operand Type is not defined"))
+};
+
+function PGe (v1: Any, v2: Any) : Any
+{
+  if Any..isexception(v1) then v1 else if Any..isexception(v2) then v2
+  else if Any..isfrom_bool(v1) && Any..isfrom_bool(v2) then
+    from_bool(bool_to_int(Any..as_bool!(v1)) >= bool_to_int(Any..as_bool!(v2)))
+  else if Any..isfrom_bool(v1) && Any..isfrom_int(v2) then
+    from_bool(bool_to_int(Any..as_bool!(v1)) >= Any..as_int!(v2))
+  else if Any..isfrom_int(v1) && Any..isfrom_bool(v2) then
+    from_bool(Any..as_int!(v1) >= bool_to_int(Any..as_bool!(v2)))
+  else if Any..isfrom_bool(v1) && Any..isfrom_float(v2) then
+    from_bool(bool_to_real(Any..as_bool!(v1)) >= Any..as_float!(v2))
+  else if Any..isfrom_float(v1) && Any..isfrom_bool(v2) then
+    from_bool(Any..as_float!(v1) >= bool_to_real(Any..as_bool!(v2)))
+  else if Any..isfrom_int(v1) && Any..isfrom_int(v2) then
+    from_bool(Any..as_int!(v1) >= Any..as_int!(v2))
+  else if Any..isfrom_int(v1) && Any..isfrom_float(v2) then
+    from_bool(int_to_real(Any..as_int!(v1)) >= Any..as_float!(v2))
+  else if Any..isfrom_float(v1) && Any..isfrom_int(v2) then
+    from_bool(Any..as_float!(v1) >= int_to_real(Any..as_int!(v2)))
+  else if Any..isfrom_float(v1) && Any..isfrom_float(v2) then
+    from_bool(Any..as_float!(v1) >= Any..as_float!(v2))
+  else if Any..isfrom_string(v1) && Any..isfrom_string(v2) then
+    from_bool(string_ge(Any..as_string!(v1), Any..as_string!(v2)))
+  else if Any..isfrom_ListAny(v1) && Any..isfrom_ListAny(v2) then
+    from_bool(List_ge(Any..as_ListAny!(v1),Any..as_ListAny!(v2)))
+  else if Any..isfrom_datetime(v1) && Any..isfrom_datetime(v2) then
+    from_bool(Any..as_datetime!(v1) >=Any..as_datetime!(v2))
+  else
+    exception(UndefinedError ("Operand Type is not defined"))
+};
+
+function PEq (v: Any, v': Any) : Any {
+  from_bool(normalize_any(v) == normalize_any (v'))
+};
+
+function PNEq (v: Any, v': Any) : Any {
+  from_bool(normalize_any(v) != normalize_any (v'))
+};
+
+// /////////////////////////////////////////////////////////////////////////////////////
+// Modelling of Python Boolean operations And and Or
+// /////////////////////////////////////////////////////////////////////////////////////
+
+function PAnd (v1: Any, v2: Any) : Any
+  requires (Any..isfrom_bool(v1) || Any..isfrom_none(v1) || Any..isfrom_string(v1) || Any..isfrom_int(v1))
+{
+  if ! Any_to_bool (v1) then v1 else v2
+};
+
+function POr (v1: Any, v2: Any) : Any
+  requires (Any..isfrom_bool(v1) || Any..isfrom_none(v1) || Any..isfrom_string(v1) || Any..isfrom_int(v1))
+{
+  if Any_to_bool (v1) then v1 else v2
+};
+
+// /////////////////////////////////////////////////////////////////////////////////////
+// Modelling of other Python operations, currrently unsupported
+// /////////////////////////////////////////////////////////////////////////////////////
+function PPow (v1: Any, v2: Any) : Any
+{
+  exception(UnimplementedError ("Pow operator is not supported"))
+};
+
+function PMod (v1: Any, v2: Any) : Any
+{
+  exception(UnimplementedError ("Mod operator is not supported"))
+};
+
+// /////////////////////////////////////////////////////////////////////////////////////
+// Modelling some datetime-related Python operations, for testing purpose
+// /////////////////////////////////////////////////////////////////////////////////////
+
+function to_string(a: Any) : string;
+
+function to_string_any(a: Any) : Any {
+  from_string(to_string(a))
+};
+
+function datetime_strptime(dtstring: Any, format: Any) : Any;
+
+procedure datetime_tostring_cancel(dt: Any)
+  invokeOn datetime_strptime(to_string_any(dt), from_string ("%Y-%m-%d"))
+  ensures datetime_strptime(to_string_any(dt), from_string ("%Y-%m-%d")) == dt;
+
+procedure datetime_date(d: Any) returns (ret: Any, error: Error)
+  requires Any..isfrom_datetime(d) summary "(Origin_datetime_date_Requires)d_type"
+  ensures Any..isfrom_datetime(ret) && Any..as_datetime!(ret) <= Any..as_datetime!(d) summary "ret_type"
+{
+  var timedt: int;
+  if Any..isfrom_datetime(d) then {
+    // summary "timedt_le";
+    assume timedt <= Any..as_datetime!(d);
+    ret := from_datetime(timedt);
+    error := NoError()
+  }
+  else {
+    ret := from_none();
+    error := TypeError("Input must be datetime")
+  }
+};
+
+procedure datetime_now() returns (ret: Any)
+  ensures Any..isfrom_datetime(ret) summary "ret_type"
+{
+  var d: int;
+  ret := from_datetime(d)
+};
+
+procedure timedelta_func(days: Any, hours: Any) returns (delta : Any, maybe_except: Error)
+  requires Any..isfrom_none(days) || Any..isfrom_int(days) summary "(Origin_timedelta_Requires)"
+  requires Any..isfrom_none(hours) || Any..isfrom_int(hours) summary "(Origin_timedelta_Requires)hours_type"
+  requires Any..isfrom_int(days) ==> Any..as_int!(days)>=0 summary "(Origin_timedelta_Requires)days_pos"
+  requires Any..isfrom_int(hours) ==> Any..as_int!(hours)>=0 summary "(Origin_timedelta_Requires)hours_pos"
+  ensures Any..isfrom_int(delta) && Any..as_int!(delta)>=0 summary "ret_pos"
+{
+  var days_i : int := 0;
+  if Any..isfrom_int(days) then {
+        days_i := Any..as_int!(days)
+  };
+  var hours_i : int := 0;
+  if Any..isfrom_int(hours) then {
+        hours_i := Any..as_int!(hours)
+  };
+  delta := from_int ((((days_i * 24) + hours_i) * 3600) * 1000000)
+};
+
+// /////////////////////////////////////////////////////////////////////////////////////
+// For testing purpose
+// /////////////////////////////////////////////////////////////////////////////////////
+
+procedure test_helper_procedure(req_name : Any, opt_name : Any) returns (ret: Any, maybe_except: Error)
+  requires req_name == from_string("foo") summary "(Origin_test_helper_procedure_Requires)req_name_is_foo"
+  requires (Any..isfrom_none(opt_name)) || (Any..isfrom_string(opt_name)) summary "(Origin_test_helper_procedure_Requires)req_opt_name_none_or_str"
+  requires (opt_name == from_none()) || (opt_name == from_string("bar")) summary "(Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar"
+  ensures (Error..isNoError(maybe_except)) summary "ensures_maybe_except_none"
+{
+  assert req_name == from_string("foo") summary "assert_name_is_foo";
+  assert (Any..isfrom_none(opt_name)) || (Any..isfrom_string(opt_name)) summary "assert_opt_name_none_or_str";
+  assert (opt_name == from_none()) || (opt_name == from_string("bar")) summary "assert_opt_name_none_or_bar";
+  assume (Error..isNoError(maybe_except)) // summary "assume_maybe_except_none"
+};
+
+procedure print(msg : Any) returns ();
 
 #end
 
@@ -147,7 +957,7 @@ datatype FIRST_END_MARKER { }
 Parse the Laurel DDM prelude into a Laurel Program.
 -/
 public def pythonRuntimeLaurelPart : Laurel.Program :=
-  match Laurel.TransM.run none (Laurel.parseProgram pythonRuntimeLaurelPartDDM) with
+  match Laurel.TransM.run (some $ .file "") (Laurel.parseProgram pythonRuntimeLaurelPartDDM) with
   | .ok p => p
   | .error e => dbg_trace s!"SOUND BUG: Failed to parse Python runtime Laurel part: {e}"; default
 
diff --git a/Strata/Languages/Python/PythonToLaurel.lean b/Strata/Languages/Python/PythonToLaurel.lean
index b8642e40d..4bb9d71f9 100644
--- a/Strata/Languages/Python/PythonToLaurel.lean
+++ b/Strata/Languages/Python/PythonToLaurel.lean
@@ -1028,7 +1028,7 @@ partial def translateAssign  (ctx : TranslationContext)
         | target :: slices =>
             let target ← translateExpr ctx target
             let slices ← slices.mapM (translateExpr ctx)
-            let anySetsExpr := mkStmtExprMd (StmtExpr.StaticCall "Any_sets" [target, ListAny_mk slices, rhs_trans])
+            let anySetsExpr := ⟨ StmtExpr.StaticCall "Any_sets" [ListAny_mk slices, target, rhs_trans] , md ⟩
             let assignStmts := [mkStmtExprMd (StmtExpr.Assign [target] anySetsExpr)]
             return (ctx,assignStmts)
         | _ =>  throw (.internalError "Invalid Subscript Expr")
@@ -1661,7 +1661,8 @@ def translateClass (ctx : TranslationContext) (classStmt : Python.stmt SourceRan
     for stmt in body do
       if let .FunctionDef .. := stmt then
         let proc ← translateMethod ctx className stmt
-        instanceProcedures := instanceProcedures.push proc
+        -- TODO stop replacing the body of instance proceduces with an empty one
+        instanceProcedures := instanceProcedures.push { proc with body := .Opaque [] .none [] }
 
     return ({
       name := className
@@ -1774,9 +1775,9 @@ def PreludeInfo.ofLaurelProgram (prog : Laurel.Program) : PreludeInfo where
     prog.staticProcedures.filterMap fun p =>
       if p.body.isExternal then none
       else
-        let noDefault : Option (Python.expr SourceRange) := none
+        let noneexpr : Python.expr SourceRange := .Constant default (.ConNone default) default
         let args := p.inputs.map fun param =>
-          (param.name.text, getHighTypeName param.type.val, noDefault)
+          (param.name.text, getHighTypeName param.type.val, some noneexpr)
         let ret := p.outputs.head?.map fun param => getHighTypeName param.type.val
         some { name := p.name.text, args := args, hasKwargs := false, ret := ret }
   functions :=
@@ -1965,21 +1966,6 @@ def pythonToLaurel' (info : PreludeInfo)
 
   return (program, ctx)
 
-/-- Generate External procedure stubs for prelude names so the Laurel
-    `resolve` pass can see them. -/
-def preludeStubs (info : PreludeInfo) : List Laurel.Procedure :=
-  let functionStubs := info.functions.map fun funcname =>
-    { name := { text := funcname }, inputs := [], outputs := [],
-      preconditions := [], determinism := .deterministic none,
-      decreases := none, body := .External, md := default,
-      isFunctional := true }
-  let procedureStubs := info.procedureNames.map fun funcname =>
-    { name := { text := funcname }, inputs := [], outputs := [],
-      preconditions := [], determinism := .deterministic none,
-      decreases := none, body := .External, md := default,
-      isFunctional := false }
-  functionStubs ++ procedureStubs
-
 /-- Translate Python module to Laurel Program.
     Delegates to `pythonToLaurel'` after extracting prelude info,
     then prepends External stubs so the Laurel resolve pass can
@@ -1991,11 +1977,7 @@ def pythonToLaurel (prelude: Core.Program)
     (overloadTable : OverloadTable := {})
     : Except TranslationError (Laurel.Program × TranslationContext) := do
   let info := PreludeInfo.ofCoreProgram prelude
-  let (program, ctx) ← pythonToLaurel' info pyCommands prev_ctx filePath overloadTable
-  let stubs := preludeStubs info
-  return ({ program with
-    staticProcedures := stubs ++ program.staticProcedures }, ctx)
-
+  pythonToLaurel' info pyCommands prev_ctx filePath overloadTable
 
 end -- public section
 end Strata.Python
diff --git a/Strata/Languages/Python/Specs/ToLaurel.lean b/Strata/Languages/Python/Specs/ToLaurel.lean
index c78d0173c..f4edd619f 100644
--- a/Strata/Languages/Python/Specs/ToLaurel.lean
+++ b/Strata/Languages/Python/Specs/ToLaurel.lean
@@ -469,6 +469,7 @@ def funcDeclToLaurel (procName : String) (func : FunctionDecl)
       pure (anyInputs, anyOutputs, body)
     else
       pure (inputs, outputs, Body.Opaque [] none [])
+  let md ← mkMdWithFileRange func.loc
   return {
     name := procName
     inputs := inputs.toList
@@ -478,7 +479,7 @@ def funcDeclToLaurel (procName : String) (func : FunctionDecl)
     decreases := none
     isFunctional := false
     body := body
-    md := .empty
+    md := md
   }
 
 /-- Convert a class definition to Laurel types and procedures. -/
diff --git a/StrataMain.lean b/StrataMain.lean
index c3be67030..f5d4b5216 100644
--- a/StrataMain.lean
+++ b/StrataMain.lean
@@ -649,6 +649,8 @@ def pyAnalyzeLaurelCommand : Command where
     IO.println "\n==== Verification Results ===="
     let mut s := ""
     for vcResult in vcResults do
+      let propertySummaryOption := vcResult.obligation.metadata.getPropertySummary
+      let propertyDescription := propertySummaryOption.getD vcResult.obligation.label
       let (locationPrefix, locationSuffix) := match Imperative.getFileRange vcResult.obligation.metadata with
         | some fr =>
           if fr.range.isNone then ("", "")
@@ -674,7 +676,7 @@ def pyAnalyzeLaurelCommand : Command where
                 ("", "")
         | none => ("", "")
       let outcomeStr := vcResult.formatOutcome
-      s := s ++ s!"{locationPrefix}{vcResult.obligation.label}: \
+      s := s ++ s!"{locationPrefix}{propertyDescription}: \
                     {outcomeStr}{locationSuffix}\n"
     IO.println s
     -- Output in SARIF format if requested
diff --git a/StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean b/StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean
index ab2b6ab56..7f4c1ac7a 100644
--- a/StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean
+++ b/StrataTest/Languages/Laurel/ConstrainedTypeElimTest.lean
@@ -67,7 +67,7 @@ deterministic
 def scopeProgram : String := r"
 constrained pos = v: int where v > 0 witness 1
 procedure test(b: bool) {
-  if (b) {
+  if b then {
     var x: pos := 1
   };
   {
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T15_ShortCircuit.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T15_ShortCircuit.lean
index 25149623e..fbb1c1f36 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T15_ShortCircuit.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T15_ShortCircuit.lean
@@ -27,11 +27,15 @@ procedure mustNotCallProc(): int
 
 procedure testAndThenFunc() {
   var b: bool := false && mustNotCallFunc(0) > 0;
+//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
+// TODO caused by a bug in Core: https://github.com/strata-org/Strata/issues/697
   assert !b
 };
 
 procedure testOrElseFunc() {
   var b: bool := true || mustNotCallFunc(0) > 0;
+//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
+// TODO caused by a bug in Core: https://github.com/strata-org/Strata/issues/697
   assert b
 };
 
@@ -44,10 +48,14 @@ procedure testImpliesFunc() {
 
 procedure testAndThenDivByZero() {
   assert !(false && 1 / 0 > 0)
+//^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
+// TODO caused by a bug in Core.
 };
 
 procedure testOrElseDivByZero() {
   assert true || 1 / 0 > 0
+//^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
+// TODO caused by a bug in Core: https://github.com/strata-org/Strata/issues/697
 };
 
 procedure testImpliesDivByZero() {
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T18_RecursiveFunction.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T18_RecursiveFunction.lean
new file mode 100644
index 000000000..a0325e7c1
--- /dev/null
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T18_RecursiveFunction.lean
@@ -0,0 +1,55 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import StrataTest.Util.TestDiagnostics
+import StrataTest.Languages.Laurel.TestExamples
+
+open StrataTest.Util
+open Strata
+
+namespace Strata.Laurel
+
+/-
+A recursive function over a recursive datatype.
+The `isRecursive` flag should be inferred automatically from the self-call.
+-/
+def program := r"
+datatype IntList {
+  Nil(),
+  Cons(head: int, tail: IntList)
+}
+
+function listLen(xs: IntList): int {
+  if IntList..isNil(xs) then 0
+  else 1 + listLen(IntList..tail!(xs))
+};
+
+procedure testListLen() {
+  var xs: IntList := Cons(1, Cons(2, Nil()));
+  assert listLen(xs) == 2
+};
+
+// Mutual recursion
+function listLenEven(xs: IntList): bool {
+  if IntList..isNil(xs) then true
+  else listLenOdd(IntList..tail!(xs))
+};
+
+function listLenOdd(xs: IntList): bool {
+  if IntList..isNil(xs) then false
+  else listLenEven(IntList..tail!(xs))
+};
+
+procedure testMutualRecursion() {
+  var xs: IntList := Cons(1, Cons(2, Nil()));
+  assert listLenEven(xs) == true
+};
+"
+
+#guard_msgs (drop info, error) in
+#eval testInputWithOffset "RecursiveFunction" program 14 processLaurelFile
+
+end Strata.Laurel
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_InvokeOn.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_InvokeOn.lean
new file mode 100644
index 000000000..b1ade4f39
--- /dev/null
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T19_InvokeOn.lean
@@ -0,0 +1,71 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import StrataTest.Util.TestDiagnostics
+import StrataTest.Languages.Laurel.TestExamples
+
+open StrataTest.Util
+open Strata
+
+namespace Strata.Laurel
+
+def program := r#"
+function P(x: int): bool;
+function Q(x: int): bool;
+
+function assertP(x: int): int requires P(x);
+function needsPAndQsInvoke1(): int {
+  assertP(3)
+};
+
+procedure PAndQ(x: int)
+  invokeOn P(x)
+  ensures P(x) && Q(x);
+
+function needsPAndQsInvoke2(): int {
+  assertP(3)
+};
+
+// The axiom fires because P(x) appears in the goal.
+procedure fireAxiomUsingPattern(x: int) {
+  assert P(x)
+};
+
+procedure axiomDoesNotFireBecauseOfPattern(x: int) {
+  assert Q(x)
+//^^^^^^^^^^^ error: assertion could not be proved
+};
+
+function A(x: int, y: real): bool;
+function B(x: real): bool;
+procedure AAndB(x: int, y: real)
+  invokeOn A(x, y)
+  ensures A(x, y) && B(y);
+
+procedure invokeA(x: int, y :real) {
+  assert A(x, y)
+};
+
+procedure invokeB(x: int, y :real) {
+  assert B(y)
+//^^^^^^^^^^^ error: assertion could not be proved
+};
+
+function R(x: int): bool;
+procedure badPostcondition(x: int)
+  invokeOn R(x)
+  ensures R(x)
+//        ^^^^ error: assertion does not hold
+{
+};
+
+"#
+
+#guard_msgs (drop info, error) in
+#eval testInputWithOffset "InvokeOn" program 14
+  (Strata.Laurel.processLaurelFileWithOptions { Core.VerifyOptions.default with solver := "z3" })
+
+end Strata.Laurel
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
index ce53e09f0..fec34e8c4 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
@@ -30,8 +30,8 @@ procedure multipleAssignments() {
 
 procedure conditionalAssignmentInExpression(x: int) {
   var y: int := 0;
-  var z: int := (if (x > 0) { y := y + 1 } else { 0 }) + y;
-  if (x > 0) {
+  var z: int := (if x > 0 then { y := y + 1 } else { 0 }) + y;
+  if x > 0 then {
     assert y == 1;
     assert z == 2
   } else {
@@ -42,7 +42,7 @@ procedure conditionalAssignmentInExpression(x: int) {
 
 procedure anotherConditionAssignmentInExpression(c: bool) {
   var b: bool := c;
-  var z: bool := (if (b) { b := false } else (b := true)) || b;
+  var z: bool := (if b then { b := false } else (b := true)) || b;
   assert z
 //^^^^^^^^ error: assertion does not hold
 };
@@ -90,8 +90,8 @@ procedure imperativeCallInExpressionPosition() {
 procedure imperativeCallInConditionalExpression(b: bool) {
   var counter: int := 0;
   // The imperative call in the then-branch is lifted out of the expression.
-  var result: int := (if (b) { imperativeProc(counter) } else { 0 }) + counter;
-  if (b) {
+  var result: int := (if b then { imperativeProc(counter) } else { 0 }) + counter;
+  if b then {
     assert result == 1
   } else {
     assert result == 0
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean
index c9c37b65b..150ee55f5 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean
@@ -14,8 +14,8 @@ namespace Strata.Laurel
 
 def program := r"
 function returnAtEnd(x: int) returns (r: int) {
-  if (x > 0) {
-    if (x == 1) {
+  if x > 0 then {
+    if x == 1 then {
       return 1
     } else {
       return 2
@@ -26,12 +26,12 @@ function returnAtEnd(x: int) returns (r: int) {
 };
 
 function elseWithCall(): int {
-  if (true) 3 else returnAtEnd(3)
+  if true then 3 else returnAtEnd(3)
 };
 
 function guardInFunction(x: int) returns (r: int) {
-  if (x > 0) {
-    if (x == 1) {
+  if x > 0 then {
+    if x == 1 then {
       return 1
     } else {
       return 2
@@ -54,9 +54,9 @@ procedure testFunctions() {
 procedure guards(a: int) returns (r: int)
 {
   var b: int := a + 2;
-  if (b > 2) {
+  if b > 2 then {
       var c: int := b + 3;
-      if (c > 3) {
+      if c > 3 then {
           return c + 4
       };
       var d: int := c + 5;
@@ -73,12 +73,12 @@ procedure dag(a: int) returns (r: int)
 {
   var b: int;
 
-  if (a > 0) {
+  if a > 0 then {
     b := 1
   };
-  assert if (a > 0) { b == 1 } else { true };
-  assert if (a > 0) { b == 2 } else { true };
-//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
+  assert if a > 0 then { b == 1 } else { true };
+  assert if a > 0 then { b == 2 } else { true };
+//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion does not hold
   return b
 };
 "
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean
index ed4c4d55e..b336119ea 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlowError.lean
@@ -41,8 +41,8 @@ function localVariableWithoutInitializer(): int {
 };
 
 function deadCodeAfterIfElse(x: int) returns (r: int) {
-  if (x > 0) { return 1 } else { return 2 };
-//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: if-then-else only supported as the last statement in a block
+  if x > 0 then { return 1 } else { return 2 };
+//^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: if-then-else only supported as the last statement in a block
   return 3
 };
 "
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T4_LoopJumps.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T4_LoopJumps.lean
index bf54f0bbb..040bf3a18 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T4_LoopJumps.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T4_LoopJumps.lean
@@ -20,11 +20,11 @@ procedure whileWithBreakAndContinue(steps: int, continueSteps: int, exitSteps: i
       invariant counter >= 0
     {
       {
-        if (steps == exitSteps) {
+        if steps == exitSteps then {
           counter = -10;
           exit breakBlock;
         }
-        if (steps == continueSteps) {
+        if steps == continueSteps then {
           exit continueBlock;
         }
         counter = counter + 1;
@@ -51,12 +51,12 @@ proof whileWithBreakAndContinue_body() {
 
   loopStart: {
     assert counter >= 0;
-    if (steps > 0) {
-      if (steps == exitSteps) {
+    if steps > 0 then {
+      if steps == exitSteps then {
         counter = -10;
         exit loopStart;
       }
-      if (steps == continueSteps) {
+      if steps == continueSteps then {
         exit loopStart;
       }
       counter = counter + 1;
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T7_Decreases.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T7_Decreases.lean
index dd13a46c5..ee5cfc149 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T7_Decreases.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T7_Decreases.lean
@@ -58,7 +58,7 @@ proof foo_body {
 
 proof bar_body {
   var x: nat;
-  if (x != 0) {
+  if x != 0 then {
     assert decreases([x, 0], [x - 1, 1]);
   }
 }
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean
index 72ac115d2..b67e9c5f3 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8_Postconditions.lean
@@ -17,7 +17,7 @@ procedure opaqueBody(x: int) returns (r: int)
 // the presence of the ensures make the body opaque. we can consider more explicit syntax.
   ensures r > 0
 {
-  if (x > 0) { r := x }
+  if x > 0 then { r := x }
   else { r := 1 }
 };
 
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8b_EarlyReturnPostconditions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8b_EarlyReturnPostconditions.lean
index b3d3e5069..2795f28a2 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T8b_EarlyReturnPostconditions.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T8b_EarlyReturnPostconditions.lean
@@ -16,7 +16,7 @@ def program := r"
 procedure earlyReturnCorrect(x: int) returns (r: int)
   ensures r >= 0
 {
-  if (x < 0) {
+  if x < 0 then {
     return -x
   };
   return x
@@ -26,7 +26,7 @@ procedure earlyReturnBuggy(x: int) returns (r: int)
   ensures r >= 0
 //        ^^^^^^ error: assertion does not hold
 {
-  if (x < 0) {
+  if x < 0 then {
     return x
   };
   return x
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean b/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean
index 5610675d1..ca863ecc7 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T1_MutableFields.lean
@@ -71,7 +71,7 @@ procedure subsequentHeapMutations(c: Container) {
 procedure implicitEquality(c: Container, d: Container) {
   c#intValue := 1;
   d#intValue := 2;
-  if (c#intValue == d#intValue) {
+  if c#intValue == d#intValue then {
     assert c == d
   } else {
     // Somehow we can't prove this here
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/WIP/6. TypeTests.lr.st b/StrataTest/Languages/Laurel/Examples/Objects/WIP/6. TypeTests.lr.st
index cb4e57afc..6d94f9a08 100644
--- a/StrataTest/Languages/Laurel/Examples/Objects/WIP/6. TypeTests.lr.st	
+++ b/StrataTest/Languages/Laurel/Examples/Objects/WIP/6. TypeTests.lr.st	
@@ -23,7 +23,7 @@ procedure typeTests(e: Extended1) {
   var b: Base = e as Base; // even upcasts are not implicit, but they pass statically
   var e2 = e as Extended2;
 //           ^^ error: could not prove 'e' is of type 'Extended2'
-  if (e is Extended2) {
+  if e is Extended2 then {
     // unreachable, but that's OK
     var e2pass = e as Extended2; // no error
   }
diff --git a/StrataTest/Languages/Laurel/LiftHolesTest.lean b/StrataTest/Languages/Laurel/LiftHolesTest.lean
index 41c9e7ae7..21471f78f 100644
--- a/StrataTest/Languages/Laurel/LiftHolesTest.lean
+++ b/StrataTest/Languages/Laurel/LiftHolesTest.lean
@@ -133,7 +133,7 @@ deterministic
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { if (<?>) { assert true } };
+procedure test() { if <?> then { assert true } };
 "
 
 -- Hole in then-branch of if-then-else inside typed local variable → int.
@@ -149,7 +149,7 @@ deterministic
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { var x: int := if (true) <?> else 0 };
+procedure test() { var x: int := if true then <?> else 0 };
 "
 
 -- Hole as while-loop condition → bool.
@@ -290,7 +290,7 @@ deterministic
 -/
 #guard_msgs in
 #eval! parseElimAndPrint r"
-procedure test() { if (1 + <?> > 0) { assert true } };
+procedure test() { if 1 + <?> > 0 then { assert true } };
 "
 
 -- Hole in Implies inside while invariant → bool.
diff --git a/StrataTest/Languages/Laurel/TestExamples.lean b/StrataTest/Languages/Laurel/TestExamples.lean
index d5f18f16a..3f16e79f7 100644
--- a/StrataTest/Languages/Laurel/TestExamples.lean
+++ b/StrataTest/Languages/Laurel/TestExamples.lean
@@ -19,7 +19,7 @@ open Lean.Parser (InputContext)
 
 namespace Strata.Laurel
 
-def processLaurelFile (input : InputContext) : IO (Array Diagnostic) := do
+def processLaurelFileWithOptions (options : Core.VerifyOptions) (input : InputContext) : IO (Array Diagnostic) := do
   let dialects := Strata.Elab.LoadedDialects.ofDialects! #[initDialect, Laurel]
   let strataProgram ← parseStrataProgramFromDialect dialects Laurel.name input
 
@@ -29,8 +29,11 @@ def processLaurelFile (input : InputContext) : IO (Array Diagnostic) := do
   | .error transErrors => throw (IO.userError s!"Translation errors: {transErrors}")
   | .ok laurelProgram =>
     let files := Map.insert Map.empty uri input.fileMap
-    let diagnostics ← Laurel.verifyToDiagnostics files laurelProgram
+    let diagnostics ← Laurel.verifyToDiagnostics files laurelProgram options
 
     pure diagnostics
 
+def processLaurelFile (input : InputContext) : IO (Array Diagnostic) :=
+  processLaurelFileWithOptions Core.VerifyOptions.default input
+
 end Laurel
diff --git a/StrataTest/Languages/Laurel/tests/test_control_flow.lr.st b/StrataTest/Languages/Laurel/tests/test_control_flow.lr.st
index 22bc315c0..b255bd7b3 100644
--- a/StrataTest/Languages/Laurel/tests/test_control_flow.lr.st
+++ b/StrataTest/Languages/Laurel/tests/test_control_flow.lr.st
@@ -2,7 +2,7 @@ procedure main() {
     var x: int := 5;
     var result: int := 0;
 
-    if (x == 5) {
+    if x == 5 then {
         result := 10
     } else {
         result := 20
@@ -12,8 +12,8 @@ procedure main() {
     var y: int := 7;
     var status: int := 0;
 
-    if (y == 7) {
-        if (y == 7) {
+    if y == 7 then {
+        if y == 7 then {
             status := 1
         } else {
             status := 2
@@ -26,7 +26,7 @@ procedure main() {
     var a: int := 10;
     var b: int := 0;
 
-    if (a > 3) {
+    if a > 3 then {
         b := 1
     } else {
         b := 2
diff --git a/StrataTest/Languages/Python/AnalyzeLaurelTest.lean b/StrataTest/Languages/Python/AnalyzeLaurelTest.lean
index bbc3414ac..574ffefb7 100644
--- a/StrataTest/Languages/Python/AnalyzeLaurelTest.lean
+++ b/StrataTest/Languages/Python/AnalyzeLaurelTest.lean
@@ -239,8 +239,8 @@ private meta def runTestCase (pythonCmd : System.FilePath) (tmpDir : System.File
       match Strata.translateCombinedLaurel laurel with
       | (some core, []) =>
         match Core.typeCheck Core.VerifyOptions.quiet core (moreFns := Strata.Python.ReFactory) with
-        | .error _ => return none  -- Expected: Core type checking fails
-        | .ok _ => return some "test_class_any_as_composite.py: expected Core type checking to fail"
+        | .error errors => return some s!"test_class_any_as_composite.py: {errors}"
+        | .ok _ => return none
       | (_, errors) => return some s!"test_class_any_as_composite.py: Laurel to Core failed: {errors}"
     tasks := tasks.push ("test_class_any_as_composite.py", task)
     -- Collect results
diff --git a/StrataTest/Languages/Python/PreludeVerifyTest.lean b/StrataTest/Languages/Python/PreludeVerifyTest.lean
index e33516a56..664163cf2 100644
--- a/StrataTest/Languages/Python/PreludeVerifyTest.lean
+++ b/StrataTest/Languages/Python/PreludeVerifyTest.lean
@@ -33,7 +33,7 @@ private def verifyPrelude : IO Core.VCResults := do
 
 /--
 info:
-Obligation: List_get_body_calls_List_get_0
+Obligation: postcondition
 Property: assert
 Result: ✅ pass
 
@@ -41,10 +41,34 @@ Obligation: List_take_body_calls_List_take_0
 Property: assert
 Result: ✅ pass
 
+Obligation: List_take_len_post_postcondition_calls_List_take_0
+Property: assert
+Result: ✅ pass
+
+Obligation: postcondition
+Property: assert
+Result: ✅ pass
+
 Obligation: List_drop_body_calls_List_drop_0
 Property: assert
 Result: ✅ pass
 
+Obligation: List_drop_len_post_postcondition_calls_List_drop_0
+Property: assert
+Result: ✅ pass
+
+Obligation: postcondition
+Property: assert
+Result: ✅ pass
+
+Obligation: postcondition
+Property: assert
+Result: ✅ pass
+
+Obligation: List_get_body_calls_List_get_0
+Property: assert
+Result: ✅ pass
+
 Obligation: List_slice_body_calls_List_drop_0
 Property: assert
 Result: ✅ pass
@@ -121,31 +145,31 @@ Obligation: POr_body_calls_Any_to_bool_0
 Property: assert
 Result: ✅ pass
 
-Obligation: ret_type
+Obligation: postcondition
 Property: assert
 Result: ✅ pass
 
-Obligation: ret_type
+Obligation: postcondition
 Property: assert
 Result: ✅ pass
 
-Obligation: ret_pos
+Obligation: postcondition
 Property: assert
 Result: ✅ pass
 
-Obligation: assert_name_is_foo
+Obligation: assert(40418)
 Property: assert
 Result: ✅ pass
 
-Obligation: assert_opt_name_none_or_str
+Obligation: assert(40488)
 Property: assert
 Result: ✅ pass
 
-Obligation: assert_opt_name_none_or_bar
+Obligation: assert(40599)
 Property: assert
 Result: ✅ pass
 
-Obligation: ensures_maybe_except_none
+Obligation: postcondition
 Property: assert
 Result: ✅ pass
 -/
diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_decl.expected b/StrataTest/Languages/Python/expected_laurel/test_class_decl.expected
index 11dfb812f..02e41a188 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_decl.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_decl.expected
@@ -1,6 +1,6 @@
 
 ==== Verification Results ====
-callElimAssert_requires_5: ✅ pass
+callElimAssert_requires_4: ✅ pass
 ite_cond_calls_Any_to_bool_0: ✅ pass (at line 13, col 0)
 
 DETAIL: 2 passed, 0 failed, 0 inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_field_any.expected b/StrataTest/Languages/Python/expected_laurel/test_class_field_any.expected
index 7e837fa65..2373bfc4b 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_field_any.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_field_any.expected
@@ -1,6 +1,6 @@
 
 ==== Verification Results ====
-callElimAssert_requires_5: ✅ pass
+callElimAssert_requires_3: ✅ pass
 assert_assert(113)_calls_Any_to_bool_0: ✅ pass (at line 6, col 0)
 assert(113): ❓ unknown (at line 6, col 0)
 
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 c6e25fbc9..11dfb812f 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_field_init.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_field_init.expected
@@ -1,6 +1,6 @@
 
 ==== Verification Results ====
-callElimAssert_requires_7: ✅ pass
+callElimAssert_requires_5: ✅ pass
 ite_cond_calls_Any_to_bool_0: ✅ pass (at line 13, col 0)
 
 DETAIL: 2 passed, 0 failed, 0 inconclusive
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 47b9b62c9..771f2ea1c 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_field_use.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_field_use.expected
@@ -1,6 +1,6 @@
 
 ==== Verification Results ====
-callElimAssert_requires_10: ✅ pass
+callElimAssert_requires_7: ✅ pass
 assert_assert(285)_calls_Any_to_bool_0: ✅ pass (at line 14, col 4)
 Assertion failed at line 14, col 4: assert(285): ❌ fail
 
diff --git a/StrataTest/Languages/Python/expected_laurel/test_class_methods.expected b/StrataTest/Languages/Python/expected_laurel/test_class_methods.expected
index e859e2238..7ba4fea44 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_methods.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_methods.expected
@@ -1,15 +1,15 @@
 
 ==== Verification Results ====
-callElimAssert_requires_14: ✅ pass
+callElimAssert_requires_12: ✅ pass
 assert_assert(445)_calls_Any_to_bool_0: ✅ pass (at line 21, col 4)
 assert(445): ❓ unknown (at line 21, col 4)
 assert_assert(539)_calls_Any_to_bool_0: ✅ pass (at line 24, col 4)
 Assertion failed at line 24, col 4: assert(539): ❌ fail
 assert_assert(654)_calls_Any_to_bool_0: ✅ pass (at line 28, col 4)
 Assertion failed at line 28, col 4: assert(654): ❌ fail
-callElimAssert_req_name_is_foo_4: ✅ pass (at line 30, col 4)
-callElimAssert_req_opt_name_none_or_str_5: ✅ pass (at line 30, col 4)
-callElimAssert_req_opt_name_none_or_bar_6: ✅ pass (at line 30, col 4)
+callElimAssert_requires_0_4: ✅ pass (at line 30, col 4)
+callElimAssert_requires_1_5: ✅ pass (at line 30, col 4)
+callElimAssert_requires_2_6: ✅ pass (at line 30, col 4)
 ite_cond_calls_Any_to_bool_0: ✅ pass (at line 32, col 0)
 
 DETAIL: 8 passed, 2 failed, 1 inconclusive
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 39014c9b3..9ed3eb2b2 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_class_with_methods.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_class_with_methods.expected
@@ -1,13 +1,13 @@
 
 ==== Verification Results ====
-callElimAssert_requires_13: ✅ pass
+callElimAssert_requires_11: ✅ pass
 assert_assert(459)_calls_Any_to_bool_0: ✅ pass (at line 23, col 4)
 Assertion failed at line 23, col 4: assert(459): ❌ fail
 assert_assert(544)_calls_Any_to_bool_0: ✅ pass (at line 26, col 4)
 assert(544): ❓ unknown (at line 26, col 4)
-callElimAssert_req_name_is_foo_4: ✅ pass (at line 28, col 4)
-callElimAssert_req_opt_name_none_or_str_5: ✅ pass (at line 28, col 4)
-callElimAssert_req_opt_name_none_or_bar_6: ✅ pass (at line 28, col 4)
+callElimAssert_requires_0_4: ✅ pass (at line 28, col 4)
+callElimAssert_requires_1_5: ✅ pass (at line 28, col 4)
+callElimAssert_requires_2_6: ✅ pass (at line 28, col 4)
 ite_cond_calls_Any_to_bool_0: ✅ pass (at line 30, col 0)
 
 DETAIL: 7 passed, 1 failed, 1 inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_datetime.expected b/StrataTest/Languages/Python/expected_laurel/test_datetime.expected
index 5793dd936..22f65503b 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_datetime.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_datetime.expected
@@ -1,10 +1,10 @@
 
 ==== Verification Results ====
-callElimAssert_d_type_12: ✅ pass
-callElimAssert_days_type_4: ✅ pass
-callElimAssert_hours_type_5: ✅ pass
-callElimAssert_days_pos_6: ✅ pass
-callElimAssert_hours_pos_7: ✅ pass
+callElimAssert_requires_12: ✅ pass
+callElimAssert_requires_0_4: ✅ pass
+callElimAssert_requires_1_5: ✅ pass
+callElimAssert_requires_2_6: ✅ pass
+callElimAssert_requires_3_7: ✅ pass
 assert_assert(554)_calls_Any_to_bool_0: ✅ pass (at line 21, col 0)
 assert(554): ✅ pass (at line 21, col 0)
 assert_assert(673)_calls_Any_to_bool_0: ✅ pass (at line 25, col 0)
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 7921843b3..7c64f8fbf 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_function_def_calls.expected
@@ -1,8 +1,8 @@
 
 ==== Verification Results ====
-callElimAssert_req_name_is_foo_4: ❓ unknown (at line 6, col 4)
-callElimAssert_req_opt_name_none_or_str_5: ✅ pass (at line 6, col 4)
-callElimAssert_req_opt_name_none_or_bar_6: ✅ pass (at line 6, col 4)
+callElimAssert_requires_0_4: ❓ unknown (at line 6, col 4)
+callElimAssert_requires_1_5: ✅ pass (at line 6, col 4)
+callElimAssert_requires_2_6: ✅ pass (at line 6, col 4)
 ite_cond_calls_Any_to_bool_0: ✅ pass (at line 11, col 0)
 
 DETAIL: 3 passed, 0 failed, 1 inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_missing_models.expected b/StrataTest/Languages/Python/expected_laurel/test_missing_models.expected
index 360a1cd14..887c5ac8a 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_missing_models.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_missing_models.expected
@@ -2,15 +2,9 @@
 ==== Verification Results ====
 init_calls_Any_get_0: ❓ unknown (at line 8, col 4)
 init_calls_Any_get_1: ❓ unknown (at line 8, col 4)
-Assertion failed at line 9, col 4: callElimAssert_req_name_is_foo_22: ❌ fail
-callElimAssert_req_opt_name_none_or_str_23: ✅ pass (at line 9, col 4)
-callElimAssert_req_opt_name_none_or_bar_24: ✅ pass (at line 9, col 4)
-callElimAssert_req_name_is_foo_13: ✅ pass (at line 12, col 4)
-callElimAssert_req_opt_name_none_or_str_14: ✅ pass (at line 12, col 4)
-callElimAssert_req_opt_name_none_or_bar_15: ✅ pass (at line 12, col 4)
-callElimAssert_req_name_is_foo_4: ✅ pass (at line 15, col 4)
-callElimAssert_req_opt_name_none_or_str_5: ✅ pass (at line 15, col 4)
-callElimAssert_req_opt_name_none_or_bar_6: ✅ pass (at line 15, col 4)
+Assertion failed at line 9, col 4: callElimAssert_requires_0_22: ❌ fail
+callElimAssert_requires_1_23: ✅ pass (at line 9, col 4)
+callElimAssert_requires_2_24: ✅ pass (at line 9, col 4)
 
-DETAIL: 8 passed, 1 failed, 2 inconclusive
+DETAIL: 2 passed, 1 failed, 2 inconclusive
 RESULT: Failures found
diff --git a/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected b/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected
index 81fe21731..36f0f7d98 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_multi_function.expected
@@ -8,9 +8,9 @@ ite_cond_calls_Any_to_bool_0: ❓ unknown (at line 18, col 4)
 set_LaurelResult_calls_Any_get_0: ❓ unknown
 assert_assert(651)_calls_Any_to_bool_0: ✅ pass (at line 24, col 4)
 Assertion failed at line 24, col 4: assert(651): ❌ fail
-callElimAssert_req_name_is_foo_9: ✅ pass (at line 26, col 4)
-callElimAssert_req_opt_name_none_or_str_10: ✅ pass (at line 26, col 4)
-callElimAssert_req_opt_name_none_or_bar_11: ✅ pass (at line 26, col 4)
+callElimAssert_requires_0_9: ✅ pass (at line 26, col 4)
+callElimAssert_requires_1_10: ✅ pass (at line 26, col 4)
+callElimAssert_requires_2_11: ✅ pass (at line 26, col 4)
 ite_cond_calls_Any_to_bool_0: ✅ pass (at line 28, col 0)
 
 DETAIL: 7 passed, 2 failed, 3 inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_precondition_verification.expected b/StrataTest/Languages/Python/expected_laurel/test_precondition_verification.expected
index d73d8a4f7..86e5f53f2 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_precondition_verification.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_precondition_verification.expected
@@ -1,17 +1,17 @@
 
 ==== Verification Results ====
-callElimAssert_req_name_is_foo_28: ✅ pass (at line 8, col 4)
-callElimAssert_req_opt_name_none_or_str_29: ✅ pass (at line 8, col 4)
-callElimAssert_req_opt_name_none_or_bar_30: ✅ pass (at line 8, col 4)
-callElimAssert_req_name_is_foo_20: ✅ pass (at line 11, col 4)
-callElimAssert_req_opt_name_none_or_str_21: ✅ pass (at line 11, col 4)
-callElimAssert_req_opt_name_none_or_bar_22: ✅ pass (at line 11, col 4)
-Assertion failed at line 14, col 4: callElimAssert_req_name_is_foo_12: ❌ fail
-callElimAssert_req_opt_name_none_or_str_13: ✅ pass (at line 14, col 4)
-callElimAssert_req_opt_name_none_or_bar_14: ✅ pass (at line 14, col 4)
-callElimAssert_req_name_is_foo_4: ✅ pass (at line 17, col 4)
-callElimAssert_req_opt_name_none_or_str_5: ✅ pass (at line 17, col 4)
-Assertion failed at line 17, col 4: callElimAssert_req_opt_name_none_or_bar_6: ❌ fail
+callElimAssert_requires_0_28: ✅ pass (at line 8, col 4)
+callElimAssert_requires_1_29: ✅ pass (at line 8, col 4)
+callElimAssert_requires_2_30: ✅ pass (at line 8, col 4)
+callElimAssert_requires_0_20: ✅ pass (at line 11, col 4)
+callElimAssert_requires_1_21: ✅ pass (at line 11, col 4)
+callElimAssert_requires_2_22: ✅ pass (at line 11, col 4)
+Assertion failed at line 14, col 4: callElimAssert_requires_0_12: ❌ fail
+callElimAssert_requires_1_13: ✅ pass (at line 14, col 4)
+callElimAssert_requires_2_14: ✅ pass (at line 14, col 4)
+callElimAssert_requires_0_4: ✅ pass (at line 17, col 4)
+callElimAssert_requires_1_5: ✅ pass (at line 17, col 4)
+Assertion failed at line 17, col 4: callElimAssert_requires_2_6: ❌ fail
 ite_cond_calls_Any_to_bool_0: ✅ pass (at line 19, col 0)
 
 DETAIL: 11 passed, 2 failed, 0 inconclusive
diff --git a/StrataTest/Languages/Python/expected_laurel/test_with_statement.expected b/StrataTest/Languages/Python/expected_laurel/test_with_statement.expected
index 999fb6f17..56a2a5618 100644
--- a/StrataTest/Languages/Python/expected_laurel/test_with_statement.expected
+++ b/StrataTest/Languages/Python/expected_laurel/test_with_statement.expected
@@ -1,23 +1,23 @@
 
 ==== Verification Results ====
-callElimAssert_requires_12: ✅ pass
-callElimAssert_requires_6: ✅ pass
+callElimAssert_requires_9: ✅ pass
+callElimAssert_requires_5: ✅ pass
 callElimAssert_requires_2: ✅ pass
 assert_assert(368)_calls_Any_to_bool_0: ✅ pass (at line 19, col 4)
 Assertion failed at line 19, col 4: assert(368): ❌ fail
-callElimAssert_requires_25: ✅ pass
 callElimAssert_requires_19: ✅ pass
+callElimAssert_requires_15: ✅ pass
 assert_assert(500)_calls_Any_to_bool_0: ✅ pass (at line 25, col 8)
 Assertion failed at line 25, col 8: assert(500): ❌ fail
-callElimAssert_requires_15: ✅ pass
-callElimAssert_requires_51: ✅ pass
-callElimAssert_requires_45: ✅ pass
+callElimAssert_requires_12: ✅ pass
 callElimAssert_requires_39: ✅ pass
 callElimAssert_requires_35: ✅ pass
-assert_assert(666)_calls_Any_to_bool_0: ✅ pass (at line 32, col 8)
-assert(666): ❓ unknown (at line 32, col 8)
 callElimAssert_requires_31: ✅ pass
 callElimAssert_requires_28: ✅ pass
+assert_assert(666)_calls_Any_to_bool_0: ✅ pass (at line 32, col 8)
+assert(666): ❓ unknown (at line 32, col 8)
+callElimAssert_requires_25: ✅ pass
+callElimAssert_requires_22: ✅ pass
 
 DETAIL: 15 passed, 2 failed, 1 inconclusive
 RESULT: Failures found