mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

Revert "Fixed bug in par-or tactic."

Browse source 
This reverts commit 89b6589a37.
This commit is contained in:
Christoph M. Wintersteiger 2015-10-28 18:42:16 +00:00
parent 1523626a2b
commit c537084056
1 changed files with 315 additions and 316 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/tactic/tactical.cpp
View file

@ -573,11 +573,10 @@ 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 (successful && finished_id == UINT_MAX) { if (finished_id == UINT_MAX) {
finished_id = i; finished_id = i;
first = true; first = true;
} }