diff --git a/Strata/Cli/VerifyOptions.lean b/Strata/Cli/VerifyOptions.lean
index ac27060ebb..71d8d55e6d 100644
--- a/Strata/Cli/VerifyOptions.lean
+++ b/Strata/Cli/VerifyOptions.lean
@@ -173,7 +173,8 @@ def parseLaurelVerifyOptions (pflags : ParsedFlags)
   let translateOptions : LaurelTranslateOptions :=
     { base.translateOptions with
       keepAllFilesPrefix
-      overflowChecks := verifyOptions.overflowChecks }
+      overflowChecks := verifyOptions.overflowChecks
+      enumeratedModifiesClauses := verifyOptions.useArrayTheory }
   return { translateOptions, verifyOptions }
 
 end -- public section
diff --git a/Strata/Languages/Laurel/ConstrainedTypeElim.lean b/Strata/Languages/Laurel/ConstrainedTypeElim.lean
index 566dab3ae6..47b3bb709f 100644
--- a/Strata/Languages/Laurel/ConstrainedTypeElim.lean
+++ b/Strata/Languages/Laurel/ConstrainedTypeElim.lean
@@ -248,7 +248,7 @@ public def constrainedTypeElimPass : LoweringPass where
   name := "ConstrainedTypeElim"
   documentation := "Eliminates constrained types by replacing them with their base types and generating constraint-checking functions and witness procedures. Type tests against constrained types are rewritten to call the generated constraint function."
   needsResolves := true
