From d00d6a3506d57a2a58d3a62e9e915ce05697f676 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 25 Aug 2015 13:21:33 -0700 Subject: [PATCH] enable Boolean propagation in AUFBV to fix inefficiency (bit-blasting destroys simplifications that are possible by simple Boolean propagation). Fixes issue #194 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_conflict_resolution.cpp | 3 +-- src/smt/smt_setup.cpp | 1 + 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index a68d4d820..818e12fd1 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -115,8 +115,7 @@ namespace smt { break; case eq_justification::CONGRUENCE: { TRACE("conflict_detail", tout << "#" << lhs->get_owner_id() << " = " << rhs->get_owner_id() << " congruence\n";); - if (!lhs->is_eq()) - TRACE("dyn_ack_target", tout << "dyn_ack_target2: " << lhs->get_owner_id() << " " << rhs->get_owner_id() << "\n";); + CTRACE("dyn_ack_target", !lhs->is_eq(), tout << "dyn_ack_target2: " << lhs->get_owner_id() << " " << rhs->get_owner_id() << "\n";); m_dyn_ack_manager.used_cg_eh(lhs->get_owner(), rhs->get_owner()); unsigned num_args = lhs->get_num_args(); SASSERT(num_args == rhs->get_num_args()); diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index b72ecbd84..dba4ef57f 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -551,6 +551,7 @@ namespace smt { m_params.m_bv_cc = false; m_params.m_bb_ext_gates = true; m_params.m_nnf_cnf = false; + m_params.m_propagate_booleans = true; m_context.register_plugin(alloc(smt::theory_bv, m_manager, m_params, m_params)); m_context.register_plugin(alloc(smt::theory_array, m_manager, m_params)); }