summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--float_test10.bpl5
-rw-r--r--float_test8.bpl5
-rw-r--r--float_test9.bpl5
3 files changed, 15 insertions, 0 deletions
diff --git a/float_test10.bpl b/float_test10.bpl
new file mode 100644
index 00000000..7423a3a0
--- /dev/null
+++ b/float_test10.bpl
@@ -0,0 +1,5 @@
+ procedure F() returns () {
+ var x : float;
+ x := fp (0.5 23 8);
+ assert x == fp (0 -1);
+} \ No newline at end of file
diff --git a/float_test8.bpl b/float_test8.bpl
new file mode 100644
index 00000000..8d881126
--- /dev/null
+++ b/float_test8.bpl
@@ -0,0 +1,5 @@
+procedure F() returns () {
+ var x : float;
+ x := fp(.1) + fp(.1);
+ assert x == fp(.2);
+} \ No newline at end of file
diff --git a/float_test9.bpl b/float_test9.bpl
new file mode 100644
index 00000000..7423a3a0
--- /dev/null
+++ b/float_test9.bpl
@@ -0,0 +1,5 @@
+ procedure F() returns () {
+ var x : float;
+ x := fp (0.5 23 8);
+ assert x == fp (0 -1);
+} \ No newline at end of file