diff --git a/src/sat/smt/polysat/number.h b/src/sat/smt/polysat/number.h
index 56c66b2f4..0426d2521 100644
--- a/src/sat/smt/polysat/number.h
+++ b/src/sat/smt/polysat/number.h
@@ -27,4 +27,22 @@ namespace polysat {
         return val - mod(val, rational::power_of_two(k));
     }
 
+    /** floor(a / 2^k) for a >= 0 */
+    inline rational div2k_floor(rational const& a, unsigned k)
+    {
+        SASSERT(a >= 0);  // machine_div2k rounds towards 0
+        return machine_div2k(a, k);
+    }
+
+    /** ceil(a / 2^k) for a >= 0 */
+    inline rational div2k_ceil(rational const& a, unsigned k)
+    {
+        // Note: ceil(a/b) == floor((a-1)/b) + 1 for integers a,b and b > 0
+        // Special case for a = 0, because machine_div2k(a, k) does not return floor(a/2^k), but rounds towards 0 instead.
+        if (a.is_zero())
+            return a;
+        SASSERT(a > 0);  // machine_div2k rounds towards 0
+        return machine_div2k(a - 1, k) + 1;
+    }
+
 }
diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp
index fef2fc307..6bb85a16e 100644
--- a/src/sat/smt/polysat/viable.cpp
+++ b/src/sat/smt/polysat/viable.cpp
@@ -1007,22 +1007,6 @@ namespace polysat {
     }
 
 
-    rational div2k_floor(rational const& a, unsigned k)
-    {
-        SASSERT(a >= 0);  // machine_div2k rounds towards 0
-        return machine_div2k(a, k);
-    }
-
-    rational div2k_ceil(rational const& a, unsigned k)
-    {
-        // Note: ceil(a/b) == floor((a-1)/b) + 1 for integers a,b and b > 0
-        // Special case for a = 0, because machine_div2k(a, k) does not return floor(a/2^k), but rounds towards 0 instead.
-        if (a.is_zero())
-            return a;
-        return machine_div2k(a - 1, k) + 1;
-    }
-
-
     /// Let x = concat(y, z) and x not in [lo;hi[.
     /// Returns an interval I such that z not in I.
     r_interval viable::chop_off_upper(r_interval const& i, unsigned const Ny, unsigned const Nz, rational const* y_fixed_value) {