diff --git a/Strata/Languages/Python/BoogiePrelude.lean b/Strata/Languages/Python/BoogiePrelude.lean
index ff4229c4e..7eb7cd3dc 100644
--- a/Strata/Languages/Python/BoogiePrelude.lean
+++ b/Strata/Languages/Python/BoogiePrelude.lean
@@ -190,14 +190,13 @@ procedure timedelta(days: IntOrNone, hours: IntOrNone) returns (delta : int, may
 spec{
 }
 {
-  havoc delta;
   var days_i : int := 0;
   if (IntOrNone..isIntOrNone_mk_int(days)) {
         days_i := IntOrNone_int_val(days);
   }
   var hours_i : int := 0;
   if (IntOrNone..isIntOrNone_mk_int(hours)) {
-        days_i := IntOrNone_int_val(hours);
+        hours_i := IntOrNone_int_val(hours);
   }
   assume [assume_timedelta_sign_matches]: (delta == (((days_i * 24) + hours_i) * 3600) * 1000000);
 };
@@ -244,7 +243,6 @@ spec {
   ensures (Datetime_get_timedelta(d) == Timedelta_mk(0,0,0));
 }
 {
-  havoc d;
   assume [assume_datetime_now]: (Datetime_get_timedelta(d) == Timedelta_mk(0,0,0));
 };
 
@@ -253,7 +251,6 @@ spec {
   ensures (Datetime_get_timedelta(d) == Timedelta_mk(0,0,0));
 }
 {
-  havoc d;
   assume [assume_datetime_now]: (Datetime_get_timedelta(d) == Timedelta_mk(0,0,0));
 };
 
@@ -282,8 +279,7 @@ axiom [Datetime_lt_ax]:
 
 type Date;
 procedure datetime_date(dt: Datetime) returns (d : Datetime, maybe_except: ExceptOrNone)
-spec{}
-{havoc d;};
+spec{};
 
 function datetime_to_str(dt : Datetime) : string;
 
@@ -295,7 +291,6 @@ spec{
   ensures [ensures_str_strp_reverse]: (forall dt : Datetime :: {d == dt} ((time == datetime_to_str(dt)) <==> (d == dt)));
 }
 {
-  havoc d;
   assume [assume_str_strp_reverse]: (forall dt : Datetime :: {d == dt} ((time == datetime_to_str(dt)) <==> (d == dt)));
 };
 
@@ -310,24 +305,16 @@ procedure import(names : ListStr) returns ();
 procedure print(msg : string, opt : StrOrNone) returns ();
 
 procedure json_dumps(msg : DictStrAny, opt_indent : IntOrNone) returns (s: string, maybe_except: ExceptOrNone)
-spec{}
-{havoc s;}
-;
+spec{};
 
 procedure json_loads(msg : string) returns (d: DictStrAny, maybe_except: ExceptOrNone)
-spec{}
-{havoc d;}
-;
+spec{};
 
 procedure input(msg : string) returns (result: string, maybe_except: ExceptOrNone)
-spec{}
-{havoc result;}
-;
+spec{};
 
 procedure random_choice(l : ListStr) returns (result: string, maybe_except: ExceptOrNone)
-spec{}
-{havoc result;}
-;
+spec{};
 
 function str_in_list_str(s : string, l: ListStr) : bool;
 
diff --git a/Strata/Transform/BoogieTransform.lean b/Strata/Transform/BoogieTransform.lean
index ad5584f3d..eeb313356 100644
--- a/Strata/Transform/BoogieTransform.lean
+++ b/Strata/Transform/BoogieTransform.lean
@@ -187,20 +187,51 @@ def createOldVarsSubst
     | ((v', _), v) => (v, createFvar v')
 
 
-
 /- Generic runner functions -/
 
-def runStmts (f : Statement → Program → BoogieTransformM (List Statement))
+-- Only visit top-level statements and run f
+def runStmts (f : Command → Program → BoogieTransformM (List Statement))
     (ss : List Statement) (inputProg : Program)
     : BoogieTransformM (List Statement) := do
   match ss with
   | [] => return []
   | s :: ss =>
-    let s' := (f s inputProg)
+    let s' := match s with
+      | .cmd c => f c inputProg
+      | s => return [s]
     let ss' := (runStmts f ss inputProg)
     return (← s') ++ (← ss')
 
-def runProcedures (f : Statement → Program → BoogieTransformM (List Statement))
+-- Recursively visit all blocks and run f
+def runStmtsRec (f : Command → Program → BoogieTransformM (List Statement))
+    (ss : List Statement) (inputProg : Program)
+    : BoogieTransformM (List Statement) := do
+  match ss with
+  | [] => return []
+  | s :: ss' =>
+    let ss'' ← (runStmtsRec f ss' inputProg)
+    let sres ← (match s with
+      | .cmd c => do
+        let res ← f c inputProg
+        return res
+      | .block lbl b md => do
+        let b' ← runStmtsRec f b inputProg
+        return [.block lbl b' md]
+      | .ite c thenb elseb md => do
+        let thenb' ← runStmtsRec f thenb inputProg
+        let elseb' ← runStmtsRec f elseb inputProg
+        return [.ite c thenb' elseb' md]
+      | .loop guard measure invariant body md => do
+        let body' ← runStmtsRec f body inputProg
+        return [.loop guard measure invariant body' md]
+      | .goto _lbl _md =>
+        return [s])
+    return (sres ++ ss'')
+termination_by sizeOf ss
+decreasing_by
+  all_goals (unfold Imperative.instSizeOfBlock; decreasing_tactic)
+
+def runProcedures (f : Command → Program → BoogieTransformM (List Statement))
     (dcls : List Decl) (inputProg : Program)
     : BoogieTransformM (List Decl) := do
   match dcls with
@@ -208,11 +239,12 @@ def runProcedures (f : Statement → Program → BoogieTransformM (List Statemen
   | d :: ds =>
     match d with
     | .proc p md =>
-      return Decl.proc { p with body := ← (runStmts f p.body inputProg ) } md ::
-        (← (runProcedures f ds inputProg))
+      return Decl.proc {
+          p with body := ← (runStmtsRec f p.body inputProg)
+        } md :: (← (runProcedures f ds inputProg))
     | _ => return d :: (← (runProcedures f ds inputProg))
 
-def runProgram (f : Statement → Program → BoogieTransformM (List Statement))
+def runProgram (f : Command → Program → BoogieTransformM (List Statement))
     (p : Program) : BoogieTransformM Program := do
   let newDecls ← runProcedures f p.decls p
   return { decls := newDecls }
diff --git a/Strata/Transform/CallElim.lean b/Strata/Transform/CallElim.lean
index cb1f4e8f1..96748474f 100644
--- a/Strata/Transform/CallElim.lean
+++ b/Strata/Transform/CallElim.lean
@@ -14,12 +14,12 @@ namespace CallElim
 open Boogie.Transform
 
 /--
-The main call elimination transformation algorithm on a single statement.
+The main call elimination transformation algorithm on a single command.
 The returned result is a sequence of statements
 -/
-def callElimStmt (st: Statement) (p : Program)
+def callElimCmd (cmd: Command) (p : Program)
   : BoogieTransformM (List Statement) := do
-    match st with
+    match cmd with
       | .call lhs procName args _ =>
 
         let some proc := Program.Procedure.find? p procName | throw s!"Procedure {procName} not found in program"
@@ -83,18 +83,19 @@ def callElimStmt (st: Statement) (p : Program)
                         (arg_subst ++ ret_subst)
 
         return argInit ++ outInit ++ oldInit ++ asserts ++ havocs ++ assumes
-      | _ => return [ st ]
+      | _ => return [ .cmd cmd ]
 
+-- Visits top-level statements and do call elimination
 def callElimStmts (ss: List Statement) (prog : Program) :=
-  runStmts callElimStmt ss prog
+  runStmts callElimCmd ss prog
 
 def callElimL (dcls : List Decl) (prog : Program) :=
-  runProcedures callElimStmt dcls prog
+  runProcedures callElimCmd dcls prog
 
 /-- Call Elimination for an entire program by walking through all procedure
 bodies -/
 def callElim' (p : Program) : BoogieTransformM Program :=
-  runProgram callElimStmt p
+  runProgram callElimCmd p
 
 end CallElim
 end Boogie
diff --git a/Strata/Transform/CallElimCorrect.lean b/Strata/Transform/CallElimCorrect.lean
index 351be77fb..c09748d9c 100644
--- a/Strata/Transform/CallElimCorrect.lean
+++ b/Strata/Transform/CallElimCorrect.lean
@@ -173,7 +173,7 @@ theorem callElimBlockNoExcept :
   -- ∧ WF.WFStatementsProp p sts
   := by
   intros st p wf
-  simp [Transform.run, runStmts, CallElim.callElimStmts, CallElim.callElimStmt]
+  simp [Transform.run, runStmts, CallElim.callElimStmts, CallElim.callElimCmd]
   cases st with
   | block l b md => exists [.block l b md]
   | ite cd tb eb md => exists [.ite cd tb eb md]
@@ -188,6 +188,7 @@ theorem callElimBlockNoExcept :
       next heq =>
       cases heq
       next st =>
+      simp only [] -- reduce match
       split <;>
         simp only [StateT.run, bind, ExceptT.bind, ExceptT.mk, StateT.bind, genArgExprIdentsTrip, ne_eq, liftM,
               monadLift, MonadLift.monadLift, ExceptT.lift, Functor.map, List.unzip_snd, ite_not, ExceptT.bindCont, ExceptT.map,
@@ -272,10 +273,7 @@ theorem callElimBlockNoExcept :
         unfold BoogieIdent.unres at *
         split at wf <;> simp_all
     . -- other case
-      exfalso
-      next st Hfalse =>
-      specialize Hfalse lhs procName args md
-      simp_all
+      grind
 
 theorem postconditions_subst_unwrap :
   substPost ∈
@@ -3291,7 +3289,7 @@ theorem callElimStatementCorrect [LawfulBEq Expression.Expr] :
     := by
   intros Hp Hgv Heval Hwfc Hwf Hwfp Hwfgen Hwfgenst Helim
   cases st <;>
-  simp [Transform.runWith, StateT.run, callElimStmts, runStmts, callElimStmt,
+  simp [Transform.runWith, StateT.run, callElimStmts, runStmts, callElimCmd,
         pure, ExceptT.pure, ExceptT.mk, StateT.pure,
         bind, ExceptT.bind, ExceptT.bindCont, StateT.bind,
         ] at Helim
diff --git a/Strata/Transform/ProcedureInlining.lean b/Strata/Transform/ProcedureInlining.lean
index 5ef92babe..2d49b53fe 100644
--- a/Strata/Transform/ProcedureInlining.lean
+++ b/Strata/Transform/ProcedureInlining.lean
@@ -191,12 +191,15 @@ This function does not update the specification because inlineCallStmt will not
 use the specification. This will have to change if Strata also wants to support
 the reachability query.
 -/
-def inlineCallStmt (st: Statement) (p : Program)
+def inlineCallCmd (excluded_calls:List String := [])
+                  (cmd: Command) (p : Program)
   : BoogieTransformM (List Statement) :=
     open Lambda in do
-    match st with
+    match cmd with
       | .call lhs procName args _ =>
 
+        if procName ∈ excluded_calls then return [.cmd cmd] else
+
         let some proc := Program.Procedure.find? p procName
           | throw s!"Procedure {procName} not found in program"
 
@@ -223,12 +226,14 @@ def inlineCallStmt (st: Statement) (p : Program)
 
         -- Create a fresh var statement for each LHS
         let outputTrips ← genOutExprIdentsTrip sigOutputs sigOutputs.unzip.fst
-        let outputInit := createInitVars
+        let outputInits := createInitVars
           (outputTrips.map (fun ((tmpvar,ty),orgvar) => ((orgvar,ty),tmpvar)))
+        let outputHavocs := outputTrips.map (fun
+          (_,orgvar) => Statement.havoc orgvar)
         -- Create a var statement for each procedure input arguments.
         -- The input parameter expression is assigned to these new vars.
         --let inputTrips ← genArgExprIdentsTrip sigInputs args
-        let inputInit := createInits (sigInputs.zip args)
+        let inputInits := createInits (sigInputs.zip args)
         -- Assign the output variables in the signature to the actual output
         -- variables used in the callee.
         let outputSetStmts :=
@@ -243,29 +248,20 @@ def inlineCallStmt (st: Statement) (p : Program)
             outs_lhs_and_sig
 
         let stmts:List (Imperative.Stmt Boogie.Expression Boogie.Command)
-          := inputInit ++ outputInit ++ proc.body ++ outputSetStmts
+          := inputInits ++ outputInits ++ outputHavocs ++ proc.body ++
+             outputSetStmts
 
         return [.block (procName ++ "$inlined") stmts]
-      | _ => return [st]
 
-def inlineCallStmts (ss: List Statement) (prog : Program)
-  : BoogieTransformM (List Statement) := do match ss with
-    | [] => return []
-    | s :: ss =>
-      let s' := (inlineCallStmt s prog)
-      let ss' := (inlineCallStmts ss prog)
-      return (← s') ++ (← ss')
+      | _ => return [.cmd cmd]
+
+def inlineCallStmtsRec (ss: List Statement) (prog : Program)
+  : BoogieTransformM (List Statement) :=
+  runStmtsRec inlineCallCmd ss prog
 
 def inlineCallL (dcls : List Decl) (prog : Program)
   : BoogieTransformM (List Decl) :=
-  match dcls with
-  | [] => return []
-  | d :: ds =>
-    match d with
-    | .proc p md =>
-      return Decl.proc { p with body := ← (inlineCallStmts p.body prog ) } md ::
-        (← (inlineCallL ds prog))
-    | _       => return d :: (← (inlineCallL ds prog))
+  runProcedures inlineCallCmd dcls prog
 
 end ProcedureInlining
 end Boogie
diff --git a/StrataMain.lean b/StrataMain.lean
index 53c5a9298..f6c85a2a5 100644
--- a/StrataMain.lean
+++ b/StrataMain.lean
@@ -9,9 +9,10 @@ import Strata.DDM.Elab
 import Strata.DDM.Ion
 import Strata.Util.IO
 
-import Strata.Languages.Python.Python
 import Strata.DDM.Integration.Java.Gen
-import StrataTest.Transform.ProcedureInlining
+import Strata.Languages.Python.Python
+import Strata.Transform.BoogieTransform
+import Strata.Transform.ProcedureInlining
 
 def exitFailure {α} (message : String) : IO α := do
   IO.eprintln (message  ++ "\n\nRun strata --help for additional help.")
@@ -202,18 +203,22 @@ def pyAnalyzeCommand : Command where
     let newPgm : Boogie.Program := { decls := preludePgm.decls ++ bpgm.decls }
     if verbose then
       IO.print newPgm
-    let newPgm := runInlineCall newPgm
-    if verbose then
-      IO.println "Inlined: "
-      IO.print newPgm
-    let solverName : String := "Strata/Languages/Python/z3_parallel.py"
-    let vcResults ← EIO.toIO (fun f => IO.Error.userError (toString f))
-                        (Boogie.verify solverName newPgm { Options.default with stopOnFirstError := false, verbose, removeIrrelevantAxioms := true }
-                                                   (moreFns := Strata.Python.ReFactory))
-    let mut s := ""
-    for vcResult in vcResults do
-      s := s ++ s!"\n{vcResult.obligation.label}: {Std.format vcResult.result}\n"
-    IO.println s
+    match Boogie.Transform.runProgram
+          (Boogie.ProcedureInlining.inlineCallCmd (excluded_calls := ["main"]))
+          newPgm .emp with
+    | ⟨.error e, _⟩ => panic! e
+    | ⟨.ok newPgm, _⟩ =>
+      if verbose then
+        IO.println "Inlined: "
+        IO.print newPgm
+      let solverName : String := "Strata/Languages/Python/z3_parallel.py"
+      let vcResults ← EIO.toIO (fun f => IO.Error.userError (toString f))
+                          (Boogie.verify solverName newPgm { Options.default with stopOnFirstError := false, verbose, removeIrrelevantAxioms := true }
+                                                    (moreFns := Strata.Python.ReFactory))
+      let mut s := ""
+      for vcResult in vcResults do
+        s := s ++ s!"\n{vcResult.obligation.label}: {Std.format vcResult.result}\n"
+      IO.println s
 
 def javaGenCommand : Command where
   name := "javaGen"
diff --git a/StrataTest/Languages/Boogie/ExprEvalTest.lean b/StrataTest/Languages/Boogie/ExprEvalTest.lean
index 59c06d97f..d24a47224 100644
--- a/StrataTest/Languages/Boogie/ExprEvalTest.lean
+++ b/StrataTest/Languages/Boogie/ExprEvalTest.lean
@@ -186,7 +186,7 @@ open Lambda.LTy.Syntax
   (.app () (.app () (.op () (BoogieIdent.unres "Int.Add") .none) eb[#100]) eb[#50]))
 
 
--- This may take a while (~ 1min)
+-- This may take a while (~ 5min)
 #eval (checkFactoryOps false)
 
 open Plausible TestGen
diff --git a/StrataTest/Languages/Python/expected/README.md b/StrataTest/Languages/Python/expected/README.md
index e93a56d3d..e98538107 100644
--- a/StrataTest/Languages/Python/expected/README.md
+++ b/StrataTest/Languages/Python/expected/README.md
@@ -3,6 +3,12 @@
 `StrataTest/Languages/Python/expected/test_precondition_verification.expected` looks like this:
 
 ```
+datetime_now_ensures_0: verified
+
+datetime_utcnow_ensures_0: verified
+
+ensures_str_strp_reverse: verified
+
 assert_name_is_foo: verified
 
 assert_opt_name_none_or_str: verified
@@ -11,31 +17,31 @@ assert_opt_name_none_or_bar: verified
 
 ensures_maybe_except_none: verified
 
-test_helper_procedure_assert_name_is_foo_3: verified
+test_helper_procedure_assert_name_is_foo_27: verified
 
-test_helper_procedure_assert_opt_name_none_or_str_4: verified
+test_helper_procedure_assert_opt_name_none_or_str_28: verified
 
-test_helper_procedure_assert_opt_name_none_or_bar_5: verified
+test_helper_procedure_assert_opt_name_none_or_bar_29: verified
 
-test_helper_procedure_assert_name_is_foo_11: verified
+test_helper_procedure_assert_name_is_foo_19: verified
 
-test_helper_procedure_assert_opt_name_none_or_str_12: verified
+test_helper_procedure_assert_opt_name_none_or_str_20: verified
 
-test_helper_procedure_assert_opt_name_none_or_bar_13: verified
+test_helper_procedure_assert_opt_name_none_or_bar_21: verified
 
-test_helper_procedure_assert_name_is_foo_19: failed
+test_helper_procedure_assert_name_is_foo_11: failed
 CEx: 
 
-test_helper_procedure_assert_opt_name_none_or_str_20: verified
+test_helper_procedure_assert_opt_name_none_or_str_12: verified
 
-test_helper_procedure_assert_opt_name_none_or_bar_21: verified
+test_helper_procedure_assert_opt_name_none_or_bar_13: verified
 
-test_helper_procedure_assert_name_is_foo_27: verified
+test_helper_procedure_assert_name_is_foo_3: verified
 
-test_helper_procedure_assert_opt_name_none_or_str_28: verified
+test_helper_procedure_assert_opt_name_none_or_str_4: verified
 
-test_helper_procedure_assert_opt_name_none_or_bar_29: failure
-CEx:
+test_helper_procedure_assert_opt_name_none_or_bar_5: failed
+CEx: 
 ```
 
 This can be read as:
@@ -71,9 +77,9 @@ Each of the following triples:
 ```
 test_helper_procedure_assert_name_is_foo_3: verified
 
-test_helper_procedure_assert_opt_name_none_or_str_5: verified
+test_helper_procedure_assert_opt_name_none_or_str_4: verified
 
-test_helper_procedure_assert_opt_name_none_or_bar_5: verified
+test_helper_procedure_assert_opt_name_none_or_bar_5: failed
 ```
 
-Comes from checking the assertions in the inlined calls of `test_helper_procedure`. The first two triples succeed, the third has a failure because `"Foo" != "foo"`, and the final has a failure because `"Bar" != "bar"`.
\ No newline at end of file
+Comes from checking the assertions in the inlined calls of `test_helper_procedure`. The first two triples succeed, the third has a failure because `"Foo" != "foo"`, and the final has a failure because `"Bar" != "bar"`.
diff --git a/StrataTest/Languages/Python/expected/test_precondition_verification.expected b/StrataTest/Languages/Python/expected/test_precondition_verification.expected
index 6d0e7f871..a0bbc7124 100644
--- a/StrataTest/Languages/Python/expected/test_precondition_verification.expected
+++ b/StrataTest/Languages/Python/expected/test_precondition_verification.expected
@@ -13,28 +13,28 @@ assert_opt_name_none_or_bar: verified
 
 ensures_maybe_except_none: verified
 
-test_helper_procedure_assert_name_is_foo_3: verified
+test_helper_procedure_assert_name_is_foo_27: verified
 
-test_helper_procedure_assert_opt_name_none_or_str_4: verified
+test_helper_procedure_assert_opt_name_none_or_str_28: verified
 
-test_helper_procedure_assert_opt_name_none_or_bar_5: verified
+test_helper_procedure_assert_opt_name_none_or_bar_29: verified
 
-test_helper_procedure_assert_name_is_foo_11: verified
+test_helper_procedure_assert_name_is_foo_19: verified
 
-test_helper_procedure_assert_opt_name_none_or_str_12: verified
+test_helper_procedure_assert_opt_name_none_or_str_20: verified
 
-test_helper_procedure_assert_opt_name_none_or_bar_13: verified
+test_helper_procedure_assert_opt_name_none_or_bar_21: verified
 
-test_helper_procedure_assert_name_is_foo_19: failed
+test_helper_procedure_assert_name_is_foo_11: failed
 CEx: 
 
-test_helper_procedure_assert_opt_name_none_or_str_20: verified
+test_helper_procedure_assert_opt_name_none_or_str_12: verified
 
-test_helper_procedure_assert_opt_name_none_or_bar_21: verified
+test_helper_procedure_assert_opt_name_none_or_bar_13: verified
 
-test_helper_procedure_assert_name_is_foo_27: verified
+test_helper_procedure_assert_name_is_foo_3: verified
 
-test_helper_procedure_assert_opt_name_none_or_str_28: verified
+test_helper_procedure_assert_opt_name_none_or_str_4: verified
 
-test_helper_procedure_assert_opt_name_none_or_bar_29: failed
+test_helper_procedure_assert_opt_name_none_or_bar_5: failed
 CEx: 
diff --git a/StrataTest/Transform/ProcedureInlining.lean b/StrataTest/Transform/ProcedureInlining.lean
index 41fb1a982..85d332902 100644
--- a/StrataTest/Transform/ProcedureInlining.lean
+++ b/StrataTest/Transform/ProcedureInlining.lean
@@ -209,9 +209,8 @@ end
 
 private def alphaEquiv (p1 p2:Boogie.Procedure):Except Format Bool := do
   if p1.body.length ≠ p2.body.length then
-    dbg_trace f!"p1: {p1}"
-    dbg_trace f!"p2: {p2}"
-    .error (s!"# statements do not match: inlined fn one has {p1.body.length}"
+    .error (s!"# statements do not match: in {p1.header.name}, "
+        ++ s!"inlined fn one has {p1.body.length}"
         ++ s!" whereas the answer has {p2.body.length}")
   else
     let newmap:IdMap := IdMap.mk ([], []) []
@@ -228,7 +227,7 @@ def translate (t : Strata.Program) : Boogie.Program :=
   (TransM.run Inhabited.default (translateProgram t)).fst
 
 def runInlineCall (p : Boogie.Program) : Boogie.Program :=
-  match (runProgram inlineCallStmt p .emp) with
+  match (runProgram inlineCallCmd p .emp) with
   | ⟨.ok res, _⟩ => res
   | ⟨.error e, _⟩ => panic! e
 
@@ -242,7 +241,9 @@ def checkInlining (prog : Boogie.Program) (progAns : Boogie.Program)
       match alphaEquiv p p' with
       | .ok _ => return .true
       | .error msg =>
+        dbg_trace s!"----- Inlined program ----"
         dbg_trace s!"{toString prog'}"
+        dbg_trace s!"----- Answer ----"
         dbg_trace s!"{toString progAns}"
         .error msg
     | _, _ => .error "?")
@@ -253,7 +254,6 @@ def Test1 :=
 #strata
 program Boogie;
 procedure f(x : bool) returns (y : bool) {
-  havoc x;
   y := !x;
 };
 
@@ -268,7 +268,6 @@ def Test1Ans :=
 #strata
 program Boogie;
 procedure f(x : bool) returns (y : bool) {
-  havoc x;
   y := !x;
 };
 
@@ -278,7 +277,7 @@ procedure h() returns () {
   inlined: {
     var tmp_arg_0 : bool := b_in;
     var tmp_arg_1 : bool;
-    havoc tmp_arg_0;
+    havoc tmp_arg_1;
     tmp_arg_1 := !tmp_arg_0;
     b_out := tmp_arg_1;
   }
@@ -326,6 +325,7 @@ procedure h() returns () {
   inlined: {
     var f_x : bool := b_in;
     var f_y : bool;
+    havoc f_y;
     if (f_x) {
       goto f_end;
     } else {
@@ -344,4 +344,57 @@ procedure h() returns () {
 #eval checkInlining (translate Test2) (translate Test2Ans)
 
 
+--- Test procedure calls inside subblocks
+
+def Test3 :=
+#strata
+program Boogie;
+procedure f(x : int) returns (y : int) {
+  y := x;
+};
+
+procedure g() returns () {
+  var f_out : int;
+  if (true) {
+    call f_out := f(1);
+  } else {
+    call f_out := f(2);
+  }
+};
+#end
+
+def Test3Ans :=
+#strata
+program Boogie;
+procedure f(x : int) returns (y : int) {
+  y := x;
+};
+
+procedure g() returns () {
+  var f_out : int;
+  if (true) {
+    inlined1: {
+      var f_x : int := 1;
+      var f_y : int;
+      havoc f_y;
+      f_y := f_x;
+      f_out := f_y;
+    }
+  } else {
+    inlined1: {
+      var f_x2 : int := 2;
+      var f_y2 : int;
+      havoc f_y2;
+      f_y2 := f_x2;
+      f_out := f_y2;
+    }
+  }
+};
+#end
+
+/-- info: ok: true -/
+#guard_msgs in
+#eval checkInlining (translate Test3) (translate Test3Ans)
+
+
 end ProcedureInliningExamples