diff --git a/Strata/DDM/AST.lean b/Strata/DDM/AST.lean
index 92b9608e9..cf4d502c8 100644
--- a/Strata/DDM/AST.lean
+++ b/Strata/DDM/AST.lean
@@ -8,6 +8,7 @@ module
 public import Std.Data.HashMap.Basic
 public import Strata.DDM.Util.ByteArray
 public import Strata.DDM.Util.Decimal
+public import Lean.Data.Position
 public import Strata.DDM.AST.Datatype
 
 import Std.Data.HashMap
@@ -17,6 +18,7 @@ set_option autoImplicit false
 
 public section
 namespace Strata
+open Std (ToFormat Format format)
 
 abbrev DialectName := String
 
@@ -234,7 +236,7 @@ structure SourceRange where
   start : String.Pos.Raw
   /-- One past the end of the range. -/
   stop : String.Pos.Raw
-deriving BEq, Inhabited, Repr
+deriving DecidableEq, Inhabited, Repr
 
 namespace SourceRange
 
@@ -242,8 +244,38 @@ def none : SourceRange := { start := 0, stop := 0 }
 
 def isNone (loc : SourceRange) : Bool := loc.start = 0 ∧ loc.stop = 0
 
+instance : ToFormat SourceRange where
+ format fr := f!"{fr.start}-{fr.stop}"
+
 end SourceRange
 
+inductive Uri where
+  | file (path: String)
+  deriving DecidableEq, Repr, Inhabited
+
+instance : ToFormat Uri where
+ format fr := match fr with | .file path => path
+
+structure FileRange where
+  file: Uri
+  range: Strata.SourceRange
+  deriving DecidableEq, Repr, Inhabited
+
+instance : ToFormat FileRange where
+ format fr := f!"{fr.file}:{fr.range}"
+
+structure File2dRange where
+  file: Uri
+  start: Lean.Position
+  ending: Lean.Position
+  deriving DecidableEq, Repr
+
+instance : ToFormat File2dRange where
+ format fr :=
+    let baseName := match fr.file with
+                    | .file path => (path.splitToList (· == '/')).getLast!
+    f!"{baseName}({fr.start.line}, {fr.start.column})-({fr.ending.line}, {fr.ending.column})"
+
 abbrev Arg := ArgF SourceRange
 abbrev Expr := ExprF SourceRange
 abbrev Operation := OperationF SourceRange
