Skip to content

Commit

Permalink
Merge pull request #186 from michael-emmi/z3-parameters
Browse files Browse the repository at this point in the history 
Updating Z3 model_compress parameter.
  • Loading branch information
@michael-emmi
michael-emmi authored Dec 31, 2019
2 parents 0376574 + 8385b53 commit c7f0ff4
Show file tree
Hide file tree
Showing 12 changed files with 114 additions and 118 deletions.
2 changes: 1 addition & 1 deletion .travis.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ git:
env:
global:
- SOLUTION=Source/Boogie-NetCore.sln
- Z3URL=https://github.com/Z3Prover/z3/releases/download/z3-4.8.4/z3-4.8.4.d6df51951f4c-x64-ubuntu-14.04.zip
- Z3URL=https://github.com/Z3Prover/z3/releases/download/z3-4.8.7/z3-4.8.7-x64-ubuntu-16.04.zip
jobs:
- CONFIGURATION=Debug
- CONFIGURATION=Release
Expand Down
2 changes: 1 addition & 1 deletion Source/Provers/SMTLib/Z3.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -291,7 +291,7 @@ public static void SetupOptions(SMTLibProverOptions options)

if (major > 4 || (major == 4 && minor >= 8)) {
// {:captureState} does not work with compressed models
options.AddWeakSmtOption("model_compress", "false");
options.AddWeakSmtOption("model.compact", "false");
}

