diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index a0b6b592f..33b755a52 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -436,12 +436,12 @@ namespace polysat {
 
     template<bool FORWARD>
     bool viable::refine_bits(pvar v, rational const& val, fixed_bits_info const& fbi) {
-
-        pdd v_pdd = s.var(v);
+        pdd_manager& m = s.var2pdd(v);
+        unsigned const k = s.size(v);
 
         // TODO: We might also extend simultaneously up and downwards if we want the actual interval (however, this might make use of more fixed bits and is weaker - worse - therefore)
         entry* ne = alloc_entry();
-        rational new_val = extend_by_bits<FORWARD>(v_pdd, val, fbi, ne->src, ne->side_cond);
+        rational new_val = extend_by_bits<FORWARD>(k, val, fbi, ne->src, ne->side_cond);
 
         if (new_val == val) {
             m_alloc.push_back(ne);
@@ -450,18 +450,18 @@ namespace polysat {
 
         // TODO: Extend in both directions? (Less justifications vs. bigger intervals)
         // TODO: could also try to extend backwards as much as we can without introducing new justifications?
-        rational new_val2 = extend_by_bits<!FORWARD>(v_pdd, val, fbi, ne->src, ne->side_cond);
+        rational new_val2 = extend_by_bits<!FORWARD>(k, val, fbi, ne->src, ne->side_cond);
 
         ne->refined = true;
         ne->coeff = 1;
         ne->bit_width = s.size(v);
         if (FORWARD) {
             LOG("refine-bits FORWARD for v" << v << " = " << val << " to [" << new_val2 << ", " << new_val << "[");
-            ne->interval = eval_interval::proper(v_pdd.manager().mk_val(new_val2), new_val2, v_pdd.manager().mk_val(new_val), new_val);
+            ne->interval = eval_interval::proper(m.mk_val(new_val2), new_val2, m.mk_val(new_val), new_val);
         }
         else {
             LOG("refine-bits BACKWARD for v" << v << " = " << val << " to [" << new_val << ", " << new_val2 << "[");
-            ne->interval = eval_interval::proper(v_pdd.manager().mk_val(new_val), new_val, v_pdd.manager().mk_val(new_val2), new_val2);
+            ne->interval = eval_interval::proper(m.mk_val(new_val), new_val, m.mk_val(new_val2), new_val2);
         }
         SASSERT(ne->interval.currently_contains(val));
         intersect(v, ne);
@@ -713,15 +713,10 @@ namespace polysat {
     }
 
     // Skips all values that are not feasible w.r.t. fixed bits
-    template<bool FORWARD>
-    rational viable::extend_by_bits(pdd const& var, rational const& bound, fixed_bits_info const& fbi, vector<signed_constraint>& src, vector<signed_constraint>& side_cond) const {
-        unsigned const k = var.power_of_2();
-        if (fbi.is_empty())  // TODO: this check doesn't do anything.
-            return bound;
-
+    template <bool FORWARD>
+    rational viable::extend_by_bits(unsigned k, rational const& bound, fixed_bits_info const& fbi, vector<signed_constraint>& src, vector<signed_constraint>& side_cond) const {
         svector<lbool> const& fixed = fbi.fixed;
-
-        SASSERT(k == fixed.size());
+        SASSERT(k <= fixed.size());
 
         sat::literal_set added_src;
         sat::literal_set added_side_cond;
diff --git a/src/math/polysat/viable.h b/src/math/polysat/viable.h
index cf23546d2..8d1679148 100644
--- a/src/math/polysat/viable.h
+++ b/src/math/polysat/viable.h
@@ -167,7 +167,7 @@ namespace polysat {
         bool refine_disequal_lin(pvar v, rational const& val);
 
         template<bool FORWARD>
-        rational extend_by_bits(pdd const& var, rational const& bounds, fixed_bits_info const& fbi, vector<signed_constraint>& out_src, vector<signed_constraint>& out_side_cond) const;
+        rational extend_by_bits(unsigned num_bits, rational const& bounds, fixed_bits_info const& fbi, vector<signed_constraint>& out_src, vector<signed_constraint>& out_side_cond) const;
 
         bool collect_bit_information(pvar v, bool add_conflict, fixed_bits_info& out_fbi);