mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

bv_bounds: fix crash in push() when realloc happened

Browse source
This commit is contained in:
Nuno Lopes 2016-02-19 11:06:22 +00:00
parent 121b3b60f3
commit c618838ed9
1 changed files with 11 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/tactic/bv/bv_bounds_tactic.cpp
View file

@ -152,10 +152,12 @@ std::ostream& operator<<(std::ostream& o, const interval& I) {
class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
ast_manager& m;
bv_util m_bv;
vector<obj_map<expr, interval> > m_scopes;
obj_map<expr, interval> *m_bound;
typedef obj_map<expr, interval> map;
ast_manager& m;
bv_util m_bv;
vector<map> m_scopes;
map *m_bound;
bool is_bound(expr *e, expr*& v, interval& b) {
rational n;
@ -208,7 +210,7 @@ class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier {
public:
bv_bounds_simplifier(ast_manager& m) : m(m), m_bv(m) {
m_scopes.push_back(obj_map<expr, interval>());
m_scopes.push_back(map());
m_bound = &m_scopes.back();
}
@ -275,8 +277,11 @@ public:
virtual void push() {
TRACE("bv", tout << "push\n";);
m_scopes.push_back(*m_bound);
unsigned sz = m_scopes.size();
m_scopes.resize(sz + 1);
m_bound = &m_scopes.back();
m_bound->~map();
new (m_bound) map(m_scopes[sz - 1]);
}
virtual void pop(unsigned num_scopes) {