if (options.TimeLimit > 0)
Expand Down
4 changes: 2 additions & 2 deletions Test/aitest9/TestIntervals.bpl.expect
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ Execution trace:
TestIntervals.bpl(7,5): anon0
TestIntervals.bpl(8,3): anon9_LoopHead
TestIntervals.bpl(14,14): anon10_Then
TestIntervals.bpl(15,14): anon11_Then
TestIntervals.bpl(16,14): anon12_Then
TestIntervals.bpl(15,3): anon11_Else
TestIntervals.bpl(16,3): anon12_Else
TestIntervals.bpl(19,5): anon8
TestIntervals.bpl(70,3): Error BP5001: This assertion might not hold.
Execution trace:
Expand Down
4 changes: 0 additions & 4 deletions Test/extractloops/t3.bpl.rb4.expect
View file
Original file line number Diff line number Diff line change
@@ -1,10 +1,6 @@
(0,0): Error BP5001: This assertion might not hold.
Execution trace:
t3.bpl(19,3): anon0
t3.bpl(24,3): anon3_LoopHead
Inlined call to procedure foo begins
t3.bpl(10,5): anon0
Inlined call to procedure foo ends
t3.bpl(28,3): anon3_LoopBody
t3.bpl(24,3): anon3_LoopHead
Inlined call to procedure foo begins
Expand Down
15 changes: 10 additions & 5 deletions Test/livevars/bla1.bpl.expect
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,9 +31,11 @@ Execution trace:
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(1417,3): inline$storm_IoSetCancelRoutine$0$anon9_Else#1
bla1.bpl(1425,3): inline$storm_IoSetCancelRoutine$0$anon10_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(1440,3): inline$storm_IoSetCancelRoutine$0$anon11_Else#1
bla1.bpl(1448,3): inline$storm_IoSetCancelRoutine$0$anon12_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
Expand All @@ -51,14 +53,17 @@ Execution trace:
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(1814,3): inline$storm_IoCancelIrp$0$anon14_Else#1
bla1.bpl(1822,3): inline$storm_IoCancelIrp$0$anon15_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(1840,3): inline$storm_IoCancelIrp$0$anon16_Else#1
bla1.bpl(1848,3): inline$storm_IoCancelIrp$0$anon17_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(1949,3): inline$storm_IoAcquireCancelSpinLock$0$anon6_Else#1
bla1.bpl(1957,3): inline$storm_IoAcquireCancelSpinLock$0$anon7_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
Expand Down
184 changes: 87 additions & 97 deletions Test/livevars/stack_overflow.bpl.expect
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,109 +27,99 @@ Execution trace:
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(2005,3): inline$BDLPnP$0$label_36_false#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(66448,3): inline$BDLPnP$0$label_52_case_2#1
stack_overflow.bpl(66497,3): inline$BDLPnPQueryRemove$0$anon22_Else#1
stack_overflow.bpl(66511,3): inline$BDLPnPQueryRemove$0$label_8_true#1
stack_overflow.bpl(66555,3): inline$BDLPnPQueryRemove$0$anon23_Else#1
stack_overflow.bpl(66569,3): inline$BDLPnPQueryRemove$0$label_18_true#1
stack_overflow.bpl(66613,3): inline$BDLPnPQueryRemove$0$anon24_Else#1
stack_overflow.bpl(66627,3): inline$BDLPnPQueryRemove$0$label_28_true#1
stack_overflow.bpl(66634,3): inline$BDLPnPQueryRemove$0$label_29#1
stack_overflow.bpl(66638,3): inline$BDLPnPQueryRemove$0$anon25_Else#1
stack_overflow.bpl(66648,3): inline$BDLPnPQueryRemove$0$label_33_false#1
stack_overflow.bpl(66725,3): inline$IoGetCurrentIrpStackLocation$23$label_3_true#1
stack_overflow.bpl(66746,3): inline$IoCopyCurrentIrpStackLocationToNext$1$anon4_Else#1
stack_overflow.bpl(66787,3): inline$IoGetNextIrpStackLocation$3$label_3_true#1
stack_overflow.bpl(66806,3): inline$IoCopyCurrentIrpStackLocationToNext$1$anon5_Else#1
stack_overflow.bpl(66840,3): inline$BDLCallLowerLevelDriverAndWait$1$anon16_Else#1
stack_overflow.bpl(66874,3): inline$BDLCallLowerLevelDriverAndWait$1$anon17_Else#1
stack_overflow.bpl(66902,3): inline$storm_IoSetCompletionRoutine$1$label_7_false#1
stack_overflow.bpl(66972,3): inline$IoGetNextIrpStackLocation$4$label_3_true#1
stack_overflow.bpl(66991,3): inline$storm_IoSetCompletionRoutine$1$anon5_Else#1
stack_overflow.bpl(67007,3): inline$storm_IoSetCompletionRoutine$1$label_1#1
stack_overflow.bpl(67024,3): inline$BDLCallLowerLevelDriverAndWait$1$anon18_Else#1
stack_overflow.bpl(67064,3): inline$IoGetCurrentIrpStackLocation$24$label_3_true#1
stack_overflow.bpl(67085,3): inline$BDLCallLowerLevelDriverAndWait$1$anon19_Else#1
stack_overflow.bpl(72053,3): inline$BDLCallLowerLevelDriverAndWait$1$label_18_true#1
stack_overflow.bpl(72062,3): inline$BDLCallLowerLevelDriverAndWait$1$anon21_Else#1
stack_overflow.bpl(72107,3): inline$storm_IoCallDriver$3$label_9_false#1
stack_overflow.bpl(72177,3): inline$IoSetNextIrpStackLocation$4$label_3_true#1
stack_overflow.bpl(72183,3): inline$IoSetNextIrpStackLocation$4$label_5#1
stack_overflow.bpl(72205,3): inline$storm_IoCallDriver$3$anon11_Else#1
stack_overflow.bpl(72245,3): inline$IoGetCurrentIrpStackLocation$34$label_3_true#1
stack_overflow.bpl(72266,3): inline$storm_IoCallDriver$3$anon13_Else#1
stack_overflow.bpl(74633,3): inline$storm_IoCallDriver$3$label_27_case_1#1
stack_overflow.bpl(74703,3): inline$IoGetCurrentIrpStackLocation$39$label_3_true#1
stack_overflow.bpl(74724,3): inline$CallCompletionRoutine$7$anon10_Else#1
stack_overflow.bpl(74781,3): inline$IoGetCurrentIrpStackLocation$40$label_3_true#1
stack_overflow.bpl(74802,3): inline$CallCompletionRoutine$7$anon11_Else#1
stack_overflow.bpl(74819,3): inline$CallCompletionRoutine$7$label_18_true#1
stack_overflow.bpl(75936,3): inline$CallCompletionRoutine$7$label_20_icall_2#1
stack_overflow.bpl(76013,3): inline$IoGetCurrentIrpStackLocation$41$label_3_true#1
stack_overflow.bpl(76036,3): inline$BDLDevicePowerIoCompletion$7$anon30_Else#1
stack_overflow.bpl(76081,3): inline$BDLDevicePowerIoCompletion$7$anon31_Else#1
stack_overflow.bpl(76095,3): inline$BDLDevicePowerIoCompletion$7$label_20_true#1
stack_overflow.bpl(76139,3): inline$BDLDevicePowerIoCompletion$7$anon32_Else#1
stack_overflow.bpl(76153,3): inline$BDLDevicePowerIoCompletion$7$label_30_true#1
stack_overflow.bpl(76197,3): inline$BDLDevicePowerIoCompletion$7$anon33_Else#1
stack_overflow.bpl(76211,3): inline$BDLDevicePowerIoCompletion$7$label_40_true#1
stack_overflow.bpl(76226,3): inline$BDLDevicePowerIoCompletion$7$label_41_true#1
stack_overflow.bpl(76257,3): inline$BDLDevicePowerIoCompletion$7$label_44_true#1
stack_overflow.bpl(76282,3): inline$BDLDevicePowerIoCompletion$7$label_55_false#1
stack_overflow.bpl(76290,3): inline$BDLDevicePowerIoCompletion$7$anon34_Else#1
stack_overflow.bpl(76466,3): inline$BDLDevicePowerIoCompletion$7$label_83#1
stack_overflow.bpl(76472,3): inline$BDLDevicePowerIoCompletion$7$label_86#1
stack_overflow.bpl(76476,3): inline$BDLDevicePowerIoCompletion$7$anon38_Else#1
stack_overflow.bpl(76487,3): inline$BDLDevicePowerIoCompletion$7$anon39_Else#1
stack_overflow.bpl(76512,3): inline$storm_IoCompleteRequest$15$label_6_false#1
stack_overflow.bpl(76551,3): inline$storm_IoCompleteRequest$15$label_7#1
stack_overflow.bpl(76556,3): inline$storm_IoCompleteRequest$15$label_1#1
stack_overflow.bpl(76569,3): inline$BDLDevicePowerIoCompletion$7$anon40_Else#1
stack_overflow.bpl(76580,3): inline$BDLDevicePowerIoCompletion$7$anon41_Else#1
stack_overflow.bpl(76611,3): inline$BDLDevicePowerIoCompletion$7$anon42_Else#1
stack_overflow.bpl(76625,3): inline$BDLDevicePowerIoCompletion$7$label_101_true#1
stack_overflow.bpl(76669,3): inline$BDLDevicePowerIoCompletion$7$anon43_Else#1
stack_overflow.bpl(76683,3): inline$BDLDevicePowerIoCompletion$7$label_111_true#1
stack_overflow.bpl(76727,3): inline$BDLDevicePowerIoCompletion$7$anon44_Else#1
stack_overflow.bpl(76741,3): inline$BDLDevicePowerIoCompletion$7$label_121_true#1
stack_overflow.bpl(76748,3): inline$BDLDevicePowerIoCompletion$7$label_122#1
stack_overflow.bpl(76820,3): inline$CallCompletionRoutine$7$anon13_Else#1
stack_overflow.bpl(76934,3): inline$CallCompletionRoutine$7$label_24_true#1
stack_overflow.bpl(76943,3): inline$CallCompletionRoutine$7$label_1#1
stack_overflow.bpl(76964,3): inline$storm_IoCallDriver$3$anon15_Else#1
stack_overflow.bpl(76992,3): inline$storm_IoCallDriver$3$label_36#1
stack_overflow.bpl(76996,3): inline$storm_IoCallDriver$3$label_1#1
stack_overflow.bpl(77018,3): inline$storm_PoCallDriver$1$anon2_Else#1
stack_overflow.bpl(77043,3): inline$BDLCallLowerLevelDriverAndWait$1$anon22_Else#1
stack_overflow.bpl(77057,3): inline$BDLCallLowerLevelDriverAndWait$1$label_29_false#1
stack_overflow.bpl(77215,3): inline$BDLCallLowerLevelDriverAndWait$1$label_30#1
stack_overflow.bpl(77258,3): inline$BDLPnPQueryRemove$0$anon26_Else#1
stack_overflow.bpl(77272,3): inline$BDLPnPQueryRemove$0$label_65_false#1
stack_overflow.bpl(77490,3): inline$BDLPnPQueryRemove$0$anon27_Else#1
stack_overflow.bpl(77504,3): inline$BDLPnPQueryRemove$0$label_41_true#1
stack_overflow.bpl(77548,3): inline$BDLPnPQueryRemove$0$anon28_Else#1
stack_overflow.bpl(77558,3): inline$BDLPnPQueryRemove$0$label_51_false#1
stack_overflow.bpl(77606,3): inline$BDLPnPQueryRemove$0$anon29_Else#1
stack_overflow.bpl(77616,3): inline$BDLPnPQueryRemove$0$label_61_false#1
stack_overflow.bpl(77627,3): inline$BDLPnPQueryRemove$0$label_62#1
stack_overflow.bpl(77669,3): inline$BDLPnP$0$anon68_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
Expand Down
6 changes: 4 additions & 2 deletions Test/test15/CaptureState.bpl.expect
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,7 @@ Execution trace:
*** MODEL
%lbl%@1 -> false
%lbl%+0 -> true
%lbl%+2 -> false
%lbl%+3 -> true
%lbl%+4 -> true
%lbl%+5 -> true
Expand All @@ -16,12 +17,13 @@ Heap -> |T@[Ref,FieldName]Int!val!0|
m -> **m
m@0 -> (- 8)
m@1 -> (- 7)
m@2 -> 0
m@3 -> (- 7)
r -> **r
r@0 -> (- 14)
this -> T@Ref!val!0
x -> 40
y -> **y
y -> 0
$mv_state -> {
4 0 -> true
4 1 -> true
Expand All @@ -44,7 +46,7 @@ tickleBool -> {
r -> **r
this -> T@Ref!val!0
x -> 40
y -> **y
y -> 0
*** END_STATE
*** STATE top
*** END_STATE
Expand Down
3 changes: 3 additions & 0 deletions Test/test15/ModelTest.bpl.expect
View file
Original file line number Diff line number Diff line change
@@ -1,11 +1,14 @@
*** MODEL
%lbl%@1 -> false
%lbl%@2 -> false
%lbl%+0 -> true
%lbl%+3 -> true
i@0 -> 1
j@0 -> 2
j@1 -> 3
j@2 -> 4
r -> T@ref!val!0
s -> T@ref!val!0
tickleBool -> {
false -> true
true -> true
Expand Down
Loading

0 comments on commit c7f0ff4

Please sign in to comment.