From 6e37a3c5b81326d8403ee414c816ad95363d7522 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 13 Nov 2025 19:17:24 -1000 Subject: [PATCH] t Signed-off-by: Lev Nachmanson --- src/nlsat/nlsat_solver.cpp | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 13b9e4fd3..fe7e760a2 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -1139,7 +1139,7 @@ namespace nlsat { used_vars[v] = true; } TRACE(nlsat, display(tout << "(echo \"#" << ++ttt << " expl lemma ", n, cls) << "\")\n"); - display(out << "(echo \"#" << ttt << " ", n, cls) << "\")\n"; + display(out << "(echo \"#" << ttt << (is_valid?" learned " : " conflict ") , n, cls) << "\")\n"; out << "(set-logic ALL)\n"; if (is_valid) { display_smt2_bool_decls(out, used_bools); @@ -2249,12 +2249,8 @@ namespace nlsat { for (var v : vars) used_vars[v] = true; } - out << "(echo \"assignment lemma " << ttt << "\")\n"; + out << "(echo \"#" << ttt<< " assignment lemma\")\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_bool_assignment(out, false, &used_bools);