From 717eaee0063074b804098d3cfd44a7a3f822b064 Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Tue, 16 Feb 2010 05:07:46 +0000
Subject: Implemented block coalescing invoked right after type checking.
 Controlled by the option /coalesceBlocks (default is to perform the
 optimization).

---
 Test/aitest1/Answer      |  90 ++++--------------------
 Test/aitest1/Linear4.bpl |   4 +-
 Test/aitest1/Linear5.bpl |   8 ++-
 Test/aitest9/answer      |   2 -
 Test/inline/Answer       |  41 +++--------
 Test/livevars/Answer     | 178 +++--------------------------------------------
 Test/test2/Answer        |   8 +--
 7 files changed, 45 insertions(+), 286 deletions(-)

(limited to 'Test')

diff --git a/Test/aitest1/Answer b/Test/aitest1/Answer
index 4e5c8f27..ca9ff22a 100644
--- a/Test/aitest1/Answer
+++ b/Test/aitest1/Answer
@@ -121,29 +121,9 @@ implementation FooTooStepByStep()
   L0:
     assume true;
     i := 5;
-    assume i == 5;
-    goto L1;
-
-  L1:
-    assume i == 5;
     i := 3 * i + 1;
-    assume i == 16;
-    goto L2;
-
-  L2:
-    assume i == 16;
     i := 3 * (i + 1);
-    assume 1 / 3 * i == 17;
-    goto L3;
-
-  L3:
-    assume 1 / 3 * i == 17;
     i := 1 + 3 * i;
-    assume i == 154;
-    goto L4;
-
-  L4:
-    assume i == 154;
     i := (i + 1) * 3;
     assume 1 / 3 * i == 155;
     return;
@@ -256,13 +236,18 @@ implementation p()
     assume true;
     assume x < y;
     assume x + 1 <= y;
-    goto B;
+    goto B, C;
 
   B:
     assume x + 1 <= y;
     x := x * x;
     assume true;
     return;
+
+  C:
+    assume x + 1 <= y;
+    assume x + 1 <= y;
+    return;
 }
 
 
@@ -285,25 +270,30 @@ implementation p()
     assume true;
     assume 0 - 1 <= x;
     assume -1 <= x;
-    goto B;
+    goto B, E;
 
   B:
     assume -1 <= x;
     assume x < y;
     assume x + 1 <= y && -1 <= x;
-    goto C;
+    goto C, E;
 
   C:
     assume x + 1 <= y && -1 <= x;
     x := x * x;
     assume 0 <= y;
-    goto D;
+    goto D, E;
 
   D:
     assume 0 <= y;
     x := y;
     assume x == y && 0 <= y;
     return;
+
+  E:
+    assume true;
+    assume true;
+    return;
 }
 
 
@@ -405,54 +395,14 @@ implementation foo()
   A:
     assume true;
     n := 0;
-    assume n == 0;
-    goto B;
-
-  B:
-    assume n == 0;
     j := 0;
-    assume j == 0 && n == 0;
-    goto C;
-
-  C:
-    assume j == 0 && n == 0;
     i := j + 1;
-    assume i == j + 1 && j == 0 && n == 0;
-    goto D;
-
-  D:
-    assume i == j + 1 && j == 0 && n == 0;
     i := i + 1;
-    assume i == j + 2 && j == 0 && n == 0;
-    goto E;
-
-  E:
-    assume i == j + 2 && j == 0 && n == 0;
     i := i + 1;
-    assume i == j + 3 && j == 0 && n == 0;
-    goto F;
-
-  F:
-    assume i == j + 3 && j == 0 && n == 0;
     i := i + 1;
-    assume i == j + 4 && j == 0 && n == 0;
-    goto G;
-
-  G:
-    assume i == j + 4 && j == 0 && n == 0;
     i := i + 1;
-    assume i == j + 5 && j == 0 && n == 0;
-    goto H;
-
-  H:
-    assume i == j + 5 && j == 0 && n == 0;
     j := j + 1;
     assume i == j + 4 && j == 1 && n == 0;
-    goto I;
-
-  I:
-    assume i == j + 4 && j == 1 && n == 0;
-    assume i == j + 4 && j == 1 && n == 0;
     return;
 }
 
@@ -481,19 +431,9 @@ implementation foo()
   loop0:  // cut point
     assume 4 <= n && 0 <= i && j == i + 1;
     assume j <= n;
-    assume j <= n && 4 <= n && 0 <= i && j == i + 1;
-    goto loop1;
-
-  loop1:
-    assume j <= n && 4 <= n && 0 <= i && j == i + 1;
     i := i + 1;
-    assume 1 <= i && j == i && j <= n && 4 <= n;
-    goto loop2;
-
-  loop2:
-    assume j <= n && 4 <= n && 1 <= i && j == i;
     j := j + 1;
-    assume j <= n + 1 && j == i + 1 && 4 <= n && 1 <= i;
+    assume j <= n + 1 && j == i + 1 && 1 <= i && 4 <= n;
     goto loop0, exit;
 
   exit:
diff --git a/Test/aitest1/Linear4.bpl b/Test/aitest1/Linear4.bpl
index c8c4605c..2207debe 100644
--- a/Test/aitest1/Linear4.bpl
+++ b/Test/aitest1/Linear4.bpl
@@ -8,8 +8,10 @@ procedure p()
 {
   A:
     assume x < y;
-    goto B;
+    goto B, C;
   B:
     x := x*x;
     return;
+  C:
+    return;
 }
diff --git a/Test/aitest1/Linear5.bpl b/Test/aitest1/Linear5.bpl
index 4f04999c..199cb6f2 100644
--- a/Test/aitest1/Linear5.bpl
+++ b/Test/aitest1/Linear5.bpl
@@ -8,14 +8,16 @@ procedure p()
 {
   A:
     assume -1 <= x;
-    goto B;
+    goto B, E;
   B:
     assume x < y;
-    goto C;
+    goto C, E;
   C:
     x := x*x;
-    goto D;
+    goto D, E;
   D:
     x := y;
     return;
+  E:
+    return;
 }
diff --git a/Test/aitest9/answer b/Test/aitest9/answer
index dd10a8b3..d6bba688 100644
--- a/Test/aitest9/answer
+++ b/Test/aitest9/answer
@@ -14,13 +14,11 @@ Execution trace:
     TestIntervals.bpl(5,5): anon0
     TestIntervals.bpl(6,3): anon9_LoopHead
     TestIntervals.bpl(6,3): anon9_LoopDone
-    TestIntervals.bpl(11,5): anon2
     TestIntervals.bpl(12,14): anon10_Then
     TestIntervals.bpl(13,3): anon4
     TestIntervals.bpl(13,14): anon11_Then
     TestIntervals.bpl(14,3): anon6
     TestIntervals.bpl(14,14): anon12_Then
     TestIntervals.bpl(17,5): anon8
-    TestIntervals.bpl(21,3): Next
 
 Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/inline/Answer b/Test/inline/Answer
index d5a12321..934b45ba 100644
--- a/Test/inline/Answer
+++ b/Test/inline/Answer
@@ -356,9 +356,6 @@ implementation recursivetest()
 
   inline$recursive$0$anon3_Else:
     assume inline$recursive$0$x != 0;
-    goto inline$recursive$0$anon2;
-
-  inline$recursive$0$anon2:
     goto inline$recursive$1$Entry;
 
   inline$recursive$1$Entry:
@@ -375,9 +372,6 @@ implementation recursivetest()
 
   inline$recursive$1$anon3_Else:
     assume inline$recursive$1$x != 0;
-    goto inline$recursive$1$anon2;
-
-  inline$recursive$1$anon2:
     goto inline$recursive$2$Entry;
 
   inline$recursive$2$Entry:
@@ -394,26 +388,23 @@ implementation recursivetest()
 
   inline$recursive$2$anon3_Else:
     assume inline$recursive$2$x != 0;
-    goto inline$recursive$2$anon2;
-
-  inline$recursive$2$anon2:
     call inline$recursive$2$k := recursive(inline$recursive$2$x - 1);
     inline$recursive$2$y := inline$recursive$2$y + inline$recursive$2$k;
     goto inline$recursive$2$Return;
 
   inline$recursive$2$Return:
     inline$recursive$1$k := inline$recursive$2$y;
-    goto inline$recursive$1$anon2$1;
+    goto inline$recursive$1$anon3_Else$1;
 
-  inline$recursive$1$anon2$1:
+  inline$recursive$1$anon3_Else$1:
     inline$recursive$1$y := inline$recursive$1$y + inline$recursive$1$k;
     goto inline$recursive$1$Return;
 
   inline$recursive$1$Return:
     inline$recursive$0$k := inline$recursive$1$y;
