Merging complete. Everything looks good *crosses fingers*

1 files changed, 26 insertions, 26 deletions

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