Removed old test infrastructure files except for

./AbsHoudini/
./doomed/
./z3api/
./test17/

because their conversion to lit incomplete.

2 files changed, 0 insertions, 387 deletions

diff --git a/Test/livevars/Answer b/Test/livevars/Answer
deleted file mode 100644
index a7a77b7b..00000000
--- a/Test/livevars/Answer
+++ /dev/null
@@ -1,375 +0,0 @@
-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

-

-Boogie program verifier finished with 1 verified, 0 errors

-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

-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

-

-Boogie program verifier finished with 1 verified, 0 errors

-

-Boogie program verifier finished with 1 verified, 0 errors

diff --git a/Test/livevars/runtest.bat b/Test/livevars/runtest.bat
deleted file mode 100644
index dbd3cb8c..00000000
--- a/Test/livevars/runtest.bat
+++ /dev/null
@@ -1,12 +0,0 @@
-@echo off

-setlocal

-

-set BGEXE=..\..\Binaries\Boogie.exe

-rem set BGEXE=mono ..\..\Binaries\Boogie.exe

-

-%BGEXE% %* /noinfer /useArrayTheory bla1.bpl

-%BGEXE% %* /noinfer /useArrayTheory daytona_bug2_ioctl_example_1.bpl

-%BGEXE% %* /noinfer /useArrayTheory daytona_bug2_ioctl_example_2.bpl

-%BGEXE% %* /noinfer /useArrayTheory stack_overflow.bpl

-%BGEXE% %* /noinfer /useArrayTheory NestedOneDimensionalMap.bpl

-%BGEXE% %* /noinfer /useArrayTheory TwoDimensionalMap.bpl