diff options
| author |  Checkmate50 <dgeisler50@gmail.com> | 2015-11-29 14:28:17 -0700 |
|---|---|---|
| committer | Checkmate50 <dgeisler50@gmail.com> | 2015-11-29 14:28:17 -0700 |
| commit | a1c9e11736bda4bf8ea4bf431523b9b975b01670 (patch) | |
| tree | 7cb10a22d54fa41c535f96299c76e06bae6953a8 /float_test8.bpl | |
| parent | a3b2bfa16f991f4d5f844b6d18e836e57b4195a1 (diff) | |
Special fp types (such as infinity and NaN are now translated by boogie
Diffstat (limited to 'float_test8.bpl')
| -rw-r--r-- | float_test8.bpl | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/float_test8.bpl b/float_test8.bpl index 32fb8863..554dcf00 100644 --- a/float_test8.bpl +++ b/float_test8.bpl @@ -1,5 +1,3 @@ procedure F() returns () { - var x : float; - x := fp(0.1) + fp(0.1); - assert x == fp(0.2); + assert fp(-oo)==fp(-oo); }
\ No newline at end of file |