diff --git a/src/sat/smt/polysat/fixed_bits.cpp b/src/sat/smt/polysat/fixed_bits.cpp
index 4fce10ad4..698a647a0 100644
--- a/src/sat/smt/polysat/fixed_bits.cpp
+++ b/src/sat/smt/polysat/fixed_bits.cpp
@@ -41,8 +41,8 @@ namespace polysat {
                 SASSERT(s.offset + s.length <= sz);
                 rational hi_val = s.value;
                 rational lo_val = mod(s.value + 1, sbw);                
-                pdd lo = c.value(rational::power_of_two(sz - s.offset - s.length) * lo_val, sz);
-                pdd hi = c.value(rational::power_of_two(sz - s.offset - s.length) * hi_val, sz);
+                pdd lo = c.value(rational::power_of_two(sz - s.length) * lo_val, sz);
+                pdd hi = c.value(rational::power_of_two(sz - s.length) * hi_val, sz);
                 fi.reset();
                 fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val);
                 fi.deps.push_back(dependency({ m_var, s }));
@@ -54,6 +54,7 @@ namespace polysat {
             // slice, properly contains variable.
             // s.offset refers to offset in containing value.
             if (s.length > sz && mod(machine_div2k(s.value, s.offset), bw) != val) {
+                
                 rational hi_val = mod(machine_div2k(s.value, s.offset), bw);
                 rational lo_val = mod(hi_val + 1, bw);
                 pdd lo = c.value(lo_val, sz);
diff --git a/src/sat/smt/polysat_internalize.cpp b/src/sat/smt/polysat_internalize.cpp
index 5acae56ce..eae10cd9e 100644
--- a/src/sat/smt/polysat_internalize.cpp
+++ b/src/sat/smt/polysat_internalize.cpp
@@ -655,6 +655,7 @@ namespace polysat {
     }
 
     void solver::internalize_extract(app* e) {
+        ensure_pdd_var(e->get_arg(0));
         m_delayed_axioms.push_back(e);
         ctx.push(push_back_vector(m_delayed_axioms));
         var2pdd(expr2enode(e)->get_th_var(get_id()));
@@ -696,8 +697,33 @@ namespace polysat {
         }
     }
 
+    void solver::ensure_pdd_var(expr* e) {
+        auto n = expr2enode(e);
+        auto v = n->get_th_var(get_id());
+        auto q = var2pdd(v);
+        if (q.is_val() || q.is_var())
+            return;
+        unsigned bv_size = get_bv_size(v);
+        pvar pv = m_core.add_var(bv_size);
+        pdd p = m_core.var(pv);
+        ctx.push(vector_value_trail(m_var2pdd, v));
+        m_pddvar2var.setx(pv, v, UINT_MAX);
+        m_var2pdd[v] = p;
+        auto sc = m_core.eq(p, q);
+        dependency d = dependency::axiom();
+        auto idx = m_core.register_constraint(sc, d);
+        TRACE("bv", tout << "add definition for " << mk_pp(e, m) << " " << p << ": " << sc << "\n";);
+        m_core.assign_eh(idx, false);
+    }
+
+    //
+    // subterms under concatentation and extract need to be variables or constants such that 
+    // viable can perform proper slices.
+    //
     void solver::internalize_concat(app* e) {
         SASSERT(bv.is_concat(e));
+        for (auto arg : *e)
+            ensure_pdd_var(arg);        
         m_delayed_axioms.push_back(e);
         ctx.push(push_back_vector(m_delayed_axioms));
         var2pdd(expr2enode(e)->get_th_var(get_id()));
diff --git a/src/sat/smt/polysat_solver.h b/src/sat/smt/polysat_solver.h
index 1ece260a6..837cea15a 100644
--- a/src/sat/smt/polysat_solver.h
+++ b/src/sat/smt/polysat_solver.h
@@ -195,6 +195,7 @@ namespace polysat {
         void assert_bv2int_axiom(app * n);
         void assert_int2bv_axiom(app* n);
 
+        void ensure_pdd_var(expr* e);
         pdd expr2pdd(expr* e);
         pdd var2pdd(euf::theory_var v);
         void internalize_set(expr* e, pdd const& p);