From 962f8d5252b3f5ec4d19e0cd2a430934bd55cc6d Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sun, 28 Jun 2015 01:44:30 +0100
Subject: Normalise line endings using a .gitattributes file. Unfortunately
 this required that this commit globally modify most files. If you want to use
 git blame to see the real author of a line use the ``-w`` flag so that
 whitespace changes are ignored.

---
 Test/z3api/boog17.bpl | 52 +++++++++++++++++++++++++--------------------------
 1 file changed, 26 insertions(+), 26 deletions(-)

(limited to 'Test/z3api/boog17.bpl')

diff --git a/Test/z3api/boog17.bpl b/Test/z3api/boog17.bpl
index 89159af1..24d87dc7 100644
--- a/Test/z3api/boog17.bpl
+++ b/Test/z3api/boog17.bpl
@@ -1,27 +1,27 @@
-type name;
-type ref;
-const unique g : int;
-axiom(g != 0);
-
-const unique PINT4_name:name;
-
-function PLUS(a:int, a_size:int, b:int) returns (int);
-axiom(forall a:int, a_size:int, b:int :: {PLUS(a,a_size,b)} PLUS(a,a_size,b) == a + a_size * b);
-
-function HasType(v:int, t:name) returns (bool);
-
-
-procedure  main ( ) returns ($result.main$11.5$1$:int) {
-  var p : int;
-
-start:
-  assume(HasType(p, PINT4_name));
-  goto label_3;
-
-label_3:
-  goto label_4;
-
-label_4:
-  p := PLUS(g, 4, 55) ;
-  assert(HasType(p, PINT4_name));
+type name;
+type ref;
+const unique g : int;
+axiom(g != 0);
+
+const unique PINT4_name:name;
+
+function PLUS(a:int, a_size:int, b:int) returns (int);
+axiom(forall a:int, a_size:int, b:int :: {PLUS(a,a_size,b)} PLUS(a,a_size,b) == a + a_size * b);
+
+function HasType(v:int, t:name) returns (bool);
+
+
+procedure  main ( ) returns ($result.main$11.5$1$:int) {
+  var p : int;
+
+start:
+  assume(HasType(p, PINT4_name));
+  goto label_3;
+
+label_3:
+  goto label_4;
+
+label_4:
+  p := PLUS(g, 4, 55) ;
+  assert(HasType(p, PINT4_name));
 }
\ No newline at end of file
-- 
cgit v1.2.3