diff --git a/src/ast/macros/quasi_macros.h b/src/ast/macros/quasi_macros.h
index 9c371bea9..b5681e8a6 100644
--- a/src/ast/macros/quasi_macros.h
+++ b/src/ast/macros/quasi_macros.h
@@ -65,7 +65,6 @@ public:
     /**
        \brief Find pure function macros and apply them.
     */
-    // bool operator()(unsigned n, expr * const * exprs, proof * const * prs, expr_ref_vector & new_exprs, proof_ref_vector & new_prs);    
     bool operator()(unsigned n, justified_expr const* fmls, vector<justified_expr>& new_fmls);
     bool operator()(expr_ref_vector & exprs, proof_ref_vector & prs, expr_dependency_ref_vector & deps);
 
diff --git a/src/util/mpq.h b/src/util/mpq.h
index f6554a640..4cc15229f 100644
--- a/src/util/mpq.h
+++ b/src/util/mpq.h
@@ -136,10 +136,17 @@ public:
 
     void del(mpz & a) { mpz_manager<SYNCH>::del(a); }
 
+
     void del(mpq & a) {
         del(a.m_num);
         del(a.m_den);
     }
+
+    static void del(mpq_manager* m, mpq & a) {
+        mpz_manager<SYNCH>::del(m, a.m_num);
+        mpz_manager<SYNCH>::del(m, a.m_den);
+    }
+
     
     void get_numerator(mpq const & a, mpz & n) { set(n, a.m_num); }
 
diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index 30372ab6b..a6b05a877 100644
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -230,9 +230,10 @@ mpz_manager<SYNCH>::sign_cell::sign_cell(mpz_manager& m, mpz const& a):
 
 
 template<bool SYNCH>
-void mpz_manager<SYNCH>::del(mpz & a) { 
+void mpz_manager<SYNCH>::del(mpz_manager<SYNCH>* m, mpz & a) { 
     if (a.m_ptr) {
-        deallocate(a.m_owner == mpz_self, a.m_ptr); 
+        SASSERT(m);
+        m->deallocate(a.m_owner == mpz_self, a.m_ptr); 
         a.m_ptr = nullptr;
         a.m_kind = mpz_small;
         a.m_owner = mpz_self;
diff --git a/src/util/mpz.h b/src/util/mpz.h
index 87a9f0b5b..d11abb2dd 100644
--- a/src/util/mpz.h
+++ b/src/util/mpz.h
@@ -401,7 +401,9 @@ public:
 
     static mpz mk_z(int val) { return mpz(val); }
     
-    void del(mpz & a);
+    void del(mpz & a) { del(this, a); }
+
+    static void del(mpz_manager* m, mpz & a);
     
     void add(mpz const & a, mpz const & b, mpz & c);
 
diff --git a/src/util/rational.h b/src/util/rational.h
index 0c5c6b9e2..d078b62ef 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -63,7 +63,7 @@ public:
     struct ui64 {};
     rational(uint64_t i, ui64) { m().set(m_val, i); }
     
-    ~rational() { m().del(m_val); }
+    ~rational() { synch_mpq_manager::del(g_mpq_manager, m_val); }
     
     mpq const & to_mpq() const { return m_val; }