From def2de69f49e1ae1a4e4922446b20e8e407f8c5a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 9 Apr 2020 11:31:29 -0700
Subject: [PATCH] fix #3882 ?

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_parallel.cpp | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

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> smt_params;
         scoped_ptr_vector<ast_manager> pms;
         scoped_ptr_vector<context> pctxs;
         vector<expr_ref_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);