diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp
index 2bb7e2a30ca..7c1c1904091 100644
--- a/src/sat/smt/q_solver.cpp
+++ b/src/sat/smt/q_solver.cpp
@@ -262,6 +262,8 @@ namespace q {
                 m_expanded.push_back(r);
                 return true;
             }
+            if (r == q)
+                return false;
             q = to_quantifier(r);
         }
         if (is_forall(q))