From bce903ae97a72b75e04efa841159054d642fc30b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 4 Jun 2021 15:52:38 -0700
Subject: [PATCH] #5324

---
 src/ast/normal_forms/pull_quant.cpp |  2 +-
 src/sat/smt/q_solver.cpp            | 11 ++++++++---
 2 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/src/ast/normal_forms/pull_quant.cpp b/src/ast/normal_forms/pull_quant.cpp
index 390d6f63b..e0e2de1f7 100644
--- a/src/ast/normal_forms/pull_quant.cpp
+++ b/src/ast/normal_forms/pull_quant.cpp
@@ -276,7 +276,7 @@ struct pull_quant::imp {
 
             if (is_exists(old_q)) {
                 result = m.mk_not(new_body);
-                result = m.mk_not(m.update_quantifier(old_q, exists_k, result));
+                result = m.mk_not(m.update_quantifier(old_q, forall_k, result));
                 if (m.proofs_enabled()) 
                     m.mk_rewrite(old_q, result);
                 return true;
diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp
index 66f1323cf..2caf0eb75 100644
--- a/src/sat/smt/q_solver.cpp
+++ b/src/sat/smt/q_solver.cpp
@@ -181,9 +181,14 @@ namespace q {
             return q_flat;
         proof_ref pr(m);
         expr_ref  new_q(m);
-        pull_quant pull(m);
-        pull(q, new_q, pr);
-        SASSERT(is_well_sorted(m, new_q));
+        if (is_forall(q)) {
+            pull_quant pull(m);
+            pull(q, new_q, pr);
+            SASSERT(is_well_sorted(m, new_q));
+        }
+        else {
+            new_q = q;
+        }
         q_flat = to_quantifier(new_q);
         m.inc_ref(q_flat);
         m.inc_ref(q);