-  run := fun p m _ =>
+  run := fun _ p m =>
     let (p', diags) := constrainedTypeElim m p
     (p', diags, {})
 
diff --git a/Strata/Languages/Laurel/ContractPass.lean b/Strata/Languages/Laurel/ContractPass.lean
index cc93ba02f9..2d9b98ffb0 100644
--- a/Strata/Languages/Laurel/ContractPass.lean
+++ b/Strata/Languages/Laurel/ContractPass.lean
@@ -453,7 +453,7 @@ public def contractPass : LoweringPass where
   documentation := "Lowers pre and postcondition to assertions and assumptions around call-sites and procedure bodies"
   comesAfter := [⟨ eliminateReturnStatementsPass.meta, "The contract pass wraps the body of procedures to get: `assume preconditions; body; assert postconditions`. Eliminating returns first means that the postcondition assertions are guaranteed to execute."⟩ ]
   needsResolves := true
-  run := fun p _m _ =>
+  run := fun _ p _m =>
     let (p', diags) := lowerContracts p
     (p', diags, {})
 
diff --git a/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean b/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean
index 57007a95a5..85303d227e 100644
--- a/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean
+++ b/Strata/Languages/Laurel/CoreGroupingAndOrdering.lean
@@ -267,7 +267,7 @@ then collecting datatypes and constants.
 Functions are grouped into SCCs (for mutual recursion). Proofs are emitted
 as individual `procedure` decls. Both participate in the topological ordering
 so that axioms are available to functions that need them."
-  run := fun p _ _ =>
+  run := fun _ p _ =>
     (orderFunctionsAndProcedures p, [], {})
 
 end Strata.Laurel
diff --git a/Strata/Languages/Laurel/DesugarShortCircuit.lean b/Strata/Languages/Laurel/DesugarShortCircuit.lean
index b8d65c1e40..9c7c24dc76 100644
--- a/Strata/Languages/Laurel/DesugarShortCircuit.lean
+++ b/Strata/Languages/Laurel/DesugarShortCircuit.lean
@@ -59,7 +59,7 @@ end -- public section
 public def desugarShortCircuitPass : LoweringPass where
   name := "DesugarShortCircuit"
   documentation := "Rewrites short-circuit boolean operators (`&&` and `||`) into equivalent conditional expressions. This simplifies subsequent passes and the final translation to Core, which does not have short-circuit semantics built in."
-  run := fun p _ _ =>
+  run := fun _ p _ =>
     (desugarShortCircuit p, [], {})
   comesBefore := [
       ⟨ liftImperativeExpressionsPass.meta, "The desugar short circuit pass introduces if-then-else expressions whose control-flow must be taken into account by the lifting pass."⟩]
diff --git a/Strata/Languages/Laurel/EliminateDeterministicHoles.lean b/Strata/Languages/Laurel/EliminateDeterministicHoles.lean
index d7286e86c7..83538bf728 100644
--- a/Strata/Languages/Laurel/EliminateDeterministicHoles.lean
+++ b/Strata/Languages/Laurel/EliminateDeterministicHoles.lean
@@ -93,7 +93,7 @@ end -- public section
 public def eliminateDeterministicHolesPass : LoweringPass where
   name := "EliminateDeterministicHoles"
   documentation := "Replaces every deterministic hole with a call to a freshly generated uninterpreted function. After this pass the program contains only non-deterministic holes. Assumes `InferHoleTypes` has already annotated holes with types."
-  run := fun p _m _ =>
+  run := fun _ p _m =>
     let (p', stats) := eliminateDeterministicHoles p
     (p', [], stats)
 
diff --git a/Strata/Languages/Laurel/EliminateDoWhile.lean b/Strata/Languages/Laurel/EliminateDoWhile.lean
index 345b1ad694..56f4e3d498 100644
--- a/Strata/Languages/Laurel/EliminateDoWhile.lean
+++ b/Strata/Languages/Laurel/EliminateDoWhile.lean
@@ -76,7 +76,7 @@ def eliminateDoWhile (program : Program) : Program :=
 public def eliminateDoWhilePass : LoweringPass where
   name := "EliminateDoWhile"
   documentation := "Lowers post-test `While` loops (the `do … while` form) into the pre-test loop `{ while(true) invariant I { BODY; if (!COND) exit L } } L`, with a fresh `$`-prefixed exit label `L`. Runs early so no later pass observes a post-test loop; the invariant is checked at the loop head, matching `while`."
-  run := fun p _m _ => (eliminateDoWhile p, [], {})
+  run := fun _ p _m => (eliminateDoWhile p, [], {})
 
 end -- public section
 end Strata.Laurel
diff --git a/Strata/Languages/Laurel/EliminateIncrDecr.lean b/Strata/Languages/Laurel/EliminateIncrDecr.lean
index 7f1c06a2a5..82e8a3adfd 100644
--- a/Strata/Languages/Laurel/EliminateIncrDecr.lean
+++ b/Strata/Languages/Laurel/EliminateIncrDecr.lean
@@ -103,7 +103,7 @@ def eliminateIncrDecr (program : Program) : Program :=
 public def eliminateIncrDecrPass : LoweringPass where
   name := "EliminateIncrDecr"
   documentation := "Lowers Java-style increment/decrement operators (`++x`, `x++`, `--x`, `x--`) into existing Laurel assignment and arithmetic constructs. Prefix forms yield the new value; postfix forms yield the old value. Runs early so that no later pass observes an `.IncrDecr` node."
-  run := fun p _m _ => (eliminateIncrDecr p, [], {})
+  run := fun _ p _m => (eliminateIncrDecr p, [], {})
 
 end -- public section
 end Strata.Laurel
diff --git a/Strata/Languages/Laurel/EliminateReturnStatements.lean b/Strata/Languages/Laurel/EliminateReturnStatements.lean
index d2a7743765..c0129afc07 100644
--- a/Strata/Languages/Laurel/EliminateReturnStatements.lean
+++ b/Strata/Languages/Laurel/EliminateReturnStatements.lean
@@ -73,7 +73,7 @@ def eliminateReturnStatements (program : Program) : Program :=
 public def eliminateReturnStatementsPass : LoweringPass where
   name := "EliminateReturnStatements"
   documentation := "Lower return statements to exit statements. Wrap each procedure body with a 'return' block"
-  run := fun p _m _ =>
+  run := fun _ p _m =>
     let p' := eliminateReturnStatements p
     (p', [], {})
   -- comesBefore := [contractPass]
diff --git a/Strata/Languages/Laurel/EliminateValueInReturns.lean b/Strata/Languages/Laurel/EliminateValueInReturns.lean
index d209465bf6..3d274f6c48 100644
--- a/Strata/Languages/Laurel/EliminateValueInReturns.lean
+++ b/Strata/Languages/Laurel/EliminateValueInReturns.lean
@@ -95,6 +95,6 @@ end -- public section
 public def eliminateValueInReturnsPass : LoweringPass where
   name := "EliminateValueInReturns"
   documentation := "Rewrites `return expr` into `outParam := expr; return` for imperative procedures that have an output parameter. This decouples the return-value assignment from the final Core translation, which no longer needs to know about output parameters when translating returns."
-  run := fun p _m _ => (eliminateValueInReturnsTransform p, [], {})
+  run := fun _ p _m => (eliminateValueInReturnsTransform p, [], {})
 
 end Laurel
diff --git a/Strata/Languages/Laurel/HeapParameterization.lean b/Strata/Languages/Laurel/HeapParameterization.lean
index 4fb4ff74a4..daf9e9f4b7 100644
--- a/Strata/Languages/Laurel/HeapParameterization.lean
+++ b/Strata/Languages/Laurel/HeapParameterization.lean
@@ -585,7 +585,7 @@ public def heapParameterizationPass : LoweringPass where
   name := "HeapParameterization"
   documentation := "Transforms procedures that interact with the heap by adding explicit heap parameters. The heap is modeled as `Map Composite (Map Field Box)`. Procedures that write the heap receive both an input and output heap parameter; procedures that only read the heap receive an input heap parameter. Field reads and writes are rewritten to use `readField` and `updateField` functions."
   needsResolves := false -- Only resolve again after completing HeapParam, ModifiesClauses and TypeHierarchy. These are logically one pass.
-  run := fun p m _ =>
+  run := fun _ p m =>
     (heapParameterization m p, [], {})
   comesAfter := [⟨ eliminateValueInReturnsPass.meta, "eliminate value in returns need to come before any passes that change the amount of output parameters of procedures." ⟩]
   comesBefore := [⟨ liftImperativeExpressionsPass.meta, "the heap parameterization pass introduces assignments (to the heap variables) that need to be lifted."⟩]
diff --git a/Strata/Languages/Laurel/InferHoleTypes.lean b/Strata/Languages/Laurel/InferHoleTypes.lean
index 994627c3e1..029a142934 100644
--- a/Strata/Languages/Laurel/InferHoleTypes.lean
+++ b/Strata/Languages/Laurel/InferHoleTypes.lean
@@ -195,7 +195,7 @@ end -- public section
 public def inferHoleTypesPass : LoweringPass where
   name := "InferHoleTypes"
   documentation := "Annotates every verification hole (`.Hole`) in the program with a type inferred from context. This type information is needed by subsequent passes that replace holes with uninterpreted functions or nondeterministic values."
-  run := fun p m _ =>
+  run := fun _ p m =>
     let (p', diags, stats) := inferHoleTypes m p
     (p', diags, stats)
   comesBefore := [
diff --git a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
index 298b93f1b6..4e048572c5 100644
--- a/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
+++ b/Strata/Languages/Laurel/LaurelCompilationPipeline.lean
@@ -148,7 +148,7 @@ private def runLaurelPasses
   let mut allStats : Statistics := {}
 
   for pass in laurelPipeline do
-    let (program', diags, stats) ← pctx.withPhase pass.name do pure (pass.run program model options)
+    let (program', diags, stats) ← pctx.withPhase pass.name do pure (pass.run options program model)
     program := program'
     allDiags := allDiags ++ diags
     allStats := allStats.merge stats
@@ -207,13 +207,13 @@ def translateWithLaurel (options : LaurelTranslateOptions) (program : Program)
   if passDiags.any (·.type != .Warning) then
     return (none, passDiags, program, stats)
 
-  let unorderedCore := (transparencyPass.run program model options).1
+  let unorderedCore := (transparencyPass.run options program model).1
   emit "transparencyPass" "core.st" unorderedCore
   let mut unorderedCore := unorderedCore
   let mut fnModel := model
 
   for pass in unorderedCorePipeline do
-    unorderedCore := (pass.run unorderedCore fnModel options).1
+    unorderedCore := (pass.run options unorderedCore fnModel).1
     if pass.needsResolves then
       let compositeTypes := program.types.filter (fun t => match t with | .Composite _ => true | _ => false)
       let (uc', m', errors) := resolveUnorderedCore unorderedCore (some fnModel) compositeTypes
@@ -227,10 +227,10 @@ def translateWithLaurel (options : LaurelTranslateOptions) (program : Program)
       fnModel := m'
     emit pass.name "unorderedCoreWithLaurelTypes.st" unorderedCore
 
-  let coreWithLaurelTypes := (orderingPass.run unorderedCore model options).1
+  let coreWithLaurelTypes := (orderingPass.run options unorderedCore model).1
 
   emit "CoreWithLaurelTypes" "core.st" coreWithLaurelTypes
-  let (coreProgram, coreDiagnostics, _) := laurelToCoreSchemaPass.run coreWithLaurelTypes fnModel options
+  let (coreProgram, coreDiagnostics, _) := laurelToCoreSchemaPass.run options coreWithLaurelTypes fnModel
   let mut allDiagnostics: List DiagnosticModel := passDiags ++ coreDiagnostics;
 
   emit "Core" "core.st" coreProgram
diff --git a/Strata/Languages/Laurel/LaurelPass.lean b/Strata/Languages/Laurel/LaurelPass.lean
index 130ae2cf09..7a61739a16 100644
--- a/Strata/Languages/Laurel/LaurelPass.lean
+++ b/Strata/Languages/Laurel/LaurelPass.lean
@@ -16,6 +16,10 @@ public section
 structure LaurelTranslateOptions where
   inlineFunctionsWhenPossible : Bool := false
   overflowChecks : Core.OverflowChecks := {}
+  /-- Quantifier-free modifies frame for single-reference clauses. Set-valued entries
+      keep the quantified frame. If the procedure's modifies clause contains sets,
+      this option has no effect. Use with the verifier's `useArrayTheory`. -/
+  enumeratedModifiesClauses : Bool := false
   keepAllFilesPrefix : Option String := none
 
 instance : Inhabited LaurelTranslateOptions where
@@ -52,7 +56,7 @@ end
     metadata fields remain directly accessible (e.g. `p.name`). -/
 structure LaurelPass (Input: Type) (Output: Type) extends PassMeta where
   /-- The pass action. -/
-  run : Input → SemanticModel → LaurelTranslateOptions → Output × List DiagnosticModel × Statistics
+  run : LaurelTranslateOptions → Input → SemanticModel → Output × List DiagnosticModel × Statistics
 
 abbrev LoweringPass := LaurelPass Laurel.Program Laurel.Program
 
diff --git a/Strata/Languages/Laurel/LaurelToCoreSchemaPass.lean b/Strata/Languages/Laurel/LaurelToCoreSchemaPass.lean
index 3c6cda03cd..e5a62a87dd 100644
--- a/Strata/Languages/Laurel/LaurelToCoreSchemaPass.lean
+++ b/Strata/Languages/Laurel/LaurelToCoreSchemaPass.lean
@@ -806,7 +806,7 @@ public def laurelToCoreSchemaPass : LaurelPass CoreWithLaurelTypes Core.Program
   - The @[cases] parameter is inferred for recursive functions.
   - Laurel parameter definitions are translated to Core ones.
   - Laurel calling conventions are translated to Core ones."
-  run := fun p fnModel options =>
+  run := fun options p fnModel =>
     let initState : TranslateState := { model := fnModel, overflowChecks := options.overflowChecks }
     let (coreProgramOption, translateState) :=
       runTranslateM initState (translateLaurelToCore options p)
diff --git a/Strata/Languages/Laurel/LiftImperativeExpressions.lean b/Strata/Languages/Laurel/LiftImperativeExpressions.lean
index 971bafbf91..d47560585d 100644
--- a/Strata/Languages/Laurel/LiftImperativeExpressions.lean
+++ b/Strata/Languages/Laurel/LiftImperativeExpressions.lean
@@ -688,7 +688,7 @@ public def liftImperativeExpressionsPass : LaurelPass UnorderedCoreWithLaurelTyp
   documentation := "Lifts assignments and other imperative expressions that appear in expression contexts into preceding statements. This is necessary because Strata Core does not support assignments within expressions. The pass introduces fresh temporary variables where needed."
   comesAfter := [⟨ transparencyPass.meta, "The imperative expression lifting is only done in procedures, so it comes after the transparency pass"⟩]
   needsResolves := true
-  run := fun p m _ =>
+  run := fun _ p m =>
     (liftImperativeExpressionsInCore p m, [], {})
 
 end Laurel
diff --git a/Strata/Languages/Laurel/LiftInstanceProcedures.lean b/Strata/Languages/Laurel/LiftInstanceProcedures.lean
index 34ae4366c0..7486c8497e 100644
--- a/Strata/Languages/Laurel/LiftInstanceProcedures.lean
+++ b/Strata/Languages/Laurel/LiftInstanceProcedures.lean
@@ -129,7 +129,7 @@ public def liftInstanceProceduresPass : LoweringPass where
   name := "LiftInstanceProcedures"
   documentation := "Lifts every procedure declared inside a `composite` block to a top-level static procedure named `<CompositeName>$<methodName>` and rewrites call sites resolved to an instance procedure (including `obj#method(args)` surface syntax) to point at the lifted name. Clears `instanceProcedures` on every composite. Must run before HeapParameterization."
   needsResolves := true
-  run := fun p m _ => (liftInstanceProcedures m p, [], {})
+  run := fun _ p m => (liftInstanceProcedures m p, [], {})
   comesBefore := [⟨ eliminateValueInReturnsPass.meta, "eliminateValueInReturns only applies to static methods, hence all instance methods must have been lifted before." ⟩]
 
 end Strata.Laurel
diff --git a/Strata/Languages/Laurel/MergeAndLiftReturns.lean b/Strata/Languages/Laurel/MergeAndLiftReturns.lean
index 06f44102d1..28a40b215a 100644
--- a/Strata/Languages/Laurel/MergeAndLiftReturns.lean
+++ b/Strata/Languages/Laurel/MergeAndLiftReturns.lean
@@ -93,7 +93,7 @@ public def mergeAndLiftReturnsPass : LoweringPass where
   documentation := "Attempts to merge and lift returns so that only a single outer return remains, enabling the procedure to be more easily converted to a functional form."
   needsResolves := true
   comesBefore := [⟨ eliminateValueInReturnsPass.meta, "Lifts returns with a value, so the value should not yet have been lowered."⟩]
-  run := fun p _m _ =>
+  run := fun _ p _m =>
     let (p', diags) := mergeAndLiftReturns p
     (p', diags, {})
 
diff --git a/Strata/Languages/Laurel/ModifiesClauses.lean b/Strata/Languages/Laurel/ModifiesClauses.lean
index dbe7eef50f..8b4817224f 100644
--- a/Strata/Languages/Laurel/ModifiesClauses.lean
+++ b/Strata/Languages/Laurel/ModifiesClauses.lean
@@ -11,28 +11,12 @@ import Strata.Languages.Laurel.HeapParameterizationConstants
 import Strata.Languages.Laurel.HeapParameterization
 import Strata.Languages.Laurel.Grammar.AbstractToConcreteTreeTranslator
 import Strata.Languages.Laurel.LaurelTypes
+import Strata.Languages.Laurel.MapStmtExpr
 
 /-
-Modifies clause transformation (Laurel → Laurel).
-
-Transforms procedures with modifies clauses by generating a frame condition
-and conjoining it with the postcondition. After this pass, the modifies list
-is cleared since its semantics have been absorbed into the postcondition.
-
-This pass should run after heap parameterization, which has already:
-- Added explicit heap parameter ($heap as inout)
-- Transformed field accesses to readField/updateField calls
-- Collected field constants
-
-The frame condition states: for every object not mentioned in the modifies clause,
-all field values are preserved between the input and output heaps.
-
-Generates:
-  forall $obj: Composite, $fld: Field =>
-    $obj < old($heap).nextReference && notModified($obj) ==> readField(old($heap), $obj, $fld) == readField($heap, $obj, $fld)
-
-where `notModified($obj)` is the conjunction of `$obj != e` for each single entry `e`,
-and `!(select(s, $obj))` for each set entry `s`.
+Modifies clause transformation (Laurel → Laurel), run after heap parameterization:
+generate a frame per `modifies` clause and clear it. Under array theory with only
+individual refs, callers assume a quantifier-free frame and the body checks it per exit.
 -/
 
 namespace Strata.Laurel
@@ -91,45 +75,64 @@ def conjoinAll (exprs : List StmtExprMd) : StmtExprMd :=
   | first :: rest => rest.foldl (fun acc e => mkMd <| .PrimitiveOp .And [acc, e]) first
 
 /--
-Build the modifies frame condition as a Laurel StmtExpr.
-
-Generates a single quantified formula:
+Quantified (pointwise) frame: every allocated object the `modifies` clause does not name keeps
+all of its field values across the call.
 
   forall $obj: Composite, $fld: Field =>
     notModified($obj) && $obj < old($heap).nextReference ==> readField(old($heap), $obj, $fld) == readField($heap, $obj, $fld)
-
-Returns `none` if there are no entries.
 -/
-def buildModifiesEnsures (proc: Procedure) (model: SemanticModel) (modifiesExprs : List StmtExprMd)
-    (heapName : Identifier) : Option StmtExprMd :=
-  let entries := extractModifiesEntries model modifiesExprs
+def buildQuantifiedFrame (proc : Procedure) (entries : List ModifiesEntry)
+    (heapIn heapOut : StmtExprMd) : StmtExprMd :=
   let objName : Identifier := "$modifies_obj"
   let fldName : Identifier := "$modifies_fld"
   let obj := mkMd <| .Var (.Local objName)
   let fld := mkMd <| .Var (.Local fldName)
-  let heapIn := mkMd <| .Old (mkMd (.Var (.Local heapName)))
-  let heapOut := mkMd <| .Var (.Local heapName)
-      -- Build the "obj is allocated" condition: Composite..ref($obj) < old($heap).nextReference
   let heapCounter := mkMd <| .StaticCall "Heap..nextReference!" [heapIn]
   let objRef := mkMd <| .StaticCall "Composite..ref!" [obj]
   let objAllocated := mkMd <| .PrimitiveOp .Lt [objRef, heapCounter]
   let antecedent := if entries.isEmpty
     then objAllocated
     else
-      -- Build the "not modified" precondition from all entries
-      -- Combine: $obj < old($heap).nextReference && notModified($obj)
       let notModified := conjoinAll (entries.map (buildNotModifiedForEntry obj))
       mkMd <| .PrimitiveOp .And [objAllocated, notModified]
-  -- Build: readField(old($heap), $obj, $fld) == readField($heap, $obj, $fld)
   let readIn := mkMd <| .StaticCall "readField" [heapIn, obj, fld]
   let readOut := mkMd <| .StaticCall "readField" [heapOut, obj, fld]
   let heapUnchanged := mkMd <| .PrimitiveOp .Eq [readIn, readOut]
-  -- Build: antecedent ==> heapUnchanged
   let implBody := mkMd <| .PrimitiveOp .Implies [antecedent, heapUnchanged]
-  -- Build: forall $obj: Composite, $fld: Field => ...
   let innerForall := mkMd <| .Quantifier .Forall ⟨ fldName, { val := .UserDefined "Field", source := none } ⟩ none implBody
-  let outerForall : StmtExprMd := { val := .Quantifier .Forall ⟨ objName, { val := .UserDefined "Composite", source := none } ⟩ none innerForall, source := proc.name.source }
-  some outerForall
+  { val := .Quantifier .Forall ⟨ objName, { val := .UserDefined "Composite", source := none } ⟩ none innerForall, source := proc.name.source }
+
+/-- Quantifier-free frame: output `data` equals input with only the named rows
+overwritten, and `nextReference` is monotone. -/
+def buildEnumeratedFrame (proc : Procedure) (entries : List ModifiesEntry)
+    (heapIn heapOut : StmtExprMd) : StmtExprMd :=
+  let data h := mkMd <| .StaticCall "Heap..data!" [h]
+  let nextRef h := mkMd <| .StaticCall "Heap..nextReference!" [h]
+  let dataOut := data heapOut
+  let modifiedRefs := entries.filterMap fun e => match e with | .single r => some r | _ => none
+  let framedData := modifiedRefs.foldr
+    (fun ref acc => mkMd <| .StaticCall "update" [acc, ref, mkMd <| .StaticCall "select" [dataOut, ref]])
+    (data heapIn)
+  let dataPreserved := mkMd <| .PrimitiveOp .Eq [dataOut, framedData]
+  let refsMonotone := mkMd <| .PrimitiveOp .Leq [nextRef heapIn, nextRef heapOut]
+  { val := .PrimitiveOp .And [dataPreserved, refsMonotone], source := proc.name.source }
+
+/-- True when the `modifies` clause is non-empty and names only individual references
+(no set-valued entries), so the enumerated frame applies. -/
+def onlyIndividualRefs (entries : List ModifiesEntry) : Bool :=
+  !entries.isEmpty && entries.all fun e => match e with | .single _ => true | _ => false
+
+/-- Assert `frame` before every exit of `body` (`return` and body-block `exit`) and at its end. -/
+def insertFrameChecks (proc : Procedure) (frame : StmtExprMd) (body : StmtExprMd) : StmtExprMd :=
+  let src := proc.name.source
+  let check : StmtExprMd := { val := .Assert { condition := frame, summary := "modifies clause" }, source := src }
+  let wrap (e : StmtExprMd) : StmtExprMd := { val := .Block [check, e] none, source := e.source }
+  let beforeExits := mapStmtExpr (fun e =>
+    match e.val with
+    | .Return _ => wrap e
+    | .Exit l => if l == bodyLabel then wrap e else e
+    | _ => e) body
+  { val := .Block [beforeExits, check] none, source := src }
 
 /--
 Check whether a procedure has a `$heap` output parameter,
@@ -138,35 +141,32 @@ indicating it mutates the heap.
 def hasHeapOut (proc : Procedure) : Bool :=
   proc.outputs.any (fun p => p.name.text == "$heap")
 
-/--
-Transform a single procedure: if it has modifies clauses, generate the frame
-condition and conjoin it with the postcondition, then clear the modifies list.
-
-If the procedure has `modifies *`, no frame condition is generated (the procedure
-may modify anything on the heap), and the modifies list is simply cleared.
-
-If the procedure has a `$heap` but no modifies clause, adds a postcondition
-that all allocated objects are preserved between heaps:
-  `forall $obj: Composite, $fld: Field => $obj < old($heap).nextReference ==> readField(old($heap), $obj, $fld) == readField($heap, $obj, $fld)`
-
-If the modifies clause uses a wildcard (`*`), the frame condition is skipped
-entirely — the procedure may modify anything.
--/
+/-- Build and attach `proc`'s modifies frame, then clear the clause. -/
 def transformModifiesClauses (model: SemanticModel)
-    (proc : Procedure) : Except (Array DiagnosticModel) Procedure :=
+    (proc : Procedure) (useEnumeratedFrame : Bool) : Except (Array DiagnosticModel) Procedure :=
   match proc.body with
   | .External => .ok proc
   | .Opaque postconds impl modifiesExprs =>
       if hasModifiesWildcard modifiesExprs then
-        -- modifies * means the procedure can modify anything; no frame condition
         .ok { proc with body := .Opaque postconds impl [] }
       else if hasHeapOut proc then
-        let heapName := heapVarName
-        let frameCondition := buildModifiesEnsures proc model modifiesExprs heapName
-        let postconds' := match frameCondition with
-          | some frame => postconds ++ [{ condition := frame, summary := "modifies clause" }]
-          | none => postconds
-        .ok { proc with body := .Opaque postconds' impl [] }
+        let entries := extractModifiesEntries model modifiesExprs
+        let heapIn := mkMd <| .Old (mkMd (.Var (.Local heapVarName)))
+        let heapOut := mkMd <| .Var (.Local heapVarName)
+        if useEnumeratedFrame && onlyIndividualRefs entries then
+          -- Callers assume the quantifier-free frame; the body re-checks the
+          -- pointwise frame at every exit.
+          let pointwise := buildQuantifiedFrame proc entries heapIn heapOut
+          let framePost : Condition :=
+            { condition := buildEnumeratedFrame proc entries heapIn heapOut,
+              summary := "modifies clause", free := true }
+          let impl' := impl.map (insertFrameChecks proc pointwise)
+          .ok { proc with body := .Opaque (postconds ++ [framePost]) impl' [] }
+        else
+          let framePost : Condition :=
+            { condition := buildQuantifiedFrame proc entries heapIn heapOut,
+              summary := "modifies clause" }
+          .ok { proc with body := .Opaque (postconds ++ [framePost]) impl [] }
       else
         .ok proc
   | _ => .ok proc
@@ -223,9 +223,9 @@ This is a Laurel → Laurel pass that should run after heap parameterization.
 Always returns the (best-effort) transformed program together with any diagnostics,
 so that later passes can continue and report additional errors.
 -/
-def modifiesClausesTransform (model: SemanticModel) (program : Program) : Program × List DiagnosticModel :=
+def modifiesClausesTransform (model: SemanticModel) (program : Program) (useEnumeratedFrame : Bool) : Program × List DiagnosticModel :=
   let (procs', errors) := program.staticProcedures.foldl (fun (acc, errs) proc =>
-    match transformModifiesClauses model proc with
+    match transformModifiesClauses model proc useEnumeratedFrame with
     | .ok proc' => (acc ++ [proc'], errs)
     | .error newErrs => (acc ++ [proc], errs ++ newErrs.toList)
   ) ([], [])
@@ -237,18 +237,18 @@ end -- public section
 public def filterNonCompositeModifiesPass : LoweringPass where
   name := "FilterNonCompositeModifies"
   documentation := "Filters modifies clauses that refer to non-composite types (e.g. primitives), which cannot be heap-parameterized. Emits a warning for each removed clause. Should run before heap parameterization so that phase remains agnostic to modifies clauses."
-  run := fun p m _ =>
+  run := fun _ p m =>
     let (p', diags) := filterNonCompositeModifies m p
     (p', diags, {})
 
 /-- Pipeline pass: translate modifies clauses into ensures clauses. -/
 public def modifiesClausesTransformPass : LoweringPass where
   name := "ModifiesClausesTransform"
-  documentation := "Translates modifies clauses into additional ensures clauses. The modifies clause of a procedure is translated into a quantified assertion that states objects not mentioned in the modifies clause have their field values preserved between the input and output heap."
+  documentation := "Translate modifies clauses into frame conditions on the contract."
   needsResolves := true
   comesAfter := [⟨ heapParameterizationPass.meta, "the modifies pass refers to several types and variables introduced by heap parameterization: Composite, Field, $heap_in, $heap."⟩]
-  run := fun p m _ =>
-    let (p', diags) := modifiesClausesTransform m p
+  run := fun options p m =>
+    let (p', diags) := modifiesClausesTransform m p (useEnumeratedFrame := options.enumeratedModifiesClauses)
     (p', diags, {})
 
 end Strata.Laurel
diff --git a/Strata/Languages/Laurel/PushOldInward.lean b/Strata/Languages/Laurel/PushOldInward.lean
index c9db47123a..dfd190d1a0 100644
--- a/Strata/Languages/Laurel/PushOldInward.lean
+++ b/Strata/Languages/Laurel/PushOldInward.lean
@@ -80,7 +80,7 @@ def pushOldInward (program : Program) : Program × List DiagnosticModel :=
 public def pushOldInwardPass : LoweringPass where
   name := "pushOldInward"
   documentation := "Distributes `old(...)` over its subexpressions until each `old` immediately wraps an inout variable. Warns on `old(e)` where `e` mentions no inout parameter and on nested `old(old(...))`."
-  run := fun p _ _ =>
+  run := fun _ p _ =>
     let (p', diags) := pushOldInward p
     (p', diags, {})
 
diff --git a/Strata/Languages/Laurel/TransparencyPass.lean b/Strata/Languages/Laurel/TransparencyPass.lean
index c44751ff96..9ed040c98a 100644
--- a/Strata/Languages/Laurel/TransparencyPass.lean
+++ b/Strata/Languages/Laurel/TransparencyPass.lean
@@ -171,7 +171,7 @@ For each procedure:
   - Generate a function with the same signature, named `foo$asFunction`
   - If transparent, the function gets a functional body (assertions erased, calls to functional versions)
   - If the function has a body, add a free postcondition equating the procedure output to the function"
-  run := fun p _ _ =>
+  run := fun _ p _ =>
     (createFunctionsForTransparentBodies p, [], {})
 
 end -- public section
diff --git a/Strata/Languages/Laurel/TypeAliasElim.lean b/Strata/Languages/Laurel/TypeAliasElim.lean
index 65a3a462e2..a3af677f35 100644
--- a/Strata/Languages/Laurel/TypeAliasElim.lean
+++ b/Strata/Languages/Laurel/TypeAliasElim.lean
@@ -65,6 +65,6 @@ public def typeAliasElimPass : LoweringPass where
   name := "TypeAliasElim"
   documentation := "Eliminates type aliases by replacing all UserDefined references to alias names with their resolved target types. Chained aliases are resolved transitively. Alias entries are removed from the type list."
   needsResolves := true
-  run := fun p m _ => (typeAliasElim m p, [], {})
+  run := fun _ p m => (typeAliasElim m p, [], {})
 
 end Strata.Laurel
diff --git a/Strata/Languages/Laurel/TypeHierarchy.lean b/Strata/Languages/Laurel/TypeHierarchy.lean
index 0414298e6a..079eb38be0 100644
--- a/Strata/Languages/Laurel/TypeHierarchy.lean
+++ b/Strata/Languages/Laurel/TypeHierarchy.lean
@@ -193,7 +193,7 @@ public def typeHierarchyTransformPass : LoweringPass where
   documentation := "Encodes the object-oriented type hierarchy (inheritance, dynamic dispatch, type tests, and casts) into explicit operations on a flat representation. Composite types with parents are flattened, and dynamic dispatch is resolved through type-test chains."
   needsResolves := false -- Only resolve again after completing HeapParam, ModifiesClauses and TypeHierarchy. These are logically one pass.
   comesAfter := [⟨ heapParameterizationPass.meta, "the type hierarchy pass modifies the 'Composite' datatype that is introduced by this pass."⟩]
-  run := fun p m _ =>
+  run := fun _ p m =>
     (typeHierarchyTransform m p, [], {})
 
 end Strata.Laurel
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T2c_ModifiesClausesArrayTheory.lean b/StrataTest/Languages/Laurel/Examples/Objects/T2c_ModifiesClausesArrayTheory.lean
new file mode 100644
index 0000000000..b6c820e22d
--- /dev/null
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T2c_ModifiesClausesArrayTheory.lean
@@ -0,0 +1,126 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+/-
+Under `--use-array-theory`, the `ModifiesClauses` pass emits a quantifier-free
+heap-equation frame —
+  `data!($heap) == update(data!(old), ref, select(data!($heap), ref))`
+— instead of the `forall obj fld. notModified(obj) ==> readField(old) == readField(new)`
+form. The same procedures must verify under either encoding; this pins the
+array-theory path. Mirrors `T2_ModifiesClauses` but with `useArrayTheory := true`.
+-/
+
+import StrataTest.Util.TestLaurel
+
+open StrataTest.Util
+open Strata
+
+#eval testLaurel
+    (options := { defaultLaurelTestOptions with
+      translateOptions := { defaultLaurelTestOptions.translateOptions with enumeratedModifiesClauses := true },
+      verifyOptions := { defaultLaurelTestOptions.verifyOptions with useArrayTheory := true } }) <|
+#strata
+program Laurel;
+composite Container {
+  var value: int
+}
+
+procedure modifyContainerOpaque(c: Container) returns (b: bool)
+  opaque
+  modifies c
+{
+  c#value := c#value + 1;
+  true
+};
+
+procedure caller()
+  opaque
+{
+  var c: Container := new Container;
+  var d: Container := new Container;
+  var x: int := d#value;
+  var b: bool := modifyContainerOpaque(c);
+  assert x == d#value // pass: d#value is preserved (d ∉ modifies)
+};
+
+procedure multipleModifiesClauses(c: Container, d: Container, e: Container)
+  opaque
+  modifies c
+  modifies d
+;
+
+procedure multipleModifiesClausesCaller()
+  opaque
+{
+  var c: Container := new Container;
+  var d: Container := new Container;
+  var e: Container := new Container;
+  var x: int := e#value;
+  multipleModifiesClauses(c, d, e);
+  assert x == e#value // pass: e is preserved (not in the modifies set)
+};
+
+procedure newObjectDoNotCountForModifies()
+  opaque
+{
+  var c: Container := new Container;
+  c#value := 1
+};
+
+// Regression: an allocating body verifies under array theory (bodies use the pointwise frame).
+procedure allocatesInModifiesBody(c: Container) returns (b: bool)
+  opaque
+  modifies c
+{
+  c#value := c#value + 1;
+  var t: Container := new Container;
+  t#value := 99;
+  true
+};
+
+// Regression: a body that allocates via a CALL still verifies (the callee
+// newObjectDoNotCountForModifies grows the heap); the pointwise frame tolerates it.
+procedure allocatesViaCall(c: Container) returns (b: bool)
+  opaque
+  modifies c
+{
+  c#value := c#value + 1;
+  newObjectDoNotCountForModifies();
+  true
+};
+
+// Soundness: writes outside the modifies clause are still rejected.
+
+procedure modifyContainerWithoutPermission2(c: Container, d: Container)
+//        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: modifies clause does not hold
+  opaque
+  modifies d
+{
+    c#value := 2
+};
+
+procedure modifyContainerWithoutPermission3(c: Container, d: Container)
+//        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ error: modifies clause could not be proved
+  opaque
+  modifies d
+{
+    var i: bool := modifyContainerOpaque(c)
+};
+
+// Soundness: an illegal write on an EARLY-RETURN path is rejected. Exercises the
+// frame assert inserted before each exit, not just the fall-through tail.
+procedure modifyOnEarlyReturnPath(c: Container, d: Container) returns (b: bool)
+//        ^^^^^^^^^^^^^^^^^^^^^^^ error: modifies clause does not hold
+  opaque
+  modifies d
+{
+  if c#value > 0 then {
+    c#value := 1;
+    return true
+  };
+  return false
+};
+#end
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T2d_ModifiesFrameSoundness.lean b/StrataTest/Languages/Laurel/Examples/Objects/T2d_ModifiesFrameSoundness.lean
new file mode 100644
index 0000000000..a4eb274bd9
--- /dev/null
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T2d_ModifiesFrameSoundness.lean
@@ -0,0 +1,298 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+/-
+Soundness of the quantifier-free modifies frame under `--use-array-theory`: illegal
+writes are rejected, legal shapes verify, callers may assume the free frame, and a
+fresh object exposed to a caller is not pinned by it.
+-/
+
+import StrataTest.Util.TestLaurel
+
+open StrataTest.Util
+open Strata
+
+private def arrayTheoryOpts :=
+  { defaultLaurelTestOptions with
+    translateOptions := { defaultLaurelTestOptions.translateOptions with enumeratedModifiesClauses := true },
+    verifyOptions := { defaultLaurelTestOptions.verifyOptions with useArrayTheory := true } }
+
+/-! ## 1. Illegal writes are rejected -/
+
+#eval testLaurel (options := arrayTheoryOpts) <|
+#strata
+program Laurel;
+composite Container {
+  var value: int
+}
+
+procedure writeNonFrameConditional(c: Container, d: Container)
+//        ^^^^^^^^^^^^^^^^^^^^^^^^ error: modifies clause does not hold
+  opaque
+  modifies d
+{
+  if d#value > 0 then {
+    c#value := 7
+  }
+};
+
+procedure writeAfterEarlyReturn(c: Container, d: Container) returns (b: bool)
+//        ^^^^^^^^^^^^^^^^^^^^^ error: modifies clause does not hold
+  opaque
+  modifies d
+{
+  if d#value > 100 then {
+    return true
+  };
+  c#value := 7;
+  return false
+};
+
+procedure writeOneOfManyNonFrame(c: Container, d: Container, e: Container)
+//        ^^^^^^^^^^^^^^^^^^^^^^ error: modifies clause does not hold
+  opaque
+  modifies c
+  modifies d
+{
+  e#value := 9
+};
+
+procedure writeFrameAndNonFrame(c: Container, d: Container)
+//        ^^^^^^^^^^^^^^^^^^^^^ error: modifies clause does not hold
+  opaque
+  modifies c
+{
+  c#value := 1;
+  d#value := 2
+};
+
+procedure writeNestedIf(c: Container, d: Container)
+//        ^^^^^^^^^^^^^ error: modifies clause does not hold
+  opaque
+  modifies d
+{
+  if d#value > 0 then {
+    if d#value > 5 then {
+      c#value := 1
+    }
+  }
+};
+#end
+
+/-! ## 2. Legal shapes still verify -/
+
+#eval testLaurel (options := arrayTheoryOpts) <|
+#strata
+program Laurel;
+composite Container {
+  var value: int
+}
+
+procedure writeFrameConditional(c: Container)
+  opaque
+  modifies c
+{
+  if c#value > 0 then {
+    c#value := c#value + 1
+  }
+};
+
+procedure modifyThenEarlyReturn(c: Container) returns (b: bool)
+  opaque
+  modifies c
+{
+  c#value := 1;
+  if c#value > 0 then {
+    return true
+  };
+  return false
+};
+
+procedure modifyTwoDeclared(c: Container, d: Container)
+  opaque
+  modifies c
+  modifies d
+{
+  c#value := 1;
+  d#value := 2
+};
+
+procedure allocThenModifyDeclared(c: Container)
+  opaque
+  modifies c
+{
+  var t: Container := new Container;
+  t#value := 99;
+  c#value := 5
+};
+#end
+
+/-! ## 3. Callers may assume the free frame; it does not over-promise -/
+
+#eval testLaurel (options := arrayTheoryOpts) <|
+#strata
+program Laurel;
+composite Container {
+  var value: int
+}
+
+procedure bodyModifier(c: Container) returns (b: bool)
+  opaque
+  modifies c
+{
+  c#value := c#value + 1;
+  true
+};
+
+procedure allocatingBody(c: Container) returns (b: bool)
+  opaque
+  modifies c
+{
+  c#value := c#value + 1;
+  var t: Container := new Container;
+  t#value := 99;
+  true
+};
+
+procedure bodyModifierTwo(c: Container, d: Container)
+  opaque
+  modifies c
+  modifies d
+{
+  c#value := 1;
+  d#value := 2
+};
+
+procedure callerUnrelatedPreserved()
+  opaque
+{
+  var c: Container := new Container;
+  var d: Container := new Container;
+  var x: int := d#value;
+  var b: bool := bodyModifier(c);
+  assert x == d#value
+};
+
+procedure callerModifiedNotPreserved()
+  opaque
+{
+  var c: Container := new Container;
+  var x: int := c#value;
+  var b: bool := bodyModifier(c);
+  assert x == c#value
+//^^^^^^^^^^^^^^^^^^^ error: assertion could not be proved
+};
+
+procedure callerExactValuePreserved()
+  opaque
+{
+  var c: Container := new Container;
+  var d: Container := new Container;
+  d#value := 5;
+  var b: bool := bodyModifier(c);
+  assert d#value == 5
+};
+
+procedure callerOfAllocatingBody()
+  opaque
+{
+  var c: Container := new Container;
+  var d: Container := new Container;
+  var x: int := d#value;
+  var b: bool := allocatingBody(c);
+  assert x == d#value
+};
+
+procedure callerMultiUnrelated()
+  opaque
+{
+  var c: Container := new Container;
+  var d: Container := new Container;
+  var e: Container := new Container;
+  var x: int := e#value;
+  bodyModifierTwo(c, d);
+  assert x == e#value
+};
+#end
+
+/-! ## 4. Multiple exits and bodiless/body parity -/
+
+#eval testLaurel (options := arrayTheoryOpts) <|
+#strata
+program Laurel;
+composite Container {
+  var value: int
+}
+
+procedure multiExitAllLegal(c: Container) returns (b: bool)
+  opaque
+  modifies c
+{
+  c#value := 1;
+  if c#value > 0 then {
+    c#value := 2;
+    return true
+  };
+  c#value := 3;
+  return false
+};
+
+procedure illegalAfterLegalEarlyExit(c: Container, d: Container) returns (b: bool)
+//        ^^^^^^^^^^^^^^^^^^^^^^^^^^ error: modifies clause does not hold
+  opaque
+  modifies c
+{
+  if c#value > 0 then {
+    c#value := 1;
+    return true
+  };
+  d#value := 9;
+  return false
+};
+
+procedure bodilessModifier(c: Container)
+  opaque
+  modifies c;
+
+procedure callerOfBodiless()
+  opaque
+{
+  var c: Container := new Container;
+  var d: Container := new Container;
+  var x: int := d#value;
+  bodilessModifier(c);
+  assert x == d#value
+};
+#end
+
+/-! ## 5. A fresh object exposed to a caller is not pinned by the frame -/
+
+#eval testLaurel (options := arrayTheoryOpts) <|
+#strata
+program Laurel;
+composite Container {
+  var value: int
+  var child: Container
+}
+
+procedure stashFresh(c: Container)
+  opaque
+  modifies c
+{
+  var t: Container := new Container;
+  t#value := 42;
+  c#child := t
+};
+
+procedure callerCannotPinFreshField()
+  opaque
+{
+  var c: Container := new Container;
+  stashFresh(c);
+  assert c#child#value == 42
+//^^^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion could not be proved
+};
+#end
diff --git a/StrataTest/Languages/Laurel/Examples/Objects/T2e_ModifiesArrayTheoryPerf.lean b/StrataTest/Languages/Laurel/Examples/Objects/T2e_ModifiesArrayTheoryPerf.lean
new file mode 100644
index 0000000000..9b1acea61d
--- /dev/null
+++ b/StrataTest/Languages/Laurel/Examples/Objects/T2e_ModifiesArrayTheoryPerf.lean
@@ -0,0 +1,121 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+/-
+Perf / regression: the array-theory frame is not merely faster, it is more
+complete on heap-heavy code.
+
+`stress` makes a deep chain of opaque heap-modifying calls on freshly allocated
+objects, then asserts that an object allocated *before* the chain is untouched.
+
+  - Under the `∀` frame (array theory off) the solver cannot instantiate the
+    quantified frame across the whole chain: the assertion "could not be proved".
+    This is a definite verdict in ~2s, not a wall-clock timeout.
+  - Under the quantifier-free frame (`--use-array-theory`) the same assertion
+    verifies: each step is a `store` on a single row, so the read of the
+    untouched object is a pure array rewrite with nothing to instantiate.
+
+The two blocks are identical apart from `useArrayTheory`.
+
+Note: the `∀` outcome depends on the SMT solver's quantifier heuristics. If a
+future solver discharges it, the annotation below must be updated.
+-/
+
+import StrataTest.Util.TestLaurel
+
+open StrataTest.Util
+open Strata
+
+-- ∀ frame (array theory off): the chain defeats quantifier instantiation.
+#eval testLaurel
+    (options := { defaultLaurelTestOptions with
+      translateOptions := { defaultLaurelTestOptions.translateOptions with enumeratedModifiesClauses := false },
+      verifyOptions := { defaultLaurelTestOptions.verifyOptions with useArrayTheory := false } }) <|
+#strata
+program Laurel;
+composite Container {
+  var value: int
+}
+
+procedure modifyOne(c: Container)
+  opaque
+  modifies c;
+
+procedure stress()
+  opaque
+  modifies *
+{
+  var target: Container := new Container;
+  var x: int := target#value;
+  var c0: Container := new Container; modifyOne(c0);
+  var c1: Container := new Container; modifyOne(c1);
+  var c2: Container := new Container; modifyOne(c2);
+  var c3: Container := new Container; modifyOne(c3);
+  var c4: Container := new Container; modifyOne(c4);
+  var c5: Container := new Container; modifyOne(c5);
+  var c6: Container := new Container; modifyOne(c6);
+  var c7: Container := new Container; modifyOne(c7);
+  var c8: Container := new Container; modifyOne(c8);
+  var c9: Container := new Container; modifyOne(c9);
+  var c10: Container := new Container; modifyOne(c10);
+  var c11: Container := new Container; modifyOne(c11);
+  var c12: Container := new Container; modifyOne(c12);
+  var c13: Container := new Container; modifyOne(c13);
+  var c14: Container := new Container; modifyOne(c14);
+  var c15: Container := new Container; modifyOne(c15);
+  var c16: Container := new Container; modifyOne(c16);
+  var c17: Container := new Container; modifyOne(c17);
+  var c18: Container := new Container; modifyOne(c18);
+  var c19: Container := new Container; modifyOne(c19);
+  assert x == target#value
+//^^^^^^^^^^^^^^^^^^^^^^^^ error: assertion could not be proved
+};
+#end
+
+-- Quantifier-free frame (--use-array-theory): the same program verifies.
+#eval testLaurel
+    (options := { defaultLaurelTestOptions with
+      translateOptions := { defaultLaurelTestOptions.translateOptions with enumeratedModifiesClauses := true },
+      verifyOptions := { defaultLaurelTestOptions.verifyOptions with useArrayTheory := true } }) <|
+#strata
+program Laurel;
+composite Container {
+  var value: int
+}
+
+procedure modifyOne(c: Container)
+  opaque
+  modifies c;
+
+procedure stress()
+  opaque
+  modifies *
+{
+  var target: Container := new Container;
+  var x: int := target#value;
+  var c0: Container := new Container; modifyOne(c0);
+  var c1: Container := new Container; modifyOne(c1);
+  var c2: Container := new Container; modifyOne(c2);
+  var c3: Container := new Container; modifyOne(c3);
+  var c4: Container := new Container; modifyOne(c4);
+  var c5: Container := new Container; modifyOne(c5);
+  var c6: Container := new Container; modifyOne(c6);
+  var c7: Container := new Container; modifyOne(c7);
+  var c8: Container := new Container; modifyOne(c8);
+  var c9: Container := new Container; modifyOne(c9);
+  var c10: Container := new Container; modifyOne(c10);
+  var c11: Container := new Container; modifyOne(c11);
+  var c12: Container := new Container; modifyOne(c12);
+  var c13: Container := new Container; modifyOne(c13);
+  var c14: Container := new Container; modifyOne(c14);
+  var c15: Container := new Container; modifyOne(c15);
+  var c16: Container := new Container; modifyOne(c16);
+  var c17: Container := new Container; modifyOne(c17);
+  var c18: Container := new Container; modifyOne(c18);
+  var c19: Container := new Container; modifyOne(c19);
+  assert x == target#value
+};
+#end
diff --git a/StrataTest/Languages/Laurel/ModifiesFrameExitChecksTest.lean b/StrataTest/Languages/Laurel/ModifiesFrameExitChecksTest.lean
new file mode 100644
index 0000000000..51087b7eec
--- /dev/null
+++ b/StrataTest/Languages/Laurel/ModifiesFrameExitChecksTest.lean
@@ -0,0 +1,32 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+/-
+`insertFrameChecks` asserts the frame before every procedure exit (a `return` or an
+`exit` of the body block) and at the fall-through tail, but not before an `exit` of
+another label. Each wrap plus the tail adds one `assert`, so the counts pin which
+exits are instrumented, including the `exit bodyLabel` arm no frontend reaches.
+-/
+
+import Strata.Languages.Laurel.ModifiesClauses
+
+open Strata.Laurel
+
+namespace StrataTest.Laurel.ModifiesFrameExitChecks
+
+private def frame : StmtExprMd := { val := .LiteralBool true, source := none }
+private def node (e : StmtExpr) : StmtExprMd := { val := e, source := none }
+private def assertCount (e : StmtExprMd) : Nat :=
+  (reprStr e |>.splitOn "assert").length - 1
+
+#guard assertCount (insertFrameChecks default frame (node (.Return none))) == 2
+#guard assertCount (insertFrameChecks default frame (node (.Exit bodyLabel))) == 2
+#guard assertCount (insertFrameChecks default frame (node (.Exit "loop"))) == 1
+#guard assertCount
+  (insertFrameChecks default frame
+    (node (.Block [node (.Exit bodyLabel), node (.Exit "loop")] none))) == 2
+
+end StrataTest.Laurel.ModifiesFrameExitChecks
diff --git a/StrataTest/Languages/Laurel/ModifiesFrameQuantifierFreeTest.lean b/StrataTest/Languages/Laurel/ModifiesFrameQuantifierFreeTest.lean
new file mode 100644
index 0000000000..6dd53c1b45
--- /dev/null
+++ b/StrataTest/Languages/Laurel/ModifiesFrameQuantifierFreeTest.lean
@@ -0,0 +1,34 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+/-
+Structural check, independent of the solver: the enumerated modifies frame
+(`buildEnumeratedFrame`) must contain no quantifier, so there is nothing for the
+solver to instantiate. The `∀`-based frame it replaces (`buildQuantifiedFrame`)
+does contain one; asserting both pins the property and shows the check
+discriminates between the two encodings.
+-/
+
+import Strata.Languages.Laurel.ModifiesClauses
+
+open Strata.Laurel
+
+namespace StrataTest.Laurel.ModifiesFrameQuantifierFree
+
+private def selfRef : StmtExprMd := { val := .Var (.Local "self"), source := none }
+private def heapIn  : StmtExprMd := { val := .Var (.Local "$heap_in"), source := none }
+private def heapOut : StmtExprMd := { val := .Var (.Local "$heap"), source := none }
+private def singleRefModifies : List ModifiesEntry := [.single selfRef]
+
+/-- Whether the (pretty-printed) frame mentions a quantifier. -/
+private def hasQuantifier (e : StmtExprMd) : Bool :=
+  let s := reprStr e
+  (s.splitOn "forall").length > 1 || (s.splitOn "exists").length > 1
+
+#guard !hasQuantifier (buildEnumeratedFrame default singleRefModifies heapIn heapOut)
+#guard  hasQuantifier (buildQuantifiedFrame   default singleRefModifies heapIn heapOut)
+
+end StrataTest.Laurel.ModifiesFrameQuantifierFree