From e916065f7c8b611fb2c4d397589d2770958b9e1e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 8 Sep 2025 19:14:25 -0700
Subject: [PATCH] fix bug in activate node!

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/util/search_tree.h | 19 ++++++++++---------
 1 file changed, 10 insertions(+), 9 deletions(-)

diff --git a/src/util/search_tree.h b/src/util/search_tree.h
index 778315fab..c2bae663c 100644
--- a/src/util/search_tree.h
+++ b/src/util/search_tree.h
@@ -221,28 +221,29 @@ namespace search_tree {
             auto res = activate_from_root(n);
             if (res)
                 return res;
-            while (n) {
-                if (n->left() && n->left()->get_status() == status::closed &&
-                    n->right() && n->right()->get_status() == status::closed) {
-                    n->set_status(status::closed);
-                    n = n->parent();
+
+            auto p = n->parent();
+            while (p) {
+                if (p->left() && p->left()->get_status() == status::closed &&
+                    p->right() && p->right()->get_status() == status::closed) {
+                    p->set_status(status::closed);
+                    n = p;                    
+                    p = n->parent();
                     continue;
                 }
-                auto p = n->parent();
-                if (!p)
-                    return nullptr;
                 if (n == p->left()) {
                     res = activate_from_root(p->right());
                     if (res)
                         return res;
                 }
                 else {
-                    SASSERT(n == p->right());
+                    VERIFY(n == p->right());
                     res = activate_from_root(p->left());
                     if (res)
                         return res;
                 }                   
                 n = p;
+                p = n->parent();
             }
             return nullptr;
         }