mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 02:42:02 +00:00
Code Activity

Fixed bug in par-or tactic.

Browse source 
Fixes #269.
This commit is contained in:
Christoph M. Wintersteiger 2015-10-28 15:34:30 +00:00
parent 2218f86f03
commit 89b6589a37
1 changed files with 316 additions and 315 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/tactic/tactical.cpp
View file

@ -573,10 +573,11 @@ public:
try { try {
t(in_copy, _result, _mc, _pc, _core); t(in_copy, _result, _mc, _pc, _core);
bool successful = is_decided(_result);
bool first = false; bool first = false;
#pragma omp critical (par_tactical) #pragma omp critical (par_tactical)
{ {
if (finished_id == UINT_MAX) { if (successful && finished_id == UINT_MAX) {
finished_id = i; finished_id = i;
first = true; first = true;
} }