1 files changed, 37 insertions, 37 deletions
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;