fix #3807

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/macros/macro_manager.cpp

@@ -25,6 +25,7 @@ Revision History:
 #include "ast/rewriter/th_rewriter.h"
 #include "ast/rewriter/rewriter_def.h"
 #include "ast/ast_pp.h"
+#include "ast/ast_translation.h"
 #include "ast/recurse_expr_def.h"
 
 
@@ -95,6 +96,26 @@ void macro_manager::reset() {
     m_deps.reset();
 }
 
+void macro_manager::copy_to(macro_manager& dst) {
+    ast_manager& tm = dst.get_manager();
+    ast_translation tr(m, tm);
+    for (func_decl* f : m_decls) {
+        func_decl_ref f2(tr(f), tm);
+        quantifier_ref q2(tr(m_decl2macro[f]), tm);
+        proof_ref pr2(tm);
+        expr_dependency_ref dep2(tm);
+        proof* pr1 = nullptr;
+        if (m_decl2macro_pr.find(f, pr1)) {
+            pr2 = tr(pr1);
+        }
+        expr_dependency* dep1 = m_decl2macro_dep[f];
+        if (dep1) {
+            dep2 = ::translate(dep1, m, tm);
+        }
+        dst.insert(f2, q2, pr2, dep2);        
+    }
+}
+
 bool macro_manager::insert(func_decl * f, quantifier * q, proof * pr, expr_dependency* dep) {
     TRACE("macro_insert", tout << "trying to create macro: " << f->get_name() << "\n" << mk_pp(q, m) << "\n";);
 

src/ast/macros/macro_manager.h

@@ -65,6 +65,7 @@ class macro_manager {
 public:
     macro_manager(ast_manager & m);
     ~macro_manager();
+    void copy_to(macro_manager& dst);
     ast_manager & get_manager() const { return m; }
     macro_util & get_util() { return m_util; }
     bool insert(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep = nullptr);

src/smt/asserted_formulas.h

@@ -268,6 +268,7 @@ class asserted_formulas {
     // Macros
     //
     // -----------------------------------
+    macro_manager& get_macro_manager() { return m_macro_manager; }
     unsigned get_num_macros() const { return m_macro_manager.get_num_macros(); }
     unsigned get_first_macro_last_level() const { return m_macro_manager.get_first_macro_last_level(); }
     func_decl * get_macro_func_decl(unsigned i) const { return m_macro_manager.get_macro_func_decl(i); }

src/smt/smt_context.cpp

@@ -160,6 +160,8 @@ namespace smt {
             dst_af.assert_expr(fml, pr);
         }
 
+        src_af.get_macro_manager().copy_to(dst_af.get_macro_manager());
+
         if (!src_ctx.m_setup.already_configured()) {
             return;
         }