diff --git a/Strata/DDM/Ion.lean b/Strata/DDM/Ion.lean
index 1f84e6b43..f86a04c7d 100644
--- a/Strata/DDM/Ion.lean
+++ b/Strata/DDM/Ion.lean
@@ -183,7 +183,7 @@ private protected def asList (v : Ion SymbolId) : FromIonM { a : Array (Ion Symb
   match v with
   | .mk (.list args) =>
     return .mk args (by simp; omega)
-  | _ => throw s!"Expected list"
+  | x => throw s!"Expected list"
 
 private protected def asSexp (name : String) (v : Ion SymbolId) : FromIonM ({ a : Array (Ion SymbolId) // a.size > 0 ∧ sizeOf a < sizeOf v}) :=
   match v with
@@ -284,7 +284,7 @@ private def deserializeValue {α} (bs : ByteArray) (act : Ion SymbolId → FromI
       throw s!"Error reading Ion: {msg} (offset = {off})"
     | .ok a => pure a
   let .isTrue p := inferInstanceAs (Decidable (a.size = 1))
-    | throw s!"Expected single Ion value."
+    | throw s!"Expected single Ion value, but got {repr a}."
   let entries := a[0]
   let .isTrue p := inferInstanceAs (Decidable (entries.size = 2))
     | throw s!"Expected symbol table and value in dialect."
@@ -1405,6 +1405,11 @@ private instance : FromIon Dialect where
 
 end Dialect
 
+structure StrataFile where
+  filePath : String
+  program : Program
+  deriving Inhabited
+
 namespace Program
 
 private instance : CachedToIon Program where
@@ -1430,7 +1435,7 @@ def fromIonFragment (f : Ion.Fragment)
     commands := ← fromIonFragmentCommands f
   }
 
-def fromIon (dialects : DialectMap) (dialect : DialectName) (bytes : ByteArray) : Except String Strata.Program := do
+def fileFromIon (dialects : DialectMap) (dialect : DialectName) (bytes : ByteArray) : Except String Strata.Program := do
   let (hdr, frag) ←
     match Strata.Ion.Header.parse bytes with
     | .error msg =>
@@ -1445,5 +1450,60 @@ def fromIon (dialects : DialectMap) (dialect : DialectName) (bytes : ByteArray)
       throw s!"{name} program found when {dialect} expected."
     fromIonFragment frag dialects dialect
 
+def filesFromIon (dialects : DialectMap) (bytes : ByteArray) : Except String (List StrataFile) := do
+  let ctx ←
+    match Ion.deserialize bytes with
+    | .error (off, msg) => throw s!"Error reading Ion: {msg} (offset = {off})"
+    | .ok a =>
+      if p : a.size = 1 then
+        pure a[0]
+      else
+        throw s!"Expected single Ion value"
+
+  let .isTrue p := inferInstanceAs (Decidable (ctx.size = 2))
+    | throw "Expected symbol table and value"
+
+  let symbols ←
+    match SymbolTable.ofLocalSymbolTable ctx[0] with
+    | .error (p, msg) => throw s!"Error at {p}: {msg}"
+    | .ok symbols => pure symbols
+
+  let ionCtx : FromIonContext := ⟨symbols⟩
+
+  let ⟨filesList, _⟩ ← FromIonM.asList ctx[1]! ionCtx
+
+  let tbl := symbols
+  let filePathId := tbl.symbolId! "filePath"
+  let programId := tbl.symbolId! "program"
+
+  filesList.toList.mapM fun fileEntry => do
+    let fields ← FromIonM.asStruct0 fileEntry ionCtx
+
+    let some (_, filePathData) := fields.find? (·.fst == filePathId)
+      | throw "Could not find 'filePath' field"
+
+    let some (_, programData) := fields.find? (·.fst == programId)
+      | throw "Could not find 'program' field"
+
+    let filePath ← FromIonM.asString "filePath" filePathData ionCtx
+
+    let ⟨programValues, _⟩ ← FromIonM.asList programData ionCtx
+    let .isTrue ne := inferInstanceAs (Decidable (programValues.size ≥ 1))
+      | throw "Expected program header"
+
+    let hdr ← Ion.Header.fromIon programValues[0] ionCtx
+    let dialect ← match hdr with
+      | .program name => pure name
+      | .dialect _ => throw "Expected program, not dialect"
+
+    let frag : Ion.Fragment := {
+      symbols := symbols,
+      values := programValues,
+      offset := 1
+    }
+
+    let program ← fromIonFragment frag dialects dialect
+
+    pure { filePath := filePath, program := program }
+
 end Strata.Program
-end
diff --git a/Strata/DL/Imperative/MetaData.lean b/Strata/DL/Imperative/MetaData.lean
index 3364a5fa8..987008a0e 100644
--- a/Strata/DL/Imperative/MetaData.lean
+++ b/Strata/DL/Imperative/MetaData.lean
@@ -6,6 +6,7 @@
 
 import Strata.DL.Imperative.PureExpr
 import Strata.DL.Util.DecidableEq
+import Strata.DDM.AST
 import Lean.Data.Position
 
 namespace Imperative
@@ -65,22 +66,6 @@ instance [Repr P.Ident] : Repr (MetaDataElem.Field P) where
       | .label s => f!"MetaDataElem.Field.label {s}"
     Repr.addAppParen res prec
 
-inductive Uri where
-  | file (path: String)
-  deriving DecidableEq, Repr
-
-instance : ToFormat Uri where
- format fr := match fr with | .file path => path
-
-structure FileRange where
-  file: Uri
-  start: Lean.Position
-  ending: Lean.Position
-  deriving DecidableEq, Repr
-
-instance : ToFormat FileRange where
- format fr := f!"{fr.file}:{fr.start}-{fr.ending}"
-
 /-- A metadata value, which can be either an expression, a message, or a fileRange -/
 inductive MetaDataElem.Value (P : PureExpr) where
   /-- Metadata value in the form of a structured expression. -/
@@ -88,11 +73,12 @@ inductive MetaDataElem.Value (P : PureExpr) where
   /-- Metadata value in the form of an arbitrary string. -/
   | msg (s : String)
   /-- Metadata value in the form of a fileRange. -/
-  | fileRange (r: FileRange)
-
+  | fileRange (r: Strata.FileRange)
+  /-- Metadata value in the form of a fileRange. -/
+  | file2dRange (r: Strata.File2dRange)
 
 instance [ToFormat P.Expr] : ToFormat (MetaDataElem.Value P) where
-  format f := match f with | .expr e => f!"{e}" | .msg s => f!"{s}" | .fileRange r => f!"{r}"
+  format f := match f with | .expr e => f!"{e}" | .msg s => f!"{s}" | .fileRange r => f!"{r}" | .file2dRange r => f!"{r}"
 
 instance [Repr P.Expr] : Repr (MetaDataElem.Value P) where
   reprPrec v prec :=
@@ -100,7 +86,8 @@ instance [Repr P.Expr] : Repr (MetaDataElem.Value P) where
       match v with
       | .expr e => f!"MetaDataElem.Value.expr {reprPrec e prec}"
       | .msg s => f!"MetaDataElem.Value.msg {s}"
-      | .fileRange fr => f!"MetaDataElem.Value.fileRange {repr fr}"
+      | .fileRange fr => f!"MetaDataElem.Value.fileRange {fr}"
+      | .file2dRange fr => f!"MetaDataElem.Value.file2dRange {fr}"
     Repr.addAppParen res prec
 
 def MetaDataElem.Value.beq [BEq P.Expr] (v1 v2 : MetaDataElem.Value P) :=
@@ -108,6 +95,7 @@ def MetaDataElem.Value.beq [BEq P.Expr] (v1 v2 : MetaDataElem.Value P) :=
   | .expr e1, .expr e2 => e1 == e2
   | .msg m1, .msg m2 => m1 == m2
   | .fileRange r1, .fileRange r2 => r1 == r2
+  | .file2dRange r1, .file2dRange r2 => r1 == r2
   | _, _ => false
 
 instance [BEq P.Expr] : BEq (MetaDataElem.Value P) where
@@ -183,11 +171,18 @@ instance [Repr P.Expr] [Repr P.Ident] : Repr (MetaDataElem P) where
 
 def MetaData.fileRange : MetaDataElem.Field P := .label "fileRange"
 
+def getFileRange {P : PureExpr} [BEq P.Ident] (md: MetaData P) : Option Strata.FileRange := do
+  let fileRangeElement <- md.findElem Imperative.MetaData.fileRange
+  match fileRangeElement.value with
+    | .fileRange fileRange =>
+      some fileRange
+    | _ => none
+
 def MetaData.formatFileRange? {P} [BEq P.Ident] (md : MetaData P) (includeEnd? : Bool := false) :
     Option Std.Format := do
   let fileRangeElem ← md.findElem MetaData.fileRange
   match fileRangeElem.value with
-  | .fileRange m =>
+  | .file2dRange m =>
     let baseName := match m.file with
                     | .file path => (path.splitToList (· == '/')).getLast!
     if includeEnd? then
diff --git a/Strata/DL/Imperative/SMTUtils.lean b/Strata/DL/Imperative/SMTUtils.lean
index 832238382..8373de3ab 100644
--- a/Strata/DL/Imperative/SMTUtils.lean
+++ b/Strata/DL/Imperative/SMTUtils.lean
@@ -115,7 +115,7 @@ def processModel {P : PureExpr} [ToFormat P.Ident]
     | none => .error f!"Cannot find model for id: {id}"
     | some p => .ok p.value
 
-def runSolver (solver : String) (args : Array String) : IO String := do
+def runSolver (solver : String) (args : Array String) : IO IO.Process.Output := do
   let output ← IO.Process.output {
     cmd := solver
     args := args
@@ -123,15 +123,16 @@ def runSolver (solver : String) (args : Array String) : IO String := do
   -- dbg_trace f!"runSolver: exitcode: {repr output.exitCode}\n\
   --                         stderr: {repr output.stderr}\n\
   --                         stdout: {repr output.stdout}"
-  return output.stdout
+  return output
 
 def solverResult {P : PureExpr} [ToFormat P.Ident]
     (typedVarToSMTFn : P.Ident → P.Ty → Except Format (String × Strata.SMT.TermType))
-    (vars : List P.TypedIdent) (ans : String)
+    (vars : List P.TypedIdent) (output : IO.Process.Output)
     (E : Strata.SMT.EncoderState) : Except Format (Result P.TypedIdent) := do
-  let pos := (ans.find (fun c => c == '\n' || c == '\r')).byteIdx
-  let verdict := ans.take pos
-  let rest := ans.drop pos
+  let stdout := output.stdout
+  let pos := (stdout.find (fun c => c == '\n' || c == '\r')).byteIdx
+  let verdict := stdout.take pos
+  let rest := stdout.drop pos
   match verdict with
   | "sat"     =>
     let rawModel ← getModel rest
@@ -139,7 +140,7 @@ def solverResult {P : PureExpr} [ToFormat P.Ident]
     .ok (.sat model)
   | "unsat"   =>  .ok .unsat
   | "unknown" =>  .ok .unknown
-  | other     =>  .error other
+  | _     =>  .error s!"stderr:{output.stderr}\nsolver stdout: {output.stdout}\n"
 
 def VC_folder_name: String := "vcs"
 
@@ -169,8 +170,8 @@ def dischargeObligation {P : PureExpr} [ToFormat P.Ident]
       .ok "--produce-models"
     else
       return .error f!"Unsupported SMT solver: {smtsolver}"
-  let solver_out ← runSolver smtsolver #[filename, produce_models]
-  match solverResult typedVarToSMTFn vars solver_out estate with
+  let solver_output ← runSolver smtsolver #[filename, produce_models]
+  match solverResult typedVarToSMTFn vars solver_output estate with
   | .error e => return .error e
   | .ok result => return .ok (result, estate)
 
diff --git a/Strata/Languages/Boogie/DDMTransform/Translate.lean b/Strata/Languages/Boogie/DDMTransform/Translate.lean
index 133aa433a..21a32c258 100644
--- a/Strata/Languages/Boogie/DDMTransform/Translate.lean
+++ b/Strata/Languages/Boogie/DDMTransform/Translate.lean
@@ -50,7 +50,7 @@ def SourceRange.toMetaData (ictx : InputContext) (sr : SourceRange) : Imperative
   let startPos := ictx.fileMap.toPosition sr.start
   let endPos := ictx.fileMap.toPosition sr.stop
   let uri: Uri := .file file
-  let fileRangeElt := ⟨ MetaData.fileRange, .fileRange ⟨ uri, startPos, endPos ⟩ ⟩
+  let fileRangeElt := ⟨ MetaData.fileRange, .file2dRange ⟨ uri, startPos, endPos ⟩ ⟩
   #[fileRangeElt]
 
 def getOpMetaData (op : Operation) : TransM (Imperative.MetaData Boogie.Expression) :=
diff --git a/Strata/Languages/Boogie/Verifier.lean b/Strata/Languages/Boogie/Verifier.lean
index aeb9f88f7..b2ead526d 100644
--- a/Strata/Languages/Boogie/Verifier.lean
+++ b/Strata/Languages/Boogie/Verifier.lean
@@ -11,12 +11,14 @@ import Strata.Languages.Boogie.SMTEncoder
 import Strata.DL.Imperative.MetaData
 import Strata.DL.Imperative.SMTUtils
 import Strata.DL.SMT.CexParser
+import Strata.DDM.AST
 
 ---------------------------------------------------------------------
 
 namespace Strata.SMT.Encoder
 
 open Strata.SMT.Encoder
+open Strata
 
 -- Derived from Strata.SMT.Encoder.encode.
 def encodeBoogie (ctx : Boogie.SMT.Context) (prelude : SolverM Unit) (ts : List Term) :
@@ -123,7 +125,7 @@ def runSolver (solver : String) (args : Array String) : IO IO.Process.Output :=
   --                         stdout: {repr output.stdout}"
   return output
 
-def solverResult (vars : List (IdentT LMonoTy Visibility)) (output: IO.Process.Output)
+def solverResult (vars : List (IdentT LMonoTy Visibility)) (output : IO.Process.Output)
     (ctx : SMT.Context) (E : EncoderState) :
   Except Format Result := do
   let stdout := output.stdout
@@ -142,17 +144,25 @@ def solverResult (vars : List (IdentT LMonoTy Visibility)) (output: IO.Process.O
     | .error _model_err => (.ok (.sat []))
   | "unsat"   =>  .ok .unsat
   | "unknown" =>  .ok .unknown
-  | _     =>  .error (stdout ++ output.stderr)
+  | _     =>  .error s!"stderr:{output.stderr}\nsolver stdout: {output.stdout}\n"
 
 open Imperative
 
-def formatPositionMetaData [BEq P.Ident] [ToFormat P.Expr] (md : MetaData P): Option Format := do
+def formatPositionMetaData [BEq P.Ident] [ToFormat P.Expr]
+  (files: Map Strata.Uri Lean.FileMap)
+  (md : MetaData P): Option Format := do
   let fileRangeElem ← md.findElem MetaData.fileRange
   match fileRangeElem.value with
-  | .fileRange m =>
-    let baseName := match m.file with
+  | .fileRange fileRange =>
+    let fileMap := (files.find? fileRange.file).get!
+    let startPos := fileMap.toPosition fileRange.range.start
+    let baseName := match fileRange.file with
                     | .file path => (path.splitToList (· == '/')).getLast!
-    return f!"{baseName}({m.start.line}, {m.start.column})"
+    return f!"{baseName}({startPos.line}, {startPos.column})"
+  | .file2dRange file2dRange =>
+    let baseName := match file2dRange.file with
+                    | .file path => (path.splitToList (· == '/')).getLast!
+    return f!"{baseName}({file2dRange.start.line}, {file2dRange.ending.column})"
   | _ => none
 
 structure VCResult where
@@ -291,7 +301,7 @@ def verifySingleEnv (smtsolver : String) (pE : Program × Env) (options : Option
         -- let rand_suffix ← IO.rand 0 0xFFFFFFFF
         let ans ←
             IO.toEIO
-              (fun e => f!"{e}")
+              (fun e => f!"IO error: {e}")
               (dischargeObligation options
                 (ProofObligation.getVars obligation) smtsolver
                   (Imperative.smt2_filename obligation.label)
@@ -365,35 +375,51 @@ def verify
   else
     panic! s!"DDM Transform Error: {repr errors}"
 
-/-- A diagnostic produced by analyzing a file -/
-structure Diagnostic where
-  start : Lean.Position
-  ending : Lean.Position
+structure DiagnosticModel where
+  fileRange : Strata.FileRange
   message : String
   deriving Repr, BEq
 
-def toDiagnostic (vcr : Boogie.VCResult) : Option Diagnostic := do
-  -- Only create a diagnostic if the result is not .unsat (i.e., verification failed)
+def toDiagnosticModel (vcr : Boogie.VCResult) : Option DiagnosticModel := do
   match vcr.result with
   | .unsat => none  -- Verification succeeded, no diagnostic
   | result =>
-    -- Extract file range from metadata
     let fileRangeElem ← vcr.obligation.metadata.findElem Imperative.MetaData.fileRange
     match fileRangeElem.value with
-    | .fileRange range =>
+    | .fileRange fileRange =>
       let message := match result with
         | .sat _ => "assertion does not hold"
-        | .unknown => "assertion could not be proved"
+        | .unknown => "assertion verification result is unknown"
         | .err msg => s!"verification error: {msg}"
         | _ => "verification failed"
+
       some {
         -- Subtract headerOffset to account for program header we added
-        start := { line := range.start.line, column := range.start.column }
-        ending := { line := range.ending.line, column := range.ending.column }
+        fileRange := fileRange
         message := message
       }
     | _ => none
 
+structure Diagnostic where
+  start : Lean.Position
+  ending : Lean.Position
+  message : String
+  deriving Repr, BEq
+
+def DiagnosticModel.toDiagnostic (files: Map Strata.Uri Lean.FileMap) (dm: DiagnosticModel): Diagnostic :=
+  let fileMap := (files.find? dm.fileRange.file).get!
+  let startPos := fileMap.toPosition dm.fileRange.range.start
+  let endPos := fileMap.toPosition dm.fileRange.range.stop
+  {
+    start := { line := startPos.line, column := startPos.column }
+    ending := { line := endPos.line, column := endPos.column }
+    message := dm.message
+  }
+
+def Boogie.VCResult.toDiagnostic (files: Map Strata.Uri Lean.FileMap) (vcr : Boogie.VCResult) : Option Diagnostic := do
+  let modelOption := toDiagnosticModel vcr
+  modelOption.map (fun dm => dm.toDiagnostic files)
+
 end Strata
 
 ---------------------------------------------------------------------
diff --git a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
index dddb18df2..18000897f 100644
--- a/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
+++ b/Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean
@@ -10,36 +10,34 @@ import Strata.Languages.Laurel.Laurel
 import Strata.DL.Imperative.MetaData
 import Strata.Languages.Boogie.Expressions
 
+namespace Strata
 namespace Laurel
 
 open Std (ToFormat Format format)
-open Strata (QualifiedIdent Arg SourceRange)
+open Strata (QualifiedIdent Arg SourceRange Uri FileRange)
 open Lean.Parser (InputContext)
-open Imperative (MetaData Uri FileRange)
+open Imperative (MetaData)
 
 structure TransState where
-  inputCtx : InputContext
+  uri : Uri
+  errors : Array String
 
 abbrev TransM := StateT TransState (Except String)
 
-def TransM.run (ictx : InputContext) (m : TransM α) : Except String α :=
-  match StateT.run m { inputCtx := ictx } with
+def TransM.run (uri : Uri) (m : TransM α) : Except String α :=
+  match StateT.run m { uri := uri, errors := #[] } with
   | .ok (v, _) => .ok v
   | .error e => .error e
 
 def TransM.error (msg : String) : TransM α :=
   throw msg
 
-def SourceRange.toMetaData (ictx : InputContext) (sr : SourceRange) : Imperative.MetaData Boogie.Expression :=
-  let file := ictx.fileName
-  let startPos := ictx.fileMap.toPosition sr.start
-  let endPos := ictx.fileMap.toPosition sr.stop
-  let uri : Uri := .file file
-  let fileRangeElt := ⟨ Imperative.MetaDataElem.Field.label "fileRange", .fileRange ⟨ uri, startPos, endPos ⟩ ⟩
+def SourceRange.toMetaData (uri : Uri) (sr : SourceRange) : Imperative.MetaData Boogie.Expression :=
+  let fileRangeElt := ⟨ Imperative.MetaDataElem.Field.label "fileRange", .fileRange ⟨ uri, sr.start, sr.stop ⟩ ⟩
   #[fileRangeElt]
 
 def getArgMetaData (arg : Arg) : TransM (Imperative.MetaData Boogie.Expression) :=
-  return SourceRange.toMetaData (← get).inputCtx arg.ann
+  return SourceRange.toMetaData (← get).uri arg.ann
 
 def checkOp (op : Strata.Operation) (name : QualifiedIdent) (argc : Nat) :
   TransM Unit := do
@@ -63,13 +61,13 @@ def translateBool (arg : Arg) : TransM Bool := do
   match arg with
   | .expr (.fn _ name) =>
     match name with
-    | q`Laurel.boolTrue => return true
-    | q`Laurel.boolFalse => return false
+    | q`Init.boolTrue => return true
+    | q`Init.boolFalse => return false
     | _ => TransM.error s!"translateBool expects boolTrue or boolFalse, got {repr name}"
   | .op op =>
     match op.name with
-    | q`Laurel.boolTrue => return true
-    | q`Laurel.boolFalse => return false
+    | q`Init.boolTrue => return true
+    | q`Init.boolFalse => return false
     | _ => TransM.error s!"translateBool expects boolTrue or boolFalse, got {repr op.name}"
   | x => TransM.error s!"translateBool expects expression or operation, got {repr x}"
 
@@ -151,8 +149,7 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExpr := do
     | q`Laurel.block, #[arg0] =>
       let stmts ← translateSeqCommand arg0
       return .Block stmts none
-    | q`Laurel.boolTrue, _ => return .LiteralBool true
-    | q`Laurel.boolFalse, _ => return .LiteralBool false
+    | q`Laurel.literalBool, #[arg0] => return .LiteralBool (← translateBool arg0)
     | q`Laurel.int, #[arg0] =>
       let n ← translateNat arg0
       return .LiteralInt n
@@ -177,7 +174,8 @@ partial def translateStmtExpr (arg : Arg) : TransM StmtExpr := do
     | q`Laurel.assign, #[arg0, arg1] =>
       let target ← translateStmtExpr arg0
       let value ← translateStmtExpr arg1
-      return .Assign target value
+      let md ← getArgMetaData (.op op)
+      return .Assign target value md
     | q`Laurel.call, #[arg0, argsSeq] =>
       let callee ← translateStmtExpr arg0
       let calleeName := match callee with
diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
index 54e60016b..81cdc79a3 100644
--- a/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
+++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.lean
@@ -7,72 +7,7 @@
 -- Minimal Laurel dialect for AssertFalse example
 import Strata
 
-#dialect
-dialect Laurel;
+namespace Strata
+namespace Laurel
 
-// Types
-category LaurelType;
-op intType : LaurelType => "int";
-op boolType : LaurelType => "bool";
-
-category StmtExpr;
-
-op boolTrue() : StmtExpr => "true";
-op boolFalse() : StmtExpr => "false";
-op int(n : Num) : StmtExpr => n;
-
-// Variable declarations
-category OptionalType;
-op optionalType(varType: LaurelType): OptionalType => ":" varType;
-
-category OptionalAssignment;
-op optionalAssignment(value: StmtExpr): OptionalAssignment => ":=" value:0;
-
-op varDecl (name: Ident, varType: Option OptionalType, assignment: Option OptionalAssignment): StmtExpr
-  => @[prec(0)] "var " name varType assignment ";";
-
-// Identifiers/Variables
-op identifier (name: Ident): StmtExpr => name;
-op parenthesis (inner: StmtExpr): StmtExpr => "(" inner ")";
-
-// Assignment
-op assign (target: StmtExpr, value: StmtExpr): StmtExpr => target ":=" value ";";
-
-// Binary operators
-op add (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(60)] lhs "+" rhs;
-op eq (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs "==" rhs;
-op neq (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs "!=" rhs;
-op gt (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs ">" rhs;
-op lt (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs "<" rhs;
-op le (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs "<=" rhs;
-op ge (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs ">=" rhs;
-
-op call(callee: StmtExpr, args: CommaSepBy StmtExpr): StmtExpr => callee "(" args ")";
-
-// If-else
-category OptionalElse;
-op optionalElse(stmts : StmtExpr) : OptionalElse => "else" stmts;
-
-op ifThenElse (cond: StmtExpr, thenBranch: StmtExpr, elseBranch: Option OptionalElse): StmtExpr =>
-  @[prec(20)] "if (" cond ") " thenBranch:0 elseBranch:0;
-
-op assert (cond : StmtExpr) : StmtExpr => "assert " cond ";";
-op assume (cond : StmtExpr) : StmtExpr => "assume " cond ";";
-op return (value : StmtExpr) : StmtExpr => "return " value ";";
-op block (stmts : Seq StmtExpr) : StmtExpr => @[prec(1000)] "{" stmts "}";
-
-category Parameter;
-op parameter (name: Ident, paramType: LaurelType): Parameter => name ":" paramType;
-
-category ReturnParameters;
-op returnParameters(parameters: CommaSepBy Parameter): ReturnParameters => "returns" "(" parameters ")";
-
-category Procedure;
-op procedure (name : Ident, parameters: CommaSepBy Parameter,
-  returnParameters: Option ReturnParameters,
-  body : StmtExpr) : Procedure =>
-  "procedure " name "(" parameters ")" returnParameters body:0;
-
-op program (staticProcedures: Seq Procedure): Command => staticProcedures;
-
-#end
+#load_dialect "./LaurelGrammar.st"
diff --git a/Strata/Languages/Laurel/Grammar/LaurelGrammar.st b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
new file mode 100644
index 000000000..6efdcaeb1
--- /dev/null
+++ b/Strata/Languages/Laurel/Grammar/LaurelGrammar.st
@@ -0,0 +1,64 @@
+dialect Laurel;
+
+// Types
+category LaurelType;
+op intType : LaurelType => "int";
+op boolType : LaurelType => "bool";
+
+category StmtExpr;
+op literalBool (b: Bool): StmtExpr => b;
+op int(n : Num) : StmtExpr => n;
+
+// Variable declarations
+category OptionalType;
+op optionalType(varType: LaurelType): OptionalType => ":" varType;
+
+category OptionalAssignment;
+op optionalAssignment(value: StmtExpr): OptionalAssignment => ":=" value:0;
+
+op varDecl (name: Ident, varType: Option OptionalType, assignment: Option OptionalAssignment): StmtExpr
+  => @[prec(0)] "var " name varType assignment ";";
+
+// Identifiers/Variables
+op identifier (name: Ident): StmtExpr => name;
+op parenthesis (inner: StmtExpr): StmtExpr => "(" inner ")";
+
+// Assignment
+op assign (target: StmtExpr, value: StmtExpr): StmtExpr => target ":=" value ";";
+
+// Binary operators
+op add (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(60)] lhs "+" rhs;
+op eq (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs "==" rhs;
+op neq (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs "!=" rhs;
+op gt (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs ">" rhs;
+op lt (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs "<" rhs;
+op le (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs "<=" rhs;
+op ge (lhs: StmtExpr, rhs: StmtExpr): StmtExpr => @[prec(40)] lhs ">=" rhs;
+
+op call(callee: StmtExpr, args: CommaSepBy StmtExpr): StmtExpr => callee "(" args ")";
+
+// If-else
+category OptionalElse;
+op optionalElse(stmts : StmtExpr) : OptionalElse => "else" stmts;
+
+op ifThenElse (cond: StmtExpr, thenBranch: StmtExpr, elseBranch: Option OptionalElse): StmtExpr =>
+  @[prec(20)] "if (" cond ") " thenBranch:0 elseBranch:0;
+
+op assert (cond : StmtExpr) : StmtExpr => "assert " cond ";";
+op assume (cond : StmtExpr) : StmtExpr => "assume " cond ";";
+op return (value : StmtExpr) : StmtExpr => "return " value ";";
+op block (stmts : Seq StmtExpr) : StmtExpr => @[prec(1000)] "{" stmts "}";
+
+category Parameter;
+op parameter (name: Ident, paramType: LaurelType): Parameter => name ":" paramType;
+
+category ReturnParameters;
+op returnParameters(parameters: CommaSepBy Parameter): ReturnParameters => "returns" "(" parameters ")";
+
+category Procedure;
+op procedure (name : Ident, parameters: CommaSepBy Parameter,
+  returnParameters: Option ReturnParameters,
+  body : StmtExpr) : Procedure =>
+  "procedure " name "(" parameters ")" returnParameters body:0;
+
+op program (staticProcedures: Seq Procedure): Command => staticProcedures;
\ No newline at end of file
diff --git a/Strata/Languages/Laurel/Laurel.lean b/Strata/Languages/Laurel/Laurel.lean
index b113a13ba..0ff07151e 100644
--- a/Strata/Languages/Laurel/Laurel.lean
+++ b/Strata/Languages/Laurel/Laurel.lean
@@ -43,6 +43,7 @@ Design choices:
 - Construction of composite types is WIP. It needs a design first.
 
 -/
+namespace Strata
 namespace Laurel
 
 abbrev Identifier := String /- Potentially this could be an Int to save resources. -/
@@ -130,7 +131,7 @@ inductive StmtExpr : Type where
   | LiteralBool (value: Bool)
   | Identifier (name : Identifier)
   /- Assign is only allowed in an impure context -/
-  | Assign (target : StmtExpr) (value : StmtExpr)
+  | Assign (target : StmtExpr) (value : StmtExpr) (md : Imperative.MetaData Boogie.Expression)
   /- Used by itself for fields reads and in combination with Assign for field writes -/
   | FieldSelect (target : StmtExpr) (fieldName : Identifier)
   /- PureFieldUpdate is the only way to assign values to fields of pure types -/
diff --git a/Strata/Languages/Laurel/LaurelFormat.lean b/Strata/Languages/Laurel/LaurelFormat.lean
index 1c34062a3..5f8a3e57b 100644
--- a/Strata/Languages/Laurel/LaurelFormat.lean
+++ b/Strata/Languages/Laurel/LaurelFormat.lean
@@ -6,6 +6,7 @@
 
 import Strata.Languages.Laurel.Laurel
 
+namespace Strata
 namespace Laurel
 
 open Std (Format)
@@ -66,7 +67,7 @@ def formatStmtExpr (s:StmtExpr) : Format :=
   | .LiteralInt n => Format.text (toString n)
   | .LiteralBool b => if b then "true" else "false"
   | .Identifier name => Format.text name
-  | .Assign target value =>
+  | .Assign target value _ =>
       formatStmtExpr target ++ " := " ++ formatStmtExpr value
   | .FieldSelect target field =>
       formatStmtExpr target ++ "." ++ Format.text field
diff --git a/Strata/Languages/Laurel/LaurelToBoogieTranslator.lean b/Strata/Languages/Laurel/LaurelToBoogieTranslator.lean
index 445806ffa..2c86fb099 100644
--- a/Strata/Languages/Laurel/LaurelToBoogieTranslator.lean
+++ b/Strata/Languages/Laurel/LaurelToBoogieTranslator.lean
@@ -15,12 +15,12 @@ import Strata.DL.Imperative.Stmt
 import Strata.DL.Lambda.LExpr
 import Strata.Languages.Laurel.LaurelFormat
 
-namespace Laurel
-
 open Boogie (VCResult VCResults)
-open Strata
-
 open Boogie (intAddOp intSubOp intMulOp intDivOp intModOp intNegOp intLtOp intLeOp intGtOp intGeOp boolAndOp boolOrOp boolNotOp)
+
+namespace Strata.Laurel
+
+open Strata
 open Lambda (LMonoTy LTy LExpr)
 
 /-
@@ -75,7 +75,7 @@ def translateExpr (expr : StmtExpr) : Boogie.Expression.Expr :=
                   | some e => translateExpr e
                   | none => .const () (.intConst 0)
       .ite () bcond bthen belse
-  | .Assign _ value => translateExpr value  -- For expressions, just translate the value
+  | .Assign _ value _ => translateExpr value  -- For expressions, just translate the value
   | .StaticCall name args =>
       -- Create function call as an op application
       let ident := Boogie.BoogieIdent.glob name
@@ -115,7 +115,7 @@ def translateStmt (outputParams : List Parameter) (stmt : StmtExpr) : List Boogi
                             | .TBool => .const () (.boolConst false)
                             | _ => .const () (.intConst 0)
           [Boogie.Statement.init ident boogieType defaultExpr]
-  | .Assign target value =>
+  | .Assign target value _ =>
       match target with
       | .Identifier name =>
           let ident := Boogie.BoogieIdent.locl name
@@ -192,32 +192,45 @@ def translateProcedure (proc : Procedure) : Boogie.Procedure :=
 /--
 Translate Laurel Program to Boogie Program
 -/
-def translate (program : Program) : Boogie.Program :=
+def translate (program : Program) : Except (Array DiagnosticModel) Boogie.Program := do
   -- First, sequence all assignments (move them out of expression positions)
-  let sequencedProgram := liftExpressionAssignments program
+  let sequencedProgram ← liftExpressionAssignments program
   dbg_trace "=== Sequenced program Program ==="
   dbg_trace (toString (Std.Format.pretty (Std.ToFormat.format sequencedProgram)))
   dbg_trace "================================="
   -- Then translate to Boogie
   let procedures := sequencedProgram.staticProcedures.map translateProcedure
   let decls := procedures.map (fun p => Boogie.Decl.proc p .empty)
-  { decls := decls }
+  return { decls := decls }
 
 /--
 Verify a Laurel program using an SMT solver
 -/
 def verifyToVcResults (smtsolver : String) (program : Program)
-    (options : Options := Options.default) : IO VCResults := do
-  let boogieProgram := translate program
+    (options : Options := Options.default) : IO (Except (Array DiagnosticModel) VCResults) := do
+  let boogieProgramExcept := translate program
   -- Debug: Print the generated Boogie program
-  dbg_trace "=== Generated Boogie Program ==="
-  dbg_trace (toString (Std.Format.pretty (Std.ToFormat.format boogieProgram)))
-  dbg_trace "================================="
-  EIO.toIO (fun f => IO.Error.userError (toString f))
-      (Boogie.verify smtsolver boogieProgram options)
+  match boogieProgramExcept with
+    | .error e => return .error e
+    | .ok boogieProgram =>
+      dbg_trace "=== Generated Boogie Program ==="
+      dbg_trace (toString (Std.Format.pretty (Std.ToFormat.format boogieProgram)))
+      dbg_trace "================================="
+      let ioResult <- EIO.toIO (fun f => IO.Error.userError (toString f))
+          (Boogie.verify smtsolver boogieProgram options)
+      return .ok ioResult
+
+def verifyToDiagnostics (smtsolver : String) (files: Map Strata.Uri Lean.FileMap) (program : Program): IO (Array Diagnostic) := do
+  let results <- verifyToVcResults smtsolver program
+  match results with
+  | .error errors => return errors.map (fun dm => dm.toDiagnostic files)
+  | .ok results => return results.filterMap (fun dm => dm.toDiagnostic files)
+
 
-def verifyToDiagnostics (smtsolver : String) (program : Program): IO (Array Diagnostic)  := do
+def verifyToDiagnosticModels (smtsolver : String) (program : Program): IO (Array DiagnosticModel) := do
   let results <- verifyToVcResults smtsolver program
-  return results.filterMap toDiagnostic
+  match results with
+  | .error errors => return errors
+  | .ok results => return results.filterMap toDiagnosticModel
 
 end Laurel
diff --git a/Strata/Languages/Laurel/LiftExpressionAssignments.lean b/Strata/Languages/Laurel/LiftExpressionAssignments.lean
index 0221e4d40..00dbef228 100644
--- a/Strata/Languages/Laurel/LiftExpressionAssignments.lean
+++ b/Strata/Languages/Laurel/LiftExpressionAssignments.lean
@@ -5,7 +5,11 @@
 -/
 
 import Strata.Languages.Laurel.Laurel
+import Strata.Languages.Laurel.LaurelFormat
+import Strata.Languages.Boogie.Verifier
 
+
+namespace Strata
 namespace Laurel
 
 /-
@@ -23,7 +27,9 @@ Becomes:
 -/
 
 structure SequenceState where
+  insideCondition : Bool
   prependedStmts : List StmtExpr := []
+  diagnostics : List DiagnosticModel
   tempCounter : Nat := 0
 
 abbrev SequenceM := StateM SequenceState
@@ -31,6 +37,21 @@ abbrev SequenceM := StateM SequenceState
 def SequenceM.addPrependedStmt (stmt : StmtExpr) : SequenceM Unit :=
   modify fun s => { s with prependedStmts := stmt :: s.prependedStmts }
 
+def SequenceM.addDiagnostic (d : DiagnosticModel) : SequenceM Unit :=
+  modify fun s => { s with diagnostics := d :: s.diagnostics }
+
+def checkOutsideCondition(md: Imperative.MetaData Boogie.Expression): SequenceM Unit := do
+  let state <- get
+  if state.insideCondition then
+    let fileRange := (Imperative.getFileRange md).get!
+    SequenceM.addDiagnostic {
+        fileRange := fileRange,
+        message := "Could not lift assigment in expression that is evaluated conditionally"
+    }
+
+def SequenceM.setInsideCondition : SequenceM Unit := do
+  modify fun s => { s with insideCondition := true }
+
 def SequenceM.takePrependedStmts : SequenceM (List StmtExpr) := do
   let stmts := (← get).prependedStmts
   modify fun s => { s with prependedStmts := [] }
@@ -48,12 +69,13 @@ Returns the transformed expression with assignments replaced by variable referen
 -/
 def transformExpr (expr : StmtExpr) : SequenceM StmtExpr := do
   match expr with
-  | .Assign target value =>
+  | .Assign target value md =>
+      checkOutsideCondition md
       -- This is an assignment in expression context
       -- We need to: 1) execute the assignment, 2) capture the value in a temporary
       -- This prevents subsequent assignments to the same variable from changing the value
       let seqValue ← transformExpr value
-      let assignStmt := StmtExpr.Assign target seqValue
+      let assignStmt := StmtExpr.Assign target seqValue md
       SequenceM.addPrependedStmt assignStmt
       -- Create a temporary variable to capture the assigned value
       -- Use TInt as the type (could be refined with type inference)
@@ -69,6 +91,7 @@ def transformExpr (expr : StmtExpr) : SequenceM StmtExpr := do
 
   | .IfThenElse cond thenBranch elseBranch =>
       let seqCond ← transformExpr cond
+      SequenceM.setInsideCondition
       let seqThen ← transformExpr thenBranch
       let seqElse ← match elseBranch with
         | some e => transformExpr e >>= (pure ∘ some)
@@ -129,14 +152,19 @@ def transformStmt (stmt : StmtExpr) : SequenceM (List StmtExpr) := do
       | none =>
           return [stmt]
 
-  | .Assign target value =>
+  | .Assign target value md =>
       -- Top-level assignment (statement context)
       let seqTarget ← transformExpr target
       let seqValue ← transformExpr value
-      SequenceM.addPrependedStmt <| .Assign seqTarget seqValue
+      SequenceM.addPrependedStmt <| .Assign seqTarget seqValue md
       SequenceM.takePrependedStmts
 
   | .IfThenElse cond thenBranch elseBranch =>
+      -- Process condition (extract assignments)
+      let seqCond ← transformExpr cond
+
+      SequenceM.setInsideCondition
+
       let seqThen ← transformStmt thenBranch
       let thenBlock := .Block seqThen none
 
@@ -146,7 +174,6 @@ def transformStmt (stmt : StmtExpr) : SequenceM (List StmtExpr) := do
             pure (some (.Block se none))
         | none => pure none
 
-      let seqCond ← transformExpr cond
       SequenceM.addPrependedStmt <| .IfThenElse seqCond thenBlock seqElse
       SequenceM.takePrependedStmts
 
@@ -160,24 +187,28 @@ def transformStmt (stmt : StmtExpr) : SequenceM (List StmtExpr) := do
 
 end
 
-def transformProcedureBody (body : StmtExpr) : StmtExpr :=
-  let (seqStmts, _) := transformStmt body |>.run {}
+def transformProcedureBody (body : StmtExpr) : SequenceM StmtExpr := do
+  let seqStmts <- transformStmt body
   match seqStmts with
-  | [single] => single
-  | multiple => .Block multiple.reverse none
+  | [single] => pure single
+  | multiple => pure <| .Block multiple.reverse none
 
-def transformProcedure (proc : Procedure) : Procedure :=
+def transformProcedure (proc : Procedure) : SequenceM Procedure := do
   match proc.body with
   | .Transparent bodyExpr =>
-      let seqBody := transformProcedureBody bodyExpr
-      { proc with body := .Transparent seqBody }
-  | _ => proc  -- Opaque and Abstract bodies unchanged
+      let seqBody <- transformProcedureBody bodyExpr
+      pure { proc with body := .Transparent seqBody }
+  | _ => pure proc  -- Opaque and Abstract bodies unchanged
 
 /--
 Transform a program to lift all assignments that occur in an expression context.
 -/
-def liftExpressionAssignments (program : Program) : Program :=
-  let seqProcedures := program.staticProcedures.map transformProcedure
-  { program with staticProcedures := seqProcedures }
+def liftExpressionAssignments (program : Program) : Except (Array DiagnosticModel) Program :=
+  let (seqProcedures, afterState) := (program.staticProcedures.mapM transformProcedure).run
+    { insideCondition := false, diagnostics := [] }
+  if !afterState.diagnostics.isEmpty then
+    .error afterState.diagnostics.toArray
+  else
+    .ok { program with staticProcedures := seqProcedures }
 
 end Laurel
diff --git a/StrataMain.lean b/StrataMain.lean
index 53c5a9298..95746613c 100644
--- a/StrataMain.lean
+++ b/StrataMain.lean
@@ -13,8 +13,12 @@ import Strata.Languages.Python.Python
 import Strata.DDM.Integration.Java.Gen
 import StrataTest.Transform.ProcedureInlining
 
+import Strata.Languages.Laurel.Grammar.LaurelGrammar
+import Strata.Languages.Laurel.Grammar.ConcreteToAbstractTreeTranslator
+import Strata.Languages.Laurel.LaurelToBoogieTranslator
+
 def exitFailure {α} (message : String) : IO α := do
-  IO.eprintln (message  ++ "\n\nRun strata --help for additional help.")
+  IO.eprintln ("Exception: " ++ message  ++ "\n\nRun strata --help for additional help.")
   IO.Process.exit 1
 
 namespace Strata
@@ -173,7 +177,7 @@ def readPythonStrata (path : String) : IO Strata.Program := do
   let bytes ← Strata.Util.readBinInputSource path
   if ! bytes.startsWith Ion.binaryVersionMarker then
     exitFailure s!"pyAnalyze expected Ion file"
-  match Strata.Program.fromIon Strata.Python.Python_map Strata.Python.Python.name bytes with
+  match Strata.Program.fileFromIon Strata.Python.Python_map Strata.Python.Python.name bytes with
   | .ok p => pure p
   | .error msg => exitFailure msg
 
@@ -232,6 +236,46 @@ def javaGenCommand : Command where
     | .program _ =>
       exitFailure "Expected a dialect file, not a program file."
 
+def deserializeIonToLaurelFiles (bytes : ByteArray) : IO (List Strata.StrataFile) := do
+  match Strata.Program.filesFromIon Strata.Laurel.Laurel_map bytes with
+  | .ok files => pure files
+  | .error msg => exitFailure msg
+
+def laurelAnalyzeCommand : Command where
+  name := "laurelAnalyze"
+  args := []
+  help := "Analyze a Laurel Ion program from stdin. Write diagnostics to stdout."
+  callback := fun _ _ => do
+    -- Read bytes from stdin
+    let stdinBytes ← (← IO.getStdin).readBinToEnd
+
+    let strataFiles ← deserializeIonToLaurelFiles stdinBytes
+
+    let mut combinedProgram : Laurel.Program := {
+      staticProcedures := []
+      staticFields := []
+      types := []
+    }
+
+    for strataFile in strataFiles do
+
+      let transResult := Laurel.TransM.run (Strata.Uri.file strataFile.filePath) (Laurel.parseProgram strataFile.program)
+      match transResult with
+      | .error transErrors => exitFailure s!"Translation errors in {strataFile.filePath}: {transErrors}"
+      | .ok laurelProgram =>
+
+        combinedProgram := {
+          staticProcedures := combinedProgram.staticProcedures ++ laurelProgram.staticProcedures
+          staticFields := combinedProgram.staticFields ++ laurelProgram.staticFields
+          types := combinedProgram.types ++ laurelProgram.types
+        }
+
+    let diagnostics ← Laurel.verifyToDiagnosticModels "z3" combinedProgram
+
+    IO.println s!"==== DIAGNOSTICS ===="
+    for diag in diagnostics do
+      IO.println s!"{Std.format diag.fileRange.file}:{diag.fileRange.range.start}-{diag.fileRange.range.stop}: {diag.message}"
+
 def commandList : List Command := [
       javaGenCommand,
       checkCommand,
@@ -240,6 +284,7 @@ def commandList : List Command := [
       diffCommand,
       pyAnalyzeCommand,
       pyTranslateCommand,
+      laurelAnalyzeCommand,
     ]
 
 def commandMap : Std.HashMap String Command :=
diff --git a/StrataTest/DDM/Integration/Java/TestGen.lean b/StrataTest/DDM/Integration/Java/TestGen.lean
index 8dc4012e5..d8aa12202 100644
--- a/StrataTest/DDM/Integration/Java/TestGen.lean
+++ b/StrataTest/DDM/Integration/Java/TestGen.lean
@@ -300,7 +300,7 @@ elab "#testCompile" : command => do
 #testCompile
 
 -- Test 13: Roundtrip - verify Lean can read Java-generated Ion
--- Depends on testdata/comprehensive.ion (generated by Tools/Java/regenerate-testdata.sh)
+-- Depends on testdata/comprehensive.ion
 elab "#testRoundtrip" : command => do
   let env ← Lean.getEnv
   let state := Strata.dialectExt.getState env
@@ -308,7 +308,7 @@ elab "#testRoundtrip" : command => do
     | Lean.logError "Simple dialect not found"; return
   let dm := Strata.DialectMap.ofList! [Strata.initDialect, simple]
   let ionBytes ← IO.FS.readBinFile "StrataTest/DDM/Integration/Java/testdata/comprehensive.ion"
-  match Strata.Program.fromIon dm "Simple" ionBytes with
+  match Strata.Program.fileFromIon dm "Simple" ionBytes with
   | .error e => Lean.logError s!"Roundtrip test failed: {e}"
   | .ok prog =>
     if prog.commands.size != 1 then Lean.logError "Expected 1 command"; return
@@ -320,4 +320,58 @@ elab "#testRoundtrip" : command => do
 
 #testRoundtrip
 
+-- Test 14: Roundtrip with fromIonFiles - verify Lean can read Java-generated Ion array format
+-- Depends on testdata/comprehensive-files.ion
+elab "#testRoundtripFiles" : command => do
+  let env ← Lean.getEnv
+  let state := Strata.dialectExt.getState env
+  let some simple := state.loaded.dialects["Simple"]?
+    | Lean.logError "Simple dialect not found"; return
+  let dm := Strata.DialectMap.ofList! [Strata.initDialect, simple]
+  let ionBytes ← IO.FS.readBinFile "StrataTest/DDM/Integration/Java/testdata/comprehensive-files.ion"
+  match Strata.Program.filesFromIon dm ionBytes with
+  | .error e => Lean.logError s!"Roundtrip files test failed: {e}"
+  | .ok files =>
+    if files.length != 2 then
+      Lean.logError s!"Expected 2 files, got {files.length}"
+      return
+
+    -- Check first file
+    let file1 := files[0]!
+    if file1.filePath != "file1.st" then
+      Lean.logError s!"File 1: Expected path 'file1.st', got '{file1.filePath}'"
+      return
+    if file1.program.commands.size != 1 then
+      Lean.logError s!"File 1: Expected 1 command, got {file1.program.commands.size}"
+      return
+    let cmd1 := file1.program.commands[0]!
+    if cmd1.name != (⟨"Simple", "block"⟩ : Strata.QualifiedIdent) then
+      Lean.logError "File 1: Expected block command"; return
+    if let .seq _ stmts := cmd1.args[0]! then
+      if stmts.size != 2 then
+        Lean.logError s!"File 1: Expected 2 statements, got {stmts.size}"
+        return
+    else
+      Lean.logError "File 1: Expected seq argument"; return
+
+    -- Check second file
+    let file2 := files[1]!
+    if file2.filePath != "file2.st" then
+      Lean.logError s!"File 2: Expected path 'file2.st', got '{file2.filePath}'"
+      return
+    if file2.program.commands.size != 1 then
+      Lean.logError s!"File 2: Expected 1 command, got {file2.program.commands.size}"
+      return
+    let cmd2 := file2.program.commands[0]!
+    if cmd2.name != (⟨"Simple", "block"⟩ : Strata.QualifiedIdent) then
+      Lean.logError "File 2: Expected block command"; return
+    if let .seq _ stmts := cmd2.args[0]! then
+      if stmts.size != 3 then
+        Lean.logError s!"File 2: Expected 3 statements, got {stmts.size}"
+        return
+    else
+      Lean.logError "File 2: Expected seq argument"; return
+
+#testRoundtripFiles
+
 end Strata.Java.Test
diff --git a/StrataTest/DDM/Integration/Java/regenerate-testdata.sh b/StrataTest/DDM/Integration/Java/regenerate-testdata.sh
index d4acc3130..7163658da 100755
--- a/StrataTest/DDM/Integration/Java/regenerate-testdata.sh
+++ b/StrataTest/DDM/Integration/Java/regenerate-testdata.sh
@@ -21,7 +21,7 @@ echo "=== Compiling Java ==="
 javac -cp "$JAR" $GEN_DIR/com/strata/simple/*.java $TESTDATA/GenerateTestData.java
 
 echo "=== Generating test data ==="
-java -cp "$JAR:$GEN_DIR:$TESTDATA" GenerateTestData "$TESTDATA/comprehensive.ion"
+java -cp "$JAR:$GEN_DIR:$TESTDATA" GenerateTestData "$TESTDATA/comprehensive.ion" "$TESTDATA/comprehensive-files.ion"
 
 echo "=== Cleaning up ==="
 rm -rf "$GEN_DIR"
@@ -31,4 +31,4 @@ echo "=== Verifying with Lean ==="
 (cd "$STRATA_ROOT" && lake exe strata print --include "$STRATA_ROOT/StrataTest/DDM/Integration/Java/$TESTDATA" "$STRATA_ROOT/StrataTest/DDM/Integration/Java/$TESTDATA/comprehensive.ion" 2>&1 | tail -1)
 
 echo ""
-echo "Done! Regenerated $TESTDATA/comprehensive.ion"
+echo "Done! Regenerated $TESTDATA/comprehensive.ion and $TESTDATA/comprehensive-files.ion"
diff --git a/StrataTest/DDM/Integration/Java/testdata/GenerateTestData.java b/StrataTest/DDM/Integration/Java/testdata/GenerateTestData.java
index e451b183e..395ac4c74 100644
--- a/StrataTest/DDM/Integration/Java/testdata/GenerateTestData.java
+++ b/StrataTest/DDM/Integration/Java/testdata/GenerateTestData.java
@@ -10,6 +10,14 @@ public class GenerateTestData {
     public static void main(String[] args) throws Exception {
         var ion = IonSystemBuilder.standard().build();
         var serializer = new IonSerializer(ion);
+        generateSingleProgram(ion, serializer, args[0]);
+
+        if (args.length > 1) {
+            generateMultipleFiles(ion, serializer, args[1]);
+        }
+    }
+
+    private static void generateSingleProgram(IonSystem ion, IonSerializer serializer, String outPath) throws Exception {
         
         // AST covering: Num, Str, Ident, Bool, Decimal, ByteArray, Option, Seq, nesting
         Node ast = block(List.of(
@@ -25,11 +33,55 @@ public static void main(String[] args) throws Exception {
         program.add(header);
         program.add(serializer.serializeCommand(ast));
         
-        try (var out = new FileOutputStream(args[0])) {
+        try (var out = new FileOutputStream(outPath)) {
             var writer = IonBinaryWriterBuilder.standard().build(out);
             program.writeTo(writer);
             writer.close();
         }
-        System.out.println("Generated: " + args[0]);
+        System.out.println("Generated: " + outPath);
+    }
+
+    private static void generateMultipleFiles(IonSystem ion, IonSerializer serializer, String outPath) throws Exception {
+        Node ast1 = block(List.of(
+            assign("x", num(42)),
+            print("first file")));
+
+        IonList program1 = ion.newEmptyList();
+        IonSexp header1 = ion.newEmptySexp();
+        header1.add(ion.newSymbol("program"));
+        header1.add(ion.newString("Simple"));
+        program1.add(header1);
+        program1.add(serializer.serializeCommand(ast1));
+
+        Node ast2 = block(List.of(
+            assign("y", add(num(1), num(2))),
+            print("second file"),
+            ifStmt(true, block(List.of()), Optional.empty())));
+
+        IonList program2 = ion.newEmptyList();
+        IonSexp header2 = ion.newEmptySexp();
+        header2.add(ion.newSymbol("program"));
+        header2.add(ion.newString("Simple"));
+        program2.add(header2);
+        program2.add(serializer.serializeCommand(ast2));
+
+        IonList files = ion.newEmptyList();
+
+        IonStruct file1 = ion.newEmptyStruct();
+        file1.put("filePath", ion.newString("file1.st"));
+        file1.put("program", program1);
+        files.add(file1);
+
+        IonStruct file2 = ion.newEmptyStruct();
+        file2.put("filePath", ion.newString("file2.st"));
+        file2.put("program", program2);
+        files.add(file2);
+
+        try (var out = new FileOutputStream(outPath)) {
+            var writer = IonBinaryWriterBuilder.standard().build(out);
+            files.writeTo(writer);
+            writer.close();
+        }
+        System.out.println("Generated: " + outPath);
     }
 }
diff --git a/StrataTest/DDM/Integration/Java/testdata/comprehensive-files.ion b/StrataTest/DDM/Integration/Java/testdata/comprehensive-files.ion
new file mode 100644
index 000000000..9361a13ce
Binary files /dev/null and b/StrataTest/DDM/Integration/Java/testdata/comprehensive-files.ion differ
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T1_AssertFalse.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T1_AssertFalse.lean
index 03a18be68..79f93745f 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T1_AssertFalse.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T1_AssertFalse.lean
@@ -8,8 +8,8 @@ import StrataTest.Util.TestDiagnostics
 import StrataTest.Languages.Laurel.TestExamples
 
 open StrataTest.Util
-open Strata
 
+namespace Strata
 namespace Laurel
 
 def program := r"
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
index 04d658343..59be97e3b 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressions.lean
@@ -10,20 +10,16 @@ import StrataTest.Languages.Laurel.TestExamples
 open StrataTest.Util
 open Strata
 
-namespace Laurel
+namespace Strata.Laurel
 
 def program: String := r"
-procedure nestedImpureStatements(x: int) {
+procedure NestedImpureStatements() {
   var y := 0;
-  if (y := y + 1; == { y := y + 1; x }) {
-    assert x == 1;
-    assert y == x + 1;
-  } else {
-    assert x != 1;
-  }
-  assert y == 2;
-    assert false;
-//  ^^^^^^^^^^^^^ error: assertion does not hold
+  var x := y;
+  var z := y := y + 1;;
+    assert x == y;
+//  ^^^^^^^^^^^^^^ error: assertion does not hold
+  assert z == y;
 }
 "
 
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsNotSupported.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsNotSupported.lean
new file mode 100644
index 000000000..cb3ad8d2c
--- /dev/null
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T2_ImpureExpressionsNotSupported.lean
@@ -0,0 +1,32 @@
+/-
+  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: String := r"
+procedure conditionalAssignmentInExpression(x: int) {
+  var y := 0;
+  var z := if (x > 0) { y := y + 1; } else { 0 };
+//                      ^^^^^^^^^^^ error: Could not lift assigment in expression that is evaluated conditionally
+  if (x > 0) {
+    assert y == 1;
+  } else {
+    assert z == 0;
+    assert y == 0;
+  }
+}
+"
+
+#eval! testInputWithOffset "T2_ImpureExpressionsNotSupported" program 14 processLaurelFile
+
+
+end Laurel
diff --git a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean
index f0467c36b..27decdde1 100644
--- a/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean
+++ b/StrataTest/Languages/Laurel/Examples/Fundamentals/T3_ControlFlow.lean
@@ -10,6 +10,7 @@ import StrataTest.Languages.Laurel.TestExamples
 open StrataTest.Util
 open Strata
 
+namespace Strata
 namespace Laurel
 
 def program := r"
diff --git a/StrataTest/Languages/Laurel/TestExamples.lean b/StrataTest/Languages/Laurel/TestExamples.lean
index 473eacb03..1b5c61586 100644
--- a/StrataTest/Languages/Laurel/TestExamples.lean
+++ b/StrataTest/Languages/Laurel/TestExamples.lean
@@ -17,20 +17,20 @@ open Strata
 open Strata.Elab (parseStrataProgramFromDialect)
 open Lean.Parser (InputContext)
 
-namespace Laurel
+namespace Strata.Laurel
 
 def processLaurelFile (input : InputContext) : IO (Array Diagnostic) := do
   let dialects := Strata.Elab.LoadedDialects.ofDialects! #[initDialect, Laurel]
   let strataProgram ← parseStrataProgramFromDialect dialects Laurel.name input
 
-  -- Convert to Laurel.Program using parseProgram (handles unwrapping the program operation)
-  let laurelProgram ← match Laurel.TransM.run input (Laurel.parseProgram strataProgram) with
-    | .ok program => pure program
-    | .error errMsg => throw (IO.userError s!"Translation error: {errMsg}")
+  let uri := Strata.Uri.file input.fileName
+  let transResult := Laurel.TransM.run uri (Laurel.parseProgram strataProgram)
+  match transResult with
+  | .error transErrors => throw (IO.userError s!"Translation errors: {transErrors}")
+  | .ok laurelProgram =>
+    let files := Map.insert Map.empty uri input.fileMap
+    let diagnostics ← Laurel.verifyToDiagnostics "z3" files laurelProgram
 
-  -- Verify the program
-  let diagnostics ← Laurel.verifyToDiagnostics "z3" laurelProgram
-
-  pure diagnostics
+    pure diagnostics
 
 end Laurel