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/test2/sk_hack.bpl | 68 +++++++++++++++++++++++++-------------------------
 1 file changed, 34 insertions(+), 34 deletions(-)

(limited to 'Test/test2/sk_hack.bpl')

diff --git a/Test/test2/sk_hack.bpl b/Test/test2/sk_hack.bpl
index 7ce8e4dc..163bbc26 100644
--- a/Test/test2/sk_hack.bpl
+++ b/Test/test2/sk_hack.bpl
@@ -1,34 +1,34 @@
-// RUN: %boogie -noinfer "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-function in_set(int) returns(bool);
-function next(int) returns(int);
-function f(int) returns(bool);
-function g(int) returns(bool);
-
-// this function is treated specially by Z3 when used in triggers
-//    sk_hack(f(x)) means to activate the e-node f(x0) when trying to prove
-//    !(forall x : T :: {sk_hack(f(x))} p(x)) by proving !p(x0) 
-//    (i.e., after skolemization of x to x0).
-function sk_hack(bool) returns(bool);
-
-// PR: sk_hack cannot be defined as a polymorphic function
-// when using /quantifierTypePremisses:a, because then it would
-// get an additional explicit type parameter, and Z3 would
-// no longer recognise it.
-
-procedure foo()
-{
-  assume (forall x:int :: {in_set(next(x))}
-     in_set(x) ==> in_set(next(x)));
-
-  assume (forall x:int :: {in_set(x)}
-     in_set(x) ==> f(x));
-
-  assume (forall x:int :: {f(next(x))}
-     f(next(x)) ==> g(x));
-
-  assert (forall x:int ::
-    { sk_hack(in_set(next(x))) }
-    in_set(x) ==> g(x));
-  }
-
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+function in_set(int) returns(bool);
+function next(int) returns(int);
+function f(int) returns(bool);
+function g(int) returns(bool);
+
+// this function is treated specially by Z3 when used in triggers
+//    sk_hack(f(x)) means to activate the e-node f(x0) when trying to prove
+//    !(forall x : T :: {sk_hack(f(x))} p(x)) by proving !p(x0) 
+//    (i.e., after skolemization of x to x0).
+function sk_hack(bool) returns(bool);
+
+// PR: sk_hack cannot be defined as a polymorphic function
+// when using /quantifierTypePremisses:a, because then it would
+// get an additional explicit type parameter, and Z3 would
+// no longer recognise it.
+
+procedure foo()
+{
+  assume (forall x:int :: {in_set(next(x))}
+     in_set(x) ==> in_set(next(x)));
+
+  assume (forall x:int :: {in_set(x)}
+     in_set(x) ==> f(x));
+
+  assume (forall x:int :: {f(next(x))}
+     f(next(x)) ==> g(x));
+
+  assert (forall x:int ::
+    { sk_hack(in_set(next(x))) }
+    in_set(x) ==> g(x));
+  }
+
-- 
cgit v1.2.3