projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 16ade2e) | patch
Update to symfpu 0.0.7, fixes RTI 3/5 issue (#3007)
authorMartin <martin.brain@cs.ox.ac.uk>
Tue, 21 May 2019 17:49:37 +0000 (18:49 +0100)
committerAndres Noetzli <andres.noetzli@gmail.com>
Tue, 21 May 2019 17:49:37 +0000 (10:49 -0700)
commit1c1c178db1755a441792d84465dcb8397f1f2011
tree3c9f0d90bf2aabb0bab790767ad5de5170e985e2tree
parent16ade2e20b6fd2afc49b8ea70d128ae665dff409commit | diff
Update to symfpu 0.0.7, fixes RTI 3/5 issue (#3007)

Fixes #2932. fp.roundToIntegral was rounding some very small subnormals up to
between 1 and 2, which is A. wrong and B. not idempotent.  The
corresponding symfpu update fixes this as it was an overflow caused
by the unpacked significand not being able to represent an extra
significand bits.
contrib/get-symfpu diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/fp/rti_3_5_bug.smt2 [new file with mode: 0644] blob
test/regress/regress0/fp/rti_3_5_bug_report.smt2 [new file with mode: 0644] blob