From b53d69be18044ac7bf378dc1b1a61bd4266cfcd1 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Fri, 13 Oct 2017 01:00:10 +0100 Subject: [PATCH] fpa_rewriter: remove a mpq copy --- src/ast/rewriter/fpa_rewriter.cpp | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 818336c75..ce14349b2 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -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 & em1 = m_fm.m_powers2(ebits); - scoped_mpq q(mpqm); - mpqm.set(q, r1.to_mpq()); - SASSERT(mpzm.is_one(q.get().denominator())); + const mpq & q = r1.to_mpq(); + SASSERT(mpzm.is_one(q.denominator())); scoped_mpz z(mpzm); - z = q.get().numerator(); + z = q.numerator(); mpzm.rem(z, sm1, sig); mpzm.div(z, sm1, z);