mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-23 06:01:26 +00:00
Code Activity

t

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-11-13 19:24:31 -10:00
parent 6e37a3c5b8
commit eba6a66e6f
1 changed files with 0 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/nlsat/nlsat_solver.cpp
View file

@ -1177,12 +1177,6 @@ namespace nlsat {
TRACE(nlsat_sort, display(tout << "mk_clause:\n", *cls) << "\n";); TRACE(nlsat_sort, display(tout << "mk_clause:\n", *cls) << "\n";);
std::sort(cls->begin(), cls->end(), lit_lt(*this)); std::sort(cls->begin(), cls->end(), lit_lt(*this));
TRACE(nlsat, display(tout << " after sort:\n", *cls) << "\n";); TRACE(nlsat, display(tout << " after sort:\n", *cls) << "\n";);
if (learned && m_log_lemmas) {
log_lemma(verbose_stream(), *cls);
}
if (learned && m_check_lemmas) {
check_lemma(cls->size(), cls->data(), false, cls->assumptions());
}
if (learned) if (learned)
m_learned.push_back(cls); m_learned.push_back(cls);
else else