diff --git a/src/math/polysat/constraint_manager.cpp b/src/math/polysat/constraint_manager.cpp
index 124257e99..411ba5bd0 100644
--- a/src/math/polysat/constraint_manager.cpp
+++ b/src/math/polysat/constraint_manager.cpp
@@ -640,14 +640,16 @@ namespace polysat {
         return s.var(v);
     }
 
-    pdd constraint_manager::zero_ext(pdd const& p, unsigned bit_width) {
-        SASSERT(bit_width > p.power_of_2());
+    pdd constraint_manager::zero_ext(pdd const& p, unsigned extra_bits) {
+        SASSERT(extra_bits > 0);
+        unsigned const p_sz = p.power_of_2();
+        unsigned const v_sz = p_sz + extra_bits;
         pdd const q = s.var(s.m_names.mk_name(p));
-        constraint_dedup::bv_ext_args const args = {false, q.var(), bit_width};
+        constraint_dedup::bv_ext_args const args = {false, q.var(), extra_bits};
         auto const it = m_dedup.m_bv_ext_expr.find_iterator(args);
         if (it != m_dedup.m_bv_ext_expr.end())
             return s.var(it->m_value);
-        pdd const v = s.var(s.add_var(bit_width));
+        pdd const v = s.var(s.add_var(v_sz));
         m_dedup.m_bv_ext_expr.insert(args, v.var());
         // (1)  v[|p|-1:0] = p
         s.add_eq(q, extract(v, p.power_of_2() - 1, 0));
@@ -656,20 +658,21 @@ namespace polysat {
         return v;
     }
 
-    pdd constraint_manager::sign_ext(pdd const& p, unsigned bit_width) {
+    pdd constraint_manager::sign_ext(pdd const& p, unsigned extra_bits) {
+        SASSERT(extra_bits > 0);
         unsigned const p_sz = p. power_of_2();
-        SASSERT(bit_width > p_sz);
+        unsigned const v_sz = p_sz + extra_bits;
         pdd const q = s.var(s.m_names.mk_name(p));
-        constraint_dedup::bv_ext_args const args = {true, q.var(), bit_width};
+        constraint_dedup::bv_ext_args const args = {true, q.var(), extra_bits};
         auto const it = m_dedup.m_bv_ext_expr.find_iterator(args);
         if (it != m_dedup.m_bv_ext_expr.end())
             return s.var(it->m_value);
-        pdd const v = s.var(s.add_var(bit_width));
+        pdd const v = s.var(s.add_var(v_sz));
         m_dedup.m_bv_ext_expr.insert(args, v.var());
         // (1)  v[|p|-1:0] = p
         s.add_eq(q, extract(v, p_sz - 1, 0));
-        // (2)  Let h := v[bit_width-1:|p|]
-        pdd const h = extract(v, bit_width - 1, p_sz);
+        // (2)  Let h := v[|v|-1:|p|]
+        pdd const h = extract(v, v_sz - 1, p_sz);
         signed_constraint p_negative = s.uge(p, rational::power_of_two(p_sz - 1));
         // (3)  p < 2^(|p|-1)   ==>  h = 0
         s.add_clause(p_negative, s.eq(h), false);
diff --git a/src/math/polysat/constraint_manager.h b/src/math/polysat/constraint_manager.h
index 0ba7987ca..84695c710 100644
--- a/src/math/polysat/constraint_manager.h
+++ b/src/math/polysat/constraint_manager.h
@@ -172,8 +172,8 @@ namespace polysat {
         pdd concat(pdd const& p, pdd const& q);
         pdd concat(unsigned num_args, pdd const* args);
 
-        pdd zero_ext(pdd const& p, unsigned bit_width);
-        pdd sign_ext(pdd const& p, unsigned bit_width);
+        pdd zero_ext(pdd const& p, unsigned extra_bits);
+        pdd sign_ext(pdd const& p, unsigned extra_bits);
 
         constraint* const* begin() const { return m_constraints.data(); }
         constraint* const* end() const { return m_constraints.data() + m_constraints.size(); }
diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h
index 7dce13f19..e11af346f 100644
--- a/src/math/polysat/solver.h
+++ b/src/math/polysat/solver.h
@@ -419,10 +419,10 @@ namespace polysat {
         pdd concat(unsigned num_args, pdd const* args) { return m_constraints.concat(num_args, args); }
 
         /** Create expression for zero-extension of p */
-        pdd zero_ext(pdd const& p, unsigned bit_width) { return m_constraints.zero_ext(p, bit_width); }
+        pdd zero_ext(pdd const& p, unsigned extra_bits) { return m_constraints.zero_ext(p, extra_bits); }
 
         /** Create expression for signed-extension of p */
-        pdd sign_ext(pdd const& p, unsigned bit_width) { return m_constraints.sign_ext(p, bit_width); }
+        pdd sign_ext(pdd const& p, unsigned extra_bits) { return m_constraints.sign_ext(p, extra_bits); }
 
         /**
         * Create terms for unsigned quot-rem
diff --git a/src/sat/smt/bv_polysat.cpp b/src/sat/smt/bv_polysat.cpp
index 40d5bf0f3..83ea239fa 100644
--- a/src/sat/smt/bv_polysat.cpp
+++ b/src/sat/smt/bv_polysat.cpp
@@ -89,10 +89,10 @@ namespace bv {
         case OP_BSREM0:           break;
         case OP_BUREM0:           break;
         case OP_BSMOD0:           break;
+        // TODO: what about those naked breaks above? is this handled elsewhere?
 
         case OP_EXTRACT:          polysat_extract(a); break;
         case OP_CONCAT:           polysat_concat(a); break;
-
         case OP_ZERO_EXT:         polysat_par_unary(a, [&](pdd const& p, unsigned sz) { return m_polysat.zero_ext(p, sz); }); break;
         case OP_SIGN_EXT:         polysat_par_unary(a, [&](pdd const& p, unsigned sz) { return m_polysat.sign_ext(p, sz); }); break;
 
@@ -199,8 +199,8 @@ namespace bv {
 
     void solver::polysat_par_unary(app* e, std::function<polysat::pdd(polysat::pdd,unsigned)> const& fn) {
         pdd const p = expr2pdd(e->get_arg(0));
-        unsigned const sz = e->get_parameter(0).get_int();
-        polysat_set(e, fn(p, sz));
+        unsigned const par = e->get_parameter(0).get_int();
+        polysat_set(e, fn(p, par));
     }
 
     void solver::polysat_binary(app* e, std::function<polysat::pdd(polysat::pdd, polysat::pdd)> const& fn) {