diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index 3bec0738b..1bf95ad39 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -582,6 +582,7 @@ namespace datalog {
             m_rule_properties.check_existential_tail();
             m_rule_properties.check_for_negated_predicates();
             m_rule_properties.check_uninterpreted_free();
+            m_rule_properties.check_quantifier_free(exists_k);
             break;
         case BMC_ENGINE:
             m_rule_properties.collect(r);
diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp
index 14f641c44..7923eeae4 100644
--- a/src/muz/base/rule_properties.cpp
+++ b/src/muz/base/rule_properties.cpp
@@ -72,6 +72,27 @@ void rule_properties::check_quantifier_free() {
     }
 }
 
+static const std::string qkind_str(quantifier_kind qkind) {
+    switch(qkind) {
+    case forall_k: return "FORALL";
+    case exists_k: return "EXISTS";
+    case lambda_k: return "LAMBDA";
+    }
+}
+
+void rule_properties::check_quantifier_free(quantifier_kind qkind) {
+    for (auto &kv : m_quantifiers) {
+        if (kv.get_key().get_kind() == qkind) {
+            rule *r = kv.get_value();
+            std::stringstream stm;
+            stm << "cannot process " << qkind_str(qkind) << " quantifier in rule ";
+            r->display(m_ctx, stm);
+            throw default_exception(stm.str());
+        } 
+    }
+
+}
+
 void rule_properties::check_for_negated_predicates() {
     if (!m_negative_rules.empty()) {
         rule* r = m_negative_rules[0];
@@ -235,5 +256,7 @@ void rule_properties::reset() {
     m_negative_rules.reset();
     m_inf_sort.reset();
     m_collected = false;
+    m_is_monotone = true;
+    m_generate_proof = false;
 }
 
diff --git a/src/muz/base/rule_properties.h b/src/muz/base/rule_properties.h
index 6946a7854..1e3bb307a 100644
--- a/src/muz/base/rule_properties.h
+++ b/src/muz/base/rule_properties.h
@@ -27,6 +27,7 @@ Notes:
 #include "ast/array_decl_plugin.h"
 #include "ast/arith_decl_plugin.h"
 #include "muz/base/dl_rule.h"
+#include "ast/expr_functors.h"
 
 namespace datalog {
     class rule_properties {
@@ -58,6 +59,7 @@ namespace datalog {
         void set_generate_proof(bool generate_proof) { m_generate_proof = generate_proof; } 
         void collect(rule_set const& r);
         void check_quantifier_free();
+        void check_quantifier_free(quantifier_kind qkind);
         void check_uninterpreted_free();
         void check_existential_tail();
         void check_for_negated_predicates();