diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index bed009e0c..f591741a8 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -46,9 +46,11 @@ namespace smt { ERROR_EX }; + vector smt_params; scoped_ptr_vector pms; scoped_ptr_vector pctxs; vector pasms; + ast_manager& m = ctx.m; scoped_limits sl(m.limit()); unsigned finished_id = UINT_MAX; @@ -61,10 +63,13 @@ namespace smt { 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) { ast_manager* new_m = alloc(ast_manager, m, true); 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::copy(ctx, new_ctx, true); new_ctx.set_random_seed(i + ctx.get_fparams().m_random_seed);