diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-06-29 16:56:29 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-06-29 16:56:29 -0700 |
| commit | 0796ae97021a8b93b939a6b89986449eb3ff605a (patch) | |
| tree | abc42d44560615f7ed487290cd6413e5c8880fbb /Test | |
| parent | efe732baac2d81573bdd220e41bffaedf1f9eab4 (diff) | |
| parent | b043af23c8ea53af582b0d59f557c150c0cfc1e6 (diff) | |
Merge
Diffstat (limited to 'Test')
42 files changed, 771 insertions, 82 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index e20f2253..d5107ecd 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -147,16 +147,16 @@ Execution trace: SmallTests.dfy(81,5): anon9_LoopHead
(0,0): anon9_LoopBody
(0,0): anon10_Then
-SmallTests.dfy(116,5): Error: call may violate caller's modifies clause
+SmallTests.dfy(116,5): Error: call may violate context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon4_Else
(0,0): anon3
-SmallTests.dfy(129,9): Error: call may violate caller's modifies clause
+SmallTests.dfy(129,9): Error: call may violate context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-SmallTests.dfy(131,9): Error: call may violate caller's modifies clause
+SmallTests.dfy(131,9): Error: call may violate context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon3_Else
@@ -458,7 +458,7 @@ ParseErrors.dfy(18,18): error: chaining not allowed from the previous operator 9 parse errors detected in ParseErrors.dfy
-------------------- Array.dfy --------------------
-Array.dfy(10,8): Error: assignment may update an array element not in the enclosing method's modifies clause
+Array.dfy(10,8): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon5_Then
@@ -473,13 +473,13 @@ Execution trace: Array.dfy(48,20): Error: assertion violation
Execution trace:
(0,0): anon0
-Array.dfy(56,8): Error: assignment may update an array element not in the enclosing method's modifies clause
+Array.dfy(56,8): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon5_Then
(0,0): anon2
(0,0): anon6_Then
-Array.dfy(63,8): Error: assignment may update an array element not in the enclosing method's modifies clause
+Array.dfy(63,8): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon5_Then
@@ -498,10 +498,10 @@ Execution trace: (0,0): anon7_Else
(0,0): anon8_Then
(0,0): anon9_Then
-Array.dfy(131,6): Error: assignment may update an array element not in the enclosing method's modifies clause
+Array.dfy(131,6): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
-Array.dfy(138,6): Error: assignment may update an array element not in the enclosing method's modifies clause
+Array.dfy(138,6): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
@@ -637,7 +637,7 @@ Basics.dfy(147,10): Error: target object may be null Execution trace:
(0,0): anon0
(0,0): anon3
-Basics.dfy(147,10): Error: assignment may update an object not in the enclosing method's modifies clause
+Basics.dfy(147,10): Error: assignment may update an object not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon3
@@ -1005,3 +1005,88 @@ RefinementErrors.dfy(42,9): Error: Refined class has a member with the same name RefinementErrors.dfy(12,10): Error: Refinement methods can only be declared in refinement classes: M
RefinementErrors.dfy(34,10): Error: Different number of output variables
6 resolution/type errors detected in RefinementErrors.dfy
+
+-------------------- LoopModifies.dfy --------------------
+LoopModifies.dfy(6,5): Error: assignment may update an array element not in the enclosing context's modifies clause
+Execution trace:
+ (0,0): anon0
+LoopModifies.dfy(17,8): Error: assignment may update an array element not in the enclosing context's modifies clause
+Execution trace:
+ (0,0): anon0
+ LoopModifies.dfy(14,4): anon9_LoopHead
+ (0,0): anon9_LoopBody
+ LoopModifies.dfy(14,4): anon10_Else
+ (0,0): anon5
+ LoopModifies.dfy(14,4): anon12_Else
+ (0,0): anon7
+LoopModifies.dfy(46,8): Error: assignment may update an array element not in the enclosing context's modifies clause
+Execution trace:
+ (0,0): anon0
+ LoopModifies.dfy(42,4): anon9_LoopHead
+ (0,0): anon9_LoopBody
+ LoopModifies.dfy(42,4): anon10_Else
+ (0,0): anon5
+ LoopModifies.dfy(42,4): anon12_Else
+ (0,0): anon7
+LoopModifies.dfy(61,8): Error: assignment may update an array element not in the enclosing context's modifies clause
+Execution trace:
+ (0,0): anon0
+ LoopModifies.dfy(57,4): anon9_LoopHead
+ (0,0): anon9_LoopBody
+ LoopModifies.dfy(57,4): anon10_Else
+ (0,0): anon5
+ LoopModifies.dfy(57,4): anon12_Else
+ (0,0): anon7
+LoopModifies.dfy(74,4): Error: loop modifies clause may violate context's modifies clause
+Execution trace:
+ (0,0): anon0
+LoopModifies.dfy(98,5): Error: assignment may update an array element not in the enclosing context's modifies clause
+Execution trace:
+ (0,0): anon0
+ LoopModifies.dfy(90,4): anon9_LoopHead
+ (0,0): anon9_LoopBody
+ LoopModifies.dfy(90,4): anon10_Else
+ (0,0): anon5
+ LoopModifies.dfy(90,4): anon12_Else
+ (0,0): anon7
+LoopModifies.dfy(146,5): Error: assignment may update an array element not in the enclosing context's modifies clause
+Execution trace:
+ (0,0): anon0
+ LoopModifies.dfy(134,4): anon17_LoopHead
+ (0,0): anon17_LoopBody
+ LoopModifies.dfy(134,4): anon18_Else
+ (0,0): anon5
+ LoopModifies.dfy(134,4): anon20_Else
+ (0,0): anon7
+ LoopModifies.dfy(139,7): anon21_LoopHead
+ (0,0): anon21_LoopBody
+ LoopModifies.dfy(139,7): anon22_Else
+ (0,0): anon12
+ LoopModifies.dfy(139,7): anon24_Else
+ (0,0): anon14
+LoopModifies.dfy(197,10): Error: assignment may update an array element not in the enclosing context's modifies clause
+Execution trace:
+ (0,0): anon0
+ LoopModifies.dfy(193,4): anon9_LoopHead
+ (0,0): anon9_LoopBody
+ LoopModifies.dfy(193,4): anon10_Else
+ (0,0): anon5
+ LoopModifies.dfy(193,4): anon12_Else
+ (0,0): anon7
+LoopModifies.dfy(260,10): Error: assignment may update an array element not in the enclosing context's modifies clause
+Execution trace:
+ (0,0): anon0
+ LoopModifies.dfy(248,4): anon17_LoopHead
+ (0,0): anon17_LoopBody
+ LoopModifies.dfy(248,4): anon18_Else
+ (0,0): anon5
+ LoopModifies.dfy(248,4): anon20_Else
+ (0,0): anon7
+ LoopModifies.dfy(256,7): anon21_LoopHead
+ (0,0): anon21_LoopBody
+ LoopModifies.dfy(256,7): anon22_Else
+ (0,0): anon12
+ LoopModifies.dfy(256,7): anon24_Else
+ (0,0): anon14
+
+Dafny program verifier finished with 21 verified, 9 errors
diff --git a/Test/dafny0/LoopModifies.dfy b/Test/dafny0/LoopModifies.dfy new file mode 100644 index 00000000..17a4228e --- /dev/null +++ b/Test/dafny0/LoopModifies.dfy @@ -0,0 +1,293 @@ +
+// regular modifies sanity test:
+method Testing1(a: array<int>)
+ requires a != null && a.Length > 0;
+{
+ a[0] := 0;
+}
+
+// array inside while loop, without explict modifies clause:
+method Testing2(a: array<int>)
+ requires a != null && a.Length > 0;
+{
+ var i := 0;
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ {
+ a[0] := i;
+ i := i + 1;
+ }
+}
+
+// array inside while loop, without explict modifies clause:
+method Testing2A(a: array<int>)
+ requires a != null && a.Length > 0;
+ modifies a;
+{
+ var i := 0;
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ {
+ // now there is no problem.
+ a[0] := i;
+ i := i + 1;
+ }
+}
+
+// array inside while loop, with explict modifies clause:
+method Testing3(a: array<int>)
+ requires a != null && a.Length > 0;
+{
+ var i := 0;
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ modifies;
+ {
+ a[0] := i;
+ i := i + 1;
+ }
+}
+
+// modifies restricts:
+method Testing4(a: array<int>)
+ requires a != null && a.Length > 0;
+ modifies a;
+{
+ var i := 0;
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ modifies;
+ {
+ a[0] := i;
+ i := i + 1;
+ }
+ // should be ok.
+ a[0] := 1;
+}
+
+// modifies not a subset:
+method Testing5(a: array<int>)
+ requires a != null && a.Length > 0;
+ modifies;
+{
+ var i := 0;
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ modifies a;
+ {
+ a[0] := i;
+ i := i + 1;
+ }
+}
+
+// modifies is a subset, but modifications occur outside:
+method Testing6(a: array<int>, b: array<int>)
+ requires a != null && a.Length > 0;
+ requires b != null && b.Length > 0;
+ modifies a, b;
+{
+ var i := 0;
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ modifies a;
+ {
+ // cool.
+ a[0] := i;
+
+ // not cool.
+ b[0] := i;
+ i := i + 1;
+ }
+}
+
+// heap outside modifies is actually preserved:
+method Testing7(a: array<int>, b: array<int>)
+ requires a != null && a.Length > 0;
+ requires b != null && b.Length > 0;
+ requires a != b;
+ modifies a, b;
+{
+ var i := 0;
+ b[0] := 4;
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ modifies a;
+ {
+ // still good.
+ a[0] := i;
+ i := i + 1;
+ }
+ // this is new, and good:
+ assert b[0] == 4;
+}
+
+// modifies actually restrict frame when nested:
+method Testing8(a: array<int>, b: array<int>, c: array<int>)
+ requires a != null && a.Length > 0;
+ requires b != null && b.Length > 0;
+ requires c != null && c.Length > 0;
+ requires a != b && b != c && c != a;
+ modifies a, b, c;
+{
+ var i := 0;
+ b[0] := 4;
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ modifies a, b;
+ {
+ var j := 0;
+ while(j < 10)
+ invariant 0 <= j <= 10;
+ modifies a;
+ {
+ // happy:
+ a[0] := j;
+ // not happy:
+ b[0] := i;
+ j := j + 1;
+ }
+ i := i + 1;
+ }
+ c[0] := 1;
+}
+
+// heap outside modifies preserved when nested:
+method Testing9(a: array<int>, b: array<int>, c: array<int>)
+ requires a != null && a.Length > 0;
+ requires b != null && b.Length > 0;
+ requires c != null && c.Length > 0;
+ requires a != b && b != c && c != a;
+ modifies a, b, c;
+{
+ var i := 0;
+ b[0] := 4;
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ modifies a, b;
+ {
+ var j := 0;
+ b[0] := i;
+ while(j < 10)
+ invariant 0 <= j <= 10;
+ modifies a;
+ {
+ a[0] := j;
+ j := j + 1;
+ }
+ assert b[0] == i;
+ i := i + 1;
+ }
+ c[0] := 1;
+}
+
+// allocation, fresh tests:
+
+// allocated things not automatically in modifies of loops:
+method Testing10(a: array<int>)
+ requires a != null && a.Length > 0;
+ modifies a;
+{
+ var i := 0;
+ var arr := new int[1];
+ arr[0] := 1; // good, even though not in method modifies.
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ modifies a;
+ {
+ arr[0] := 1; // bad.
+ i := i + 1;
+ }
+}
+
+// unless no modifies given, in which case the context is used:
+method Testing10a(a: array<int>)
+ requires a != null && a.Length > 0;
+ modifies a;
+{
+ var i := 0;
+ var arr := new int[1];
+ arr[0] := 1; // still good.
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ {
+ arr[0] := 1; // no modifies, so allowed to touch arr.
+ i := i + 1;
+ }
+}
+
+// arr still accessible after loop that can't touch it.
+method Testing11()
+{
+ var i := 0;
+ var arr := new int[1];
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ modifies;
+ {
+ arr := new int[1];
+ arr[0] := 1;
+ var j := 0;
+ while(j < 10)
+ invariant 0 <= j <= 10;
+ modifies;
+ {
+ // can't touch arr in here.
+ j := j + 1;
+ }
+ arr[0] := 2;
+ i := i + 1;
+ }
+}
+
+// allocation inside a loop is still ok:
+method Testing11a(a: array<int>)
+ requires a != null && a.Length > 0;
+ modifies a;
+{
+ var i := 0;
+ while(i < 10)
+ invariant 0 <= i <= 10;
+ modifies a;
+ {
+ var arr := new int[1];
+ arr[0] := 1; // can modify arr, even though it
+ // is not in modifies because it is fresh.
+ var j := 0;
+ while(j < 10)
+ invariant 0 <= j <= 10;
+ modifies a;
+ {
+ arr[0] := 3; // can't touch arr, as allocated before modifies captured.
+ j := j + 1;
+ }
+ i := i + 1;
+ }
+}
+
+class Elem
+{
+ var i: int;
+}
+
+// capture of modifies clause at beginning of loop:
+method Testing12(a: Elem, b: Elem, c: Elem)
+ requires a != null && b != null && c != null;
+ requires a != b && b != c && c != a; // all different.
+ modifies a, b, c;
+{
+ var i := 0;
+ var S := {a, b, c};
+ // S "captured" here for purposes of modifies clause.
+ while(S != {})
+ modifies S;
+ decreases S;
+ {
+ var j := choose S;
+ // these still good, even though S shrinks to not include them.
+ a.i := i;
+ b.i := i;
+ c.i := i;
+ S := S - {j};
+ i := i + 1;
+ }
+}
\ No newline at end of file diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat index aed9ee8a..3c64f623 100644 --- a/Test/dafny0/runtest.bat +++ b/Test/dafny0/runtest.bat @@ -18,7 +18,7 @@ for %%f in (TypeTests.dfy NatTypes.dfy SmallTests.dfy Definedness.dfy Comprehensions.dfy Basics.dfy ControlStructures.dfy
Termination.dfy DTypes.dfy
TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy
- Refinement.dfy RefinementErrors.dfy) do (
+ Refinement.dfy RefinementErrors.dfy LoopModifies.dfy) do (
echo.
echo -------------------- %%f --------------------
%DAFNY_EXE% /compile:0 %* %%f
diff --git a/Test/z3api/Answer b/Test/z3api/Answer index 782aa852..d18f12ef 100644 --- a/Test/z3api/Answer +++ b/Test/z3api/Answer @@ -1,9 +1,9 @@ -------------------- boog0.bpl --------------------
-boog0.bpl(51,1): Error BP5003: A postcondition might not hold at this return statement.
-boog0.bpl(45,3): Related location: This is the postcondition that might not hold.
+boog0.bpl(49,1): Error BP5003: A postcondition might not hold on this return path.
+boog0.bpl(43,3): Related location: This is the postcondition that might not hold.
Execution trace:
- boog0.bpl(48,7): anon0
+ boog0.bpl(46,7): anon0
Boogie program verifier finished with 1 verified, 1 error
@@ -12,17 +12,17 @@ Boogie program verifier finished with 1 verified, 1 error Boogie program verifier finished with 1 verified, 0 errors
-------------------- boog2.bpl --------------------
-boog2.bpl(23,1): Error BP5003: A postcondition might not hold at this return statement.
-boog2.bpl(19,3): Related location: This is the postcondition that might not hold.
+boog2.bpl(24,1): Error BP5003: A postcondition might not hold on this return path.
+boog2.bpl(20,3): Related location: This is the postcondition that might not hold.
Execution trace:
- boog2.bpl(22,8): anon0
+ boog2.bpl(23,8): anon0
Boogie program verifier finished with 1 verified, 1 error
-------------------- boog3.bpl --------------------
-boog3.bpl(6,3): Error BP5001: This assertion might not hold.
+boog3.bpl(7,3): Error BP5001: This assertion might not hold.
Execution trace:
- boog3.bpl(6,3): anon0
+ boog3.bpl(7,3): anon0
Boogie program verifier finished with 0 verified, 1 error
@@ -31,11 +31,11 @@ Boogie program verifier finished with 0 verified, 1 error Boogie program verifier finished with 1 verified, 0 errors
-------------------- boog5.bpl --------------------
-boog5.bpl(36,3): Error BP5003: A postcondition might not hold at this return statement.
-boog5.bpl(29,3): Related location: This is the postcondition that might not hold.
+boog5.bpl(37,3): Error BP5003: A postcondition might not hold on this return path.
+boog5.bpl(30,3): Related location: This is the postcondition that might not hold.
Execution trace:
- boog5.bpl(32,3): anon0
- boog5.bpl(35,13): anon3_Else
+ boog5.bpl(33,3): anon0
+ boog5.bpl(36,13): anon3_Else
Boogie program verifier finished with 0 verified, 1 error
@@ -44,91 +44,92 @@ Boogie program verifier finished with 0 verified, 1 error Boogie program verifier finished with 1 verified, 0 errors
-------------------- boog7.bpl --------------------
-boog7.bpl(17,1): Error BP5003: A postcondition might not hold at this return statement.
-boog7.bpl(13,3): Related location: This is the postcondition that might not hold.
+boog7.bpl(18,1): Error BP5003: A postcondition might not hold on this return path.
+boog7.bpl(14,3): Related location: This is the postcondition that might not hold.
Execution trace:
- boog7.bpl(16,11): anon0
+ boog7.bpl(17,11): anon0
Boogie program verifier finished with 0 verified, 1 error
-------------------- boog8.bpl --------------------
-boog8.bpl(7,12): Error: no bitvector handling specified, please use /bv:i or /bv:z flag
-boog8.bpl(7,18): Error: no bitvector handling specified, please use /bv:i or /bv:z flag
-2 type checking errors detected in boog8.bpl
+boog8.bpl(23,1): Error BP5003: A postcondition might not hold on this return path.
+boog8.bpl(19,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ boog8.bpl(22,11): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
-------------------- boog9.bpl --------------------
-boog9.bpl(19,1): Error BP5003: A postcondition might not hold at this return statement.
-boog9.bpl(15,3): Related location: This is the postcondition that might not hold.
+boog9.bpl(20,1): Error BP5003: A postcondition might not hold on this return path.
+boog9.bpl(16,3): Related location: This is the postcondition that might not hold.
Execution trace:
- boog9.bpl(18,11): anon0
+ boog9.bpl(19,11): anon0
Boogie program verifier finished with 0 verified, 1 error
-------------------- boog10.bpl --------------------
-boog10.bpl(18,3): Error BP5001: This assertion might not hold.
+boog10.bpl(19,3): Error BP5001: This assertion might not hold.
Execution trace:
- boog10.bpl(18,3): anon0
+ boog10.bpl(19,3): anon0
Boogie program verifier finished with 0 verified, 1 error
-------------------- boog11.bpl --------------------
-boog11.bpl(14,1): Error BP5003: A postcondition might not hold at this return statement.
-boog11.bpl(10,3): Related location: This is the postcondition that might not hold.
+boog11.bpl(15,1): Error BP5003: A postcondition might not hold on this return path.
+boog11.bpl(11,3): Related location: This is the postcondition that might not hold.
Execution trace:
- boog11.bpl(13,8): anon0
+ boog11.bpl(14,8): anon0
Boogie program verifier finished with 0 verified, 1 error
-------------------- boog12.bpl --------------------
-boog12.bpl(18,1): Error BP5003: A postcondition might not hold at this return statement.
-boog12.bpl(13,3): Related location: This is the postcondition that might not hold.
+boog12.bpl(19,1): Error BP5003: A postcondition might not hold on this return path.
+boog12.bpl(14,3): Related location: This is the postcondition that might not hold.
Execution trace:
- boog12.bpl(16,16): anon0
+ boog12.bpl(17,16): anon0
Boogie program verifier finished with 0 verified, 1 error
-------------------- boog13.bpl --------------------
-boog13.bpl(9,11): Error: more than one declaration of variable name: v
+boog13.bpl(10,18): Error: more than one declaration of variable name: v
1 name resolution errors detected in boog13.bpl
-------------------- boog14.bpl --------------------
-boog14.bpl(11,1): Error BP5003: A postcondition might not hold at this return statement.
-boog14.bpl(8,1): Related location: This is the postcondition that might not hold.
+boog14.bpl(12,1): Error BP5003: A postcondition might not hold on this return path.
+boog14.bpl(9,1): Related location: This is the postcondition that might not hold.
Execution trace:
- boog14.bpl(10,8): anon0
+ boog14.bpl(11,8): anon0
Boogie program verifier finished with 0 verified, 1 error
-------------------- boog15.bpl --------------------
-boog15.bpl(10,1): Error BP5003: A postcondition might not hold at this return statement.
-boog15.bpl(7,1): Related location: This is the postcondition that might not hold.
+boog15.bpl(11,1): Error BP5003: A postcondition might not hold on this return path.
+boog15.bpl(8,1): Related location: This is the postcondition that might not hold.
Execution trace:
- boog15.bpl(9,8): anon0
+ boog15.bpl(10,8): anon0
Boogie program verifier finished with 0 verified, 1 error
-------------------- boog16.bpl --------------------
-boog16.bpl(11,1): Error BP5003: A postcondition might not hold at this return statement.
-boog16.bpl(8,1): Related location: This is the postcondition that might not hold.
+boog16.bpl(12,1): Error BP5003: A postcondition might not hold on this return path.
+boog16.bpl(9,1): Related location: This is the postcondition that might not hold.
Execution trace:
- boog16.bpl(10,8): anon0
+ boog16.bpl(11,8): anon0
Boogie program verifier finished with 0 verified, 1 error
-------------------- boog17.bpl --------------------
-boog17.bpl(24,3): Error BP5001: This assertion might not hold.
+boog17.bpl(26,3): Error BP5001: This assertion might not hold.
Execution trace:
- boog17.bpl(15,1): start
- boog17.bpl(19,1): label_3
- boog17.bpl(22,1): label_4
+ boog17.bpl(17,1): start
Boogie program verifier finished with 0 verified, 1 error
-------------------- boog18.bpl --------------------
-boog18.bpl(15,1): Error BP5003: A postcondition might not hold at this return statement.
-boog18.bpl(12,1): Related location: This is the postcondition that might not hold.
+boog18.bpl(16,1): Error BP5003: A postcondition might not hold on this return path.
+boog18.bpl(13,1): Related location: This is the postcondition that might not hold.
Execution trace:
- boog18.bpl(14,4): anon0
+ boog18.bpl(15,4): anon0
Boogie program verifier finished with 0 verified, 1 error
@@ -137,9 +138,9 @@ Boogie program verifier finished with 0 verified, 1 error Boogie program verifier finished with 1 verified, 0 errors
-------------------- boog20.bpl --------------------
-boog20.bpl(15,1): Error BP5001: This assertion might not hold.
+boog20.bpl(16,1): Error BP5001: This assertion might not hold.
Execution trace:
- boog20.bpl(15,1): anon0
+ boog20.bpl(16,1): anon0
Boogie program verifier finished with 0 verified, 1 error
@@ -148,7 +149,7 @@ Boogie program verifier finished with 0 verified, 1 error Boogie program verifier finished with 1 verified, 0 errors
-------------------- boog22.bpl --------------------
-boog22.bpl(4,9): Error: more than one declaration of function/procedure name: f1
+boog22.bpl(5,9): Error: more than one declaration of function/procedure name: f1
1 name resolution errors detected in boog22.bpl
-------------------- boog23.bpl --------------------
@@ -176,12 +177,83 @@ Boogie program verifier finished with 1 verified, 0 errors Boogie program verifier finished with 1 verified, 0 errors
-------------------- boog31.bpl --------------------
-boog31.bpl(12,1): Error BP5001: This assertion might not hold.
+boog31.bpl(13,1): Error BP5001: This assertion might not hold.
Execution trace:
- boog31.bpl(12,1): anon0
+ boog31.bpl(13,1): anon0
Boogie program verifier finished with 0 verified, 1 error
-------------------- boog34.bpl --------------------
Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- boog35.bpl --------------------
+boog35.bpl(16,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ boog35.bpl(14,11): anon0
+
+Boogie program verifier finished with 1 verified, 1 error
+
+-------------------- bar1.bpl --------------------
+bar1.bpl(25,1): Error BP5003: A postcondition might not hold on this return path.
+bar1.bpl(21,1): Related location: This is the postcondition that might not hold.
+Execution trace:
+ bar1.bpl(24,3): anon0
+ Inlined call to procedure foo begins
+ bar1.bpl(13,5): anon0
+ Inlined call to procedure bar begins
+ bar1.bpl(7,5): anon0
+ Inlined call to procedure bar ends
+ Inlined call to procedure bar begins
+ bar1.bpl(7,5): anon0
+ Inlined call to procedure bar ends
+ Inlined call to procedure foo ends
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- bar2.bpl --------------------
+bar2.bpl(21,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ bar2.bpl(19,3): anon0
+ Inlined call to procedure foo begins
+ bar2.bpl(5,3): anon0
+ bar2.bpl(9,7): anon3_Else
+ Inlined call to procedure foo ends
+ Inlined call to procedure foo begins
+ bar2.bpl(5,3): anon0
+ bar2.bpl(6,7): anon3_Then
+ Inlined call to procedure foo ends
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- bar3.bpl --------------------
+bar3.bpl(41,1): Error BP5003: A postcondition might not hold on this return path.
+bar3.bpl(34,1): Related location: This is the postcondition that might not hold.
+Execution trace:
+ bar3.bpl(38,3): anon0
+ Inlined call to procedure foo begins
+ bar3.bpl(18,3): anon0
+ bar3.bpl(24,7): anon3_Else
+ Inlined call to procedure bar begins
+ bar3.bpl(7,3): anon0
+ bar3.bpl(10,7): anon3_Else
+ Inlined call to procedure bar ends
+ Inlined call to procedure bar begins
+ bar3.bpl(7,3): anon0
+ bar3.bpl(10,7): anon3_Else
+ Inlined call to procedure bar ends
+ Inlined call to procedure foo ends
+ Inlined call to procedure bar begins
+ bar3.bpl(7,3): anon0
+ bar3.bpl(10,7): anon3_Else
+ Inlined call to procedure bar ends
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- bar4.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- bar6.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/z3api/Boog24.bpl b/Test/z3api/Boog24.bpl index c5e2eea6..d3da775d 100644 --- a/Test/z3api/Boog24.bpl +++ b/Test/z3api/Boog24.bpl @@ -1,3 +1,4 @@ +type ref;
function LIFT(a:bool) returns (int);
axiom(forall a:bool :: {LIFT(a)} a <==> LIFT(a) != 0);
diff --git a/Test/z3api/bar1.bpl b/Test/z3api/bar1.bpl new file mode 100644 index 00000000..845954d5 --- /dev/null +++ b/Test/z3api/bar1.bpl @@ -0,0 +1,26 @@ +var x: int;
+var y: int;
+
+procedure {:inline 1} bar()
+modifies y;
+{
+ y := y + 1;
+}
+
+procedure {:inline 1} foo()
+modifies x, y;
+{
+ x := x + 1;
+ call bar();
+ call bar();
+ x := x + 1;
+}
+
+procedure main()
+requires x == y;
+ensures x != y;
+modifies x, y;
+{
+ call foo();
+}
+
diff --git a/Test/z3api/bar2.bpl b/Test/z3api/bar2.bpl new file mode 100644 index 00000000..76991a8f --- /dev/null +++ b/Test/z3api/bar2.bpl @@ -0,0 +1,24 @@ +
+procedure {:inline 1} foo() returns (x: bool)
+{
+ var b: bool;
+ if (b) {
+ x := false;
+ return;
+ } else {
+ x := true;
+ return;
+ }
+}
+
+procedure main()
+{
+ var b1: bool;
+ var b2: bool;
+
+ call b1 := foo();
+ call b2 := foo();
+ assert b1 == b2;
+}
+
+
diff --git a/Test/z3api/bar3.bpl b/Test/z3api/bar3.bpl new file mode 100644 index 00000000..7bd91184 --- /dev/null +++ b/Test/z3api/bar3.bpl @@ -0,0 +1,41 @@ +var y: int;
+var x: int;
+
+procedure {:inline 1} bar(b: bool)
+modifies y;
+{
+ if (b) {
+ y := y + 1;
+ } else {
+ y := y - 1;
+ }
+}
+
+procedure {:inline 1} foo()
+modifies x, y;
+{
+ var b: bool;
+ if (b) {
+ x := x + 1;
+ call bar(true);
+ call bar(true);
+ x := x + 1;
+ } else {
+ x := x - 1;
+ call bar(false);
+ call bar(false);
+ x := x - 1;
+ }
+}
+
+
+procedure main()
+requires x == y;
+ensures x == y;
+modifies x, y;
+modifies y;
+{
+ call foo();
+ assert x == y;
+ call bar(false);
+}
diff --git a/Test/z3api/bar4.bpl b/Test/z3api/bar4.bpl new file mode 100644 index 00000000..84640811 --- /dev/null +++ b/Test/z3api/bar4.bpl @@ -0,0 +1,38 @@ +var y: int;
+var x: int;
+
+procedure {:inline 1} bar() returns (b: bool)
+modifies y;
+{
+ if (b) {
+ y := y + 1;
+ } else {
+ y := y - 1;
+ }
+}
+
+procedure {:inline 1} foo()
+modifies x, y;
+{
+ var b: bool;
+
+ call b := bar();
+ if (b) {
+ x := x + 1;
+ } else {
+ x := x - 1;
+ }
+}
+
+
+procedure main() returns (b: bool)
+requires x == y;
+ensures !b ==> x == y+1;
+ensures b ==> x+1 == y;
+modifies x, y;
+modifies y;
+{
+ call foo();
+ assert x == y;
+ call b := bar();
+}
diff --git a/Test/z3api/bar6.bpl b/Test/z3api/bar6.bpl new file mode 100644 index 00000000..e133aef7 --- /dev/null +++ b/Test/z3api/bar6.bpl @@ -0,0 +1,36 @@ +var M: [int]int;
+
+procedure {:inline 1} bar(y: int) returns (b: bool)
+modifies M;
+{
+ if (b) {
+ M[y] := M[y] + 1;
+ } else {
+ M[y] := M[y] - 1;
+ }
+}
+
+procedure {:inline 1} foo(x: int, y: int)
+modifies M;
+{
+ var b: bool;
+
+ call b := bar(y);
+ if (b) {
+ M[x] := M[x] + 1;
+ } else {
+ M[x] := M[x] - 1;
+ }
+}
+
+procedure main(x: int, y: int) returns (b: bool)
+requires x != y;
+requires M[x] == M[y];
+ensures !b ==> M[x] == M[y]+1;
+ensures b ==> M[x]+1 == M[y];
+modifies M;
+{
+ call foo(x, y);
+ assert M[x] == M[y];
+ call b := bar(y);
+}
diff --git a/Test/z3api/boog0.bpl b/Test/z3api/boog0.bpl index 1b9bee36..4206152b 100644 --- a/Test/z3api/boog0.bpl +++ b/Test/z3api/boog0.bpl @@ -1,3 +1,4 @@ +type ref;
type Wicket;
const w: Wicket;
var favorite: Wicket;
@@ -6,7 +7,7 @@ function age(Wicket) returns (int); axiom age(w)==7;
procedure NewFavorite(p: Wicket);
- modifies favorite
;
+ modifies favorite;
ensures favorite==p;
@@ -19,7 +20,7 @@ const myRef: ref; const v: Wicket;
axiom 7 < 8;
-axiom 7 <= 8;
+axiom 7 <= 8;
axiom 8 > 7;
axiom 8 >= 7;
axiom 6 != 7;
@@ -37,7 +38,7 @@ axiom ((7==7) && (8==8)); var favorite2: Wicket;
procedure SwapFavorites()
- modifies favorite,favorite2
;
+ modifies favorite,favorite2;
ensures (favorite==old(favorite2)) && (favorite2==old(favorite));
{
diff --git a/Test/z3api/boog1.bpl b/Test/z3api/boog1.bpl index 6b6cce75..9f4d2349 100644 --- a/Test/z3api/boog1.bpl +++ b/Test/z3api/boog1.bpl @@ -1,3 +1,4 @@ +type ref;
type Wicket;
const w: Wicket;
var favorite: Wicket;
@@ -7,7 +8,8 @@ function age(Wicket) returns (int); axiom age(w)==7;
procedure NewFavorite(p: Wicket);
- modifies favorite
;
+ modifies favorite
+;
ensures favorite==p;
diff --git a/Test/z3api/boog10.bpl b/Test/z3api/boog10.bpl index 5ac43287..075432d7 100644 --- a/Test/z3api/boog10.bpl +++ b/Test/z3api/boog10.bpl @@ -1,3 +1,4 @@ +type ref;
// types
type Color;
const unique red: Color;
@@ -9,7 +10,8 @@ var myColor: Color; // procedure
procedure SetTo(c: Color);
- modifies myColor
;
+ modifies myColor
+;
ensures myColor==c;
diff --git a/Test/z3api/boog11.bpl b/Test/z3api/boog11.bpl index e66802ea..5b83de6a 100644 --- a/Test/z3api/boog11.bpl +++ b/Test/z3api/boog11.bpl @@ -1,10 +1,12 @@ +type ref;
// types
const top: ref;
var myRef: ref;
// procedure
procedure SetTo(r: ref);
- modifies myRef
;
+ modifies myRef
+;
ensures myRef==r;
diff --git a/Test/z3api/boog12.bpl b/Test/z3api/boog12.bpl index d20a8f35..c277a674 100644 --- a/Test/z3api/boog12.bpl +++ b/Test/z3api/boog12.bpl @@ -1,3 +1,4 @@ +type ref;
// types
type Color;
const blue: Color;
@@ -7,7 +8,8 @@ var myMatrix:[int,int] Color; // procedure
procedure SetTo(c: Color);
- modifies myArray, myMatrix
;
+ modifies myArray, myMatrix
+;
ensures myArray[0]==c;
diff --git a/Test/z3api/boog13.bpl b/Test/z3api/boog13.bpl index a4f854f5..9cd873c6 100644 --- a/Test/z3api/boog13.bpl +++ b/Test/z3api/boog13.bpl @@ -1,3 +1,4 @@ +type ref;
// types
type Wicket;
var favorite: Wicket;
@@ -6,14 +7,16 @@ var v: Wicket; function age(w:Wicket) returns (int);
axiom (exists v:Wicket :: age(v)<8 &&
- (forall v:Wicket
:: age(v)==7)
+ (forall v:Wicket
+ :: age(v)==7)
);
// procedure
procedure SetToSeven(p: Wicket);
- modifies favorite
;
+ modifies favorite
+;
ensures favorite==p;
diff --git a/Test/z3api/boog14.bpl b/Test/z3api/boog14.bpl index c163ed18..41450d85 100644 --- a/Test/z3api/boog14.bpl +++ b/Test/z3api/boog14.bpl @@ -1,3 +1,4 @@ +type ref;
function choose(a:bool, b:int, c:int) returns (x:int);
axiom(forall a:bool, b:int, c:int :: {choose(a,b,c)} a ==> choose(a,b,c) == b);
diff --git a/Test/z3api/boog15.bpl b/Test/z3api/boog15.bpl index ef792b2b..428c0f6e 100644 --- a/Test/z3api/boog15.bpl +++ b/Test/z3api/boog15.bpl @@ -1,3 +1,4 @@ +type ref;
function AtLeast(int, int) returns ([int]bool);
axiom(forall n:int, x:int :: {AtLeast(n,x)} AtLeast(n,x)[x]);
diff --git a/Test/z3api/boog16.bpl b/Test/z3api/boog16.bpl index 48afd41d..a002c166 100644 --- a/Test/z3api/boog16.bpl +++ b/Test/z3api/boog16.bpl @@ -1,3 +1,4 @@ +type ref;
function choose(a:bool, b:int, c:int) returns (x:int);
axiom(forall a:bool, b:int, c:int ::
{choose(a,b,c)} !a ==> choose(a,b,c) == c);
diff --git a/Test/z3api/boog17.bpl b/Test/z3api/boog17.bpl index 6f886f49..89159af1 100644 --- a/Test/z3api/boog17.bpl +++ b/Test/z3api/boog17.bpl @@ -1,3 +1,5 @@ +type name;
+type ref;
const unique g : int;
axiom(g != 0);
diff --git a/Test/z3api/boog18.bpl b/Test/z3api/boog18.bpl index fe0cbc10..35f7d48a 100644 --- a/Test/z3api/boog18.bpl +++ b/Test/z3api/boog18.bpl @@ -1,3 +1,4 @@ +type ref;
const A100INT4_name:int;
function Match(a:int, t:int) returns (int);
diff --git a/Test/z3api/boog19.bpl b/Test/z3api/boog19.bpl index 17b199dd..178bb04f 100644 --- a/Test/z3api/boog19.bpl +++ b/Test/z3api/boog19.bpl @@ -1,3 +1,5 @@ +type name;
+type ref;
var alloc:[int]name;
diff --git a/Test/z3api/boog2.bpl b/Test/z3api/boog2.bpl index 74c05a28..315c51af 100644 --- a/Test/z3api/boog2.bpl +++ b/Test/z3api/boog2.bpl @@ -1,10 +1,12 @@ +type ref;
type Wicket;
var favorite: Wicket;
var hate: Wicket;
procedure NewFavorite(p: Wicket);
- modifies favorite
;
+ modifies favorite
+;
ensures favorite==p;
diff --git a/Test/z3api/boog20.bpl b/Test/z3api/boog20.bpl index fa714972..10181400 100644 --- a/Test/z3api/boog20.bpl +++ b/Test/z3api/boog20.bpl @@ -1,3 +1,4 @@ +type ref;
function PLUS(int, int, int) returns (int);
function Rep(int, int) returns (int);
diff --git a/Test/z3api/boog21.bpl b/Test/z3api/boog21.bpl index 1f4fa6dc..8e3abde7 100644 --- a/Test/z3api/boog21.bpl +++ b/Test/z3api/boog21.bpl @@ -1,3 +1,4 @@ +type ref;
function PLUS(int, int, int) returns (int);
function Rep(int,int) returns (int);
@@ -5,7 +6,8 @@ function Rep(int,int) returns (int); // ERROR
-axiom(forall a:int, b:int, z:int :: Rep(a,b) == PLUS(a,b,z
));
+axiom(forall a:int, b:int, z:int :: Rep(a,b) == PLUS(a,b,z
+));
axiom(forall n:int, x:int :: {Rep(n,x)} (exists k:int :: Rep(n,x) == x));
// END ERROR
diff --git a/Test/z3api/boog22.bpl b/Test/z3api/boog22.bpl index 95e45849..c255a3c5 100644 --- a/Test/z3api/boog22.bpl +++ b/Test/z3api/boog22.bpl @@ -1,3 +1,4 @@ +type ref;
type W;
function f1(W,int) returns (int);
diff --git a/Test/z3api/boog23.bpl b/Test/z3api/boog23.bpl index 41c68790..4e0fc4d0 100644 --- a/Test/z3api/boog23.bpl +++ b/Test/z3api/boog23.bpl @@ -1,3 +1,5 @@ +type name;
+type ref;
type byte;
function OneByteToInt(byte) returns (int);
function TwoBytesToInt(byte, byte) returns (int);
diff --git a/Test/z3api/boog25.bpl b/Test/z3api/boog25.bpl index 0a8b5e92..0ee4163c 100644 --- a/Test/z3api/boog25.bpl +++ b/Test/z3api/boog25.bpl @@ -1,3 +1,5 @@ +type name;
+type ref;
type byte;
function OneByteToInt(byte) returns (int);
function TwoBytesToInt(byte, byte) returns (int);
diff --git a/Test/z3api/boog28.bpl b/Test/z3api/boog28.bpl index 989dbf75..ab7f4ad2 100644 --- a/Test/z3api/boog28.bpl +++ b/Test/z3api/boog28.bpl @@ -1,3 +1,4 @@ +type ref;
function LIFT(x:bool) returns (int);
axiom(forall x:bool :: {LIFT(x)} x <==> LIFT(x) != 0);
diff --git a/Test/z3api/boog29.bpl b/Test/z3api/boog29.bpl index 8a97944d..035e69fd 100644 --- a/Test/z3api/boog29.bpl +++ b/Test/z3api/boog29.bpl @@ -1,3 +1,4 @@ +type ref;
function LIFT(x:bool) returns (int);
axiom(forall x:bool :: {LIFT(x)} x <==> LIFT(x) != 0);
diff --git a/Test/z3api/boog3.bpl b/Test/z3api/boog3.bpl index 9e04ac5b..207ddbd0 100644 --- a/Test/z3api/boog3.bpl +++ b/Test/z3api/boog3.bpl @@ -1,3 +1,4 @@ +type ref;
type Wicket;
procedure Dummy();
diff --git a/Test/z3api/boog30.bpl b/Test/z3api/boog30.bpl index ae682156..81e04f20 100644 --- a/Test/z3api/boog30.bpl +++ b/Test/z3api/boog30.bpl @@ -1,3 +1,4 @@ +type ref;
function LIFT(x:bool) returns (int);
axiom(forall x:bool :: {LIFT(x)} x <==> LIFT(x) != 0);
diff --git a/Test/z3api/boog31.bpl b/Test/z3api/boog31.bpl index 219effce..86386a90 100644 --- a/Test/z3api/boog31.bpl +++ b/Test/z3api/boog31.bpl @@ -1,3 +1,4 @@ +type ref;
const b1:bool;
const b2:bool;
diff --git a/Test/z3api/boog34.bpl b/Test/z3api/boog34.bpl index 62e7e82b..88a587aa 100644 --- a/Test/z3api/boog34.bpl +++ b/Test/z3api/boog34.bpl @@ -1,3 +1,4 @@ +type ref;
function Rep(int, int) returns (int);
axiom(forall n:int, x:int :: {Rep(n,x)}
diff --git a/Test/z3api/boog35.bpl b/Test/z3api/boog35.bpl new file mode 100644 index 00000000..beae0c74 --- /dev/null +++ b/Test/z3api/boog35.bpl @@ -0,0 +1,17 @@ +procedure foo1(x: int, y: int)
+{
+ var a: [int][int]int;
+
+ a[x][y] := 42;
+
+ assert a[x][y] == 42;
+}
+
+procedure foo2(x: int, y: int)
+{
+ var a: [int][int]int;
+
+ a[x][y] := 42;
+
+ assert a[x][y] == 43;
+}
\ No newline at end of file diff --git a/Test/z3api/boog4.bpl b/Test/z3api/boog4.bpl index 46eda549..95ec7011 100644 --- a/Test/z3api/boog4.bpl +++ b/Test/z3api/boog4.bpl @@ -1,3 +1,4 @@ +type ref;
type Wicket;
const w: Wicket;
@@ -10,7 +11,8 @@ function age(Wicket) returns (int); axiom age(w)==7;
axiom 7 < 8;
-axiom 7 <= 8;
+axiom 7 <= 8;
+
axiom 8 > 7;
axiom 8 >= 7;
axiom 6 != 7;
@@ -28,7 +30,8 @@ axiom 7!=7; procedure NewFavorite(p: Wicket);
- modifies favorite
;
+ modifies favorite
+;
ensures favorite==p;
diff --git a/Test/z3api/boog5.bpl b/Test/z3api/boog5.bpl index 0db94bba..4b76fd22 100644 --- a/Test/z3api/boog5.bpl +++ b/Test/z3api/boog5.bpl @@ -1,3 +1,4 @@ +type ref;
// types
type Wicket;
@@ -23,7 +24,8 @@ axiom age(x)==4; // procedure
procedure SetToSeven(p: Wicket);
- modifies favorite
;
+ modifies favorite
+;
ensures favorite==p;
@@ -32,7 +34,8 @@ implementation SetToSeven(l: Wicket) { favorite:=l;
} else {
favorite:=v;
- }
+ }
+
}
diff --git a/Test/z3api/boog6.bpl b/Test/z3api/boog6.bpl index 55c1dc7e..f6c3c23f 100644 --- a/Test/z3api/boog6.bpl +++ b/Test/z3api/boog6.bpl @@ -1,3 +1,4 @@ +type ref;
// types
type Wicket;
@@ -10,7 +11,8 @@ axiom b==true; // procedure
procedure SetToSeven(p: Wicket);
- modifies favorite
;
+ modifies favorite
+;
ensures favorite==p;
diff --git a/Test/z3api/boog7.bpl b/Test/z3api/boog7.bpl index 36f952d1..78e5e3e6 100644 --- a/Test/z3api/boog7.bpl +++ b/Test/z3api/boog7.bpl @@ -1,3 +1,4 @@ +type ref;
// consts
const w: int;
@@ -7,7 +8,8 @@ var favorite: int; // procedure
procedure SetToSeven(p: int);
- modifies favorite
;
+ modifies favorite
+;
ensures favorite==p;
diff --git a/Test/z3api/boog8.bpl b/Test/z3api/boog8.bpl index 0ac4f163..121f27cf 100644 --- a/Test/z3api/boog8.bpl +++ b/Test/z3api/boog8.bpl @@ -1,3 +1,4 @@ +type ref;
// types
type Wicket;
var favorite: Wicket;
@@ -12,7 +13,8 @@ axiom myBool==true; // procedure
procedure SetToSeven(p: Wicket);
- modifies favorite
;
+ modifies favorite
+;
ensures favorite==p;
diff --git a/Test/z3api/boog9.bpl b/Test/z3api/boog9.bpl index 55897a1d..3bd6ff63 100644 --- a/Test/z3api/boog9.bpl +++ b/Test/z3api/boog9.bpl @@ -1,3 +1,4 @@ +type ref;
// types
type Wicket;
var favorite: Wicket;
@@ -9,7 +10,8 @@ axiom (exists v:Wicket :: age(v)<8); // procedure
procedure SetToSeven(p: Wicket);
- modifies favorite
;
+ modifies favorite
+;
ensures favorite==p;
diff --git a/Test/z3api/runtest.bat b/Test/z3api/runtest.bat index 5daa36c0..6645667e 100644 --- a/Test/z3api/runtest.bat +++ b/Test/z3api/runtest.bat @@ -3,8 +3,14 @@ setlocal set BGEXE=..\..\Binaries\Boogie.exe
-for %%f in (boog0.bpl boog1.bpl boog2.bpl boog3.bpl boog4.bpl boog5.bpl boog6.bpl boog7.bpl boog8.bpl boog9.bpl boog10.bpl boog11.bpl boog12.bpl boog13.bpl boog14.bpl boog15.bpl boog16.bpl boog17.bpl boog18.bpl boog19.bpl boog20.bpl boog21.bpl boog22.bpl boog23.bpl boog24.bpl boog25.bpl boog28.bpl boog29.bpl boog30.bpl boog31.bpl boog34.bpl) do (
+for %%f in (boog0.bpl boog1.bpl boog2.bpl boog3.bpl boog4.bpl boog5.bpl boog6.bpl boog7.bpl boog8.bpl boog9.bpl boog10.bpl boog11.bpl boog12.bpl boog13.bpl boog14.bpl boog15.bpl boog16.bpl boog17.bpl boog18.bpl boog19.bpl boog20.bpl boog21.bpl boog22.bpl boog23.bpl boog24.bpl boog25.bpl boog28.bpl boog29.bpl boog30.bpl boog31.bpl boog34.bpl boog35.bpl) do (
echo.
echo -------------------- %%f --------------------
- %BGEXE% %* /nologo /prover:z3api %%f
+ %BGEXE% %* /nologo /typeEncoding:m /prover:z3api %%f
)
+
+for %%f in (bar1.bpl bar2.bpl bar3.bpl bar4.bpl bar6.bpl) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %BGEXE% %* /nologo /noinfer /stratifiedInline:1 /prover:z3api %%f
+)
\ No newline at end of file |