diff --git a/src/sat/smt/polysat/fixed_bits.cpp b/src/sat/smt/polysat/fixed_bits.cpp
index 6b9f95811..3c745e315 100644
--- a/src/sat/smt/polysat/fixed_bits.cpp
+++ b/src/sat/smt/polysat/fixed_bits.cpp
@@ -36,7 +36,6 @@ namespace polysat {
     // 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);
@@ -49,22 +48,22 @@ namespace polysat {
                 SASSERT(s.offset + s.length <= 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);
+                pdd lo = c.value(rational::power_of_two(sz - s.length) * (s.value + 1), sz);
+                pdd hi = c.value(rational::power_of_two(sz - s.length) * 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));
+                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 = bw;
                 fi.coeff = 1;
-                // verbose_stream() << "fixed bits sub: v" << m_var << " value " << val << " "  << fi << "\n";
+                // verbose_stream() << "fixed bits sub: v" << m_var << " " << sz << " value " << val << " "  << fi << "\n";
                 return false;
             }
             // 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) {
+            if (false && 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);
diff --git a/src/sat/smt/polysat/ule_constraint.cpp b/src/sat/smt/polysat/ule_constraint.cpp
index 22171b742..806f823fb 100644
--- a/src/sat/smt/polysat/ule_constraint.cpp
+++ b/src/sat/smt/polysat/ule_constraint.cpp
@@ -323,6 +323,7 @@ namespace polysat {
     // Evaluate lhs <= rhs
     lbool ule_constraint::eval(pdd const& lhs, pdd const& rhs) {
         // NOTE: don't assume simplifications here because we also call this on partially substituted constraints
+
         if (lhs.is_zero())
             return l_true;      // 0 <= p
         if (lhs == rhs)
diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp
index a98d7e702..0ffc19a72 100644
--- a/src/sat/smt/polysat/viable.cpp
+++ b/src/sat/smt/polysat/viable.cpp
@@ -655,6 +655,7 @@ namespace polysat {
             
             // a < x <= b <=>
             // a + 1 <= x < b + 1
+            // x - a - 1 < b - a
 
             auto vlo = c.value(mod((e.value - 1) * p2eb + 1, p2b), bw);
             auto vhi = c.value(mod(e.value * p2eb + 1, p2b), bw);
@@ -666,6 +667,7 @@ namespace polysat {
             verbose_stream() << "before bw " << ebw << " " << bw << " " << *e.e << "\nafter  bw " << abw << " " << aw << " " << *after.e << "\n";
             if (!t.is_val())
                 IF_VERBOSE(0, verbose_stream() << "symbolic t : " << t << "\n");
+            verbose_stream() << t - vlo << " " << vhi - vlo << "\n";
 
 #endif
             auto sc = cs.ult(t - vlo, vhi - vlo);
@@ -676,6 +678,7 @@ namespace polysat {
                 deps.push_back(c.propagate(sc, c.explain_weak_eval(sc)));
             t.reset(lo.manager());
             t = c.value(mod(e.value, rational::power_of_two(aw)), aw);
+            // verbose_stream() << "after " << t << "\n";
         }
 
         if (abw < aw)