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/test20/PolyFuns1.bpl | 122 +++++++++++++++++++++++-----------------------
 1 file changed, 61 insertions(+), 61 deletions(-)

(limited to 'Test/test20/PolyFuns1.bpl')

diff --git a/Test/test20/PolyFuns1.bpl b/Test/test20/PolyFuns1.bpl
index 12a8a1b8..01d6638c 100644
--- a/Test/test20/PolyFuns1.bpl
+++ b/Test/test20/PolyFuns1.bpl
@@ -1,61 +1,61 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-function F<a>( <b>[b]a ) returns (bool);
-const M:  <a>[ <b>[b]a ] bool;
-
-procedure P()
-{
-  var f: <c>[c]c;
-  var b: bool;
-
-  b := F(f);  // type error
-  b := M[f];  // type error
-  b := (forall g: <c>[c]c :: F(g));  // type error
-  b := (forall g: <c>[c]c :: M[g]);  // type error
-}
-
-type Field a;
-axiom (exists<a> x:<c>[Field c]a, y:<d>[Field d]d :: x == y);   // error: not unifiable
-axiom (forall<a> x:<c>[Field c]a, y:<d>[Field d]d :: x == y);   // error: not unifiable
-
-procedure Uhu<a>(x: <c>[Field c]a, y: <d>[Field d]d);
-procedure Oyeah<T>(t: T)
-{
-  var xx: <cc>[Field cc]T;
-  var yy: <dd>[Field dd]dd;
-  var zz: <ee>[Field T]ee;
-
-  call Uhu(xx, yy);
-  call Uhu(yy, yy);  // type error in argument 0
-  call Uhu(xx, xx);  // type error in argument 1
-  assert xx == yy;  // error: not unifiable
-  assert yy == xx;  // error: not unifiable
-
-  call Uhu(xx, zz);  // type error in argument 1
-}
-
-procedure Jitters()
-{
-  var x: <a>[a,a]int;
-  var y: <b>[b,int]int;
-  var z: <c>[int,c]int;
-  assert x == y;  // error: not unifiable
-  assert y == z;  // error: not unifiable
-  assert x == z;  // error: not unifiable
-}
-
-procedure Nuther()
-{
-  var x: <a,b>[a,a,b]int;
-  var y: <a,b>[a,b,b]int;
-  assert x == y;  // error: not unifiable
-}
-
-type NagainCtor a;
-procedure Nagain()
-  requires (forall<a,b> x: a, y: b :: x == y);
-  ensures (forall<a,b> x: a, y: Field b, z: NagainCtor b :: x == y && x == z);
-  ensures (forall<b> y: Field b, z: NagainCtor b :: y == z);  // error: types not unifiable
-{
-}
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+function F<a>( <b>[b]a ) returns (bool);
+const M:  <a>[ <b>[b]a ] bool;
+
+procedure P()
+{
+  var f: <c>[c]c;
+  var b: bool;
+
+  b := F(f);  // type error
+  b := M[f];  // type error
+  b := (forall g: <c>[c]c :: F(g));  // type error
+  b := (forall g: <c>[c]c :: M[g]);  // type error
+}
+
+type Field a;
+axiom (exists<a> x:<c>[Field c]a, y:<d>[Field d]d :: x == y);   // error: not unifiable
+axiom (forall<a> x:<c>[Field c]a, y:<d>[Field d]d :: x == y);   // error: not unifiable
+
+procedure Uhu<a>(x: <c>[Field c]a, y: <d>[Field d]d);
+procedure Oyeah<T>(t: T)
+{
+  var xx: <cc>[Field cc]T;
+  var yy: <dd>[Field dd]dd;
+  var zz: <ee>[Field T]ee;
+
+  call Uhu(xx, yy);
+  call Uhu(yy, yy);  // type error in argument 0
+  call Uhu(xx, xx);  // type error in argument 1
+  assert xx == yy;  // error: not unifiable
+  assert yy == xx;  // error: not unifiable
+
+  call Uhu(xx, zz);  // type error in argument 1
+}
+
+procedure Jitters()
+{
+  var x: <a>[a,a]int;
+  var y: <b>[b,int]int;
+  var z: <c>[int,c]int;
+  assert x == y;  // error: not unifiable
+  assert y == z;  // error: not unifiable
+  assert x == z;  // error: not unifiable
+}
+
+procedure Nuther()
+{
+  var x: <a,b>[a,a,b]int;
+  var y: <a,b>[a,b,b]int;
+  assert x == y;  // error: not unifiable
+}
+
+type NagainCtor a;
+procedure Nagain()
+  requires (forall<a,b> x: a, y: b :: x == y);
+  ensures (forall<a,b> x: a, y: Field b, z: NagainCtor b :: x == y && x == z);
+  ensures (forall<b> y: Field b, z: NagainCtor b :: y == z);  // error: types not unifiable
+{
+}
-- 
cgit v1.2.3