From 10dc8d7313e5c5ff0e71b7d94e492b6f9a201f7a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 12 Jan 2022 12:49:06 -0800
Subject: [PATCH] #5753

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

diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp
index d58b9b4d0..762b2ca4f 100644
--- a/src/sat/smt/q_solver.cpp
+++ b/src/sat/smt/q_solver.cpp
@@ -65,6 +65,7 @@ namespace q {
     }
 
     sat::check_result solver::check() {
+        std::cout << "check\n";
         if (ctx.get_config().m_ematching && m_ematch())
             return sat::check_result::CR_CONTINUE;
 
@@ -230,10 +231,9 @@ namespace q {
     bool solver::expand(quantifier* q) {
         expr_ref r(q, m);
         proof_ref pr(m);
-        ctx.rewrite(r);
         m_der(r, r, pr);
         m_expanded.reset();
-        if (r != q) {
+        if (q != r) {
             ctx.rewrite(r);
             m_expanded.push_back(r);
             return true;