-    goto inline$recursive$0$anon2$1;
+    goto inline$recursive$0$anon3_Else$1;
 
-  inline$recursive$0$anon2$1:
+  inline$recursive$0$anon3_Else$1:
     inline$recursive$0$y := inline$recursive$0$y + inline$recursive$0$k;
     goto inline$recursive$0$Return;
 
@@ -453,9 +444,6 @@ implementation recursive(x: int) returns (y: int)
 
   anon3_Else:
     assume x != 0;
-    goto anon2;
-
-  anon2:
     goto inline$recursive$0$Entry;
 
   inline$recursive$0$Entry:
@@ -472,9 +460,6 @@ implementation recursive(x: int) returns (y: int)
 
   inline$recursive$0$anon3_Else:
     assume inline$recursive$0$x != 0;
-    goto inline$recursive$0$anon2;
-
-  inline$recursive$0$anon2:
     goto inline$recursive$1$Entry;
 
   inline$recursive$1$Entry:
@@ -491,9 +476,6 @@ implementation recursive(x: int) returns (y: int)
 
   inline$recursive$1$anon3_Else:
     assume inline$recursive$1$x != 0;
-    goto inline$recursive$1$anon2;
-
-  inline$recursive$1$anon2:
     goto inline$recursive$2$Entry;
 
   inline$recursive$2$Entry:
@@ -510,34 +492,31 @@ implementation recursive(x: int) returns (y: int)
 
   inline$recursive$2$anon3_Else:
     assume inline$recursive$2$x != 0;
-    goto inline$recursive$2$anon2;
-
-  inline$recursive$2$anon2:
     call inline$recursive$2$k := recursive(inline$recursive$2$x - 1);
     inline$recursive$2$y := inline$recursive$2$y + inline$recursive$2$k;
     goto inline$recursive$2$Return;
 
   inline$recursive$2$Return:
     inline$recursive$1$k := inline$recursive$2$y;
-    goto inline$recursive$1$anon2$1;
+    goto inline$recursive$1$anon3_Else$1;
 
-  inline$recursive$1$anon2$1:
+  inline$recursive$1$anon3_Else$1:
     inline$recursive$1$y := inline$recursive$1$y + inline$recursive$1$k;
     goto inline$recursive$1$Return;
 
   inline$recursive$1$Return:
     inline$recursive$0$k := inline$recursive$1$y;
-    goto inline$recursive$0$anon2$1;
+    goto inline$recursive$0$anon3_Else$1;
 
-  inline$recursive$0$anon2$1:
+  inline$recursive$0$anon3_Else$1:
     inline$recursive$0$y := inline$recursive$0$y + inline$recursive$0$k;
     goto inline$recursive$0$Return;
 
   inline$recursive$0$Return:
     k := inline$recursive$0$y;
-    goto anon2$1;
+    goto anon3_Else$1;
 
-  anon2$1:
+  anon3_Else$1:
     y := y + k;
     return;
 }
diff --git a/Test/livevars/Answer b/Test/livevars/Answer
index d958205f..aaaee494 100644
--- a/Test/livevars/Answer
+++ b/Test/livevars/Answer
@@ -4,16 +4,12 @@ Execution trace:
     bla1.bpl(789,3): anon10_Then#1
     bla1.bpl(794,3): anon2#1
     bla1.bpl(822,3): inline$storm_IoAllocateIrp$0$label_8_case_1#1
-    bla1.bpl(830,3): inline$storm_IoAllocateIrp$0$label_13#1
     bla1.bpl(854,3): inline$storm_IoAllocateIrp$0$anon14_Then#1
     bla1.bpl(859,3): inline$storm_IoAllocateIrp$0$anon2#1
     bla1.bpl(879,3): inline$storm_IoAllocateIrp$0$anon16_Then#1
     bla1.bpl(884,3): inline$storm_IoAllocateIrp$0$anon5#1
     bla1.bpl(904,3): inline$storm_IoAllocateIrp$0$anon18_Then#1
     bla1.bpl(909,3): inline$storm_IoAllocateIrp$0$anon8#1
-    bla1.bpl(913,3): inline$storm_IoAllocateIrp$0$label_20#1
-    bla1.bpl(917,3): inline$storm_IoAllocateIrp$0$label_21#1
-    bla1.bpl(921,3): inline$storm_IoAllocateIrp$0$label_22#1
     bla1.bpl(945,3): inline$storm_IoAllocateIrp$0$anon20_Then#1
     bla1.bpl(950,3): inline$storm_IoAllocateIrp$0$anon11#1
     bla1.bpl(981,3): inline$IoGetNextIrpStackLocation$0$anon3_Then#1
@@ -21,12 +17,6 @@ Execution trace:
     bla1.bpl(1018,3): inline$storm_IoAllocateIrp$0$anon22_Then#1
     bla1.bpl(1023,3): inline$storm_IoAllocateIrp$0$anon13#1
     bla1.bpl(1035,3): inline$storm_IoAllocateIrp$0$label_36#1
-    bla1.bpl(1039,3): inline$storm_IoAllocateIrp$0$label_1#1
-    bla1.bpl(1042,3): inline$storm_IoAllocateIrp$0$Return#1
-    bla1.bpl(1046,3): label_6$1#1
-    bla1.bpl(1049,3): label_9#1
-    bla1.bpl(1053,3): label_10#1
-    bla1.bpl(1068,3): inline$IoSetNextIrpStackLocation$0$label_3#1
     bla1.bpl(1089,3): inline$IoSetNextIrpStackLocation$0$anon6_Then#1
     bla1.bpl(1094,3): inline$IoSetNextIrpStackLocation$0$anon2#1
     bla1.bpl(1112,3): inline$IoSetNextIrpStackLocation$0$anon8_Then#1
@@ -35,7 +25,6 @@ Execution trace:
     bla1.bpl(1162,3): inline$IoGetCurrentIrpStackLocation$0$anon2#1
     bla1.bpl(1197,3): anon12_Then#1
     bla1.bpl(1202,3): anon5#1
-    bla1.bpl(1209,3): label_20#1
     bla1.bpl(1255,3): inline$IoGetCurrentIrpStackLocation$1$anon3_Then#1
     bla1.bpl(1259,3): inline$IoGetCurrentIrpStackLocation$1$anon2#1
     bla1.bpl(1308,3): inline$I8xDeviceControl$0$anon3_Then#1
@@ -43,7 +32,6 @@ Execution trace:
     bla1.bpl(1348,3): inline$I8xKeyboardGetSysButtonEvent$0$label_9_false#1
     bla1.bpl(1376,3): inline$storm_IoSetCancelRoutine$0$label_7_false#1
     bla1.bpl(1408,3): inline$storm_IoSetCancelRoutine$0$label_8#1
-    bla1.bpl(1412,3): inline$storm_IoSetCancelRoutine$0$label_16#1
     bla1.bpl(1415,3): inline$storm_IoSetCancelRoutine$0$anon9_Else#1
     bla1.bpl(1423,3): inline$storm_IoSetCancelRoutine$0$anon10_Then#1
     bla1.bpl(1431,3): inline$storm_IoSetCancelRoutine$0$anon3#1
@@ -56,7 +44,6 @@ Execution trace:
     bla1.bpl(1532,3): inline$I8xKeyboardGetSysButtonEvent$0$anon7_Then#1
     bla1.bpl(1542,3): inline$I8xKeyboardGetSysButtonEvent$0$anon2#1
     bla1.bpl(1566,3): inline$I8xKeyboardGetSysButtonEvent$0$label_23_true#1
-    bla1.bpl(1570,3): inline$I8xKeyboardGetSysButtonEvent$0$label_27#1
     bla1.bpl(1579,3): inline$I8xKeyboardGetSysButtonEvent$0$label_13#1
     bla1.bpl(1586,3): inline$I8xKeyboardGetSysButtonEvent$0$label_13_true#1
     bla1.bpl(1619,3): inline$storm_IoCompleteRequest$0$label_6_false#1
@@ -65,7 +52,7 @@ Execution trace:
     bla1.bpl(1662,3): inline$storm_IoCompleteRequest$0$anon5_Then#1
     bla1.bpl(1672,3): inline$storm_IoCompleteRequest$0$anon2#1
     bla1.bpl(1734,3): anon14_Then#1
-    bla1.bpl(1747,3): label_24#1
+    bla1.bpl(1739,3): anon7#1
     bla1.bpl(1796,3): inline$storm_IoCancelIrp$0$anon12_Then#1
     bla1.bpl(1801,3): inline$storm_IoCancelIrp$0$anon2#1
     bla1.bpl(1812,3): inline$storm_IoCancelIrp$0$anon14_Else#1
