mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

remove reference to deprecated code in cmd_context

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-02-14 17:00:02 -08:00
parent 5cdfa7cd1c
commit 96c05b0289
3 changed files with 10 additions and 32 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/solver/parallel_tactic.cpp
View file

@ -391,10 +391,15 @@ private:
log_branches(status);
}
void report_sat(solver_state& s) {
void report_sat(solver_state& s, solver* conquer) {
close_branch(s, l_true);
model_ref mdl;
s.get_solver().get_model(mdl);
if (conquer) {
conquer->get_model(mdl);
}
else {
s.get_solver().get_model(mdl);
}
if (mdl) {
std::lock_guard<std::mutex> lock(m_mutex);
if (&s.m() != &m_manager) {
@ -453,7 +458,7 @@ private:
if (canceled(s)) return;
switch (s.simplify()) {
case l_undef: break;
case l_true: report_sat(s); return;
case l_true: report_sat(s, nullptr); return;
case l_false: report_unsat(s); return;
}
if (canceled(s)) return;
@ -498,7 +503,7 @@ private:
break;
case l_true:
report_sat(s);
report_sat(s, conquer.get());
if (conquer) {
collect_statistics(*conquer.get());
}