From 16ef89905d8b5702347021271bdd071d5bf80277 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nuno.lopes@tecnico.ulisboa.pt>
Date: Wed, 14 Sep 2022 11:50:53 +0100
Subject: [PATCH] fix infinite loop in internalize

---
 src/api/api_stats.cpp   |  2 +-
 src/smt/smt_context.cpp | 35 +++++++++++++++++------------------
 2 files changed, 18 insertions(+), 19 deletions(-)

diff --git a/src/api/api_stats.cpp b/src/api/api_stats.cpp
index c90850404..a3b8bacf0 100644
--- a/src/api/api_stats.cpp
+++ b/src/api/api_stats.cpp
@@ -28,7 +28,7 @@ extern "C" {
         RESET_ERROR_CODE();
         std::ostringstream buffer;
         to_stats_ref(s).display_smt2(buffer);
-        std::string result = buffer.str();
+        std::string result = std::move(buffer).str();
         // Hack for removing the trailing '\n'
         SASSERT(result.size() > 0);
         result.resize(result.size()-1);
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index e318d4771..1bae0ef86 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3207,26 +3207,25 @@ namespace smt {
             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++;
-                }
-                m_asserted_formulas.commit();
-            }
-            if (m_asserted_formulas.inconsistent() && !inconsistent()) {
-                asserted_inconsistent();
+            if (m_asserted_formulas.inconsistent()) {
+                if (!inconsistent())
+                    asserted_inconsistent();
                 break;
             }
+            qhead = m_asserted_formulas.get_qhead();
+            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;
+            }
+            m_asserted_formulas.commit();
         }
         while (qhead < m_asserted_formulas.get_num_formulas());