@@ -76,9 +63,7 @@ Execution trace:
     bla1.bpl(1856,3): inline$storm_IoCancelIrp$0$anon8#1
     bla1.bpl(1867,3): inline$storm_IoCancelIrp$0$anon18_Then#1
     bla1.bpl(1872,3): inline$storm_IoCancelIrp$0$anon10#1
-    bla1.bpl(1876,3): inline$storm_IoCancelIrp$0$label_13#1
     bla1.bpl(1932,3): inline$storm_IoAcquireCancelSpinLock$0$label_11_true#1
-    bla1.bpl(1938,3): inline$storm_IoAcquireCancelSpinLock$0$label_15#1
     bla1.bpl(1947,3): inline$storm_IoAcquireCancelSpinLock$0$anon6_Else#1
     bla1.bpl(1955,3): inline$storm_IoAcquireCancelSpinLock$0$anon7_Then#1
     bla1.bpl(1965,3): inline$storm_IoAcquireCancelSpinLock$0$anon3#1
@@ -86,16 +71,10 @@ Execution trace:
     bla1.bpl(1981,3): inline$storm_IoAcquireCancelSpinLock$0$anon5#1
     bla1.bpl(2005,3): inline$storm_IoCancelIrp$0$label_16_true#1
     bla1.bpl(2023,3): inline$storm_IoCancelIrp$0$label_22_true#1
-    bla1.bpl(2027,3): inline$storm_IoCancelIrp$0$label_24#1
     bla1.bpl(2036,3): inline$storm_IoCancelIrp$0$label_25_false#1
     bla1.bpl(2054,3): inline$storm_IoCancelIrp$0$label_1#1
-    bla1.bpl(2057,3): inline$storm_IoCancelIrp$0$Return#1
-    bla1.bpl(2060,3): inline$cancel$0$label_3$1#1
-    bla1.bpl(2063,3): inline$cancel$0$label_1#1
-    bla1.bpl(2066,3): inline$cancel$0$Return#1
-    bla1.bpl(2069,3): label_24$1#1
     bla1.bpl(2076,3): anon15_Then#1
-    bla1.bpl(2086,3): label_1#1
+    bla1.bpl(2081,3): anon9#1
 
 Boogie program verifier finished with 0 verified, 1 error
 
@@ -106,7 +85,6 @@ Execution trace:
     daytona_bug2_ioctl_example_2.bpl(846,3): anon22_Then#2
     daytona_bug2_ioctl_example_2.bpl(851,3): anon2#2
     daytona_bug2_ioctl_example_2.bpl(879,3): inline$storm_IoAllocateIrp$0$label_8_case_1#2
-    daytona_bug2_ioctl_example_2.bpl(887,3): inline$storm_IoAllocateIrp$0$label_13#2
     daytona_bug2_ioctl_example_2.bpl(911,3): inline$storm_IoAllocateIrp$0$anon18_Then#2
     daytona_bug2_ioctl_example_2.bpl(916,3): inline$storm_IoAllocateIrp$0$anon2#2
     daytona_bug2_ioctl_example_2.bpl(936,3): inline$storm_IoAllocateIrp$0$anon20_Then#2
@@ -114,9 +92,6 @@ Execution trace:
     daytona_bug2_ioctl_example_2.bpl(961,3): inline$storm_IoAllocateIrp$0$anon22_Then#2
     daytona_bug2_ioctl_example_2.bpl(966,3): inline$storm_IoAllocateIrp$0$anon8#2
     daytona_bug2_ioctl_example_2.bpl(974,3): inline$storm_IoAllocateIrp$0$anon24_Else#2
-    daytona_bug2_ioctl_example_2.bpl(978,3): inline$storm_IoAllocateIrp$0$anon10#2
-    daytona_bug2_ioctl_example_2.bpl(982,3): inline$storm_IoAllocateIrp$0$label_21#2
-    daytona_bug2_ioctl_example_2.bpl(986,3): inline$storm_IoAllocateIrp$0$label_22#2
     daytona_bug2_ioctl_example_2.bpl(1010,3): inline$storm_IoAllocateIrp$0$anon25_Then#2
     daytona_bug2_ioctl_example_2.bpl(1015,3): inline$storm_IoAllocateIrp$0$anon13#2
     daytona_bug2_ioctl_example_2.bpl(1046,3): inline$IoGetNextIrpStackLocation$0$anon3_Then#2
@@ -125,11 +100,8 @@ Execution trace:
     daytona_bug2_ioctl_example_2.bpl(1090,3): inline$storm_IoAllocateIrp$0$anon28_Then#2
     daytona_bug2_ioctl_example_2.bpl(1095,3): inline$storm_IoAllocateIrp$0$anon17#2
     daytona_bug2_ioctl_example_2.bpl(1115,3): inline$storm_IoAllocateIrp$0$label_36#2
-    daytona_bug2_ioctl_example_2.bpl(1119,3): inline$storm_IoAllocateIrp$0$label_1#2
     daytona_bug2_ioctl_example_2.bpl(1129,3): anon24_Else#2
     daytona_bug2_ioctl_example_2.bpl(1144,3): anon25_Else#2
-    daytona_bug2_ioctl_example_2.bpl(1148,3): anon6#2
-    daytona_bug2_ioctl_example_2.bpl(1163,3): inline$IoSetNextIrpStackLocation$0$label_3#2
     daytona_bug2_ioctl_example_2.bpl(1184,3): inline$IoSetNextIrpStackLocation$0$anon6_Then#2
     daytona_bug2_ioctl_example_2.bpl(1189,3): inline$IoSetNextIrpStackLocation$0$anon2#2
     daytona_bug2_ioctl_example_2.bpl(1207,3): inline$IoSetNextIrpStackLocation$0$anon8_Then#2
@@ -142,15 +114,11 @@ Execution trace:
     daytona_bug2_ioctl_example_2.bpl(1311,3): anon13#2
     daytona_bug2_ioctl_example_2.bpl(1343,3): inline$myInitDriver$0$anon5_Then#2
     daytona_bug2_ioctl_example_2.bpl(1348,3): inline$myInitDriver$0$anon2#2
-    daytona_bug2_ioctl_example_2.bpl(1353,3): inline$myInitDriver$0$label_5#2
-    daytona_bug2_ioctl_example_2.bpl(1359,3): inline$storm_KeInitializeSpinLock$0$Entry#2
     daytona_bug2_ioctl_example_2.bpl(1383,3): inline$storm_KeInitializeSpinLock$0$anon3_Then#2
     daytona_bug2_ioctl_example_2.bpl(1388,3): inline$storm_KeInitializeSpinLock$0$anon2#2
     daytona_bug2_ioctl_example_2.bpl(1401,3): inline$myInitDriver$0$anon7_Else#2
     daytona_bug2_ioctl_example_2.bpl(1416,3): inline$myInitDriver$0$Return#2
-    daytona_bug2_ioctl_example_2.bpl(1419,3): label_19$1#2
     daytona_bug2_ioctl_example_2.bpl(1422,3): anon30_Else#2
-    daytona_bug2_ioctl_example_2.bpl(1432,3): label_23#2
     daytona_bug2_ioctl_example_2.bpl(1478,3): inline$IoGetCurrentIrpStackLocation$1$anon3_Then#2
     daytona_bug2_ioctl_example_2.bpl(1482,3): inline$IoGetCurrentIrpStackLocation$1$anon2#2
     daytona_bug2_ioctl_example_2.bpl(1495,3): inline$dispatch$0$anon4_Else#2
@@ -164,30 +132,23 @@ Execution trace:
     daytona_bug2_ioctl_example_2.bpl(1629,3): inline$IoGetCurrentIrpStackLocation$2$anon2#2
     daytona_bug2_ioctl_example_2.bpl(1642,3): inline$I8xDeviceControl$0$anon16_Else#2
     daytona_bug2_ioctl_example_2.bpl(1655,3): inline$I8xDeviceControl$0$label_19_case_2#2
-    daytona_bug2_ioctl_example_2.bpl(1668,3): inline$I8xKeyboardGetSysButtonEvent$0$start#2
     daytona_bug2_ioctl_example_2.bpl(1719,3): inline$IoGetCurrentIrpStackLocation$4$anon3_Then#2
     daytona_bug2_ioctl_example_2.bpl(1723,3): inline$IoGetCurrentIrpStackLocation$4$anon2#2
     daytona_bug2_ioctl_example_2.bpl(1736,3): inline$I8xKeyboardGetSysButtonEvent$0$anon34_Else#2
     daytona_bug2_ioctl_example_2.bpl(1749,3): inline$I8xKeyboardGetSysButtonEvent$0$label_14_false#2
     daytona_bug2_ioctl_example_2.bpl(1757,3): inline$I8xKeyboardGetSysButtonEvent$0$label_15_false#2
