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

fix #3590

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-31 15:43:33 -07:00
parent ae447cfdad
commit 4ee0462beb
2 changed files with 7 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/solver/parallel_tactic.cpp
View file

@ -33,6 +33,7 @@ Notes:
#include <cmath> #include <cmath>
#include <condition_variable> #include <condition_variable>
#include "util/scoped_ptr_vector.h" #include "util/scoped_ptr_vector.h"
#include "ast/ast_pp.h"
#include "ast/ast_util.h" #include "ast/ast_util.h"
#include "ast/ast_translation.h" #include "ast/ast_translation.h"
#include "solver/solver.h" #include "solver/solver.h"
@ -141,6 +142,8 @@ class parallel_tactic : public tactic {
for (auto* t : m_active) dealloc(t); for (auto* t : m_active) dealloc(t);
m_tasks.reset(); m_tasks.reset();
m_active.reset(); m_active.reset();
m_num_waiters = 0;
m_shutdown = false;
} }
std::ostream& display(std::ostream& out) { std::ostream& display(std::ostream& out) {
@ -696,6 +699,7 @@ public:
} }
void operator ()(const goal_ref & g,goal_ref_buffer & result) override { void operator ()(const goal_ref & g,goal_ref_buffer & result) override {
cleanup();
fail_if_proof_generation("parallel-tactic", g); fail_if_proof_generation("parallel-tactic", g);
ast_manager& m = g->m(); ast_manager& m = g->m();
solver* s = m_solver->translate(m, m_params); solver* s = m_solver->translate(m, m_params);
@ -744,6 +748,8 @@ public:
void cleanup() override { void cleanup() override {
m_queue.reset(); m_queue.reset();
m_models.reset();
m_stats.reset();
} }
tactic* translate(ast_manager& m) override { tactic* translate(ast_manager& m) override {

2
src/tactic/tactic.cpp
View file

@ -178,7 +178,7 @@ lbool check_sat(tactic & t, goal_ref & g, model_ref & md, labels_vec & labels, p
if (r.size() > 0) { if (r.size() > 0) {
pr = r[0]->pr(0); pr = r[0]->pr(0);
TRACE("tactic", tout << pr << "\n";); CTRACE("tactic", pr, tout << pr << "\n";);
} }