diff options
Diffstat (limited to 'Test/test21')
155 files changed, 1322 insertions, 347 deletions
diff --git a/Test/test21/Answer b/Test/test21/Answer index 73feaf41..fba65f5f 100644 --- a/Test/test21/Answer +++ b/Test/test21/Answer @@ -3,129 +3,129 @@ Boogie program verifier finished with 3 verified, 0 errors
--------------------- File DisjointDomains2.bpl ----------------------------
-DisjointDomains2.bpl(11,5): Error BP5001: This assertion might not hold.
+DisjointDomains2.bpl(17,5): Error BP5001: This assertion might not hold.
Execution trace:
- DisjointDomains2.bpl(9,3): start
-DisjointDomains2.bpl(18,5): Error BP5001: This assertion might not hold.
+ DisjointDomains2.bpl(15,3): start
+DisjointDomains2.bpl(24,5): Error BP5001: This assertion might not hold.
Execution trace:
- DisjointDomains2.bpl(16,3): start
+ DisjointDomains2.bpl(22,3): start
Boogie program verifier finished with 4 verified, 2 errors
--------------------- File FunAxioms.bpl ----------------------------
-FunAxioms.bpl(30,3): Error BP5001: This assertion might not hold.
+FunAxioms.bpl(36,3): Error BP5001: This assertion might not hold.
Execution trace:
- FunAxioms.bpl(18,3): anon0
+ FunAxioms.bpl(24,3): anon0
Boogie program verifier finished with 1 verified, 1 error
--------------------- File FunAxioms2.bpl ----------------------------
-FunAxioms2.bpl(20,3): Error BP5001: This assertion might not hold.
+FunAxioms2.bpl(26,3): Error BP5001: This assertion might not hold.
Execution trace:
- FunAxioms2.bpl(16,5): anon0
+ FunAxioms2.bpl(22,5): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File PolyList.bpl ----------------------------
-PolyList.bpl(42,3): Error BP5001: This assertion might not hold.
+PolyList.bpl(48,3): Error BP5001: This assertion might not hold.
Execution trace:
- PolyList.bpl(27,7): anon0
-PolyList.bpl(60,3): Error BP5001: This assertion might not hold.
+ PolyList.bpl(33,7): anon0
+PolyList.bpl(66,3): Error BP5001: This assertion might not hold.
Execution trace:
- PolyList.bpl(49,7): anon0
+ PolyList.bpl(55,7): anon0
Boogie program verifier finished with 0 verified, 2 errors
--------------------- File Maps0.bpl ----------------------------
-Maps0.bpl(23,3): Error BP5001: This assertion might not hold.
+Maps0.bpl(29,3): Error BP5001: This assertion might not hold.
Execution trace:
- Maps0.bpl(14,3): anon0
-Maps0.bpl(46,3): Error BP5001: This assertion might not hold.
+ Maps0.bpl(20,3): anon0
+Maps0.bpl(52,3): Error BP5001: This assertion might not hold.
Execution trace:
- Maps0.bpl(41,9): anon0
-Maps0.bpl(49,3): Error BP5001: This assertion might not hold.
+ Maps0.bpl(47,9): anon0
+Maps0.bpl(55,3): Error BP5001: This assertion might not hold.
Execution trace:
- Maps0.bpl(41,9): anon0
-Maps0.bpl(52,3): Error BP5001: This assertion might not hold.
+ Maps0.bpl(47,9): anon0
+Maps0.bpl(58,3): Error BP5001: This assertion might not hold.
Execution trace:
- Maps0.bpl(41,9): anon0
-Maps0.bpl(53,3): Error BP5001: This assertion might not hold.
+ Maps0.bpl(47,9): anon0
+Maps0.bpl(59,3): Error BP5001: This assertion might not hold.
Execution trace:
- Maps0.bpl(41,9): anon0
+ Maps0.bpl(47,9): anon0
Boogie program verifier finished with 1 verified, 5 errors
--------------------- File Maps1.bpl ----------------------------
-Maps1.bpl(26,3): Error BP5001: This assertion might not hold.
+Maps1.bpl(32,3): Error BP5001: This assertion might not hold.
Execution trace:
- Maps1.bpl(19,3): anon0
-Maps1.bpl(31,3): Error BP5001: This assertion might not hold.
+ Maps1.bpl(25,3): anon0
+Maps1.bpl(37,3): Error BP5001: This assertion might not hold.
Execution trace:
- Maps1.bpl(19,3): anon0
+ Maps1.bpl(25,3): anon0
Boogie program verifier finished with 0 verified, 2 errors
--------------------- File InterestingExamples0.bpl ----------------------------
-InterestingExamples0.bpl(7,1): Error BP5001: This assertion might not hold.
+InterestingExamples0.bpl(13,1): Error BP5001: This assertion might not hold.
Execution trace:
- InterestingExamples0.bpl(5,6): anon0
+ InterestingExamples0.bpl(11,6): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File InterestingExamples1.bpl ----------------------------
-InterestingExamples1.bpl(16,3): Error BP5001: This assertion might not hold.
-Execution trace:
- InterestingExamples1.bpl(13,5): anon0
InterestingExamples1.bpl(22,3): Error BP5001: This assertion might not hold.
Execution trace:
- InterestingExamples1.bpl(13,5): anon0
+ InterestingExamples1.bpl(19,5): anon0
+InterestingExamples1.bpl(28,3): Error BP5001: This assertion might not hold.
+Execution trace:
+ InterestingExamples1.bpl(19,5): anon0
Boogie program verifier finished with 0 verified, 2 errors
--------------------- File InterestingExamples2.bpl ----------------------------
-InterestingExamples2.bpl(9,1): Error BP5001: This assertion might not hold.
+InterestingExamples2.bpl(15,1): Error BP5001: This assertion might not hold.
Execution trace:
- InterestingExamples2.bpl(8,6): anon0
-InterestingExamples2.bpl(10,1): Error BP5001: This assertion might not hold.
+ InterestingExamples2.bpl(14,6): anon0
+InterestingExamples2.bpl(16,1): Error BP5001: This assertion might not hold.
Execution trace:
- InterestingExamples2.bpl(8,6): anon0
+ InterestingExamples2.bpl(14,6): anon0
Boogie program verifier finished with 0 verified, 2 errors
--------------------- File InterestingExamples3.bpl ----------------------------
-InterestingExamples3.bpl(15,2): Error BP5001: This assertion might not hold.
+InterestingExamples3.bpl(21,2): Error BP5001: This assertion might not hold.
Execution trace:
- InterestingExamples3.bpl(13,2): anon0
+ InterestingExamples3.bpl(19,2): anon0
Boogie program verifier finished with 2 verified, 1 error
--------------------- File InterestingExamples4.bpl ----------------------------
-InterestingExamples4.bpl(36,3): Error BP5001: This assertion might not hold.
+InterestingExamples4.bpl(42,3): Error BP5001: This assertion might not hold.
Execution trace:
- InterestingExamples4.bpl(36,3): anon0
-InterestingExamples4.bpl(39,3): Error BP5001: This assertion might not hold.
+ InterestingExamples4.bpl(42,3): anon0
+InterestingExamples4.bpl(45,3): Error BP5001: This assertion might not hold.
Execution trace:
- InterestingExamples4.bpl(36,3): anon0
+ InterestingExamples4.bpl(42,3): anon0
Boogie program verifier finished with 0 verified, 2 errors
--------------------- File InterestingExamples5.bpl ----------------------------
Boogie program verifier finished with 1 verified, 0 errors
--------------------- File Colors.bpl ----------------------------
-Colors.bpl(13,3): Error BP5001: This assertion might not hold.
+Colors.bpl(19,3): Error BP5001: This assertion might not hold.
Execution trace:
- Colors.bpl(12,3): anon0
-Colors.bpl(20,3): Error BP5001: This assertion might not hold.
+ Colors.bpl(18,3): anon0
+Colors.bpl(26,3): Error BP5001: This assertion might not hold.
Execution trace:
- Colors.bpl(19,3): anon0
+ Colors.bpl(25,3): anon0
Boogie program verifier finished with 0 verified, 2 errors
--------------------- File HeapAbstraction.bpl ----------------------------
Boogie program verifier finished with 1 verified, 0 errors
--------------------- File HeapAxiom.bpl ----------------------------
-HeapAxiom.bpl(24,3): Error BP5001: This assertion might not hold.
+HeapAxiom.bpl(30,3): Error BP5001: This assertion might not hold.
Execution trace:
- HeapAxiom.bpl(13,3): anon0
+ HeapAxiom.bpl(19,3): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File Triggers0.bpl ----------------------------
-Triggers0.bpl(39,3): Error BP5001: This assertion might not hold.
+Triggers0.bpl(45,3): Error BP5001: This assertion might not hold.
Execution trace:
- Triggers0.bpl(39,3): anon0
-Triggers0.bpl(43,3): Error BP5001: This assertion might not hold.
+ Triggers0.bpl(45,3): anon0
+Triggers0.bpl(49,3): Error BP5001: This assertion might not hold.
Execution trace:
- Triggers0.bpl(39,3): anon0
+ Triggers0.bpl(45,3): anon0
Boogie program verifier finished with 1 verified, 2 errors
--------------------- File Triggers1.bpl ----------------------------
@@ -135,158 +135,158 @@ Boogie program verifier finished with 1 verified, 0 errors Boogie program verifier finished with 1 verified, 0 errors
--------------------- File Casts.bpl ----------------------------
-Casts.bpl(10,3): Error BP5001: This assertion might not hold.
+Casts.bpl(16,3): Error BP5001: This assertion might not hold.
Execution trace:
- Casts.bpl(6,3): anon0
+ Casts.bpl(12,3): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File BooleanQuantification.bpl ----------------------------
-BooleanQuantification.bpl(19,3): Error BP5001: This assertion might not hold.
+BooleanQuantification.bpl(25,3): Error BP5001: This assertion might not hold.
Execution trace:
- BooleanQuantification.bpl(18,3): anon0
-BooleanQuantification.bpl(31,3): Error BP5001: This assertion might not hold.
+ BooleanQuantification.bpl(24,3): anon0
+BooleanQuantification.bpl(37,3): Error BP5001: This assertion might not hold.
Execution trace:
- BooleanQuantification.bpl(29,3): anon0
+ BooleanQuantification.bpl(35,3): anon0
Boogie program verifier finished with 2 verified, 2 errors
--------------------- File EmptyList.bpl ----------------------------
-EmptyList.bpl(46,9): Warning: type parameter a is ambiguous, instantiating to List int
-EmptyList.bpl(28,3): Error BP5001: This assertion might not hold.
+EmptyList.bpl(52,9): Warning: type parameter a is ambiguous, instantiating to List int
+EmptyList.bpl(34,3): Error BP5001: This assertion might not hold.
Execution trace:
- EmptyList.bpl(26,5): anon0
-EmptyList.bpl(42,3): Error BP5001: This assertion might not hold.
+ EmptyList.bpl(32,5): anon0
+EmptyList.bpl(48,3): Error BP5001: This assertion might not hold.
Execution trace:
- EmptyList.bpl(26,5): anon0
-EmptyList.bpl(46,3): Error BP5001: This assertion might not hold.
+ EmptyList.bpl(32,5): anon0
+EmptyList.bpl(52,3): Error BP5001: This assertion might not hold.
Execution trace:
- EmptyList.bpl(46,3): anon0
+ EmptyList.bpl(52,3): anon0
Boogie program verifier finished with 0 verified, 3 errors
--------------------- File Boxing.bpl ----------------------------
-Boxing.bpl(19,3): Error BP5001: This assertion might not hold.
+Boxing.bpl(25,3): Error BP5001: This assertion might not hold.
Execution trace:
- Boxing.bpl(15,6): anon0
-Boxing.bpl(20,3): Error BP5001: This assertion might not hold.
+ Boxing.bpl(21,6): anon0
+Boxing.bpl(26,3): Error BP5001: This assertion might not hold.
Execution trace:
- Boxing.bpl(15,6): anon0
+ Boxing.bpl(21,6): anon0
Boogie program verifier finished with 0 verified, 2 errors
--------------------- File MapOutputTypeParams.bpl ----------------------------
-MapOutputTypeParams.bpl(29,3): Warning: type parameter a is ambiguous, instantiating to int
-MapOutputTypeParams.bpl(12,3): Error BP5001: This assertion might not hold.
+MapOutputTypeParams.bpl(35,3): Warning: type parameter a is ambiguous, instantiating to int
+MapOutputTypeParams.bpl(18,3): Error BP5001: This assertion might not hold.
Execution trace:
- MapOutputTypeParams.bpl(7,9): anon0
-MapOutputTypeParams.bpl(13,3): Error BP5001: This assertion might not hold.
+ MapOutputTypeParams.bpl(13,9): anon0
+MapOutputTypeParams.bpl(19,3): Error BP5001: This assertion might not hold.
Execution trace:
- MapOutputTypeParams.bpl(7,9): anon0
-MapOutputTypeParams.bpl(23,3): Error BP5001: This assertion might not hold.
+ MapOutputTypeParams.bpl(13,9): anon0
+MapOutputTypeParams.bpl(29,3): Error BP5001: This assertion might not hold.
Execution trace:
- MapOutputTypeParams.bpl(19,9): anon0
-MapOutputTypeParams.bpl(24,3): Error BP5001: This assertion might not hold.
+ MapOutputTypeParams.bpl(25,9): anon0
+MapOutputTypeParams.bpl(30,3): Error BP5001: This assertion might not hold.
Execution trace:
- MapOutputTypeParams.bpl(19,9): anon0
-MapOutputTypeParams.bpl(31,3): Error BP5001: This assertion might not hold.
+ MapOutputTypeParams.bpl(25,9): anon0
+MapOutputTypeParams.bpl(37,3): Error BP5001: This assertion might not hold.
Execution trace:
- MapOutputTypeParams.bpl(28,8): anon0
-MapOutputTypeParams.bpl(32,3): Error BP5001: This assertion might not hold.
+ MapOutputTypeParams.bpl(34,8): anon0
+MapOutputTypeParams.bpl(38,3): Error BP5001: This assertion might not hold.
Execution trace:
- MapOutputTypeParams.bpl(28,8): anon0
+ MapOutputTypeParams.bpl(34,8): anon0
Boogie program verifier finished with 0 verified, 6 errors
--------------------- File ParallelAssignment.bpl ----------------------------
-ParallelAssignment.bpl(26,3): Error BP5001: This assertion might not hold.
+ParallelAssignment.bpl(32,3): Error BP5001: This assertion might not hold.
Execution trace:
- ParallelAssignment.bpl(15,5): anon0
-ParallelAssignment.bpl(35,3): Error BP5001: This assertion might not hold.
+ ParallelAssignment.bpl(21,5): anon0
+ParallelAssignment.bpl(41,3): Error BP5001: This assertion might not hold.
Execution trace:
- ParallelAssignment.bpl(15,5): anon0
-ParallelAssignment.bpl(54,3): Error BP5001: This assertion might not hold.
+ ParallelAssignment.bpl(21,5): anon0
+ParallelAssignment.bpl(60,3): Error BP5001: This assertion might not hold.
Execution trace:
- ParallelAssignment.bpl(40,11): anon0
+ ParallelAssignment.bpl(46,11): anon0
Boogie program verifier finished with 0 verified, 3 errors
--------------------- File BooleanQuantification2.bpl ----------------------------
-BooleanQuantification2.bpl(13,3): Error BP5001: This assertion might not hold.
+BooleanQuantification2.bpl(19,3): Error BP5001: This assertion might not hold.
Execution trace:
- BooleanQuantification2.bpl(10,3): anon0
+ BooleanQuantification2.bpl(16,3): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File Flattening.bpl ----------------------------
-Flattening.bpl(12,3): Error BP5001: This assertion might not hold.
+Flattening.bpl(18,3): Error BP5001: This assertion might not hold.
Execution trace:
- Flattening.bpl(12,3): anon0
+ Flattening.bpl(18,3): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File Orderings.bpl ----------------------------
-Orderings.bpl(14,3): Error BP5001: This assertion might not hold.
+Orderings.bpl(20,3): Error BP5001: This assertion might not hold.
Execution trace:
- Orderings.bpl(9,3): anon0
+ Orderings.bpl(15,3): anon0
Boogie program verifier finished with 1 verified, 1 error
--------------------- File Orderings2.bpl ----------------------------
-Orderings2.bpl(17,3): Error BP5001: This assertion might not hold.
+Orderings2.bpl(23,3): Error BP5001: This assertion might not hold.
Execution trace:
- Orderings2.bpl(12,3): anon0
+ Orderings2.bpl(18,3): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File Orderings3.bpl ----------------------------
-Orderings3.bpl(29,3): Error BP5001: This assertion might not hold.
+Orderings3.bpl(35,3): Error BP5001: This assertion might not hold.
Execution trace:
- Orderings3.bpl(15,3): anon0
-Orderings3.bpl(34,3): Error BP5001: This assertion might not hold.
+ Orderings3.bpl(21,3): anon0
+Orderings3.bpl(40,3): Error BP5001: This assertion might not hold.
Execution trace:
- Orderings3.bpl(34,3): anon0
-Orderings3.bpl(36,3): Error BP5001: This assertion might not hold.
+ Orderings3.bpl(40,3): anon0
+Orderings3.bpl(42,3): Error BP5001: This assertion might not hold.
Execution trace:
- Orderings3.bpl(34,3): anon0
+ Orderings3.bpl(40,3): anon0
Boogie program verifier finished with 0 verified, 3 errors
--------------------- File Orderings4.bpl ----------------------------
-Orderings4.bpl(10,3): Error BP5001: This assertion might not hold.
+Orderings4.bpl(16,3): Error BP5001: This assertion might not hold.
Execution trace:
- Orderings4.bpl(9,3): anon0
+ Orderings4.bpl(15,3): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File EmptySetBug.bpl ----------------------------
-EmptySetBug.bpl(27,3): Error BP5001: This assertion might not hold.
+EmptySetBug.bpl(33,3): Error BP5001: This assertion might not hold.
Execution trace:
- EmptySetBug.bpl(25,5): anon0
-EmptySetBug.bpl(29,3): Error BP5001: This assertion might not hold.
+ EmptySetBug.bpl(31,5): anon0
+EmptySetBug.bpl(35,3): Error BP5001: This assertion might not hold.
Execution trace:
- EmptySetBug.bpl(25,5): anon0
+ EmptySetBug.bpl(31,5): anon0
Boogie program verifier finished with 0 verified, 2 errors
--------------------- File Coercions2.bpl ----------------------------
-Coercions2.bpl(12,23): Warning: type parameter a is ambiguous, instantiating to int
-Coercions2.bpl(18,3): Error BP5001: This assertion might not hold.
+Coercions2.bpl(18,23): Warning: type parameter a is ambiguous, instantiating to int
+Coercions2.bpl(24,3): Error BP5001: This assertion might not hold.
Execution trace:
- Coercions2.bpl(18,3): anon0
-Coercions2.bpl(23,3): Error BP5001: This assertion might not hold.
+ Coercions2.bpl(24,3): anon0
+Coercions2.bpl(29,3): Error BP5001: This assertion might not hold.
Execution trace:
- Coercions2.bpl(18,3): anon0
+ Coercions2.bpl(24,3): anon0
Boogie program verifier finished with 0 verified, 2 errors
--------------------- File MapAxiomsConsistency.bpl ----------------------------
-MapAxiomsConsistency.bpl(94,5): Error BP5001: This assertion might not hold.
+MapAxiomsConsistency.bpl(100,5): Error BP5001: This assertion might not hold.
Execution trace:
- MapAxiomsConsistency.bpl(79,13): anon0
+ MapAxiomsConsistency.bpl(85,13): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File LargeLiterals0.bpl ----------------------------
-LargeLiterals0.bpl(18,3): Error BP5001: This assertion might not hold.
+LargeLiterals0.bpl(24,3): Error BP5001: This assertion might not hold.
Execution trace:
- LargeLiterals0.bpl(7,5): anon0
+ LargeLiterals0.bpl(13,5): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File Real.bpl ----------------------------
-Real.bpl(26,5): Error BP5001: This assertion might not hold.
+Real.bpl(32,5): Error BP5001: This assertion might not hold.
Execution trace:
- Real.bpl(23,5): anon0
- Real.bpl(26,5): anon3_Then
-Real.bpl(41,5): Error BP5001: This assertion might not hold.
+ Real.bpl(29,5): anon0
+ Real.bpl(32,5): anon3_Then
+Real.bpl(47,5): Error BP5001: This assertion might not hold.
Execution trace:
- Real.bpl(34,3): anon0
- Real.bpl(41,5): anon3_Else
+ Real.bpl(40,3): anon0
+ Real.bpl(47,5): anon3_Else
Boogie program verifier finished with 2 verified, 2 errors
--------------------- File NameClash.bpl ----------------------------
@@ -296,9 +296,9 @@ Boogie program verifier finished with 1 verified, 0 errors Boogie program verifier finished with 1 verified, 0 errors
--------------------- File LargeLiterals0.bpl ----------------------------
-LargeLiterals0.bpl(18,3): Error BP5001: This assertion might not hold.
+LargeLiterals0.bpl(24,3): Error BP5001: This assertion might not hold.
Execution trace:
- LargeLiterals0.bpl(7,5): anon0
+ LargeLiterals0.bpl(13,5): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File LetSorting.bpl ----------------------------
@@ -306,272 +306,272 @@ Boogie program verifier finished with 0 verified, 1 error Boogie program verifier finished with 1 verified, 0 errors
--------------------- TypeEncoding p z3types ----------------------------
--------------------- File DisjointDomains.bpl ----------------------------
-DisjointDomains.bpl(14,5): Error BP5001: This assertion might not hold.
-Execution trace:
- DisjointDomains.bpl(11,3): start
-DisjointDomains.bpl(21,5): Error BP5001: This assertion might not hold.
+DisjointDomains.bpl(20,5): Error BP5001: This assertion might not hold.
Execution trace:
- DisjointDomains.bpl(20,3): start
+ DisjointDomains.bpl(17,3): start
DisjointDomains.bpl(27,5): Error BP5001: This assertion might not hold.
Execution trace:
DisjointDomains.bpl(26,3): start
+DisjointDomains.bpl(33,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ DisjointDomains.bpl(32,3): start
Boogie program verifier finished with 0 verified, 3 errors
--------------------- File DisjointDomains2.bpl ----------------------------
-DisjointDomains2.bpl(11,5): Error BP5001: This assertion might not hold.
+DisjointDomains2.bpl(17,5): Error BP5001: This assertion might not hold.
Execution trace:
- DisjointDomains2.bpl(9,3): start
-DisjointDomains2.bpl(18,5): Error BP5001: This assertion might not hold.
+ DisjointDomains2.bpl(15,3): start
+DisjointDomains2.bpl(24,5): Error BP5001: This assertion might not hold.
Execution trace:
- DisjointDomains2.bpl(16,3): start
-DisjointDomains2.bpl(32,5): Error BP5001: This assertion might not hold.
+ DisjointDomains2.bpl(22,3): start
+DisjointDomains2.bpl(38,5): Error BP5001: This assertion might not hold.
Execution trace:
- DisjointDomains2.bpl(30,3): start
-DisjointDomains2.bpl(39,5): Error BP5001: This assertion might not hold.
+ DisjointDomains2.bpl(36,3): start
+DisjointDomains2.bpl(45,5): Error BP5001: This assertion might not hold.
Execution trace:
- DisjointDomains2.bpl(37,3): start
-DisjointDomains2.bpl(49,5): Error BP5001: This assertion might not hold.
+ DisjointDomains2.bpl(43,3): start
+DisjointDomains2.bpl(55,5): Error BP5001: This assertion might not hold.
Execution trace:
- DisjointDomains2.bpl(45,3): start
-DisjointDomains2.bpl(63,5): Error BP5001: This assertion might not hold.
+ DisjointDomains2.bpl(51,3): start
+DisjointDomains2.bpl(69,5): Error BP5001: This assertion might not hold.
Execution trace:
- DisjointDomains2.bpl(58,3): start
+ DisjointDomains2.bpl(64,3): start
Boogie program verifier finished with 0 verified, 6 errors
--------------------- File FunAxioms.bpl ----------------------------
-FunAxioms.bpl(30,3): Error BP5001: This assertion might not hold.
+FunAxioms.bpl(36,3): Error BP5001: This assertion might not hold.
Execution trace:
- FunAxioms.bpl(18,3): anon0
+ FunAxioms.bpl(24,3): anon0
Boogie program verifier finished with 1 verified, 1 error
--------------------- File FunAxioms2.bpl ----------------------------
-FunAxioms2.bpl(20,3): Error BP5001: This assertion might not hold.
+FunAxioms2.bpl(26,3): Error BP5001: This assertion might not hold.
Execution trace:
- FunAxioms2.bpl(16,5): anon0
+ FunAxioms2.bpl(22,5): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File PolyList.bpl ----------------------------
-PolyList.bpl(42,3): Error BP5001: This assertion might not hold.
+PolyList.bpl(48,3): Error BP5001: This assertion might not hold.
Execution trace:
- PolyList.bpl(27,7): anon0
-PolyList.bpl(60,3): Error BP5001: This assertion might not hold.
+ PolyList.bpl(33,7): anon0
+PolyList.bpl(66,3): Error BP5001: This assertion might not hold.
Execution trace:
- PolyList.bpl(49,7): anon0
+ PolyList.bpl(55,7): anon0
Boogie program verifier finished with 0 verified, 2 errors
--------------------- File Maps0.bpl ----------------------------
-Maps0.bpl(23,3): Error BP5001: This assertion might not hold.
+Maps0.bpl(29,3): Error BP5001: This assertion might not hold.
Execution trace:
- Maps0.bpl(14,3): anon0
-Maps0.bpl(32,3): Error BP5001: This assertion might not hold.
+ Maps0.bpl(20,3): anon0
+Maps0.bpl(38,3): Error BP5001: This assertion might not hold.
Execution trace:
- Maps0.bpl(32,3): anon0
-Maps0.bpl(53,3): Error BP5001: This assertion might not hold.
+ Maps0.bpl(38,3): anon0
+Maps0.bpl(59,3): Error BP5001: This assertion might not hold.
Execution trace:
- Maps0.bpl(41,9): anon0
+ Maps0.bpl(47,9): anon0
Boogie program verifier finished with 0 verified, 3 errors
--------------------- File Maps1.bpl ----------------------------
-Maps1.bpl(31,3): Error BP5001: This assertion might not hold.
+Maps1.bpl(37,3): Error BP5001: This assertion might not hold.
Execution trace:
- Maps1.bpl(19,3): anon0
+ Maps1.bpl(25,3): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File InterestingExamples0.bpl ----------------------------
Boogie program verifier finished with 1 verified, 0 errors
--------------------- File InterestingExamples1.bpl ----------------------------
-InterestingExamples1.bpl(22,3): Error BP5001: This assertion might not hold.
+InterestingExamples1.bpl(28,3): Error BP5001: This assertion might not hold.
Execution trace:
- InterestingExamples1.bpl(13,5): anon0
+ InterestingExamples1.bpl(19,5): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File InterestingExamples2.bpl ----------------------------
Boogie program verifier finished with 1 verified, 0 errors
--------------------- File InterestingExamples3.bpl ----------------------------
-InterestingExamples3.bpl(15,2): Error BP5001: This assertion might not hold.
+InterestingExamples3.bpl(21,2): Error BP5001: This assertion might not hold.
Execution trace:
- InterestingExamples3.bpl(13,2): anon0
+ InterestingExamples3.bpl(19,2): anon0
Boogie program verifier finished with 2 verified, 1 error
--------------------- File InterestingExamples4.bpl ----------------------------
-InterestingExamples4.bpl(39,3): Error BP5001: This assertion might not hold.
+InterestingExamples4.bpl(45,3): Error BP5001: This assertion might not hold.
Execution trace:
- InterestingExamples4.bpl(36,3): anon0
+ InterestingExamples4.bpl(42,3): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File InterestingExamples5.bpl ----------------------------
Boogie program verifier finished with 1 verified, 0 errors
--------------------- File Colors.bpl ----------------------------
-Colors.bpl(13,3): Error BP5001: This assertion might not hold.
+Colors.bpl(19,3): Error BP5001: This assertion might not hold.
Execution trace:
- Colors.bpl(12,3): anon0
-Colors.bpl(20,3): Error BP5001: This assertion might not hold.
+ Colors.bpl(18,3): anon0
+Colors.bpl(26,3): Error BP5001: This assertion might not hold.
Execution trace:
- Colors.bpl(19,3): anon0
+ Colors.bpl(25,3): anon0
Boogie program verifier finished with 0 verified, 2 errors
--------------------- File HeapAbstraction.bpl ----------------------------
-HeapAbstraction.bpl(15,3): Error BP5001: This assertion might not hold.
+HeapAbstraction.bpl(21,3): Error BP5001: This assertion might not hold.
Execution trace:
- HeapAbstraction.bpl(14,3): anon0
+ HeapAbstraction.bpl(20,3): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File HeapAxiom.bpl ----------------------------
-HeapAxiom.bpl(24,3): Error BP5001: This assertion might not hold.
+HeapAxiom.bpl(30,3): Error BP5001: This assertion might not hold.
Execution trace:
- HeapAxiom.bpl(13,3): anon0
+ HeapAxiom.bpl(19,3): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File Triggers0.bpl ----------------------------
-Triggers0.bpl(39,3): Error BP5001: This assertion might not hold.
+Triggers0.bpl(45,3): Error BP5001: This assertion might not hold.
Execution trace:
- Triggers0.bpl(39,3): anon0
-Triggers0.bpl(43,3): Error BP5001: This assertion might not hold.
+ Triggers0.bpl(45,3): anon0
+Triggers0.bpl(49,3): Error BP5001: This assertion might not hold.
Execution trace:
- Triggers0.bpl(39,3): anon0
+ Triggers0.bpl(45,3): anon0
Boogie program verifier finished with 1 verified, 2 errors
--------------------- File Triggers1.bpl ----------------------------
-Triggers1.bpl(16,3): Error BP5001: This assertion might not hold.
+Triggers1.bpl(22,3): Error BP5001: This assertion might not hold.
Execution trace:
- Triggers1.bpl(12,3): anon0
+ Triggers1.bpl(18,3): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File Keywords.bpl ----------------------------
Boogie program verifier finished with 1 verified, 0 errors
--------------------- File Casts.bpl ----------------------------
-Casts.bpl(10,3): Error BP5001: This assertion might not hold.
+Casts.bpl(16,3): Error BP5001: This assertion might not hold.
Execution trace:
- Casts.bpl(6,3): anon0
+ Casts.bpl(12,3): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File BooleanQuantification.bpl ----------------------------
-BooleanQuantification.bpl(19,3): Error BP5001: This assertion might not hold.
+BooleanQuantification.bpl(25,3): Error BP5001: This assertion might not hold.
Execution trace:
- BooleanQuantification.bpl(18,3): anon0
-BooleanQuantification.bpl(31,3): Error BP5001: This assertion might not hold.
+ BooleanQuantification.bpl(24,3): anon0
+BooleanQuantification.bpl(37,3): Error BP5001: This assertion might not hold.
Execution trace:
- BooleanQuantification.bpl(29,3): anon0
+ BooleanQuantification.bpl(35,3): anon0
Boogie program verifier finished with 2 verified, 2 errors
--------------------- File EmptyList.bpl ----------------------------
-EmptyList.bpl(46,9): Warning: type parameter a is ambiguous, instantiating to List int
-EmptyList.bpl(42,3): Error BP5001: This assertion might not hold.
+EmptyList.bpl(52,9): Warning: type parameter a is ambiguous, instantiating to List int
+EmptyList.bpl(48,3): Error BP5001: This assertion might not hold.
Execution trace:
- EmptyList.bpl(26,5): anon0
+ EmptyList.bpl(32,5): anon0
Boogie program verifier finished with 1 verified, 1 error
--------------------- File Boxing.bpl ----------------------------
-Boxing.bpl(20,3): Error BP5001: This assertion might not hold.
+Boxing.bpl(26,3): Error BP5001: This assertion might not hold.
Execution trace:
- Boxing.bpl(15,6): anon0
+ Boxing.bpl(21,6): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File MapOutputTypeParams.bpl ----------------------------
-MapOutputTypeParams.bpl(29,3): Warning: type parameter a is ambiguous, instantiating to int
-MapOutputTypeParams.bpl(13,3): Error BP5001: This assertion might not hold.
+MapOutputTypeParams.bpl(35,3): Warning: type parameter a is ambiguous, instantiating to int
+MapOutputTypeParams.bpl(19,3): Error BP5001: This assertion might not hold.
Execution trace:
- MapOutputTypeParams.bpl(7,9): anon0
-MapOutputTypeParams.bpl(24,3): Error BP5001: This assertion might not hold.
+ MapOutputTypeParams.bpl(13,9): anon0
+MapOutputTypeParams.bpl(30,3): Error BP5001: This assertion might not hold.
Execution trace:
- MapOutputTypeParams.bpl(19,9): anon0
-MapOutputTypeParams.bpl(32,3): Error BP5001: This assertion might not hold.
+ MapOutputTypeParams.bpl(25,9): anon0
+MapOutputTypeParams.bpl(38,3): Error BP5001: This assertion might not hold.
Execution trace:
- MapOutputTypeParams.bpl(28,8): anon0
+ MapOutputTypeParams.bpl(34,8): anon0
Boogie program verifier finished with 0 verified, 3 errors
--------------------- File ParallelAssignment.bpl ----------------------------
-ParallelAssignment.bpl(26,3): Error BP5001: This assertion might not hold.
+ParallelAssignment.bpl(32,3): Error BP5001: This assertion might not hold.
Execution trace:
- ParallelAssignment.bpl(15,5): anon0
-ParallelAssignment.bpl(35,3): Error BP5001: This assertion might not hold.
+ ParallelAssignment.bpl(21,5): anon0
+ParallelAssignment.bpl(41,3): Error BP5001: This assertion might not hold.
Execution trace:
- ParallelAssignment.bpl(15,5): anon0
-ParallelAssignment.bpl(54,3): Error BP5001: This assertion might not hold.
+ ParallelAssignment.bpl(21,5): anon0
+ParallelAssignment.bpl(60,3): Error BP5001: This assertion might not hold.
Execution trace:
- ParallelAssignment.bpl(40,11): anon0
+ ParallelAssignment.bpl(46,11): anon0
Boogie program verifier finished with 0 verified, 3 errors
--------------------- File BooleanQuantification2.bpl ----------------------------
-BooleanQuantification2.bpl(13,3): Error BP5001: This assertion might not hold.
+BooleanQuantification2.bpl(19,3): Error BP5001: This assertion might not hold.
Execution trace:
- BooleanQuantification2.bpl(10,3): anon0
+ BooleanQuantification2.bpl(16,3): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File Flattening.bpl ----------------------------
-Flattening.bpl(12,3): Error BP5001: This assertion might not hold.
+Flattening.bpl(18,3): Error BP5001: This assertion might not hold.
Execution trace:
- Flattening.bpl(12,3): anon0
+ Flattening.bpl(18,3): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File Orderings.bpl ----------------------------
-Orderings.bpl(14,3): Error BP5001: This assertion might not hold.
+Orderings.bpl(20,3): Error BP5001: This assertion might not hold.
Execution trace:
- Orderings.bpl(9,3): anon0
+ Orderings.bpl(15,3): anon0
Boogie program verifier finished with 1 verified, 1 error
--------------------- File Orderings2.bpl ----------------------------
-Orderings2.bpl(17,3): Error BP5001: This assertion might not hold.
+Orderings2.bpl(23,3): Error BP5001: This assertion might not hold.
Execution trace:
- Orderings2.bpl(12,3): anon0
+ Orderings2.bpl(18,3): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File Orderings3.bpl ----------------------------
-Orderings3.bpl(29,3): Error BP5001: This assertion might not hold.
+Orderings3.bpl(35,3): Error BP5001: This assertion might not hold.
Execution trace:
- Orderings3.bpl(15,3): anon0
-Orderings3.bpl(34,3): Error BP5001: This assertion might not hold.
+ Orderings3.bpl(21,3): anon0
+Orderings3.bpl(40,3): Error BP5001: This assertion might not hold.
Execution trace:
- Orderings3.bpl(34,3): anon0
-Orderings3.bpl(36,3): Error BP5001: This assertion might not hold.
+ Orderings3.bpl(40,3): anon0
+Orderings3.bpl(42,3): Error BP5001: This assertion might not hold.
Execution trace:
- Orderings3.bpl(34,3): anon0
+ Orderings3.bpl(40,3): anon0
Boogie program verifier finished with 0 verified, 3 errors
--------------------- File Orderings4.bpl ----------------------------
-Orderings4.bpl(10,3): Error BP5001: This assertion might not hold.
+Orderings4.bpl(16,3): Error BP5001: This assertion might not hold.
Execution trace:
- Orderings4.bpl(9,3): anon0
+ Orderings4.bpl(15,3): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File EmptySetBug.bpl ----------------------------
-EmptySetBug.bpl(29,3): Error BP5001: This assertion might not hold.
+EmptySetBug.bpl(35,3): Error BP5001: This assertion might not hold.
Execution trace:
- EmptySetBug.bpl(25,5): anon0
+ EmptySetBug.bpl(31,5): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File Coercions2.bpl ----------------------------
-Coercions2.bpl(12,23): Warning: type parameter a is ambiguous, instantiating to int
-Coercions2.bpl(23,3): Error BP5001: This assertion might not hold.
+Coercions2.bpl(18,23): Warning: type parameter a is ambiguous, instantiating to int
+Coercions2.bpl(29,3): Error BP5001: This assertion might not hold.
Execution trace:
- Coercions2.bpl(18,3): anon0
+ Coercions2.bpl(24,3): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File MapAxiomsConsistency.bpl ----------------------------
-MapAxiomsConsistency.bpl(94,5): Error BP5001: This assertion might not hold.
+MapAxiomsConsistency.bpl(100,5): Error BP5001: This assertion might not hold.
Execution trace:
- MapAxiomsConsistency.bpl(79,13): anon0
+ MapAxiomsConsistency.bpl(85,13): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File LargeLiterals0.bpl ----------------------------
-LargeLiterals0.bpl(18,3): Error BP5001: This assertion might not hold.
+LargeLiterals0.bpl(24,3): Error BP5001: This assertion might not hold.
Execution trace:
- LargeLiterals0.bpl(7,5): anon0
+ LargeLiterals0.bpl(13,5): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File Real.bpl ----------------------------
-Real.bpl(26,5): Error BP5001: This assertion might not hold.
+Real.bpl(32,5): Error BP5001: This assertion might not hold.
Execution trace:
- Real.bpl(23,5): anon0
- Real.bpl(26,5): anon3_Then
-Real.bpl(41,5): Error BP5001: This assertion might not hold.
+ Real.bpl(29,5): anon0
+ Real.bpl(32,5): anon3_Then
+Real.bpl(47,5): Error BP5001: This assertion might not hold.
Execution trace:
- Real.bpl(34,3): anon0
- Real.bpl(41,5): anon3_Else
+ Real.bpl(40,3): anon0
+ Real.bpl(47,5): anon3_Else
Boogie program verifier finished with 2 verified, 2 errors
--------------------- File NameClash.bpl ----------------------------
@@ -581,9 +581,9 @@ Boogie program verifier finished with 1 verified, 0 errors Boogie program verifier finished with 1 verified, 0 errors
--------------------- File LargeLiterals0.bpl ----------------------------
-LargeLiterals0.bpl(18,3): Error BP5001: This assertion might not hold.
+LargeLiterals0.bpl(24,3): Error BP5001: This assertion might not hold.
Execution trace:
- LargeLiterals0.bpl(7,5): anon0
+ LargeLiterals0.bpl(13,5): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File LetSorting.bpl ----------------------------
@@ -591,275 +591,275 @@ Boogie program verifier finished with 0 verified, 1 error Boogie program verifier finished with 1 verified, 0 errors
--------------------- TypeEncoding a z3types ----------------------------
--------------------- File DisjointDomains.bpl ----------------------------
-DisjointDomains.bpl(14,5): Error BP5001: This assertion might not hold.
-Execution trace:
- DisjointDomains.bpl(11,3): start
-DisjointDomains.bpl(21,5): Error BP5001: This assertion might not hold.
+DisjointDomains.bpl(20,5): Error BP5001: This assertion might not hold.
Execution trace:
- DisjointDomains.bpl(20,3): start
+ DisjointDomains.bpl(17,3): start
DisjointDomains.bpl(27,5): Error BP5001: This assertion might not hold.
Execution trace:
DisjointDomains.bpl(26,3): start
+DisjointDomains.bpl(33,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ DisjointDomains.bpl(32,3): start
Boogie program verifier finished with 0 verified, 3 errors
--------------------- File DisjointDomains2.bpl ----------------------------
-DisjointDomains2.bpl(11,5): Error BP5001: This assertion might not hold.
+DisjointDomains2.bpl(17,5): Error BP5001: This assertion might not hold.
Execution trace:
- DisjointDomains2.bpl(9,3): start
-DisjointDomains2.bpl(18,5): Error BP5001: This assertion might not hold.
+ DisjointDomains2.bpl(15,3): start
+DisjointDomains2.bpl(24,5): Error BP5001: This assertion might not hold.
Execution trace:
- DisjointDomains2.bpl(16,3): start
-DisjointDomains2.bpl(32,5): Error BP5001: This assertion might not hold.
+ DisjointDomains2.bpl(22,3): start
+DisjointDomains2.bpl(38,5): Error BP5001: This assertion might not hold.
Execution trace:
- DisjointDomains2.bpl(30,3): start
-DisjointDomains2.bpl(39,5): Error BP5001: This assertion might not hold.
+ DisjointDomains2.bpl(36,3): start
+DisjointDomains2.bpl(45,5): Error BP5001: This assertion might not hold.
Execution trace:
- DisjointDomains2.bpl(37,3): start
-DisjointDomains2.bpl(49,5): Error BP5001: This assertion might not hold.
+ DisjointDomains2.bpl(43,3): start
+DisjointDomains2.bpl(55,5): Error BP5001: This assertion might not hold.
Execution trace:
- DisjointDomains2.bpl(45,3): start
-DisjointDomains2.bpl(63,5): Error BP5001: This assertion might not hold.
+ DisjointDomains2.bpl(51,3): start
+DisjointDomains2.bpl(69,5): Error BP5001: This assertion might not hold.
Execution trace:
- DisjointDomains2.bpl(58,3): start
+ DisjointDomains2.bpl(64,3): start
Boogie program verifier finished with 0 verified, 6 errors
--------------------- File FunAxioms.bpl ----------------------------
-FunAxioms.bpl(30,3): Error BP5001: This assertion might not hold.
+FunAxioms.bpl(36,3): Error BP5001: This assertion might not hold.
Execution trace:
- FunAxioms.bpl(18,3): anon0
+ FunAxioms.bpl(24,3): anon0
Boogie program verifier finished with 1 verified, 1 error
--------------------- File FunAxioms2.bpl ----------------------------
-FunAxioms2.bpl(20,3): Error BP5001: This assertion might not hold.
+FunAxioms2.bpl(26,3): Error BP5001: This assertion might not hold.
Execution trace:
- FunAxioms2.bpl(16,5): anon0
+ FunAxioms2.bpl(22,5): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File PolyList.bpl ----------------------------
-PolyList.bpl(42,3): Error BP5001: This assertion might not hold.
+PolyList.bpl(48,3): Error BP5001: This assertion might not hold.
Execution trace:
- PolyList.bpl(27,7): anon0
-PolyList.bpl(60,3): Error BP5001: This assertion might not hold.
+ PolyList.bpl(33,7): anon0
+PolyList.bpl(66,3): Error BP5001: This assertion might not hold.
Execution trace:
- PolyList.bpl(49,7): anon0
+ PolyList.bpl(55,7): anon0
Boogie program verifier finished with 0 verified, 2 errors
--------------------- File Maps0.bpl ----------------------------
-Maps0.bpl(23,3): Error BP5001: This assertion might not hold.
+Maps0.bpl(29,3): Error BP5001: This assertion might not hold.
Execution trace:
- Maps0.bpl(14,3): anon0
-Maps0.bpl(32,3): Error BP5001: This assertion might not hold.
+ Maps0.bpl(20,3): anon0
+Maps0.bpl(38,3): Error BP5001: This assertion might not hold.
Execution trace:
- Maps0.bpl(32,3): anon0
-Maps0.bpl(53,3): Error BP5001: This assertion might not hold.
+ Maps0.bpl(38,3): anon0
+Maps0.bpl(59,3): Error BP5001: This assertion might not hold.
Execution trace:
- Maps0.bpl(41,9): anon0
+ Maps0.bpl(47,9): anon0
Boogie program verifier finished with 0 verified, 3 errors
--------------------- File Maps1.bpl ----------------------------
-Maps1.bpl(31,3): Error BP5001: This assertion might not hold.
+Maps1.bpl(37,3): Error BP5001: This assertion might not hold.
Execution trace:
- Maps1.bpl(19,3): anon0
+ Maps1.bpl(25,3): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File InterestingExamples0.bpl ----------------------------
Boogie program verifier finished with 1 verified, 0 errors
--------------------- File InterestingExamples1.bpl ----------------------------
-InterestingExamples1.bpl(22,3): Error BP5001: This assertion might not hold.
+InterestingExamples1.bpl(28,3): Error BP5001: This assertion might not hold.
Execution trace:
- InterestingExamples1.bpl(13,5): anon0
+ InterestingExamples1.bpl(19,5): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File InterestingExamples2.bpl ----------------------------
Boogie program verifier finished with 1 verified, 0 errors
--------------------- File InterestingExamples3.bpl ----------------------------
-InterestingExamples3.bpl(15,2): Error BP5001: This assertion might not hold.
+InterestingExamples3.bpl(21,2): Error BP5001: This assertion might not hold.
Execution trace:
- InterestingExamples3.bpl(13,2): anon0
+ InterestingExamples3.bpl(19,2): anon0
Boogie program verifier finished with 2 verified, 1 error
--------------------- File InterestingExamples4.bpl ----------------------------
-InterestingExamples4.bpl(36,3): Error BP5001: This assertion might not hold.
+InterestingExamples4.bpl(42,3): Error BP5001: This assertion might not hold.
Execution trace:
- InterestingExamples4.bpl(36,3): anon0
-InterestingExamples4.bpl(39,3): Error BP5001: This assertion might not hold.
+ InterestingExamples4.bpl(42,3): anon0
+InterestingExamples4.bpl(45,3): Error BP5001: This assertion might not hold.
Execution trace:
- InterestingExamples4.bpl(36,3): anon0
+ InterestingExamples4.bpl(42,3): anon0
Boogie program verifier finished with 0 verified, 2 errors
--------------------- File InterestingExamples5.bpl ----------------------------
Boogie program verifier finished with 1 verified, 0 errors
--------------------- File Colors.bpl ----------------------------
-Colors.bpl(13,3): Error BP5001: This assertion might not hold.
+Colors.bpl(19,3): Error BP5001: This assertion might not hold.
Execution trace:
- Colors.bpl(12,3): anon0
-Colors.bpl(20,3): Error BP5001: This assertion might not hold.
+ Colors.bpl(18,3): anon0
+Colors.bpl(26,3): Error BP5001: This assertion might not hold.
Execution trace:
- Colors.bpl(19,3): anon0
+ Colors.bpl(25,3): anon0
Boogie program verifier finished with 0 verified, 2 errors
--------------------- File HeapAbstraction.bpl ----------------------------
-HeapAbstraction.bpl(15,3): Error BP5001: This assertion might not hold.
+HeapAbstraction.bpl(21,3): Error BP5001: This assertion might not hold.
Execution trace:
- HeapAbstraction.bpl(14,3): anon0
+ HeapAbstraction.bpl(20,3): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File HeapAxiom.bpl ----------------------------
-HeapAxiom.bpl(24,3): Error BP5001: This assertion might not hold.
+HeapAxiom.bpl(30,3): Error BP5001: This assertion might not hold.
Execution trace:
- HeapAxiom.bpl(13,3): anon0
+ HeapAxiom.bpl(19,3): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File Triggers0.bpl ----------------------------
-Triggers0.bpl(39,3): Error BP5001: This assertion might not hold.
+Triggers0.bpl(45,3): Error BP5001: This assertion might not hold.
Execution trace:
- Triggers0.bpl(39,3): anon0
-Triggers0.bpl(43,3): Error BP5001: This assertion might not hold.
+ Triggers0.bpl(45,3): anon0
+Triggers0.bpl(49,3): Error BP5001: This assertion might not hold.
Execution trace:
- Triggers0.bpl(39,3): anon0
+ Triggers0.bpl(45,3): anon0
Boogie program verifier finished with 1 verified, 2 errors
--------------------- File Triggers1.bpl ----------------------------
-Triggers1.bpl(16,3): Error BP5001: This assertion might not hold.
+Triggers1.bpl(22,3): Error BP5001: This assertion might not hold.
Execution trace:
- Triggers1.bpl(12,3): anon0
+ Triggers1.bpl(18,3): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File Keywords.bpl ----------------------------
Boogie program verifier finished with 1 verified, 0 errors
--------------------- File Casts.bpl ----------------------------
-Casts.bpl(10,3): Error BP5001: This assertion might not hold.
+Casts.bpl(16,3): Error BP5001: This assertion might not hold.
Execution trace:
- Casts.bpl(6,3): anon0
+ Casts.bpl(12,3): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File BooleanQuantification.bpl ----------------------------
-BooleanQuantification.bpl(19,3): Error BP5001: This assertion might not hold.
+BooleanQuantification.bpl(25,3): Error BP5001: This assertion might not hold.
Execution trace:
- BooleanQuantification.bpl(18,3): anon0
-BooleanQuantification.bpl(31,3): Error BP5001: This assertion might not hold.
+ BooleanQuantification.bpl(24,3): anon0
+BooleanQuantification.bpl(37,3): Error BP5001: This assertion might not hold.
Execution trace:
- BooleanQuantification.bpl(29,3): anon0
+ BooleanQuantification.bpl(35,3): anon0
Boogie program verifier finished with 2 verified, 2 errors
--------------------- File EmptyList.bpl ----------------------------
-EmptyList.bpl(46,9): Warning: type parameter a is ambiguous, instantiating to List int
-EmptyList.bpl(42,3): Error BP5001: This assertion might not hold.
+EmptyList.bpl(52,9): Warning: type parameter a is ambiguous, instantiating to List int
+EmptyList.bpl(48,3): Error BP5001: This assertion might not hold.
Execution trace:
- EmptyList.bpl(26,5): anon0
+ EmptyList.bpl(32,5): anon0
Boogie program verifier finished with 1 verified, 1 error
--------------------- File Boxing.bpl ----------------------------
-Boxing.bpl(20,3): Error BP5001: This assertion might not hold.
+Boxing.bpl(26,3): Error BP5001: This assertion might not hold.
Execution trace:
- Boxing.bpl(15,6): anon0
+ Boxing.bpl(21,6): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File MapOutputTypeParams.bpl ----------------------------
-MapOutputTypeParams.bpl(29,3): Warning: type parameter a is ambiguous, instantiating to int
-MapOutputTypeParams.bpl(13,3): Error BP5001: This assertion might not hold.
+MapOutputTypeParams.bpl(35,3): Warning: type parameter a is ambiguous, instantiating to int
+MapOutputTypeParams.bpl(19,3): Error BP5001: This assertion might not hold.
Execution trace:
- MapOutputTypeParams.bpl(7,9): anon0
-MapOutputTypeParams.bpl(24,3): Error BP5001: This assertion might not hold.
+ MapOutputTypeParams.bpl(13,9): anon0
+MapOutputTypeParams.bpl(30,3): Error BP5001: This assertion might not hold.
Execution trace:
- MapOutputTypeParams.bpl(19,9): anon0
-MapOutputTypeParams.bpl(32,3): Error BP5001: This assertion might not hold.
+ MapOutputTypeParams.bpl(25,9): anon0
+MapOutputTypeParams.bpl(38,3): Error BP5001: This assertion might not hold.
Execution trace:
- MapOutputTypeParams.bpl(28,8): anon0
+ MapOutputTypeParams.bpl(34,8): anon0
Boogie program verifier finished with 0 verified, 3 errors
--------------------- File ParallelAssignment.bpl ----------------------------
-ParallelAssignment.bpl(26,3): Error BP5001: This assertion might not hold.
+ParallelAssignment.bpl(32,3): Error BP5001: This assertion might not hold.
Execution trace:
- ParallelAssignment.bpl(15,5): anon0
-ParallelAssignment.bpl(35,3): Error BP5001: This assertion might not hold.
+ ParallelAssignment.bpl(21,5): anon0
+ParallelAssignment.bpl(41,3): Error BP5001: This assertion might not hold.
Execution trace:
- ParallelAssignment.bpl(15,5): anon0
-ParallelAssignment.bpl(54,3): Error BP5001: This assertion might not hold.
+ ParallelAssignment.bpl(21,5): anon0
+ParallelAssignment.bpl(60,3): Error BP5001: This assertion might not hold.
Execution trace:
- ParallelAssignment.bpl(40,11): anon0
+ ParallelAssignment.bpl(46,11): anon0
Boogie program verifier finished with 0 verified, 3 errors
--------------------- File BooleanQuantification2.bpl ----------------------------
-BooleanQuantification2.bpl(13,3): Error BP5001: This assertion might not hold.
+BooleanQuantification2.bpl(19,3): Error BP5001: This assertion might not hold.
Execution trace:
- BooleanQuantification2.bpl(10,3): anon0
+ BooleanQuantification2.bpl(16,3): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File Flattening.bpl ----------------------------
-Flattening.bpl(12,3): Error BP5001: This assertion might not hold.
+Flattening.bpl(18,3): Error BP5001: This assertion might not hold.
Execution trace:
- Flattening.bpl(12,3): anon0
+ Flattening.bpl(18,3): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File Orderings.bpl ----------------------------
-Orderings.bpl(14,3): Error BP5001: This assertion might not hold.
+Orderings.bpl(20,3): Error BP5001: This assertion might not hold.
Execution trace:
- Orderings.bpl(9,3): anon0
+ Orderings.bpl(15,3): anon0
Boogie program verifier finished with 1 verified, 1 error
--------------------- File Orderings2.bpl ----------------------------
-Orderings2.bpl(17,3): Error BP5001: This assertion might not hold.
+Orderings2.bpl(23,3): Error BP5001: This assertion might not hold.
Execution trace:
- Orderings2.bpl(12,3): anon0
+ Orderings2.bpl(18,3): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File Orderings3.bpl ----------------------------
-Orderings3.bpl(29,3): Error BP5001: This assertion might not hold.
+Orderings3.bpl(35,3): Error BP5001: This assertion might not hold.
Execution trace:
- Orderings3.bpl(15,3): anon0
-Orderings3.bpl(34,3): Error BP5001: This assertion might not hold.
+ Orderings3.bpl(21,3): anon0
+Orderings3.bpl(40,3): Error BP5001: This assertion might not hold.
Execution trace:
- Orderings3.bpl(34,3): anon0
-Orderings3.bpl(36,3): Error BP5001: This assertion might not hold.
+ Orderings3.bpl(40,3): anon0
+Orderings3.bpl(42,3): Error BP5001: This assertion might not hold.
Execution trace:
- Orderings3.bpl(34,3): anon0
+ Orderings3.bpl(40,3): anon0
Boogie program verifier finished with 0 verified, 3 errors
--------------------- File Orderings4.bpl ----------------------------
-Orderings4.bpl(10,3): Error BP5001: This assertion might not hold.
+Orderings4.bpl(16,3): Error BP5001: This assertion might not hold.
Execution trace:
- Orderings4.bpl(9,3): anon0
+ Orderings4.bpl(15,3): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File EmptySetBug.bpl ----------------------------
-EmptySetBug.bpl(29,3): Error BP5001: This assertion might not hold.
+EmptySetBug.bpl(35,3): Error BP5001: This assertion might not hold.
Execution trace:
- EmptySetBug.bpl(25,5): anon0
+ EmptySetBug.bpl(31,5): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File Coercions2.bpl ----------------------------
-Coercions2.bpl(12,23): Warning: type parameter a is ambiguous, instantiating to int
-Coercions2.bpl(23,3): Error BP5001: This assertion might not hold.
+Coercions2.bpl(18,23): Warning: type parameter a is ambiguous, instantiating to int
+Coercions2.bpl(29,3): Error BP5001: This assertion might not hold.
Execution trace:
- Coercions2.bpl(18,3): anon0
+ Coercions2.bpl(24,3): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File MapAxiomsConsistency.bpl ----------------------------
-MapAxiomsConsistency.bpl(94,5): Error BP5001: This assertion might not hold.
+MapAxiomsConsistency.bpl(100,5): Error BP5001: This assertion might not hold.
Execution trace:
- MapAxiomsConsistency.bpl(79,13): anon0
+ MapAxiomsConsistency.bpl(85,13): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File LargeLiterals0.bpl ----------------------------
-LargeLiterals0.bpl(18,3): Error BP5001: This assertion might not hold.
+LargeLiterals0.bpl(24,3): Error BP5001: This assertion might not hold.
Execution trace:
- LargeLiterals0.bpl(7,5): anon0
+ LargeLiterals0.bpl(13,5): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File Real.bpl ----------------------------
-Real.bpl(26,5): Error BP5001: This assertion might not hold.
+Real.bpl(32,5): Error BP5001: This assertion might not hold.
Execution trace:
- Real.bpl(23,5): anon0
- Real.bpl(26,5): anon3_Then
-Real.bpl(41,5): Error BP5001: This assertion might not hold.
+ Real.bpl(29,5): anon0
+ Real.bpl(32,5): anon3_Then
+Real.bpl(47,5): Error BP5001: This assertion might not hold.
Execution trace:
- Real.bpl(34,3): anon0
- Real.bpl(41,5): anon3_Else
+ Real.bpl(40,3): anon0
+ Real.bpl(47,5): anon3_Else
Boogie program verifier finished with 2 verified, 2 errors
--------------------- File NameClash.bpl ----------------------------
@@ -869,9 +869,9 @@ Boogie program verifier finished with 1 verified, 0 errors Boogie program verifier finished with 1 verified, 0 errors
--------------------- File LargeLiterals0.bpl ----------------------------
-LargeLiterals0.bpl(18,3): Error BP5001: This assertion might not hold.
+LargeLiterals0.bpl(24,3): Error BP5001: This assertion might not hold.
Execution trace:
- LargeLiterals0.bpl(7,5): anon0
+ LargeLiterals0.bpl(13,5): anon0
Boogie program verifier finished with 0 verified, 1 error
--------------------- File LetSorting.bpl ----------------------------
diff --git a/Test/test21/BooleanQuantification.bpl b/Test/test21/BooleanQuantification.bpl index 52416e9d..527ab174 100644 --- a/Test/test21/BooleanQuantification.bpl +++ b/Test/test21/BooleanQuantification.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
diff --git a/Test/test21/BooleanQuantification.bpl.a.expect b/Test/test21/BooleanQuantification.bpl.a.expect new file mode 100644 index 00000000..4f2f67ff --- /dev/null +++ b/Test/test21/BooleanQuantification.bpl.a.expect @@ -0,0 +1,8 @@ +BooleanQuantification.bpl(25,3): Error BP5001: This assertion might not hold. +Execution trace: + BooleanQuantification.bpl(24,3): anon0 +BooleanQuantification.bpl(37,3): Error BP5001: This assertion might not hold. +Execution trace: + BooleanQuantification.bpl(35,3): anon0 + +Boogie program verifier finished with 2 verified, 2 errors diff --git a/Test/test21/BooleanQuantification.bpl.n.expect b/Test/test21/BooleanQuantification.bpl.n.expect new file mode 100644 index 00000000..4f2f67ff --- /dev/null +++ b/Test/test21/BooleanQuantification.bpl.n.expect @@ -0,0 +1,8 @@ +BooleanQuantification.bpl(25,3): Error BP5001: This assertion might not hold. +Execution trace: + BooleanQuantification.bpl(24,3): anon0 +BooleanQuantification.bpl(37,3): Error BP5001: This assertion might not hold. +Execution trace: + BooleanQuantification.bpl(35,3): anon0 + +Boogie program verifier finished with 2 verified, 2 errors diff --git a/Test/test21/BooleanQuantification.bpl.p.expect b/Test/test21/BooleanQuantification.bpl.p.expect new file mode 100644 index 00000000..4f2f67ff --- /dev/null +++ b/Test/test21/BooleanQuantification.bpl.p.expect @@ -0,0 +1,8 @@ +BooleanQuantification.bpl(25,3): Error BP5001: This assertion might not hold. +Execution trace: + BooleanQuantification.bpl(24,3): anon0 +BooleanQuantification.bpl(37,3): Error BP5001: This assertion might not hold. +Execution trace: + BooleanQuantification.bpl(35,3): anon0 + +Boogie program verifier finished with 2 verified, 2 errors diff --git a/Test/test21/BooleanQuantification2.bpl b/Test/test21/BooleanQuantification2.bpl index af6e1f4f..73234024 100644 --- a/Test/test21/BooleanQuantification2.bpl +++ b/Test/test21/BooleanQuantification2.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
axiom (forall x:bool :: x || !x);
diff --git a/Test/test21/BooleanQuantification2.bpl.a.expect b/Test/test21/BooleanQuantification2.bpl.a.expect new file mode 100644 index 00000000..8b6378ac --- /dev/null +++ b/Test/test21/BooleanQuantification2.bpl.a.expect @@ -0,0 +1,5 @@ +BooleanQuantification2.bpl(19,3): Error BP5001: This assertion might not hold. +Execution trace: + BooleanQuantification2.bpl(16,3): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/BooleanQuantification2.bpl.n.expect b/Test/test21/BooleanQuantification2.bpl.n.expect new file mode 100644 index 00000000..8b6378ac --- /dev/null +++ b/Test/test21/BooleanQuantification2.bpl.n.expect @@ -0,0 +1,5 @@ +BooleanQuantification2.bpl(19,3): Error BP5001: This assertion might not hold. +Execution trace: + BooleanQuantification2.bpl(16,3): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/BooleanQuantification2.bpl.p.expect b/Test/test21/BooleanQuantification2.bpl.p.expect new file mode 100644 index 00000000..8b6378ac --- /dev/null +++ b/Test/test21/BooleanQuantification2.bpl.p.expect @@ -0,0 +1,5 @@ +BooleanQuantification2.bpl(19,3): Error BP5001: This assertion might not hold. +Execution trace: + BooleanQuantification2.bpl(16,3): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Boxing.bpl b/Test/test21/Boxing.bpl index 08967891..00e3013e 100644 --- a/Test/test21/Boxing.bpl +++ b/Test/test21/Boxing.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
type Box;
diff --git a/Test/test21/Boxing.bpl.a.expect b/Test/test21/Boxing.bpl.a.expect new file mode 100644 index 00000000..092747bc --- /dev/null +++ b/Test/test21/Boxing.bpl.a.expect @@ -0,0 +1,5 @@ +Boxing.bpl(26,3): Error BP5001: This assertion might not hold. +Execution trace: + Boxing.bpl(21,6): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Boxing.bpl.n.expect b/Test/test21/Boxing.bpl.n.expect new file mode 100644 index 00000000..c19befee --- /dev/null +++ b/Test/test21/Boxing.bpl.n.expect @@ -0,0 +1,8 @@ +Boxing.bpl(25,3): Error BP5001: This assertion might not hold. +Execution trace: + Boxing.bpl(21,6): anon0 +Boxing.bpl(26,3): Error BP5001: This assertion might not hold. +Execution trace: + Boxing.bpl(21,6): anon0 + +Boogie program verifier finished with 0 verified, 2 errors diff --git a/Test/test21/Boxing.bpl.p.expect b/Test/test21/Boxing.bpl.p.expect new file mode 100644 index 00000000..092747bc --- /dev/null +++ b/Test/test21/Boxing.bpl.p.expect @@ -0,0 +1,5 @@ +Boxing.bpl(26,3): Error BP5001: This assertion might not hold. +Execution trace: + Boxing.bpl(21,6): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Casts.bpl b/Test/test21/Casts.bpl index 5173021e..1320cff2 100644 --- a/Test/test21/Casts.bpl +++ b/Test/test21/Casts.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
procedure P() returns () {
diff --git a/Test/test21/Casts.bpl.a.expect b/Test/test21/Casts.bpl.a.expect new file mode 100644 index 00000000..ecda264e --- /dev/null +++ b/Test/test21/Casts.bpl.a.expect @@ -0,0 +1,5 @@ +Casts.bpl(16,3): Error BP5001: This assertion might not hold. +Execution trace: + Casts.bpl(12,3): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Casts.bpl.n.expect b/Test/test21/Casts.bpl.n.expect new file mode 100644 index 00000000..ecda264e --- /dev/null +++ b/Test/test21/Casts.bpl.n.expect @@ -0,0 +1,5 @@ +Casts.bpl(16,3): Error BP5001: This assertion might not hold. +Execution trace: + Casts.bpl(12,3): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Casts.bpl.p.expect b/Test/test21/Casts.bpl.p.expect new file mode 100644 index 00000000..ecda264e --- /dev/null +++ b/Test/test21/Casts.bpl.p.expect @@ -0,0 +1,5 @@ +Casts.bpl(16,3): Error BP5001: This assertion might not hold. +Execution trace: + Casts.bpl(12,3): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Coercions2.bpl b/Test/test21/Coercions2.bpl index c5abb724..849376f5 100644 --- a/Test/test21/Coercions2.bpl +++ b/Test/test21/Coercions2.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
type Box, C;
diff --git a/Test/test21/Coercions2.bpl.a.expect b/Test/test21/Coercions2.bpl.a.expect new file mode 100644 index 00000000..04c35bf4 --- /dev/null +++ b/Test/test21/Coercions2.bpl.a.expect @@ -0,0 +1,6 @@ +Coercions2.bpl(18,23): Warning: type parameter a is ambiguous, instantiating to int +Coercions2.bpl(29,3): Error BP5001: This assertion might not hold. +Execution trace: + Coercions2.bpl(24,3): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Coercions2.bpl.n.expect b/Test/test21/Coercions2.bpl.n.expect new file mode 100644 index 00000000..121a25ff --- /dev/null +++ b/Test/test21/Coercions2.bpl.n.expect @@ -0,0 +1,9 @@ +Coercions2.bpl(18,23): Warning: type parameter a is ambiguous, instantiating to int +Coercions2.bpl(24,3): Error BP5001: This assertion might not hold. +Execution trace: + Coercions2.bpl(24,3): anon0 +Coercions2.bpl(29,3): Error BP5001: This assertion might not hold. +Execution trace: + Coercions2.bpl(24,3): anon0 + +Boogie program verifier finished with 0 verified, 2 errors diff --git a/Test/test21/Coercions2.bpl.p.expect b/Test/test21/Coercions2.bpl.p.expect new file mode 100644 index 00000000..04c35bf4 --- /dev/null +++ b/Test/test21/Coercions2.bpl.p.expect @@ -0,0 +1,6 @@ +Coercions2.bpl(18,23): Warning: type parameter a is ambiguous, instantiating to int +Coercions2.bpl(29,3): Error BP5001: This assertion might not hold. +Execution trace: + Coercions2.bpl(24,3): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Colors.bpl b/Test/test21/Colors.bpl index be25cc15..7e63c9ff 100644 --- a/Test/test21/Colors.bpl +++ b/Test/test21/Colors.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
type Color;
diff --git a/Test/test21/Colors.bpl.a.expect b/Test/test21/Colors.bpl.a.expect new file mode 100644 index 00000000..4339b770 --- /dev/null +++ b/Test/test21/Colors.bpl.a.expect @@ -0,0 +1,8 @@ +Colors.bpl(19,3): Error BP5001: This assertion might not hold. +Execution trace: + Colors.bpl(18,3): anon0 +Colors.bpl(26,3): Error BP5001: This assertion might not hold. +Execution trace: + Colors.bpl(25,3): anon0 + +Boogie program verifier finished with 0 verified, 2 errors diff --git a/Test/test21/Colors.bpl.n.expect b/Test/test21/Colors.bpl.n.expect new file mode 100644 index 00000000..4339b770 --- /dev/null +++ b/Test/test21/Colors.bpl.n.expect @@ -0,0 +1,8 @@ +Colors.bpl(19,3): Error BP5001: This assertion might not hold. +Execution trace: + Colors.bpl(18,3): anon0 +Colors.bpl(26,3): Error BP5001: This assertion might not hold. +Execution trace: + Colors.bpl(25,3): anon0 + +Boogie program verifier finished with 0 verified, 2 errors diff --git a/Test/test21/Colors.bpl.p.expect b/Test/test21/Colors.bpl.p.expect new file mode 100644 index 00000000..4339b770 --- /dev/null +++ b/Test/test21/Colors.bpl.p.expect @@ -0,0 +1,8 @@ +Colors.bpl(19,3): Error BP5001: This assertion might not hold. +Execution trace: + Colors.bpl(18,3): anon0 +Colors.bpl(26,3): Error BP5001: This assertion might not hold. +Execution trace: + Colors.bpl(25,3): anon0 + +Boogie program verifier finished with 0 verified, 2 errors diff --git a/Test/test21/DisjointDomains.bpl b/Test/test21/DisjointDomains.bpl index 88647e6b..303d0e4f 100644 --- a/Test/test21/DisjointDomains.bpl +++ b/Test/test21/DisjointDomains.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
type C _;
function f<a>(C a) returns (int);
diff --git a/Test/test21/DisjointDomains.bpl.a.expect b/Test/test21/DisjointDomains.bpl.a.expect new file mode 100644 index 00000000..e813890c --- /dev/null +++ b/Test/test21/DisjointDomains.bpl.a.expect @@ -0,0 +1,11 @@ +DisjointDomains.bpl(20,5): Error BP5001: This assertion might not hold. +Execution trace: + DisjointDomains.bpl(17,3): start +DisjointDomains.bpl(27,5): Error BP5001: This assertion might not hold. +Execution trace: + DisjointDomains.bpl(26,3): start +DisjointDomains.bpl(33,5): Error BP5001: This assertion might not hold. +Execution trace: + DisjointDomains.bpl(32,3): start + +Boogie program verifier finished with 0 verified, 3 errors diff --git a/Test/test21/DisjointDomains.bpl.n.expect b/Test/test21/DisjointDomains.bpl.n.expect new file mode 100644 index 00000000..a9949f2e --- /dev/null +++ b/Test/test21/DisjointDomains.bpl.n.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 3 verified, 0 errors diff --git a/Test/test21/DisjointDomains.bpl.p.expect b/Test/test21/DisjointDomains.bpl.p.expect new file mode 100644 index 00000000..e813890c --- /dev/null +++ b/Test/test21/DisjointDomains.bpl.p.expect @@ -0,0 +1,11 @@ +DisjointDomains.bpl(20,5): Error BP5001: This assertion might not hold. +Execution trace: + DisjointDomains.bpl(17,3): start +DisjointDomains.bpl(27,5): Error BP5001: This assertion might not hold. +Execution trace: + DisjointDomains.bpl(26,3): start +DisjointDomains.bpl(33,5): Error BP5001: This assertion might not hold. +Execution trace: + DisjointDomains.bpl(32,3): start + +Boogie program verifier finished with 0 verified, 3 errors diff --git a/Test/test21/DisjointDomains2.bpl b/Test/test21/DisjointDomains2.bpl index 3cac88ca..8677d9dc 100644 --- a/Test/test21/DisjointDomains2.bpl +++ b/Test/test21/DisjointDomains2.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
type C _;
function f<a>(C a) returns (int);
diff --git a/Test/test21/DisjointDomains2.bpl.a.expect b/Test/test21/DisjointDomains2.bpl.a.expect new file mode 100644 index 00000000..f0f40a57 --- /dev/null +++ b/Test/test21/DisjointDomains2.bpl.a.expect @@ -0,0 +1,20 @@ +DisjointDomains2.bpl(17,5): Error BP5001: This assertion might not hold. +Execution trace: + DisjointDomains2.bpl(15,3): start +DisjointDomains2.bpl(24,5): Error BP5001: This assertion might not hold. +Execution trace: + DisjointDomains2.bpl(22,3): start +DisjointDomains2.bpl(38,5): Error BP5001: This assertion might not hold. +Execution trace: + DisjointDomains2.bpl(36,3): start +DisjointDomains2.bpl(45,5): Error BP5001: This assertion might not hold. +Execution trace: + DisjointDomains2.bpl(43,3): start +DisjointDomains2.bpl(55,5): Error BP5001: This assertion might not hold. +Execution trace: + DisjointDomains2.bpl(51,3): start +DisjointDomains2.bpl(69,5): Error BP5001: This assertion might not hold. +Execution trace: + DisjointDomains2.bpl(64,3): start + +Boogie program verifier finished with 0 verified, 6 errors diff --git a/Test/test21/DisjointDomains2.bpl.n.expect b/Test/test21/DisjointDomains2.bpl.n.expect new file mode 100644 index 00000000..c378844e --- /dev/null +++ b/Test/test21/DisjointDomains2.bpl.n.expect @@ -0,0 +1,8 @@ +DisjointDomains2.bpl(17,5): Error BP5001: This assertion might not hold. +Execution trace: + DisjointDomains2.bpl(15,3): start +DisjointDomains2.bpl(24,5): Error BP5001: This assertion might not hold. +Execution trace: + DisjointDomains2.bpl(22,3): start + +Boogie program verifier finished with 4 verified, 2 errors diff --git a/Test/test21/DisjointDomains2.bpl.p.expect b/Test/test21/DisjointDomains2.bpl.p.expect new file mode 100644 index 00000000..f0f40a57 --- /dev/null +++ b/Test/test21/DisjointDomains2.bpl.p.expect @@ -0,0 +1,20 @@ +DisjointDomains2.bpl(17,5): Error BP5001: This assertion might not hold. +Execution trace: + DisjointDomains2.bpl(15,3): start +DisjointDomains2.bpl(24,5): Error BP5001: This assertion might not hold. +Execution trace: + DisjointDomains2.bpl(22,3): start +DisjointDomains2.bpl(38,5): Error BP5001: This assertion might not hold. +Execution trace: + DisjointDomains2.bpl(36,3): start +DisjointDomains2.bpl(45,5): Error BP5001: This assertion might not hold. +Execution trace: + DisjointDomains2.bpl(43,3): start +DisjointDomains2.bpl(55,5): Error BP5001: This assertion might not hold. +Execution trace: + DisjointDomains2.bpl(51,3): start +DisjointDomains2.bpl(69,5): Error BP5001: This assertion might not hold. +Execution trace: + DisjointDomains2.bpl(64,3): start + +Boogie program verifier finished with 0 verified, 6 errors diff --git a/Test/test21/EmptyList.bpl b/Test/test21/EmptyList.bpl index a6b90638..28362b73 100644 --- a/Test/test21/EmptyList.bpl +++ b/Test/test21/EmptyList.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
type List _;
diff --git a/Test/test21/EmptyList.bpl.a.expect b/Test/test21/EmptyList.bpl.a.expect new file mode 100644 index 00000000..c15d8d6f --- /dev/null +++ b/Test/test21/EmptyList.bpl.a.expect @@ -0,0 +1,6 @@ +EmptyList.bpl(52,9): Warning: type parameter a is ambiguous, instantiating to List int +EmptyList.bpl(48,3): Error BP5001: This assertion might not hold. +Execution trace: + EmptyList.bpl(32,5): anon0 + +Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/test21/EmptyList.bpl.n.expect b/Test/test21/EmptyList.bpl.n.expect new file mode 100644 index 00000000..3895affe --- /dev/null +++ b/Test/test21/EmptyList.bpl.n.expect @@ -0,0 +1,12 @@ +EmptyList.bpl(52,9): Warning: type parameter a is ambiguous, instantiating to List int +EmptyList.bpl(34,3): Error BP5001: This assertion might not hold. +Execution trace: + EmptyList.bpl(32,5): anon0 +EmptyList.bpl(48,3): Error BP5001: This assertion might not hold. +Execution trace: + EmptyList.bpl(32,5): anon0 +EmptyList.bpl(52,3): Error BP5001: This assertion might not hold. +Execution trace: + EmptyList.bpl(52,3): anon0 + +Boogie program verifier finished with 0 verified, 3 errors diff --git a/Test/test21/EmptyList.bpl.p.expect b/Test/test21/EmptyList.bpl.p.expect new file mode 100644 index 00000000..c15d8d6f --- /dev/null +++ b/Test/test21/EmptyList.bpl.p.expect @@ -0,0 +1,6 @@ +EmptyList.bpl(52,9): Warning: type parameter a is ambiguous, instantiating to List int +EmptyList.bpl(48,3): Error BP5001: This assertion might not hold. +Execution trace: + EmptyList.bpl(32,5): anon0 + +Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/test21/EmptySetBug.bpl b/Test/test21/EmptySetBug.bpl index 424d998c..06a42652 100644 --- a/Test/test21/EmptySetBug.bpl +++ b/Test/test21/EmptySetBug.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
type ref;
const null: ref;
diff --git a/Test/test21/EmptySetBug.bpl.a.expect b/Test/test21/EmptySetBug.bpl.a.expect new file mode 100644 index 00000000..8b3d17b8 --- /dev/null +++ b/Test/test21/EmptySetBug.bpl.a.expect @@ -0,0 +1,5 @@ +EmptySetBug.bpl(35,3): Error BP5001: This assertion might not hold. +Execution trace: + EmptySetBug.bpl(31,5): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/EmptySetBug.bpl.n.expect b/Test/test21/EmptySetBug.bpl.n.expect new file mode 100644 index 00000000..a37a8c14 --- /dev/null +++ b/Test/test21/EmptySetBug.bpl.n.expect @@ -0,0 +1,8 @@ +EmptySetBug.bpl(33,3): Error BP5001: This assertion might not hold. +Execution trace: + EmptySetBug.bpl(31,5): anon0 +EmptySetBug.bpl(35,3): Error BP5001: This assertion might not hold. +Execution trace: + EmptySetBug.bpl(31,5): anon0 + +Boogie program verifier finished with 0 verified, 2 errors diff --git a/Test/test21/EmptySetBug.bpl.p.expect b/Test/test21/EmptySetBug.bpl.p.expect new file mode 100644 index 00000000..8b3d17b8 --- /dev/null +++ b/Test/test21/EmptySetBug.bpl.p.expect @@ -0,0 +1,5 @@ +EmptySetBug.bpl(35,3): Error BP5001: This assertion might not hold. +Execution trace: + EmptySetBug.bpl(31,5): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Flattening.bpl b/Test/test21/Flattening.bpl index 10899931..4ef7e5c8 100644 --- a/Test/test21/Flattening.bpl +++ b/Test/test21/Flattening.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
function g(int) returns (int);
diff --git a/Test/test21/Flattening.bpl.a.expect b/Test/test21/Flattening.bpl.a.expect new file mode 100644 index 00000000..e68a8891 --- /dev/null +++ b/Test/test21/Flattening.bpl.a.expect @@ -0,0 +1,5 @@ +Flattening.bpl(18,3): Error BP5001: This assertion might not hold. +Execution trace: + Flattening.bpl(18,3): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Flattening.bpl.n.expect b/Test/test21/Flattening.bpl.n.expect new file mode 100644 index 00000000..e68a8891 --- /dev/null +++ b/Test/test21/Flattening.bpl.n.expect @@ -0,0 +1,5 @@ +Flattening.bpl(18,3): Error BP5001: This assertion might not hold. +Execution trace: + Flattening.bpl(18,3): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Flattening.bpl.p.expect b/Test/test21/Flattening.bpl.p.expect new file mode 100644 index 00000000..e68a8891 --- /dev/null +++ b/Test/test21/Flattening.bpl.p.expect @@ -0,0 +1,5 @@ +Flattening.bpl(18,3): Error BP5001: This assertion might not hold. +Execution trace: + Flattening.bpl(18,3): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/FunAxioms.bpl b/Test/test21/FunAxioms.bpl index 850f4d08..c51024ad 100644 --- a/Test/test21/FunAxioms.bpl +++ b/Test/test21/FunAxioms.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
type Pair a b;
diff --git a/Test/test21/FunAxioms.bpl.a.expect b/Test/test21/FunAxioms.bpl.a.expect new file mode 100644 index 00000000..b6fa4917 --- /dev/null +++ b/Test/test21/FunAxioms.bpl.a.expect @@ -0,0 +1,5 @@ +FunAxioms.bpl(36,3): Error BP5001: This assertion might not hold. +Execution trace: + FunAxioms.bpl(24,3): anon0 + +Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/test21/FunAxioms.bpl.n.expect b/Test/test21/FunAxioms.bpl.n.expect new file mode 100644 index 00000000..b6fa4917 --- /dev/null +++ b/Test/test21/FunAxioms.bpl.n.expect @@ -0,0 +1,5 @@ +FunAxioms.bpl(36,3): Error BP5001: This assertion might not hold. +Execution trace: + FunAxioms.bpl(24,3): anon0 + +Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/test21/FunAxioms.bpl.p.expect b/Test/test21/FunAxioms.bpl.p.expect new file mode 100644 index 00000000..b6fa4917 --- /dev/null +++ b/Test/test21/FunAxioms.bpl.p.expect @@ -0,0 +1,5 @@ +FunAxioms.bpl(36,3): Error BP5001: This assertion might not hold. +Execution trace: + FunAxioms.bpl(24,3): anon0 + +Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/test21/FunAxioms2.bpl b/Test/test21/FunAxioms2.bpl index f487dcab..3b9bccf2 100644 --- a/Test/test21/FunAxioms2.bpl +++ b/Test/test21/FunAxioms2.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
type T;
diff --git a/Test/test21/FunAxioms2.bpl.a.expect b/Test/test21/FunAxioms2.bpl.a.expect new file mode 100644 index 00000000..bf34a7a0 --- /dev/null +++ b/Test/test21/FunAxioms2.bpl.a.expect @@ -0,0 +1,5 @@ +FunAxioms2.bpl(26,3): Error BP5001: This assertion might not hold. +Execution trace: + FunAxioms2.bpl(22,5): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/FunAxioms2.bpl.n.expect b/Test/test21/FunAxioms2.bpl.n.expect new file mode 100644 index 00000000..bf34a7a0 --- /dev/null +++ b/Test/test21/FunAxioms2.bpl.n.expect @@ -0,0 +1,5 @@ +FunAxioms2.bpl(26,3): Error BP5001: This assertion might not hold. +Execution trace: + FunAxioms2.bpl(22,5): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/FunAxioms2.bpl.p.expect b/Test/test21/FunAxioms2.bpl.p.expect new file mode 100644 index 00000000..bf34a7a0 --- /dev/null +++ b/Test/test21/FunAxioms2.bpl.p.expect @@ -0,0 +1,5 @@ +FunAxioms2.bpl(26,3): Error BP5001: This assertion might not hold. +Execution trace: + FunAxioms2.bpl(22,5): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/HeapAbstraction.bpl b/Test/test21/HeapAbstraction.bpl index 1d2a7f99..6f88189c 100644 --- a/Test/test21/HeapAbstraction.bpl +++ b/Test/test21/HeapAbstraction.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
type Field a, Heap = <a>[ref, Field a]a;
diff --git a/Test/test21/HeapAbstraction.bpl.a.expect b/Test/test21/HeapAbstraction.bpl.a.expect new file mode 100644 index 00000000..1058ef91 --- /dev/null +++ b/Test/test21/HeapAbstraction.bpl.a.expect @@ -0,0 +1,5 @@ +HeapAbstraction.bpl(21,3): Error BP5001: This assertion might not hold. +Execution trace: + HeapAbstraction.bpl(20,3): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/HeapAbstraction.bpl.n.expect b/Test/test21/HeapAbstraction.bpl.n.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/test21/HeapAbstraction.bpl.n.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/test21/HeapAbstraction.bpl.p.expect b/Test/test21/HeapAbstraction.bpl.p.expect new file mode 100644 index 00000000..1058ef91 --- /dev/null +++ b/Test/test21/HeapAbstraction.bpl.p.expect @@ -0,0 +1,5 @@ +HeapAbstraction.bpl(21,3): Error BP5001: This assertion might not hold. +Execution trace: + HeapAbstraction.bpl(20,3): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/HeapAxiom.bpl b/Test/test21/HeapAxiom.bpl index 8972c6af..adb3f632 100644 --- a/Test/test21/HeapAxiom.bpl +++ b/Test/test21/HeapAxiom.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
type Field a, Heap = <a>[ref, Field a]a;
diff --git a/Test/test21/HeapAxiom.bpl.a.expect b/Test/test21/HeapAxiom.bpl.a.expect new file mode 100644 index 00000000..26a96105 --- /dev/null +++ b/Test/test21/HeapAxiom.bpl.a.expect @@ -0,0 +1,5 @@ +HeapAxiom.bpl(30,3): Error BP5001: This assertion might not hold. +Execution trace: + HeapAxiom.bpl(19,3): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/HeapAxiom.bpl.n.expect b/Test/test21/HeapAxiom.bpl.n.expect new file mode 100644 index 00000000..26a96105 --- /dev/null +++ b/Test/test21/HeapAxiom.bpl.n.expect @@ -0,0 +1,5 @@ +HeapAxiom.bpl(30,3): Error BP5001: This assertion might not hold. +Execution trace: + HeapAxiom.bpl(19,3): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/HeapAxiom.bpl.p.expect b/Test/test21/HeapAxiom.bpl.p.expect new file mode 100644 index 00000000..26a96105 --- /dev/null +++ b/Test/test21/HeapAxiom.bpl.p.expect @@ -0,0 +1,5 @@ +HeapAxiom.bpl(30,3): Error BP5001: This assertion might not hold. +Execution trace: + HeapAxiom.bpl(19,3): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/InterestingExamples0.bpl b/Test/test21/InterestingExamples0.bpl index d1b90d10..d3021553 100644 --- a/Test/test21/InterestingExamples0.bpl +++ b/Test/test21/InterestingExamples0.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
procedure P() returns () {
var a : <t>[t]int;
diff --git a/Test/test21/InterestingExamples0.bpl.a.expect b/Test/test21/InterestingExamples0.bpl.a.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/test21/InterestingExamples0.bpl.a.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/test21/InterestingExamples0.bpl.n.expect b/Test/test21/InterestingExamples0.bpl.n.expect new file mode 100644 index 00000000..f549a09a --- /dev/null +++ b/Test/test21/InterestingExamples0.bpl.n.expect @@ -0,0 +1,5 @@ +InterestingExamples0.bpl(13,1): Error BP5001: This assertion might not hold. +Execution trace: + InterestingExamples0.bpl(11,6): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/InterestingExamples0.bpl.p.expect b/Test/test21/InterestingExamples0.bpl.p.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/test21/InterestingExamples0.bpl.p.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/test21/InterestingExamples1.bpl b/Test/test21/InterestingExamples1.bpl index 3ec7449e..a530c625 100644 --- a/Test/test21/InterestingExamples1.bpl +++ b/Test/test21/InterestingExamples1.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
type Set = <a> [a] bool;
type Field a;
diff --git a/Test/test21/InterestingExamples1.bpl.a.expect b/Test/test21/InterestingExamples1.bpl.a.expect new file mode 100644 index 00000000..8ee75548 --- /dev/null +++ b/Test/test21/InterestingExamples1.bpl.a.expect @@ -0,0 +1,5 @@ +InterestingExamples1.bpl(28,3): Error BP5001: This assertion might not hold. +Execution trace: + InterestingExamples1.bpl(19,5): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/InterestingExamples1.bpl.n.expect b/Test/test21/InterestingExamples1.bpl.n.expect new file mode 100644 index 00000000..b757672b --- /dev/null +++ b/Test/test21/InterestingExamples1.bpl.n.expect @@ -0,0 +1,8 @@ +InterestingExamples1.bpl(22,3): Error BP5001: This assertion might not hold. +Execution trace: + InterestingExamples1.bpl(19,5): anon0 +InterestingExamples1.bpl(28,3): Error BP5001: This assertion might not hold. +Execution trace: + InterestingExamples1.bpl(19,5): anon0 + +Boogie program verifier finished with 0 verified, 2 errors diff --git a/Test/test21/InterestingExamples1.bpl.p.expect b/Test/test21/InterestingExamples1.bpl.p.expect new file mode 100644 index 00000000..8ee75548 --- /dev/null +++ b/Test/test21/InterestingExamples1.bpl.p.expect @@ -0,0 +1,5 @@ +InterestingExamples1.bpl(28,3): Error BP5001: This assertion might not hold. +Execution trace: + InterestingExamples1.bpl(19,5): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/InterestingExamples2.bpl b/Test/test21/InterestingExamples2.bpl index 62374cb6..fd17b122 100644 --- a/Test/test21/InterestingExamples2.bpl +++ b/Test/test21/InterestingExamples2.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
procedure P() returns () {
diff --git a/Test/test21/InterestingExamples2.bpl.a.expect b/Test/test21/InterestingExamples2.bpl.a.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/test21/InterestingExamples2.bpl.a.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/test21/InterestingExamples2.bpl.n.expect b/Test/test21/InterestingExamples2.bpl.n.expect new file mode 100644 index 00000000..389abe51 --- /dev/null +++ b/Test/test21/InterestingExamples2.bpl.n.expect @@ -0,0 +1,8 @@ +InterestingExamples2.bpl(15,1): Error BP5001: This assertion might not hold. +Execution trace: + InterestingExamples2.bpl(14,6): anon0 +InterestingExamples2.bpl(16,1): Error BP5001: This assertion might not hold. +Execution trace: + InterestingExamples2.bpl(14,6): anon0 + +Boogie program verifier finished with 0 verified, 2 errors diff --git a/Test/test21/InterestingExamples2.bpl.p.expect b/Test/test21/InterestingExamples2.bpl.p.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/test21/InterestingExamples2.bpl.p.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/test21/InterestingExamples3.bpl b/Test/test21/InterestingExamples3.bpl index 8eef3dff..3acca9a1 100644 --- a/Test/test21/InterestingExamples3.bpl +++ b/Test/test21/InterestingExamples3.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
procedure P() returns () {
diff --git a/Test/test21/InterestingExamples3.bpl.a.expect b/Test/test21/InterestingExamples3.bpl.a.expect new file mode 100644 index 00000000..b02bbbdf --- /dev/null +++ b/Test/test21/InterestingExamples3.bpl.a.expect @@ -0,0 +1,5 @@ +InterestingExamples3.bpl(21,2): Error BP5001: This assertion might not hold. +Execution trace: + InterestingExamples3.bpl(19,2): anon0 + +Boogie program verifier finished with 2 verified, 1 error diff --git a/Test/test21/InterestingExamples3.bpl.n.expect b/Test/test21/InterestingExamples3.bpl.n.expect new file mode 100644 index 00000000..b02bbbdf --- /dev/null +++ b/Test/test21/InterestingExamples3.bpl.n.expect @@ -0,0 +1,5 @@ +InterestingExamples3.bpl(21,2): Error BP5001: This assertion might not hold. +Execution trace: + InterestingExamples3.bpl(19,2): anon0 + +Boogie program verifier finished with 2 verified, 1 error diff --git a/Test/test21/InterestingExamples3.bpl.p.expect b/Test/test21/InterestingExamples3.bpl.p.expect new file mode 100644 index 00000000..b02bbbdf --- /dev/null +++ b/Test/test21/InterestingExamples3.bpl.p.expect @@ -0,0 +1,5 @@ +InterestingExamples3.bpl(21,2): Error BP5001: This assertion might not hold. +Execution trace: + InterestingExamples3.bpl(19,2): anon0 + +Boogie program verifier finished with 2 verified, 1 error diff --git a/Test/test21/InterestingExamples4.bpl b/Test/test21/InterestingExamples4.bpl index 67636af1..db2e9682 100644 --- a/Test/test21/InterestingExamples4.bpl +++ b/Test/test21/InterestingExamples4.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
// a property that should hold according to the Boogie semantics
// (but no automatic theorem prover will be able to prove it)
diff --git a/Test/test21/InterestingExamples4.bpl.a.expect b/Test/test21/InterestingExamples4.bpl.a.expect new file mode 100644 index 00000000..346e844b --- /dev/null +++ b/Test/test21/InterestingExamples4.bpl.a.expect @@ -0,0 +1,8 @@ +InterestingExamples4.bpl(42,3): Error BP5001: This assertion might not hold. +Execution trace: + InterestingExamples4.bpl(42,3): anon0 +InterestingExamples4.bpl(45,3): Error BP5001: This assertion might not hold. +Execution trace: + InterestingExamples4.bpl(42,3): anon0 + +Boogie program verifier finished with 0 verified, 2 errors diff --git a/Test/test21/InterestingExamples4.bpl.n.expect b/Test/test21/InterestingExamples4.bpl.n.expect new file mode 100644 index 00000000..346e844b --- /dev/null +++ b/Test/test21/InterestingExamples4.bpl.n.expect @@ -0,0 +1,8 @@ +InterestingExamples4.bpl(42,3): Error BP5001: This assertion might not hold. +Execution trace: + InterestingExamples4.bpl(42,3): anon0 +InterestingExamples4.bpl(45,3): Error BP5001: This assertion might not hold. +Execution trace: + InterestingExamples4.bpl(42,3): anon0 + +Boogie program verifier finished with 0 verified, 2 errors diff --git a/Test/test21/InterestingExamples4.bpl.p.expect b/Test/test21/InterestingExamples4.bpl.p.expect new file mode 100644 index 00000000..bb912e59 --- /dev/null +++ b/Test/test21/InterestingExamples4.bpl.p.expect @@ -0,0 +1,5 @@ +InterestingExamples4.bpl(45,3): Error BP5001: This assertion might not hold. +Execution trace: + InterestingExamples4.bpl(42,3): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/InterestingExamples5.bpl b/Test/test21/InterestingExamples5.bpl index b6c48b63..be388839 100644 --- a/Test/test21/InterestingExamples5.bpl +++ b/Test/test21/InterestingExamples5.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
type C a;
diff --git a/Test/test21/InterestingExamples5.bpl.a.expect b/Test/test21/InterestingExamples5.bpl.a.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/test21/InterestingExamples5.bpl.a.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/test21/InterestingExamples5.bpl.n.expect b/Test/test21/InterestingExamples5.bpl.n.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/test21/InterestingExamples5.bpl.n.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/test21/InterestingExamples5.bpl.p.expect b/Test/test21/InterestingExamples5.bpl.p.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/test21/InterestingExamples5.bpl.p.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/test21/Keywords.bpl b/Test/test21/Keywords.bpl index daf38b45..9af526e4 100644 --- a/Test/test21/Keywords.bpl +++ b/Test/test21/Keywords.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
function NOT(x:int) returns(int);
diff --git a/Test/test21/Keywords.bpl.a.expect b/Test/test21/Keywords.bpl.a.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/test21/Keywords.bpl.a.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/test21/Keywords.bpl.n.expect b/Test/test21/Keywords.bpl.n.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/test21/Keywords.bpl.n.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/test21/Keywords.bpl.p.expect b/Test/test21/Keywords.bpl.p.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/test21/Keywords.bpl.p.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/test21/LargeLiterals0.bpl b/Test/test21/LargeLiterals0.bpl index a77ffadd..203e9bc5 100644 --- a/Test/test21/LargeLiterals0.bpl +++ b/Test/test21/LargeLiterals0.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
var x : int;
diff --git a/Test/test21/LargeLiterals0.bpl.a.expect b/Test/test21/LargeLiterals0.bpl.a.expect new file mode 100644 index 00000000..1f42b69e --- /dev/null +++ b/Test/test21/LargeLiterals0.bpl.a.expect @@ -0,0 +1,5 @@ +LargeLiterals0.bpl(24,3): Error BP5001: This assertion might not hold. +Execution trace: + LargeLiterals0.bpl(13,5): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/LargeLiterals0.bpl.n.expect b/Test/test21/LargeLiterals0.bpl.n.expect new file mode 100644 index 00000000..1f42b69e --- /dev/null +++ b/Test/test21/LargeLiterals0.bpl.n.expect @@ -0,0 +1,5 @@ +LargeLiterals0.bpl(24,3): Error BP5001: This assertion might not hold. +Execution trace: + LargeLiterals0.bpl(13,5): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/LargeLiterals0.bpl.p.expect b/Test/test21/LargeLiterals0.bpl.p.expect new file mode 100644 index 00000000..1f42b69e --- /dev/null +++ b/Test/test21/LargeLiterals0.bpl.p.expect @@ -0,0 +1,5 @@ +LargeLiterals0.bpl(24,3): Error BP5001: This assertion might not hold. +Execution trace: + LargeLiterals0.bpl(13,5): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/LetSorting.bpl b/Test/test21/LetSorting.bpl index 3dc59fde..38e77396 100644 --- a/Test/test21/LetSorting.bpl +++ b/Test/test21/LetSorting.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
procedure Array0() returns (z: int)
diff --git a/Test/test21/LetSorting.bpl.a.expect b/Test/test21/LetSorting.bpl.a.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/test21/LetSorting.bpl.a.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/test21/LetSorting.bpl.n.expect b/Test/test21/LetSorting.bpl.n.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/test21/LetSorting.bpl.n.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/test21/LetSorting.bpl.p.expect b/Test/test21/LetSorting.bpl.p.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/test21/LetSorting.bpl.p.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/test21/MapAxiomsConsistency.bpl b/Test/test21/MapAxiomsConsistency.bpl index a27f89c4..66e7a142 100644 --- a/Test/test21/MapAxiomsConsistency.bpl +++ b/Test/test21/MapAxiomsConsistency.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
// Dafny program verifier version 0.92, Copyright (c) 2003-2008, Microsoft.
// Command Line Options: /trace /typeEncoding:arguments /print:test.bpl test.dfy
diff --git a/Test/test21/MapAxiomsConsistency.bpl.a.expect b/Test/test21/MapAxiomsConsistency.bpl.a.expect new file mode 100644 index 00000000..eabc661f --- /dev/null +++ b/Test/test21/MapAxiomsConsistency.bpl.a.expect @@ -0,0 +1,5 @@ +MapAxiomsConsistency.bpl(100,5): Error BP5001: This assertion might not hold. +Execution trace: + MapAxiomsConsistency.bpl(85,13): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/MapAxiomsConsistency.bpl.n.expect b/Test/test21/MapAxiomsConsistency.bpl.n.expect new file mode 100644 index 00000000..eabc661f --- /dev/null +++ b/Test/test21/MapAxiomsConsistency.bpl.n.expect @@ -0,0 +1,5 @@ +MapAxiomsConsistency.bpl(100,5): Error BP5001: This assertion might not hold. +Execution trace: + MapAxiomsConsistency.bpl(85,13): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/MapAxiomsConsistency.bpl.p.expect b/Test/test21/MapAxiomsConsistency.bpl.p.expect new file mode 100644 index 00000000..eabc661f --- /dev/null +++ b/Test/test21/MapAxiomsConsistency.bpl.p.expect @@ -0,0 +1,5 @@ +MapAxiomsConsistency.bpl(100,5): Error BP5001: This assertion might not hold. +Execution trace: + MapAxiomsConsistency.bpl(85,13): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/MapOutputTypeParams.bpl b/Test/test21/MapOutputTypeParams.bpl index f0ca307f..4e83e6f1 100644 --- a/Test/test21/MapOutputTypeParams.bpl +++ b/Test/test21/MapOutputTypeParams.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
diff --git a/Test/test21/MapOutputTypeParams.bpl.a.expect b/Test/test21/MapOutputTypeParams.bpl.a.expect new file mode 100644 index 00000000..5e4aa0be --- /dev/null +++ b/Test/test21/MapOutputTypeParams.bpl.a.expect @@ -0,0 +1,12 @@ +MapOutputTypeParams.bpl(35,3): Warning: type parameter a is ambiguous, instantiating to int +MapOutputTypeParams.bpl(19,3): Error BP5001: This assertion might not hold. +Execution trace: + MapOutputTypeParams.bpl(13,9): anon0 +MapOutputTypeParams.bpl(30,3): Error BP5001: This assertion might not hold. +Execution trace: + MapOutputTypeParams.bpl(25,9): anon0 +MapOutputTypeParams.bpl(38,3): Error BP5001: This assertion might not hold. +Execution trace: + MapOutputTypeParams.bpl(34,8): anon0 + +Boogie program verifier finished with 0 verified, 3 errors diff --git a/Test/test21/MapOutputTypeParams.bpl.n.expect b/Test/test21/MapOutputTypeParams.bpl.n.expect new file mode 100644 index 00000000..3c56324d --- /dev/null +++ b/Test/test21/MapOutputTypeParams.bpl.n.expect @@ -0,0 +1,21 @@ +MapOutputTypeParams.bpl(35,3): Warning: type parameter a is ambiguous, instantiating to int +MapOutputTypeParams.bpl(18,3): Error BP5001: This assertion might not hold. +Execution trace: + MapOutputTypeParams.bpl(13,9): anon0 +MapOutputTypeParams.bpl(19,3): Error BP5001: This assertion might not hold. +Execution trace: + MapOutputTypeParams.bpl(13,9): anon0 +MapOutputTypeParams.bpl(29,3): Error BP5001: This assertion might not hold. +Execution trace: + MapOutputTypeParams.bpl(25,9): anon0 +MapOutputTypeParams.bpl(30,3): Error BP5001: This assertion might not hold. +Execution trace: + MapOutputTypeParams.bpl(25,9): anon0 +MapOutputTypeParams.bpl(37,3): Error BP5001: This assertion might not hold. +Execution trace: + MapOutputTypeParams.bpl(34,8): anon0 +MapOutputTypeParams.bpl(38,3): Error BP5001: This assertion might not hold. +Execution trace: + MapOutputTypeParams.bpl(34,8): anon0 + +Boogie program verifier finished with 0 verified, 6 errors diff --git a/Test/test21/MapOutputTypeParams.bpl.p.expect b/Test/test21/MapOutputTypeParams.bpl.p.expect new file mode 100644 index 00000000..5e4aa0be --- /dev/null +++ b/Test/test21/MapOutputTypeParams.bpl.p.expect @@ -0,0 +1,12 @@ +MapOutputTypeParams.bpl(35,3): Warning: type parameter a is ambiguous, instantiating to int +MapOutputTypeParams.bpl(19,3): Error BP5001: This assertion might not hold. +Execution trace: + MapOutputTypeParams.bpl(13,9): anon0 +MapOutputTypeParams.bpl(30,3): Error BP5001: This assertion might not hold. +Execution trace: + MapOutputTypeParams.bpl(25,9): anon0 +MapOutputTypeParams.bpl(38,3): Error BP5001: This assertion might not hold. +Execution trace: + MapOutputTypeParams.bpl(34,8): anon0 + +Boogie program verifier finished with 0 verified, 3 errors diff --git a/Test/test21/Maps0.bpl b/Test/test21/Maps0.bpl index 6c382a96..ba3a0f98 100644 --- a/Test/test21/Maps0.bpl +++ b/Test/test21/Maps0.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
const a : [int] bool;
diff --git a/Test/test21/Maps0.bpl.a.expect b/Test/test21/Maps0.bpl.a.expect new file mode 100644 index 00000000..ff15a125 --- /dev/null +++ b/Test/test21/Maps0.bpl.a.expect @@ -0,0 +1,11 @@ +Maps0.bpl(29,3): Error BP5001: This assertion might not hold. +Execution trace: + Maps0.bpl(20,3): anon0 +Maps0.bpl(38,3): Error BP5001: This assertion might not hold. +Execution trace: + Maps0.bpl(38,3): anon0 +Maps0.bpl(59,3): Error BP5001: This assertion might not hold. +Execution trace: + Maps0.bpl(47,9): anon0 + +Boogie program verifier finished with 0 verified, 3 errors diff --git a/Test/test21/Maps0.bpl.n.expect b/Test/test21/Maps0.bpl.n.expect new file mode 100644 index 00000000..4ca5c450 --- /dev/null +++ b/Test/test21/Maps0.bpl.n.expect @@ -0,0 +1,17 @@ +Maps0.bpl(29,3): Error BP5001: This assertion might not hold. +Execution trace: + Maps0.bpl(20,3): anon0 +Maps0.bpl(52,3): Error BP5001: This assertion might not hold. +Execution trace: + Maps0.bpl(47,9): anon0 +Maps0.bpl(55,3): Error BP5001: This assertion might not hold. +Execution trace: + Maps0.bpl(47,9): anon0 +Maps0.bpl(58,3): Error BP5001: This assertion might not hold. +Execution trace: + Maps0.bpl(47,9): anon0 +Maps0.bpl(59,3): Error BP5001: This assertion might not hold. +Execution trace: + Maps0.bpl(47,9): anon0 + +Boogie program verifier finished with 1 verified, 5 errors diff --git a/Test/test21/Maps0.bpl.p.expect b/Test/test21/Maps0.bpl.p.expect new file mode 100644 index 00000000..ff15a125 --- /dev/null +++ b/Test/test21/Maps0.bpl.p.expect @@ -0,0 +1,11 @@ +Maps0.bpl(29,3): Error BP5001: This assertion might not hold. +Execution trace: + Maps0.bpl(20,3): anon0 +Maps0.bpl(38,3): Error BP5001: This assertion might not hold. +Execution trace: + Maps0.bpl(38,3): anon0 +Maps0.bpl(59,3): Error BP5001: This assertion might not hold. +Execution trace: + Maps0.bpl(47,9): anon0 + +Boogie program verifier finished with 0 verified, 3 errors diff --git a/Test/test21/Maps1.bpl b/Test/test21/Maps1.bpl index 94d29e32..417521eb 100644 --- a/Test/test21/Maps1.bpl +++ b/Test/test21/Maps1.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
// different map type classes with the same arity
diff --git a/Test/test21/Maps1.bpl.a.expect b/Test/test21/Maps1.bpl.a.expect new file mode 100644 index 00000000..230f04b8 --- /dev/null +++ b/Test/test21/Maps1.bpl.a.expect @@ -0,0 +1,5 @@ +Maps1.bpl(37,3): Error BP5001: This assertion might not hold. +Execution trace: + Maps1.bpl(25,3): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Maps1.bpl.n.expect b/Test/test21/Maps1.bpl.n.expect new file mode 100644 index 00000000..48be36cc --- /dev/null +++ b/Test/test21/Maps1.bpl.n.expect @@ -0,0 +1,8 @@ +Maps1.bpl(32,3): Error BP5001: This assertion might not hold. +Execution trace: + Maps1.bpl(25,3): anon0 +Maps1.bpl(37,3): Error BP5001: This assertion might not hold. +Execution trace: + Maps1.bpl(25,3): anon0 + +Boogie program verifier finished with 0 verified, 2 errors diff --git a/Test/test21/Maps1.bpl.p.expect b/Test/test21/Maps1.bpl.p.expect new file mode 100644 index 00000000..230f04b8 --- /dev/null +++ b/Test/test21/Maps1.bpl.p.expect @@ -0,0 +1,5 @@ +Maps1.bpl(37,3): Error BP5001: This assertion might not hold. +Execution trace: + Maps1.bpl(25,3): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Maps2.bpl b/Test/test21/Maps2.bpl index 3f055c1d..1a38ae48 100644 --- a/Test/test21/Maps2.bpl +++ b/Test/test21/Maps2.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
type T;
diff --git a/Test/test21/NameClash.bpl b/Test/test21/NameClash.bpl index 6e1ade48..9b6fefa8 100644 --- a/Test/test21/NameClash.bpl +++ b/Test/test21/NameClash.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
function f(int) returns (int);
diff --git a/Test/test21/NameClash.bpl.a.expect b/Test/test21/NameClash.bpl.a.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/test21/NameClash.bpl.a.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/test21/NameClash.bpl.n.expect b/Test/test21/NameClash.bpl.n.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/test21/NameClash.bpl.n.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/test21/NameClash.bpl.p.expect b/Test/test21/NameClash.bpl.p.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/test21/NameClash.bpl.p.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/test21/Orderings.bpl b/Test/test21/Orderings.bpl index 78439bc1..6a048224 100644 --- a/Test/test21/Orderings.bpl +++ b/Test/test21/Orderings.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
const a, b:int;
diff --git a/Test/test21/Orderings.bpl.a.expect b/Test/test21/Orderings.bpl.a.expect new file mode 100644 index 00000000..a603901c --- /dev/null +++ b/Test/test21/Orderings.bpl.a.expect @@ -0,0 +1,5 @@ +Orderings.bpl(20,3): Error BP5001: This assertion might not hold. +Execution trace: + Orderings.bpl(15,3): anon0 + +Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/test21/Orderings.bpl.n.expect b/Test/test21/Orderings.bpl.n.expect new file mode 100644 index 00000000..a603901c --- /dev/null +++ b/Test/test21/Orderings.bpl.n.expect @@ -0,0 +1,5 @@ +Orderings.bpl(20,3): Error BP5001: This assertion might not hold. +Execution trace: + Orderings.bpl(15,3): anon0 + +Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/test21/Orderings.bpl.p.expect b/Test/test21/Orderings.bpl.p.expect new file mode 100644 index 00000000..a603901c --- /dev/null +++ b/Test/test21/Orderings.bpl.p.expect @@ -0,0 +1,5 @@ +Orderings.bpl(20,3): Error BP5001: This assertion might not hold. +Execution trace: + Orderings.bpl(15,3): anon0 + +Boogie program verifier finished with 1 verified, 1 error diff --git a/Test/test21/Orderings2.bpl b/Test/test21/Orderings2.bpl index 75becb2a..fe01184c 100644 --- a/Test/test21/Orderings2.bpl +++ b/Test/test21/Orderings2.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
const b:int;
diff --git a/Test/test21/Orderings2.bpl.a.expect b/Test/test21/Orderings2.bpl.a.expect new file mode 100644 index 00000000..c949b4d5 --- /dev/null +++ b/Test/test21/Orderings2.bpl.a.expect @@ -0,0 +1,5 @@ +Orderings2.bpl(23,3): Error BP5001: This assertion might not hold. +Execution trace: + Orderings2.bpl(18,3): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Orderings2.bpl.n.expect b/Test/test21/Orderings2.bpl.n.expect new file mode 100644 index 00000000..c949b4d5 --- /dev/null +++ b/Test/test21/Orderings2.bpl.n.expect @@ -0,0 +1,5 @@ +Orderings2.bpl(23,3): Error BP5001: This assertion might not hold. +Execution trace: + Orderings2.bpl(18,3): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Orderings2.bpl.p.expect b/Test/test21/Orderings2.bpl.p.expect new file mode 100644 index 00000000..c949b4d5 --- /dev/null +++ b/Test/test21/Orderings2.bpl.p.expect @@ -0,0 +1,5 @@ +Orderings2.bpl(23,3): Error BP5001: This assertion might not hold. +Execution trace: + Orderings2.bpl(18,3): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Orderings3.bpl b/Test/test21/Orderings3.bpl index c94d298c..a842be12 100644 --- a/Test/test21/Orderings3.bpl +++ b/Test/test21/Orderings3.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
// Example from the Boogie 2 language report
diff --git a/Test/test21/Orderings3.bpl.a.expect b/Test/test21/Orderings3.bpl.a.expect new file mode 100644 index 00000000..3efb7e01 --- /dev/null +++ b/Test/test21/Orderings3.bpl.a.expect @@ -0,0 +1,11 @@ +Orderings3.bpl(35,3): Error BP5001: This assertion might not hold. +Execution trace: + Orderings3.bpl(21,3): anon0 +Orderings3.bpl(40,3): Error BP5001: This assertion might not hold. +Execution trace: + Orderings3.bpl(40,3): anon0 +Orderings3.bpl(42,3): Error BP5001: This assertion might not hold. +Execution trace: + Orderings3.bpl(40,3): anon0 + +Boogie program verifier finished with 0 verified, 3 errors diff --git a/Test/test21/Orderings3.bpl.n.expect b/Test/test21/Orderings3.bpl.n.expect new file mode 100644 index 00000000..3efb7e01 --- /dev/null +++ b/Test/test21/Orderings3.bpl.n.expect @@ -0,0 +1,11 @@ +Orderings3.bpl(35,3): Error BP5001: This assertion might not hold. +Execution trace: + Orderings3.bpl(21,3): anon0 +Orderings3.bpl(40,3): Error BP5001: This assertion might not hold. +Execution trace: + Orderings3.bpl(40,3): anon0 +Orderings3.bpl(42,3): Error BP5001: This assertion might not hold. +Execution trace: + Orderings3.bpl(40,3): anon0 + +Boogie program verifier finished with 0 verified, 3 errors diff --git a/Test/test21/Orderings3.bpl.p.expect b/Test/test21/Orderings3.bpl.p.expect new file mode 100644 index 00000000..3efb7e01 --- /dev/null +++ b/Test/test21/Orderings3.bpl.p.expect @@ -0,0 +1,11 @@ +Orderings3.bpl(35,3): Error BP5001: This assertion might not hold. +Execution trace: + Orderings3.bpl(21,3): anon0 +Orderings3.bpl(40,3): Error BP5001: This assertion might not hold. +Execution trace: + Orderings3.bpl(40,3): anon0 +Orderings3.bpl(42,3): Error BP5001: This assertion might not hold. +Execution trace: + Orderings3.bpl(40,3): anon0 + +Boogie program verifier finished with 0 verified, 3 errors diff --git a/Test/test21/Orderings4.bpl b/Test/test21/Orderings4.bpl index 3058287f..62f7b7fa 100644 --- a/Test/test21/Orderings4.bpl +++ b/Test/test21/Orderings4.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
type Wicket;
diff --git a/Test/test21/Orderings4.bpl.a.expect b/Test/test21/Orderings4.bpl.a.expect new file mode 100644 index 00000000..769f76b4 --- /dev/null +++ b/Test/test21/Orderings4.bpl.a.expect @@ -0,0 +1,5 @@ +Orderings4.bpl(16,3): Error BP5001: This assertion might not hold. +Execution trace: + Orderings4.bpl(15,3): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Orderings4.bpl.n.expect b/Test/test21/Orderings4.bpl.n.expect new file mode 100644 index 00000000..769f76b4 --- /dev/null +++ b/Test/test21/Orderings4.bpl.n.expect @@ -0,0 +1,5 @@ +Orderings4.bpl(16,3): Error BP5001: This assertion might not hold. +Execution trace: + Orderings4.bpl(15,3): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Orderings4.bpl.p.expect b/Test/test21/Orderings4.bpl.p.expect new file mode 100644 index 00000000..769f76b4 --- /dev/null +++ b/Test/test21/Orderings4.bpl.p.expect @@ -0,0 +1,5 @@ +Orderings4.bpl(16,3): Error BP5001: This assertion might not hold. +Execution trace: + Orderings4.bpl(15,3): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/ParallelAssignment.bpl b/Test/test21/ParallelAssignment.bpl index 05791b8e..6bd414e9 100644 --- a/Test/test21/ParallelAssignment.bpl +++ b/Test/test21/ParallelAssignment.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
// Examples from the Boogie2 language report
type C, D;
diff --git a/Test/test21/ParallelAssignment.bpl.a.expect b/Test/test21/ParallelAssignment.bpl.a.expect new file mode 100644 index 00000000..7334a3f4 --- /dev/null +++ b/Test/test21/ParallelAssignment.bpl.a.expect @@ -0,0 +1,11 @@ +ParallelAssignment.bpl(32,3): Error BP5001: This assertion might not hold. +Execution trace: + ParallelAssignment.bpl(21,5): anon0 +ParallelAssignment.bpl(41,3): Error BP5001: This assertion might not hold. +Execution trace: + ParallelAssignment.bpl(21,5): anon0 +ParallelAssignment.bpl(60,3): Error BP5001: This assertion might not hold. +Execution trace: + ParallelAssignment.bpl(46,11): anon0 + +Boogie program verifier finished with 0 verified, 3 errors diff --git a/Test/test21/ParallelAssignment.bpl.n.expect b/Test/test21/ParallelAssignment.bpl.n.expect new file mode 100644 index 00000000..7334a3f4 --- /dev/null +++ b/Test/test21/ParallelAssignment.bpl.n.expect @@ -0,0 +1,11 @@ +ParallelAssignment.bpl(32,3): Error BP5001: This assertion might not hold. +Execution trace: + ParallelAssignment.bpl(21,5): anon0 +ParallelAssignment.bpl(41,3): Error BP5001: This assertion might not hold. +Execution trace: + ParallelAssignment.bpl(21,5): anon0 +ParallelAssignment.bpl(60,3): Error BP5001: This assertion might not hold. +Execution trace: + ParallelAssignment.bpl(46,11): anon0 + +Boogie program verifier finished with 0 verified, 3 errors diff --git a/Test/test21/ParallelAssignment.bpl.p.expect b/Test/test21/ParallelAssignment.bpl.p.expect new file mode 100644 index 00000000..7334a3f4 --- /dev/null +++ b/Test/test21/ParallelAssignment.bpl.p.expect @@ -0,0 +1,11 @@ +ParallelAssignment.bpl(32,3): Error BP5001: This assertion might not hold. +Execution trace: + ParallelAssignment.bpl(21,5): anon0 +ParallelAssignment.bpl(41,3): Error BP5001: This assertion might not hold. +Execution trace: + ParallelAssignment.bpl(21,5): anon0 +ParallelAssignment.bpl(60,3): Error BP5001: This assertion might not hold. +Execution trace: + ParallelAssignment.bpl(46,11): anon0 + +Boogie program verifier finished with 0 verified, 3 errors diff --git a/Test/test21/PolyList.bpl b/Test/test21/PolyList.bpl index 49d515f9..c68c637e 100644 --- a/Test/test21/PolyList.bpl +++ b/Test/test21/PolyList.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
diff --git a/Test/test21/PolyList.bpl.a.expect b/Test/test21/PolyList.bpl.a.expect new file mode 100644 index 00000000..26132ce3 --- /dev/null +++ b/Test/test21/PolyList.bpl.a.expect @@ -0,0 +1,8 @@ +PolyList.bpl(48,3): Error BP5001: This assertion might not hold. +Execution trace: + PolyList.bpl(33,7): anon0 +PolyList.bpl(66,3): Error BP5001: This assertion might not hold. +Execution trace: + PolyList.bpl(55,7): anon0 + +Boogie program verifier finished with 0 verified, 2 errors diff --git a/Test/test21/PolyList.bpl.n.expect b/Test/test21/PolyList.bpl.n.expect new file mode 100644 index 00000000..26132ce3 --- /dev/null +++ b/Test/test21/PolyList.bpl.n.expect @@ -0,0 +1,8 @@ +PolyList.bpl(48,3): Error BP5001: This assertion might not hold. +Execution trace: + PolyList.bpl(33,7): anon0 +PolyList.bpl(66,3): Error BP5001: This assertion might not hold. +Execution trace: + PolyList.bpl(55,7): anon0 + +Boogie program verifier finished with 0 verified, 2 errors diff --git a/Test/test21/PolyList.bpl.p.expect b/Test/test21/PolyList.bpl.p.expect new file mode 100644 index 00000000..26132ce3 --- /dev/null +++ b/Test/test21/PolyList.bpl.p.expect @@ -0,0 +1,8 @@ +PolyList.bpl(48,3): Error BP5001: This assertion might not hold. +Execution trace: + PolyList.bpl(33,7): anon0 +PolyList.bpl(66,3): Error BP5001: This assertion might not hold. +Execution trace: + PolyList.bpl(55,7): anon0 + +Boogie program verifier finished with 0 verified, 2 errors diff --git a/Test/test21/Real.bpl b/Test/test21/Real.bpl index c9a2f14d..42b1f889 100644 --- a/Test/test21/Real.bpl +++ b/Test/test21/Real.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
axiom (forall r: real :: r == 0.0 || r / r == 1.0);
procedure P(a: real, b: real) returns () {
diff --git a/Test/test21/Real.bpl.a.expect b/Test/test21/Real.bpl.a.expect new file mode 100644 index 00000000..9b8dc4f1 --- /dev/null +++ b/Test/test21/Real.bpl.a.expect @@ -0,0 +1,10 @@ +Real.bpl(32,5): Error BP5001: This assertion might not hold. +Execution trace: + Real.bpl(29,5): anon0 + Real.bpl(32,5): anon3_Then +Real.bpl(47,5): Error BP5001: This assertion might not hold. +Execution trace: + Real.bpl(40,3): anon0 + Real.bpl(47,5): anon3_Else + +Boogie program verifier finished with 2 verified, 2 errors diff --git a/Test/test21/Real.bpl.n.expect b/Test/test21/Real.bpl.n.expect new file mode 100644 index 00000000..9b8dc4f1 --- /dev/null +++ b/Test/test21/Real.bpl.n.expect @@ -0,0 +1,10 @@ +Real.bpl(32,5): Error BP5001: This assertion might not hold. +Execution trace: + Real.bpl(29,5): anon0 + Real.bpl(32,5): anon3_Then +Real.bpl(47,5): Error BP5001: This assertion might not hold. +Execution trace: + Real.bpl(40,3): anon0 + Real.bpl(47,5): anon3_Else + +Boogie program verifier finished with 2 verified, 2 errors diff --git a/Test/test21/Real.bpl.p.expect b/Test/test21/Real.bpl.p.expect new file mode 100644 index 00000000..9b8dc4f1 --- /dev/null +++ b/Test/test21/Real.bpl.p.expect @@ -0,0 +1,10 @@ +Real.bpl(32,5): Error BP5001: This assertion might not hold. +Execution trace: + Real.bpl(29,5): anon0 + Real.bpl(32,5): anon3_Then +Real.bpl(47,5): Error BP5001: This assertion might not hold. +Execution trace: + Real.bpl(40,3): anon0 + Real.bpl(47,5): anon3_Else + +Boogie program verifier finished with 2 verified, 2 errors diff --git a/Test/test21/Triggers0.bpl b/Test/test21/Triggers0.bpl index 4f7a8d11..f58b168f 100644 --- a/Test/test21/Triggers0.bpl +++ b/Test/test21/Triggers0.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
const ar : [int]bool;
diff --git a/Test/test21/Triggers0.bpl.a.expect b/Test/test21/Triggers0.bpl.a.expect new file mode 100644 index 00000000..44c7c84c --- /dev/null +++ b/Test/test21/Triggers0.bpl.a.expect @@ -0,0 +1,8 @@ +Triggers0.bpl(45,3): Error BP5001: This assertion might not hold. +Execution trace: + Triggers0.bpl(45,3): anon0 +Triggers0.bpl(49,3): Error BP5001: This assertion might not hold. +Execution trace: + Triggers0.bpl(45,3): anon0 + +Boogie program verifier finished with 1 verified, 2 errors diff --git a/Test/test21/Triggers0.bpl.n.expect b/Test/test21/Triggers0.bpl.n.expect new file mode 100644 index 00000000..44c7c84c --- /dev/null +++ b/Test/test21/Triggers0.bpl.n.expect @@ -0,0 +1,8 @@ +Triggers0.bpl(45,3): Error BP5001: This assertion might not hold. +Execution trace: + Triggers0.bpl(45,3): anon0 +Triggers0.bpl(49,3): Error BP5001: This assertion might not hold. +Execution trace: + Triggers0.bpl(45,3): anon0 + +Boogie program verifier finished with 1 verified, 2 errors diff --git a/Test/test21/Triggers0.bpl.p.expect b/Test/test21/Triggers0.bpl.p.expect new file mode 100644 index 00000000..44c7c84c --- /dev/null +++ b/Test/test21/Triggers0.bpl.p.expect @@ -0,0 +1,8 @@ +Triggers0.bpl(45,3): Error BP5001: This assertion might not hold. +Execution trace: + Triggers0.bpl(45,3): anon0 +Triggers0.bpl(49,3): Error BP5001: This assertion might not hold. +Execution trace: + Triggers0.bpl(45,3): anon0 + +Boogie program verifier finished with 1 verified, 2 errors diff --git a/Test/test21/Triggers1.bpl b/Test/test21/Triggers1.bpl index 3633e704..63a780f5 100644 --- a/Test/test21/Triggers1.bpl +++ b/Test/test21/Triggers1.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
diff --git a/Test/test21/Triggers1.bpl.a.expect b/Test/test21/Triggers1.bpl.a.expect new file mode 100644 index 00000000..817ddf31 --- /dev/null +++ b/Test/test21/Triggers1.bpl.a.expect @@ -0,0 +1,5 @@ +Triggers1.bpl(22,3): Error BP5001: This assertion might not hold. +Execution trace: + Triggers1.bpl(18,3): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/Triggers1.bpl.n.expect b/Test/test21/Triggers1.bpl.n.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/test21/Triggers1.bpl.n.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/test21/Triggers1.bpl.p.expect b/Test/test21/Triggers1.bpl.p.expect new file mode 100644 index 00000000..817ddf31 --- /dev/null +++ b/Test/test21/Triggers1.bpl.p.expect @@ -0,0 +1,5 @@ +Triggers1.bpl(22,3): Error BP5001: This assertion might not hold. +Execution trace: + Triggers1.bpl(18,3): anon0 + +Boogie program verifier finished with 0 verified, 1 error diff --git a/Test/test21/test3_AddMethod_conv.bpl b/Test/test21/test3_AddMethod_conv.bpl index 1382fdeb..ad4baba8 100644 --- a/Test/test21/test3_AddMethod_conv.bpl +++ b/Test/test21/test3_AddMethod_conv.bpl @@ -1,3 +1,9 @@ +// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t
+// RUN: %diff %s.n.expect %t
+// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t
+// RUN: %diff %s.p.expect %t
+// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t
+// RUN: %diff %s.a.expect %t
// Spec# program verifier version 0.90, Copyright (c) 2003-2008, Microsoft.
// Command Line Options: /print:debug.txt AddMethod.dll
|