-    daytona_bug2_ioctl_example_2.bpl(1762,3): inline$I8xKeyboardGetSysButtonEvent$0$label_23#2
-    daytona_bug2_ioctl_example_2.bpl(1768,3): inline$storm_KeAcquireSpinLock$0$Entry#2
     daytona_bug2_ioctl_example_2.bpl(1811,3): inline$storm_KeAcquireSpinLock$0$anon10_Else#2
-    daytona_bug2_ioctl_example_2.bpl(1815,3): inline$storm_KeAcquireSpinLock$0$anon1#2
     daytona_bug2_ioctl_example_2.bpl(1835,3): inline$storm_KeAcquireSpinLock$0$label_13_true#2
     daytona_bug2_ioctl_example_2.bpl(1843,3): inline$storm_KeAcquireSpinLock$0$anon11_Else#2
-    daytona_bug2_ioctl_example_2.bpl(1847,3): inline$storm_KeAcquireSpinLock$0$anon4#2
     daytona_bug2_ioctl_example_2.bpl(1867,3): inline$storm_KeAcquireSpinLock$0$anon12_Then#2
     daytona_bug2_ioctl_example_2.bpl(1872,3): inline$storm_KeAcquireSpinLock$0$anon7#2
     daytona_bug2_ioctl_example_2.bpl(1883,3): inline$storm_KeAcquireSpinLock$0$anon14_Then#2
     daytona_bug2_ioctl_example_2.bpl(1888,3): inline$storm_KeAcquireSpinLock$0$anon9#2
     daytona_bug2_ioctl_example_2.bpl(1903,3): inline$storm_KeAcquireSpinLock$0$Return#2
-    daytona_bug2_ioctl_example_2.bpl(1906,3): inline$I8xKeyboardGetSysButtonEvent$0$label_23$1#2
     daytona_bug2_ioctl_example_2.bpl(1909,3): inline$I8xKeyboardGetSysButtonEvent$0$anon36_Else#2
     daytona_bug2_ioctl_example_2.bpl(1920,3): inline$I8xKeyboardGetSysButtonEvent$0$label_56_false#2
     daytona_bug2_ioctl_example_2.bpl(1951,3): inline$storm_IoSetCancelRoutine$0$label_7_false#2
     daytona_bug2_ioctl_example_2.bpl(1991,3): inline$storm_IoSetCancelRoutine$0$label_8#2
-    daytona_bug2_ioctl_example_2.bpl(1995,3): inline$storm_IoSetCancelRoutine$0$label_16#2
     daytona_bug2_ioctl_example_2.bpl(2010,3): inline$storm_IoSetCancelRoutine$0$anon12_Then#2
     daytona_bug2_ioctl_example_2.bpl(2014,3): inline$storm_IoSetCancelRoutine$0$anon5#2
     daytona_bug2_ioctl_example_2.bpl(2034,3): inline$storm_IoSetCancelRoutine$0$anon14_Then#2
@@ -195,14 +156,12 @@ Execution trace:
     daytona_bug2_ioctl_example_2.bpl(2050,3): inline$storm_IoSetCancelRoutine$0$anon16_Then#2
     daytona_bug2_ioctl_example_2.bpl(2055,3): inline$storm_IoSetCancelRoutine$0$anon10#2
     daytona_bug2_ioctl_example_2.bpl(2069,3): inline$storm_IoSetCancelRoutine$0$Return#2
-    daytona_bug2_ioctl_example_2.bpl(2072,3): inline$I8xKeyboardGetSysButtonEvent$0$label_62$1#2
     daytona_bug2_ioctl_example_2.bpl(2075,3): inline$I8xKeyboardGetSysButtonEvent$0$anon44_Else#2
     daytona_bug2_ioctl_example_2.bpl(2200,3): inline$I8xKeyboardGetSysButtonEvent$0$anon45_Else#2
     daytona_bug2_ioctl_example_2.bpl(2208,3): inline$I8xKeyboardGetSysButtonEvent$0$anon46_Then#2
     daytona_bug2_ioctl_example_2.bpl(2218,3): inline$I8xKeyboardGetSysButtonEvent$0$anon24#2
     daytona_bug2_ioctl_example_2.bpl(2246,3): inline$storm_IoSetCancelRoutine$1$label_7_false#2
     daytona_bug2_ioctl_example_2.bpl(2286,3): inline$storm_IoSetCancelRoutine$1$label_8#2
-    daytona_bug2_ioctl_example_2.bpl(2290,3): inline$storm_IoSetCancelRoutine$1$label_16#2
     daytona_bug2_ioctl_example_2.bpl(2293,3): inline$storm_IoSetCancelRoutine$1$anon12_Else#2
     daytona_bug2_ioctl_example_2.bpl(2301,3): inline$storm_IoSetCancelRoutine$1$anon13_Then#2
     daytona_bug2_ioctl_example_2.bpl(2311,3): inline$storm_IoSetCancelRoutine$1$anon5#2
@@ -212,18 +171,14 @@ Execution trace:
     daytona_bug2_ioctl_example_2.bpl(2348,3): inline$storm_IoSetCancelRoutine$1$anon16_Then#2
     daytona_bug2_ioctl_example_2.bpl(2353,3): inline$storm_IoSetCancelRoutine$1$anon10#2
     daytona_bug2_ioctl_example_2.bpl(2368,3): inline$storm_IoSetCancelRoutine$1$Return#2
-    daytona_bug2_ioctl_example_2.bpl(2372,3): inline$I8xKeyboardGetSysButtonEvent$0$label_69$1#2
     daytona_bug2_ioctl_example_2.bpl(2375,3): inline$I8xKeyboardGetSysButtonEvent$0$anon50_Else#2
     daytona_bug2_ioctl_example_2.bpl(2385,3): inline$I8xKeyboardGetSysButtonEvent$0$label_72_false#2
     daytona_bug2_ioctl_example_2.bpl(2407,3): inline$storm_IoMarkIrpPending$2$label_6_false#2
     daytona_bug2_ioctl_example_2.bpl(2447,3): inline$storm_IoMarkIrpPending$2$label_1#2
     daytona_bug2_ioctl_example_2.bpl(2454,3): inline$storm_IoMarkIrpPending$2$Return#2
-    daytona_bug2_ioctl_example_2.bpl(2457,3): inline$I8xKeyboardGetSysButtonEvent$0$label_73$1#2
     daytona_bug2_ioctl_example_2.bpl(2460,3): inline$I8xKeyboardGetSysButtonEvent$0$anon51_Else#2
     daytona_bug2_ioctl_example_2.bpl(2507,3): inline$I8xKeyboardGetSysButtonEvent$0$label_59#2
-    daytona_bug2_ioctl_example_2.bpl(2514,3): inline$storm_KeReleaseSpinLock$0$Entry#2
     daytona_bug2_ioctl_example_2.bpl(2533,3): inline$storm_KeReleaseSpinLock$0$anon8_Else#2
-    daytona_bug2_ioctl_example_2.bpl(2537,3): inline$storm_KeReleaseSpinLock$0$anon1#2
     daytona_bug2_ioctl_example_2.bpl(2574,3): inline$storm_KeReleaseSpinLock$0$label_11_true#2
     daytona_bug2_ioctl_example_2.bpl(2581,3): inline$storm_KeReleaseSpinLock$0$anon9_Else#2
     daytona_bug2_ioctl_example_2.bpl(2589,3): inline$storm_KeReleaseSpinLock$0$anon10_Then#2
@@ -231,7 +186,6 @@ Execution trace:
     daytona_bug2_ioctl_example_2.bpl(2610,3): inline$storm_KeReleaseSpinLock$0$anon11_Then#2
     daytona_bug2_ioctl_example_2.bpl(2615,3): inline$storm_KeReleaseSpinLock$0$anon7#2
     daytona_bug2_ioctl_example_2.bpl(2626,3): inline$storm_KeReleaseSpinLock$0$Return#2
-    daytona_bug2_ioctl_example_2.bpl(2629,3): inline$I8xKeyboardGetSysButtonEvent$0$label_59$1#2
     daytona_bug2_ioctl_example_2.bpl(2632,3): inline$I8xKeyboardGetSysButtonEvent$0$anon43_Else#2
     daytona_bug2_ioctl_example_2.bpl(2858,3): inline$I8xKeyboardGetSysButtonEvent$0$label_51#2
     daytona_bug2_ioctl_example_2.bpl(2865,3): inline$I8xKeyboardGetSysButtonEvent$0$label_51_true#2
@@ -241,23 +195,18 @@ Execution trace:
     daytona_bug2_ioctl_example_2.bpl(2959,3): inline$storm_IoCompleteRequest$2$anon7_Then#2
     daytona_bug2_ioctl_example_2.bpl(2969,3): inline$storm_IoCompleteRequest$2$anon2#2
     daytona_bug2_ioctl_example_2.bpl(2980,3): inline$storm_IoCompleteRequest$2$Return#2
