From 491d990ed1b1f9d84bd2880c63171a62fb471626 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 13 Jun 2026 08:38:58 -0700 Subject: [PATCH] use structured parameters Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 3 ++- src/smt/smt_solver.cpp | 4 +++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index e03ae8c07..ae5cef768 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -492,7 +492,8 @@ public: } sat::literal_vector lits; expr_ref_vector fmls(m); - if (!m_params.get_bool("cube.lookahead", false)) { + parallel_params pp(m_params); + if (!pp.cube_lookahead()) { sat::bool_var_vector candidates; unsigned search_lvl = m_solver.search_lvl(); for (sat::bool_var v : vars) { diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 3687f1194..dd03c3a6c 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -27,6 +27,7 @@ Notes: #include "params/smt_params.h" #include "params/smt_params_helper.hpp" #include "solver/solver_na2as.h" +#include "solver/parallel_params.hpp" #include "solver/mus.h" #include @@ -436,7 +437,8 @@ namespace { expr_ref_vector cube(expr_ref_vector& vars, unsigned cutoff) override { ast_manager& m = get_manager(); - if (!get_params().get_bool("cube.lookahead", false)) { + parallel_params pp(get_params()); + if (!pp.cube_lookahead()) { auto& ctx = m_context.get_context(); expr_mark selected_vars; for (expr* v : vars)