From 009708ed07c487f6ec031f6f4d47ad00fa459b80 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Mon, 9 Jul 2018 10:52:27 +0100
Subject: [PATCH] remove unneeded creation of tmp mpz_manager

---
 src/math/polynomial/algebraic_numbers.cpp | 20 ++++++++------------
 src/util/mpq.h                            |  6 ++++++
 2 files changed, 14 insertions(+), 12 deletions(-)

diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp
index 5811811fc..aa4fc5a39 100644
--- a/src/math/polynomial/algebraic_numbers.cpp
+++ b/src/math/polynomial/algebraic_numbers.cpp
@@ -2629,17 +2629,15 @@ namespace algebraic_numbers {
             }
             else if (a.is_basic()) {
                 mpq const & v = basic_value(a);
-                scoped_mpz neg_n(qm());
+                mpz neg_n;
                 qm().set(neg_n, v.numerator());
                 qm().neg(neg_n);
-                unsynch_mpz_manager zmgr;
-                // FIXME: remove these copies
-                mpz coeffs[2] = { zmgr.dup(neg_n.get()), zmgr.dup(v.denominator()) };
+                mpz coeffs[2] = { std::move(neg_n), qm().dup(v.denominator()) };
                 out << "(";
                 upm().display(out, 2, coeffs, "#");
                 out << ", 1)"; // first root of the polynomial d*# - n
-                zmgr.del(coeffs[0]);
-                zmgr.del(coeffs[1]);
+                qm().del(coeffs[0]);
+                qm().del(coeffs[1]);
             }
             else {
                 algebraic_cell * c = a.to_algebraic();
@@ -2679,17 +2677,15 @@ namespace algebraic_numbers {
             }
             else if (a.is_basic()) {
                 mpq const & v = basic_value(a);
-                scoped_mpz neg_n(qm());
+                mpz neg_n;
                 qm().set(neg_n, v.numerator());
                 qm().neg(neg_n);
-                unsynch_mpz_manager zmgr;
-                // FIXME: remove these copies
-                mpz coeffs[2] = { zmgr.dup(neg_n.get()), zmgr.dup(v.denominator()) };
+                mpz coeffs[2] = { std::move(neg_n), qm().dup(v.denominator()) };
                 out << "(root-obj ";
                 upm().display_smt2(out, 2, coeffs, "x");
                 out << " 1)"; // first root of the polynomial d*# - n
-                zmgr.del(coeffs[0]);
-                zmgr.del(coeffs[1]);
+                qm().del(coeffs[0]);
+                qm().del(coeffs[1]);
             }
             else {
                 algebraic_cell * c = a.to_algebraic();
diff --git a/src/util/mpq.h b/src/util/mpq.h
index 1bccabc74..b7bdbf400 100644
--- a/src/util/mpq.h
+++ b/src/util/mpq.h
@@ -714,6 +714,12 @@ public:
         return temp;
     }
 
+    mpz dup(const mpz & source) {
+        mpz temp;
+        set(temp, source);
+        return temp;
+    }
+
     void swap(mpz & a, mpz & b) { mpz_manager<SYNCH>::swap(a, b); }
 
     void swap(mpq & a, mpq & b) {