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/test0/WhereResolution.bpl | 128 ++++++++++++++++++++---------------------
 1 file changed, 64 insertions(+), 64 deletions(-)

(limited to 'Test/test0/WhereResolution.bpl')

diff --git a/Test/test0/WhereResolution.bpl b/Test/test0/WhereResolution.bpl
index fac91dc8..9083d1fa 100644
--- a/Test/test0/WhereResolution.bpl
+++ b/Test/test0/WhereResolution.bpl
@@ -1,64 +1,64 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-type double;
-
-function R(int) returns (bool);
-function K(double, bool) returns (bool);
-
-var y: int where R(y);
-var g: int where h ==> g == 12;
-var h: bool where g < 100;
-var k: double where K(k, h);
-
-procedure P(x: int where x > 0) returns (y: int where y < 0);
-  requires x < 100;
-  modifies g;
-  ensures -100 < y;
-
-implementation P(xx: int) returns (yy: int)
-{
-  var a: int where a == 10;
-  var b: int where a == b && b < g;
-
-  start:
-    a := xx;
-    call b := P(a);
-    yy := b;
-    return;
-}
-
-procedure Q(w: int where x < w || x > alpha/*error: out-parameter alpha is not in scope*/, x: int where x + w > 0)
-    returns (v: bool where v,
-             y: int where x + y + z < 0,
-             z: int where g == 12,
-             alpha: ref where old(alpha) != null,  // error: cannot use old in where clause
-             beta: ref where (forall r: ref :: r == beta ==> beta == null))
-  requires x < 100;
-  modifies g;
-  ensures -100 < y;
-{
-  var a: int;
-  var b: int;
-
-  start:
-    a := x;
-    call b := P(a);
-    y := b;
-    return;
-}
-
-const SomeConstant: ref;
-
-procedure Cnst(n: ref where n != SomeConstant) returns (SomeConstant: int)
-{
-  var m: ref where m != SomeConstant;
-  var k: int where k != SomeConstant;
-  var r: ref where (forall abc: ref :: abc == SomeConstant);
-  var b: bool;
-  start:
-    b := (forall l: ref :: l == SomeConstant);
-    return;
-}
-
-type ref;
-const null : ref;
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type double;
+
+function R(int) returns (bool);
+function K(double, bool) returns (bool);
+
+var y: int where R(y);
+var g: int where h ==> g == 12;
+var h: bool where g < 100;
+var k: double where K(k, h);
+
+procedure P(x: int where x > 0) returns (y: int where y < 0);
+  requires x < 100;
+  modifies g;
+  ensures -100 < y;
+
+implementation P(xx: int) returns (yy: int)
+{
+  var a: int where a == 10;
+  var b: int where a == b && b < g;
+
+  start:
+    a := xx;
+    call b := P(a);
+    yy := b;
+    return;
+}
+
+procedure Q(w: int where x < w || x > alpha/*error: out-parameter alpha is not in scope*/, x: int where x + w > 0)
+    returns (v: bool where v,
+             y: int where x + y + z < 0,
+             z: int where g == 12,
+             alpha: ref where old(alpha) != null,  // error: cannot use old in where clause
+             beta: ref where (forall r: ref :: r == beta ==> beta == null))
+  requires x < 100;
+  modifies g;
+  ensures -100 < y;
+{
+  var a: int;
+  var b: int;
+
+  start:
+    a := x;
+    call b := P(a);
+    y := b;
+    return;
+}
+
+const SomeConstant: ref;
+
+procedure Cnst(n: ref where n != SomeConstant) returns (SomeConstant: int)
+{
+  var m: ref where m != SomeConstant;
+  var k: int where k != SomeConstant;
+  var r: ref where (forall abc: ref :: abc == SomeConstant);
+  var b: bool;
+  start:
+    b := (forall l: ref :: l == SomeConstant);
+    return;
+}
+
+type ref;
+const null : ref;
-- 
cgit v1.2.3