-    daytona_bug2_ioctl_example_2.bpl(2983,3): inline$I8xCompleteSysButtonIrp$0$label_6$1#2
     daytona_bug2_ioctl_example_2.bpl(2986,3): inline$I8xCompleteSysButtonIrp$0$anon2_Else#2
     daytona_bug2_ioctl_example_2.bpl(3000,3): inline$I8xCompleteSysButtonIrp$0$Return#2
-    daytona_bug2_ioctl_example_2.bpl(3003,3): inline$I8xKeyboardGetSysButtonEvent$0$label_53$1#2
     daytona_bug2_ioctl_example_2.bpl(3006,3): inline$I8xKeyboardGetSysButtonEvent$0$anon42_Else#2
     daytona_bug2_ioctl_example_2.bpl(3157,3): inline$I8xKeyboardGetSysButtonEvent$0$label_1#2
     daytona_bug2_ioctl_example_2.bpl(3169,3): inline$I8xKeyboardGetSysButtonEvent$0$Return#2
-    daytona_bug2_ioctl_example_2.bpl(3172,3): inline$I8xDeviceControl$0$label_24$1#2
     daytona_bug2_ioctl_example_2.bpl(3175,3): inline$I8xDeviceControl$0$anon18_Else#2
     daytona_bug2_ioctl_example_2.bpl(3644,3): inline$I8xDeviceControl$0$label_1#2
     daytona_bug2_ioctl_example_2.bpl(3655,3): inline$I8xDeviceControl$0$Return#2
-    daytona_bug2_ioctl_example_2.bpl(3658,3): inline$dispatch$0$label_8$1#2
     daytona_bug2_ioctl_example_2.bpl(3661,3): inline$dispatch$0$anon5_Else#2
     daytona_bug2_ioctl_example_2.bpl(3682,3): inline$dispatch$0$Return#2
-    daytona_bug2_ioctl_example_2.bpl(3685,3): label_23$1#2
     daytona_bug2_ioctl_example_2.bpl(3692,3): anon31_Then#2
-    daytona_bug2_ioctl_example_2.bpl(3705,3): label_27#2
+    daytona_bug2_ioctl_example_2.bpl(3697,3): anon17#2
     daytona_bug2_ioctl_example_2.bpl(3754,3): inline$storm_IoCancelIrp$0$anon23_Then#2
     daytona_bug2_ioctl_example_2.bpl(3759,3): inline$storm_IoCancelIrp$0$anon2#2
     daytona_bug2_ioctl_example_2.bpl(3783,3): inline$storm_IoCancelIrp$0$anon25_Then#2
@@ -266,137 +215,85 @@ Execution trace:
     daytona_bug2_ioctl_example_2.bpl(3814,3): inline$storm_IoCancelIrp$0$anon8#2
     daytona_bug2_ioctl_example_2.bpl(3825,3): inline$storm_IoCancelIrp$0$anon29_Then#2
     daytona_bug2_ioctl_example_2.bpl(3830,3): inline$storm_IoCancelIrp$0$anon10#2
-    daytona_bug2_ioctl_example_2.bpl(3834,3): inline$storm_IoCancelIrp$0$label_13#2
     daytona_bug2_ioctl_example_2.bpl(3890,3): inline$storm_IoAcquireCancelSpinLock$0$label_11_true#2
     daytona_bug2_ioctl_example_2.bpl(3900,3): inline$storm_IoAcquireCancelSpinLock$0$anon8_Else#2
-    daytona_bug2_ioctl_example_2.bpl(3904,3): inline$storm_IoAcquireCancelSpinLock$0$anon2#2
     daytona_bug2_ioctl_example_2.bpl(3913,3): inline$storm_IoAcquireCancelSpinLock$0$anon9_Else#2
     daytona_bug2_ioctl_example_2.bpl(3921,3): inline$storm_IoAcquireCancelSpinLock$0$anon10_Then#2
     daytona_bug2_ioctl_example_2.bpl(3931,3): inline$storm_IoAcquireCancelSpinLock$0$anon5#2
     daytona_bug2_ioctl_example_2.bpl(3942,3): inline$storm_IoAcquireCancelSpinLock$0$anon11_Then#2
     daytona_bug2_ioctl_example_2.bpl(3947,3): inline$storm_IoAcquireCancelSpinLock$0$anon7#2
     daytona_bug2_ioctl_example_2.bpl(3958,3): inline$storm_IoAcquireCancelSpinLock$0$Return#2
-    daytona_bug2_ioctl_example_2.bpl(3961,3): inline$storm_IoCancelIrp$0$label_13$1#2
     daytona_bug2_ioctl_example_2.bpl(3964,3): inline$storm_IoCancelIrp$0$anon30_Else#2
     daytona_bug2_ioctl_example_2.bpl(3982,3): inline$storm_IoCancelIrp$0$label_16_true#2
     daytona_bug2_ioctl_example_2.bpl(4000,3): inline$storm_IoCancelIrp$0$label_22_true#2
     daytona_bug2_ioctl_example_2.bpl(4008,3): inline$storm_IoCancelIrp$0$anon32_Else#2
-    daytona_bug2_ioctl_example_2.bpl(4012,3): inline$storm_IoCancelIrp$0$anon16#2
     daytona_bug2_ioctl_example_2.bpl(4021,3): inline$storm_IoCancelIrp$0$label_27_false#2
     daytona_bug2_ioctl_example_2.bpl(4722,3): inline$storm_IoCancelIrp$0$label_1#2
     daytona_bug2_ioctl_example_2.bpl(4741,3): inline$storm_IoCancelIrp$0$Return#2
-    daytona_bug2_ioctl_example_2.bpl(4744,3): inline$cancel$0$label_3$1#2
     daytona_bug2_ioctl_example_2.bpl(4757,3): inline$cancel$0$anon2_Then#2
     daytona_bug2_ioctl_example_2.bpl(4771,3): anon32_Then#2
-    daytona_bug2_ioctl_example_2.bpl(4784,3): label_31#2
+    daytona_bug2_ioctl_example_2.bpl(4776,3): anon19#2
     daytona_bug2_ioctl_example_2.bpl(4814,3): anon33_Then#2
-    daytona_bug2_ioctl_example_2.bpl(4824,3): label_1#2
+    daytona_bug2_ioctl_example_2.bpl(4819,3): anon21#2
 
 Boogie program verifier finished with 0 verified, 1 error
 stack_overflow.bpl(97942,5): Error BP5001: This assertion might not hold.
 Execution trace:
     stack_overflow.bpl(1141,3): start#1
-    stack_overflow.bpl(1163,3): label_8#1
-    stack_overflow.bpl(1168,3): label_9#1
     stack_overflow.bpl(1197,3): inline$storm_IoAllocateIrp$0$label_8_case_1#1
-    stack_overflow.bpl(1205,3): inline$storm_IoAllocateIrp$0$label_13#1
-    stack_overflow.bpl(1216,3): inline$storm_IoAllocateIrp$0$label_18#1
-    stack_overflow.bpl(1221,3): inline$storm_IoAllocateIrp$0$label_19#1
     stack_overflow.bpl(1230,3): inline$storm_IoAllocateIrp$0$anon6_Else#1
-    stack_overflow.bpl(1234,3): inline$storm_IoAllocateIrp$0$anon1#1
-    stack_overflow.bpl(1238,3): inline$storm_IoAllocateIrp$0$label_21#1
-    stack_overflow.bpl(1242,3): inline$storm_IoAllocateIrp$0$label_22#1
     stack_overflow.bpl(1283,3): inline$IoGetNextIrpStackLocation$0$label_3_true#1
     stack_overflow.bpl(1302,3): inline$storm_IoAllocateIrp$0$anon7_Else#1
     stack_overflow.bpl(1321,3): inline$storm_IoAllocateIrp$0$anon8_Else#1
     stack_overflow.bpl(1330,3): inline$storm_IoAllocateIrp$0$anon5#1
     stack_overflow.bpl(1350,3): inline$storm_IoAllocateIrp$0$label_36#1
-    stack_overflow.bpl(1354,3): inline$storm_IoAllocateIrp$0$label_1#1
     stack_overflow.bpl(1364,3): anon10_Else#1
     stack_overflow.bpl(1379,3): anon11_Else#1
-    stack_overflow.bpl(1383,3): anon3#1
     stack_overflow.bpl(1418,3): inline$IoSetNextIrpStackLocation$0$label_3_true#1
     stack_overflow.bpl(1424,3): inline$IoSetNextIrpStackLocation$0$label_5#1
