mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
patch bounds normalization bug found by dvitek
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
4732e03259
commit
a8fb15ce2c
|
@ -123,21 +123,41 @@ struct bv_size_reduction_tactic::imp {
|
|||
negated = true;
|
||||
f = to_app(f)->get_arg(0);
|
||||
}
|
||||
|
||||
|
||||
if (m_util.is_bv_sle(f, lhs, rhs)) {
|
||||
bv_sz = m_util.get_bv_size(lhs);
|
||||
if (is_uninterp_const(lhs) && m_util.is_numeral(rhs, val, bv_sz)) {
|
||||
TRACE("bv_size_reduction", tout << (negated?"not ":"") << mk_ismt2_pp(f, m) << std::endl; );
|
||||
// v <= k
|
||||
if (negated) update_signed_lower(to_app(lhs), val+numeral(1));
|
||||
val = m_util.norm(val, bv_sz, true);
|
||||
if (negated) {
|
||||
val += numeral(1);
|
||||
if (m_util.norm(val, bv_sz, true) != val) {
|
||||
// bound is infeasible.
|
||||
}
|
||||
else {
|
||||
update_signed_lower(to_app(lhs), val);
|
||||
}
|
||||
}
|
||||
else update_signed_upper(to_app(lhs), val);
|
||||
}
|
||||
else if (is_uninterp_const(rhs) && m_util.is_numeral(lhs, val, bv_sz)) {
|
||||
TRACE("bv_size_reduction", tout << (negated?"not ":"") << mk_ismt2_pp(f, m) << std::endl; );
|
||||
// k <= v
|
||||
if (negated) update_signed_upper(to_app(rhs), val-numeral(1));
|
||||
val = m_util.norm(val, bv_sz, true);
|
||||
if (negated) {
|
||||
val -= numeral(1);
|
||||
if (m_util.norm(val, bv_sz, true) != val) {
|
||||
// bound is infeasible.
|
||||
}
|
||||
else {
|
||||
update_signed_upper(to_app(lhs), val);
|
||||
}
|
||||
}
|
||||
else update_signed_lower(to_app(rhs), val);
|
||||
}
|
||||
}
|
||||
|
||||
#if 0
|
||||
else if (m_util.is_bv_ule(f, lhs, rhs)) {
|
||||
if (is_uninterp_const(lhs) && m_util.is_numeral(rhs, val, bv_sz)) {
|
||||
|
|
Loading…
Reference in a new issue