mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

change behavior on allocation excess to process exit to avoid memory smashes on exception unsafe code blocks. Fixes issue #175

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2015-09-02 16:12:19 -07:00
parent fdef17683a
commit b4d0e6076e
2 changed files with 17 additions and 16 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/tactic/arith/eq2bv_tactic.cpp
View file

@ -258,11 +258,21 @@ public:
}
}
bool is_var_const_pair(expr* e, expr* c, unsigned& k) {
rational r;
if (is_uninterp_const(e) && a.is_numeral(c, r) && r.is_unsigned() && !m_nonfd.is_marked(e)) {
k = r.get_unsigned();
return true;
}
else {
return false;
}
}
bool is_upper(expr* f) {
expr* e1, *e2;
rational r;
if ((a.is_le(f, e1, e2) || a.is_ge(f, e2, e1)) &&
is_uninterp_const(e1) && a.is_numeral(e2, r) && r.is_unsigned() && !m_nonfd.is_marked(e1)) {
unsigned k;
if ((a.is_le(f, e1, e2) || a.is_ge(f, e2, e1)) && is_var_const_pair(e1, e2, k)) {
SASSERT(m_bounds.has_upper(e1));
return true;
}
@ -271,9 +281,8 @@ public:
bool is_lower(expr* f) {
expr* e1, *e2;
rational r;
if ((a.is_le(f, e1, e2) || a.is_ge(f, e2, e1)) &&
is_uninterp_const(e2) && a.is_numeral(e1, r) && r.is_unsigned() && !m_nonfd.is_marked(e2)) {
unsigned k;
if ((a.is_le(f, e1, e2) || a.is_ge(f, e2, e1)) && is_var_const_pair(e2, e1, k)) {
SASSERT(m_bounds.has_lower(e2));
return true;
}
@ -284,7 +293,6 @@ public:
return is_lower(f) || is_upper(f);
}
void collect_fd(expr* f) {
if (is_bound(f)) return;
m_todo.push_back(f);