diff --git a/src/ast/macros/macro_manager.cpp b/src/ast/macros/macro_manager.cpp
index 001c6ad06..254663c66 100644
--- a/src/ast/macros/macro_manager.cpp
+++ b/src/ast/macros/macro_manager.cpp
@@ -197,6 +197,7 @@ void macro_manager::get_head_def(quantifier * q, func_decl * d, app * & head, ex
     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));
+    SASSERT(!is_not || m.is_bool(lhs));     
     if (is_app_of(lhs, d)) {
         revert = false;
         head = to_app(lhs);
diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp
index 00f96299b..8a4036730 100644
--- a/src/ast/macros/macro_util.cpp
+++ b/src/ast/macros/macro_util.cpp
@@ -185,6 +185,7 @@ bool macro_util::is_left_simple_macro(expr * n, unsigned num_decls, app_ref & he
         return true;
     }
     if (m_manager.is_not(n, lhs) && m_manager.is_eq(lhs, lhs, rhs) &&
+        m_manager.is_bool(lhs) &&
         is_macro_head(lhs, num_decls) &&
         !is_forbidden(to_app(lhs)->get_decl()) &&
         !occurs(to_app(lhs)->get_decl(), rhs)) {
@@ -224,6 +225,7 @@ bool macro_util::is_right_simple_macro(expr * n, unsigned num_decls, app_ref & h
         return true;
     }
     if (m_manager.is_not(n, n) && m_manager.is_eq(n, lhs, rhs) &&
+        m_manager.is_bool(lhs) &&
         is_macro_head(rhs, num_decls) &&
         !is_forbidden(to_app(rhs)->get_decl()) &&
         !occurs(to_app(rhs)->get_decl(), lhs)) {