diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index 3555e5bdc..aeccd2633 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -567,6 +567,7 @@ namespace datalog {
             m_rule_properties.check_uninterpreted_free();
             break;
         case QPDR_ENGINE:
+            std::cout << "QD\n";
             m_rule_properties.collect(r);
             m_rule_properties.check_for_negated_predicates();
             m_rule_properties.check_uninterpreted_free();
diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp
index 455e02e45..619f88e3b 100644
--- a/src/muz/base/rule_properties.cpp
+++ b/src/muz/base/rule_properties.cpp
@@ -142,7 +142,7 @@ void rule_properties::check_existential_tail() {
             todo.push_back(e2);
         }
         else if (is_quantifier(e)) {
-            todo.push_back(to_quantifier(e)->get_expr());
+            tocheck.push_back(to_quantifier(e)->get_expr());
         }
         else if ((m.is_eq(e, e1, e2) || m.is_iff(e, e1, e2)) && 
                  m.is_true(e1)) {