From 5d49cb551909d950239d490a07b60c4edbec2fbe Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 22 Apr 2021 22:42:05 -0700
Subject: [PATCH] #5211

---
 src/ast/euf/euf_egraph.cpp | 3 ++-
 src/sat/sat_extension.h    | 2 +-
 src/sat/smt/bv_solver.cpp  | 1 +
 3 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index c9396717a..401958546 100644
--- a/src/ast/euf/euf_egraph.cpp
+++ b/src/ast/euf/euf_egraph.cpp
@@ -765,7 +765,6 @@ namespace euf {
 
     void egraph::copy_from(egraph const& src, std::function<void*(void*)>& copy_justification) {
         SASSERT(m_scopes.empty());
-        SASSERT(src.m_scopes.empty());
         SASSERT(m_nodes.empty());
         ptr_vector<enode> old_expr2new_enode, args;
         ast_translation tr(src.m, m);
@@ -793,6 +792,8 @@ namespace euf {
                 merge(n2, n2t, n1->m_justification.copy(copy_justification));
         }
         propagate();
+        for (unsigned i = 0; i < src.m_scopes.size(); ++i)
+            push();
     }
 }
 
diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h
index 0f5ccdcc3..b03518065 100644
--- a/src/sat/sat_extension.h
+++ b/src/sat/sat_extension.h
@@ -68,7 +68,7 @@ namespace sat {
         symbol m_name;
         solver* m_solver { nullptr };
     public:        
-        extension(symbol const& name, int id): m_id(id), m_name(name) {}
+        extension(symbol const& name, int id): m_id(id), m_name(name) { }
         virtual ~extension() {}
         int get_id() const { return m_id; }
         void set_solver(solver* s) { m_solver = s; }        
diff --git a/src/sat/smt/bv_solver.cpp b/src/sat/smt/bv_solver.cpp
index 8c7238f1f..35ea2e104 100644
--- a/src/sat/smt/bv_solver.cpp
+++ b/src/sat/smt/bv_solver.cpp
@@ -661,6 +661,7 @@ namespace bv {
             result->m_bits[i].append(m_bits[i]);
             result->m_zero_one_bits[i].append(m_zero_one_bits[i]);
         }
+        result->set_solver(&ctx.s());
         for (theory_var i = 0; i < static_cast<theory_var>(get_num_vars()); ++i)
             if (find(i) != i)
                 result->m_find.merge(i, find(i));