From db274ebe01ba81195b30b848d77386ffa2fff865 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 23 Jun 2019 16:48:42 -0700 Subject: [PATCH] relax condition for distributing extract over ite #2359 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/bv_rewriter.cpp | 7 +++++-- src/math/interval/interval_def.h | 2 +- src/smt/smt_context.cpp | 2 +- 3 files changed, 7 insertions(+), 4 deletions(-) diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index 24f23ea45..7dabd19c4 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -784,10 +784,13 @@ br_status bv_rewriter::mk_extract(unsigned high, unsigned low, expr * arg, expr_ } } + // issue #2359 led to relaxing condition for propagating extract over ite. + // It is propagted inwards only in the case that it leads to at most one + // branch of ite to be expanded or if one of the expanded ite branches have a single + // reference count. expr* c = nullptr, *t = nullptr, *e = nullptr; if (m().is_ite(arg, c, t, e) && - (t->get_ref_count() == 1 || !m().is_ite(t)) && - (e->get_ref_count() == 1 || !m().is_ite(e))) { + (t->get_ref_count() == 1 || e->get_ref_count() == 1 || !m().is_ite(t) || !m().is_ite(e))) { result = m().mk_ite(c, m_mk_extract(high, low, t), m_mk_extract(high, low, e)); return BR_REWRITE2; } diff --git a/src/math/interval/interval_def.h b/src/math/interval/interval_def.h index 19058b231..293a85eac 100644 --- a/src/math/interval/interval_def.h +++ b/src/math/interval/interval_def.h @@ -1018,7 +1018,7 @@ void interval_manager::mul(interval const & i1, interval const & i2, interval #ifdef _TRACE static unsigned call_id = 0; #endif -#if Z3DEBUG || _TRACE +#if Z3DEBUG bool i1_contains_zero = contains_zero(i1); bool i2_contains_zero = contains_zero(i2); #endif diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index d240ebb1e..1c0d91534 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -2849,7 +2849,7 @@ namespace smt { } void context::push() { - TRACE("trigger_bug", tout << "context::push()\n";); + TRACE("unit_subsumption_bug", display(tout << "context::push()\n");); scoped_suspend_rlimit _suspend_cancel(m_manager.limit()); pop_to_base_lvl(); setup_context(false);