From 4b1419261faee8b9b3122f95e54b5ea328529af3 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 21 Mar 2022 16:23:43 -0700
Subject: [PATCH] #5778

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

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