-    stack_overflow.bpl(1432,3): inline$IoSetNextIrpStackLocation$0$label_6#1
     stack_overflow.bpl(1446,3): anon12_Else#1
     stack_overflow.bpl(1486,3): inline$IoGetCurrentIrpStackLocation$0$label_3_true#1
     stack_overflow.bpl(1507,3): anon13_Else#1
-    stack_overflow.bpl(1532,3): inline$myInitDriver$0$label_4#1
-    stack_overflow.bpl(1541,3): inline$myInitDriver$0$label_6#1
-    stack_overflow.bpl(1547,3): inline$storm_KeInitializeSpinLock$0$Entry#1
-    stack_overflow.bpl(1555,3): inline$storm_KeInitializeSpinLock$0$label_3#1
     stack_overflow.bpl(1569,3): inline$myInitDriver$0$anon8_Else#1
-    stack_overflow.bpl(1577,3): inline$myInitDriver$0$label_9#1
-    stack_overflow.bpl(1583,3): inline$storm_KeInitializeSpinLock$1$Entry#1
-    stack_overflow.bpl(1591,3): inline$storm_KeInitializeSpinLock$1$label_3#1
     stack_overflow.bpl(1605,3): inline$myInitDriver$0$anon9_Else#1
-    stack_overflow.bpl(1613,3): inline$myInitDriver$0$label_12#1
-    stack_overflow.bpl(1619,3): inline$storm_KeInitializeSpinLock$2$Entry#1
-    stack_overflow.bpl(1627,3): inline$storm_KeInitializeSpinLock$2$label_3#1
     stack_overflow.bpl(1641,3): inline$myInitDriver$0$anon10_Else#1
-    stack_overflow.bpl(1649,3): inline$myInitDriver$0$label_15#1
-    stack_overflow.bpl(1655,3): inline$storm_KeInitializeSpinLock$3$Entry#1
-    stack_overflow.bpl(1663,3): inline$storm_KeInitializeSpinLock$3$label_3#1
     stack_overflow.bpl(1677,3): inline$myInitDriver$0$anon11_Else#1
     stack_overflow.bpl(1704,3): inline$myInitDriver$0$Return#1
-    stack_overflow.bpl(1707,3): label_23$1#1
     stack_overflow.bpl(1710,3): anon14_Else#1
-    stack_overflow.bpl(1729,3): inline$storm_thread_dispatch$0$start#1
     stack_overflow.bpl(1773,3): inline$IoGetCurrentIrpStackLocation$1$label_3_true#1
     stack_overflow.bpl(1794,3): inline$storm_thread_dispatch$0$anon4_Else#1
-    stack_overflow.bpl(1827,3): inline$BDLPnP$0$label_6#1
     stack_overflow.bpl(1877,3): inline$BDLPnP$0$anon54_Else#1
     stack_overflow.bpl(1891,3): inline$BDLPnP$0$label_16_true#1
-    stack_overflow.bpl(1895,3): inline$BDLPnP$0$label_20#1
-    stack_overflow.bpl(1899,3): inline$BDLPnP$0$label_21#1
-    stack_overflow.bpl(1903,3): inline$BDLPnP$0$label_22#1
     stack_overflow.bpl(1935,3): inline$BDLPnP$0$anon55_Else#1
     stack_overflow.bpl(1949,3): inline$BDLPnP$0$label_26_true#1
-    stack_overflow.bpl(1953,3): inline$BDLPnP$0$label_30#1
-    stack_overflow.bpl(1957,3): inline$BDLPnP$0$label_31#1
-    stack_overflow.bpl(1961,3): inline$BDLPnP$0$label_32#1
     stack_overflow.bpl(1993,3): inline$BDLPnP$0$anon56_Else#1
     stack_overflow.bpl(2007,3): inline$BDLPnP$0$label_36_true#1
     stack_overflow.bpl(2052,3): inline$IoGetCurrentIrpStackLocation$2$label_3_true#1
     stack_overflow.bpl(2073,3): inline$BDLPnP$0$anon57_Else#1
-    stack_overflow.bpl(2083,3): inline$BDLPnP$0$label_43#1
     stack_overflow.bpl(2100,3): inline$BDLPnP$0$label_44_true#1
     stack_overflow.bpl(2109,3): inline$BDLPnP$0$label_47#1
     stack_overflow.bpl(2113,3): inline$BDLPnP$0$anon58_Else#1
     stack_overflow.bpl(2127,3): inline$BDLPnP$0$label_51_false#1
     stack_overflow.bpl(77682,3): inline$BDLPnP$0$label_52_case_1#1
-    stack_overflow.bpl(77695,3): inline$BDLPnPStart$0$start#1
     stack_overflow.bpl(77742,3): inline$BDLPnPStart$0$anon36_Else#1
     stack_overflow.bpl(77756,3): inline$BDLPnPStart$0$label_11_true#1
-    stack_overflow.bpl(77760,3): inline$BDLPnPStart$0$label_15#1
-    stack_overflow.bpl(77764,3): inline$BDLPnPStart$0$label_16#1
-    stack_overflow.bpl(77768,3): inline$BDLPnPStart$0$label_17#1
     stack_overflow.bpl(77800,3): inline$BDLPnPStart$0$anon37_Else#1
     stack_overflow.bpl(77814,3): inline$BDLPnPStart$0$label_21_true#1
-    stack_overflow.bpl(77818,3): inline$BDLPnPStart$0$label_25#1
-    stack_overflow.bpl(77822,3): inline$BDLPnPStart$0$label_26#1
-    stack_overflow.bpl(77826,3): inline$BDLPnPStart$0$label_27#1
     stack_overflow.bpl(77858,3): inline$BDLPnPStart$0$anon38_Else#1
     stack_overflow.bpl(77872,3): inline$BDLPnPStart$0$label_31_true#1
-    stack_overflow.bpl(77886,3): inline$BDLCallLowerLevelDriverAndWait$0$start#1
+    stack_overflow.bpl(77879,3): inline$BDLPnPStart$0$label_32#1
     stack_overflow.bpl(77951,3): inline$IoGetCurrentIrpStackLocation$3$label_3_true#1
     stack_overflow.bpl(77972,3): inline$IoCopyCurrentIrpStackLocationToNext$0$anon4_Else#1
     stack_overflow.bpl(78013,3): inline$IoGetNextIrpStackLocation$1$label_3_true#1
     stack_overflow.bpl(78032,3): inline$IoCopyCurrentIrpStackLocationToNext$0$anon5_Else#1
     stack_overflow.bpl(78060,3): inline$IoCopyCurrentIrpStackLocationToNext$0$Return#1
-    stack_overflow.bpl(78063,3): inline$BDLCallLowerLevelDriverAndWait$0$label_6$1#1
     stack_overflow.bpl(78066,3): inline$BDLCallLowerLevelDriverAndWait$0$anon16_Else#1
-    stack_overflow.bpl(78086,3): inline$storm_KeInitializeEvent$0$label_3#1
     stack_overflow.bpl(78100,3): inline$BDLCallLowerLevelDriverAndWait$0$anon17_Else#1
     stack_overflow.bpl(78128,3): inline$storm_IoSetCompletionRoutine$0$label_7_false#1
     stack_overflow.bpl(78167,3): inline$storm_IoSetCompletionRoutine$0$label_8#1
-    stack_overflow.bpl(78170,3): inline$IoGetNextIrpStackLocation$2$Entry#1
-    stack_overflow.bpl(78174,3): inline$IoGetNextIrpStackLocation$2$start#1
-    stack_overflow.bpl(78178,3): inline$IoGetNextIrpStackLocation$2$label_3#1
     stack_overflow.bpl(78198,3): inline$IoGetNextIrpStackLocation$2$label_3_true#1
     stack_overflow.bpl(78217,3): inline$storm_IoSetCompletionRoutine$0$anon5_Else#1
     stack_overflow.bpl(78244,3): inline$storm_IoSetCompletionRoutine$0$Return#1
-    stack_overflow.bpl(78247,3): inline$BDLCallLowerLevelDriverAndWait$0$label_12$1#1
     stack_overflow.bpl(78250,3): inline$BDLCallLowerLevelDriverAndWait$0$anon18_Else#1
     stack_overflow.bpl(78290,3): inline$IoGetCurrentIrpStackLocation$4$label_3_true#1
     stack_overflow.bpl(78311,3): inline$BDLCallLowerLevelDriverAndWait$0$anon19_Else#1
@@ -404,37 +301,24 @@ Execution trace:
     stack_overflow.bpl(83288,3): inline$BDLCallLowerLevelDriverAndWait$0$anon21_Else#1
     stack_overflow.bpl(83333,3): inline$storm_IoCallDriver$1$label_9_false#1
     stack_overflow.bpl(83372,3): inline$storm_IoCallDriver$1$label_10#1
