diff --git a/src/sat/smt/polysat/core.cpp b/src/sat/smt/polysat/core.cpp
index dd30e8227..793db7392 100644
--- a/src/sat/smt/polysat/core.cpp
+++ b/src/sat/smt/polysat/core.cpp
@@ -149,13 +149,14 @@ namespace polysat {
         m_var = m_var_queue.next_var();       
         s.trail().push(mk_dqueue_var(m_var, *this));
         switch (m_viable.find_viable(m_var, m_value)) {
-        case find_t::empty:
-            s.set_lemma(m_viable.get_core(), 0, m_viable.explain());
-            // propagate_unsat_core();
+        case find_t::empty: 
+            s.set_lemma(m_viable.get_core(), m_viable.explain());
+            // propagate_unsat_core();        
             return sat::check_result::CR_CONTINUE;
-        case find_t::singleton:
+        case find_t::singleton: {
             s.propagate(m_constraints.eq(var2pdd(m_var), m_value), m_viable.explain());
             return sat::check_result::CR_CONTINUE;
+        }
         case find_t::multiple:  
             s.add_eq_literal(m_var, m_value);
             return sat::check_result::CR_CONTINUE;
diff --git a/src/sat/smt/polysat/types.h b/src/sat/smt/polysat/types.h
index 6f855f98b..e7beb3eb1 100644
--- a/src/sat/smt/polysat/types.h
+++ b/src/sat/smt/polysat/types.h
@@ -107,7 +107,7 @@ namespace polysat {
         virtual ~solver_interface() {}
         virtual void add_eq_literal(pvar v, rational const& val) = 0;
         virtual void set_conflict(dependency_vector const& core) = 0;
-        virtual void set_lemma(core_vector const& aux_core, unsigned level, dependency_vector const& core) = 0;
+        virtual void set_lemma(core_vector const& aux_core, dependency_vector const& core) = 0;
         virtual void add_polysat_clause(char const* name, core_vector cs, bool redundant) = 0;
         virtual dependency propagate(signed_constraint sc, dependency_vector const& deps) = 0;
         virtual void propagate(dependency const& d, bool sign, dependency_vector const& deps) = 0;
diff --git a/src/sat/smt/polysat_solver.cpp b/src/sat/smt/polysat_solver.cpp
index c14ca1d14..a713cc4a4 100644
--- a/src/sat/smt/polysat_solver.cpp
+++ b/src/sat/smt/polysat_solver.cpp
@@ -130,8 +130,13 @@ namespace polysat {
         return { core, eqs };
     }
 
-    void solver::set_lemma(core_vector const& aux_core, unsigned level, dependency_vector const& core) {
+    void solver::set_lemma(core_vector const& aux_core, dependency_vector const& core) {
         auto [lits, eqs] = explain_deps(core);
+        unsigned level = 0;
+        for (auto const& [n1, n2] : eqs)
+            ctx.get_eq_antecedents(n1, n2, lits);
+        for (auto lit : lits)
+            level = std::max(level, s().lvl(lit));
         auto ex = euf::th_explain::conflict(*this, lits, eqs, nullptr);
         ctx.push(value_trail<bool>(m_has_lemma));
         m_has_lemma = true;
diff --git a/src/sat/smt/polysat_solver.h b/src/sat/smt/polysat_solver.h
index a04c76618..e88eafdd2 100644
--- a/src/sat/smt/polysat_solver.h
+++ b/src/sat/smt/polysat_solver.h
@@ -144,7 +144,7 @@ namespace polysat {
         // callbacks from core
         void add_eq_literal(pvar v, rational const& val) override;
         void set_conflict(dependency_vector const& core) override;
-        void set_lemma(core_vector const& aux_core, unsigned level, dependency_vector const& core) override;
+        void set_lemma(core_vector const& aux_core, dependency_vector const& core) override;
         dependency propagate(signed_constraint sc, dependency_vector const& deps) override;
         void propagate(dependency const& d, bool sign, dependency_vector const& deps) override;
         trail_stack& trail() override;