From a0e0aa8a839614351567168eefa7b85ed143f314 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 13 Nov 2025 18:54:34 -1000 Subject: [PATCH] t Signed-off-by: Lev Nachmanson --- src/nlsat/nlsat_solver.cpp | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index f7ff54223..4d92bd741 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -1121,7 +1121,7 @@ namespace nlsat { } void log_lemma(std::ostream& out, clause const& cls) { - log_lemma(out, cls.size(), cls.data(), false); + log_lemma(out, cls.size(), cls.data(), true); } void log_lemma(std::ostream& out, unsigned n, literal const* cls, bool is_valid) { @@ -2251,8 +2251,12 @@ namespace nlsat { } out << "(echo \"assignment lemma " << ttt << "\")\n"; out << "(set-logic ALL)\n"; + for (var x = 0; x < num_vars(); ++x) { + if (m_assignment.is_assigned(x)) + used_vars.setx(x, true, false); + } display_smt2_bool_decls(out, used_bools); - display_smt2_arith_decls(out, used_vars); + display_smt2_arith_decls(out, used_vars); display_bool_assignment(out, false, &used_bools); display_num_assignment(out, &used_vars); for (literal lit : core) {