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

fix lifetimes for crashes in #4525

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-07-21 12:53:46 -07:00
parent f17ead21f9
commit b1824fea10
1 changed files with 7 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/smt/theory_lra.cpp
View file

@ -935,7 +935,7 @@ public:
m_bp(*this), m_bp(*this),
m_bounded_range_idx(0), m_bounded_range_idx(0),
m_bounded_range_lit(null_literal), m_bounded_range_lit(null_literal),
m_bound_predicates(m), m_bound_terms(m),
m_bound_predicate(m) m_bound_predicate(m)
{ {
} }
@ -3935,8 +3935,9 @@ public:
}; };
unsigned m_bounded_range_idx; // current size of bounded range. unsigned m_bounded_range_idx; // current size of bounded range.
literal m_bounded_range_lit; // current bounded range literal literal m_bounded_range_lit; // current bounded range literal
expr_ref_vector m_bound_predicates; // predicates used for bounds expr_ref_vector m_bound_terms; // predicates used for bounds
expr_ref m_bound_predicate; expr_ref m_bound_predicate;
obj_map<expr, expr*> m_predicate2term; obj_map<expr, expr*> m_predicate2term;
obj_map<expr, bound_info> m_term2bound_info; obj_map<expr, bound_info> m_term2bound_info;
@ -4013,8 +4014,9 @@ public:
expr_ref lo(a.mk_ge(t, a.mk_int(offset - bi.m_range)), m); expr_ref lo(a.mk_ge(t, a.mk_int(offset - bi.m_range)), m);
mk_axiom(~m_bounded_range_lit, mk_literal(hi)); mk_axiom(~m_bounded_range_lit, mk_literal(hi));
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_terms.push_back(lo);
m_bound_predicates.push_back(hi); m_bound_terms.push_back(hi);
m_bound_terms.push_back(t);
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);
@ -4022,7 +4024,7 @@ public:
void setup() { void setup() {
m_bounded_range_lit = null_literal; m_bounded_range_lit = null_literal;
m_bound_predicates.reset(); m_bound_terms.reset();
m_bound_predicate = nullptr; m_bound_predicate = nullptr;
m_predicate2term.reset(); m_predicate2term.reset();
m_term2bound_info.reset(); m_term2bound_info.reset();