diff --git a/src/math/polysat/conflict.cpp b/src/math/polysat/conflict.cpp
index 08b11d867..707f585a9 100644
--- a/src/math/polysat/conflict.cpp
+++ b/src/math/polysat/conflict.cpp
@@ -194,7 +194,7 @@ namespace polysat {
     unsigned conflict::effective_level() const {
         SASSERT(!empty());
         // If m_dep is set, the corresponding constraint was asserted at m_level and is not valid earlier.
-        if (m_dep != null_dependency)
+        if (!m_dep.is_null())
             return m_level;
         // In other cases, m_level just tracks the level at which the conflict appeared.
         // Find the minimal level at which the conflict is still valid.
@@ -211,7 +211,7 @@ namespace polysat {
     bool conflict::is_valid() const {
         SASSERT(!empty());
         // If m_dep is set, the corresponding constraint was asserted at m_level and is not valid earlier.
-        if (m_dep != null_dependency)
+        if (!m_dep.is_null())
             return m_level <= s.m_level;
         // All conflict constraints must be bool-assigned.
         for (unsigned lit_idx : m_literals)
@@ -657,6 +657,8 @@ namespace polysat {
 
     std::ostream& conflict::display(std::ostream& out) const {
         out << "lvl " << m_level;
+        if (!m_dep.is_null())
+            out << "dep " << m_dep;
         char const* sep = " ";
         for (auto c : *this)
             out << sep << c->bvar2string() << " " << c, sep = " ; ";
diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 8e43a4446..b26718e3b 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -1503,15 +1503,19 @@ namespace polysat {
             // NOTE: the output may look confusing since relevant op_constraints are not printed (does not affect correctness of the core).
             uint_set vars;
             for (auto d : deps) {
+                bool found = false;
                 for (sat::bool_var b = 0; b < m_bvars.size(); ++b) {
                     if (m_bvars.dep(b) != d)
                         continue;
+                    found = true;
                     sat::literal lit(b, m_bvars.value(b) == l_false);
                     SASSERT(m_bvars.is_true(lit));
                     verbose_stream() << "    " << d << ": " << lit_pp(*this, lit) << "\n";
                     for (pvar v : lit2cnstr(lit).vars())
                         vars.insert(v);
                 }
+                if (!found)
+                    verbose_stream() << "    " << d << ": <no constraint in polysat>\n";
             }
             for (pvar v : vars)
                 if (signed_constraint c = m_constraints.find_op_by_result_var(v))
@@ -1519,16 +1523,24 @@ namespace polysat {
         });
 #if ENABLE_LEMMA_VALIDITY_CHECK
         clause_builder cb(*this, "unsat core check");
+        bool ok = true;
         for (auto d : deps) {
+            bool found = false;
             for (sat::bool_var b = 0; b < m_bvars.size(); ++b) {
                 if (m_bvars.dep(b) != d)
                     continue;
+                found = true;
                 sat::literal lit(b, m_bvars.value(b) == l_false);
                 VERIFY(m_bvars.is_true(lit));
                 cb.insert(~lit);
             }
+            if (!found) {
+                ok = false;
+                // VERIFY_EQ(d, m_conflict.m_dep);
+            }
         }
-        log_lemma_smt2(*cb.build());  // check the unsat core
+        if (ok)
+            log_lemma_smt2(*cb.build());  // check the unsat core
 #endif
     }