CBMC 5.3 and prior: bug in encoding of floating-point division

Skip to first unread message

Daniel Kroening

Feb 17, 2016, 9:19:20 AM2/17/16
to cpr...@googlegroups.com
Dear everyone,

as part of our routine QA process we have found an issue with our model
of floating-point divide. In a few cases where very large numbers are
divided by very small (subnormal) numbers, zero is returned rather than
infinity. Given that the range of numbers required to trigger this
issue we do not believe that it will have a major impact on users but
please contact us if this is an issue for you. The patch has been
applied to the subversion trunk and will be in the next release.

With best regards,

Reply all
Reply to author
0 new messages