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/inline/test4.bpl | 108 +++++++++++++++++++++++++-------------------------
 1 file changed, 54 insertions(+), 54 deletions(-)

(limited to 'Test/inline/test4.bpl')

diff --git a/Test/inline/test4.bpl b/Test/inline/test4.bpl
index 7743c498..2a646b58 100644
--- a/Test/inline/test4.bpl
+++ b/Test/inline/test4.bpl
@@ -1,55 +1,55 @@
-// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-procedure main(x:int)
-{
-	var A:[int]int;
-	var i:int;
-	var b:bool;
-	var size:int;
-	
-	call i,b := find(A, size, x);
-
-	if(b) {
-		assert(i > 0 && A[i] == x);
-	}
-
-	return;
-}
-
-procedure {:inline 1} find(A:[int]int, size:int, x:int) returns (ret:int, found:bool)
-{
-	var i:int;
-	var b:bool;
-
-	ret := -1;
-	b := false;
-	found := b;
-	i := 0;
-
-	while(i < size) {
-		call b := check(A, i, x);
-		if(b) {
-		      ret := i;
-		      found := b;
-		      break;
-		}
-	
-	}
-
-	return;
-
-}
-
-
-procedure {:inline 3} check (A:[int]int, i:int, c:int) returns (ret:bool)
-	  requires i >= 0;
-	  ensures (old(A[i]) > c) ==> ret == true;
-{
-	if(A[i] == c) {
-		ret := true;
-	} else {
-	       ret := false;
-	}
-	return;
+// RUN: %boogie -inline:spec -print:- -env:0 -printInlined -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+procedure main(x:int)
+{
+	var A:[int]int;
+	var i:int;
+	var b:bool;
+	var size:int;
+	
+	call i,b := find(A, size, x);
+
+	if(b) {
+		assert(i > 0 && A[i] == x);
+	}
+
+	return;
+}
+
+procedure {:inline 1} find(A:[int]int, size:int, x:int) returns (ret:int, found:bool)
+{
+	var i:int;
+	var b:bool;
+
+	ret := -1;
+	b := false;
+	found := b;
+	i := 0;
+
+	while(i < size) {
+		call b := check(A, i, x);
+		if(b) {
+		      ret := i;
+		      found := b;
+		      break;
+		}
+	
+	}
+
+	return;
+
+}
+
+
+procedure {:inline 3} check (A:[int]int, i:int, c:int) returns (ret:bool)
+	  requires i >= 0;
+	  ensures (old(A[i]) > c) ==> ret == true;
+{
+	if(A[i] == c) {
+		ret := true;
+	} else {
+	       ret := false;
+	}
+	return;
 }
\ No newline at end of file
-- 
cgit v1.2.3