mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

generate lemmas from nla_intervals

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2019-06-14 17:47:03 -07:00
parent 3f6ecfb3b6
commit 8258e2a8fd
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_lra.cpp
View file

@ -2327,7 +2327,7 @@ public:
struct local_bound_propagator: public lp::lp_bound_propagator {
imp & m_imp;
local_bound_propagator(imp& i) : lp_bound_propagator(*i.m_solver, i.get_nla_solver()), m_imp(i) {}
local_bound_propagator(imp& i) : lp_bound_propagator(*i.m_solver), m_imp(i) {}
bool bound_is_interesting(unsigned j, lp::lconstraint_kind kind, const rational & v) override {
return m_imp.bound_is_interesting(j, kind, v);
@ -2375,7 +2375,7 @@ public:
m_params.reset();
m_explanation.clear();
local_bound_propagator bp(*this);
bp.explain_implied_bound(be);
lp().explain_implied_bound(be, bp);
}
CTRACE("arith", m_unassigned_bounds[v] == 0, tout << "missed bound\n";);
updt_unassigned_bounds(v, -1);