From 00b9ebe879d87859a10f6e7427a0d9e59ee50dcd Mon Sep 17 00:00:00 2001 From: Michael Emmi Date: Mon, 30 Dec 2019 16:42:11 -0500 Subject: [PATCH 1/3] Updating Z3 model_compress parameter. * Z3 4.8.7 consolidates model.compact and model_compress. --- Source/Provers/SMTLib/Z3.cs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs index 1689ed4bf..dd916cedb 100644 --- a/Source/Provers/SMTLib/Z3.cs +++ b/Source/Provers/SMTLib/Z3.cs @@ -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) From 262f43bad68c804309c127781c078fa4ad8cbe81 Mon Sep 17 00:00:00 2001 From: Michael Emmi Date: Tue, 31 Dec 2019 13:33:12 -0500 Subject: [PATCH 2/3] Udated to Z3 4.8.7. --- .travis.yml | 2 +- Test/aitest9/TestIntervals.bpl.expect | 4 +- Test/extractloops/t3.bpl.rb4.expect | 4 - Test/livevars/bla1.bpl.expect | 15 +- Test/livevars/stack_overflow.bpl.expect | 184 +++++++++--------- Test/test15/CaptureState.bpl.expect | 6 +- Test/test15/ModelTest.bpl.expect | 3 + Test/test7/MultipleErrors.bpl.e1.dag.expect | 4 +- Test/test7/MultipleErrors.bpl.e1.local.expect | 4 +- Test/test7/MultipleErrors.bpl.e10.dag.expect | 2 +- 10 files changed, 112 insertions(+), 116 deletions(-) diff --git a/.travis.yml b/.travis.yml index f56def253..f87da52f7 100644 --- a/.travis.yml +++ b/.travis.yml @@ -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 diff --git a/Test/aitest9/TestIntervals.bpl.expect b/Test/aitest9/TestIntervals.bpl.expect index b4b7175ee..f0d6824ed 100644 --- a/Test/aitest9/TestIntervals.bpl.expect +++ b/Test/aitest9/TestIntervals.bpl.expect @@ -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: diff --git a/Test/extractloops/t3.bpl.rb4.expect b/Test/extractloops/t3.bpl.rb4.expect index cdcdd0f24..d32af5c5f 100644 --- a/Test/extractloops/t3.bpl.rb4.expect +++ b/Test/extractloops/t3.bpl.rb4.expect @@ -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 diff --git a/Test/livevars/bla1.bpl.expect b/Test/livevars/bla1.bpl.expect index cc392841f..ac7a1b37a 100644 --- a/Test/livevars/bla1.bpl.expect +++ b/Test/livevars/bla1.bpl.expect @@ -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 @@ -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 diff --git a/Test/livevars/stack_overflow.bpl.expect b/Test/livevars/stack_overflow.bpl.expect index 10b3fa145..408c616c6 100644 --- a/Test/livevars/stack_overflow.bpl.expect +++ b/Test/livevars/stack_overflow.bpl.expect @@ -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 diff --git a/Test/test15/CaptureState.bpl.expect b/Test/test15/CaptureState.bpl.expect index 6a52f7705..7ba7640c8 100644 --- a/Test/test15/CaptureState.bpl.expect +++ b/Test/test15/CaptureState.bpl.expect @@ -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 @@ -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 @@ -44,7 +46,7 @@ tickleBool -> { r -> **r this -> T@Ref!val!0 x -> 40 - y -> **y + y -> 0 *** END_STATE *** STATE top *** END_STATE diff --git a/Test/test15/ModelTest.bpl.expect b/Test/test15/ModelTest.bpl.expect index d5fb154e2..992159933 100644 --- a/Test/test15/ModelTest.bpl.expect +++ b/Test/test15/ModelTest.bpl.expect @@ -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 diff --git a/Test/test7/MultipleErrors.bpl.e1.dag.expect b/Test/test7/MultipleErrors.bpl.e1.dag.expect index 73db2a211..00037e68c 100644 --- a/Test/test7/MultipleErrors.bpl.e1.dag.expect +++ b/Test/test7/MultipleErrors.bpl.e1.dag.expect @@ -1,6 +1,6 @@ -MultipleErrors.bpl(28,3): Error BP5001: This assertion might not hold. +MultipleErrors.bpl(32,3): Error BP5001: This assertion might not hold. Execution trace: MultipleErrors.bpl(24,1): start - MultipleErrors.bpl(27,1): A + MultipleErrors.bpl(31,1): B Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test7/MultipleErrors.bpl.e1.local.expect b/Test/test7/MultipleErrors.bpl.e1.local.expect index f4acb1008..617c87593 100644 --- a/Test/test7/MultipleErrors.bpl.e1.local.expect +++ b/Test/test7/MultipleErrors.bpl.e1.local.expect @@ -1,5 +1,5 @@ -MultipleErrors.bpl(32,3): Error BP5001: This assertion might not hold. +MultipleErrors.bpl(28,3): Error BP5001: This assertion might not hold. Execution trace: - MultipleErrors.bpl(31,1): B + MultipleErrors.bpl(27,1): A Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test7/MultipleErrors.bpl.e10.dag.expect b/Test/test7/MultipleErrors.bpl.e10.dag.expect index 5ac162dfe..493a0e3f1 100644 --- a/Test/test7/MultipleErrors.bpl.e10.dag.expect +++ b/Test/test7/MultipleErrors.bpl.e10.dag.expect @@ -9,7 +9,7 @@ Execution trace: MultipleErrors.bpl(36,3): Error BP5001: This assertion might not hold. Execution trace: MultipleErrors.bpl(24,1): start - MultipleErrors.bpl(27,1): A + MultipleErrors.bpl(31,1): B MultipleErrors.bpl(35,1): C Boogie program verifier finished with 0 verified, 3 errors From 8385b53a388f4c885bc84d6b4e39811dfbabf29b Mon Sep 17 00:00:00 2001 From: Michael Emmi Date: Tue, 31 Dec 2019 14:04:10 -0500 Subject: [PATCH 3/3] Adjusting Rlimitouts0 test for more efficient Z3. --- Test/test2/Rlimitouts0.bpl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Test/test2/Rlimitouts0.bpl b/Test/test2/Rlimitouts0.bpl index c48fe2c3d..b6934e8fd 100644 --- a/Test/test2/Rlimitouts0.bpl +++ b/Test/test2/Rlimitouts0.bpl @@ -34,7 +34,7 @@ procedure TestRlimit1(in: [int]int, len: int) returns (out: [int]int); requires 0 < len; ensures (forall j: int :: 0 <= j && j < len ==> out[j] == in[j]); -implementation {:rlimit 60000} TestRlimit1(in: [int]int, len: int) returns (out: [int]int) +implementation {:rlimit 6000000} TestRlimit1(in: [int]int, len: int) returns (out: [int]int) { var i : int;