mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix #3882 ?

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-09 11:31:29 -07:00
parent cc794a19bc
commit def2de69f4
1 changed files with 6 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/smt/smt_parallel.cpp
View file

@ -46,9 +46,11 @@ namespace smt {
ERROR_EX ERROR_EX
}; };
vector<smt_params> smt_params;
scoped_ptr_vector<ast_manager> pms; scoped_ptr_vector<ast_manager> pms;
scoped_ptr_vector<context> pctxs; scoped_ptr_vector<context> pctxs;
vector<expr_ref_vector> pasms; vector<expr_ref_vector> pasms;
ast_manager& m = ctx.m; ast_manager& m = ctx.m;
scoped_limits sl(m.limit()); scoped_limits sl(m.limit());
unsigned finished_id = UINT_MAX; unsigned finished_id = UINT_MAX;
@ -61,10 +63,13 @@ namespace smt {
throw default_exception("trace streams have to be off in parallel mode"); throw default_exception("trace streams have to be off in parallel mode");
for (unsigned i = 0; i < num_threads; ++i) {
smt_params.push_back(ctx.get_fparams());
}
for (unsigned i = 0; i < num_threads; ++i) { for (unsigned i = 0; i < num_threads; ++i) {
ast_manager* new_m = alloc(ast_manager, m, true); ast_manager* new_m = alloc(ast_manager, m, true);
pms.push_back(new_m); pms.push_back(new_m);
pctxs.push_back(alloc(context, *new_m, ctx.get_fparams(), ctx.get_params())); pctxs.push_back(alloc(context, *new_m, smt_params[i], ctx.get_params()));
context& new_ctx = *pctxs.back(); context& new_ctx = *pctxs.back();
context::copy(ctx, new_ctx, true); context::copy(ctx, new_ctx, true);
new_ctx.set_random_seed(i + ctx.get_fparams().m_random_seed); new_ctx.set_random_seed(i + ctx.get_fparams().m_random_seed);