diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index f7566250d..b975d83d7 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -598,6 +598,7 @@ namespace polysat {
             ++m_stats.m_num_propagations;
         LOG(assignment_pp(*this, v, val) << " by " << j);
         SASSERT(m_viable.is_viable(v, val));
+        SASSERT(j.is_decision() || j.is_propagation());
         SASSERT(j.level() == m_level);
         SASSERT(!is_assigned(v));
         SASSERT(std::all_of(assignment().begin(), assignment().end(), [v](auto p) { return p.first != v; }));
@@ -605,9 +606,12 @@ namespace polysat {
         m_search.push_assignment(v, val);
         m_trail.push_back(trail_instr_t::assign_i);
         m_justification[v] = j; 
-        SASSERT(m_viable_fallback.check_constraints(v));
+        // Decision should satisfy all univariate constraints.
+        // Propagation might violate some other constraint; but we will notice that in the propagation loop when v is propagated.
+        // TODO: on the other hand, checking constraints here would have us discover some conflicts earlier.
+        SASSERT(!j.is_decision() || m_viable_fallback.check_constraints(v));
 #if ENABLE_LINEAR_SOLVER
-        // TODO: convert justification into a format that can be tracked in a depdendency core.
+        // TODO: convert justification into a format that can be tracked in a dependency core.
         m_linear_solver.set_value(v, val, UINT_MAX);
 #endif
     }
diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp
index c1e75ba04..e21fe37bd 100644
--- a/src/math/polysat/viable.cpp
+++ b/src/math/polysat/viable.cpp
@@ -790,8 +790,10 @@ namespace polysat {
         for (auto const& c : m_constraints[v]) {
             // for this check, all variables need to be assigned
             DEBUG_CODE(for (pvar w : c->vars()) { SASSERT(s.is_assigned(w)); });
-            if (c.is_currently_false(s))
+            if (c.is_currently_false(s)) {
+                LOG(assignment_pp(s, v, s.get_value(v)) << " violates constraint " << lit_pp(s, c));
                 return false;
+            }
             SASSERT(c.is_currently_true(s));
         }
         return true;