projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 114a215) | patch
Fix an incorrect limit in conversion from real to float (#4418)
authorMartin <martin.brain@cs.ox.ac.uk>
Tue, 26 May 2020 18:49:01 +0000 (19:49 +0100)
committerGitHub <noreply@github.com>
Tue, 26 May 2020 18:49:01 +0000 (13:49 -0500)
commitd8b6767e4e5285fef3cf4450b9cba04431e40727
treea752140ddb4ae5985aa5f34c1c24f479d4693977tree
parent114a215e9b33effb361c4b000fb23085ce9f079acommit | diff
Fix an incorrect limit in conversion from real to float (#4418)

This error is a bit inexplicable but very very definitely wrong.
A test case from the original bug report is included.
src/util/floatingpoint.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/fp/issue3619.smt2 [new file with mode: 0644] blob