diff --git a/src/util/search_tree.h b/src/util/search_tree.h
index 2b58edd95..5ec2e5776 100644
--- a/src/util/search_tree.h
+++ b/src/util/search_tree.h
@@ -54,6 +54,8 @@ namespace search_tree {
         literal const& get_literal() const { return m_literal; }
         bool literal_is_null() const { return Config::is_null(m_literal); }
         void split(literal const& a, literal const& b) {
+            SASSERT(!Config::literal_is_null(a));
+            SASSERT(!Config::literal_is_null(b));
             if (m_status != status::active)
                 return;
             SASSERT(!m_left);
@@ -136,13 +138,8 @@ namespace search_tree {
         
         // Split current node if it is active.
         // After the call, n is open and has two children.
-        void split(node<Config>* n, literal const& a, literal const& b) {
-            SASSERT(!Config::literal_is_null(a));
-            SASSERT(!Config::literal_is_null(b));
-            if (n->get_status() == status::active) {              
-                n->split(a, b);
-                n->set_status(status::open);
-            }
+        void split(node<Config>* n, literal const& a, literal const& b) {           
+            n->split(a, b);
         }
 
         // conflict is given by a set of literals.
@@ -155,6 +152,7 @@ namespace search_tree {
             }           
             SASSERT(n != m_root.get());
             // all literals in conflict are on the path from root to n
+            // remove assumptions from conflict to ensure this.
             DEBUG_CODE(
                 auto on_path = [&](literal const& a) {
                     node<Config>* p = n;
@@ -226,4 +224,4 @@ namespace search_tree {
         }
 
     };
-}
+}
\ No newline at end of file