From 34969b71ee246e7b7e1c3b13dd782ba19c630bcd Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 13 Sep 2022 19:58:32 -0700
Subject: [PATCH] #6340 again - reduce new assertions in fresh iteration

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_context.cpp | 42 ++++++++++++++++++++++++-----------------
 1 file changed, 25 insertions(+), 17 deletions(-)

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index bc8f9ea64..e318d4771 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3202,26 +3202,34 @@ namespace smt {
         flet<bool> _internalizing(m_internalizing_assertions, true);
         TRACE("internalize_assertions", tout << "internalize_assertions()...\n";);
         timeit tt(get_verbosity_level() >= 100, "smt.preprocessing");
-        reduce_assertions();
-        if (get_cancel_flag()) return;
-        if (!m_asserted_formulas.inconsistent()) {
-            unsigned qhead = m_asserted_formulas.get_qhead();
-            while (qhead < m_asserted_formulas.get_num_formulas()) {
-                if (get_cancel_flag()) {
-                    m_asserted_formulas.commit(qhead);
-                    return;
+        unsigned qhead = 0;
+        do {
+            reduce_assertions();
+            if (get_cancel_flag()) 
+                return;
+            qhead = m_asserted_formulas.get_qhead();
+            if (!m_asserted_formulas.inconsistent()) {
+                unsigned sz = m_asserted_formulas.get_num_formulas();
+                while (qhead < sz) {
+                    if (get_cancel_flag()) {
+                        m_asserted_formulas.commit(qhead);
+                        return;
+                    }
+                    expr * f   = m_asserted_formulas.get_formula(qhead);
+                    proof * pr = m_asserted_formulas.get_formula_proof(qhead);
+                    SASSERT(!pr || f == m.get_fact(pr));
+                    internalize_assertion(f, pr, 0);
+                    qhead++;
                 }
-                expr * f   = m_asserted_formulas.get_formula(qhead);
-                proof * pr = m_asserted_formulas.get_formula_proof(qhead);
-                SASSERT(!pr || f == m.get_fact(pr));
-                internalize_assertion(f, pr, 0);
-                qhead++;
+                m_asserted_formulas.commit();
+            }
+            if (m_asserted_formulas.inconsistent() && !inconsistent()) {
+                asserted_inconsistent();
+                break;
             }
-            m_asserted_formulas.commit();
-        }
-        if (m_asserted_formulas.inconsistent() && !inconsistent()) {
-            asserted_inconsistent();
         }
+        while (qhead < m_asserted_formulas.get_num_formulas());
+
         TRACE("internalize_assertions", tout << "after internalize_assertions()...\n";
               tout << "inconsistent: " << inconsistent() << "\n";);
         TRACE("after_internalize_assertions", display(tout););