mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-26 04:56:03 +00:00
Code Activity

ensure that max-conflicts is propagated to nra-solver

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-08-17 13:58:31 -07:00
parent e76f9f2615
commit f486617f81
2 changed files with 6 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/math/lp/nla_core.cpp
View file

@ -38,7 +38,7 @@ core::core(lp::lar_solver& s, params_ref const& p, reslimit & lim) :
m_grobner(this), m_grobner(this),
m_emons(m_evars), m_emons(m_evars),
m_use_nra_model(false), m_use_nra_model(false),
m_nra(s, m_nra_lim, *this), m_nra(s, m_nra_lim, *this, p),
m_throttle(lra.trail(), m_throttle(lra.trail(),
lra.settings().stats()) { lra.settings().stats()) {
m_nlsat_delay_bound = lp_settings().nlsat_delay(); m_nlsat_delay_bound = lp_settings().nlsat_delay();
@ -1561,6 +1561,9 @@ lbool core::check() {
if (no_effect() && params().arith_nl_nra()) { if (no_effect() && params().arith_nl_nra()) {
scoped_limits sl(m_reslim); scoped_limits sl(m_reslim);
sl.push_child(&m_nra_lim); sl.push_child(&m_nra_lim);
params_ref p;
p.set_uint("max_conflicts", lp_settings().m_max_conflicts);
m_nra.updt_params(p);
ret = m_nra.check(); ret = m_nra.check();
lp_settings().stats().m_nra_calls++; lp_settings().stats().m_nra_calls++;
} }

2
src/smt/theory_lra.cpp
View file

@ -1427,6 +1427,8 @@ public:
void init_search_eh() { void init_search_eh() {
m_arith_eq_adapter.init_search_eh(); m_arith_eq_adapter.init_search_eh();
m_num_conflicts = 0; m_num_conflicts = 0;
if (m_solver)
lp().settings().m_max_conflicts = ctx().get_fparams().m_max_conflicts;
} }
bool can_get_value(theory_var v) const { bool can_get_value(theory_var v) const {