From 79fdb4755ad089e0b6f5cde871f7b52cd0c3ba5c Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 19 Nov 2025 12:42:12 -1000 Subject: [PATCH] improve log_lemma Signed-off-by: Lev Nachmanson --- src/nlsat/nlsat_solver.cpp | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 9ec27469b..6b3781daa 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -1141,7 +1141,10 @@ namespace nlsat { used_vars[v] = true; } display(out << "(echo \"#" << m_lemma_count++ << ":" << annotation << ":", n, cls) << "\")\n"; - out << "(set-logic NRA)\n"; + if (m_log_lemma_smtrat) + out << "(set-logic NRA)\n"; + else + out << "(set-logic ALL)\n"; out << "(set-option :rlimit " << m_lemma_rlimit << ")\n"; if (is_valid) { display_smt2_bool_decls(out, used_bools); @@ -2262,7 +2265,11 @@ namespace nlsat { } } out << "(echo \"#" << m_lemma_count++ << ":assignment lemma " << comment.str() << "\")\n"; - out << "(set-logic NRA)\n"; + if (m_log_lemma_smtrat) + out << "(set-logic NRA)\n"; + else + out << "(set-logic ALL)\n"; + out << "(set-option :rlimit " << m_lemma_rlimit << ")\n"; display_smt2_bool_decls(out, used_bools); display_smt2_arith_decls(out, used_vars); @@ -2300,6 +2307,7 @@ namespace nlsat { print_out_as_math(verbose_stream(), jst) << std::endl; m_lazy_clause.reset(); + m_explain.main_operator(jst.num_lits(), jst.lits(), m_lazy_clause); for (unsigned i = 0; i < sz; i++) m_lazy_clause.push_back(~jst.lit(i));