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/Prog0.bpl | 106 +++++++++++++++++++++++++--------------------------
 1 file changed, 53 insertions(+), 53 deletions(-)

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

diff --git a/Test/test0/Prog0.bpl b/Test/test0/Prog0.bpl
index d9e467ec..51383660 100644
--- a/Test/test0/Prog0.bpl
+++ b/Test/test0/Prog0.bpl
@@ -1,53 +1,53 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff NoErrors.expect "%t"
-// BoogiePL Examples
-
-type elements;
-
-var x:int;  var y:real;  var z:ref;		// Variables
-var x.3:bool; var $ar:ref;		// Names can have glyphs
-
-const a, b, c:int;		// Consts
-
-function f (int, int) returns (int);	// Function with arity 2
-function g (   int , int) returns (int);	// Function with arity 2
-function h(int,int) returns (int);	// Function with arity 2
-
-function m (int) returns (int);	// Function with arity 1
-function k(int) returns (int);	// Function with arity 1
-
-
-axiom 	
-  (forall x : int :: f(g(h(a,b),c),x) > 100) ;
-
-procedure p (x:int, y:ref) returns (z:int, w:[int,ref]ref, q:int);
-
-
-procedure q(x:int, y:ref) returns (z:int)	// Procedure with output params
-  requires x > 0;		// as many req/ens/mod you want
-  ensures z > 3;	
-  ensures old(x) == 1;		// old only in ensures..
-  modifies z,y,$ar;
-{  
-  var t, s: int;
-  var r: [int,ref]ref;
-  
-  start:			// one label per block
-    t := x;
-    s := t;
-    z := x + t;
-    call s, r,z := p(t,r[3,null]);	// procedure call with mutiple returns
-    goto continue, end ;	// as many labels as you like
- 
-  continue:
-    return;			// ends control flow
-    
-  end:
-    goto start;
-}    
-
-procedure s(e: elements) { L: return; }
-procedure r (x:int, y:ref) returns (z:int);
-
-type ref;
-const null : ref;
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff NoErrors.expect "%t"
+// BoogiePL Examples
+
+type elements;
+
+var x:int;  var y:real;  var z:ref;		// Variables
+var x.3:bool; var $ar:ref;		// Names can have glyphs
+
+const a, b, c:int;		// Consts
+
+function f (int, int) returns (int);	// Function with arity 2
+function g (   int , int) returns (int);	// Function with arity 2
+function h(int,int) returns (int);	// Function with arity 2
+
+function m (int) returns (int);	// Function with arity 1
+function k(int) returns (int);	// Function with arity 1
+
+
+axiom 	
+  (forall x : int :: f(g(h(a,b),c),x) > 100) ;
+
+procedure p (x:int, y:ref) returns (z:int, w:[int,ref]ref, q:int);
+
+
+procedure q(x:int, y:ref) returns (z:int)	// Procedure with output params
+  requires x > 0;		// as many req/ens/mod you want
+  ensures z > 3;	
+  ensures old(x) == 1;		// old only in ensures..
+  modifies z,y,$ar;
+{  
+  var t, s: int;
+  var r: [int,ref]ref;
+  
+  start:			// one label per block
+    t := x;
+    s := t;
+    z := x + t;
+    call s, r,z := p(t,r[3,null]);	// procedure call with mutiple returns
+    goto continue, end ;	// as many labels as you like
+ 
+  continue:
+    return;			// ends control flow
+    
+  end:
+    goto start;
+}    
+
+procedure s(e: elements) { L: return; }
+procedure r (x:int, y:ref) returns (z:int);
+
+type ref;
+const null : ref;
-- 
cgit v1.2.3