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)