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/test1/IntReal.bpl | 100 ++++++++++++++++++++++++-------------------------
 1 file changed, 50 insertions(+), 50 deletions(-)

(limited to 'Test/test1/IntReal.bpl')

diff --git a/Test/test1/IntReal.bpl b/Test/test1/IntReal.bpl
index 962aadf3..7b3d77e5 100644
--- a/Test/test1/IntReal.bpl
+++ b/Test/test1/IntReal.bpl
@@ -1,50 +1,50 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-const i: int;
-const r: real;
-
-axiom i == 0;
-axiom i >= 0.0;                // type error
-axiom i <= 0.0e0;              // type error
-axiom i < 0.0e-0;              // type error
-axiom i > 0.0e20;              // type error
-
-axiom -i == r;                 // type error
-axiom i + r == 0.0;            // type error
-axiom i - r == 0.0;            // type error
-axiom i * r == 0.0;            // type error
-axiom i div r == 0;            // type error
-axiom i mod r == 0;            // type error
-
-axiom i / i == 0;              // type error
-axiom i / i == 0.0;
-axiom i / r == 0.0;
-axiom r / i == 0.0;
-axiom r / r == 0.0;
-
-axiom i ** r == 0.0;           // type error
-axiom r ** r == 0.0;
-
-axiom real(i) == 0.0;
-axiom real(i) == i;            // type error
-axiom int(r) == 0;
-axiom int(r) == r;             // type error
-axiom int(real(i)) == i;
-axiom real(int(r)) == r;
-axiom int(int(r)) == i;        // type error
-axiom real(real(i)) == r;      // type error
-
-axiom i == 0;
-axiom real(i) >= 0.0;
-axiom real(i) <= 0.0e0;
-axiom r < 0.0e-0;
-axiom r > 0.0e20;
-
-axiom -r == real(i);
-axiom real(i) + r == 0.0;
-axiom r - real(0) == 0.0;
-axiom r * r == 0.0;
-axiom r div 0 == 0;            // type error
-axiom r mod 0 == 0;            // type error
-
-axiom r ** r == 0.0;
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+const i: int;
+const r: real;
+
+axiom i == 0;
+axiom i >= 0.0;                // type error
+axiom i <= 0.0e0;              // type error
+axiom i < 0.0e-0;              // type error
+axiom i > 0.0e20;              // type error
+
+axiom -i == r;                 // type error
+axiom i + r == 0.0;            // type error
+axiom i - r == 0.0;            // type error
+axiom i * r == 0.0;            // type error
+axiom i div r == 0;            // type error
+axiom i mod r == 0;            // type error
+
+axiom i / i == 0;              // type error
+axiom i / i == 0.0;
+axiom i / r == 0.0;
+axiom r / i == 0.0;
+axiom r / r == 0.0;
+
+axiom i ** r == 0.0;           // type error
+axiom r ** r == 0.0;
+
+axiom real(i) == 0.0;
+axiom real(i) == i;            // type error
+axiom int(r) == 0;
+axiom int(r) == r;             // type error
+axiom int(real(i)) == i;
+axiom real(int(r)) == r;
+axiom int(int(r)) == i;        // type error
+axiom real(real(i)) == r;      // type error
+
+axiom i == 0;
+axiom real(i) >= 0.0;
+axiom real(i) <= 0.0e0;
+axiom r < 0.0e-0;
+axiom r > 0.0e20;
+
+axiom -r == real(i);
+axiom real(i) + r == 0.0;
+axiom r - real(0) == 0.0;
+axiom r * r == 0.0;
+axiom r div 0 == 0;            // type error
+axiom r mod 0 == 0;            // type error
+
+axiom r ** r == 0.0;
-- 
cgit v1.2.3