Initial set of files.

author: mikebarnett <unknown> 2009-07-15 21:03:41 +0000
committer: mikebarnett <unknown> 2009-07-15 21:03:41 +0000
commit: ce1c2de044c91624370411e23acab13b0381949b (patch)
tree: 592539996fe08050ead5ee210c973801611dde40 /Test/test20
21 files changed, 937 insertions, 0 deletions
diff --git a/Test/test20/Answer b/Test/test20/Answer
new file mode 100644
index 00000000..a4b991f7
--- /dev/null
+++ b/Test/test20/Answer
@@ -0,0 +1,192 @@
+TypeDecls0.bpl(20,5): Error: more than one declaration of type name: C
+TypeDecls0.bpl(13,12): Error: more than one declaration of type variable: a
+TypeDecls0.bpl(14,18): Error: more than one declaration of type variable: a
+TypeDecls0.bpl(18,17): Error: type variable must occur in map arguments: b
+TypeDecls0.bpl(22,9): Error: type constructor received wrong number of arguments: C
+TypeDecls0.bpl(24,9): Error: undeclared type: A0
+TypeDecls0.bpl(25,9): Error: undeclared type: F
+TypeDecls0.bpl(28,9): Error: type constructor received wrong number of arguments: E
+TypeDecls0.bpl(30,9): Error: type constructor received wrong number of arguments: E
+TypeDecls0.bpl(32,9): Error: type constructor received wrong number of arguments: E
+TypeDecls0.bpl(38,11): Error: type constructor received wrong number of arguments: E
+TypeDecls0.bpl(38,13): Error: type constructor received wrong number of arguments: E
+12 name resolution errors detected in TypeDecls0.bpl
+TypeDecls1.bpl(7,13): Error: invalid type for argument 0 in map select: int (expected: <b>[b]a)
+TypeDecls1.bpl(13,25): Error: right-hand side in map store with wrong type: int (expected: bool)
+TypeDecls1.bpl(19,36): Error: invalid type for argument 0 in map select: <c>[c]c (expected: <b>[b]a)
+TypeDecls1.bpl(21,13): Error: invalid type for argument 0 in map select: <a>[<b>[b]a]bool (expected: <b>[b]a)
+4 type checking errors detected in TypeDecls1.bpl
+Prog0.bpl(17,10): Error: type variable must occur in map arguments: a
+Prog0.bpl(29,27): Error: more than one declaration of type variable: beta
+Prog0.bpl(32,22): Error: undeclared type: alpha
+Prog0.bpl(33,35): Error: undeclared type: alpha
+4 name resolution errors detected in Prog0.bpl
+Prog1.bpl(18,11): Error: invalid type for argument 0 in map select: int (expected: ref)
+Prog1.bpl(19,14): Error: invalid type for argument 1 in map select: int (expected: Field a)
+Prog1.bpl(20,17): Error: invalid argument types (bool and int) to binary operator >=
+3 type checking errors detected in Prog1.bpl
+Prog2.bpl(6,14): Error: trigger does not mention alpha, which does not occur in variables types either
+1 type checking errors detected in Prog2.bpl
+PolyFuns0.bpl(23,33): Error: invalid type for argument 1 in application of fieldValue: ref (expected: Field a)
+PolyFuns0.bpl(40,18): Error: invalid type for argument 1 in application of lessThan: bool (expected: a)
+PolyFuns0.bpl(41,43): Error: invalid type for argument 1 in application of lessThan: b (expected: a)
+PolyFuns0.bpl(53,55): Error: invalid argument types (<c>[Field c]a and <d>[Field d]d) to binary operator ==
+4 type checking errors detected in PolyFuns0.bpl
+PolyFuns1.bpl(10,9): Error: invalid type for argument 0 in application of F: <c>[c]c (expected: <b>[b]a)
+PolyFuns1.bpl(11,9): Error: invalid type for argument 0 in map select: <c>[c]c (expected: <b>[b]a)
+PolyFuns1.bpl(12,31): Error: invalid type for argument 0 in application of F: <c>[c]c (expected: <b>[b]a)
+PolyFuns1.bpl(13,31): Error: invalid type for argument 0 in map select: <c>[c]c (expected: <b>[b]a)
+PolyFuns1.bpl(17,55): Error: invalid argument types (<c>[Field c]a and <d>[Field d]d) to binary operator ==
+PolyFuns1.bpl(18,55): Error: invalid argument types (<c>[Field c]a and <d>[Field d]d) to binary operator ==
+PolyFuns1.bpl(28,11): Error: invalid type for argument 0 in call to Uhu: <dd>[Field dd]dd (expected: <c>[Field c]a)
+PolyFuns1.bpl(29,15): Error: invalid type for argument 1 in call to Uhu: <cc>[Field cc]T (expected: <d>[Field d]d)
+PolyFuns1.bpl(30,12): Error: invalid argument types (<cc>[Field cc]T and <dd>[Field dd]dd) to binary operator ==
+PolyFuns1.bpl(31,12): Error: invalid argument types (<dd>[Field dd]dd and <cc>[Field cc]T) to binary operator ==
+PolyFuns1.bpl(33,15): Error: invalid type for argument 1 in call to Uhu: <ee>[Field T]ee (expected: <d>[Field d]d)
+PolyFuns1.bpl(41,11): Error: invalid argument types (<a>[a,a]int and <b>[b,int]int) to binary operator ==
+PolyFuns1.bpl(42,11): Error: invalid argument types (<b>[b,int]int and <c>[int,c]int) to binary operator ==
+PolyFuns1.bpl(43,11): Error: invalid argument types (<a>[a,a]int and <c>[int,c]int) to binary operator ==
+PolyFuns1.bpl(50,11): Error: invalid argument types (<a,b>[a,a,b]int and <a,b>[a,b,b]int) to binary operator ==
+PolyFuns1.bpl(57,54): Error: invalid argument types (Field b and NagainCtor b) to binary operator ==
+16 type checking errors detected in PolyFuns1.bpl
+PolyProcs0.bpl(11,16): Error: invalid type for argument 0 in map select: Field b (expected: ref)
+PolyProcs0.bpl(11,19): Error: invalid type for argument 1 in map select: ref (expected: Field a)
+PolyProcs0.bpl(21,30): Error: invalid type for argument 1 in call to FieldAccess: Field int (expected: ref)
+PolyProcs0.bpl(21,34): Error: invalid type for argument 2 in call to FieldAccess: ref (expected: Field b)
+PolyProcs0.bpl(25,7): Error: invalid type for out-parameter 0 in call to FieldAccess: bool (expected: int)
+PolyProcs0.bpl(26,35): Error: invalid type for argument 2 in call to FieldAccess: ref (expected: Field b)
+PolyProcs0.bpl(41,35): Error: invalid type for argument 1 in call forall to injective: Field int (expected: ref)
+7 type checking errors detected in PolyProcs0.bpl
+TypeSynonyms0.bpl(9,5): Error: type synonym could not be resolved because of cycles: Cyclic0 (replacing body with "bool" to continue resolving)
+TypeSynonyms0.bpl(10,5): Error: type synonym could not be resolved because of cycles: Cyclic1 (replacing body with "bool" to continue resolving)
+TypeSynonyms0.bpl(12,5): Error: type synonym could not be resolved because of cycles: AlsoCyclic (replacing body with "bool" to continue resolving)
+TypeSynonyms0.bpl(22,10): Error: type constructor received wrong number of arguments: Field
+TypeSynonyms0.bpl(23,10): Error: type synonym received wrong number of arguments: Set
+TypeSynonyms0.bpl(26,10): Error: type variable must occur in map arguments: a
+6 name resolution errors detected in TypeSynonyms0.bpl
+TypeSynonyms1.bpl(46,8): Error: invalid type for argument 0 in application of h: <b>[b,b,<b2>[b2,b,int]int]int (expected: nested2)
+1 type checking errors detected in TypeSynonyms1.bpl
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+type Set a = [a]bool;
+
+type Field _;
+
+type Heap = <a>[ref,Field a]a;
+
+type notAllParams a b = Field b;
+
+type Cyclic0 = Cyclic1;
+
+type Cyclic1 = Cyclic0;
+
+type AlsoCyclic a = <b>[AlsoCyclic b]int;
+
+type C _ _;
+
+type C2 b a = C a b;
+
+function f(C int bool) returns (int);
+
+const x: C2 bool int;
+
+const y: Field int bool;
+
+const z: Set int bool;
+
+const d: <a,b>[notAllParams a b]int;
+
+type ref;
+<console>(10,-1): Error: type synonym could not be resolved because of cycles: Cyclic0 (replacing body with "bool" to continue resolving)
+<console>(12,-1): Error: type synonym could not be resolved because of cycles: Cyclic1 (replacing body with "bool" to continue resolving)
+<console>(14,-1): Error: type synonym could not be resolved because of cycles: AlsoCyclic (replacing body with "bool" to continue resolving)
+<console>(24,8): Error: type constructor received wrong number of arguments: Field
+<console>(26,8): Error: type synonym received wrong number of arguments: Set
+<console>(28,8): Error: type variable must occur in map arguments: a
+6 name resolution errors detected in TypeSynonyms0.bpl
+
+type Set a = [a]bool;
+
+function union<a>(x: Set a, y: Set a) returns (Set a);
+
+axiom (forall<a> x: Set a, y: Set a, z: a :: (x[z] || y[z]) == union(x, y)[z]);
+
+const intSet0: Set int;
+
+axiom (forall x: int :: intSet0[x] == (x == 0 || x == 2 || x == 3));
+
+const intSet1: Set int;
+
+axiom (forall x: int :: intSet1[x] == (x == 0 - 5 || x == 3));
+
+procedure P();
+
+
+
+implementation P()
+{
+    assert (forall x: int :: union(intSet0, intSet1)[x] == (x == 0 - 5 || x == 0 || x == 2 || x == 3));
+}
+
+
+
+type Set a = [a]bool;
+
+function union<a>(x: Set a, y: Set a) returns (Set a);
+
+axiom (forall<a> x: Set a, y: Set a, z: a :: x[z] || y[z] <==> union(x, y)[z]);
+
+const intSet0: Set int;
+
+axiom (forall x: int :: intSet0[x] <==> x == 0 || x == 2 || x == 3);
+
+const intSet1: Set int;
+
+axiom (forall x: int :: intSet1[x] <==> x == 0 - 5 || x == 3);
+
+procedure P();
+
+
+
+implementation P()
+{
+    assert (forall x: int :: union(intSet0, intSet1)[x] <==> x == 0 - 5 || x == 0 || x == 2 || x == 3);
+}
+
+
+
+Boogie program verifier finished with 0 verified, 0 errors
+PolyPolyPoly.bpl(12,26): Error: invalid argument types ([]? and <a>[]C a) to binary operator ==
+PolyPolyPoly.bpl(15,23): Error: invalid argument types ([]? and <a>[]C a) to binary operator ==
+PolyPolyPoly.bpl(21,57): Error: invalid type for argument 1 in map select: b (expected: a)
+3 type checking errors detected in PolyPolyPoly.bpl
+PolyPolyPoly2.bpl(5,8): Warning: type parameter a is ambiguous, instantiating to int
+PolyPolyPoly2.bpl(7,8): Warning: type parameter a is ambiguous, instantiating to <arg0,res>[arg0]res
+PolyPolyPoly2.bpl(11,8): Warning: type parameter a is ambiguous, instantiating to bv0
+PolyPolyPoly2.bpl(11,15): Warning: type parameter a is ambiguous, instantiating to bv0
+PolyPolyPoly2.bpl(11,27): Warning: type parameter a is ambiguous, instantiating to bv17
+PolyPolyPoly2.bpl(12,8): Warning: type parameter a is ambiguous, instantiating to bv17
+PolyPolyPoly2.bpl(12,15): Warning: type parameter a is ambiguous, instantiating to bv0
+PolyPolyPoly2.bpl(22,7): Warning: type parameter a is ambiguous, instantiating to int
+PolyPolyPoly2.bpl(31,3): Warning: type parameter a is ambiguous, instantiating to int
+PolyPolyPoly2.bpl(32,3): Warning: type parameter a is ambiguous, instantiating to int
+
+Boogie program verifier finished with 0 verified, 0 errors
+ProcParamReordering.bpl(13,15): Error: mismatched type of in-parameter in implementation P: y (named b in implementation)
+ProcParamReordering.bpl(15,15): Error: mismatched number of type parameters in procedure implementation: P
+2 type checking errors detected in ProcParamReordering.bpl
+ParallelAssignment.bpl(17,2): Error: mismatched types in assignment command (cannot assign bool to int)
+ParallelAssignment.bpl(18,4): Error: invalid type for argument 0 in map assignment: bool (expected: int)
+ParallelAssignment.bpl(20,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: z
+3 type checking errors detected in ParallelAssignment.bpl
+ParallelAssignment2.bpl(9,7): Error: number of left-hand sides does not match number of right-hand sides
+ParallelAssignment2.bpl(10,9): Error: variable a is assigned more than once in parallel assignment
+2 name resolution errors detected in ParallelAssignment2.bpl
+Coercions.bpl(11,8): Error: int cannot be coerced to E <a>[a]int
+Coercions.bpl(13,8): Error: C cannot be coerced to D
+Coercions.bpl(15,9): Error: int cannot be coerced to D
+Coercions.bpl(16,9): Error: int cannot be coerced to E int
+4 type checking errors detected in Coercions.bpl
+
+Boogie program verifier finished with 0 verified, 0 errors
diff --git a/Test/test20/Coercions.bpl b/Test/test20/Coercions.bpl
new file mode 100644
index 00000000..cab68149
--- /dev/null
+++ b/Test/test20/Coercions.bpl
@@ -0,0 +1,17 @@
+
+
+type C, D, E _;
+
+const x:int;
+const c:C;
+const d:D;
+
+axiom (x:int > 0);
+axiom (x:int < 0);
+axiom (x:E <a>[a]int < 0);   // impossible coercion
+
+axiom (c:D == d);            // impossible coercion
+
+axiom (15:D == d);           // impossible coercion
+axiom (15:E int == d);       // impossible coercion
+axiom ((18*15):int == 0);
diff --git a/Test/test20/EmptySeq.bpl b/Test/test20/EmptySeq.bpl
new file mode 100644
index 00000000..8fecfdf4
--- /dev/null
+++ b/Test/test20/EmptySeq.bpl
@@ -0,0 +1,6 @@
+type Seq T;
+
+function Seq#Length<T>(Seq T) returns (int);
+function Seq#Empty<T>() returns (Seq T);
+
+axiom (forall<T> :: Seq#Length(Seq#Empty(): Seq T) == 0);
diff --git a/Test/test20/Output b/Test/test20/Output
new file mode 100644
index 00000000..a4b991f7
--- /dev/null
+++ b/Test/test20/Output
@@ -0,0 +1,192 @@
+TypeDecls0.bpl(20,5): Error: more than one declaration of type name: C
+TypeDecls0.bpl(13,12): Error: more than one declaration of type variable: a
+TypeDecls0.bpl(14,18): Error: more than one declaration of type variable: a
+TypeDecls0.bpl(18,17): Error: type variable must occur in map arguments: b
+TypeDecls0.bpl(22,9): Error: type constructor received wrong number of arguments: C
+TypeDecls0.bpl(24,9): Error: undeclared type: A0
+TypeDecls0.bpl(25,9): Error: undeclared type: F
+TypeDecls0.bpl(28,9): Error: type constructor received wrong number of arguments: E
+TypeDecls0.bpl(30,9): Error: type constructor received wrong number of arguments: E
+TypeDecls0.bpl(32,9): Error: type constructor received wrong number of arguments: E
+TypeDecls0.bpl(38,11): Error: type constructor received wrong number of arguments: E
+TypeDecls0.bpl(38,13): Error: type constructor received wrong number of arguments: E
+12 name resolution errors detected in TypeDecls0.bpl
+TypeDecls1.bpl(7,13): Error: invalid type for argument 0 in map select: int (expected: <b>[b]a)
+TypeDecls1.bpl(13,25): Error: right-hand side in map store with wrong type: int (expected: bool)
+TypeDecls1.bpl(19,36): Error: invalid type for argument 0 in map select: <c>[c]c (expected: <b>[b]a)
+TypeDecls1.bpl(21,13): Error: invalid type for argument 0 in map select: <a>[<b>[b]a]bool (expected: <b>[b]a)
+4 type checking errors detected in TypeDecls1.bpl
+Prog0.bpl(17,10): Error: type variable must occur in map arguments: a
+Prog0.bpl(29,27): Error: more than one declaration of type variable: beta
+Prog0.bpl(32,22): Error: undeclared type: alpha
+Prog0.bpl(33,35): Error: undeclared type: alpha
+4 name resolution errors detected in Prog0.bpl
+Prog1.bpl(18,11): Error: invalid type for argument 0 in map select: int (expected: ref)
+Prog1.bpl(19,14): Error: invalid type for argument 1 in map select: int (expected: Field a)
+Prog1.bpl(20,17): Error: invalid argument types (bool and int) to binary operator >=
+3 type checking errors detected in Prog1.bpl
+Prog2.bpl(6,14): Error: trigger does not mention alpha, which does not occur in variables types either
+1 type checking errors detected in Prog2.bpl
+PolyFuns0.bpl(23,33): Error: invalid type for argument 1 in application of fieldValue: ref (expected: Field a)
+PolyFuns0.bpl(40,18): Error: invalid type for argument 1 in application of lessThan: bool (expected: a)
+PolyFuns0.bpl(41,43): Error: invalid type for argument 1 in application of lessThan: b (expected: a)
+PolyFuns0.bpl(53,55): Error: invalid argument types (<c>[Field c]a and <d>[Field d]d) to binary operator ==
+4 type checking errors detected in PolyFuns0.bpl
+PolyFuns1.bpl(10,9): Error: invalid type for argument 0 in application of F: <c>[c]c (expected: <b>[b]a)
+PolyFuns1.bpl(11,9): Error: invalid type for argument 0 in map select: <c>[c]c (expected: <b>[b]a)
+PolyFuns1.bpl(12,31): Error: invalid type for argument 0 in application of F: <c>[c]c (expected: <b>[b]a)
+PolyFuns1.bpl(13,31): Error: invalid type for argument 0 in map select: <c>[c]c (expected: <b>[b]a)
+PolyFuns1.bpl(17,55): Error: invalid argument types (<c>[Field c]a and <d>[Field d]d) to binary operator ==
+PolyFuns1.bpl(18,55): Error: invalid argument types (<c>[Field c]a and <d>[Field d]d) to binary operator ==
+PolyFuns1.bpl(28,11): Error: invalid type for argument 0 in call to Uhu: <dd>[Field dd]dd (expected: <c>[Field c]a)
+PolyFuns1.bpl(29,15): Error: invalid type for argument 1 in call to Uhu: <cc>[Field cc]T (expected: <d>[Field d]d)
+PolyFuns1.bpl(30,12): Error: invalid argument types (<cc>[Field cc]T and <dd>[Field dd]dd) to binary operator ==
+PolyFuns1.bpl(31,12): Error: invalid argument types (<dd>[Field dd]dd and <cc>[Field cc]T) to binary operator ==
+PolyFuns1.bpl(33,15): Error: invalid type for argument 1 in call to Uhu: <ee>[Field T]ee (expected: <d>[Field d]d)
+PolyFuns1.bpl(41,11): Error: invalid argument types (<a>[a,a]int and <b>[b,int]int) to binary operator ==
+PolyFuns1.bpl(42,11): Error: invalid argument types (<b>[b,int]int and <c>[int,c]int) to binary operator ==
+PolyFuns1.bpl(43,11): Error: invalid argument types (<a>[a,a]int and <c>[int,c]int) to binary operator ==
+PolyFuns1.bpl(50,11): Error: invalid argument types (<a,b>[a,a,b]int and <a,b>[a,b,b]int) to binary operator ==
+PolyFuns1.bpl(57,54): Error: invalid argument types (Field b and NagainCtor b) to binary operator ==
+16 type checking errors detected in PolyFuns1.bpl
+PolyProcs0.bpl(11,16): Error: invalid type for argument 0 in map select: Field b (expected: ref)
+PolyProcs0.bpl(11,19): Error: invalid type for argument 1 in map select: ref (expected: Field a)
+PolyProcs0.bpl(21,30): Error: invalid type for argument 1 in call to FieldAccess: Field int (expected: ref)
+PolyProcs0.bpl(21,34): Error: invalid type for argument 2 in call to FieldAccess: ref (expected: Field b)
+PolyProcs0.bpl(25,7): Error: invalid type for out-parameter 0 in call to FieldAccess: bool (expected: int)
+PolyProcs0.bpl(26,35): Error: invalid type for argument 2 in call to FieldAccess: ref (expected: Field b)
+PolyProcs0.bpl(41,35): Error: invalid type for argument 1 in call forall to injective: Field int (expected: ref)
+7 type checking errors detected in PolyProcs0.bpl
+TypeSynonyms0.bpl(9,5): Error: type synonym could not be resolved because of cycles: Cyclic0 (replacing body with "bool" to continue resolving)
+TypeSynonyms0.bpl(10,5): Error: type synonym could not be resolved because of cycles: Cyclic1 (replacing body with "bool" to continue resolving)
+TypeSynonyms0.bpl(12,5): Error: type synonym could not be resolved because of cycles: AlsoCyclic (replacing body with "bool" to continue resolving)
+TypeSynonyms0.bpl(22,10): Error: type constructor received wrong number of arguments: Field
+TypeSynonyms0.bpl(23,10): Error: type synonym received wrong number of arguments: Set
+TypeSynonyms0.bpl(26,10): Error: type variable must occur in map arguments: a
+6 name resolution errors detected in TypeSynonyms0.bpl
+TypeSynonyms1.bpl(46,8): Error: invalid type for argument 0 in application of h: <b>[b,b,<b2>[b2,b,int]int]int (expected: nested2)
+1 type checking errors detected in TypeSynonyms1.bpl
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+type Set a = [a]bool;
+
+type Field _;
+
+type Heap = <a>[ref,Field a]a;
+
+type notAllParams a b = Field b;
+
+type Cyclic0 = Cyclic1;
+
+type Cyclic1 = Cyclic0;
+
+type AlsoCyclic a = <b>[AlsoCyclic b]int;
+
+type C _ _;
+
+type C2 b a = C a b;
+
+function f(C int bool) returns (int);
+
+const x: C2 bool int;
+
+const y: Field int bool;
+
+const z: Set int bool;
+
+const d: <a,b>[notAllParams a b]int;
+
+type ref;
+<console>(10,-1): Error: type synonym could not be resolved because of cycles: Cyclic0 (replacing body with "bool" to continue resolving)
+<console>(12,-1): Error: type synonym could not be resolved because of cycles: Cyclic1 (replacing body with "bool" to continue resolving)
+<console>(14,-1): Error: type synonym could not be resolved because of cycles: AlsoCyclic (replacing body with "bool" to continue resolving)
+<console>(24,8): Error: type constructor received wrong number of arguments: Field
+<console>(26,8): Error: type synonym received wrong number of arguments: Set
+<console>(28,8): Error: type variable must occur in map arguments: a
+6 name resolution errors detected in TypeSynonyms0.bpl
+
+type Set a = [a]bool;
+
+function union<a>(x: Set a, y: Set a) returns (Set a);
+
+axiom (forall<a> x: Set a, y: Set a, z: a :: (x[z] || y[z]) == union(x, y)[z]);
+
+const intSet0: Set int;
+
+axiom (forall x: int :: intSet0[x] == (x == 0 || x == 2 || x == 3));
+
+const intSet1: Set int;
+
+axiom (forall x: int :: intSet1[x] == (x == 0 - 5 || x == 3));
+
+procedure P();
+
+
+
+implementation P()
+{
+    assert (forall x: int :: union(intSet0, intSet1)[x] == (x == 0 - 5 || x == 0 || x == 2 || x == 3));
+}
+
+
+
+type Set a = [a]bool;
+
+function union<a>(x: Set a, y: Set a) returns (Set a);
+
+axiom (forall<a> x: Set a, y: Set a, z: a :: x[z] || y[z] <==> union(x, y)[z]);
+
+const intSet0: Set int;
+
+axiom (forall x: int :: intSet0[x] <==> x == 0 || x == 2 || x == 3);
+
+const intSet1: Set int;
+
+axiom (forall x: int :: intSet1[x] <==> x == 0 - 5 || x == 3);
+
+procedure P();
+
+
+
+implementation P()
+{
+    assert (forall x: int :: union(intSet0, intSet1)[x] <==> x == 0 - 5 || x == 0 || x == 2 || x == 3);
+}
+
+
+
+Boogie program verifier finished with 0 verified, 0 errors
+PolyPolyPoly.bpl(12,26): Error: invalid argument types ([]? and <a>[]C a) to binary operator ==
+PolyPolyPoly.bpl(15,23): Error: invalid argument types ([]? and <a>[]C a) to binary operator ==
+PolyPolyPoly.bpl(21,57): Error: invalid type for argument 1 in map select: b (expected: a)
+3 type checking errors detected in PolyPolyPoly.bpl
+PolyPolyPoly2.bpl(5,8): Warning: type parameter a is ambiguous, instantiating to int
+PolyPolyPoly2.bpl(7,8): Warning: type parameter a is ambiguous, instantiating to <arg0,res>[arg0]res
+PolyPolyPoly2.bpl(11,8): Warning: type parameter a is ambiguous, instantiating to bv0
+PolyPolyPoly2.bpl(11,15): Warning: type parameter a is ambiguous, instantiating to bv0
+PolyPolyPoly2.bpl(11,27): Warning: type parameter a is ambiguous, instantiating to bv17
+PolyPolyPoly2.bpl(12,8): Warning: type parameter a is ambiguous, instantiating to bv17
+PolyPolyPoly2.bpl(12,15): Warning: type parameter a is ambiguous, instantiating to bv0
+PolyPolyPoly2.bpl(22,7): Warning: type parameter a is ambiguous, instantiating to int
+PolyPolyPoly2.bpl(31,3): Warning: type parameter a is ambiguous, instantiating to int
+PolyPolyPoly2.bpl(32,3): Warning: type parameter a is ambiguous, instantiating to int
+
+Boogie program verifier finished with 0 verified, 0 errors
+ProcParamReordering.bpl(13,15): Error: mismatched type of in-parameter in implementation P: y (named b in implementation)
+ProcParamReordering.bpl(15,15): Error: mismatched number of type parameters in procedure implementation: P
+2 type checking errors detected in ProcParamReordering.bpl
+ParallelAssignment.bpl(17,2): Error: mismatched types in assignment command (cannot assign bool to int)
+ParallelAssignment.bpl(18,4): Error: invalid type for argument 0 in map assignment: bool (expected: int)
+ParallelAssignment.bpl(20,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: z
+3 type checking errors detected in ParallelAssignment.bpl
+ParallelAssignment2.bpl(9,7): Error: number of left-hand sides does not match number of right-hand sides
+ParallelAssignment2.bpl(10,9): Error: variable a is assigned more than once in parallel assignment
+2 name resolution errors detected in ParallelAssignment2.bpl
+Coercions.bpl(11,8): Error: int cannot be coerced to E <a>[a]int
+Coercions.bpl(13,8): Error: C cannot be coerced to D
+Coercions.bpl(15,9): Error: int cannot be coerced to D
+Coercions.bpl(16,9): Error: int cannot be coerced to E int
+4 type checking errors detected in Coercions.bpl
+
+Boogie program verifier finished with 0 verified, 0 errors
diff --git a/Test/test20/ParallelAssignment.bpl b/Test/test20/ParallelAssignment.bpl
new file mode 100644
index 00000000..3ca196c8
--- /dev/null
+++ b/Test/test20/ParallelAssignment.bpl
@@ -0,0 +1,23 @@
+// Examples from the Boogie2 language report
+// (stuff where resolution succeeds, but typechecking might fail)
+
+type C, D;
+
+var x : int;
+var y : int;
+var z : int;
+var a : [int]int;
+var b : [int][C, D]int;
+
+procedure P(i:int, j:int, m:C, n:D) returns () modifies x, y, a, b; {
+  x := x+1;
+  a[i] := 12;
+  x, y := y, x;
+  x, a[i] := x+1, x;
+  x := true;            // type error
+  a[true] := 5;         // type error
+
+  z := 23;              // assignment to non-modifiable variable
+  b[i][m, n] := 17;
+  b[i][m, n], x := a[x], y;
+}
+\ No newline at end of file
diff --git a/Test/test20/ParallelAssignment2.bpl b/Test/test20/ParallelAssignment2.bpl
new file mode 100644
index 00000000..7d1f0daf
--- /dev/null
+++ b/Test/test20/ParallelAssignment2.bpl
@@ -0,0 +1,11 @@
+// Examples from the Boogie2 language report
+// (examples where already resolution fails)
+
+var x : int;
+var y : int;
+var a : [int]int;
+
+procedure P(i:int, j:int) returns () modifies x, y, a; {
+  x, y := 1;                     // wrong number of rhss
+  a[i], a[j] := a[j], a[i];      // variable assigned more than once
+}
+\ No newline at end of file
diff --git a/Test/test20/PolyFuns0.bpl b/Test/test20/PolyFuns0.bpl
new file mode 100644
index 00000000..938bc197
--- /dev/null
+++ b/Test/test20/PolyFuns0.bpl
@@ -0,0 +1,55 @@
+
+
+function size<alpha>(x : alpha) returns (int);
+
+axiom (forall x:int :: size(x) == 0);
+axiom (forall<alpha> x:alpha :: size(x) >= 0);
+
+axiom (forall m:[int]int, x:int :: size(m) >= m[x]);
+axiom (forall m:<a>[a]int :: size(m) == 13);
+
+type Field a;
+
+function fieldValue<a>(ref, Field a) returns (a);
+
+const intField : Field int;
+const refField : Field ref;
+const obj : ref;
+const someInt : int;
+
+axiom someInt == fieldValue(obj, intField);
+axiom someInt == fieldValue(fieldValue(obj, refField), intField);
+
+axiom someInt == fieldValue(obj, fieldValue(obj, refField)); // error: wrong argument type
+
+axiom (forall<a> f : Field a ::
+           (exists x:a :: fieldValue(obj, f) == x));
+
+axiom (forall<beta, alpha> a:alpha, b:beta ::
+              a == b ==> (exists c:alpha :: c == b));
+axiom (forall<a> f : Field a ::
+           (exists<b> x:b :: fieldValue(obj, f) == x));
+axiom (forall<a> f : Field a ::
+           (exists x:int :: fieldValue(obj, f) == x));
+
+function lessThan<a>(x : a, y : a) returns (bool);
+
+axiom (forall x:int, y:int :: x < y ==> lessThan(x, y));
+axiom lessThan(false, true);
+
+axiom lessThan(5, true);                          // error: incompatible arguments
+axiom (forall<a,b> x:a, y:b :: lessThan(x, y));   // error: incompatible arguments
+
+function lessThan2<a,b>(x : a, y : b) returns (bool);
+
+axiom (forall<a> x:a, y:a :: lessThan(x,y) == lessThan2(x,y));
+axiom (forall<a> x:a :: (exists m:a :: (forall y:a :: lessThan2(m, y))));
+
+axiom (exists<a,b> x:a, y:b :: lessThan2(x, y) == lessThan2(y, x));
+
+axiom (exists<a,b> x:<c>[Field c]a, y:<d>[Field d]b :: x == y);
+axiom (exists<a> x:<c>[Field c]a, y:<d>[Field d]int :: x == y);
+axiom (exists<a> x:<c>[Field c]int, y:<d>[Field d]a :: x == y);
+axiom (exists<a> x:<c>[Field c]a, y:<d>[Field d]d :: x == y);   // error: not unifiable
+
+type ref;
diff --git a/Test/test20/PolyFuns1.bpl b/Test/test20/PolyFuns1.bpl
new file mode 100644
index 00000000..eaca67bf
--- /dev/null
+++ b/Test/test20/PolyFuns1.bpl
@@ -0,0 +1,59 @@
+
+function F<a>( <b>[b]a ) returns (bool);
+const M:  <a>[ <b>[b]a ] bool;
+
+procedure P()
+{
+  var f: <c>[c]c;
+  var b: bool;
+
+  b := F(f);  // type error
+  b := M[f];  // type error
+  b := (forall g: <c>[c]c :: F(g));  // type error
+  b := (forall g: <c>[c]c :: M[g]);  // type error
+}
+
+type Field a;
+axiom (exists<a> x:<c>[Field c]a, y:<d>[Field d]d :: x == y);   // error: not unifiable
+axiom (forall<a> x:<c>[Field c]a, y:<d>[Field d]d :: x == y);   // error: not unifiable
+
+procedure Uhu<a>(x: <c>[Field c]a, y: <d>[Field d]d);
+procedure Oyeah<T>(t: T)
+{
+  var xx: <cc>[Field cc]T;
+  var yy: <dd>[Field dd]dd;
+  var zz: <ee>[Field T]ee;
+
+  call Uhu(xx, yy);
+  call Uhu(yy, yy);  // type error in argument 0
+  call Uhu(xx, xx);  // type error in argument 1
+  assert xx == yy;  // error: not unifiable
+  assert yy == xx;  // error: not unifiable
+
+  call Uhu(xx, zz);  // type error in argument 1
+}
+
+procedure Jitters()
+{
+  var x: <a>[a,a]int;
+  var y: <b>[b,int]int;
+  var z: <c>[int,c]int;
+  assert x == y;  // error: not unifiable
+  assert y == z;  // error: not unifiable
+  assert x == z;  // error: not unifiable
+}
+
+procedure Nuther()
+{
+  var x: <a,b>[a,a,b]int;
+  var y: <a,b>[a,b,b]int;
+  assert x == y;  // error: not unifiable
+}
+
+type NagainCtor a;
+procedure Nagain()
+  requires (forall<a,b> x: a, y: b :: x == y);
+  ensures (forall<a,b> x: a, y: Field b, z: NagainCtor b :: x == y && x == z);
+  ensures (forall<b> y: Field b, z: NagainCtor b :: y == z);  // error: types not unifiable
+{
+}
diff --git a/Test/test20/PolyPolyPoly.bpl b/Test/test20/PolyPolyPoly.bpl
new file mode 100644
index 00000000..8666d1fc
--- /dev/null
+++ b/Test/test20/PolyPolyPoly.bpl
@@ -0,0 +1,22 @@
+
+type C _;
+
+const p: <a>[]a;
+const q: <a>[a, a]a;
+const r: <a>[](C a);
+
+const x: C int;
+const y: C bool;
+
+axiom (p[][:= 5][:= true] == p);
+axiom (p[][:= 5][:= true] == r);               // error
+axiom (p[][:= x][:= y] == p);
+axiom (p[][:= x][:= y] == r);
+axiom (p[][:= x][:= 5] == r);                  // error
+axiom (p[][:= x][:= y] == p[][:= 5][:= true]);
+axiom (q[p[][:= x][:= y], p[][:= 5][:= true]] == p);
+axiom (q[p[], p[]][:= 5][:= true] == p);
+
+axiom (exists<a> x:a :: p[][:= 5][:= true] == x);
+axiom (exists<a,b> x:a, y:b :: p[][:= 5][:= true] == q[x,y]);  // error
+axiom (exists<a,b> x:a, y:b :: q[x, x] == q[y, y]);
diff --git a/Test/test20/PolyPolyPoly2.bpl b/Test/test20/PolyPolyPoly2.bpl
new file mode 100644
index 00000000..b07c565a
--- /dev/null
+++ b/Test/test20/PolyPolyPoly2.bpl
@@ -0,0 +1,34 @@
+
+const p: <a>[]a;
+const q: <a,b>[a]b;
+
+axiom (p[] == p[]);               // warning
+axiom (p[][13 := false] == q);
+axiom (p[][13 := false] == p[]);  // warning
+
+const c: bv17;
+
+axiom (p[] ++ p[] ++ c == p[]);   // warning
+axiom (p[] ++ p[] == c);          // warning
+axiom (p[] == c);
+
+type List _;
+
+function emptyList<a>() returns (List a);
+function append<a>(List a, List a) returns (List a);
+
+axiom (forall<a> l:List a :: append(emptyList(), l) == l);
+axiom (forall<a> l:List a :: append(l, emptyList()) == l);
+axiom (append(emptyList(), emptyList()) == emptyList());   // warning
+axiom (forall<a> l:List a :: l==emptyList() ==> append(l, emptyList()) == emptyList());
+
+var x: <a>[]a;
+var y: <a>[a]a;
+
+procedure P() returns () modifies x, y; {
+  x[] := 15;
+  x[] := false;
+  x[] := p[];       // warning
+  x[] := q[false];  // warning
+  y[13] := q[false];
+}
+\ No newline at end of file
diff --git a/Test/test20/PolyProcs0.bpl b/Test/test20/PolyProcs0.bpl
new file mode 100644
index 00000000..609f1167
--- /dev/null
+++ b/Test/test20/PolyProcs0.bpl
@@ -0,0 +1,44 @@
+
+
+type Field a;
+
+function FieldAccessFun<b>(heap : <a>[ref, Field a]a, obj : ref, f : Field b)
+         returns (res:b);
+
+procedure FieldAccess<b>(heap : <a>[ref, Field a]a, obj : ref, f : Field b)
+          returns (res:b) {
+  start:
+    res := heap[f, obj];    // error: wrong argument order
+    res := heap[obj, f];
+    assert res == FieldAccessFun(heap, obj, f);
+    return;
+}
+
+procedure UseHeap(heap : <a>[ref, Field a]a) {
+  var f1 : Field int; var f2 : Field bool; var obj : ref;
+  var x : int; var y : bool;
+
+  call x := FieldAccess(heap, f1, obj);  // error: wrong argument order
+  call x := FieldAccess(heap, obj, f1);
+  call y := FieldAccess(heap, obj, f2);
+
+  call y := FieldAccess(heap, obj, f1);  // error: wrong result type
+  call x := FieldAccess(heap, obj, obj); // error: wrong argument type
+}
+
+procedure injective<b>(heap : <a>[ref, Field a]a, obj0 : ref, obj1 : ref, f : Field b);
+   requires obj0 != obj1;
+   ensures heap[obj0, f] != heap[obj1, f];
+
+procedure testCallForall(heap : <a>[ref, Field a]a) {
+  var f1 : Field int; var f2 : Field bool;
+
+  start:
+    call forall injective(heap, *, *, f1);
+    call forall injective(heap, *, *, f2);
+    call forall injective(heap, *, *, *);
+
+    call forall injective(heap, *, f1, *);  // error: wrong argument type
+}
+
+type ref;
diff --git a/Test/test20/ProcParamReordering.bpl b/Test/test20/ProcParamReordering.bpl
new file mode 100644
index 00000000..404b41a3
--- /dev/null
+++ b/Test/test20/ProcParamReordering.bpl
@@ -0,0 +1,15 @@
+
+type C _;
+
+
+procedure P<a, b>(x : a, y : b) returns ();
+
+implementation P<a, b>(x : a, y : b) returns () {}
+
+implementation P<c, d>(a : c, b : d) returns () {}
+
+implementation P<d, c>(a : c, b : d) returns () {}
+
+implementation P<d, c>(a : c, b : C d) returns () {}
+
+implementation P<a>(x : a, y : a) returns () {}
+\ No newline at end of file
diff --git a/Test/test20/Prog0.bpl b/Test/test20/Prog0.bpl
new file mode 100644
index 00000000..ea71b8a8
--- /dev/null
+++ b/Test/test20/Prog0.bpl
@@ -0,0 +1,35 @@
+// Let's test some Boogie 2 features ...
+type real;
+type elements;
+
+type Field a;
+var heap : <a> [ref, Field a] a;
+
+const emptyset : <a> [a] bool;
+
+function union(<a> [a] bool, <a> [a] bool) returns (<a> [a] bool);
+
+axiom (forall x : <a> [a] bool, y : <a> [a] bool,
+              z : int ::         
+              { union(x, y)[z] } 
+              union(x, y)[z] == (x[z] || y[z]));
+
+var tau : <a> [ref] int;             // error: type variable has to occur in arguments
+
+axiom (forall x : int :: !emptyset[x]);
+
+// the more general version of the axiom that also uses type quantifiers
+
+axiom (forall<alpha>
+              x : <a> [a] bool, y : <a> [a] bool,
+              z : alpha ::         
+              { union(x, y)[z] } 
+              union(x, y)[z] == (x[z] || y[z]));
+
+axiom (forall<beta, alpha, beta> a:alpha, b:beta ::        // error: variable bound twice
+              a == b ==> (exists c:alpha :: c == b));
+
+axiom (forall<beta> a:alpha, b:beta ::                     // error: alpha is not declared
+              a == b ==> (exists c:alpha :: c == b));
+
+type ref;
diff --git a/Test/test20/Prog1.bpl b/Test/test20/Prog1.bpl
new file mode 100644
index 00000000..1d75805c
--- /dev/null
+++ b/Test/test20/Prog1.bpl
@@ -0,0 +1,26 @@
+// Let's test some Boogie 2 features ...
+type real;
+type elements;
+
+type Field a;
+var heap : <a> [ref, Field a] a;
+
+
+
+procedure p (x:int, y:ref, z:<a> [ref, Field a] a) returns (newHeap : <a> [ref, Field a] a) {
+
+  var f : Field int;
+  var g : Field bool;
+
+  var heap : <a> [ref, Field a] a;
+  
+  assert z[y, f] >= 0;
+  assert z[x, f] >= 0;   // error: x has wrong type
+  assert z[y, x] >= 0;   // error: x has wrong type
+  assert z[y, g] >= 0;   // error: result of map select has wrong type
+
+  heap[y, g] := false;
+
+}
+
+type ref;
diff --git a/Test/test20/Prog2.bpl b/Test/test20/Prog2.bpl
new file mode 100644
index 00000000..43b9b28f
--- /dev/null
+++ b/Test/test20/Prog2.bpl
@@ -0,0 +1,16 @@
+function union(<a> [a] bool, <a> [a] bool) returns (<a> [a] bool);
+
+axiom (forall<alpha>             // error: alpha has to occur in dummy types
+              x : <a> [a] bool, y : <a> [a] bool,
+              z : int ::
+              { union(x, y)[z] } 
+              union(x, y)[z] == (x[z] || y[z]));
+
+function poly<a>() returns (a);
+
+axiom (forall<alpha>
+              x : <a> [a] bool, y : <a> [a] bool,
+              z : int ::
+              { union(x, y)[z], poly() : alpha } 
+              union(x, y)[z] == (x[z] || y[z]));
+
diff --git a/Test/test20/TypeDecls0.bpl b/Test/test20/TypeDecls0.bpl
new file mode 100644
index 00000000..898e0d1a
--- /dev/null
+++ b/Test/test20/TypeDecls0.bpl
@@ -0,0 +1,45 @@
+type C a _ b;
+type D;
+type E _;
+
+var A0 : D;
+
+var A1 : C D D D;
+
+var A2 : <a,b> [b, C a b D] C a D [D]a;
+
+var A3 : <a,b> [b, C a int D] C bool ref [bv32]a;
+
+var A4 : <a,a> [a] a;            // error: a bound twice
+var A5 : <a> [a] <a> [a] int;    // error: a bound twice
+
+var A6 : <a> [a] <b> [b] int;
+
+var A7 : <a> [a] <b> [int] int;  // error: b does not occur as map argument
+
+type C _ _;                      // error: C is already declared
+
+var A8 : C int ref;              // error: wrong number of arguments
+
+var A9 : A0;                     // error: undeclared type
+var A10: F int;                  // error: undeclared type
+
+var A11: E D;
+var A12: E E D;                  // error: wrong number of arguments
+var A13: E (E D);
+var A14: E E E D;                // error: wrong number of arguments
+
+var A15: E E int;                // error: wrong number of arguments
+var A16: E (E int);
+
+var A17: bv64;
+var A18: [int] bv64;
+
+var A19: C E E D;                // error: wrong number of arguments
+var A20: C (E (E D)) int [int] int;
+var A21: C (<a> [a] <b> [b] int) int [int] int;
+
+var A22: (D);
+var A23: ((D));
+
+type ref;
diff --git a/Test/test20/TypeDecls1.bpl b/Test/test20/TypeDecls1.bpl
new file mode 100644
index 00000000..02c5536a
--- /dev/null
+++ b/Test/test20/TypeDecls1.bpl
@@ -0,0 +1,23 @@
+
+// set of maps from anything to a specific type a
+const mapSet : <a>[<b>[b]a]bool;
+
+const emptySet : <a>[a]bool;
+
+axiom mapSet[5];                            // type error
+
+axiom mapSet[emptySet] == true;
+
+axiom mapSet[emptySet := false] != mapSet;
+
+axiom mapSet[emptySet := 5] == mapSet;      // type error
+
+axiom emptySet[13 := true][13] == true;
+
+axiom (forall f : <c>[c]int, x : ref :: mapSet[f] ==> f[x] >= 0);
+
+axiom (forall f : <c>[c]c :: mapSet[f]);    // type error
+
+axiom mapSet[mapSet] == true;               // type error
+
+type ref;
diff --git a/Test/test20/TypeSynonyms0.bpl b/Test/test20/TypeSynonyms0.bpl
new file mode 100644
index 00000000..d161b5df
--- /dev/null
+++ b/Test/test20/TypeSynonyms0.bpl
@@ -0,0 +1,29 @@
+
+
+type Set a = [a]bool;
+
+type Field a, Heap = <a>[ref, Field a]a;
+
+type notAllParams a b = Field b;
+
+type Cyclic0 = Cyclic1;
+type Cyclic1 = Cyclic0;
+
+type AlsoCyclic a = <b>[AlsoCyclic b]int;
+
+type C a b;
+
+type C2 b a = C a b;
+
+function f(C int bool) returns (int);
+const x : C2 bool int;
+
+
+const y : Field int bool;       // wrong number of arguments
+const z : Set int bool;         // wrong number of arguments
+
+
+const d : <a,b>[notAllParams a b]int;         // error: not all parameters are used
+
+
+type ref;
diff --git a/Test/test20/TypeSynonyms1.bpl b/Test/test20/TypeSynonyms1.bpl
new file mode 100644
index 00000000..45b7e46d
--- /dev/null
+++ b/Test/test20/TypeSynonyms1.bpl
@@ -0,0 +1,47 @@
+
+
+
+type C a b;
+type C2 b a = C a b;
+
+
+// ordering of map type parameters
+function g0(<a,b>[C2 a b]int) returns (int);
+function g1(<a,b>[C2 b a]int) returns (int);
+function g2(<a,b>[C a b]int) returns (int);
+function g3(<a,b>[C b a]int) returns (int);
+
+const c0 : <a,b>[C2 a b]int;
+const c1 : <a,b>[C2 b a]int;
+const c2 : <a,b>[C a b]int;
+const c3 : <a,b>[C b a]int;
+
+axiom g0(c0) == 0;
+axiom g1(c0) == 0;
+axiom g2(c0) == 0;
+axiom g3(c0) == 0;
+axiom g0(c1) == 0;
+axiom g1(c1) == 0;
+axiom g2(c1) == 0;
+axiom g3(c1) == 0;
+axiom g0(c2) == 0;
+axiom g1(c2) == 0;
+axiom g2(c2) == 0;
+axiom g3(c2) == 0;
+axiom g0(c3) == 0;
+axiom g1(c3) == 0;
+axiom g2(c3) == 0;
+axiom g3(c3) == 0;
+
+
+type nested a = <b>[b, b, a]int;
+type nested2 = nested (nested int);
+
+
+function h(nested2) returns (bool);
+const e : <b>[b, b, <b2>[b2, b2, int]int]int;
+axiom h(e);
+
+const e2 : <b>[b, b, <b2>[b2, b, int]int]int;      // wrong binding
+axiom h(e2);
+
diff --git a/Test/test20/TypeSynonyms2.bpl b/Test/test20/TypeSynonyms2.bpl
new file mode 100644
index 00000000..f6fee1f3
--- /dev/null
+++ b/Test/test20/TypeSynonyms2.bpl
@@ -0,0 +1,20 @@
+
+
+type Set a = [a]bool;
+
+function union<a>(x : Set a, y : Set a) returns (Set a);
+axiom (forall<a> x : Set a, y : Set a, z : a :: (x[z] || y[z]) == union(x, y)[z]);
+
+
+const intSet0 : Set int;
+axiom (forall x:int :: intSet0[x] == (x == 0 || x == 2 || x == 3));
+
+const intSet1 : Set int;
+axiom (forall x:int :: intSet1[x] == (x == -5 || x == 3));
+
+
+procedure P() returns () {
+  assert (forall x:int :: union(intSet0, intSet1)[x] ==
+                                     (x == -5 || x == 0 || x == 2 || x == 3));
+}
+
diff --git a/Test/test20/runtest.bat b/Test/test20/runtest.bat
new file mode 100644
index 00000000..0e607a1f
--- /dev/null
+++ b/Test/test20/runtest.bat
@@ -0,0 +1,26 @@
+@echo off
+setlocal
+
+set BGEXE=..\..\Binaries\Boogie.exe
+rem set BGEXE=mono ..\..\Binaries\Boogie.exe
+
+%BGEXE% %* /noVerify TypeDecls0.bpl
+%BGEXE% %* /noVerify TypeDecls1.bpl
+%BGEXE% %* /noVerify Prog0.bpl
+%BGEXE% %* /noVerify Prog1.bpl
+%BGEXE% %* /noVerify Prog2.bpl
+%BGEXE% %* /noVerify PolyFuns0.bpl
+%BGEXE% %* /noVerify PolyFuns1.bpl
+%BGEXE% %* /noVerify PolyProcs0.bpl
+%BGEXE% %* /noVerify TypeSynonyms0.bpl
+%BGEXE% %* /noVerify TypeSynonyms1.bpl
+%BGEXE% %* TypeSynonyms2.bpl
+%BGEXE% %* /noVerify /print:- /env:0 TypeSynonyms0.bpl
+%BGEXE% %* /noVerify /print:- /env:0 /printDesugared TypeSynonyms2.bpl
+%BGEXE% %* /noVerify PolyPolyPoly.bpl
+%BGEXE% %* /noVerify PolyPolyPoly2.bpl
+%BGEXE% %* /noVerify ProcParamReordering.bpl
+%BGEXE% %* /noVerify ParallelAssignment.bpl
+%BGEXE% %* /noVerify ParallelAssignment2.bpl
+%BGEXE% %* /noVerify Coercions.bpl
+%BGEXE% %* /noVerify EmptySeq.bpl
author	mikebarnett <unknown>	2009-07-15 21:03:41 +0000
committer	mikebarnett <unknown>	2009-07-15 21:03:41 +0000
commit	ce1c2de044c91624370411e23acab13b0381949b (patch)
tree	592539996fe08050ead5ee210c973801611dde40 /Test/test20