mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

fix #5362

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-06-22 12:26:27 -07:00
parent f3737f6831
commit 55daa2424c
2 changed files with 9 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -36,7 +36,7 @@ core::core(lp::lar_solver& s, reslimit & lim) :
m_emons(m_evars),
m_reslim(lim),
m_use_nra_model(false),
m_nra(s, lim, *this)
m_nra(s, m_nra_lim, *this)
{
m_nlsat_delay = lp_settings().nlsat_delay();
}
@ -1563,10 +1563,15 @@ bool core::should_run_bounded_nlsat() {
lbool core::bounded_nlsat() {
params_ref p;
lbool ret;
p.set_uint("max_conflicts", 100);
scoped_rlimit sr(m_reslim, 100000);
m_nra.updt_params(p);
lbool ret = m_nra.check();
{
scoped_limits sl(m_reslim);
sl.push_child(&m_nra_lim);
scoped_rlimit sr(m_nra_lim, 100000);
ret = m_nra.check();
}
p.set_uint("max_conflicts", UINT_MAX);
m_nra.updt_params(p);
m_stats.m_nra_calls++;

1
src/math/lp/nla_core.h
View file

@ -175,6 +175,7 @@ private:
svector<lpvar> m_add_buffer;
mutable lp::u_set m_active_var_set;
lp::u_set m_rows;
reslimit m_nra_lim;
public:
reslimit& m_reslim;
bool m_use_nra_model;