diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 228722dcd..28b709def 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2410,7 +2410,7 @@ public: js = alloc(theory_lemma_justification, get_id(), ctx(), m_core2.size(), m_core2.data(), ps.size(), ps.data()); } - ctx().mk_clause(m_core2.size(), m_core2.data(), js, CLS_TH_LEMMA_LEARNED, nullptr); + ctx().mk_clause(m_core2.size(), m_core2.data(), js, CLS_TH_LEMMA_RELEVANT, nullptr); } else { ctx().assign(