diff --git a/src/util/mpq.h b/src/util/mpq.h
index 093cc0a44..474d38802 100644
--- a/src/util/mpq.h
+++ b/src/util/mpq.h
@@ -34,6 +34,8 @@ public:
     void swap(mpq & other) { m_num.swap(other.m_num); m_den.swap(other.m_den); }
     mpz const & numerator() const { return m_num; }
     mpz const & denominator() const { return m_den; }
+
+    double get_double() const;
 };
 
 inline void swap(mpq & m1, mpq & m2) { m1.swap(m2); }
@@ -833,9 +835,11 @@ public:
     }
 
     bool is_even(mpz const & a) { return mpz_manager<SYNCH>::is_even(a); }
-
+public:
     bool is_even(mpq const & a) { return is_int(a) && is_even(a.m_num); }
 
+    friend bool operator==(mpq const & a, mpq const & b) ;
+    friend bool operator>=(mpq const & a, mpq const & b);
 };
 
 typedef mpq_manager<true> synch_mpq_manager;
diff --git a/src/util/mpz.h b/src/util/mpz.h
index 9cb27ebff..2661cb5da 100644
--- a/src/util/mpz.h
+++ b/src/util/mpz.h
@@ -593,6 +593,15 @@ public:
         }
     }
 
+    bool lt(mpz const& a, int b) {
+        if (is_small(a)) {
+            return a.m_val < b;
+        }
+        else {
+            return lt(a, mpz(b));
+        }
+    }
+
     bool lt(mpz const & a, mpz const & b) {
         if (is_small(a) && is_small(b)) {
             return a.m_val < b.m_val;