1 files changed, 72 insertions, 72 deletions
diff --git a/Test/aitest9/TestIntervals.bpl b/Test/aitest9/TestIntervals.bpl
index 307a1da4..c9bb8284 100644
--- a/Test/aitest9/TestIntervals.bpl
+++ b/Test/aitest9/TestIntervals.bpl
@@ -1,72 +1,72 @@
-// RUN: %boogie "%s" -infer:j > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure P()
-{
-  var a: int, b: int, c: int;
-
-  a := 0;
-  while (*) {
-    a := a + 1;
-  }
-  // a in [0, infty]
-
-  b := 0;
-  if (*) { b := b + 1; }
-  if (*) { b := b + 1; }
-  if (*) { b := b + 1; }
-  // b in [0, 3]
-
-  c := a - b;
-  // c in [-3, infty]
-  goto Next;
-
-  Next:
-  assert -3 <= c;
-  assert c <= 0;  // error (there was once an error in the Intervals which thought this assertion to be true)
-}
-
-// The following tests a triply nested array, where the innermost array is a polymorphic map.
-// There was once an error in Boogie's handling of such things in the AI code.
-
-type ref;
-type teflon;
-
-type Field a;
-type HeapType = <a>[Field a]a;
-var Heap: HeapType;
-
-procedure Q(myField: Field [ref][teflon]bool, r: ref, t: teflon)
-  modifies Heap;
-{
-  Heap[myField][r][t] := true;
-}
-
-// -----
-
-procedure Neq()
-{
-  var n: int;
-  assume 2 <= n && n <= 10;
-  assume 2 != n;
-  assume n != 10;
-  while (*) {
-    n := n;
-  }
-  assert 3 <= n;
-  assert n < 10;
-}
-
-procedure NeqX()
-{
-  var n: real;
-  assume 2.0 <= n && n <= 10.0;
-  assume 2.0 != n;
-  assume n != 10.0;
-  // The following statement will cause Boogie to know about n only
-  // what the abstract interpreter has inferred so far.
-  while (*) { n := n; }
-
-  assert 2.0 <= n && n <= 10.0;  // yes
-  assert 2.0 < n;  // error, the abstract domain is not precise enough to figure this out
-  assert n < 10.0;  // error, ditto
-}
+// RUN: %boogie "%s" -infer:j > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure P()
+{
+  var a: int, b: int, c: int;
+
+  a := 0;
+  while (*) {
+    a := a + 1;
+  }
+  // a in [0, infty]
+
+  b := 0;
+  if (*) { b := b + 1; }
+  if (*) { b := b + 1; }
+  if (*) { b := b + 1; }
+  // b in [0, 3]
+
+  c := a - b;
+  // c in [-3, infty]
+  goto Next;
+
+  Next:
+  assert -3 <= c;
+  assert c <= 0;  // error (there was once an error in the Intervals which thought this assertion to be true)
+}
+
+// The following tests a triply nested array, where the innermost array is a polymorphic map.
+// There was once an error in Boogie's handling of such things in the AI code.
+
+type ref;
+type teflon;
+
+type Field a;
+type HeapType = <a>[Field a]a;
+var Heap: HeapType;
+
+procedure Q(myField: Field [ref][teflon]bool, r: ref, t: teflon)
+  modifies Heap;
+{
+  Heap[myField][r][t] := true;
+}
+
+// -----
+
+procedure Neq()
+{
+  var n: int;
+  assume 2 <= n && n <= 10;
+  assume 2 != n;
+  assume n != 10;
+  while (*) {
+    n := n;
+  }
+  assert 3 <= n;
+  assert n < 10;
+}
+
+procedure NeqX()
+{
+  var n: real;
+  assume 2.0 <= n && n <= 10.0;
+  assume 2.0 != n;
+  assume n != 10.0;
+  // The following statement will cause Boogie to know about n only
+  // what the abstract interpreter has inferred so far.
+  while (*) { n := n; }
+
+  assert 2.0 <= n && n <= 10.0;  // yes
+  assert 2.0 < n;  // error, the abstract domain is not precise enough to figure this out
+  assert n < 10.0;  // error, ditto
+}