From e70f501932415eaf06dac8acf881572a83b7a6d0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 9 Sep 2021 09:17:11 +0200
Subject: [PATCH] handle potential extra nodes from q_solver

---
 src/sat/smt/euf_solver.cpp | 32 +++++++++++++++++++++++---------
 1 file changed, 23 insertions(+), 9 deletions(-)

diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 68b70cb5e..774a76848 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -461,6 +461,13 @@ namespace euf {
             give_up = true;
         
         unsigned num_nodes = m_egraph.num_nodes();
+        auto apply_solver = [&](th_solver* e) {
+            switch (e->check()) {
+            case sat::check_result::CR_CONTINUE: cont = true; break;
+            case sat::check_result::CR_GIVEUP: give_up = true; break;
+            default: break;
+            }
+        };
         if (merge_shared_bools())
             cont = true;
         for (auto* e : m_solvers) {
@@ -468,25 +475,24 @@ namespace euf {
                 return sat::check_result::CR_GIVEUP;
             if (e == m_qsolver)
                 continue;
-            switch (e->check()) {
-            case sat::check_result::CR_CONTINUE: cont = true; break;
-            case sat::check_result::CR_GIVEUP: give_up = true; break;
-            default: break;
-            }
+            apply_solver(e);
             if (s().inconsistent())
                 return sat::check_result::CR_CONTINUE;
         }
+        if (m_qsolver) 
+            apply_solver(m_qsolver);
+
+	if (s().inconsistent())
+            return sat::check_result::CR_CONTINUE;
         if (cont)
             return sat::check_result::CR_CONTINUE;
-        if (give_up)
-            return sat::check_result::CR_GIVEUP;
         if (num_nodes < m_egraph.num_nodes()) {
             IF_VERBOSE(1, verbose_stream() << "new nodes created, but not detected\n");
             return sat::check_result::CR_CONTINUE;           
         }
-        if (m_qsolver)
-            return m_qsolver->check();
         TRACE("after_search", s().display(tout););
+        if (give_up)
+            return sat::check_result::CR_GIVEUP;
         return sat::check_result::CR_DONE;
     }
 
@@ -857,6 +863,14 @@ namespace euf {
         };
         r->m_egraph.copy_from(m_egraph, copy_justification);        
         r->set_solver(s);
+        for (euf::enode* n : r->m_egraph.nodes()) {
+            auto b = n->bool_var();
+            if (b != sat::null_bool_var) {
+                m_bool_var2expr.setx(b, n->get_expr(), nullptr);
+                SASSERT(r->m.is_bool(n->get_sort()));
+                IF_VERBOSE(0, verbose_stream() << "set bool_var " << r->bpp(n) << "\n");
+            }
+        }
         for (auto* s_orig : m_id2solver) {
             if (s_orig) {
                 auto* s_clone = s_orig->clone(*r);