mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 05:11:21 +00:00
Code Activity

fpa_rewriter: remove a mpq copy

Browse source
This commit is contained in:
Nuno Lopes 2017-10-13 01:00:10 +01:00
parent 3cc6dd1cbd
commit b53d69be18
1 changed files with 3 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/ast/rewriter/fpa_rewriter.cpp
View file

@ -125,11 +125,10 @@ br_status fpa_rewriter::mk_to_fp(func_decl * f, unsigned num_args, expr * const
const mpz & sm1 = m_fm.m_powers2(sbits - 1); const mpz & sm1 = m_fm.m_powers2(sbits - 1);
const mpz & em1 = m_fm.m_powers2(ebits); const mpz & em1 = m_fm.m_powers2(ebits);
scoped_mpq q(mpqm); const mpq & q = r1.to_mpq();
mpqm.set(q, r1.to_mpq()); SASSERT(mpzm.is_one(q.denominator()));
SASSERT(mpzm.is_one(q.get().denominator()));
scoped_mpz z(mpzm); scoped_mpz z(mpzm);
z = q.get().numerator(); z = q.numerator();
mpzm.rem(z, sm1, sig); mpzm.rem(z, sm1, sig);
mpzm.div(z, sm1, z); mpzm.div(z, sm1, z);