Added "STORM benchmarks for testing correctness of live variable analysis" lit tests.

13 files changed, 747 insertions, 360 deletions

diff --git a/Test/livevars/Answer b/Test/livevars/Answer
index 54458e4c..a7a77b7b 100644
--- a/Test/livevars/Answer
+++ b/Test/livevars/Answer
@@ -1,372 +1,372 @@
-bla1.bpl(2095,5): Error BP5001: This assertion might not hold.

+bla1.bpl(2097,5): Error BP5001: This assertion might not hold.

 Execution trace:

-    bla1.bpl(749,3): start#1

-    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(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(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

-    bla1.bpl(986,3): inline$IoGetNextIrpStackLocation$0$anon2#1

-    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(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

-    bla1.bpl(1117,3): inline$IoSetNextIrpStackLocation$0$anon5#1

-    bla1.bpl(1157,3): inline$IoGetCurrentIrpStackLocation$0$anon3_Then#1

-    bla1.bpl(1162,3): inline$IoGetCurrentIrpStackLocation$0$anon2#1

-    bla1.bpl(1197,3): anon12_Then#1

-    bla1.bpl(1202,3): anon5#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

-    bla1.bpl(1312,3): inline$I8xDeviceControl$0$anon2#1

-    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(1427,3): inline$storm_IoSetCancelRoutine$0$anon9_Then#1

-    bla1.bpl(1431,3): inline$storm_IoSetCancelRoutine$0$anon3#1

-    bla1.bpl(1451,3): inline$storm_IoSetCancelRoutine$0$anon11_Then#1

-    bla1.bpl(1456,3): inline$storm_IoSetCancelRoutine$0$anon6#1

-    bla1.bpl(1467,3): inline$storm_IoSetCancelRoutine$0$anon13_Then#1

-    bla1.bpl(1472,3): inline$storm_IoSetCancelRoutine$0$anon8#1

-    bla1.bpl(1524,3): inline$I8xKeyboardGetSysButtonEvent$0$anon6_Else#1

-    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(1586,3): inline$I8xKeyboardGetSysButtonEvent$0$label_13_true#1

-    bla1.bpl(1619,3): inline$storm_IoCompleteRequest$0$label_6_false#1

-    bla1.bpl(1654,3): inline$storm_IoCompleteRequest$0$anon4_Else#1

-    bla1.bpl(1662,3): inline$storm_IoCompleteRequest$0$anon5_Then#1

-    bla1.bpl(1672,3): inline$storm_IoCompleteRequest$0$anon2#1

-    bla1.bpl(1676,3): inline$storm_IoCompleteRequest$0$label_1#1

-    bla1.bpl(1734,3): anon14_Then#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(1825,3): inline$storm_IoCancelIrp$0$anon14_Then#1

-    bla1.bpl(1830,3): inline$storm_IoCancelIrp$0$anon5#1

-    bla1.bpl(1851,3): inline$storm_IoCancelIrp$0$anon16_Then#1

-    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(1932,3): inline$storm_IoAcquireCancelSpinLock$0$label_11_true#1

-    bla1.bpl(1960,3): inline$storm_IoAcquireCancelSpinLock$0$anon6_Then#1

-    bla1.bpl(1965,3): inline$storm_IoAcquireCancelSpinLock$0$anon3#1

-    bla1.bpl(1976,3): inline$storm_IoAcquireCancelSpinLock$0$anon8_Then#1

-    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(2036,3): inline$storm_IoCancelIrp$0$label_25_false#1

-    bla1.bpl(2076,3): anon15_Then#1

-    bla1.bpl(2081,3): anon9#1

+    bla1.bpl(751,3): start#1

+    bla1.bpl(791,3): anon10_Then#1

+    bla1.bpl(796,3): anon2#1

+    bla1.bpl(824,3): inline$storm_IoAllocateIrp$0$label_8_case_1#1

+    bla1.bpl(856,3): inline$storm_IoAllocateIrp$0$anon14_Then#1

+    bla1.bpl(861,3): inline$storm_IoAllocateIrp$0$anon2#1

+    bla1.bpl(881,3): inline$storm_IoAllocateIrp$0$anon16_Then#1

+    bla1.bpl(886,3): inline$storm_IoAllocateIrp$0$anon5#1

+    bla1.bpl(906,3): inline$storm_IoAllocateIrp$0$anon18_Then#1

+    bla1.bpl(911,3): inline$storm_IoAllocateIrp$0$anon8#1

+    bla1.bpl(947,3): inline$storm_IoAllocateIrp$0$anon20_Then#1

+    bla1.bpl(952,3): inline$storm_IoAllocateIrp$0$anon11#1

+    bla1.bpl(983,3): inline$IoGetNextIrpStackLocation$0$anon3_Then#1

+    bla1.bpl(988,3): inline$IoGetNextIrpStackLocation$0$anon2#1

+    bla1.bpl(1020,3): inline$storm_IoAllocateIrp$0$anon22_Then#1

+    bla1.bpl(1025,3): inline$storm_IoAllocateIrp$0$anon13#1

+    bla1.bpl(1037,3): inline$storm_IoAllocateIrp$0$label_36#1

+    bla1.bpl(1091,3): inline$IoSetNextIrpStackLocation$0$anon6_Then#1

+    bla1.bpl(1096,3): inline$IoSetNextIrpStackLocation$0$anon2#1

+    bla1.bpl(1114,3): inline$IoSetNextIrpStackLocation$0$anon8_Then#1

+    bla1.bpl(1119,3): inline$IoSetNextIrpStackLocation$0$anon5#1

+    bla1.bpl(1159,3): inline$IoGetCurrentIrpStackLocation$0$anon3_Then#1

+    bla1.bpl(1164,3): inline$IoGetCurrentIrpStackLocation$0$anon2#1

+    bla1.bpl(1199,3): anon12_Then#1

+    bla1.bpl(1204,3): anon5#1

+    bla1.bpl(1257,3): inline$IoGetCurrentIrpStackLocation$1$anon3_Then#1

+    bla1.bpl(1261,3): inline$IoGetCurrentIrpStackLocation$1$anon2#1

+    bla1.bpl(1310,3): inline$I8xDeviceControl$0$anon3_Then#1

+    bla1.bpl(1314,3): inline$I8xDeviceControl$0$anon2#1

+    bla1.bpl(1350,3): inline$I8xKeyboardGetSysButtonEvent$0$label_9_false#1

+    bla1.bpl(1378,3): inline$storm_IoSetCancelRoutine$0$label_7_false#1

+    bla1.bpl(1429,3): inline$storm_IoSetCancelRoutine$0$anon9_Then#1

+    bla1.bpl(1433,3): inline$storm_IoSetCancelRoutine$0$anon3#1

+    bla1.bpl(1453,3): inline$storm_IoSetCancelRoutine$0$anon11_Then#1

+    bla1.bpl(1458,3): inline$storm_IoSetCancelRoutine$0$anon6#1

+    bla1.bpl(1469,3): inline$storm_IoSetCancelRoutine$0$anon13_Then#1

+    bla1.bpl(1474,3): inline$storm_IoSetCancelRoutine$0$anon8#1

+    bla1.bpl(1526,3): inline$I8xKeyboardGetSysButtonEvent$0$anon6_Else#1

+    bla1.bpl(1534,3): inline$I8xKeyboardGetSysButtonEvent$0$anon7_Then#1

+    bla1.bpl(1544,3): inline$I8xKeyboardGetSysButtonEvent$0$anon2#1

+    bla1.bpl(1568,3): inline$I8xKeyboardGetSysButtonEvent$0$label_23_true#1

+    bla1.bpl(1588,3): inline$I8xKeyboardGetSysButtonEvent$0$label_13_true#1

+    bla1.bpl(1621,3): inline$storm_IoCompleteRequest$0$label_6_false#1

+    bla1.bpl(1656,3): inline$storm_IoCompleteRequest$0$anon4_Else#1

+    bla1.bpl(1664,3): inline$storm_IoCompleteRequest$0$anon5_Then#1

+    bla1.bpl(1674,3): inline$storm_IoCompleteRequest$0$anon2#1

+    bla1.bpl(1678,3): inline$storm_IoCompleteRequest$0$label_1#1

+    bla1.bpl(1736,3): anon14_Then#1

+    bla1.bpl(1741,3): anon7#1

+    bla1.bpl(1798,3): inline$storm_IoCancelIrp$0$anon12_Then#1

+    bla1.bpl(1803,3): inline$storm_IoCancelIrp$0$anon2#1

+    bla1.bpl(1827,3): inline$storm_IoCancelIrp$0$anon14_Then#1

+    bla1.bpl(1832,3): inline$storm_IoCancelIrp$0$anon5#1

+    bla1.bpl(1853,3): inline$storm_IoCancelIrp$0$anon16_Then#1

+    bla1.bpl(1858,3): inline$storm_IoCancelIrp$0$anon8#1

+    bla1.bpl(1869,3): inline$storm_IoCancelIrp$0$anon18_Then#1

+    bla1.bpl(1874,3): inline$storm_IoCancelIrp$0$anon10#1

+    bla1.bpl(1934,3): inline$storm_IoAcquireCancelSpinLock$0$label_11_true#1

+    bla1.bpl(1962,3): inline$storm_IoAcquireCancelSpinLock$0$anon6_Then#1

+    bla1.bpl(1967,3): inline$storm_IoAcquireCancelSpinLock$0$anon3#1

+    bla1.bpl(1978,3): inline$storm_IoAcquireCancelSpinLock$0$anon8_Then#1

+    bla1.bpl(1983,3): inline$storm_IoAcquireCancelSpinLock$0$anon5#1

+    bla1.bpl(2007,3): inline$storm_IoCancelIrp$0$label_16_true#1

+    bla1.bpl(2025,3): inline$storm_IoCancelIrp$0$label_22_true#1

+    bla1.bpl(2038,3): inline$storm_IoCancelIrp$0$label_25_false#1

+    bla1.bpl(2078,3): anon15_Then#1

+    bla1.bpl(2083,3): anon9#1

 

 Boogie program verifier finished with 0 verified, 1 error

 

 Boogie program verifier finished with 1 verified, 0 errors

-daytona_bug2_ioctl_example_2.bpl(4833,5): Error BP5001: This assertion might not hold.

+daytona_bug2_ioctl_example_2.bpl(4835,5): Error BP5001: This assertion might not hold.

 Execution trace:

-    daytona_bug2_ioctl_example_2.bpl(805,3): start#2

-    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(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

-    daytona_bug2_ioctl_example_2.bpl(941,3): inline$storm_IoAllocateIrp$0$anon5#2

-    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(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

-    daytona_bug2_ioctl_example_2.bpl(1051,3): inline$IoGetNextIrpStackLocation$0$anon2#2

-    daytona_bug2_ioctl_example_2.bpl(1066,3): inline$storm_IoAllocateIrp$0$anon27_Else#2

-    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(1129,3): anon24_Else#2

-    daytona_bug2_ioctl_example_2.bpl(1144,3): anon25_Else#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

-    daytona_bug2_ioctl_example_2.bpl(1212,3): inline$IoSetNextIrpStackLocation$0$anon5#2

-    daytona_bug2_ioctl_example_2.bpl(1225,3): anon26_Else#2

-    daytona_bug2_ioctl_example_2.bpl(1259,3): inline$IoGetCurrentIrpStackLocation$0$anon3_Then#2

-    daytona_bug2_ioctl_example_2.bpl(1264,3): inline$IoGetCurrentIrpStackLocation$0$anon2#2

-    daytona_bug2_ioctl_example_2.bpl(1279,3): anon27_Else#2

-    daytona_bug2_ioctl_example_2.bpl(1306,3): anon28_Then#2

-    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(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(1422,3): anon30_Else#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

-    daytona_bug2_ioctl_example_2.bpl(1534,3): inline$I8xDeviceControl$0$anon13_Else#2

-    daytona_bug2_ioctl_example_2.bpl(1557,3): inline$I8xDeviceControl$0$anon14_Then#2

-    daytona_bug2_ioctl_example_2.bpl(1562,3): inline$I8xDeviceControl$0$anon4#2

-    daytona_bug2_ioctl_example_2.bpl(1575,3): inline$I8xDeviceControl$0$label_11_true#2

-    daytona_bug2_ioctl_example_2.bpl(1588,3): inline$I8xDeviceControl$0$label_13_true#2

-    daytona_bug2_ioctl_example_2.bpl(1596,3): inline$I8xDeviceControl$0$label_14_false#2

-    daytona_bug2_ioctl_example_2.bpl(1625,3): inline$IoGetCurrentIrpStackLocation$2$anon3_Then#2

-    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(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(1811,3): inline$storm_KeAcquireSpinLock$0$anon10_Else#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(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(1892,3): inline$storm_KeAcquireSpinLock$0$label_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(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

-    daytona_bug2_ioctl_example_2.bpl(2039,3): inline$storm_IoSetCancelRoutine$0$anon8#2

-    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(2062,3): inline$storm_IoSetCancelRoutine$0$label_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(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

-    daytona_bug2_ioctl_example_2.bpl(2319,3): inline$storm_IoSetCancelRoutine$1$anon14_Else#2

-    daytona_bug2_ioctl_example_2.bpl(2327,3): inline$storm_IoSetCancelRoutine$1$anon15_Then#2

-    daytona_bug2_ioctl_example_2.bpl(2337,3): inline$storm_IoSetCancelRoutine$1$anon8#2

-    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(2361,3): inline$storm_IoSetCancelRoutine$1$label_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(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(2533,3): inline$storm_KeReleaseSpinLock$0$anon8_Else#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

-    daytona_bug2_ioctl_example_2.bpl(2599,3): inline$storm_KeReleaseSpinLock$0$anon5#2

-    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(2619,3): inline$storm_KeReleaseSpinLock$0$label_1#2

-    daytona_bug2_ioctl_example_2.bpl(2632,3): inline$I8xKeyboardGetSysButtonEvent$0$anon43_Else#2

-    daytona_bug2_ioctl_example_2.bpl(2865,3): inline$I8xKeyboardGetSysButtonEvent$0$label_51_true#2

-    daytona_bug2_ioctl_example_2.bpl(2908,3): inline$storm_IoCompleteRequest$2$label_6_false#2

-    daytona_bug2_ioctl_example_2.bpl(2951,3): inline$storm_IoCompleteRequest$2$anon6_Else#2

-    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(2973,3): inline$storm_IoCompleteRequest$2$label_1#2

-    daytona_bug2_ioctl_example_2.bpl(2986,3): inline$I8xCompleteSysButtonIrp$0$anon2_Else#2

-    daytona_bug2_ioctl_example_2.bpl(3006,3): inline$I8xKeyboardGetSysButtonEvent$0$anon42_Else#2

-    daytona_bug2_ioctl_example_2.bpl(3013,3): inline$I8xKeyboardGetSysButtonEvent$0$label_52#2

-    daytona_bug2_ioctl_example_2.bpl(3157,3): inline$I8xKeyboardGetSysButtonEvent$0$label_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(3661,3): inline$dispatch$0$anon5_Else#2

-    daytona_bug2_ioctl_example_2.bpl(3692,3): anon31_Then#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

-    daytona_bug2_ioctl_example_2.bpl(3788,3): inline$storm_IoCancelIrp$0$anon5#2

-    daytona_bug2_ioctl_example_2.bpl(3809,3): inline$storm_IoCancelIrp$0$anon27_Then#2

-    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(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(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(3951,3): inline$storm_IoAcquireCancelSpinLock$0$label_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(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(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(4776,3): anon19#2

-    daytona_bug2_ioctl_example_2.bpl(4814,3): anon33_Then#2

-    daytona_bug2_ioctl_example_2.bpl(4819,3): anon21#2

+    daytona_bug2_ioctl_example_2.bpl(807,3): start#2

+    daytona_bug2_ioctl_example_2.bpl(848,3): anon22_Then#2

+    daytona_bug2_ioctl_example_2.bpl(853,3): anon2#2

+    daytona_bug2_ioctl_example_2.bpl(881,3): inline$storm_IoAllocateIrp$0$label_8_case_1#2

+    daytona_bug2_ioctl_example_2.bpl(913,3): inline$storm_IoAllocateIrp$0$anon18_Then#2

+    daytona_bug2_ioctl_example_2.bpl(918,3): inline$storm_IoAllocateIrp$0$anon2#2

+    daytona_bug2_ioctl_example_2.bpl(938,3): inline$storm_IoAllocateIrp$0$anon20_Then#2

+    daytona_bug2_ioctl_example_2.bpl(943,3): inline$storm_IoAllocateIrp$0$anon5#2

+    daytona_bug2_ioctl_example_2.bpl(963,3): inline$storm_IoAllocateIrp$0$anon22_Then#2

+    daytona_bug2_ioctl_example_2.bpl(968,3): inline$storm_IoAllocateIrp$0$anon8#2

+    daytona_bug2_ioctl_example_2.bpl(976,3): inline$storm_IoAllocateIrp$0$anon24_Else#2

+    daytona_bug2_ioctl_example_2.bpl(1012,3): inline$storm_IoAllocateIrp$0$anon25_Then#2

+    daytona_bug2_ioctl_example_2.bpl(1017,3): inline$storm_IoAllocateIrp$0$anon13#2

+    daytona_bug2_ioctl_example_2.bpl(1048,3): inline$IoGetNextIrpStackLocation$0$anon3_Then#2

+    daytona_bug2_ioctl_example_2.bpl(1053,3): inline$IoGetNextIrpStackLocation$0$anon2#2

+    daytona_bug2_ioctl_example_2.bpl(1068,3): inline$storm_IoAllocateIrp$0$anon27_Else#2

+    daytona_bug2_ioctl_example_2.bpl(1092,3): inline$storm_IoAllocateIrp$0$anon28_Then#2

+    daytona_bug2_ioctl_example_2.bpl(1097,3): inline$storm_IoAllocateIrp$0$anon17#2

+    daytona_bug2_ioctl_example_2.bpl(1117,3): inline$storm_IoAllocateIrp$0$label_36#2

+    daytona_bug2_ioctl_example_2.bpl(1131,3): anon24_Else#2

+    daytona_bug2_ioctl_example_2.bpl(1146,3): anon25_Else#2

+    daytona_bug2_ioctl_example_2.bpl(1186,3): inline$IoSetNextIrpStackLocation$0$anon6_Then#2

+    daytona_bug2_ioctl_example_2.bpl(1191,3): inline$IoSetNextIrpStackLocation$0$anon2#2

+    daytona_bug2_ioctl_example_2.bpl(1209,3): inline$IoSetNextIrpStackLocation$0$anon8_Then#2

+    daytona_bug2_ioctl_example_2.bpl(1214,3): inline$IoSetNextIrpStackLocation$0$anon5#2

+    daytona_bug2_ioctl_example_2.bpl(1227,3): anon26_Else#2

+    daytona_bug2_ioctl_example_2.bpl(1261,3): inline$IoGetCurrentIrpStackLocation$0$anon3_Then#2

+    daytona_bug2_ioctl_example_2.bpl(1266,3): inline$IoGetCurrentIrpStackLocation$0$anon2#2

+    daytona_bug2_ioctl_example_2.bpl(1281,3): anon27_Else#2

+    daytona_bug2_ioctl_example_2.bpl(1308,3): anon28_Then#2

+    daytona_bug2_ioctl_example_2.bpl(1313,3): anon13#2

+    daytona_bug2_ioctl_example_2.bpl(1345,3): inline$myInitDriver$0$anon5_Then#2

+    daytona_bug2_ioctl_example_2.bpl(1350,3): inline$myInitDriver$0$anon2#2

+    daytona_bug2_ioctl_example_2.bpl(1385,3): inline$storm_KeInitializeSpinLock$0$anon3_Then#2

+    daytona_bug2_ioctl_example_2.bpl(1390,3): inline$storm_KeInitializeSpinLock$0$anon2#2

+    daytona_bug2_ioctl_example_2.bpl(1403,3): inline$myInitDriver$0$anon7_Else#2

+    daytona_bug2_ioctl_example_2.bpl(1424,3): anon30_Else#2

+    daytona_bug2_ioctl_example_2.bpl(1480,3): inline$IoGetCurrentIrpStackLocation$1$anon3_Then#2

+    daytona_bug2_ioctl_example_2.bpl(1484,3): inline$IoGetCurrentIrpStackLocation$1$anon2#2

+    daytona_bug2_ioctl_example_2.bpl(1497,3): inline$dispatch$0$anon4_Else#2

+    daytona_bug2_ioctl_example_2.bpl(1536,3): inline$I8xDeviceControl$0$anon13_Else#2

+    daytona_bug2_ioctl_example_2.bpl(1559,3): inline$I8xDeviceControl$0$anon14_Then#2

+    daytona_bug2_ioctl_example_2.bpl(1564,3): inline$I8xDeviceControl$0$anon4#2

+    daytona_bug2_ioctl_example_2.bpl(1577,3): inline$I8xDeviceControl$0$label_11_true#2

+    daytona_bug2_ioctl_example_2.bpl(1590,3): inline$I8xDeviceControl$0$label_13_true#2

+    daytona_bug2_ioctl_example_2.bpl(1598,3): inline$I8xDeviceControl$0$label_14_false#2

+    daytona_bug2_ioctl_example_2.bpl(1627,3): inline$IoGetCurrentIrpStackLocation$2$anon3_Then#2

+    daytona_bug2_ioctl_example_2.bpl(1631,3): inline$IoGetCurrentIrpStackLocation$2$anon2#2

+    daytona_bug2_ioctl_example_2.bpl(1644,3): inline$I8xDeviceControl$0$anon16_Else#2

+    daytona_bug2_ioctl_example_2.bpl(1657,3): inline$I8xDeviceControl$0$label_19_case_2#2

+    daytona_bug2_ioctl_example_2.bpl(1721,3): inline$IoGetCurrentIrpStackLocation$4$anon3_Then#2

+    daytona_bug2_ioctl_example_2.bpl(1725,3): inline$IoGetCurrentIrpStackLocation$4$anon2#2

+    daytona_bug2_ioctl_example_2.bpl(1738,3): inline$I8xKeyboardGetSysButtonEvent$0$anon34_Else#2

+    daytona_bug2_ioctl_example_2.bpl(1751,3): inline$I8xKeyboardGetSysButtonEvent$0$label_14_false#2

+    daytona_bug2_ioctl_example_2.bpl(1759,3): inline$I8xKeyboardGetSysButtonEvent$0$label_15_false#2

+    daytona_bug2_ioctl_example_2.bpl(1813,3): inline$storm_KeAcquireSpinLock$0$anon10_Else#2

+    daytona_bug2_ioctl_example_2.bpl(1837,3): inline$storm_KeAcquireSpinLock$0$label_13_true#2

+    daytona_bug2_ioctl_example_2.bpl(1845,3): inline$storm_KeAcquireSpinLock$0$anon11_Else#2

+    daytona_bug2_ioctl_example_2.bpl(1869,3): inline$storm_KeAcquireSpinLock$0$anon12_Then#2

+    daytona_bug2_ioctl_example_2.bpl(1874,3): inline$storm_KeAcquireSpinLock$0$anon7#2

+    daytona_bug2_ioctl_example_2.bpl(1885,3): inline$storm_KeAcquireSpinLock$0$anon14_Then#2

+    daytona_bug2_ioctl_example_2.bpl(1890,3): inline$storm_KeAcquireSpinLock$0$anon9#2

+    daytona_bug2_ioctl_example_2.bpl(1894,3): inline$storm_KeAcquireSpinLock$0$label_1#2

+    daytona_bug2_ioctl_example_2.bpl(1911,3): inline$I8xKeyboardGetSysButtonEvent$0$anon36_Else#2

+    daytona_bug2_ioctl_example_2.bpl(1922,3): inline$I8xKeyboardGetSysButtonEvent$0$label_56_false#2

+    daytona_bug2_ioctl_example_2.bpl(1953,3): inline$storm_IoSetCancelRoutine$0$label_7_false#2

+    daytona_bug2_ioctl_example_2.bpl(2012,3): inline$storm_IoSetCancelRoutine$0$anon12_Then#2

+    daytona_bug2_ioctl_example_2.bpl(2016,3): inline$storm_IoSetCancelRoutine$0$anon5#2

+    daytona_bug2_ioctl_example_2.bpl(2036,3): inline$storm_IoSetCancelRoutine$0$anon14_Then#2

+    daytona_bug2_ioctl_example_2.bpl(2041,3): inline$storm_IoSetCancelRoutine$0$anon8#2

+    daytona_bug2_ioctl_example_2.bpl(2052,3): inline$storm_IoSetCancelRoutine$0$anon16_Then#2

+    daytona_bug2_ioctl_example_2.bpl(2057,3): inline$storm_IoSetCancelRoutine$0$anon10#2

+    daytona_bug2_ioctl_example_2.bpl(2064,3): inline$storm_IoSetCancelRoutine$0$label_1#2

+    daytona_bug2_ioctl_example_2.bpl(2077,3): inline$I8xKeyboardGetSysButtonEvent$0$anon44_Else#2

+    daytona_bug2_ioctl_example_2.bpl(2202,3): inline$I8xKeyboardGetSysButtonEvent$0$anon45_Else#2

+    daytona_bug2_ioctl_example_2.bpl(2210,3): inline$I8xKeyboardGetSysButtonEvent$0$anon46_Then#2

+    daytona_bug2_ioctl_example_2.bpl(2220,3): inline$I8xKeyboardGetSysButtonEvent$0$anon24#2

+    daytona_bug2_ioctl_example_2.bpl(2248,3): inline$storm_IoSetCancelRoutine$1$label_7_false#2

+    daytona_bug2_ioctl_example_2.bpl(2295,3): inline$storm_IoSetCancelRoutine$1$anon12_Else#2

+    daytona_bug2_ioctl_example_2.bpl(2303,3): inline$storm_IoSetCancelRoutine$1$anon13_Then#2

+    daytona_bug2_ioctl_example_2.bpl(2313,3): inline$storm_IoSetCancelRoutine$1$anon5#2

+    daytona_bug2_ioctl_example_2.bpl(2321,3): inline$storm_IoSetCancelRoutine$1$anon14_Else#2

+    daytona_bug2_ioctl_example_2.bpl(2329,3): inline$storm_IoSetCancelRoutine$1$anon15_Then#2

+    daytona_bug2_ioctl_example_2.bpl(2339,3): inline$storm_IoSetCancelRoutine$1$anon8#2

+    daytona_bug2_ioctl_example_2.bpl(2350,3): inline$storm_IoSetCancelRoutine$1$anon16_Then#2

+    daytona_bug2_ioctl_example_2.bpl(2355,3): inline$storm_IoSetCancelRoutine$1$anon10#2

+    daytona_bug2_ioctl_example_2.bpl(2363,3): inline$storm_IoSetCancelRoutine$1$label_1#2

+    daytona_bug2_ioctl_example_2.bpl(2377,3): inline$I8xKeyboardGetSysButtonEvent$0$anon50_Else#2

+    daytona_bug2_ioctl_example_2.bpl(2387,3): inline$I8xKeyboardGetSysButtonEvent$0$label_72_false#2

+    daytona_bug2_ioctl_example_2.bpl(2409,3): inline$storm_IoMarkIrpPending$2$label_6_false#2

+    daytona_bug2_ioctl_example_2.bpl(2449,3): inline$storm_IoMarkIrpPending$2$label_1#2

+    daytona_bug2_ioctl_example_2.bpl(2462,3): inline$I8xKeyboardGetSysButtonEvent$0$anon51_Else#2

+    daytona_bug2_ioctl_example_2.bpl(2509,3): inline$I8xKeyboardGetSysButtonEvent$0$label_59#2

+    daytona_bug2_ioctl_example_2.bpl(2535,3): inline$storm_KeReleaseSpinLock$0$anon8_Else#2

+    daytona_bug2_ioctl_example_2.bpl(2576,3): inline$storm_KeReleaseSpinLock$0$label_11_true#2

+    daytona_bug2_ioctl_example_2.bpl(2583,3): inline$storm_KeReleaseSpinLock$0$anon9_Else#2

+    daytona_bug2_ioctl_example_2.bpl(2591,3): inline$storm_KeReleaseSpinLock$0$anon10_Then#2

+    daytona_bug2_ioctl_example_2.bpl(2601,3): inline$storm_KeReleaseSpinLock$0$anon5#2

+    daytona_bug2_ioctl_example_2.bpl(2612,3): inline$storm_KeReleaseSpinLock$0$anon11_Then#2

+    daytona_bug2_ioctl_example_2.bpl(2617,3): inline$storm_KeReleaseSpinLock$0$anon7#2

+    daytona_bug2_ioctl_example_2.bpl(2621,3): inline$storm_KeReleaseSpinLock$0$label_1#2

+    daytona_bug2_ioctl_example_2.bpl(2634,3): inline$I8xKeyboardGetSysButtonEvent$0$anon43_Else#2

+    daytona_bug2_ioctl_example_2.bpl(2867,3): inline$I8xKeyboardGetSysButtonEvent$0$label_51_true#2

+    daytona_bug2_ioctl_example_2.bpl(2910,3): inline$storm_IoCompleteRequest$2$label_6_false#2

+    daytona_bug2_ioctl_example_2.bpl(2953,3): inline$storm_IoCompleteRequest$2$anon6_Else#2

+    daytona_bug2_ioctl_example_2.bpl(2961,3): inline$storm_IoCompleteRequest$2$anon7_Then#2

+    daytona_bug2_ioctl_example_2.bpl(2971,3): inline$storm_IoCompleteRequest$2$anon2#2

+    daytona_bug2_ioctl_example_2.bpl(2975,3): inline$storm_IoCompleteRequest$2$label_1#2

+    daytona_bug2_ioctl_example_2.bpl(2988,3): inline$I8xCompleteSysButtonIrp$0$anon2_Else#2

+    daytona_bug2_ioctl_example_2.bpl(3008,3): inline$I8xKeyboardGetSysButtonEvent$0$anon42_Else#2

+    daytona_bug2_ioctl_example_2.bpl(3015,3): inline$I8xKeyboardGetSysButtonEvent$0$label_52#2

+    daytona_bug2_ioctl_example_2.bpl(3159,3): inline$I8xKeyboardGetSysButtonEvent$0$label_1#2

+    daytona_bug2_ioctl_example_2.bpl(3177,3): inline$I8xDeviceControl$0$anon18_Else#2

+    daytona_bug2_ioctl_example_2.bpl(3646,3): inline$I8xDeviceControl$0$label_1#2

+    daytona_bug2_ioctl_example_2.bpl(3663,3): inline$dispatch$0$anon5_Else#2

+    daytona_bug2_ioctl_example_2.bpl(3694,3): anon31_Then#2

+    daytona_bug2_ioctl_example_2.bpl(3699,3): anon17#2

+    daytona_bug2_ioctl_example_2.bpl(3756,3): inline$storm_IoCancelIrp$0$anon23_Then#2

+    daytona_bug2_ioctl_example_2.bpl(3761,3): inline$storm_IoCancelIrp$0$anon2#2

+    daytona_bug2_ioctl_example_2.bpl(3785,3): inline$storm_IoCancelIrp$0$anon25_Then#2

+    daytona_bug2_ioctl_example_2.bpl(3790,3): inline$storm_IoCancelIrp$0$anon5#2

+    daytona_bug2_ioctl_example_2.bpl(3811,3): inline$storm_IoCancelIrp$0$anon27_Then#2

+    daytona_bug2_ioctl_example_2.bpl(3816,3): inline$storm_IoCancelIrp$0$anon8#2

+    daytona_bug2_ioctl_example_2.bpl(3827,3): inline$storm_IoCancelIrp$0$anon29_Then#2

+    daytona_bug2_ioctl_example_2.bpl(3832,3): inline$storm_IoCancelIrp$0$anon10#2

+    daytona_bug2_ioctl_example_2.bpl(3892,3): inline$storm_IoAcquireCancelSpinLock$0$label_11_true#2

+    daytona_bug2_ioctl_example_2.bpl(3902,3): inline$storm_IoAcquireCancelSpinLock$0$anon8_Else#2

+    daytona_bug2_ioctl_example_2.bpl(3915,3): inline$storm_IoAcquireCancelSpinLock$0$anon9_Else#2

+    daytona_bug2_ioctl_example_2.bpl(3923,3): inline$storm_IoAcquireCancelSpinLock$0$anon10_Then#2

+    daytona_bug2_ioctl_example_2.bpl(3933,3): inline$storm_IoAcquireCancelSpinLock$0$anon5#2

+    daytona_bug2_ioctl_example_2.bpl(3944,3): inline$storm_IoAcquireCancelSpinLock$0$anon11_Then#2

+    daytona_bug2_ioctl_example_2.bpl(3949,3): inline$storm_IoAcquireCancelSpinLock$0$anon7#2

+    daytona_bug2_ioctl_example_2.bpl(3953,3): inline$storm_IoAcquireCancelSpinLock$0$label_1#2

+    daytona_bug2_ioctl_example_2.bpl(3966,3): inline$storm_IoCancelIrp$0$anon30_Else#2

+    daytona_bug2_ioctl_example_2.bpl(3984,3): inline$storm_IoCancelIrp$0$label_16_true#2

+    daytona_bug2_ioctl_example_2.bpl(4002,3): inline$storm_IoCancelIrp$0$label_22_true#2

+    daytona_bug2_ioctl_example_2.bpl(4010,3): inline$storm_IoCancelIrp$0$anon32_Else#2

+    daytona_bug2_ioctl_example_2.bpl(4023,3): inline$storm_IoCancelIrp$0$label_27_false#2

+    daytona_bug2_ioctl_example_2.bpl(4724,3): inline$storm_IoCancelIrp$0$label_1#2

+    daytona_bug2_ioctl_example_2.bpl(4759,3): inline$cancel$0$anon2_Then#2

+    daytona_bug2_ioctl_example_2.bpl(4773,3): anon32_Then#2

+    daytona_bug2_ioctl_example_2.bpl(4778,3): anon19#2

+    daytona_bug2_ioctl_example_2.bpl(4816,3): anon33_Then#2

+    daytona_bug2_ioctl_example_2.bpl(4821,3): anon21#2

 

 Boogie program verifier finished with 0 verified, 1 error

-stack_overflow.bpl(97942,5): Error BP5001: This assertion might not hold.

+stack_overflow.bpl(97944,5): Error BP5001: This assertion might not hold.

 Execution trace:

-    stack_overflow.bpl(1141,3): start#1

-    stack_overflow.bpl(1197,3): inline$storm_IoAllocateIrp$0$label_8_case_1#1

-    stack_overflow.bpl(1230,3): inline$storm_IoAllocateIrp$0$anon6_Else#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(1364,3): anon10_Else#1

-    stack_overflow.bpl(1379,3): anon11_Else#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(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(1569,3): inline$myInitDriver$0$anon8_Else#1

-    stack_overflow.bpl(1605,3): inline$myInitDriver$0$anon9_Else#1

-    stack_overflow.bpl(1641,3): inline$myInitDriver$0$anon10_Else#1

-    stack_overflow.bpl(1677,3): inline$myInitDriver$0$anon11_Else#1

-    stack_overflow.bpl(1710,3): anon14_Else#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(1877,3): inline$BDLPnP$0$anon54_Else#1

-    stack_overflow.bpl(1891,3): inline$BDLPnP$0$label_16_true#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(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(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(77742,3): inline$BDLPnPStart$0$anon36_Else#1

-    stack_overflow.bpl(77756,3): inline$BDLPnPStart$0$label_11_true#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(77858,3): inline$BDLPnPStart$0$anon38_Else#1

-    stack_overflow.bpl(77872,3): inline$BDLPnPStart$0$label_31_true#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(78066,3): inline$BDLCallLowerLevelDriverAndWait$0$anon16_Else#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(78198,3): inline$IoGetNextIrpStackLocation$2$label_3_true#1

-    stack_overflow.bpl(78217,3): inline$storm_IoSetCompletionRoutine$0$anon5_Else#1

-    stack_overflow.bpl(78233,3): inline$storm_IoSetCompletionRoutine$0$label_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

-    stack_overflow.bpl(83279,3): inline$BDLCallLowerLevelDriverAndWait$0$label_18_true#1

-    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(83403,3): inline$IoSetNextIrpStackLocation$2$label_3_true#1

-    stack_overflow.bpl(83409,3): inline$IoSetNextIrpStackLocation$2$label_5#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(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(87162,3): inline$CallCompletionRoutine$3$label_20_icall_2#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(87365,3): inline$BDLDevicePowerIoCompletion$3$anon32_Else#1

-    stack_overflow.bpl(87379,3): inline$BDLDevicePowerIoCompletion$3$label_30_true#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

-    stack_overflow.bpl(87483,3): inline$BDLDevicePowerIoCompletion$3$label_44_true#1

-    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(87613,3): inline$BDLDevicePowerIoCompletion$3$anon36_Else#1

-    stack_overflow.bpl(87627,3): inline$BDLDevicePowerIoCompletion$3$label_72_true#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(87692,3): inline$BDLDevicePowerIoCompletion$3$label_83#1

-    stack_overflow.bpl(87698,3): inline$BDLDevicePowerIoCompletion$3$label_86#1

-    stack_overflow.bpl(87702,3): inline$BDLDevicePowerIoCompletion$3$anon38_Else#1

-    stack_overflow.bpl(87713,3): inline$BDLDevicePowerIoCompletion$3$anon39_Else#1

-    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(87782,3): inline$storm_IoCompleteRequest$7$label_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(87895,3): inline$BDLDevicePowerIoCompletion$3$anon43_Else#1

-    stack_overflow.bpl(87909,3): inline$BDLDevicePowerIoCompletion$3$label_111_true#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(87974,3): inline$BDLDevicePowerIoCompletion$3$label_122#1

-    stack_overflow.bpl(88046,3): inline$CallCompletionRoutine$3$anon13_Else#1

-    stack_overflow.bpl(88160,3): inline$CallCompletionRoutine$3$label_24_true#1

-    stack_overflow.bpl(88169,3): inline$CallCompletionRoutine$3$label_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(88222,3): inline$storm_IoCallDriver$1$label_1#1

-    stack_overflow.bpl(88244,3): inline$storm_PoCallDriver$0$anon2_Else#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(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(89073,3): inline$BDLPnPStart$0$anon42_Else#1

-    stack_overflow.bpl(89087,3): inline$BDLPnPStart$0$label_66_true#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(89234,3): inline$BDLPnPStart$0$anon45_Else#1

-    stack_overflow.bpl(89248,3): inline$BDLPnPStart$0$label_91_true#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(89313,3): inline$BDLPnPStart$0$label_102#1

-    stack_overflow.bpl(89368,3): inline$BDLPnP$0$anon67_Else#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(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(94710,3): inline$BDLPnP$0$anon75_Then#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(95294,3): inline$storm_IoCancelIrp$0$anon9_Then#1

-    stack_overflow.bpl(95299,3): inline$storm_IoCancelIrp$0$anon1#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(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(97935,3): inline$storm_thread_completion$0$Return#1

+    stack_overflow.bpl(1143,3): start#1

+    stack_overflow.bpl(1199,3): inline$storm_IoAllocateIrp$0$label_8_case_1#1

+    stack_overflow.bpl(1232,3): inline$storm_IoAllocateIrp$0$anon6_Else#1

+    stack_overflow.bpl(1285,3): inline$IoGetNextIrpStackLocation$0$label_3_true#1

+    stack_overflow.bpl(1304,3): inline$storm_IoAllocateIrp$0$anon7_Else#1

+    stack_overflow.bpl(1323,3): inline$storm_IoAllocateIrp$0$anon8_Else#1

+    stack_overflow.bpl(1332,3): inline$storm_IoAllocateIrp$0$anon5#1

+    stack_overflow.bpl(1352,3): inline$storm_IoAllocateIrp$0$label_36#1

+    stack_overflow.bpl(1366,3): anon10_Else#1

+    stack_overflow.bpl(1381,3): anon11_Else#1

+    stack_overflow.bpl(1420,3): inline$IoSetNextIrpStackLocation$0$label_3_true#1

+    stack_overflow.bpl(1426,3): inline$IoSetNextIrpStackLocation$0$label_5#1

+    stack_overflow.bpl(1448,3): anon12_Else#1

+    stack_overflow.bpl(1488,3): inline$IoGetCurrentIrpStackLocation$0$label_3_true#1

+    stack_overflow.bpl(1509,3): anon13_Else#1

+    stack_overflow.bpl(1571,3): inline$myInitDriver$0$anon8_Else#1

+    stack_overflow.bpl(1607,3): inline$myInitDriver$0$anon9_Else#1

+    stack_overflow.bpl(1643,3): inline$myInitDriver$0$anon10_Else#1

+    stack_overflow.bpl(1679,3): inline$myInitDriver$0$anon11_Else#1

+    stack_overflow.bpl(1712,3): anon14_Else#1

+    stack_overflow.bpl(1775,3): inline$IoGetCurrentIrpStackLocation$1$label_3_true#1

+    stack_overflow.bpl(1796,3): inline$storm_thread_dispatch$0$anon4_Else#1

+    stack_overflow.bpl(1879,3): inline$BDLPnP$0$anon54_Else#1

+    stack_overflow.bpl(1893,3): inline$BDLPnP$0$label_16_true#1

+    stack_overflow.bpl(1937,3): inline$BDLPnP$0$anon55_Else#1

+    stack_overflow.bpl(1951,3): inline$BDLPnP$0$label_26_true#1

+    stack_overflow.bpl(1995,3): inline$BDLPnP$0$anon56_Else#1

+    stack_overflow.bpl(2009,3): inline$BDLPnP$0$label_36_true#1

+    stack_overflow.bpl(2054,3): inline$IoGetCurrentIrpStackLocation$2$label_3_true#1

+    stack_overflow.bpl(2075,3): inline$BDLPnP$0$anon57_Else#1

+    stack_overflow.bpl(2102,3): inline$BDLPnP$0$label_44_true#1

+    stack_overflow.bpl(2111,3): inline$BDLPnP$0$label_47#1

+    stack_overflow.bpl(2115,3): inline$BDLPnP$0$anon58_Else#1

+    stack_overflow.bpl(2129,3): inline$BDLPnP$0$label_51_false#1

+    stack_overflow.bpl(77684,3): inline$BDLPnP$0$label_52_case_1#1

+    stack_overflow.bpl(77744,3): inline$BDLPnPStart$0$anon36_Else#1

+    stack_overflow.bpl(77758,3): inline$BDLPnPStart$0$label_11_true#1

+    stack_overflow.bpl(77802,3): inline$BDLPnPStart$0$anon37_Else#1

+    stack_overflow.bpl(77816,3): inline$BDLPnPStart$0$label_21_true#1

+    stack_overflow.bpl(77860,3): inline$BDLPnPStart$0$anon38_Else#1

+    stack_overflow.bpl(77874,3): inline$BDLPnPStart$0$label_31_true#1

+    stack_overflow.bpl(77881,3): inline$BDLPnPStart$0$label_32#1

+    stack_overflow.bpl(77953,3): inline$IoGetCurrentIrpStackLocation$3$label_3_true#1

+    stack_overflow.bpl(77974,3): inline$IoCopyCurrentIrpStackLocationToNext$0$anon4_Else#1

+    stack_overflow.bpl(78015,3): inline$IoGetNextIrpStackLocation$1$label_3_true#1

+    stack_overflow.bpl(78034,3): inline$IoCopyCurrentIrpStackLocationToNext$0$anon5_Else#1

+    stack_overflow.bpl(78068,3): inline$BDLCallLowerLevelDriverAndWait$0$anon16_Else#1

+    stack_overflow.bpl(78102,3): inline$BDLCallLowerLevelDriverAndWait$0$anon17_Else#1

+    stack_overflow.bpl(78130,3): inline$storm_IoSetCompletionRoutine$0$label_7_false#1

+    stack_overflow.bpl(78200,3): inline$IoGetNextIrpStackLocation$2$label_3_true#1

+    stack_overflow.bpl(78219,3): inline$storm_IoSetCompletionRoutine$0$anon5_Else#1

+    stack_overflow.bpl(78235,3): inline$storm_IoSetCompletionRoutine$0$label_1#1

+    stack_overflow.bpl(78252,3): inline$BDLCallLowerLevelDriverAndWait$0$anon18_Else#1

+    stack_overflow.bpl(78292,3): inline$IoGetCurrentIrpStackLocation$4$label_3_true#1

+    stack_overflow.bpl(78313,3): inline$BDLCallLowerLevelDriverAndWait$0$anon19_Else#1

+    stack_overflow.bpl(83281,3): inline$BDLCallLowerLevelDriverAndWait$0$label_18_true#1

+    stack_overflow.bpl(83290,3): inline$BDLCallLowerLevelDriverAndWait$0$anon21_Else#1

+    stack_overflow.bpl(83335,3): inline$storm_IoCallDriver$1$label_9_false#1

+    stack_overflow.bpl(83405,3): inline$IoSetNextIrpStackLocation$2$label_3_true#1

+    stack_overflow.bpl(83411,3): inline$IoSetNextIrpStackLocation$2$label_5#1

+    stack_overflow.bpl(83433,3): inline$storm_IoCallDriver$1$anon11_Else#1

+    stack_overflow.bpl(83473,3): inline$IoGetCurrentIrpStackLocation$14$label_3_true#1

+    stack_overflow.bpl(83494,3): inline$storm_IoCallDriver$1$anon13_Else#1

+    stack_overflow.bpl(85861,3): inline$storm_IoCallDriver$1$label_27_case_1#1

+    stack_overflow.bpl(85931,3): inline$IoGetCurrentIrpStackLocation$19$label_3_true#1

+    stack_overflow.bpl(85952,3): inline$CallCompletionRoutine$3$anon10_Else#1

+    stack_overflow.bpl(86009,3): inline$IoGetCurrentIrpStackLocation$20$label_3_true#1

+    stack_overflow.bpl(86030,3): inline$CallCompletionRoutine$3$anon11_Else#1

+    stack_overflow.bpl(86047,3): inline$CallCompletionRoutine$3$label_18_true#1

+    stack_overflow.bpl(87164,3): inline$CallCompletionRoutine$3$label_20_icall_2#1

+    stack_overflow.bpl(87241,3): inline$IoGetCurrentIrpStackLocation$21$label_3_true#1

+    stack_overflow.bpl(87264,3): inline$BDLDevicePowerIoCompletion$3$anon30_Else#1

+    stack_overflow.bpl(87309,3): inline$BDLDevicePowerIoCompletion$3$anon31_Else#1

+    stack_overflow.bpl(87323,3): inline$BDLDevicePowerIoCompletion$3$label_20_true#1

+    stack_overflow.bpl(87367,3): inline$BDLDevicePowerIoCompletion$3$anon32_Else#1

+    stack_overflow.bpl(87381,3): inline$BDLDevicePowerIoCompletion$3$label_30_true#1

+    stack_overflow.bpl(87425,3): inline$BDLDevicePowerIoCompletion$3$anon33_Else#1

+    stack_overflow.bpl(87439,3): inline$BDLDevicePowerIoCompletion$3$label_40_true#1

+    stack_overflow.bpl(87454,3): inline$BDLDevicePowerIoCompletion$3$label_41_true#1

+    stack_overflow.bpl(87485,3): inline$BDLDevicePowerIoCompletion$3$label_44_true#1

+    stack_overflow.bpl(87529,3): inline$BDLDevicePowerIoCompletion$3$label_55_true#1

+    stack_overflow.bpl(87557,3): inline$BDLDevicePowerIoCompletion$3$anon35_Else#1

+    stack_overflow.bpl(87571,3): inline$BDLDevicePowerIoCompletion$3$label_62_true#1

+    stack_overflow.bpl(87615,3): inline$BDLDevicePowerIoCompletion$3$anon36_Else#1

+    stack_overflow.bpl(87629,3): inline$BDLDevicePowerIoCompletion$3$label_72_true#1

+    stack_overflow.bpl(87673,3): inline$BDLDevicePowerIoCompletion$3$anon37_Else#1

+    stack_overflow.bpl(87687,3): inline$BDLDevicePowerIoCompletion$3$label_82_true#1

+    stack_overflow.bpl(87694,3): inline$BDLDevicePowerIoCompletion$3$label_83#1

+    stack_overflow.bpl(87700,3): inline$BDLDevicePowerIoCompletion$3$label_86#1

+    stack_overflow.bpl(87704,3): inline$BDLDevicePowerIoCompletion$3$anon38_Else#1

+    stack_overflow.bpl(87715,3): inline$BDLDevicePowerIoCompletion$3$anon39_Else#1

+    stack_overflow.bpl(87740,3): inline$storm_IoCompleteRequest$7$label_6_false#1

+    stack_overflow.bpl(87779,3): inline$storm_IoCompleteRequest$7$label_7#1

+    stack_overflow.bpl(87784,3): inline$storm_IoCompleteRequest$7$label_1#1

+    stack_overflow.bpl(87797,3): inline$BDLDevicePowerIoCompletion$3$anon40_Else#1

+    stack_overflow.bpl(87808,3): inline$BDLDevicePowerIoCompletion$3$anon41_Else#1

+    stack_overflow.bpl(87839,3): inline$BDLDevicePowerIoCompletion$3$anon42_Else#1

+    stack_overflow.bpl(87853,3): inline$BDLDevicePowerIoCompletion$3$label_101_true#1

+    stack_overflow.bpl(87897,3): inline$BDLDevicePowerIoCompletion$3$anon43_Else#1

+    stack_overflow.bpl(87911,3): inline$BDLDevicePowerIoCompletion$3$label_111_true#1

+    stack_overflow.bpl(87955,3): inline$BDLDevicePowerIoCompletion$3$anon44_Else#1

+    stack_overflow.bpl(87969,3): inline$BDLDevicePowerIoCompletion$3$label_121_true#1

+    stack_overflow.bpl(87976,3): inline$BDLDevicePowerIoCompletion$3$label_122#1

+    stack_overflow.bpl(88048,3): inline$CallCompletionRoutine$3$anon13_Else#1

+    stack_overflow.bpl(88162,3): inline$CallCompletionRoutine$3$label_24_true#1

+    stack_overflow.bpl(88171,3): inline$CallCompletionRoutine$3$label_1#1

+    stack_overflow.bpl(88192,3): inline$storm_IoCallDriver$1$anon15_Else#1

+    stack_overflow.bpl(88220,3): inline$storm_IoCallDriver$1$label_36#1

+    stack_overflow.bpl(88224,3): inline$storm_IoCallDriver$1$label_1#1

+    stack_overflow.bpl(88246,3): inline$storm_PoCallDriver$0$anon2_Else#1

+    stack_overflow.bpl(88271,3): inline$BDLCallLowerLevelDriverAndWait$0$anon22_Else#1

+    stack_overflow.bpl(88285,3): inline$BDLCallLowerLevelDriverAndWait$0$label_29_false#1

+    stack_overflow.bpl(88443,3): inline$BDLCallLowerLevelDriverAndWait$0$label_30#1

+    stack_overflow.bpl(88486,3): inline$BDLPnPStart$0$anon39_Else#1

+    stack_overflow.bpl(88677,3): inline$BDLPnPStart$0$label_37_true#1

+    stack_overflow.bpl(88989,3): inline$BDLPnPStart$0$label_51_true#1

+    stack_overflow.bpl(89017,3): inline$BDLPnPStart$0$anon41_Else#1

+    stack_overflow.bpl(89031,3): inline$BDLPnPStart$0$label_56_true#1

+    stack_overflow.bpl(89075,3): inline$BDLPnPStart$0$anon42_Else#1

+    stack_overflow.bpl(89089,3): inline$BDLPnPStart$0$label_66_true#1

+    stack_overflow.bpl(89133,3): inline$BDLPnPStart$0$anon43_Else#1

+    stack_overflow.bpl(89147,3): inline$BDLPnPStart$0$label_76_true#1

+    stack_overflow.bpl(89178,3): inline$BDLPnPStart$0$anon44_Else#1

+    stack_overflow.bpl(89192,3): inline$BDLPnPStart$0$label_81_true#1

+    stack_overflow.bpl(89236,3): inline$BDLPnPStart$0$anon45_Else#1

+    stack_overflow.bpl(89250,3): inline$BDLPnPStart$0$label_91_true#1

+    stack_overflow.bpl(89294,3): inline$BDLPnPStart$0$anon46_Else#1

+    stack_overflow.bpl(89308,3): inline$BDLPnPStart$0$label_101_true#1

+    stack_overflow.bpl(89315,3): inline$BDLPnPStart$0$label_102#1

+    stack_overflow.bpl(89370,3): inline$BDLPnP$0$anon67_Else#1

+    stack_overflow.bpl(94595,3): inline$BDLPnP$0$label_139_true#1

+    stack_overflow.bpl(94624,3): inline$storm_IoCompleteRequest$57$label_6_true#1

+    stack_overflow.bpl(94632,3): inline$storm_IoCompleteRequest$57$anon3_Else#1

+    stack_overflow.bpl(94644,3): inline$storm_IoCompleteRequest$57$label_9_false#1

+    stack_overflow.bpl(94664,3): inline$storm_IoCompleteRequest$57$label_1#1

+    stack_overflow.bpl(94712,3): inline$BDLPnP$0$anon75_Then#1

+    stack_overflow.bpl(95228,3): inline$storm_thread_dispatch$0$anon5_Then#1

+    stack_overflow.bpl(95236,3): inline$storm_thread_dispatch$0$Return#1

+    stack_overflow.bpl(95296,3): inline$storm_IoCancelIrp$0$anon9_Then#1

+    stack_overflow.bpl(95301,3): inline$storm_IoCancelIrp$0$anon1#1

+    stack_overflow.bpl(95358,3): inline$storm_IoAcquireCancelSpinLock$0$anon4_Then#1

+    stack_overflow.bpl(95520,3): inline$storm_IoCancelIrp$0$anon10_Then#1

+    stack_overflow.bpl(95541,3): inline$storm_thread_cancel$0$anon2_Then#1

+    stack_overflow.bpl(95545,3): inline$storm_thread_cancel$0$Return#1

+    stack_overflow.bpl(97933,3): inline$storm_thread_completion$0$anon4_Then#1

+    stack_overflow.bpl(97937,3): inline$storm_thread_completion$0$Return#1

 

 Boogie program verifier finished with 0 verified, 1 error

 

diff --git a/Test/livevars/NestedOneDimensionalMap.bpl b/Test/livevars/NestedOneDimensionalMap.bpl
index 411316ac..23667a6f 100644
--- a/Test/livevars/NestedOneDimensionalMap.bpl
+++ b/Test/livevars/NestedOneDimensionalMap.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -useArrayTheory %s > %t

+// RUN: %diff %s.expect %t

 var k: int;

 var AllMaps__1: [int][int]int;

 

diff --git a/Test/livevars/NestedOneDimensionalMap.bpl.expect b/Test/livevars/NestedOneDimensionalMap.bpl.expect
new file mode 100644
index 00000000..37fad75c
--- /dev/null
+++ b/Test/livevars/NestedOneDimensionalMap.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/livevars/TwoDimensionalMap.bpl b/Test/livevars/TwoDimensionalMap.bpl
index 25e24b23..9bf99e88 100644
--- a/Test/livevars/TwoDimensionalMap.bpl
+++ b/Test/livevars/TwoDimensionalMap.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -useArrayTheory %s > %t

+// RUN: %diff %s.expect %t

 var k: int;

 var AllMaps__1: [int,int]int;

 

diff --git a/Test/livevars/TwoDimensionalMap.bpl.expect b/Test/livevars/TwoDimensionalMap.bpl.expect
new file mode 100644
index 00000000..37fad75c
--- /dev/null
+++ b/Test/livevars/TwoDimensionalMap.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/livevars/bla1.bpl b/Test/livevars/bla1.bpl
index 12ccc44a..97ae746a 100644
--- a/Test/livevars/bla1.bpl
+++ b/Test/livevars/bla1.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -useArrayTheory %s > %t

+// RUN: %diff %s.expect %t

 var __storm_thread_done_0 : bool;

 var __storm_thread_done_1 : bool;

 var __storm_thread_done_2 : bool;

diff --git a/Test/livevars/bla1.bpl.expect b/Test/livevars/bla1.bpl.expect
new file mode 100644
index 00000000..cc392841
--- /dev/null
+++ b/Test/livevars/bla1.bpl.expect
@@ -0,0 +1,71 @@
+bla1.bpl(2097,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    bla1.bpl(751,3): start#1
+    bla1.bpl(791,3): anon10_Then#1
+    bla1.bpl(796,3): anon2#1
+    bla1.bpl(824,3): inline$storm_IoAllocateIrp$0$label_8_case_1#1
+    bla1.bpl(856,3): inline$storm_IoAllocateIrp$0$anon14_Then#1
+    bla1.bpl(861,3): inline$storm_IoAllocateIrp$0$anon2#1
+    bla1.bpl(881,3): inline$storm_IoAllocateIrp$0$anon16_Then#1
+    bla1.bpl(886,3): inline$storm_IoAllocateIrp$0$anon5#1
+    bla1.bpl(906,3): inline$storm_IoAllocateIrp$0$anon18_Then#1
+    bla1.bpl(911,3): inline$storm_IoAllocateIrp$0$anon8#1
+    bla1.bpl(947,3): inline$storm_IoAllocateIrp$0$anon20_Then#1
+    bla1.bpl(952,3): inline$storm_IoAllocateIrp$0$anon11#1
+    bla1.bpl(983,3): inline$IoGetNextIrpStackLocation$0$anon3_Then#1
+    bla1.bpl(988,3): inline$IoGetNextIrpStackLocation$0$anon2#1
+    bla1.bpl(1020,3): inline$storm_IoAllocateIrp$0$anon22_Then#1
+    bla1.bpl(1025,3): inline$storm_IoAllocateIrp$0$anon13#1
+    bla1.bpl(1037,3): inline$storm_IoAllocateIrp$0$label_36#1
+    bla1.bpl(1091,3): inline$IoSetNextIrpStackLocation$0$anon6_Then#1
+    bla1.bpl(1096,3): inline$IoSetNextIrpStackLocation$0$anon2#1
+    bla1.bpl(1114,3): inline$IoSetNextIrpStackLocation$0$anon8_Then#1
+    bla1.bpl(1119,3): inline$IoSetNextIrpStackLocation$0$anon5#1
+    bla1.bpl(1159,3): inline$IoGetCurrentIrpStackLocation$0$anon3_Then#1
+    bla1.bpl(1164,3): inline$IoGetCurrentIrpStackLocation$0$anon2#1
+    bla1.bpl(1199,3): anon12_Then#1
+    bla1.bpl(1204,3): anon5#1
+    bla1.bpl(1257,3): inline$IoGetCurrentIrpStackLocation$1$anon3_Then#1
+    bla1.bpl(1261,3): inline$IoGetCurrentIrpStackLocation$1$anon2#1
+    bla1.bpl(1310,3): inline$I8xDeviceControl$0$anon3_Then#1
+    bla1.bpl(1314,3): inline$I8xDeviceControl$0$anon2#1
+    bla1.bpl(1350,3): inline$I8xKeyboardGetSysButtonEvent$0$label_9_false#1
+    bla1.bpl(1378,3): inline$storm_IoSetCancelRoutine$0$label_7_false#1
+    bla1.bpl(1429,3): inline$storm_IoSetCancelRoutine$0$anon9_Then#1
+    bla1.bpl(1433,3): inline$storm_IoSetCancelRoutine$0$anon3#1
+    bla1.bpl(1453,3): inline$storm_IoSetCancelRoutine$0$anon11_Then#1
+    bla1.bpl(1458,3): inline$storm_IoSetCancelRoutine$0$anon6#1
+    bla1.bpl(1469,3): inline$storm_IoSetCancelRoutine$0$anon13_Then#1
+    bla1.bpl(1474,3): inline$storm_IoSetCancelRoutine$0$anon8#1
+    bla1.bpl(1526,3): inline$I8xKeyboardGetSysButtonEvent$0$anon6_Else#1
+    bla1.bpl(1534,3): inline$I8xKeyboardGetSysButtonEvent$0$anon7_Then#1
+    bla1.bpl(1544,3): inline$I8xKeyboardGetSysButtonEvent$0$anon2#1
+    bla1.bpl(1568,3): inline$I8xKeyboardGetSysButtonEvent$0$label_23_true#1
+    bla1.bpl(1588,3): inline$I8xKeyboardGetSysButtonEvent$0$label_13_true#1
+    bla1.bpl(1621,3): inline$storm_IoCompleteRequest$0$label_6_false#1
+    bla1.bpl(1656,3): inline$storm_IoCompleteRequest$0$anon4_Else#1
+    bla1.bpl(1664,3): inline$storm_IoCompleteRequest$0$anon5_Then#1
+    bla1.bpl(1674,3): inline$storm_IoCompleteRequest$0$anon2#1
+    bla1.bpl(1678,3): inline$storm_IoCompleteRequest$0$label_1#1
+    bla1.bpl(1736,3): anon14_Then#1
+    bla1.bpl(1741,3): anon7#1
+    bla1.bpl(1798,3): inline$storm_IoCancelIrp$0$anon12_Then#1
+    bla1.bpl(1803,3): inline$storm_IoCancelIrp$0$anon2#1
+    bla1.bpl(1827,3): inline$storm_IoCancelIrp$0$anon14_Then#1
+    bla1.bpl(1832,3): inline$storm_IoCancelIrp$0$anon5#1
+    bla1.bpl(1853,3): inline$storm_IoCancelIrp$0$anon16_Then#1
+    bla1.bpl(1858,3): inline$storm_IoCancelIrp$0$anon8#1
+    bla1.bpl(1869,3): inline$storm_IoCancelIrp$0$anon18_Then#1
+    bla1.bpl(1874,3): inline$storm_IoCancelIrp$0$anon10#1
+    bla1.bpl(1934,3): inline$storm_IoAcquireCancelSpinLock$0$label_11_true#1
+    bla1.bpl(1962,3): inline$storm_IoAcquireCancelSpinLock$0$anon6_Then#1
+    bla1.bpl(1967,3): inline$storm_IoAcquireCancelSpinLock$0$anon3#1
+    bla1.bpl(1978,3): inline$storm_IoAcquireCancelSpinLock$0$anon8_Then#1
+    bla1.bpl(1983,3): inline$storm_IoAcquireCancelSpinLock$0$anon5#1
+    bla1.bpl(2007,3): inline$storm_IoCancelIrp$0$label_16_true#1
+    bla1.bpl(2025,3): inline$storm_IoCancelIrp$0$label_22_true#1
+    bla1.bpl(2038,3): inline$storm_IoCancelIrp$0$label_25_false#1
+    bla1.bpl(2078,3): anon15_Then#1
+    bla1.bpl(2083,3): anon9#1
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/livevars/daytona_bug2_ioctl_example_1.bpl b/Test/livevars/daytona_bug2_ioctl_example_1.bpl
index ae8ff08c..ee71af7c 100644
--- a/Test/livevars/daytona_bug2_ioctl_example_1.bpl
+++ b/Test/livevars/daytona_bug2_ioctl_example_1.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -useArrayTheory %s > %t

+// RUN: %diff %s.expect %t

 var __storm_thread_done_0 : bool;

 var __storm_thread_done_1 : bool;

 var __storm_thread_done_2 : bool;

diff --git a/Test/livevars/daytona_bug2_ioctl_example_1.bpl.expect b/Test/livevars/daytona_bug2_ioctl_example_1.bpl.expect
new file mode 100644
index 00000000..37fad75c
--- /dev/null
+++ b/Test/livevars/daytona_bug2_ioctl_example_1.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/livevars/daytona_bug2_ioctl_example_2.bpl b/Test/livevars/daytona_bug2_ioctl_example_2.bpl
index 44e51827..3ef1e332 100644
--- a/Test/livevars/daytona_bug2_ioctl_example_2.bpl
+++ b/Test/livevars/daytona_bug2_ioctl_example_2.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -useArrayTheory %s > %t

+// RUN: %diff %s.expect %t

 var __storm_thread_done_0 : bool;

 var __storm_thread_done_1 : bool;

 var __storm_thread_done_2 : bool;

diff --git a/Test/livevars/daytona_bug2_ioctl_example_2.bpl.expect b/Test/livevars/daytona_bug2_ioctl_example_2.bpl.expect
new file mode 100644
index 00000000..3c0d0b20
--- /dev/null
+++ b/Test/livevars/daytona_bug2_ioctl_example_2.bpl.expect
@@ -0,0 +1,148 @@
+daytona_bug2_ioctl_example_2.bpl(4835,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    daytona_bug2_ioctl_example_2.bpl(807,3): start#2
+    daytona_bug2_ioctl_example_2.bpl(848,3): anon22_Then#2
+    daytona_bug2_ioctl_example_2.bpl(853,3): anon2#2
+    daytona_bug2_ioctl_example_2.bpl(881,3): inline$storm_IoAllocateIrp$0$label_8_case_1#2
+    daytona_bug2_ioctl_example_2.bpl(913,3): inline$storm_IoAllocateIrp$0$anon18_Then#2
+    daytona_bug2_ioctl_example_2.bpl(918,3): inline$storm_IoAllocateIrp$0$anon2#2
+    daytona_bug2_ioctl_example_2.bpl(938,3): inline$storm_IoAllocateIrp$0$anon20_Then#2
+    daytona_bug2_ioctl_example_2.bpl(943,3): inline$storm_IoAllocateIrp$0$anon5#2
+    daytona_bug2_ioctl_example_2.bpl(963,3): inline$storm_IoAllocateIrp$0$anon22_Then#2
+    daytona_bug2_ioctl_example_2.bpl(968,3): inline$storm_IoAllocateIrp$0$anon8#2
+    daytona_bug2_ioctl_example_2.bpl(976,3): inline$storm_IoAllocateIrp$0$anon24_Else#2
+    daytona_bug2_ioctl_example_2.bpl(1012,3): inline$storm_IoAllocateIrp$0$anon25_Then#2
+    daytona_bug2_ioctl_example_2.bpl(1017,3): inline$storm_IoAllocateIrp$0$anon13#2
+    daytona_bug2_ioctl_example_2.bpl(1048,3): inline$IoGetNextIrpStackLocation$0$anon3_Then#2
+    daytona_bug2_ioctl_example_2.bpl(1053,3): inline$IoGetNextIrpStackLocation$0$anon2#2
+    daytona_bug2_ioctl_example_2.bpl(1068,3): inline$storm_IoAllocateIrp$0$anon27_Else#2
+    daytona_bug2_ioctl_example_2.bpl(1092,3): inline$storm_IoAllocateIrp$0$anon28_Then#2
+    daytona_bug2_ioctl_example_2.bpl(1097,3): inline$storm_IoAllocateIrp$0$anon17#2
+    daytona_bug2_ioctl_example_2.bpl(1117,3): inline$storm_IoAllocateIrp$0$label_36#2
+    daytona_bug2_ioctl_example_2.bpl(1131,3): anon24_Else#2
+    daytona_bug2_ioctl_example_2.bpl(1146,3): anon25_Else#2
+    daytona_bug2_ioctl_example_2.bpl(1186,3): inline$IoSetNextIrpStackLocation$0$anon6_Then#2
+    daytona_bug2_ioctl_example_2.bpl(1191,3): inline$IoSetNextIrpStackLocation$0$anon2#2
+    daytona_bug2_ioctl_example_2.bpl(1209,3): inline$IoSetNextIrpStackLocation$0$anon8_Then#2
+    daytona_bug2_ioctl_example_2.bpl(1214,3): inline$IoSetNextIrpStackLocation$0$anon5#2
+    daytona_bug2_ioctl_example_2.bpl(1227,3): anon26_Else#2
+    daytona_bug2_ioctl_example_2.bpl(1261,3): inline$IoGetCurrentIrpStackLocation$0$anon3_Then#2
+    daytona_bug2_ioctl_example_2.bpl(1266,3): inline$IoGetCurrentIrpStackLocation$0$anon2#2
+    daytona_bug2_ioctl_example_2.bpl(1281,3): anon27_Else#2
+    daytona_bug2_ioctl_example_2.bpl(1308,3): anon28_Then#2
+    daytona_bug2_ioctl_example_2.bpl(1313,3): anon13#2
+    daytona_bug2_ioctl_example_2.bpl(1345,3): inline$myInitDriver$0$anon5_Then#2
+    daytona_bug2_ioctl_example_2.bpl(1350,3): inline$myInitDriver$0$anon2#2
+    daytona_bug2_ioctl_example_2.bpl(1385,3): inline$storm_KeInitializeSpinLock$0$anon3_Then#2
+    daytona_bug2_ioctl_example_2.bpl(1390,3): inline$storm_KeInitializeSpinLock$0$anon2#2
+    daytona_bug2_ioctl_example_2.bpl(1403,3): inline$myInitDriver$0$anon7_Else#2
+    daytona_bug2_ioctl_example_2.bpl(1424,3): anon30_Else#2
+    daytona_bug2_ioctl_example_2.bpl(1480,3): inline$IoGetCurrentIrpStackLocation$1$anon3_Then#2
+    daytona_bug2_ioctl_example_2.bpl(1484,3): inline$IoGetCurrentIrpStackLocation$1$anon2#2
+    daytona_bug2_ioctl_example_2.bpl(1497,3): inline$dispatch$0$anon4_Else#2
+    daytona_bug2_ioctl_example_2.bpl(1536,3): inline$I8xDeviceControl$0$anon13_Else#2
+    daytona_bug2_ioctl_example_2.bpl(1559,3): inline$I8xDeviceControl$0$anon14_Then#2
+    daytona_bug2_ioctl_example_2.bpl(1564,3): inline$I8xDeviceControl$0$anon4#2
+    daytona_bug2_ioctl_example_2.bpl(1577,3): inline$I8xDeviceControl$0$label_11_true#2
+    daytona_bug2_ioctl_example_2.bpl(1590,3): inline$I8xDeviceControl$0$label_13_true#2
+    daytona_bug2_ioctl_example_2.bpl(1598,3): inline$I8xDeviceControl$0$label_14_false#2
+    daytona_bug2_ioctl_example_2.bpl(1627,3): inline$IoGetCurrentIrpStackLocation$2$anon3_Then#2
+    daytona_bug2_ioctl_example_2.bpl(1631,3): inline$IoGetCurrentIrpStackLocation$2$anon2#2
+    daytona_bug2_ioctl_example_2.bpl(1644,3): inline$I8xDeviceControl$0$anon16_Else#2
+    daytona_bug2_ioctl_example_2.bpl(1657,3): inline$I8xDeviceControl$0$label_19_case_2#2
+    daytona_bug2_ioctl_example_2.bpl(1721,3): inline$IoGetCurrentIrpStackLocation$4$anon3_Then#2
+    daytona_bug2_ioctl_example_2.bpl(1725,3): inline$IoGetCurrentIrpStackLocation$4$anon2#2
+    daytona_bug2_ioctl_example_2.bpl(1738,3): inline$I8xKeyboardGetSysButtonEvent$0$anon34_Else#2
+    daytona_bug2_ioctl_example_2.bpl(1751,3): inline$I8xKeyboardGetSysButtonEvent$0$label_14_false#2
+    daytona_bug2_ioctl_example_2.bpl(1759,3): inline$I8xKeyboardGetSysButtonEvent$0$label_15_false#2
+    daytona_bug2_ioctl_example_2.bpl(1813,3): inline$storm_KeAcquireSpinLock$0$anon10_Else#2
+    daytona_bug2_ioctl_example_2.bpl(1837,3): inline$storm_KeAcquireSpinLock$0$label_13_true#2
+    daytona_bug2_ioctl_example_2.bpl(1845,3): inline$storm_KeAcquireSpinLock$0$anon11_Else#2
+    daytona_bug2_ioctl_example_2.bpl(1869,3): inline$storm_KeAcquireSpinLock$0$anon12_Then#2
+    daytona_bug2_ioctl_example_2.bpl(1874,3): inline$storm_KeAcquireSpinLock$0$anon7#2
+    daytona_bug2_ioctl_example_2.bpl(1885,3): inline$storm_KeAcquireSpinLock$0$anon14_Then#2
+    daytona_bug2_ioctl_example_2.bpl(1890,3): inline$storm_KeAcquireSpinLock$0$anon9#2
+    daytona_bug2_ioctl_example_2.bpl(1894,3): inline$storm_KeAcquireSpinLock$0$label_1#2
+    daytona_bug2_ioctl_example_2.bpl(1911,3): inline$I8xKeyboardGetSysButtonEvent$0$anon36_Else#2
+    daytona_bug2_ioctl_example_2.bpl(1922,3): inline$I8xKeyboardGetSysButtonEvent$0$label_56_false#2
+    daytona_bug2_ioctl_example_2.bpl(1953,3): inline$storm_IoSetCancelRoutine$0$label_7_false#2
+    daytona_bug2_ioctl_example_2.bpl(2012,3): inline$storm_IoSetCancelRoutine$0$anon12_Then#2
+    daytona_bug2_ioctl_example_2.bpl(2016,3): inline$storm_IoSetCancelRoutine$0$anon5#2
+    daytona_bug2_ioctl_example_2.bpl(2036,3): inline$storm_IoSetCancelRoutine$0$anon14_Then#2
+    daytona_bug2_ioctl_example_2.bpl(2041,3): inline$storm_IoSetCancelRoutine$0$anon8#2
+    daytona_bug2_ioctl_example_2.bpl(2052,3): inline$storm_IoSetCancelRoutine$0$anon16_Then#2
+    daytona_bug2_ioctl_example_2.bpl(2057,3): inline$storm_IoSetCancelRoutine$0$anon10#2
+    daytona_bug2_ioctl_example_2.bpl(2064,3): inline$storm_IoSetCancelRoutine$0$label_1#2
+    daytona_bug2_ioctl_example_2.bpl(2077,3): inline$I8xKeyboardGetSysButtonEvent$0$anon44_Else#2
+    daytona_bug2_ioctl_example_2.bpl(2202,3): inline$I8xKeyboardGetSysButtonEvent$0$anon45_Else#2
+    daytona_bug2_ioctl_example_2.bpl(2210,3): inline$I8xKeyboardGetSysButtonEvent$0$anon46_Then#2
+    daytona_bug2_ioctl_example_2.bpl(2220,3): inline$I8xKeyboardGetSysButtonEvent$0$anon24#2
+    daytona_bug2_ioctl_example_2.bpl(2248,3): inline$storm_IoSetCancelRoutine$1$label_7_false#2
+    daytona_bug2_ioctl_example_2.bpl(2295,3): inline$storm_IoSetCancelRoutine$1$anon12_Else#2
+    daytona_bug2_ioctl_example_2.bpl(2303,3): inline$storm_IoSetCancelRoutine$1$anon13_Then#2
+    daytona_bug2_ioctl_example_2.bpl(2313,3): inline$storm_IoSetCancelRoutine$1$anon5#2
+    daytona_bug2_ioctl_example_2.bpl(2321,3): inline$storm_IoSetCancelRoutine$1$anon14_Else#2
+    daytona_bug2_ioctl_example_2.bpl(2329,3): inline$storm_IoSetCancelRoutine$1$anon15_Then#2
+    daytona_bug2_ioctl_example_2.bpl(2339,3): inline$storm_IoSetCancelRoutine$1$anon8#2
+    daytona_bug2_ioctl_example_2.bpl(2350,3): inline$storm_IoSetCancelRoutine$1$anon16_Then#2
+    daytona_bug2_ioctl_example_2.bpl(2355,3): inline$storm_IoSetCancelRoutine$1$anon10#2
+    daytona_bug2_ioctl_example_2.bpl(2363,3): inline$storm_IoSetCancelRoutine$1$label_1#2
+    daytona_bug2_ioctl_example_2.bpl(2377,3): inline$I8xKeyboardGetSysButtonEvent$0$anon50_Else#2
+    daytona_bug2_ioctl_example_2.bpl(2387,3): inline$I8xKeyboardGetSysButtonEvent$0$label_72_false#2
+    daytona_bug2_ioctl_example_2.bpl(2409,3): inline$storm_IoMarkIrpPending$2$label_6_false#2
+    daytona_bug2_ioctl_example_2.bpl(2449,3): inline$storm_IoMarkIrpPending$2$label_1#2
+    daytona_bug2_ioctl_example_2.bpl(2462,3): inline$I8xKeyboardGetSysButtonEvent$0$anon51_Else#2
+    daytona_bug2_ioctl_example_2.bpl(2509,3): inline$I8xKeyboardGetSysButtonEvent$0$label_59#2
+    daytona_bug2_ioctl_example_2.bpl(2535,3): inline$storm_KeReleaseSpinLock$0$anon8_Else#2
+    daytona_bug2_ioctl_example_2.bpl(2576,3): inline$storm_KeReleaseSpinLock$0$label_11_true#2
+    daytona_bug2_ioctl_example_2.bpl(2583,3): inline$storm_KeReleaseSpinLock$0$anon9_Else#2
+    daytona_bug2_ioctl_example_2.bpl(2591,3): inline$storm_KeReleaseSpinLock$0$anon10_Then#2
+    daytona_bug2_ioctl_example_2.bpl(2601,3): inline$storm_KeReleaseSpinLock$0$anon5#2
+    daytona_bug2_ioctl_example_2.bpl(2612,3): inline$storm_KeReleaseSpinLock$0$anon11_Then#2
+    daytona_bug2_ioctl_example_2.bpl(2617,3): inline$storm_KeReleaseSpinLock$0$anon7#2
+    daytona_bug2_ioctl_example_2.bpl(2621,3): inline$storm_KeReleaseSpinLock$0$label_1#2
+    daytona_bug2_ioctl_example_2.bpl(2634,3): inline$I8xKeyboardGetSysButtonEvent$0$anon43_Else#2
+    daytona_bug2_ioctl_example_2.bpl(2867,3): inline$I8xKeyboardGetSysButtonEvent$0$label_51_true#2
+    daytona_bug2_ioctl_example_2.bpl(2910,3): inline$storm_IoCompleteRequest$2$label_6_false#2
+    daytona_bug2_ioctl_example_2.bpl(2953,3): inline$storm_IoCompleteRequest$2$anon6_Else#2
+    daytona_bug2_ioctl_example_2.bpl(2961,3): inline$storm_IoCompleteRequest$2$anon7_Then#2
+    daytona_bug2_ioctl_example_2.bpl(2971,3): inline$storm_IoCompleteRequest$2$anon2#2
+    daytona_bug2_ioctl_example_2.bpl(2975,3): inline$storm_IoCompleteRequest$2$label_1#2
+    daytona_bug2_ioctl_example_2.bpl(2988,3): inline$I8xCompleteSysButtonIrp$0$anon2_Else#2
+    daytona_bug2_ioctl_example_2.bpl(3008,3): inline$I8xKeyboardGetSysButtonEvent$0$anon42_Else#2
+    daytona_bug2_ioctl_example_2.bpl(3015,3): inline$I8xKeyboardGetSysButtonEvent$0$label_52#2
+    daytona_bug2_ioctl_example_2.bpl(3159,3): inline$I8xKeyboardGetSysButtonEvent$0$label_1#2
+    daytona_bug2_ioctl_example_2.bpl(3177,3): inline$I8xDeviceControl$0$anon18_Else#2
+    daytona_bug2_ioctl_example_2.bpl(3646,3): inline$I8xDeviceControl$0$label_1#2
+    daytona_bug2_ioctl_example_2.bpl(3663,3): inline$dispatch$0$anon5_Else#2
+    daytona_bug2_ioctl_example_2.bpl(3694,3): anon31_Then#2
+    daytona_bug2_ioctl_example_2.bpl(3699,3): anon17#2
+    daytona_bug2_ioctl_example_2.bpl(3756,3): inline$storm_IoCancelIrp$0$anon23_Then#2
+    daytona_bug2_ioctl_example_2.bpl(3761,3): inline$storm_IoCancelIrp$0$anon2#2
+    daytona_bug2_ioctl_example_2.bpl(3785,3): inline$storm_IoCancelIrp$0$anon25_Then#2
+    daytona_bug2_ioctl_example_2.bpl(3790,3): inline$storm_IoCancelIrp$0$anon5#2
+    daytona_bug2_ioctl_example_2.bpl(3811,3): inline$storm_IoCancelIrp$0$anon27_Then#2
+    daytona_bug2_ioctl_example_2.bpl(3816,3): inline$storm_IoCancelIrp$0$anon8#2
+    daytona_bug2_ioctl_example_2.bpl(3827,3): inline$storm_IoCancelIrp$0$anon29_Then#2
+    daytona_bug2_ioctl_example_2.bpl(3832,3): inline$storm_IoCancelIrp$0$anon10#2
+    daytona_bug2_ioctl_example_2.bpl(3892,3): inline$storm_IoAcquireCancelSpinLock$0$label_11_true#2
+    daytona_bug2_ioctl_example_2.bpl(3902,3): inline$storm_IoAcquireCancelSpinLock$0$anon8_Else#2
+    daytona_bug2_ioctl_example_2.bpl(3915,3): inline$storm_IoAcquireCancelSpinLock$0$anon9_Else#2
+    daytona_bug2_ioctl_example_2.bpl(3923,3): inline$storm_IoAcquireCancelSpinLock$0$anon10_Then#2
+    daytona_bug2_ioctl_example_2.bpl(3933,3): inline$storm_IoAcquireCancelSpinLock$0$anon5#2
+    daytona_bug2_ioctl_example_2.bpl(3944,3): inline$storm_IoAcquireCancelSpinLock$0$anon11_Then#2
+    daytona_bug2_ioctl_example_2.bpl(3949,3): inline$storm_IoAcquireCancelSpinLock$0$anon7#2
+    daytona_bug2_ioctl_example_2.bpl(3953,3): inline$storm_IoAcquireCancelSpinLock$0$label_1#2
+    daytona_bug2_ioctl_example_2.bpl(3966,3): inline$storm_IoCancelIrp$0$anon30_Else#2
+    daytona_bug2_ioctl_example_2.bpl(3984,3): inline$storm_IoCancelIrp$0$label_16_true#2
+    daytona_bug2_ioctl_example_2.bpl(4002,3): inline$storm_IoCancelIrp$0$label_22_true#2
+    daytona_bug2_ioctl_example_2.bpl(4010,3): inline$storm_IoCancelIrp$0$anon32_Else#2
+    daytona_bug2_ioctl_example_2.bpl(4023,3): inline$storm_IoCancelIrp$0$label_27_false#2
+    daytona_bug2_ioctl_example_2.bpl(4724,3): inline$storm_IoCancelIrp$0$label_1#2
+    daytona_bug2_ioctl_example_2.bpl(4759,3): inline$cancel$0$anon2_Then#2
+    daytona_bug2_ioctl_example_2.bpl(4773,3): anon32_Then#2
+    daytona_bug2_ioctl_example_2.bpl(4778,3): anon19#2
+    daytona_bug2_ioctl_example_2.bpl(4816,3): anon33_Then#2
+    daytona_bug2_ioctl_example_2.bpl(4821,3): anon21#2
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/livevars/stack_overflow.bpl b/Test/livevars/stack_overflow.bpl
index fae3e863..22ccd875 100644
--- a/Test/livevars/stack_overflow.bpl
+++ b/Test/livevars/stack_overflow.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -useArrayTheory %s > %t

+// RUN: %diff %s.expect %t

 

 var raiseException : bool;

 var errorReached : bool;

diff --git a/Test/livevars/stack_overflow.bpl.expect b/Test/livevars/stack_overflow.bpl.expect
new file mode 100644
index 00000000..10b3fa14
--- /dev/null
+++ b/Test/livevars/stack_overflow.bpl.expect
@@ -0,0 +1,150 @@
+stack_overflow.bpl(97944,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    stack_overflow.bpl(1143,3): start#1
+    stack_overflow.bpl(1199,3): inline$storm_IoAllocateIrp$0$label_8_case_1#1
+    stack_overflow.bpl(1232,3): inline$storm_IoAllocateIrp$0$anon6_Else#1
+    stack_overflow.bpl(1285,3): inline$IoGetNextIrpStackLocation$0$label_3_true#1
+    stack_overflow.bpl(1304,3): inline$storm_IoAllocateIrp$0$anon7_Else#1
+    stack_overflow.bpl(1323,3): inline$storm_IoAllocateIrp$0$anon8_Else#1
+    stack_overflow.bpl(1332,3): inline$storm_IoAllocateIrp$0$anon5#1
+    stack_overflow.bpl(1352,3): inline$storm_IoAllocateIrp$0$label_36#1
+    stack_overflow.bpl(1366,3): anon10_Else#1
+    stack_overflow.bpl(1381,3): anon11_Else#1
+    stack_overflow.bpl(1420,3): inline$IoSetNextIrpStackLocation$0$label_3_true#1
+    stack_overflow.bpl(1426,3): inline$IoSetNextIrpStackLocation$0$label_5#1
+    stack_overflow.bpl(1448,3): anon12_Else#1
+    stack_overflow.bpl(1488,3): inline$IoGetCurrentIrpStackLocation$0$label_3_true#1
+    stack_overflow.bpl(1509,3): anon13_Else#1
+    stack_overflow.bpl(1571,3): inline$myInitDriver$0$anon8_Else#1
+    stack_overflow.bpl(1607,3): inline$myInitDriver$0$anon9_Else#1
+    stack_overflow.bpl(1643,3): inline$myInitDriver$0$anon10_Else#1
+    stack_overflow.bpl(1679,3): inline$myInitDriver$0$anon11_Else#1
+    stack_overflow.bpl(1712,3): anon14_Else#1
+    stack_overflow.bpl(1775,3): inline$IoGetCurrentIrpStackLocation$1$label_3_true#1
+    stack_overflow.bpl(1796,3): inline$storm_thread_dispatch$0$anon4_Else#1
+    stack_overflow.bpl(1879,3): inline$BDLPnP$0$anon54_Else#1
+    stack_overflow.bpl(1893,3): inline$BDLPnP$0$label_16_true#1
+    stack_overflow.bpl(1937,3): inline$BDLPnP$0$anon55_Else#1
+    stack_overflow.bpl(1951,3): inline$BDLPnP$0$label_26_true#1
+    stack_overflow.bpl(1995,3): inline$BDLPnP$0$anon56_Else#1
+    stack_overflow.bpl(2009,3): inline$BDLPnP$0$label_36_true#1
+    stack_overflow.bpl(2054,3): inline$IoGetCurrentIrpStackLocation$2$label_3_true#1
+    stack_overflow.bpl(2075,3): inline$BDLPnP$0$anon57_Else#1
+    stack_overflow.bpl(2102,3): inline$BDLPnP$0$label_44_true#1
+    stack_overflow.bpl(2111,3): inline$BDLPnP$0$label_47#1
+    stack_overflow.bpl(2115,3): inline$BDLPnP$0$anon58_Else#1
+    stack_overflow.bpl(2129,3): inline$BDLPnP$0$label_51_false#1
+    stack_overflow.bpl(77684,3): inline$BDLPnP$0$label_52_case_1#1
+    stack_overflow.bpl(77744,3): inline$BDLPnPStart$0$anon36_Else#1
+    stack_overflow.bpl(77758,3): inline$BDLPnPStart$0$label_11_true#1
+    stack_overflow.bpl(77802,3): inline$BDLPnPStart$0$anon37_Else#1
+    stack_overflow.bpl(77816,3): inline$BDLPnPStart$0$label_21_true#1
+    stack_overflow.bpl(77860,3): inline$BDLPnPStart$0$anon38_Else#1
+    stack_overflow.bpl(77874,3): inline$BDLPnPStart$0$label_31_true#1
+    stack_overflow.bpl(77881,3): inline$BDLPnPStart$0$label_32#1
+    stack_overflow.bpl(77953,3): inline$IoGetCurrentIrpStackLocation$3$label_3_true#1
+    stack_overflow.bpl(77974,3): inline$IoCopyCurrentIrpStackLocationToNext$0$anon4_Else#1
+    stack_overflow.bpl(78015,3): inline$IoGetNextIrpStackLocation$1$label_3_true#1
+    stack_overflow.bpl(78034,3): inline$IoCopyCurrentIrpStackLocationToNext$0$anon5_Else#1
+    stack_overflow.bpl(78068,3): inline$BDLCallLowerLevelDriverAndWait$0$anon16_Else#1
+    stack_overflow.bpl(78102,3): inline$BDLCallLowerLevelDriverAndWait$0$anon17_Else#1
+    stack_overflow.bpl(78130,3): inline$storm_IoSetCompletionRoutine$0$label_7_false#1
+    stack_overflow.bpl(78200,3): inline$IoGetNextIrpStackLocation$2$label_3_true#1
+    stack_overflow.bpl(78219,3): inline$storm_IoSetCompletionRoutine$0$anon5_Else#1
+    stack_overflow.bpl(78235,3): inline$storm_IoSetCompletionRoutine$0$label_1#1
+    stack_overflow.bpl(78252,3): inline$BDLCallLowerLevelDriverAndWait$0$anon18_Else#1
+    stack_overflow.bpl(78292,3): inline$IoGetCurrentIrpStackLocation$4$label_3_true#1
+    stack_overflow.bpl(78313,3): inline$BDLCallLowerLevelDriverAndWait$0$anon19_Else#1
+    stack_overflow.bpl(83281,3): inline$BDLCallLowerLevelDriverAndWait$0$label_18_true#1
+    stack_overflow.bpl(83290,3): inline$BDLCallLowerLevelDriverAndWait$0$anon21_Else#1
+    stack_overflow.bpl(83335,3): inline$storm_IoCallDriver$1$label_9_false#1
+    stack_overflow.bpl(83405,3): inline$IoSetNextIrpStackLocation$2$label_3_true#1
+    stack_overflow.bpl(83411,3): inline$IoSetNextIrpStackLocation$2$label_5#1
+    stack_overflow.bpl(83433,3): inline$storm_IoCallDriver$1$anon11_Else#1
+    stack_overflow.bpl(83473,3): inline$IoGetCurrentIrpStackLocation$14$label_3_true#1
+    stack_overflow.bpl(83494,3): inline$storm_IoCallDriver$1$anon13_Else#1
+    stack_overflow.bpl(85861,3): inline$storm_IoCallDriver$1$label_27_case_1#1
+    stack_overflow.bpl(85931,3): inline$IoGetCurrentIrpStackLocation$19$label_3_true#1
+    stack_overflow.bpl(85952,3): inline$CallCompletionRoutine$3$anon10_Else#1
+    stack_overflow.bpl(86009,3): inline$IoGetCurrentIrpStackLocation$20$label_3_true#1
+    stack_overflow.bpl(86030,3): inline$CallCompletionRoutine$3$anon11_Else#1
+    stack_overflow.bpl(86047,3): inline$CallCompletionRoutine$3$label_18_true#1
+    stack_overflow.bpl(87164,3): inline$CallCompletionRoutine$3$label_20_icall_2#1
+    stack_overflow.bpl(87241,3): inline$IoGetCurrentIrpStackLocation$21$label_3_true#1
+    stack_overflow.bpl(87264,3): inline$BDLDevicePowerIoCompletion$3$anon30_Else#1
+    stack_overflow.bpl(87309,3): inline$BDLDevicePowerIoCompletion$3$anon31_Else#1
+    stack_overflow.bpl(87323,3): inline$BDLDevicePowerIoCompletion$3$label_20_true#1
+    stack_overflow.bpl(87367,3): inline$BDLDevicePowerIoCompletion$3$anon32_Else#1
+    stack_overflow.bpl(87381,3): inline$BDLDevicePowerIoCompletion$3$label_30_true#1
+    stack_overflow.bpl(87425,3): inline$BDLDevicePowerIoCompletion$3$anon33_Else#1
+    stack_overflow.bpl(87439,3): inline$BDLDevicePowerIoCompletion$3$label_40_true#1
+    stack_overflow.bpl(87454,3): inline$BDLDevicePowerIoCompletion$3$label_41_true#1
+    stack_overflow.bpl(87485,3): inline$BDLDevicePowerIoCompletion$3$label_44_true#1
+    stack_overflow.bpl(87529,3): inline$BDLDevicePowerIoCompletion$3$label_55_true#1
+    stack_overflow.bpl(87557,3): inline$BDLDevicePowerIoCompletion$3$anon35_Else#1
+    stack_overflow.bpl(87571,3): inline$BDLDevicePowerIoCompletion$3$label_62_true#1
+    stack_overflow.bpl(87615,3): inline$BDLDevicePowerIoCompletion$3$anon36_Else#1
+    stack_overflow.bpl(87629,3): inline$BDLDevicePowerIoCompletion$3$label_72_true#1
+    stack_overflow.bpl(87673,3): inline$BDLDevicePowerIoCompletion$3$anon37_Else#1
+    stack_overflow.bpl(87687,3): inline$BDLDevicePowerIoCompletion$3$label_82_true#1
+    stack_overflow.bpl(87694,3): inline$BDLDevicePowerIoCompletion$3$label_83#1
+    stack_overflow.bpl(87700,3): inline$BDLDevicePowerIoCompletion$3$label_86#1
+    stack_overflow.bpl(87704,3): inline$BDLDevicePowerIoCompletion$3$anon38_Else#1
+    stack_overflow.bpl(87715,3): inline$BDLDevicePowerIoCompletion$3$anon39_Else#1
+    stack_overflow.bpl(87740,3): inline$storm_IoCompleteRequest$7$label_6_false#1
+    stack_overflow.bpl(87779,3): inline$storm_IoCompleteRequest$7$label_7#1
+    stack_overflow.bpl(87784,3): inline$storm_IoCompleteRequest$7$label_1#1
+    stack_overflow.bpl(87797,3): inline$BDLDevicePowerIoCompletion$3$anon40_Else#1
+    stack_overflow.bpl(87808,3): inline$BDLDevicePowerIoCompletion$3$anon41_Else#1
+    stack_overflow.bpl(87839,3): inline$BDLDevicePowerIoCompletion$3$anon42_Else#1
+    stack_overflow.bpl(87853,3): inline$BDLDevicePowerIoCompletion$3$label_101_true#1
+    stack_overflow.bpl(87897,3): inline$BDLDevicePowerIoCompletion$3$anon43_Else#1
+    stack_overflow.bpl(87911,3): inline$BDLDevicePowerIoCompletion$3$label_111_true#1
+    stack_overflow.bpl(87955,3): inline$BDLDevicePowerIoCompletion$3$anon44_Else#1
+    stack_overflow.bpl(87969,3): inline$BDLDevicePowerIoCompletion$3$label_121_true#1
+    stack_overflow.bpl(87976,3): inline$BDLDevicePowerIoCompletion$3$label_122#1
+    stack_overflow.bpl(88048,3): inline$CallCompletionRoutine$3$anon13_Else#1
+    stack_overflow.bpl(88162,3): inline$CallCompletionRoutine$3$label_24_true#1
+    stack_overflow.bpl(88171,3): inline$CallCompletionRoutine$3$label_1#1
+    stack_overflow.bpl(88192,3): inline$storm_IoCallDriver$1$anon15_Else#1
+    stack_overflow.bpl(88220,3): inline$storm_IoCallDriver$1$label_36#1
+    stack_overflow.bpl(88224,3): inline$storm_IoCallDriver$1$label_1#1
+    stack_overflow.bpl(88246,3): inline$storm_PoCallDriver$0$anon2_Else#1
+    stack_overflow.bpl(88271,3): inline$BDLCallLowerLevelDriverAndWait$0$anon22_Else#1
+    stack_overflow.bpl(88285,3): inline$BDLCallLowerLevelDriverAndWait$0$label_29_false#1
+    stack_overflow.bpl(88443,3): inline$BDLCallLowerLevelDriverAndWait$0$label_30#1
+    stack_overflow.bpl(88486,3): inline$BDLPnPStart$0$anon39_Else#1
+    stack_overflow.bpl(88677,3): inline$BDLPnPStart$0$label_37_true#1
+    stack_overflow.bpl(88989,3): inline$BDLPnPStart$0$label_51_true#1
+    stack_overflow.bpl(89017,3): inline$BDLPnPStart$0$anon41_Else#1
+    stack_overflow.bpl(89031,3): inline$BDLPnPStart$0$label_56_true#1
+    stack_overflow.bpl(89075,3): inline$BDLPnPStart$0$anon42_Else#1
+    stack_overflow.bpl(89089,3): inline$BDLPnPStart$0$label_66_true#1
+    stack_overflow.bpl(89133,3): inline$BDLPnPStart$0$anon43_Else#1
+    stack_overflow.bpl(89147,3): inline$BDLPnPStart$0$label_76_true#1
+    stack_overflow.bpl(89178,3): inline$BDLPnPStart$0$anon44_Else#1
+    stack_overflow.bpl(89192,3): inline$BDLPnPStart$0$label_81_true#1
+    stack_overflow.bpl(89236,3): inline$BDLPnPStart$0$anon45_Else#1
+    stack_overflow.bpl(89250,3): inline$BDLPnPStart$0$label_91_true#1
+    stack_overflow.bpl(89294,3): inline$BDLPnPStart$0$anon46_Else#1
+    stack_overflow.bpl(89308,3): inline$BDLPnPStart$0$label_101_true#1
+    stack_overflow.bpl(89315,3): inline$BDLPnPStart$0$label_102#1
+    stack_overflow.bpl(89370,3): inline$BDLPnP$0$anon67_Else#1
+    stack_overflow.bpl(94595,3): inline$BDLPnP$0$label_139_true#1
+    stack_overflow.bpl(94624,3): inline$storm_IoCompleteRequest$57$label_6_true#1
+    stack_overflow.bpl(94632,3): inline$storm_IoCompleteRequest$57$anon3_Else#1
+    stack_overflow.bpl(94644,3): inline$storm_IoCompleteRequest$57$label_9_false#1
+    stack_overflow.bpl(94664,3): inline$storm_IoCompleteRequest$57$label_1#1
+    stack_overflow.bpl(94712,3): inline$BDLPnP$0$anon75_Then#1
+    stack_overflow.bpl(95228,3): inline$storm_thread_dispatch$0$anon5_Then#1
+    stack_overflow.bpl(95236,3): inline$storm_thread_dispatch$0$Return#1
+    stack_overflow.bpl(95296,3): inline$storm_IoCancelIrp$0$anon9_Then#1
+    stack_overflow.bpl(95301,3): inline$storm_IoCancelIrp$0$anon1#1
+    stack_overflow.bpl(95358,3): inline$storm_IoAcquireCancelSpinLock$0$anon4_Then#1
+    stack_overflow.bpl(95520,3): inline$storm_IoCancelIrp$0$anon10_Then#1
+    stack_overflow.bpl(95541,3): inline$storm_thread_cancel$0$anon2_Then#1
+    stack_overflow.bpl(95545,3): inline$storm_thread_cancel$0$Return#1
+    stack_overflow.bpl(97933,3): inline$storm_thread_completion$0$anon4_Then#1
+    stack_overflow.bpl(97937,3): inline$storm_thread_completion$0$Return#1
+
+Boogie program verifier finished with 0 verified, 1 error