mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-08 03:51:16 +00:00
Code Activity

t

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-11-16 13:52:28 -10:00
parent 8e4557647f
commit c6eb9d7eb7
2 changed files with 20 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

19
src/nlsat/nlsat_solver.cpp
View file

@ -2242,7 +2242,24 @@ namespace nlsat {
for (var v : vars)
used_vars[v] = true;
}
out << "(echo \"#" << m_lemma_count++ << ":assignment lemma\")\n";
std::ostringstream comment;
bool any_var = false;
display_num_assignment(comment, &used_vars);
if (!any_var)
comment << " (none)";
comment << "; literals:";
if (jst.num_lits() == 0) {
comment << " (none)";
}
else {
for (unsigned i = 0; i < jst.num_lits(); ++i) {
comment << " ";
display(comment, jst.lit(i));
if (i < jst.num_lits() - 1)
comment << " /\\";
}
}
out << "(echo \"#" << m_lemma_count++ << ":assignment lemma " << comment.str() << "\")\n";
out << "(set-logic ALL)\n";
out << "(set-option :rlimit " << m_lemma_rlimit << ")\n";
display_smt2_bool_decls(out, used_bools);