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));
     }