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/test1/WhereTyping.bpl | 94 +++++++++++++++++++++++-----------------------
 1 file changed, 47 insertions(+), 47 deletions(-)

(limited to 'Test/test1/WhereTyping.bpl')

diff --git a/Test/test1/WhereTyping.bpl b/Test/test1/WhereTyping.bpl
index 0884e8ef..b3675f45 100644
--- a/Test/test1/WhereTyping.bpl
+++ b/Test/test1/WhereTyping.bpl
@@ -1,47 +1,47 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-var g: int where g == 12;
-
-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;
-  var b: int;
-
-  start:
-    a := xx;
-    call b := P(a);
-    yy := b;
-    return;
-}
-
-type double;
-function F(double) returns (double);
-function G(double) returns (bool);
-
-procedure Q(omega: double where omega == F(omega),
-            psi: double where psi + 1 == 0,  // error: psi doesn't have right type for +
-            pi: double where F(pi),          // error: F has wrong return type
-            sigma: double where G(sigma));
-
-
-const SomeConstant: name;
-function fgh(int) returns (int);
-
-procedure Cnst(n: name where n <: SomeConstant /*this SomeConstant refers to the const*/) returns (SomeConstant: int)
-{
-  var k: int where k != SomeConstant;  // fine, since SomeConstants refers to the out parameter
-  var m: name where m != SomeConstant;  // error: types don't match up
-  var r: ref where (forall abc: int :: abc == SomeConstant);
-  var b: bool;
-  start:
-    b := (forall x: int :: fgh(x) < SomeConstant);
-    b := (forall l: name :: l == SomeConstant);  // error: SomeConstant here refers to the out parameter
-    return;
-}
-
-type ref, name;
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var g: int where g == 12;
+
+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;
+  var b: int;
+
+  start:
+    a := xx;
+    call b := P(a);
+    yy := b;
+    return;
+}
+
+type double;
+function F(double) returns (double);
+function G(double) returns (bool);
+
+procedure Q(omega: double where omega == F(omega),
+            psi: double where psi + 1 == 0,  // error: psi doesn't have right type for +
+            pi: double where F(pi),          // error: F has wrong return type
+            sigma: double where G(sigma));
+
+
+const SomeConstant: name;
+function fgh(int) returns (int);
+
+procedure Cnst(n: name where n <: SomeConstant /*this SomeConstant refers to the const*/) returns (SomeConstant: int)
+{
+  var k: int where k != SomeConstant;  // fine, since SomeConstants refers to the out parameter
+  var m: name where m != SomeConstant;  // error: types don't match up
+  var r: ref where (forall abc: int :: abc == SomeConstant);
+  var b: bool;
+  start:
+    b := (forall x: int :: fgh(x) < SomeConstant);
+    b := (forall l: name :: l == SomeConstant);  // error: SomeConstant here refers to the out parameter
+    return;
+}
+
+type ref, name;
-- 
cgit v1.2.3