From f364ba8c8a8bd21fe6a6365a7bf3fb5f332a328d Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Thu, 23 Mar 2023 13:40:19 +0100 Subject: [PATCH] remove unused code --- src/math/polysat/solver.cpp | 16 ---------------- 1 file changed, 16 deletions(-) diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index f87026f6c..916a37ecf 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -1488,23 +1488,7 @@ namespace polysat { } 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()); - 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()); }