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/codeexpr/CodeExpr0.bpl | 110 ++++++++++++++++++++++----------------------
 1 file changed, 55 insertions(+), 55 deletions(-)

(limited to 'Test/codeexpr/CodeExpr0.bpl')

diff --git a/Test/codeexpr/CodeExpr0.bpl b/Test/codeexpr/CodeExpr0.bpl
index 97dd60e7..e6bf584d 100644
--- a/Test/codeexpr/CodeExpr0.bpl
+++ b/Test/codeexpr/CodeExpr0.bpl
@@ -1,55 +1,55 @@
-// RUN: %boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure P()
-{
-  assert |{ A: return true; }|;
-}
-
-// ------------
-
-procedure Q()
-{
-  assert |{ var x: bool; A: x := true; return x; }|;
-}
-
-procedure R()
-{
-  assert |{ var x: bool; A: x := false; return x; }|;  // error
-}
-
-procedure S()
-{
-  assert |{ var x: bool; A: return x; }|;  // error
-}
-
-// ------------
-
-procedure T(x: int, y: int)
-  requires |{ var z: bool;
-              Start: goto A;
-              A: z := false; goto B, C;
-              B: assume 0 <= x; goto D;
-              C: assume x < 0; goto R;
-              D: goto E, F;
-              E: assume 0 <= y; z := true; goto R;
-              F: assume y < 0; goto R;
-              R: return z;
-           }|;
-{
-  assert 0 <= x + y;
-}
-
-procedure U(x: int, y: int)
-  requires |{ var z: bool;
-              Start: goto A;
-              A: z := false; goto B, C;
-              B: assume 0 <= x; goto D;
-              C: assume x < 0; goto R;
-              D: goto E, F;
-              E: assume 0 <= y; z := true; goto R;
-              F: assume y < 0; goto R;
-              R: return z;
-           }|;
-{
-  assert x <= y;  // error
-}
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure P()
+{
+  assert |{ A: return true; }|;
+}
+
+// ------------
+
+procedure Q()
+{
+  assert |{ var x: bool; A: x := true; return x; }|;
+}
+
+procedure R()
+{
+  assert |{ var x: bool; A: x := false; return x; }|;  // error
+}
+
+procedure S()
+{
+  assert |{ var x: bool; A: return x; }|;  // error
+}
+
+// ------------
+
+procedure T(x: int, y: int)
+  requires |{ var z: bool;
+              Start: goto A;
+              A: z := false; goto B, C;
+              B: assume 0 <= x; goto D;
+              C: assume x < 0; goto R;
+              D: goto E, F;
+              E: assume 0 <= y; z := true; goto R;
+              F: assume y < 0; goto R;
+              R: return z;
+           }|;
+{
+  assert 0 <= x + y;
+}
+
+procedure U(x: int, y: int)
+  requires |{ var z: bool;
+              Start: goto A;
+              A: z := false; goto B, C;
+              B: assume 0 <= x; goto D;
+              C: assume x < 0; goto R;
+              D: goto E, F;
+              E: assume 0 <= y; z := true; goto R;
+              F: assume y < 0; goto R;
+              R: return z;
+           }|;
+{
+  assert x <= y;  // error
+}
-- 
cgit v1.2.3