From 550852bc62cb6d4b153f2392cf1754faeec27259 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 5 Apr 2020 13:49:26 -0700
Subject: [PATCH] fix #3765

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/ast.cpp                |  2 +-
 src/muz/spacer/spacer_util.cpp | 12 ++++++------
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 0306f7a37..c410e897e 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1501,7 +1501,7 @@ ast_manager::~ast_manager() {
     }
     m_plugins.reset();
     while (!m_ast_table.empty()) {
-        DEBUG_CODE(std::cout << "ast_manager LEAKED: " << m_ast_table.size() << std::endl;);
+        DEBUG_CODE(IF_VERBOSE(0, verbose_stream() << "ast_manager LEAKED: " << m_ast_table.size() << std::endl););
         ptr_vector<ast> roots;
         ast_mark mark;
         for (ast * n : m_ast_table) {
diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp
index 8ade9e10a..97a7262c2 100644
--- a/src/muz/spacer/spacer_util.cpp
+++ b/src/muz/spacer/spacer_util.cpp
@@ -387,7 +387,7 @@ namespace {
 
             if (!is_true && !m.is_false(v)) return;
 
-            expr *na = nullptr, *f1 = nullptr, *f2 = nullptr, *f3 = nullptr;
+            expr* na = nullptr, * f1 = nullptr, * f2 = nullptr, * f3 = nullptr;
 
             SASSERT(!m.is_false(a));
             if (m.is_true(a)) {
@@ -404,8 +404,8 @@ namespace {
             }
             else if (m.is_distinct(a)) {
                 if (!is_true) {
-                    f1 = qe::project_plugin::pick_equality(m, m_model, a);
-                    m_todo.push_back(f1);
+                    expr_ref tmp = qe::project_plugin::pick_equality(m, m_model, a);
+                    m_todo.push_back(tmp);
                 }
                 else if (a->get_num_args() == 2) {
                     add_literal(a, out);
@@ -497,15 +497,15 @@ namespace {
             if (m_visited.is_marked(e) || !is_app(e)) return;
 
             m_todo.push_back(e);
-            do {
+            for (unsigned i = 0; i < m_todo.size(); ++i) {
                 e = m_todo.back();
                 if (!is_app(e)) continue;
-                app * a = to_app(e);
+                app* a = to_app(e);
                 m_todo.pop_back();
                 process_app(a, out);
                 m_visited.mark(a, true);
             } 
-            while (!m_todo.empty());
+            m_todo.reset();
         }
 
         bool pick_implicant(const expr_ref_vector &in, expr_ref_vector &out) {