12 files changed, 327 insertions, 327 deletions
diff --git a/Test/aitest1/Bound.bpl b/Test/aitest1/Bound.bpl
index 81b3635f..f2dd2547 100644
--- a/Test/aitest1/Bound.bpl
+++ b/Test/aitest1/Bound.bpl
@@ -1,30 +1,30 @@
-// RUN: %boogie -infer:j "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-const TEST: name;
-
-procedure P()
-{
-var i: int;
-var N: int;
-
-start:
-  assume N >= 0;
-  i := 0;
-  assert i <= N;
-  goto LoopHead;
-
-LoopHead:
-  goto LoopBody, AfterLoop;
-
-LoopBody:
-  assume i < N;
-  i := i + 1;
-  goto LoopHead;
-
-AfterLoop:
-  assume !(i < N);
-  assert i == N;
-  return;
-}
-
-type name;
+// RUN: %boogie -infer:j "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+const TEST: name;
+
+procedure P()
+{
+var i: int;
+var N: int;
+
+start:
+  assume N >= 0;
+  i := 0;
+  assert i <= N;
+  goto LoopHead;
+
+LoopHead:
+  goto LoopBody, AfterLoop;
+
+LoopBody:
+  assume i < N;
+  i := i + 1;
+  goto LoopHead;
+
+AfterLoop:
+  assume !(i < N);
+  assert i == N;
+  return;
+}
+
+type name;
diff --git a/Test/aitest1/Linear0.bpl b/Test/aitest1/Linear0.bpl
index 7e55fb12..f8e2c15a 100644
--- a/Test/aitest1/Linear0.bpl
+++ b/Test/aitest1/Linear0.bpl
@@ -1,12 +1,12 @@
-// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// Simple test file for checking the inference of linear constraints.
-
-var x: int;
-var y: int;
-
-procedure p()
-{
-  start:
-    return;
-}
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// Simple test file for checking the inference of linear constraints.
+
+var x: int;
+var y: int;
+
+procedure p()
+{
+  start:
+    return;
+}
diff --git a/Test/aitest1/Linear1.bpl b/Test/aitest1/Linear1.bpl
index 855dacae..452ebc43 100644
--- a/Test/aitest1/Linear1.bpl
+++ b/Test/aitest1/Linear1.bpl
@@ -1,13 +1,13 @@
-// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// Simple test file for checking the inference of linear constraints.
-
-var x: int;
-var y: int;
-
-procedure p()
-{
-  start:
-    assume x*x == y;  // not a linear condition
-    return;
-}
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// Simple test file for checking the inference of linear constraints.
+
+var x: int;
+var y: int;
+
+procedure p()
+{
+  start:
+    assume x*x == y;  // not a linear condition
+    return;
+}
diff --git a/Test/aitest1/Linear2.bpl b/Test/aitest1/Linear2.bpl
index fa743278..6b8684c5 100644
--- a/Test/aitest1/Linear2.bpl
+++ b/Test/aitest1/Linear2.bpl
@@ -1,13 +1,13 @@
-// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// Simple test file for checking the inference of linear constraints.
-
-var x: int;
-var y: int;
-
-procedure p()
-{
-  start:
-    assume x == 8;
-    return;
-}
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// Simple test file for checking the inference of linear constraints.
+
+var x: int;
+var y: int;
+
+procedure p()
+{
+  start:
+    assume x == 8;
+    return;
+}
diff --git a/Test/aitest1/Linear3.bpl b/Test/aitest1/Linear3.bpl
index a71214fc..19bccde9 100644
--- a/Test/aitest1/Linear3.bpl
+++ b/Test/aitest1/Linear3.bpl
@@ -1,13 +1,13 @@
-// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// Simple test file for checking the inference of linear constraints.
-
-var x: int;
-var y: int;
-
-procedure p()
-{
-  start:
-    assume x < y;
-    return;
-}
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// Simple test file for checking the inference of linear constraints.
+
+var x: int;
+var y: int;
+
+procedure p()
+{
+  start:
+    assume x < y;
+    return;
+}
diff --git a/Test/aitest1/Linear4.bpl b/Test/aitest1/Linear4.bpl
index 6cd4a947..2dd17d05 100644
--- a/Test/aitest1/Linear4.bpl
+++ b/Test/aitest1/Linear4.bpl
@@ -1,19 +1,19 @@
-// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// Simple test file for checking the inference of linear constraints.
-
-var x: int;
-var y: int;
-
-procedure p()
-  modifies x;
-{
-  A:
-    assume x < y;
-    goto B, C;
-  B:
-    x := x*x;
-    return;
-  C:
-    return;
-}
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// Simple test file for checking the inference of linear constraints.
+
+var x: int;
+var y: int;
+
+procedure p()
+  modifies x;
+{
+  A:
+    assume x < y;
+    goto B, C;
+  B:
+    x := x*x;
+    return;
+  C:
+    return;
+}
diff --git a/Test/aitest1/Linear5.bpl b/Test/aitest1/Linear5.bpl
index fdd961c3..693dc3cf 100644
--- a/Test/aitest1/Linear5.bpl
+++ b/Test/aitest1/Linear5.bpl
@@ -1,25 +1,25 @@
-// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// Simple test file for checking the inference of linear constraints.
-
-var x: int;
-var y: int;
-
-procedure p()
-  modifies x;
-{
-  A:
-    assume -1 <= x;
-    goto B, E;
-  B:
-    assume x < y;
-    goto C, E;
-  C:
-    x := x*x;
-    goto D, E;
-  D:
-    x := y;
-    return;
-  E:
-    return;
-}
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// Simple test file for checking the inference of linear constraints.
+
+var x: int;
+var y: int;
+
+procedure p()
+  modifies x;
+{
+  A:
+    assume -1 <= x;
+    goto B, E;
+  B:
+    assume x < y;
+    goto C, E;
+  C:
+    x := x*x;
+    goto D, E;
+  D:
+    x := y;
+    return;
+  E:
+    return;
+}
diff --git a/Test/aitest1/Linear6.bpl b/Test/aitest1/Linear6.bpl
index a6747114..aa0623ba 100644
--- a/Test/aitest1/Linear6.bpl
+++ b/Test/aitest1/Linear6.bpl
@@ -1,23 +1,23 @@
-// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// Simple test file for checking the inference of linear constraints.
-
-var x: int;
-var y: int;
-var z: int;
-
-procedure p()
-  modifies x;
-{
-A:
-    x := 8;
-    goto B, C;
-B:
-    x := 9;
-    goto D;
-C:
-    x := 10;
-    goto D;
-D:
-    return;
-}
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// Simple test file for checking the inference of linear constraints.
+
+var x: int;
+var y: int;
+var z: int;
+
+procedure p()
+  modifies x;
+{
+A:
+    x := 8;
+    goto B, C;
+B:
+    x := 9;
+    goto D;
+C:
+    x := 10;
+    goto D;
+D:
+    return;
+}
diff --git a/Test/aitest1/Linear7.bpl b/Test/aitest1/Linear7.bpl
index 45ef3e79..37bb442f 100644
--- a/Test/aitest1/Linear7.bpl
+++ b/Test/aitest1/Linear7.bpl
@@ -1,21 +1,21 @@
-// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// Simple test file for checking the inference of linear constraints.
-
-var x: int;
-var y: int;
-var z: int;
-
-procedure p()
-{
-A:
-    goto B, C;
-B:
-    assume x <= 0;
-    goto D;
-C:
-    assume y <= 0;
-    goto D;
-D:
-    return;
-}
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// Simple test file for checking the inference of linear constraints.
+
+var x: int;
+var y: int;
+var z: int;
+
+procedure p()
+{
+A:
+    goto B, C;
+B:
+    assume x <= 0;
+    goto D;
+C:
+    assume y <= 0;
+    goto D;
+D:
+    return;
+}
diff --git a/Test/aitest1/Linear8.bpl b/Test/aitest1/Linear8.bpl
index cb86b72f..1b13423d 100644
--- a/Test/aitest1/Linear8.bpl
+++ b/Test/aitest1/Linear8.bpl
@@ -1,44 +1,44 @@
-// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-procedure foo () returns ()
-{
-  var i: int;
-  var j: int;
-  var n: int;
-
-A:  // true
-  n := 0;
-  goto B;
-
-B:  // n = 0
-  j := 0;
-  goto C;
-
-C:  // n = 0 AND j = 0
-  i := j + 1;
-  goto D;
-
-D:  // n = 0 AND j = 0 AND i = j + 1
-  i := i + 1;
-  goto E;
-
-E:  // n = 0 AND j = 0 AND i = j + 2
-  i := i + 1;
-  goto F;
-
-F:  // n = 0 AND j = 0 AND i = j + 3
-  i := i + 1;
-  goto G;
-
-G:  // n = 0 AND j = 0 AND i = j + 4
-  i := i + 1;
-  goto H;
-
-H:  // n = 0 AND j = 0 AND i = j + 1
-  j := j + 1;
-  goto I;
-
-I:  // n = 0 AND j = 1 AND i = j + 4
-  return;
-}
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure foo () returns ()
+{
+  var i: int;
+  var j: int;
+  var n: int;
+
+A:  // true
+  n := 0;
+  goto B;
+
+B:  // n = 0
+  j := 0;
+  goto C;
+
+C:  // n = 0 AND j = 0
+  i := j + 1;
+  goto D;
+
+D:  // n = 0 AND j = 0 AND i = j + 1
+  i := i + 1;
+  goto E;
+
+E:  // n = 0 AND j = 0 AND i = j + 2
+  i := i + 1;
+  goto F;
+
+F:  // n = 0 AND j = 0 AND i = j + 3
+  i := i + 1;
+  goto G;
+
+G:  // n = 0 AND j = 0 AND i = j + 4
+  i := i + 1;
+  goto H;
+
+H:  // n = 0 AND j = 0 AND i = j + 1
+  j := j + 1;
+  goto I;
+
+I:  // n = 0 AND j = 1 AND i = j + 4
+  return;
+}
diff --git a/Test/aitest1/Linear9.bpl b/Test/aitest1/Linear9.bpl
index 86687f05..72bf0d8c 100644
--- a/Test/aitest1/Linear9.bpl
+++ b/Test/aitest1/Linear9.bpl
@@ -1,31 +1,31 @@
-// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure foo () returns ()
-{
-  var i: int;
-  var j: int;
-  var n: int;
-entry:
-  assume n >= 4;
-  i := 0;
-  j := i + 1;
-  // n >= 4 AND i = 0 AND j = i+1
-  goto exit, loop0;
-
-loop0:
-  // n >= 4 AND i >= 0 AND j = i+1
-  assume j <= n;
-  goto loop1;
-loop1:
-  // n >= 4 AND i >= 0 AND j = i+1 AND j <= n
-  i := i + 1;
-  goto loop2;
-loop2:
-  j := j + 1;
-  // n >= 4 AND i >= 1 AND j = i+1 AND j <= n+1
-  goto loop0, exit;
-
-exit:
-  // n >= 4 AND i >= 0 AND j = i+1 AND j <= n+1
-  return;
-}
+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure foo () returns ()
+{
+  var i: int;
+  var j: int;
+  var n: int;
+entry:
+  assume n >= 4;
+  i := 0;
+  j := i + 1;
+  // n >= 4 AND i = 0 AND j = i+1
+  goto exit, loop0;
+
+loop0:
+  // n >= 4 AND i >= 0 AND j = i+1
+  assume j <= n;
+  goto loop1;
+loop1:
+  // n >= 4 AND i >= 0 AND j = i+1 AND j <= n
+  i := i + 1;
+  goto loop2;
+loop2:
+  j := j + 1;
+  // n >= 4 AND i >= 1 AND j = i+1 AND j <= n+1
+  goto loop0, exit;
+
+exit:
+  // n >= 4 AND i >= 0 AND j = i+1 AND j <= n+1
+  return;
+}
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;
+}