diff --git a/src/util/mpf.h b/src/util/mpf.h
index fb5f2a0221f..466d23ea53f 100644
--- a/src/util/mpf.h
+++ b/src/util/mpf.h
@@ -88,6 +88,8 @@ class mpf_manager {
 
     void neg(mpf & o);
     void neg(mpf const & x, mpf & o);
+    
+    void swap(mpf& a, mpf& b) { a.swap(b); }
 
     bool is_zero(mpf const & x);
     bool is_neg(mpf const & x);
diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index 736b401b8bb..d3e9941d3c5 100644
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -76,6 +76,13 @@ static uint64_t _trailing_zeros64(uint64_t x) {
 }
 #endif
 
+unsigned trailing_zeros(uint32_t x) {
+    return static_cast<unsigned>(_trailing_zeros32(x));
+}
+
+unsigned trailing_zeros(uint64_t x) {
+    return static_cast<unsigned>(_trailing_zeros64(x));
+}
 
 #define _bit_min(x, y) (y + ((x - y) & ((int)(x - y) >> 31)))
 #define _bit_max(x, y) (x - ((x - y) & ((int)(x - y) >> 31)))
diff --git a/src/util/mpz.h b/src/util/mpz.h
index f3c3b19b9cd..1a7b6f55e5a 100644
--- a/src/util/mpz.h
+++ b/src/util/mpz.h
@@ -29,6 +29,9 @@ Revision History:
 
 unsigned u_gcd(unsigned u, unsigned v);
 uint64_t u64_gcd(uint64_t u, uint64_t v);
+unsigned trailing_zeros(uint64_t);
+unsigned trailing_zeros(uint32_t);
+
 
 #ifdef _MP_GMP
 typedef unsigned digit_t;
diff --git a/src/util/rational.cpp b/src/util/rational.cpp
index bb443935a75..af3c89ced3c 100644
--- a/src/util/rational.cpp
+++ b/src/util/rational.cpp
@@ -130,7 +130,7 @@ bool rational::limit_denominator(rational &num, rational const& limit) {
     return false;
 }
 
-bool rational::mult_inverse(unsigned num_bits, rational & result) {
+bool rational::mult_inverse(unsigned num_bits, rational & result) const {
     rational const& n = *this;
     if (n.is_one()) {
         result = n;
diff --git a/src/util/rational.h b/src/util/rational.h
index f28a502ef25..cffd0083c52 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -157,6 +157,12 @@ class rational {
     friend inline rational numerator(rational const & r) { rational result; m().get_numerator(r.m_val, result.m_val); return result; }
     
     friend inline rational denominator(rational const & r) { rational result; m().get_denominator(r.m_val, result.m_val); return result; }
+
+    friend inline rational inv(rational const & r) {
+        rational result;
+        m().inv(r.m_val, result.m_val);
+        return result;
+    }
     
     rational & operator+=(rational const & r) { 
         m().add(m_val, r.m_val, m_val);
@@ -346,8 +352,13 @@ class rational {
     bool is_power_of_two(unsigned & shift) const {
         return m().is_power_of_two(m_val, shift);
     }
+    
+    bool is_power_of_two() const {
+        unsigned shift = 0;
+        return m().is_power_of_two(m_val, shift);
+    }
 
-    bool mult_inverse(unsigned num_bits, rational & result);
+    bool mult_inverse(unsigned num_bits, rational & result) const;
 
     static rational const & zero() {
         return m_zero;
diff --git a/src/util/scoped_numeral.h b/src/util/scoped_numeral.h
index 3b35a1bd8d8..65b75053d68 100644
--- a/src/util/scoped_numeral.h
+++ b/src/util/scoped_numeral.h
@@ -61,11 +61,11 @@ class _scoped_numeral {
     }
 
     void swap(_scoped_numeral & n) {
-        m_num.swap(n.m_num);
+        m().swap(m_num, n.m_num);
     }
 
     void swap(numeral & n) {
-        m_num.swap(n);
+        m().swap(m_num, n);
     }
 
     _scoped_numeral & operator+=(numeral const & a) {