mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

fix #5449

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-08-01 13:03:40 -07:00
parent a4cc9e7895
commit 123c446395
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/util/mpq.cpp
View file

@ -260,6 +260,7 @@ void mpq_manager<SYNCH>::set(mpq & a, char const * val) {
if (exp > 0) { if (exp > 0) {
_scoped_numeral<mpq_manager<SYNCH>> _exp(*this); _scoped_numeral<mpq_manager<SYNCH>> _exp(*this);
_scoped_numeral<mpq_manager<SYNCH>> _qten(*this); _scoped_numeral<mpq_manager<SYNCH>> _qten(*this);
_qten = 10;
power(_qten, static_cast<unsigned>(exp), _exp); power(_qten, static_cast<unsigned>(exp), _exp);
TRACE("mpq_set", tout << "a: " << to_string(a) << ", exp_sign:" << exp_sign << ", exp: " << exp << " " << to_string(_exp) << std::endl;); TRACE("mpq_set", tout << "a: " << to_string(a) << ", exp_sign:" << exp_sign << ", exp: " << exp << " " << to_string(_exp) << std::endl;);
if (exp_sign) if (exp_sign)