diff --git a/src/tactic/core/symmetry_reduce_tactic.cpp b/src/tactic/core/symmetry_reduce_tactic.cpp
index 784686a5e..33d6e976f 100644
--- a/src/tactic/core/symmetry_reduce_tactic.cpp
+++ b/src/tactic/core/symmetry_reduce_tactic.cpp
@@ -231,16 +231,15 @@ private:
     bool merge_colors(app_map const& colors1, app_map& colors2) {
         pair_map recolor;
         unsigned num_colors = 0, v1 = 0, v2 = 0, w = 0, old_max = 0;
-        app_map::iterator it = colors2.begin(), end = colors2.end();
-        for (; it != end; ++it) {
-            app* a = it->m_key;
-            v1 = it->m_value;
+        for (auto & kv : colors2) {
+            app* a = kv.m_key;
+            v1 = kv.m_value;
             VERIFY(colors1.find(a, v2));
             if (recolor.find(u_pair(v1, v2), w)) {
-                it->m_value = w;
+                kv.m_value = w;
             }
             else {
-                it->m_value = num_colors;
+                kv.m_value = num_colors;
                 recolor.insert(u_pair(v1, v2), num_colors++);
             }
             if (v1 > old_max) old_max = v1;
@@ -267,7 +266,8 @@ private:
             }
             m_app2sortid.insert(n, id);
         }
-        void operator()(quantifier * n) {}
+        void operator()(quantifier * n) {
+        }
         void operator()(var * n) {}
     };
 
@@ -278,10 +278,9 @@ private:
     }
 
     void compute_inv_app(app_map const& map, inv_app_map& inv_map) {
-        app_map::iterator it = map.begin(), end = map.end();
-        for (; it != end; ++it) {
-            app* t = it->m_key;
-            unsigned n = it->m_value;
+        for (auto & kv : map) {
+            app* t = kv.m_key;
+            unsigned n = kv.m_value;
             if (is_uninterpreted(t)) {
                 inv_app_map::entry* e = inv_map.insert_if_not_there2(n, ptr_vector<app>());
                 e->get_data().m_value.push_back(t);
@@ -635,6 +634,7 @@ void symmetry_reduce_tactic::operator()(goal_ref const & g,
                                         goal_ref_buffer & result) {
     fail_if_proof_generation("symmetry_reduce", g);
     fail_if_unsat_core_generation("symmetry_reduce", g);
+    fail_if_has_quantifiers("symmetry_reduce", g);
     result.reset();
     (*m_imp)(*(g.get()));
     g->inc_depth();
diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp
index 4c5031d32..32197107b 100644
--- a/src/tactic/tactic.cpp
+++ b/src/tactic/tactic.cpp
@@ -236,3 +236,13 @@ void fail_if_model_generation(char const * tactic_name, goal_ref const & in) {
         throw tactic_exception(std::move(msg));
     }
 }
+
+void fail_if_has_quantifiers(char const* tactic_name, goal_ref const& g) {
+    for (unsigned i = 0; i < g->size(); ++i)
+        if (has_quantifiers(g->form(i))) {
+            std::string msg = tactic_name;
+            msg += " does not apply to quantified goals";
+            throw tactic_exception(std::move(msg));
+        }
+}
+
diff --git a/src/tactic/tactic.h b/src/tactic/tactic.h
index dd6557dcc..41fe1d040 100644
--- a/src/tactic/tactic.h
+++ b/src/tactic/tactic.h
@@ -125,5 +125,6 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, p
 void fail_if_proof_generation(char const * tactic_name, goal_ref const & in);
 void fail_if_unsat_core_generation(char const * tactic_name, goal_ref const & in);
 void fail_if_model_generation(char const * tactic_name, goal_ref const & in);
+void fail_if_has_quantifiers(char const* tactic_name, goal_ref const& in);
 
 #endif