Merging complete. Everything looks good *crosses fingers*

1 files changed, 55 insertions, 55 deletions

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
+}