mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-07 14:43:23 +00:00
Code Activity

fix #3026

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-16 15:48:46 -10:00
parent ccbc4a4943
commit d25db0d3e9
1 changed files with 9 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -314,15 +314,12 @@ namespace {
} }
~bv_bounds_simplifier() override { ~bv_bounds_simplifier() override {
for (unsigned i = 0, e = m_expr_vars.size(); i < e; ++i) { for (auto* v : m_expr_vars) dealloc(v);
dealloc(m_expr_vars[i]); for (auto* b : m_bound_exprs) dealloc(b);
}
for (unsigned i = 0, e = m_bound_exprs.size(); i < e; ++i) {
dealloc(m_bound_exprs[i]);
}
} }
bool assert_expr(expr * t, bool sign) override { bool assert_expr(expr * t, bool sign) override {
TRACE("bv", tout << expr_ref(t, m) << "\n";);
while (m.is_not(t, t)) { while (m.is_not(t, t)) {
sign = !sign; sign = !sign;
} }
@ -331,8 +328,11 @@ namespace {
expr* t1; expr* t1;
if (is_bound(t, t1, b)) { if (is_bound(t, t1, b)) {
SASSERT(!m_bv.is_numeral(t1)); SASSERT(!m_bv.is_numeral(t1));
if (sign) if (sign) {
VERIFY(b.negate(b)); if (!b.negate(b)) {
return false;
}
}
TRACE("bv", tout << (sign?"(not ":"") << mk_pp(t, m) << (sign ? ")" : "") << ": " << mk_pp(t1, m) << " in " << b << "\n";); TRACE("bv", tout << (sign?"(not ":"") << mk_pp(t, m) << (sign ? ")" : "") << ": " << mk_pp(t1, m) << " in " << b << "\n";);
map::obj_map_entry* e = m_bound.find_core(t1); map::obj_map_entry* e = m_bound.find_core(t1);