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

fix #3488

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-23 10:57:15 -07:00
parent bb451c39c9
commit acb9376ea0
1 changed files with 8 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/sat/sat_solver.cpp
View file

@ -1327,6 +1327,9 @@ namespace sat {
} }
lbool solver::check_par(unsigned num_lits, literal const* lits) { lbool solver::check_par(unsigned num_lits, literal const* lits) {
if (!rlimit().inc()) {
return l_undef;
}
scoped_ptr_vector<i_local_search> ls; scoped_ptr_vector<i_local_search> ls;
scoped_ptr_vector<solver> uw; scoped_ptr_vector<solver> uw;
int num_extra_solvers = m_config.m_num_threads - 1; int num_extra_solvers = m_config.m_num_threads - 1;
@ -1442,6 +1445,11 @@ namespace sat {
} }
}; };
if (!rlimit().inc()) {
set_par(nullptr, 0);
return l_undef;
}
vector<std::thread> threads(num_threads); vector<std::thread> threads(num_threads);
for (int i = 0; i < num_threads; ++i) { for (int i = 0; i < num_threads; ++i) {
threads[i] = std::thread([&, i]() { worker_thread(i); }); threads[i] = std::thread([&, i]() { worker_thread(i); });