diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp
index ed19469a7..f2320f34a 100644
--- a/src/sat/smt/q_solver.cpp
+++ b/src/sat/smt/q_solver.cpp
@@ -258,6 +258,10 @@ namespace q {
                 m_expanded.push_back(r);
                 return true;
             }            
+            if (is_forall(q)  != is_forall(r)) {
+                m_expanded.push_back(r);
+                return true;
+            }
             q = to_quantifier(r);
         }
         if (is_forall(q))