mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
gift for Nuno
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
448cf8c31d
commit
7f590b5419
|
@ -694,7 +694,8 @@ namespace {
|
|||
bool was_updated = true;
|
||||
if (b.is_full() && b.tight) {
|
||||
r = m.mk_true();
|
||||
} else if (m_bound.find(t1, ctx)) {
|
||||
}
|
||||
else if (m_bound.find(t1, ctx)) {
|
||||
if (ctx.implies(b)) {
|
||||
r = m.mk_true();
|
||||
}
|
||||
|
@ -705,12 +706,15 @@ namespace {
|
|||
r = m.mk_eq(t1, m_bv.mk_numeral(rational(intr.l, rational::ui64()),
|
||||
m.get_sort(t1)));
|
||||
}
|
||||
else {
|
||||
was_updated = false;
|
||||
}
|
||||
}
|
||||
else {
|
||||
was_updated = false;
|
||||
}
|
||||
|
||||
CTRACE("bv", was_updated, tout << mk_pp(t, m) << " " << b << " (ctx: " << ctx << ") (intr: " << intr << "): " << r << "\n";);
|
||||
TRACE("bv", tout << mk_pp(t, m) << " " << b << " (ctx: " << ctx << ") (intr: " << intr << "): " << r << "\n";);
|
||||
if (sign && was_updated)
|
||||
r = m.mk_not(r);
|
||||
}
|
||||
|
|
|
@ -242,7 +242,7 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) {
|
|||
r = new_t;
|
||||
}
|
||||
else {
|
||||
TRACE("tactic", tout << new_c << "\n" << new_t << "\n" << new_e << "\n";);
|
||||
TRACE("simplify", tout << new_c << "\n" << new_t << "\n" << new_e << "\n";);
|
||||
r = m.mk_ite(new_c, new_t, new_e);
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue