mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-20 11:22:04 +00:00
Code Activity

fix optimization pre-processing reported by Gereon Kremer

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-04-09 20:58:57 -07:00
parent 6e57015a12
commit 2033719c14
1 changed files with 16 additions and 12 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -191,15 +191,18 @@ public:
expr* c = it->m_key; expr* c = it->m_key;
bool strict; bool strict;
rational r; rational r;
if (m_bounds.has_lower(c, r, strict)) { expr_ref fml(m);
if (m_bounds.has_lower(c, r, strict) && !r.is_neg()) {
SASSERT(!strict); SASSERT(!strict);
expr* d = m_fd.find(c); expr* d = m_fd.find(c);
g->assert_expr(bv.mk_ule(bv.mk_numeral(r, m.get_sort(d)), d), m_bounds.lower_dep(c)); fml = bv.mk_ule(bv.mk_numeral(r, m.get_sort(d)), d);
g->assert_expr(fml, m_bounds.lower_dep(c));
} }
if (m_bounds.has_upper(c, r, strict)) { if (m_bounds.has_upper(c, r, strict) && !r.is_neg()) {
SASSERT(!strict); SASSERT(!strict);
expr* d = m_fd.find(c); expr* d = m_fd.find(c);
g->assert_expr(bv.mk_ule(d, bv.mk_numeral(r, m.get_sort(d))), m_bounds.upper_dep(c)); fml = bv.mk_ule(d, bv.mk_numeral(r, m.get_sort(d)));
g->assert_expr(fml, m_bounds.upper_dep(c));
} }
} }
g->inc_depth(); g->inc_depth();
@ -247,6 +250,7 @@ public:
} }
unsigned p = next_power_of_two(it->m_value); unsigned p = next_power_of_two(it->m_value);
if (p <= 1) p = 2; if (p <= 1) p = 2;
if (it->m_value == p) p *= 2;
unsigned n = log2(p); unsigned n = log2(p);
app* z = m.mk_fresh_const("z", bv.mk_sort(n)); app* z = m.mk_fresh_const("z", bv.mk_sort(n));
m_trail.push_back(z); m_trail.push_back(z);