mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
bv_bounds/ctx_simplify: improve handling of (ite x a b) where (not x) is proved to be false
This commit is contained in:
parent
73f93dbadb
commit
121b3b60f3
|
@ -36,6 +36,11 @@ struct interval {
|
|||
|
||||
explicit interval() : l(0), h(0), sz(0), tight(false) {}
|
||||
interval(const rational& l, const rational& h, unsigned sz, bool tight = false) : l(l), h(h), sz(sz), tight(tight) {
|
||||
// canonicalize full set
|
||||
if (is_wrapped() && l == h + rational::one()) {
|
||||
this->l = rational::zero();
|
||||
this->h = uMaxInt(sz);
|
||||
}
|
||||
SASSERT(invariant());
|
||||
}
|
||||
|
||||
|
|
|
@ -458,7 +458,11 @@ struct ctx_simplify_tactic::imp {
|
|||
}
|
||||
simplify(t, new_t);
|
||||
pop(scope_level() - old_lvl);
|
||||
VERIFY(assert_expr(new_c, true));
|
||||
if (!assert_expr(new_c, true)) {
|
||||
r = new_t;
|
||||
cache(ite, r);
|
||||
return;
|
||||
}
|
||||
simplify(e, new_e);
|
||||
pop(scope_level() - old_lvl);
|
||||
if (c == new_c && t == new_t && e == new_e) {
|
||||
|
|
Loading…
Reference in a new issue