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/test2/Ensures.bpl | 154 ++++++++++++++++++++++++-------------------------
 1 file changed, 77 insertions(+), 77 deletions(-)

(limited to 'Test/test2/Ensures.bpl')

diff --git a/Test/test2/Ensures.bpl b/Test/test2/Ensures.bpl
index c37e31a0..16f6105f 100644
--- a/Test/test2/Ensures.bpl
+++ b/Test/test2/Ensures.bpl
@@ -1,77 +1,77 @@
-// RUN: %boogie -noinfer "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-var H: [ref,name]int;
-var that: ref;
-
-const X: name;
-const Y: name;
-
-procedure P(this: ref);
-  modifies H;
-  ensures H[this,X] == 5;
-
-implementation P(this: ref) {
-  start:
-    H[this,X] := 5;
-    return;
-}
-
-procedure Q(this: ref);
-  modifies H;
-  ensures (forall o: ref, F: name :: o == this && F == X ==> H[o,F] == 5);
-
-implementation Q(this: ref) {
-  start:
-    H[this,X] := 5;
-    return;
-}
-
-implementation Q(this: ref) {
-  start:
-    H[this,X] := 7;
-    return;  // error
-}
-
-implementation Q(this: ref) {
-  start:
-    return;  // error
-}
-
-implementation Q(this: ref) {
-  start:
-    H[that,X] := 5;
-    return;  // error
-}
-
-implementation Q(this: ref) {
-  start:
-    H[this,Y] := 5;
-    return;  // error
-}
-
-implementation Q(this: ref) {
-  start:
-    call P(this);
-    return;
-}
-
-implementation Q(this: ref) {
-  start:
-    call Q(this);
-    return;
-}
-
-implementation Q(this: ref) {
-  start:
-    call P(this);
-    call Q(this);
-    return;
-}
-
-implementation Q(this: ref) {
-  start:
-    call P(that);
-    return;  // error
-}
-
-type name, ref;
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var H: [ref,name]int;
+var that: ref;
+
+const X: name;
+const Y: name;
+
+procedure P(this: ref);
+  modifies H;
+  ensures H[this,X] == 5;
+
+implementation P(this: ref) {
+  start:
+    H[this,X] := 5;
+    return;
+}
+
+procedure Q(this: ref);
+  modifies H;
+  ensures (forall o: ref, F: name :: o == this && F == X ==> H[o,F] == 5);
+
+implementation Q(this: ref) {
+  start:
+    H[this,X] := 5;
+    return;
+}
+
+implementation Q(this: ref) {
+  start:
+    H[this,X] := 7;
+    return;  // error
+}
+
+implementation Q(this: ref) {
+  start:
+    return;  // error
+}
+
+implementation Q(this: ref) {
+  start:
+    H[that,X] := 5;
+    return;  // error
+}
+
+implementation Q(this: ref) {
+  start:
+    H[this,Y] := 5;
+    return;  // error
+}
+
+implementation Q(this: ref) {
+  start:
+    call P(this);
+    return;
+}
+
+implementation Q(this: ref) {
+  start:
+    call Q(this);
+    return;
+}
+
+implementation Q(this: ref) {
+  start:
+    call P(this);
+    call Q(this);
+    return;
+}
+
+implementation Q(this: ref) {
+  start:
+    call P(that);
+    return;  // error
+}
+
+type name, ref;
-- 
cgit v1.2.3