summaryrefslogtreecommitdiff
path: root/float_test2.bpl
diff options
context:
space:
mode:
authorGravatar Dietrich <dgeisler50@gmail.com>2015-04-26 16:21:38 -0600
committerGravatar Dietrich <dgeisler50@gmail.com>2015-04-26 16:21:38 -0600
commit1797c235986f576998e28380e1ec4e6005087ebb (patch)
treecc0fcae2175e5cbfd841d4cf55615657fa284251 /float_test2.bpl
parenteed63d900b802e5551bf3c31772c39d365e7fcec (diff)
Successfully parsed the float type
Diffstat (limited to 'float_test2.bpl')
-rw-r--r--float_test2.bpl4
1 files changed, 2 insertions, 2 deletions
diff --git a/float_test2.bpl b/float_test2.bpl
index 71ea7dee..fa34d8cf 100644
--- a/float_test2.bpl
+++ b/float_test2.bpl
@@ -1,5 +1,5 @@
procedure F() returns () {
- var x : real;
- var y : real;
+ var x : float;
+ var y : float;
assert x == y;
} \ No newline at end of file