mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-15 18:36:16 +00:00
Code Activity

fix tracking of bounds

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-06-15 17:36:11 -07:00
parent f882219081
commit 48d4d8d7af
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/theory_lra.cpp
View file

@ -3929,6 +3929,8 @@ public:
expr_ref lo(a.mk_ge(t, a.mk_int(bi.m_offset - bi.m_range)), m); expr_ref lo(a.mk_ge(t, a.mk_int(bi.m_offset - bi.m_range)), m);
assumptions.push_back(lo); assumptions.push_back(lo);
assumptions.push_back(hi); assumptions.push_back(hi);
m_predicate2term.insert(lo, t);
m_predicate2term.insert(hi, t);
IF_VERBOSE(10, verbose_stream() << lo << "\n" << hi << "\n"); IF_VERBOSE(10, verbose_stream() << lo << "\n" << hi << "\n");
} }
} }
@ -3978,7 +3980,6 @@ public:
mk_axiom(~m_bounded_range_lit, mk_literal(lo)); mk_axiom(~m_bounded_range_lit, mk_literal(lo));
m_bound_predicates.push_back(lo); m_bound_predicates.push_back(lo);
m_bound_predicates.push_back(hi); m_bound_predicates.push_back(hi);
IF_VERBOSE(10, verbose_stream() << "add " << lo << " " << hi << "\n");
m_predicate2term.insert(lo, t); m_predicate2term.insert(lo, t);
m_predicate2term.insert(hi, t); m_predicate2term.insert(hi, t);
m_term2bound_info.insert(t, bi); m_term2bound_info.insert(t, bi);