-    stack_overflow.bpl(83375,3): inline$IoSetNextIrpStackLocation$2$Entry#1
-    stack_overflow.bpl(83379,3): inline$IoSetNextIrpStackLocation$2$start#1
-    stack_overflow.bpl(83383,3): inline$IoSetNextIrpStackLocation$2$label_3#1
     stack_overflow.bpl(83403,3): inline$IoSetNextIrpStackLocation$2$label_3_true#1
     stack_overflow.bpl(83409,3): inline$IoSetNextIrpStackLocation$2$label_5#1
-    stack_overflow.bpl(83417,3): inline$IoSetNextIrpStackLocation$2$label_6#1
     stack_overflow.bpl(83431,3): inline$storm_IoCallDriver$1$anon11_Else#1
     stack_overflow.bpl(83471,3): inline$IoGetCurrentIrpStackLocation$14$label_3_true#1
     stack_overflow.bpl(83492,3): inline$storm_IoCallDriver$1$anon13_Else#1
-    stack_overflow.bpl(83505,3): inline$storm_IoCallDriver$1$label_23#1
     stack_overflow.bpl(85859,3): inline$storm_IoCallDriver$1$label_27_case_1#1
     stack_overflow.bpl(85929,3): inline$IoGetCurrentIrpStackLocation$19$label_3_true#1
     stack_overflow.bpl(85950,3): inline$CallCompletionRoutine$3$anon10_Else#1
     stack_overflow.bpl(86007,3): inline$IoGetCurrentIrpStackLocation$20$label_3_true#1
     stack_overflow.bpl(86028,3): inline$CallCompletionRoutine$3$anon11_Else#1
     stack_overflow.bpl(86045,3): inline$CallCompletionRoutine$3$label_18_true#1
-    stack_overflow.bpl(86049,3): inline$CallCompletionRoutine$3$label_19#1
     stack_overflow.bpl(87162,3): inline$CallCompletionRoutine$3$label_20_icall_2#1
-    stack_overflow.bpl(87173,3): inline$BDLDevicePowerIoCompletion$3$start#1
     stack_overflow.bpl(87239,3): inline$IoGetCurrentIrpStackLocation$21$label_3_true#1
     stack_overflow.bpl(87262,3): inline$BDLDevicePowerIoCompletion$3$anon30_Else#1
     stack_overflow.bpl(87307,3): inline$BDLDevicePowerIoCompletion$3$anon31_Else#1
     stack_overflow.bpl(87321,3): inline$BDLDevicePowerIoCompletion$3$label_20_true#1
-    stack_overflow.bpl(87325,3): inline$BDLDevicePowerIoCompletion$3$label_24#1
-    stack_overflow.bpl(87329,3): inline$BDLDevicePowerIoCompletion$3$label_25#1
-    stack_overflow.bpl(87333,3): inline$BDLDevicePowerIoCompletion$3$label_26#1
     stack_overflow.bpl(87365,3): inline$BDLDevicePowerIoCompletion$3$anon32_Else#1
     stack_overflow.bpl(87379,3): inline$BDLDevicePowerIoCompletion$3$label_30_true#1
-    stack_overflow.bpl(87383,3): inline$BDLDevicePowerIoCompletion$3$label_34#1
-    stack_overflow.bpl(87387,3): inline$BDLDevicePowerIoCompletion$3$label_35#1
-    stack_overflow.bpl(87391,3): inline$BDLDevicePowerIoCompletion$3$label_36#1
     stack_overflow.bpl(87423,3): inline$BDLDevicePowerIoCompletion$3$anon33_Else#1
     stack_overflow.bpl(87437,3): inline$BDLDevicePowerIoCompletion$3$label_40_true#1
     stack_overflow.bpl(87452,3): inline$BDLDevicePowerIoCompletion$3$label_41_true#1
@@ -442,14 +326,8 @@ Execution trace:
     stack_overflow.bpl(87527,3): inline$BDLDevicePowerIoCompletion$3$label_55_true#1
     stack_overflow.bpl(87555,3): inline$BDLDevicePowerIoCompletion$3$anon35_Else#1
     stack_overflow.bpl(87569,3): inline$BDLDevicePowerIoCompletion$3$label_62_true#1
-    stack_overflow.bpl(87573,3): inline$BDLDevicePowerIoCompletion$3$label_66#1
-    stack_overflow.bpl(87577,3): inline$BDLDevicePowerIoCompletion$3$label_67#1
-    stack_overflow.bpl(87581,3): inline$BDLDevicePowerIoCompletion$3$label_68#1
     stack_overflow.bpl(87613,3): inline$BDLDevicePowerIoCompletion$3$anon36_Else#1
     stack_overflow.bpl(87627,3): inline$BDLDevicePowerIoCompletion$3$label_72_true#1
-    stack_overflow.bpl(87631,3): inline$BDLDevicePowerIoCompletion$3$label_76#1
-    stack_overflow.bpl(87635,3): inline$BDLDevicePowerIoCompletion$3$label_77#1
-    stack_overflow.bpl(87639,3): inline$BDLDevicePowerIoCompletion$3$label_78#1
     stack_overflow.bpl(87671,3): inline$BDLDevicePowerIoCompletion$3$anon37_Else#1
     stack_overflow.bpl(87685,3): inline$BDLDevicePowerIoCompletion$3$label_82_true#1
     stack_overflow.bpl(87698,3): inline$BDLDevicePowerIoCompletion$3$label_86#1
@@ -458,103 +336,63 @@ Execution trace:
     stack_overflow.bpl(87738,3): inline$storm_IoCompleteRequest$7$label_6_false#1
     stack_overflow.bpl(87777,3): inline$storm_IoCompleteRequest$7$label_7#1
     stack_overflow.bpl(87789,3): inline$storm_IoCompleteRequest$7$Return#1
-    stack_overflow.bpl(87792,3): inline$BDLDevicePowerIoCompletion$3$label_92$1#1
     stack_overflow.bpl(87795,3): inline$BDLDevicePowerIoCompletion$3$anon40_Else#1
     stack_overflow.bpl(87806,3): inline$BDLDevicePowerIoCompletion$3$anon41_Else#1
     stack_overflow.bpl(87837,3): inline$BDLDevicePowerIoCompletion$3$anon42_Else#1
     stack_overflow.bpl(87851,3): inline$BDLDevicePowerIoCompletion$3$label_101_true#1
-    stack_overflow.bpl(87855,3): inline$BDLDevicePowerIoCompletion$3$label_105#1
-    stack_overflow.bpl(87859,3): inline$BDLDevicePowerIoCompletion$3$label_106#1
-    stack_overflow.bpl(87863,3): inline$BDLDevicePowerIoCompletion$3$label_107#1
     stack_overflow.bpl(87895,3): inline$BDLDevicePowerIoCompletion$3$anon43_Else#1
     stack_overflow.bpl(87909,3): inline$BDLDevicePowerIoCompletion$3$label_111_true#1
-    stack_overflow.bpl(87913,3): inline$BDLDevicePowerIoCompletion$3$label_115#1
-    stack_overflow.bpl(87917,3): inline$BDLDevicePowerIoCompletion$3$label_116#1
-    stack_overflow.bpl(87921,3): inline$BDLDevicePowerIoCompletion$3$label_117#1
     stack_overflow.bpl(87953,3): inline$BDLDevicePowerIoCompletion$3$anon44_Else#1
     stack_overflow.bpl(87967,3): inline$BDLDevicePowerIoCompletion$3$label_121_true#1
     stack_overflow.bpl(88039,3): inline$BDLDevicePowerIoCompletion$3$Return#1
-    stack_overflow.bpl(88043,3): inline$CallCompletionRoutine$3$label_20_icall_2$1#1
     stack_overflow.bpl(88046,3): inline$CallCompletionRoutine$3$anon13_Else#1
     stack_overflow.bpl(88146,3): inline$CallCompletionRoutine$3$label_20_icall_return#1
-    stack_overflow.bpl(88149,3): inline$CallCompletionRoutine$3$label_23#1
-    stack_overflow.bpl(88153,3): inline$CallCompletionRoutine$3$label_24#1
     stack_overflow.bpl(88160,3): inline$CallCompletionRoutine$3$label_24_true#1
-    stack_overflow.bpl(88164,3): inline$CallCompletionRoutine$3$label_25#1
     stack_overflow.bpl(88184,3): inline$CallCompletionRoutine$3$Return#1
-    stack_overflow.bpl(88187,3): inline$storm_IoCallDriver$1$label_39$1#1
     stack_overflow.bpl(88190,3): inline$storm_IoCallDriver$1$anon15_Else#1
     stack_overflow.bpl(88218,3): inline$storm_IoCallDriver$1$label_36#1
     stack_overflow.bpl(88237,3): inline$storm_IoCallDriver$1$Return#1
