3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00

MPF consistency fix

Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2015-01-01 15:23:27 +00:00
parent 4f453703f7
commit 97df505dba

View file

@ -336,7 +336,7 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode
TRACE("mpf_dbg", tout << "set: res = " << to_string(o) << std::endl;);
}
void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, bool sign, uint64 significand, int exponent) {
void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, bool sign, uint64 significand, mpf_exp_t exponent) {
// Assumption: this represents (sign * -1) * (significand/2^sbits) * 2^exponent.
o.ebits = ebits;
o.sbits = sbits;