2 files changed, 132 insertions, 132 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
+}
diff --git a/Test/aitest9/VarMapFixpoint.bpl b/Test/aitest9/VarMapFixpoint.bpl
index 6a051ed9..83ea45ca 100644
--- a/Test/aitest9/VarMapFixpoint.bpl
+++ b/Test/aitest9/VarMapFixpoint.bpl
@@ -1,60 +1,60 @@
-// RUN: %boogie "%s" -infer:j > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure main()
-{
-  var x: int, y: int, z: int;
-
-  start:
-    x := 2;
-    y := 6;
-    goto LoopHead;
-
-  LoopHead:
-    assert y < 10;  // error: the loop body sets y to an arbitrary value
-    goto LoopBody, LoopEnd;
-
-  LoopBody:
-    havoc y;
-    goto LoopHead;
-
-  LoopEnd:
-    return;
-}
-
-procedure SimpleWhile5() returns (returnValue: int)
-{
-  var i: int;
-
-  start:
-    returnValue := 1;
-    havoc i;
-    goto LoopHead;
-
-  LoopHead:
-    goto LoopBody, LoopEnd;
-
-  LoopBody:
-    // here, we would simply like to "assume 1 <= i", but the interval domain doesn't interpret
-    // assume commands, so we start a loop
-    i := 1;
-    goto IncLoopHead;
-
-  IncLoopHead:
-    goto IncI, IncDone;
-
-  IncI:
-    i := i + 1;
-    goto IncLoopHead;
-
-  IncDone:
-    // now we have 1 <= i
-    assert 1 <= i;
-
-    returnValue := returnValue * i;
-    i := i - 1;
-    goto LoopHead;
-
-  LoopEnd:
-    assert returnValue >= 1;
-    return;
-}
+// RUN: %boogie "%s" -infer:j > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure main()
+{
+  var x: int, y: int, z: int;
+
+  start:
+    x := 2;
+    y := 6;
+    goto LoopHead;
+
+  LoopHead:
+    assert y < 10;  // error: the loop body sets y to an arbitrary value
+    goto LoopBody, LoopEnd;
+
+  LoopBody:
+    havoc y;
+    goto LoopHead;
+
+  LoopEnd:
+    return;
+}
+
+procedure SimpleWhile5() returns (returnValue: int)
+{
+  var i: int;
+
+  start:
+    returnValue := 1;
+    havoc i;
+    goto LoopHead;
+
+  LoopHead:
+    goto LoopBody, LoopEnd;
+
+  LoopBody:
+    // here, we would simply like to "assume 1 <= i", but the interval domain doesn't interpret
+    // assume commands, so we start a loop
+    i := 1;
+    goto IncLoopHead;
+
+  IncLoopHead:
+    goto IncI, IncDone;
+
+  IncI:
+    i := i + 1;
+    goto IncLoopHead;
+
+  IncDone:
+    // now we have 1 <= i
+    assert 1 <= i;
+
+    returnValue := returnValue * i;
+    i := i - 1;
+    goto LoopHead;
+
+  LoopEnd:
+    assert returnValue >= 1;
+    return;
+}