mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 22:33:40 +00:00
Code Activity

bp

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-05 07:10:16 -08:00
parent 67cc2a8cf0
commit 7b2f6791bc
1 changed files with 6 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/smt/theory_lra.cpp
View file

@ -2394,21 +2394,15 @@ public:
bool bound_is_interesting(unsigned vi, lp::lconstraint_kind kind, const rational & bval) const { bool bound_is_interesting(unsigned vi, lp::lconstraint_kind kind, const rational & bval) const {
theory_var v = lp().local_to_external(vi); theory_var v = lp().local_to_external(vi);
if (v == null_theory_var) return false; if (v == null_theory_var)
return false;
if (m_unassigned_bounds[v] == 0 || m_bounds.size() <= static_cast<unsigned>(v)) { if (m_unassigned_bounds[v] == 0 || m_bounds.size() <= static_cast<unsigned>(v)) {
return false; return false;
} }
lp_bounds const& bounds = m_bounds[v]; for (lp_api::bound* b : m_bounds[v]) {
for (unsigned i = 0; i < bounds.size(); ++i) { if (ctx().get_assignment(b->get_bv()) == l_undef &&
lp_api::bound* b = bounds[i]; null_literal != is_bound_implied(kind, bval, *b))
if (ctx().get_assignment(b->get_bv()) != l_undef) {
continue;
}
literal lit = is_bound_implied(kind, bval, *b);
if (lit == null_literal) {
continue;
}
return true; return true;
} }
return false; return false;