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)) {