diff --git a/src/smt/smt_parallel.cpp b/src/smt/smt_parallel.cpp index 8de490cf7..f6049405d 100644 --- a/src/smt/smt_parallel.cpp +++ b/src/smt/smt_parallel.cpp @@ -317,7 +317,11 @@ namespace smt { } parallel::param_generator::param_generator(parallel& p) - : p(p), b(p.m_batch_manager), m_p(p.ctx.get_params()), m_l2g(m, p.ctx.m) { + : b(p.m_batch_manager), m_p(p.ctx.get_params()), m_l2g(m, p.ctx.m) { + // patch fix so that ctx = alloc(context, m, p.ctx.get_fparams(), m_p); doesn't crash due to some issue with default construction of m + ast_translation m_g2l(p.ctx.m, m); + m_g2l(p.ctx.m.mk_true()); + ctx = alloc(context, m, p.ctx.get_fparams(), m_p); context::copy(p.ctx, *ctx, true); // don't share initial units diff --git a/src/smt/smt_parallel.h b/src/smt/smt_parallel.h index 27111c0bd..d5980e8c3 100644 --- a/src/smt/smt_parallel.h +++ b/src/smt/smt_parallel.h @@ -118,11 +118,9 @@ namespace smt { using param_value = std::variant; using param_values = vector>; - parallel &p; batch_manager &b; ast_manager m; scoped_ptr ctx; - ast_translation m_l2g; unsigned N = 4; // number of prefix permutations to test (including current) unsigned m_max_prefix_conflicts = 1000; @@ -131,6 +129,7 @@ namespace smt { vector m_recorded_cubes; params_ref m_p; param_values m_param_state; + ast_translation m_l2g; params_ref apply_param_values(param_values const &pv); void init_param_state();