mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-22 13:41:27 +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 dc2a7dc170
commit bcb976ba1a
2 changed files with 20 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/nlsat/nlsat_explain.cpp
View file

@ -1484,7 +1484,7 @@ namespace nlsat {
m_pm.display(tout << " equation used: ", eq_ref, m_solver.display_proc()); m_pm.display(tout << " equation used: ", eq_ref, m_solver.display_proc());
tout << " = 0\n"; tout << " = 0\n";
}); });
new_lit = l; // SIMP_BUG new_lit = l;
} }
else { else {
literal assumption = new_lit; literal assumption = new_lit;
@ -1498,7 +1498,7 @@ namespace nlsat {
tout << " = 0\n"; tout << " = 0\n";
}); });
add_literal(assumption); add_literal(assumption);
new_lit = true_literal; // SIMP_BUG new_lit = true_literal;
} }
} }
else { else {
@ -1517,7 +1517,6 @@ namespace nlsat {
m_pm.display(tout << " equation used: ", eq_ref, m_solver.display_proc()); m_pm.display(tout << " equation used: ", eq_ref, m_solver.display_proc());
tout << " = 0\n"; tout << " = 0\n";
}); });
// SIMP_BUG
} }
} }
} }

19
src/nlsat/nlsat_solver.cpp
View file

@ -2242,7 +2242,24 @@ namespace nlsat {
for (var v : vars) for (var v : vars)
used_vars[v] = true; 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-logic ALL)\n";
out << "(set-option :rlimit " << m_lemma_rlimit << ")\n"; out << "(set-option :rlimit " << m_lemma_rlimit << ")\n";
display_smt2_bool_decls(out, used_bools); display_smt2_bool_decls(out, used_bools);