diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp
index 26d170fb8..2035cd533 100644
--- a/src/sat/smt/q_solver.cpp
+++ b/src/sat/smt/q_solver.cpp
@@ -41,11 +41,19 @@ namespace q {
         quantifier* q = to_quantifier(e);
 
         auto const& exp = expand(q);
-        if (exp.size() > 1) {
+        if (exp.size() > 1 && is_forall(q)) {
             for (expr* e : exp) 
                 add_clause(~l, ctx.internalize(e, l.sign(), false, false));                    
             return;
         }
+        if (exp.size() > 1 && is_exists(q)) {
+            sat::literal_vector lits;
+            lits.push_back(~l);
+            for (expr* e : exp)
+                lits.push_back(ctx.internalize(e, l.sign(), false, false));
+            add_clause(lits);
+            return;
+        }
 
         if (l.sign() == is_forall(e)) 
             add_clause(~l, skolemize(q));