summaryrefslogtreecommitdiff
path: root/Test/test1/IntReal.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/test1/IntReal.bpl')
-rw-r--r--Test/test1/IntReal.bpl100
1 files changed, 50 insertions, 50 deletions
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;