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/textbook/Find.bpl | 80 +++++++++++++++++++++++++-------------------------
 1 file changed, 40 insertions(+), 40 deletions(-)

(limited to 'Test/textbook/Find.bpl')

diff --git a/Test/textbook/Find.bpl b/Test/textbook/Find.bpl
index 5a77c621..758ba4cc 100644
--- a/Test/textbook/Find.bpl
+++ b/Test/textbook/Find.bpl
@@ -1,40 +1,40 @@
-// RUN: %boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// Declare a constant 'K' and a function 'f' and postulate that 'K' is
-// in the image of 'f'
-const K: int;
-function f(int) returns (int);
-axiom (exists k: int :: f(k) == K);
-
-// This procedure will find a domain value 'k' that 'f' maps to 'K'.  It will
-// do that by recursively enlarging the range where no such domain value exists.
-// Note, Boogie does not prove termination.
-procedure Find(a: int, b: int) returns (k: int)
-  requires a <= b;
-  requires (forall j: int :: a < j && j < b ==> f(j) != K);
-  ensures f(k) == K;
-{
-  goto A, B, C;  // nondeterministically choose one of these 3 goto targets
-
-  A:
-    assume f(a) == K;  // assume we get here only if 'f' maps 'a' to 'K'
-    k := a;
-    return;
-
-  B:
-    assume f(b) == K;  // assume we get here only if 'f' maps 'b' to 'K'
-    k := b;
-    return;
-
-  C:
-    assume f(a) != K && f(b) != K;  // neither of the two above
-    call k := Find(a-1, b+1);
-    return;
-}
-
-// This procedure shows one way to call 'Find'
-procedure Main() returns (k: int)
-  ensures f(k) == K;
-{
-  call k := Find(0, 0);
-}
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// Declare a constant 'K' and a function 'f' and postulate that 'K' is
+// in the image of 'f'
+const K: int;
+function f(int) returns (int);
+axiom (exists k: int :: f(k) == K);
+
+// This procedure will find a domain value 'k' that 'f' maps to 'K'.  It will
+// do that by recursively enlarging the range where no such domain value exists.
+// Note, Boogie does not prove termination.
+procedure Find(a: int, b: int) returns (k: int)
+  requires a <= b;
+  requires (forall j: int :: a < j && j < b ==> f(j) != K);
+  ensures f(k) == K;
+{
+  goto A, B, C;  // nondeterministically choose one of these 3 goto targets
+
+  A:
+    assume f(a) == K;  // assume we get here only if 'f' maps 'a' to 'K'
+    k := a;
+    return;
+
+  B:
+    assume f(b) == K;  // assume we get here only if 'f' maps 'b' to 'K'
+    k := b;
+    return;
+
+  C:
+    assume f(a) != K && f(b) != K;  // neither of the two above
+    call k := Find(a-1, b+1);
+    return;
+}
+
+// This procedure shows one way to call 'Find'
+procedure Main() returns (k: int)
+  ensures f(k) == K;
+{
+  call k := Find(0, 0);
+}
-- 
cgit v1.2.3