diff --git a/src/ast/macros/macro_manager.cpp b/src/ast/macros/macro_manager.cpp
index 02f4f6db4..cb766e400 100644
--- a/src/ast/macros/macro_manager.cpp
+++ b/src/ast/macros/macro_manager.cpp
@@ -106,7 +106,8 @@ bool macro_manager::insert(func_decl * f, quantifier * q, proof * pr, expr_depen
 
     app * head;
     expr * definition;
-    get_head_def(q, f, head, definition);
+    bool revert = false;
+    get_head_def(q, f, head, definition, revert);
 
     func_decl_set * s = m_deps.mk_func_decl_set();
     m_deps.collect_func_decls(definition, s);
@@ -167,17 +168,19 @@ void macro_manager::mark_forbidden(unsigned n, justified_expr const * exprs) {
 }
 
 
-void macro_manager::get_head_def(quantifier * q, func_decl * d, app * & head, expr * & def) const {
+void macro_manager::get_head_def(quantifier * q, func_decl * d, app * & head, expr * & def, bool& revert) const {
     app * body = to_app(q->get_expr());
     expr * lhs = nullptr, *rhs = nullptr;
     VERIFY(m.is_eq(body, lhs, rhs));
     SASSERT(is_app_of(lhs, d) || is_app_of(rhs, d));
     SASSERT(!is_app_of(lhs, d) || !is_app_of(rhs, d));
     if (is_app_of(lhs, d)) {
+        revert = false;
         head = to_app(lhs);
         def  = rhs;
     }
     else {
+        revert = true;
         head = to_app(rhs);
         def  = lhs;
     }
@@ -191,7 +194,8 @@ void macro_manager::display(std::ostream & out) {
         m_decl2macro.find(f, q);
         app * head;
         expr * def;
-        get_head_def(q, f, head, def);
+        bool r;
+        get_head_def(q, f, head, def, r);
         SASSERT(q);
         out << mk_pp(head, m) << " ->\n" << mk_pp(def, m) << "\n";
     }
@@ -202,7 +206,8 @@ func_decl * macro_manager::get_macro_interpretation(unsigned i, expr_ref & inter
     quantifier * q = m_macros.get(i);
     app * head;
     expr * def;
-    get_head_def(q, f, head, def);
+    bool r;
+    get_head_def(q, f, head, def, r);
     TRACE("macro_bug",
           tout << f->get_name() << "\n" << mk_pp(head, m) << "\n" << mk_pp(q, m) << "\n";);
     m_util.mk_macro_interpretation(head, q->get_num_decls(), def, interp);
@@ -256,6 +261,9 @@ struct macro_manager::macro_expander_cfg : public default_rewriter_cfg {
         if (erase_patterns) {
             result = m.update_quantifier(old_q, 0, nullptr, 0, nullptr, new_body);
         }
+        if (erase_patterns && m.proofs_enabled()) {
+            result_pr = m.mk_rewrite(old_q, result);
+        }
         return erase_patterns;
     }
 
@@ -270,7 +278,8 @@ struct macro_manager::macro_expander_cfg : public default_rewriter_cfg {
             
             app * head = nullptr;
             expr * def = nullptr;
-            mm.get_head_def(q, d, head, def);
+            bool revert = false;
+            mm.get_head_def(q, d, head, def, revert);
             unsigned num = n->get_num_args();
             SASSERT(head && def);
             TRACE("macro_manager", tout << "expanding: " << mk_pp(n, m) << "\n" << mk_pp(head, m) << " " << mk_pp(def, m) << "\n";);
@@ -293,9 +302,10 @@ struct macro_manager::macro_expander_cfg : public default_rewriter_cfg {
                 proof * qi_pr = m.mk_quant_inst(m.mk_or(m.mk_not(q), instance), num, subst_args.c_ptr());
                 proof * q_pr  = nullptr;
                 mm.m_decl2macro_pr.find(d, q_pr);
-                SASSERT(q_pr != 0);
+                SASSERT(q_pr);
                 proof * prs[2] = { qi_pr, q_pr };
                 p = m.mk_unit_resolution(2, prs);
+                if (revert) p = m.mk_symmetry(p);
             }
             else {
                 p = nullptr;
@@ -331,6 +341,7 @@ void macro_manager::expand_macros(expr * n, proof * pr, expr_dependency * dep, e
         for (;;) {
             macro_expander_rw proc(m, *this);
             proof_ref n_eq_r_pr(m);
+            SASSERT(m.get_fact(old_pr) == old_n);
             TRACE("macro_manager_bug", tout << "expand_macros:\n" << mk_pp(n, m) << "\n";);
             proc(old_n, r, n_eq_r_pr);
             new_pr = m.mk_modus_ponens(old_pr, n_eq_r_pr);
diff --git a/src/ast/macros/macro_manager.h b/src/ast/macros/macro_manager.h
index 4fcb29f5d..d63e9a27a 100644
--- a/src/ast/macros/macro_manager.h
+++ b/src/ast/macros/macro_manager.h
@@ -83,7 +83,7 @@ public:
     func_decl * get_macro_func_decl(unsigned i) const { return m_decls.get(i); }
     func_decl * get_macro_interpretation(unsigned i, expr_ref & interp) const;
     quantifier * get_macro_quantifier(func_decl * f) const { quantifier * q = nullptr; m_decl2macro.find(f, q); return q; }
-    void get_head_def(quantifier * q, func_decl * d, app * & head, expr * & def) const;
+    void get_head_def(quantifier * q, func_decl * d, app * & head, expr * & def, bool& revert) const;
     void expand_macros(expr * n, proof * pr, expr_dependency * dep, expr_ref & r, proof_ref & new_pr, expr_dependency_ref & new_dep);