diff options
Diffstat (limited to 'Test/dafny4/Bug148.dfy')
| -rw-r--r-- | Test/dafny4/Bug148.dfy | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/Test/dafny4/Bug148.dfy b/Test/dafny4/Bug148.dfy new file mode 100644 index 00000000..b7a08952 --- /dev/null +++ b/Test/dafny4/Bug148.dfy @@ -0,0 +1,25 @@ +// RUN: %dafny /compile:3 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Main()
+{
+ var zero : real := 0.0;
+ var three : real := 3.0;
+ var fifteen : real := 15.0;
+ var negone : real := -1.0;
+ var negthree : real := -3.0;
+
+ print zero <= fifteen, "\n"; // true
+ print fifteen <= zero, "\n"; // false
+ print negone <= zero, "\n"; // true
+ print zero <= negone, "\n"; // false
+ print negone <= fifteen, "\n"; // true
+ print fifteen <= negone, "\n"; // false
+
+ print zero >= fifteen, "\n"; // false
+ print fifteen >= zero, "\n"; // true
+ print negone >= zero, "\n"; // false
+ print zero >= negone, "\n"; // true
+ print negone >= fifteen, "\n"; // false
+ print fifteen >= negone, "\n"; // true
+}
|