Enabled "Verify Boogie 2" lit tests. Note the following tests fail

because they were never properly tested in the the old testing
infrastructure.

test21/Maps2.bpl
test21/test3_AddMethod_conv.bpl

1 files changed, 347 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 ----------------------------