mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

fix #3765

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-05 13:49:26 -07:00
parent e246f6649e
commit 550852bc62
2 changed files with 7 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/ast.cpp
View file

@ -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) {

12
src/muz/spacer/spacer_util.cpp
View file

@ -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) {