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

disambiguate calls to set

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-04-07 10:16:46 -07:00
parent cfd9785025
commit 4f5133cf72
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/util/hwf.cpp
View file

@ -413,12 +413,12 @@ void hwf_manager::to_rational(hwf const & x, unsynch_mpq_manager & qm, mpq & o)
scoped_mpz n(qm), d(qm); scoped_mpz n(qm), d(qm);
if (is_normal(x)) if (is_normal(x))
qm.set(n, sig(x) | 0x0010000000000000ull); qm.set(n, (uint64)(sig(x) | 0x0010000000000000ull));
else else
qm.set(n, sig(x)); qm.set(n, sig(x));
if (sgn(x)) if (sgn(x))
qm.neg(n); qm.neg(n);
qm.set(d, 0x0010000000000000ull); qm.set(d, (uint64)0x0010000000000000ull);
int e = exp(x); int e = exp(x);
if (e >= 0) if (e >= 0)
qm.mul2k(n, (unsigned)e); qm.mul2k(n, (unsigned)e);