1 files changed, 83 insertions, 83 deletions
diff --git a/Test/aitest1/ineq.bpl b/Test/aitest1/ineq.bpl
index 47f1e4f1..fc6a5847 100644
--- a/Test/aitest1/ineq.bpl
+++ b/Test/aitest1/ineq.bpl
@@ -1,83 +1,83 @@
-// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// Test the polyhedra domain for linear inequalities
-
-
-procedure SimpleLoop ()
-{  
-  var i : int;
-  
-  start:
-    i := 0;
-    goto test;
- 
-  test:
-    goto Then, Else;
-
-  Then:
-    assume i < 10;
-    i := i + 1;
-    goto test;
-
-  Else:
-    assume ! (i < 10);
-    return;
-}    
-
-
-procedure VariableBoundLoop (n : int)
-{  
-  var i : int;
-  
-  start:
-    i := 0;
-    goto test;
- 
-  test:
-    goto Then, Else;
-
-  Then:
-    assume i < n;
-    i := i + 1;
-    goto test;
-
-  Else:
-    assume ! (i < n);
-    return;
-}    
-
-procedure Foo () 
-{
- var i : int;
-
- start:
- i := 3 * i + 1;
- i := 3 * (i + 1);
- i := 1 + 3 * i;
- i := (i + 1) * 3 ;
- return;
-}
-
-procedure FooToo () 
-{
- var i : int;
-
- start:
- i := 5;
- i := 3 * i + 1;
- i := 3 * (i + 1);
- i := 1 + 3 * i;
- i := (i + 1) * 3 ;
- return;
-}
-
-procedure FooTooStepByStep () 
-{
- var i : int;
-
- L0: i := 5; goto L1;
- L1: i := 3 * i + 1; goto L2;
- L2: i := 3 * (i + 1); goto L3;
- L3: i := 1 + 3 * i; goto L4;
- L4: i := (i + 1) * 3; return;
-}
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// Test the polyhedra domain for linear inequalities
+
+
+procedure SimpleLoop ()
+{  
+  var i : int;
+  
+  start:
+    i := 0;
+    goto test;
+ 
+  test:
+    goto Then, Else;
+
+  Then:
+    assume i < 10;
+    i := i + 1;
+    goto test;
+
+  Else:
+    assume ! (i < 10);
+    return;
+}    
+
+
+procedure VariableBoundLoop (n : int)
+{  
+  var i : int;
+  
+  start:
+    i := 0;
+    goto test;
+ 
+  test:
+    goto Then, Else;
+
+  Then:
+    assume i < n;
+    i := i + 1;
+    goto test;
+
+  Else:
+    assume ! (i < n);
+    return;
+}    
+
+procedure Foo () 
+{
+ var i : int;
+
+ start:
+ i := 3 * i + 1;
+ i := 3 * (i + 1);
+ i := 1 + 3 * i;
+ i := (i + 1) * 3 ;
+ return;
+}
+
+procedure FooToo () 
+{
+ var i : int;
+
+ start:
+ i := 5;
+ i := 3 * i + 1;
+ i := 3 * (i + 1);
+ i := 1 + 3 * i;
+ i := (i + 1) * 3 ;
+ return;
+}
+
+procedure FooTooStepByStep () 
+{
+ var i : int;
+
+ L0: i := 5; goto L1;
+ L1: i := 3 * i + 1; goto L2;
+ L2: i := 3 * (i + 1); goto L3;
+ L3: i := 1 + 3 * i; goto L4;
+ L4: i := (i + 1) * 3; return;
+}