summaryrefslogtreecommitdiff
path: root/float_test3.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'float_test3.bpl')
-rw-r--r--float_test3.bpl2
1 files changed, 1 insertions, 1 deletions
diff --git a/float_test3.bpl b/float_test3.bpl
index cd0ea59e..1b70ebf4 100644
--- a/float_test3.bpl
+++ b/float_test3.bpl
@@ -2,5 +2,5 @@
var x : float;
var y : float;
y := x - x;
- assert y != x;
+ assert y == x;
} \ No newline at end of file