18 files changed, 552 insertions, 552 deletions
diff --git a/Test/test20/Coercions.bpl b/Test/test20/Coercions.bpl
index 0ad114a6..5487f33a 100644
--- a/Test/test20/Coercions.bpl
+++ b/Test/test20/Coercions.bpl
@@ -1,19 +1,19 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-
-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);
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+
+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
index 2eeb9589..b1758acc 100644
--- a/Test/test20/EmptySeq.bpl
+++ b/Test/test20/EmptySeq.bpl
@@ -1,8 +1,8 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-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);
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+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/ParallelAssignment.bpl b/Test/test20/ParallelAssignment.bpl
index d84b96ab..677bb476 100644
--- a/Test/test20/ParallelAssignment.bpl
+++ b/Test/test20/ParallelAssignment.bpl
@@ -1,25 +1,25 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// 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;
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// 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
index 8f309b75..df9e5655 100644
--- a/Test/test20/ParallelAssignment2.bpl
+++ b/Test/test20/ParallelAssignment2.bpl
@@ -1,13 +1,13 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// 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
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// 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
index c7d44b9f..b1a4a017 100644
--- a/Test/test20/PolyFuns0.bpl
+++ b/Test/test20/PolyFuns0.bpl
@@ -1,57 +1,57 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-
-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;
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+
+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
index 12a8a1b8..01d6638c 100644
--- a/Test/test20/PolyFuns1.bpl
+++ b/Test/test20/PolyFuns1.bpl
@@ -1,61 +1,61 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-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
-{
-}
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+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
index 718452f2..1b2f8823 100644
--- a/Test/test20/PolyPolyPoly.bpl
+++ b/Test/test20/PolyPolyPoly.bpl
@@ -1,24 +1,24 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-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]);
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+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
index e50251c1..cf4df9c3 100644
--- a/Test/test20/PolyPolyPoly2.bpl
+++ b/Test/test20/PolyPolyPoly2.bpl
@@ -1,36 +1,36 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-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];
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+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
index 698e2f12..cc0ba491 100644
--- a/Test/test20/PolyProcs0.bpl
+++ b/Test/test20/PolyProcs0.bpl
@@ -1,35 +1,35 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-
-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];
-
-type ref;
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+
+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];
+
+type ref;
diff --git a/Test/test20/ProcParamReordering.bpl b/Test/test20/ProcParamReordering.bpl
index 2532964f..225eed33 100644
--- a/Test/test20/ProcParamReordering.bpl
+++ b/Test/test20/ProcParamReordering.bpl
@@ -1,17 +1,17 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-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 () {}
-
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+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
index 26642737..512984dc 100644
--- a/Test/test20/Prog0.bpl
+++ b/Test/test20/Prog0.bpl
@@ -1,37 +1,37 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// Let's test some Boogie 2 features ...
-
-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;
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// Let's test some Boogie 2 features ...
+
+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
index 7fcf91b6..1c26db31 100644
--- a/Test/test20/Prog1.bpl
+++ b/Test/test20/Prog1.bpl
@@ -1,28 +1,28 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// Let's test some Boogie 2 features ...
-
-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;
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// Let's test some Boogie 2 features ...
+
+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
index 79555d28..67d9396e 100644
--- a/Test/test20/Prog2.bpl
+++ b/Test/test20/Prog2.bpl
@@ -1,18 +1,18 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-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]));
-
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+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
index a78008c2..42b988d8 100644
--- a/Test/test20/TypeDecls0.bpl
+++ b/Test/test20/TypeDecls0.bpl
@@ -1,47 +1,47 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-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;
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+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
index 52f28e06..a4fa7de6 100644
--- a/Test/test20/TypeDecls1.bpl
+++ b/Test/test20/TypeDecls1.bpl
@@ -1,25 +1,25 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-// 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;
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// 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
index 1703f4a7..261b94cf 100644
--- a/Test/test20/TypeSynonyms0.bpl
+++ b/Test/test20/TypeSynonyms0.bpl
@@ -1,33 +1,33 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// RUN: %boogie -noVerify -print:- -env:0 "%s" > "%t"
-// RUN: %diff "%s.print.expect" "%t"
-
-
-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;
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// RUN: %boogie -noVerify -print:- -env:0 "%s" > "%t"
+// RUN: %diff "%s.print.expect" "%t"
+
+
+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
index 98ecedca..9f61335c 100644
--- a/Test/test20/TypeSynonyms1.bpl
+++ b/Test/test20/TypeSynonyms1.bpl
@@ -1,49 +1,49 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-
-
-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);
-
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+
+
+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
index 1cb6e781..87a7451f 100644
--- a/Test/test20/TypeSynonyms2.bpl
+++ b/Test/test20/TypeSynonyms2.bpl
@@ -1,24 +1,24 @@
-// RUN: %boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// RUN: %boogie -noVerify -print:- -pretty:0 -env:0 -printDesugared "%s" > "%t"
-// RUN: %diff "%s.print.expect" "%t"
-
-
-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));
-}
-
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// RUN: %boogie -noVerify -print:- -pretty:0 -env:0 -printDesugared "%s" > "%t"
+// RUN: %diff "%s.print.expect" "%t"
+
+
+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));
+}
+