mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-02 17:30:23 +00:00
Code Activity

remove unused code

Browse source
This commit is contained in:
Jakob Rath 2023-03-23 13:40:19 +01:00
parent 50814c952a
commit f364ba8c8a
1 changed files with 0 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/math/polysat/solver.cpp
View file

@ -1488,23 +1488,7 @@ namespace polysat {
} }
void solver::report_unsat() { void solver::report_unsat() {
#if 0
// NOTE: backjump may destroy dependencies of the conflict (e.g., lose boolean propagations).
// so we reset the conflict, backjump, then propagate to restore the conflicts
clause_ref confl = m_conflict.build_lemma();
m_conflict.reset();
backjump(base_level()); backjump(base_level());
propagate_clause(*confl);
propagate();
if (!is_conflict())
add_clause(confl);
if (!is_conflict()) {
LOG("confl: " << show_deref(confl));
LOG("state:\n" << *this);
}
#else
backjump(base_level());
#endif
VERIFY(is_conflict()); VERIFY(is_conflict());
} }