diff --git a/src/sat/smt/polysat/fixed_bits.cpp b/src/sat/smt/polysat/fixed_bits.cpp
index 698a647a0..6b9f95811 100644
--- a/src/sat/smt/polysat/fixed_bits.cpp
+++ b/src/sat/smt/polysat/fixed_bits.cpp
@@ -29,8 +29,15 @@ namespace polysat {
         c.get_fixed_bits(v, m_fixed_slices);
     }
 
-    // if x[hi:lo] = value, then 
-    // 2^(w-hi+1)* x >= 
+    //
+    // If x[hi:lo] = value, then 
+    // let K = w - hi - 1 = w - s.length - s.offset
+    // 2^Kvalue <= 2^Kx < 2^K(value + 1)
+    // 2^Kx not in [2^K(value + 1),  2^Kvalue[
+    // bit-width : w - K = s.offset + s.length
+    //
+    // If y[hi:lo] = value, y[hi':lo'] = x
+    //
     bool fixed_bits::check(rational const& val, fi_record& fi) {
         unsigned sz = c.size(m_var);
         rational bw = rational::power_of_two(sz);
@@ -38,17 +45,21 @@ namespace polysat {
             rational sbw = rational::power_of_two(s.length);
             // slice is properly contained in bit-vector variable
             if (s.length <= sz && s.value != mod(machine_div2k(val, s.offset), sbw)) {
+
                 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.length) * lo_val, sz);
-                pdd hi = c.value(rational::power_of_two(sz - s.length) * hi_val, sz);
+                unsigned bw = s.length + s.offset;
+                unsigned K = sz - bw;
+                pdd lo = c.value(rational::power_of_two(K) * (s.value + 1), sz);
+                pdd hi = c.value(rational::power_of_two(K) * s.value, sz);
+                rational hi_val = rational::power_of_two(s.offset) * s.value;
+                rational lo_val = mod(rational::power_of_two(s.offset) * s.value + 1, rational::power_of_two(bw));
+
                 fi.reset();
                 fi.interval = eval_interval::proper(lo, lo_val, hi, hi_val);
-                fi.deps.push_back(dependency({ m_var, s }));
-                
-                fi.bit_width = s.length;
+                fi.deps.push_back(dependency({ m_var, s }));                
+                fi.bit_width = bw;
                 fi.coeff = 1;
+                // verbose_stream() << "fixed bits sub: v" << m_var << " value " << val << " "  << fi << "\n";
                 return false;
             }
             // slice, properly contains variable.
@@ -64,6 +75,7 @@ namespace polysat {
                 fi.deps.push_back(dependency({ m_var, s }));               
                 fi.bit_width = sz;
                 fi.coeff = 1;
+                verbose_stream() << "fixed bits sup: v" << m_var << " " << fi << "\n";
                 return false;
             }
         }
diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp
index af2830b92..a98d7e702 100644
--- a/src/sat/smt/polysat/viable.cpp
+++ b/src/sat/smt/polysat/viable.cpp
@@ -393,8 +393,13 @@ namespace polysat {
             return true;
         }
         else {
-            intersect(v, e);
-            TRACE("bv", tout << "fixed " << *e << "\n");
+            TRACE("bv", tout << "fixed " << val << " " << *e << "\n");
+            if (!intersect(v, e)) {
+                display(verbose_stream());
+                display_explain(verbose_stream() << "explain\n");
+                SASSERT(false);
+            }
+            
             return false;
         }
     }