diff --git a/src/test/rational.cpp b/src/test/rational.cpp
index 711958de5..8fe565c62 100644
--- a/src/test/rational.cpp
+++ b/src/test/rational.cpp
@@ -466,6 +466,28 @@ static void tst12() {
         std::cout << i << ": " << r.get_bit(i) << "\n";
 }
 
+static void tst13() {
+    std::cout << "test13\n";
+    rational const step = rational(1) / rational(3);
+    for (rational r; r < 5000; r += step) {
+        {
+            unsigned k = r.prev_power_of_two();
+            if (r >= 1) {
+                VERIFY(rational::power_of_two(k) <= r);
+                VERIFY(r < rational::power_of_two(k + 1));
+            }
+            else {
+                VERIFY_EQ(k, 0);
+            }
+        }
+        {
+            unsigned k = r.next_power_of_two();
+            VERIFY(r <= rational::power_of_two(k));
+            VERIFY(k == 0 || rational::power_of_two(k - 1) < r);
+        }
+    }
+}
+
 
 void tst_rational() {
     TRACE("rational", tout << "starting rational test...\n";);
@@ -492,4 +514,5 @@ void tst_rational() {
     tst10(true);
     tst10(false);
     tst12();
+    tst13();
 }
diff --git a/src/util/mpq.cpp b/src/util/mpq.cpp
index 324750cfa..f90843e36 100644
--- a/src/util/mpq.cpp
+++ b/src/util/mpq.cpp
@@ -316,6 +316,12 @@ unsigned mpq_manager<SYNCH>::prev_power_of_two(mpq const & a) {
     return prev_power_of_two(_tmp);
 }
 
+template<bool SYNCH>
+unsigned mpq_manager<SYNCH>::next_power_of_two(mpq const & a) {
+    _scoped_numeral<mpz_manager<SYNCH> > _tmp(*this);
+    ceil(a, _tmp);
+    return next_power_of_two(_tmp);
+}
 
 template<bool SYNCH>
 template<bool SUB>
diff --git a/src/util/mpq.h b/src/util/mpq.h
index e254ade69..1bdf8f31b 100644
--- a/src/util/mpq.h
+++ b/src/util/mpq.h
@@ -848,6 +848,14 @@ public:
     unsigned prev_power_of_two(mpz const & a) { return mpz_manager<SYNCH>::prev_power_of_two(a); }
     unsigned prev_power_of_two(mpq const & a);
 
+    /**
+       \brief Return the smallest k s.t. a <= 2^k.
+
+       \remark Return 0 if a is not positive.
+    */
+    unsigned next_power_of_two(mpz const & a) { return mpz_manager<SYNCH>::next_power_of_two(a); }
+    unsigned next_power_of_two(mpq const & a);
+
     bool is_int_perfect_square(mpq const & a, mpq & r) {
         SASSERT(is_int(a));
         reset_denominator(r);
diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index c3ba30161..296b4426e 100644
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -2288,6 +2288,19 @@ unsigned mpz_manager<SYNCH>::bitsize(mpz const & a) {
         return mlog2(a) + 1;
 }
 
+template<bool SYNCH>
+unsigned mpz_manager<SYNCH>::next_power_of_two(mpz const & a) {
+    if (is_nonpos(a))
+        return 0;
+    if (is_one(a))
+        return 0;
+    unsigned shift;
+    if (is_power_of_two(a, shift))
+        return shift;
+    else
+        return log2(a) + 1;
+}
+
 template<bool SYNCH>
 bool mpz_manager<SYNCH>::is_perfect_square(mpz const & a, mpz & root) {
     if (is_neg(a))
diff --git a/src/util/mpz.h b/src/util/mpz.h
index a1bb19395..bb1141ea7 100644
--- a/src/util/mpz.h
+++ b/src/util/mpz.h
@@ -692,6 +692,13 @@ public:
        \remark Return 0 if a is not positive.
     */
     unsigned prev_power_of_two(mpz const & a) { return log2(a); }
+
+    /**
+       \brief Return the smallest k s.t. a <= 2^k.
+
+       \remark Return 0 if a is not positive.
+    */
+    unsigned next_power_of_two(mpz const & a);
     
     /**
        \brief Return true if a^{1/n} is an integer, and store the result in a.
diff --git a/src/util/rational.h b/src/util/rational.h
index 26b93e8c5..b58d9bbb1 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -489,6 +489,18 @@ public:
         return get_num_digits(rational(10));
     }
 
+    /**
+     * \brief Return the biggest k s.t. 2^k <= a.
+     * \remark Return 0 if a is not positive.
+     */
+    unsigned prev_power_of_two() const { return m().prev_power_of_two(m_val); }
+
+    /**
+     * \brief Return the smallest k s.t. a <= 2^k.
+     * \remark Return 0 if a is not positive.
+     */
+    unsigned next_power_of_two() const { return m().next_power_of_two(m_val); }
+
     bool get_bit(unsigned index) const {
         return m().get_bit(m_val, index);
     }