1 files changed, 33 insertions, 33 deletions
diff --git a/Test/test21/InterestingExamples3.bpl b/Test/test21/InterestingExamples3.bpl
index 24e89b2b..4990fb72 100644
--- a/Test/test21/InterestingExamples3.bpl
+++ b/Test/test21/InterestingExamples3.bpl
@@ -1,33 +1,33 @@
-// 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 () {
-
- assume (forall<t> m : [t]bool ::                // uses "infinitely many" map types
-         (forall x : t ::    m[x] == false));
-
-}
-
-
-procedure Q() returns () {
- var h : [int] bool;
-
- assume (forall<t> m : [t]bool, x : t ::    m[x] == false);
- assert !h[42];
- assert false;                    // should really be provable
-}
-
-
-
-procedure R() returns () {
- var h : [int] bool;
-
- assume (forall<t> m : [t]bool, x : t ::    m[x] == false);
- assert !h[42];
- assert !h[42 := true][42];
- assert false;                    // wow
-}
+// 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 () {
+
+ assume (forall<t> m : [t]bool ::                // uses "infinitely many" map types
+         (forall x : t ::    m[x] == false));
+
+}
+
+
+procedure Q() returns () {
+ var h : [int] bool;
+
+ assume (forall<t> m : [t]bool, x : t ::    m[x] == false);
+ assert !h[42];
+ assert false;                    // should really be provable
+}
+
+
+
+procedure R() returns () {
+ var h : [int] bool;
+
+ assume (forall<t> m : [t]bool, x : t ::    m[x] == false);
+ assert !h[42];
+ assert !h[42 := true][42];
+ assert false;                    // wow
+}