diff --git a/src/ast/macros/macro_manager.cpp b/src/ast/macros/macro_manager.cpp
index 6a1f4f160..001c6ad06 100644
--- a/src/ast/macros/macro_manager.cpp
+++ b/src/ast/macros/macro_manager.cpp
@@ -126,7 +126,7 @@ bool macro_manager::insert(func_decl * f, quantifier * q, proof * pr, expr_depen
     }
 
     app * head;
-    expr * definition;
+    expr_ref definition(m);
     bool revert = false;
     get_head_def(q, f, head, definition, revert);
 
@@ -190,21 +190,22 @@ 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, bool& revert) const {
-    app * body = to_app(q->get_expr());
+void macro_manager::get_head_def(quantifier * q, func_decl * d, app * & head, expr_ref & def, bool& revert) const {
+    expr * body = q->get_expr();
     expr * lhs = nullptr, *rhs = nullptr;
+    bool is_not = m.is_not(body, body);
     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;
+        def  = is_not ? m.mk_not(rhs) : rhs;
     }
     else {
         revert = true;
         head = to_app(rhs);
-        def  = lhs;
+        def  = is_not ? m.mk_not(lhs) : lhs;
     }
 }
 
@@ -215,7 +216,7 @@ void macro_manager::display(std::ostream & out) {
         quantifier * q = nullptr;
         m_decl2macro.find(f, q);
         app * head;
-        expr * def;
+        expr_ref def(m);
         bool r;
         get_head_def(q, f, head, def, r);
         SASSERT(q);
@@ -227,7 +228,7 @@ func_decl * macro_manager::get_macro_interpretation(unsigned i, expr_ref & inter
     func_decl * f  = m_decls.get(i);
     quantifier * q = m_macros.get(i);
     app * head;
-    expr * def;
+    expr_ref def(m);
     bool r;
     get_head_def(q, f, head, def, r);
     TRACE("macro_bug",
@@ -298,7 +299,7 @@ struct macro_manager::macro_expander_cfg : public default_rewriter_cfg {
         TRACE("macro_manager", tout << "trying to expand:\n" << mk_pp(n, m) << "\nd:\n" << d->get_name() << "\n";);
         if (mm.m_decl2macro.find(d, q)) {            
             app * head = nullptr;
-            expr * def = nullptr;
+            expr_ref def(m);
             bool revert = false;
             mm.get_head_def(q, d, head, def, revert);
             unsigned num = n->get_num_args();
@@ -320,6 +321,14 @@ struct macro_manager::macro_expander_cfg : public default_rewriter_cfg {
             r = rr;
             if (m.proofs_enabled()) {
                 expr_ref instance = s(q->get_expr(), num, subst_args.data());
+                expr* eq, * lhs, * rhs;
+                if (m.is_not(instance, eq) && m.is_eq(eq, lhs, rhs)) {
+                    if (revert)
+                        instance = m.mk_eq(m.mk_not(lhs), rhs);
+                    else
+                        instance = m.mk_eq(lhs, m.mk_not(rhs));
+                }
+                SASSERT(m.is_eq(instance));
                 proof * qi_pr = m.mk_quant_inst(m.mk_or(m.mk_not(q), instance), num, subst_args.data());
                 proof * q_pr  = mm.m_decl2macro_pr.find(d);
                 proof * prs[2] = { qi_pr, q_pr };
diff --git a/src/ast/macros/macro_manager.h b/src/ast/macros/macro_manager.h
index 8000ce894..6aac12114 100644
--- a/src/ast/macros/macro_manager.h
+++ b/src/ast/macros/macro_manager.h
@@ -84,7 +84,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, bool& revert) const;
+    void get_head_def(quantifier * q, func_decl * d, app * & head, expr_ref & 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);
 
 
diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp
index c024d870e..00f96299b 100644
--- a/src/ast/macros/macro_util.cpp
+++ b/src/ast/macros/macro_util.cpp
@@ -184,6 +184,14 @@ bool macro_util::is_left_simple_macro(expr * n, unsigned num_decls, app_ref & he
         def  = rhs;
         return true;
     }
+    if (m_manager.is_not(n, lhs) && m_manager.is_eq(lhs, lhs, rhs) &&
+        is_macro_head(lhs, num_decls) &&
+        !is_forbidden(to_app(lhs)->get_decl()) &&
+        !occurs(to_app(lhs)->get_decl(), rhs)) {
+        head = to_app(lhs);
+        def  = m_manager.mk_not(rhs);
+        return true;
+    }
     return false;
 }
 
@@ -215,6 +223,14 @@ bool macro_util::is_right_simple_macro(expr * n, unsigned num_decls, app_ref & h
         def  = lhs;
         return true;
     }
+    if (m_manager.is_not(n, n) && m_manager.is_eq(n, lhs, rhs) &&
+        is_macro_head(rhs, num_decls) &&
+        !is_forbidden(to_app(rhs)->get_decl()) &&
+        !occurs(to_app(rhs)->get_decl(), lhs)) {
+        head = to_app(rhs);
+        def  = m_manager.mk_not(lhs);
+        return true;
+    }
     return false;
 }
 
diff --git a/src/ast/macros/quasi_macros.cpp b/src/ast/macros/quasi_macros.cpp
index a3e6c61e7..2920c9667 100644
--- a/src/ast/macros/quasi_macros.cpp
+++ b/src/ast/macros/quasi_macros.cpp
@@ -148,6 +148,15 @@ bool quasi_macros::depends_on(expr * e, func_decl * f) const {
     return false;
 }
 
+bool quasi_macros::is_quasi_def(quantifier* q, expr* lhs, expr* rhs) const {
+  return
+    is_non_ground_uninterp(lhs) &&
+    is_unique(to_app(lhs)->get_decl()) &&
+    !depends_on(rhs, to_app(lhs)->get_decl()) &&
+    fully_depends_on(to_app(lhs), q);
+}
+
+
 bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const {
     // Our definition of a quasi-macro:
     // Forall X. f[X] = T[X], where f[X] is a term starting with symbol f, f is uninterpreted,
@@ -158,27 +167,39 @@ bool quasi_macros::is_quasi_macro(expr * e, app_ref & a, expr_ref & t) const {
         quantifier * q = to_quantifier(e);
         expr * qe = q->get_expr(), *lhs = nullptr, *rhs = nullptr;
         if (m.is_eq(qe, lhs, rhs)) {
-            if (is_non_ground_uninterp(lhs) && is_unique(to_app(lhs)->get_decl()) &&
-                !depends_on(rhs, to_app(lhs)->get_decl()) && fully_depends_on(to_app(lhs), q)) {
-                a = to_app(lhs);
+	  if (is_quasi_def(q, lhs, rhs)) {
+	        a = to_app(lhs);
                 t = rhs;
                 return true;
-            } else if (is_non_ground_uninterp(rhs) && is_unique(to_app(rhs)->get_decl()) &&
-                !depends_on(lhs, to_app(rhs)->get_decl()) && fully_depends_on(to_app(rhs), q)) {
-                a = to_app(rhs);
+	  } else if (is_quasi_def(q, rhs, lhs)) {
+	        a = to_app(rhs);
                 t = lhs;
                 return true;
             }
-        } else if (m.is_not(qe, lhs) && is_non_ground_uninterp(lhs) &&
+        }
+	else if (m.is_not(qe, lhs) && is_non_ground_uninterp(lhs) &&
                    is_unique(to_app(lhs)->get_decl())) { // this is like f(...) = false
             a = to_app(lhs);
             t = m.mk_false();
             return true;
-        } else if (is_non_ground_uninterp(qe) && is_unique(to_app(qe)->get_decl())) { // this is like f(...) = true
+        }
+	else if (is_non_ground_uninterp(qe) && is_unique(to_app(qe)->get_decl())) { // this is like f(...) = true
             a = to_app(qe);
             t = m.mk_true();
             return true;
         }
+	else if (m.is_not(qe, lhs) && m.is_eq(lhs, lhs, rhs) && m.is_bool(lhs)) {
+	  if (is_quasi_def(q, lhs, rhs)) {
+	        a = to_app(lhs);
+                t = m.mk_not(rhs);
+                return true;
+            } else if (is_quasi_def(q, rhs, lhs)) {
+	        a = to_app(rhs);
+                t = m.mk_not(lhs);
+                return true;
+            }
+	}
+
     }
 
     return false;
diff --git a/src/ast/macros/quasi_macros.h b/src/ast/macros/quasi_macros.h
index 7ff1205e2..4441f432e 100644
--- a/src/ast/macros/quasi_macros.h
+++ b/src/ast/macros/quasi_macros.h
@@ -49,6 +49,7 @@ class quasi_macros {
     bool depends_on(expr * e, func_decl * f) const;
 
     bool is_quasi_macro(expr * e, app_ref & a, expr_ref &v) const;
+    bool is_quasi_def(quantifier* q, expr* lhs, expr* rhs) const;
     bool quasi_macro_to_macro(quantifier * q, app * a, expr * t, quantifier_ref & macro);
 
     void find_occurrences(expr * e);