diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-09-27 15:18:47 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-09-27 15:18:47 -0700 |
| commit | 7cc79726ea246593f4a903ad89b55aa0949fc915 (patch) | |
| tree | 1e94082e49e1965510993b93f35b3779d168e9a5 /Test/test1 | |
| parent | 43b80b13bd24bb789849aac3385df6ac4a8233be (diff) | |
Boogie and Dafny: adjustments to the test suite expected output (and a temporary hack in FloydCycleDetect.dfy to be corrected shortly)
Diffstat (limited to 'Test/test1')
| -rw-r--r-- | Test/test1/IntReal.bpl | 40 |
1 files changed, 20 insertions, 20 deletions
diff --git a/Test/test1/IntReal.bpl b/Test/test1/IntReal.bpl index fac41d57..976fc864 100644 --- a/Test/test1/IntReal.bpl +++ b/Test/test1/IntReal.bpl @@ -2,35 +2,35 @@ const i: int; const r: real;
axiom i == 0;
-axiom i >= 0.0; // type errror
-axiom i <= 0.0e0; // type errror
-axiom i < 0.0e-0; // type errror
-axiom i > 0.0e20; // type errror
-
-axiom -i == r; // type errror
-axiom i + r == 0.0; // type errror
-axiom i - r == 0.0; // type errror
-axiom i * r == 0.0; // type errror
-axiom i div r == 0; // type errror
-axiom i mod r == 0; // type errror
-
-axiom i / i == 0; // type errror
+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 errror
+axiom i ** r == 0.0; // type error
axiom r ** r == 0.0;
axiom real(i) == 0.0;
-axiom real(i) == i; // type errror
+axiom real(i) == i; // type error
axiom int(r) == 0;
-axiom int(r) == r; // type errror
+axiom int(r) == r; // type error
axiom int(real(i)) == i;
axiom real(int(r)) == r;
-axiom int(int(r)) == i; // type errror
-axiom real(real(i)) == r; // type errror
+axiom int(int(r)) == i; // type error
+axiom real(real(i)) == r; // type error
axiom i == 0;
axiom real(i) >= 0.0;
@@ -42,7 +42,7 @@ 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 errror
-axiom r mod 0 == 0; // type errror
+axiom r div 0 == 0; // type error
+axiom r mod 0 == 0; // type error
axiom r ** r == 0.0;
|