From 5127569aaf062585879aaa5124a26d15a8324b2f Mon Sep 17 00:00:00 2001 From: Ilana Shapiro Date: Mon, 3 Nov 2025 10:47:58 -0800 Subject: [PATCH] patch fix for default manager construction so it can be used to create the param tuning context without segfault --- src/smt/smt_parallel.cpp | 6 +++++- src/smt/smt_parallel.h | 3 +-- 2 files changed, 6 insertions(+), 3 deletions(-) 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();