Fix UNKNOWN bug in search tree about inconsistent end state (#8214)

* restore more aggressive pruning in search tree

* restore where we close children to be correct

* add core strengthening check

* fix recursion bug

* less strict core propagation

* old search tree version

* restore search tree patch

* remove flag

* debugging inconsistent end state with search, some changes need to be made in search tree, only backtrack should be closing nodes, I think the bug is when we do find_highest_attach for nonchronological backjumping, you might get to a point where the sibling is closed, so then we need to resolve further up the tree

* clean up code, fix deadlock

* delete test files

* clean up

---------

Co-authored-by: Ilana Shapiro <ilanashapiro@Mac.localdomain>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MacBook-Pro.local>
Co-authored-by: Ilana Shapiro <ilanashapiro@Ilanas-MBP.lan1>

src/smt/smt_parallel.cpp

@@ -276,6 +276,7 @@ namespace smt {
 
         IF_VERBOSE(1, m_search_tree.display(verbose_stream() << bounded_pp_exprs(core) << "\n"););
         if (m_search_tree.is_closed()) {
+            IF_VERBOSE(1, verbose_stream() << "Search tree closed, setting UNSAT\n");
             m_state = state::is_unsat;
             SASSERT(p.ctx.m_unsat_core.empty());
             for (auto e : m_search_tree.get_core_from_root())

src/util/search_tree.h

@@ -89,7 +89,7 @@ namespace search_tree {
         node *find_active_node() {
             if (m_status == status::active)
                 return this;
-            if (m_status != status::open)
+            if (m_status == status::closed)
                 return nullptr;
             node *nodes[2] = {m_left, m_right};
             for (unsigned i = 0; i < 2; ++i) {
@@ -132,7 +132,6 @@ namespace search_tree {
         random_gen m_rand;
 
         // return an active node in the subtree rooted at n, or nullptr if there is none
-        // close nodes that are fully explored (whose children are all closed)
         node<Config> *activate_from_root(node<Config> *n) {
             if (!n)
                 return nullptr;
@@ -152,8 +151,6 @@ namespace search_tree {
             child = activate_from_root(nodes[1 - index]);
             if (child)
                 return child;
-            if (left && right && left->get_status() == status::closed && right->get_status() == status::closed)
-                n->set_status(status::closed);
             return nullptr;
         }
 
@@ -190,6 +187,39 @@ namespace search_tree {
             return attach_here;
         }
 
+        // Propagate closure upward via sibling resolution starting at node `cur`.
+        // Returns true iff global UNSAT was detected.
+        bool propagate_closure_upward(node<Config>* cur) {
+            while (true) {
+                node<Config>* parent = cur->parent();
+                if (!parent)
+                    return false;
+
+                auto left  = parent->left();
+                auto right = parent->right();
+                if (!left || !right)
+                    return false;
+
+                if (left->get_status() != status::closed ||
+                    right->get_status() != status::closed)
+                    return false;
+
+                if (left->get_core().empty() ||
+                    right->get_core().empty())
+                    return false;
+
+                auto res = compute_sibling_resolvent(left, right);
+
+                if (res.empty()) {
+                    close(m_root.get(), res);   // global UNSAT
+                    return true;
+                }
+
+                close(parent, res);
+                cur = parent;  // keep bubbling
+            }
+        }
+
         void close(node<Config> *n, vector<literal> const &C) {
             if (!n || n->get_status() == status::closed)
                 return;
@@ -245,6 +275,11 @@ namespace search_tree {
 
             auto attach = find_highest_attach(p, resolvent);
             close(attach, resolvent);
+
+            // try to propagate the highest attach node upward *with sibling resolution*
+            // this handles the case when non-chronological backjumping takes us to a node whose sibling was closed by another thread
+            node<Config>* cur = attach;
+            propagate_closure_upward(cur);
         }
 
         // Given complementary sibling nodes for literals x and ¬x, sibling resolvent = (core_left ∪ core_right) \ {x,
@@ -312,6 +347,7 @@ namespace search_tree {
                            };
                        SASSERT(all_of(conflict, [&](auto const &a) { return on_path(a); })););
 
+            // Walk upward to find the nearest ancestor whose decision participates in the conflict
             while (n) {
                 if (any_of(conflict, [&](auto const &a) { return a == n->get_literal(); })) {
                     // close the subtree under n (preserves core attached to n), and attempt to resolve upwards
@@ -339,9 +375,10 @@ namespace search_tree {
 
             auto p = n->parent();
             while (p) {
-                if (p->left() && p->left()->get_status() == status::closed && p->right() &&
+                if (p->left() && p->left()->get_status() == status::closed &&
-                    p->right()->get_status() == status::closed) {
+                    p->right() && p->right()->get_status() == status::closed) {
-                    p->set_status(status::closed);
+                    if (p->get_status() != status::closed) 
+                        return nullptr; // inconsistent state
                     n = p;
                     p = n->parent();
                     continue;