2 files changed, 18 insertions, 5 deletions
diff --git a/Test/inline/Answer b/Test/inline/Answer
index 934b45ba..12cb5960 100644
--- a/Test/inline/Answer
+++ b/Test/inline/Answer
@@ -1443,13 +1443,8 @@ Boogie program verifier finished with 5 verified, 0 errors
 test5.bpl(37,3): Error BP5001: This assertion might not hold.
 Execution trace:
     test5.bpl(34,10): anon0
-    test5.bpl(25,23): inline$P$0$Entry
     test5.bpl(28,10): inline$P$0$anon0
-    test5.bpl(25,23): inline$P$0$Return
-    test5.bpl(34,10): anon0$1
-    test5.bpl(25,23): inline$P$1$Entry
     test5.bpl(28,10): inline$P$1$anon0
-    test5.bpl(25,23): inline$P$1$Return
     test5.bpl(34,10): anon0$2
 
 Boogie program verifier finished with 4 verified, 1 error
@@ -1477,6 +1472,17 @@ Boogie program verifier finished with 1 verified, 1 error
 Elevator.bpl(17,5): Error BP5005: This loop invariant might not be maintained by the loop.
 Execution trace:
     Elevator.bpl(15,3): anon0
+    Elevator.bpl(15,3): anon0$1
+    Elevator.bpl(16,3): anon10_LoopHead
+    Elevator.bpl(19,5): anon10_LoopBody
+    Elevator.bpl(99,3): inline$MoveDown_Error$0$anon0
+    Elevator.bpl(24,7): anon13_Then$1
+
+Boogie program verifier finished with 1 verified, 1 error
+-------------------- Elevator.bpl with empty blocks --------------------
+Elevator.bpl(17,5): Error BP5005: This loop invariant might not be maintained by the loop.
+Execution trace:
+    Elevator.bpl(15,3): anon0
     Elevator.bpl(68,23): inline$Initialize$0$Entry
     Elevator.bpl(71,13): inline$Initialize$0$anon0
     Elevator.bpl(68,23): inline$Initialize$0$Return
diff --git a/Test/inline/runtest.bat b/Test/inline/runtest.bat
index 335c857d..179509f8 100644
--- a/Test/inline/runtest.bat
+++ b/Test/inline/runtest.bat
@@ -18,6 +18,13 @@ for %%f in (test5.bpl expansion.bpl expansion3.bpl Elevator.bpl) do (
   %BGEXE% %* %%f
 )
 
+REM Peephole optimizations are so good that Elevator seems worthwhile
+REM to include twice among these inline tests
+for %%f in (Elevator.bpl) do (
+  echo -------------------- %%f with empty blocks --------------------
+  %BGEXE% /removeEmptyBlocks:0 %* %%f
+)
+
 echo -------------------- expansion2.bpl --------------------
 %BGEXE% %* /proverLog:expansion2.sx expansion2.bpl
 %SystemRoot%\system32\find.exe /C "xxgz" expansion2.sx