-    stack_overflow.bpl(88241,3): inline$storm_PoCallDriver$0$label_3$1#1
     stack_overflow.bpl(88244,3): inline$storm_PoCallDriver$0$anon2_Else#1
     stack_overflow.bpl(88262,3): inline$storm_PoCallDriver$0$Return#1
-    stack_overflow.bpl(88266,3): inline$BDLCallLowerLevelDriverAndWait$0$label_25$1#1
     stack_overflow.bpl(88269,3): inline$BDLCallLowerLevelDriverAndWait$0$anon22_Else#1
     stack_overflow.bpl(88283,3): inline$BDLCallLowerLevelDriverAndWait$0$label_29_false#1
     stack_overflow.bpl(88441,3): inline$BDLCallLowerLevelDriverAndWait$0$label_30#1
-    stack_overflow.bpl(88445,3): inline$BDLCallLowerLevelDriverAndWait$0$label_1#1
     stack_overflow.bpl(88477,3): inline$BDLCallLowerLevelDriverAndWait$0$Return#1
-    stack_overflow.bpl(88481,3): inline$BDLPnPStart$0$label_32$1#1
     stack_overflow.bpl(88484,3): inline$BDLPnPStart$0$anon39_Else#1
     stack_overflow.bpl(88675,3): inline$BDLPnPStart$0$label_37_true#1
     stack_overflow.bpl(88987,3): inline$BDLPnPStart$0$label_51_true#1
     stack_overflow.bpl(89015,3): inline$BDLPnPStart$0$anon41_Else#1
     stack_overflow.bpl(89029,3): inline$BDLPnPStart$0$label_56_true#1
-    stack_overflow.bpl(89033,3): inline$BDLPnPStart$0$label_60#1
-    stack_overflow.bpl(89037,3): inline$BDLPnPStart$0$label_61#1
-    stack_overflow.bpl(89041,3): inline$BDLPnPStart$0$label_62#1
     stack_overflow.bpl(89073,3): inline$BDLPnPStart$0$anon42_Else#1
     stack_overflow.bpl(89087,3): inline$BDLPnPStart$0$label_66_true#1
-    stack_overflow.bpl(89091,3): inline$BDLPnPStart$0$label_70#1
-    stack_overflow.bpl(89095,3): inline$BDLPnPStart$0$label_71#1
-    stack_overflow.bpl(89099,3): inline$BDLPnPStart$0$label_72#1
     stack_overflow.bpl(89131,3): inline$BDLPnPStart$0$anon43_Else#1
     stack_overflow.bpl(89145,3): inline$BDLPnPStart$0$label_76_true#1
     stack_overflow.bpl(89176,3): inline$BDLPnPStart$0$anon44_Else#1
     stack_overflow.bpl(89190,3): inline$BDLPnPStart$0$label_81_true#1
-    stack_overflow.bpl(89194,3): inline$BDLPnPStart$0$label_85#1
-    stack_overflow.bpl(89198,3): inline$BDLPnPStart$0$label_86#1
-    stack_overflow.bpl(89202,3): inline$BDLPnPStart$0$label_87#1
     stack_overflow.bpl(89234,3): inline$BDLPnPStart$0$anon45_Else#1
     stack_overflow.bpl(89248,3): inline$BDLPnPStart$0$label_91_true#1
-    stack_overflow.bpl(89252,3): inline$BDLPnPStart$0$label_95#1
-    stack_overflow.bpl(89256,3): inline$BDLPnPStart$0$label_96#1
-    stack_overflow.bpl(89260,3): inline$BDLPnPStart$0$label_97#1
     stack_overflow.bpl(89292,3): inline$BDLPnPStart$0$anon46_Else#1
     stack_overflow.bpl(89306,3): inline$BDLPnPStart$0$label_101_true#1
     stack_overflow.bpl(89361,3): inline$BDLPnPStart$0$Return#1
-    stack_overflow.bpl(89365,3): inline$BDLPnP$0$label_113$1#1
     stack_overflow.bpl(89368,3): inline$BDLPnP$0$anon67_Else#1
     stack_overflow.bpl(94586,3): inline$BDLPnP$0$label_139#1
     stack_overflow.bpl(94593,3): inline$BDLPnP$0$label_139_true#1
     stack_overflow.bpl(94622,3): inline$storm_IoCompleteRequest$57$label_6_true#1
     stack_overflow.bpl(94630,3): inline$storm_IoCompleteRequest$57$anon3_Else#1
-    stack_overflow.bpl(94634,3): inline$storm_IoCompleteRequest$57$anon1#1
     stack_overflow.bpl(94642,3): inline$storm_IoCompleteRequest$57$label_9_false#1
     stack_overflow.bpl(94662,3): inline$storm_IoCompleteRequest$57$label_1#1
     stack_overflow.bpl(94669,3): inline$storm_IoCompleteRequest$57$Return#1
-    stack_overflow.bpl(94672,3): inline$BDLPnP$0$label_142$1#1
     stack_overflow.bpl(94710,3): inline$BDLPnP$0$anon75_Then#1
     stack_overflow.bpl(95206,3): inline$BDLPnP$0$Return#1
-    stack_overflow.bpl(95209,3): inline$storm_thread_dispatch$0$label_8$1#1
     stack_overflow.bpl(95226,3): inline$storm_thread_dispatch$0$anon5_Then#1
     stack_overflow.bpl(95234,3): inline$storm_thread_dispatch$0$Return#1
-    stack_overflow.bpl(95237,3): label_29$1#1
-    stack_overflow.bpl(95240,3): label_32#1
-    stack_overflow.bpl(95243,3): inline$storm_thread_cancel$0$Entry#1
-    stack_overflow.bpl(95247,3): inline$storm_thread_cancel$0$start#1
-    stack_overflow.bpl(95276,3): inline$storm_IoCancelIrp$0$label_8#1
-    stack_overflow.bpl(95282,3): inline$storm_IoCancelIrp$0$label_9#1
     stack_overflow.bpl(95294,3): inline$storm_IoCancelIrp$0$anon9_Then#1
     stack_overflow.bpl(95299,3): inline$storm_IoCancelIrp$0$anon1#1
-    stack_overflow.bpl(95303,3): inline$storm_IoCancelIrp$0$label_13#1
     stack_overflow.bpl(95356,3): inline$storm_IoAcquireCancelSpinLock$0$anon4_Then#1
     stack_overflow.bpl(95518,3): inline$storm_IoCancelIrp$0$anon10_Then#1
     stack_overflow.bpl(95539,3): inline$storm_thread_cancel$0$anon2_Then#1
-    stack_overflow.bpl(95555,3): inline$storm_thread_dpc$0$start#1
-    stack_overflow.bpl(95578,3): inline$storm_thread_completion$0$start#1
+    stack_overflow.bpl(95543,3): inline$storm_thread_cancel$0$Return#1
     stack_overflow.bpl(97931,3): inline$storm_thread_completion$0$anon4_Then#1
-    stack_overflow.bpl(97941,3): label_1#1
+    stack_overflow.bpl(97935,3): inline$storm_thread_completion$0$Return#1
 
 Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/test2/Answer b/Test/test2/Answer
index dd1d944d..1e5a0d5f 100644
--- a/Test/test2/Answer
+++ b/Test/test2/Answer
@@ -250,22 +250,22 @@ Where.bpl(111,3): Error BP5001: This assertion might not hold.
 Execution trace:
     Where.bpl(102,5): anon0
     Where.bpl(104,3): anon3_LoopHead
-    Where.bpl(110,3): anon2
+    Where.bpl(104,3): anon3_LoopDone
 Where.bpl(128,3): Error BP5001: This assertion might not hold.
 Execution trace:
     Where.bpl(121,5): anon0
     Where.bpl(122,3): anon3_LoopHead
-    Where.bpl(125,3): anon2
+    Where.bpl(122,3): anon3_LoopDone
 Where.bpl(145,3): Error BP5001: This assertion might not hold.
 Execution trace:
     Where.bpl(138,5): anon0
     Where.bpl(139,3): anon3_LoopHead
-    Where.bpl(142,3): anon2
+    Where.bpl(139,3): anon3_LoopDone
 Where.bpl(162,3): Error BP5001: This assertion might not hold.
 Execution trace:
     Where.bpl(155,5): anon0
     Where.bpl(156,3): anon3_LoopHead
-    Where.bpl(159,3): anon2
+    Where.bpl(156,3): anon3_LoopDone
 
 Boogie program verifier finished with 2 verified, 9 errors
 
-- 
cgit v1.2.3