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