From 637ddf9397b87655c8d750fc21201b8eec582619 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 16 Jan 2022 18:09:38 -0800
Subject: [PATCH] fix #5777

latest issue
---
 src/sat/smt/q_solver.cpp | 4 ++++
 1 file changed, 4 insertions(+)

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