From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001
From: Checkmate50 <dgeisler50@gmail.com>
Date: Mon, 6 Jun 2016 23:14:18 -0600
Subject: Merging complete.  Everything looks good *crosses fingers*

---
 Test/aitest1/Linear9.bpl | 62 ++++++++++++++++++++++++------------------------
 1 file changed, 31 insertions(+), 31 deletions(-)

(limited to 'Test/aitest1/Linear9.bpl')

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;
+}
-- 
cgit v1.2.3