From 89aaf4b1a620d45ee4a935873d8be5d1b7ec745d Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Fri, 17 Mar 2023 14:35:15 +0100
Subject: [PATCH] resume conflict

---
 src/math/polysat/solver.cpp | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp
index 2eb63e92b..29d4e7499 100644
--- a/src/math/polysat/solver.cpp
+++ b/src/math/polysat/solver.cpp
@@ -1516,9 +1516,14 @@ namespace polysat {
     void solver::report_unsat() {
         // 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();
+        LOG("confl: " << show_deref(confl));
         m_conflict.reset();
         backjump(base_level());
+        propagate_clause(*confl);
         propagate();
+        if (!is_conflict())
+            add_clause(confl);
         VERIFY(!m_conflict.empty());
     }