diff --git a/src/sat/smt/polysat/ule_constraint.cpp b/src/sat/smt/polysat/ule_constraint.cpp
index c0c64ee2a..368dfc720 100644
--- a/src/sat/smt/polysat/ule_constraint.cpp
+++ b/src/sat/smt/polysat/ule_constraint.cpp
@@ -227,7 +227,6 @@ namespace polysat {
             lhs *= x;
             SASSERT(lhs.leading_coefficient().is_power_of_two());
         }
-        TRACE("bv_verbose", tout << "simplified " << lhs << " <= " << rhs << "\n");
     } // simplify_impl
 }
 
@@ -262,6 +261,7 @@ namespace polysat {
         if (old_is_positive != is_positive || old_lhs != lhs || old_rhs != rhs) {
             ule_pp const old_ule(to_lbool(old_is_positive), old_lhs, old_rhs);
             ule_pp const new_ule(to_lbool(is_positive), lhs, rhs);
+            TRACE("bv", tout << "original: " << old_ule << "\nsimplified: " << new_ule << "\n");
             // always-false and always-true constraints should be rewritten to 0 != 0 and 0 == 0, respectively.
             if (is_always_false(old_is_positive, old_lhs, old_rhs)) {
                 SASSERT(!is_positive);
diff --git a/src/sat/smt/polysat/viable.cpp b/src/sat/smt/polysat/viable.cpp
index c4c4c9f10..aba3d1322 100644
--- a/src/sat/smt/polysat/viable.cpp
+++ b/src/sat/smt/polysat/viable.cpp
@@ -648,11 +648,17 @@ namespace polysat {
         verbose_stream() << "\n\n\n\n\n\nNon-viable assignment for v" << m_var << " size " << c.size(m_var) << "\n";
         display_one(verbose_stream() << "entry: ", e) << "\n";
         verbose_stream() << "value " << value << "\n";
+        m_fixed_bits.display(verbose_stream() << "fixed: ") << "\n";
 
         fixed_slice_extra_vector fixed;
         offset_slice_extra_vector subslices;
         c.s.get_fixed_sub_slices(m_var, fixed, subslices);   // TODO: move into m_fixed bits?
 
+        // this case occurs if e-graph merges e.g. nodes "x - 2" and "3";
+        // polysat will see assignment "x = 5" but no fixed bits
+        if (subslices.empty())
+            return null_dependency;
+
         unsigned max_level = 0;
         for (auto const& slice : subslices)
             max_level = std::max(max_level, slice.level);
@@ -681,6 +687,9 @@ namespace polysat {
         unsigned w_level = slice.level;  // level where value of w was fixed
         if (w == m_var)
             return null_dependency;
+        if (w == e->var)
+            return null_dependency;
+
         // verbose_stream() << "v" << m_var << " size " << c.size(m_var) << ", v" << w << " size " << c.size(w) << " offset " << offset << " level " << w_level << "\n";
 
         // Let: