diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp
index fe2bd7149..834d76a1c 100644
--- a/src/smt/smt_consequences.cpp
+++ b/src/smt/smt_consequences.cpp
@@ -533,7 +533,7 @@ namespace smt {
     lbool context::preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores) {        
         pop_to_base_lvl();
         cores.reset();
-        setup_context(false);
+        setup_context(false, !asms.empty());
         internalize_assertions();
         if (m_asserted_formulas.inconsistent() || inconsistent()) {
             return l_false;
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 96b66149a..3f9166245 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -177,7 +177,7 @@ namespace smt {
             dst_ctx.assert_expr(fml1);
         }
 
-        dst_ctx.setup_context(dst_ctx.m_fparams.m_auto_config);
+        dst_ctx.setup_context(dst_ctx.m_fparams.m_auto_config, true);
         dst_ctx.internalize_assertions();
         
         dst_ctx.copy_user_propagator(src_ctx, true);
@@ -2908,7 +2908,7 @@ namespace smt {
         user_propagator::push_eh_t&       push_eh,
         user_propagator::pop_eh_t&        pop_eh,
         user_propagator::fresh_eh_t&      fresh_eh) {
-        setup_context(false);
+        setup_context(false, true);
         m_user_propagator = alloc(theory_user_propagator, *this);
         m_user_propagator->add(ctx, push_eh, pop_eh, fresh_eh);
         for (unsigned i = m_scopes.size(); i-- > 0; ) 
@@ -3004,7 +3004,7 @@ namespace smt {
 
     void context::push() {       
         pop_to_base_lvl();
-        setup_context(false);
+        setup_context(false, false);
         bool was_consistent = !inconsistent();
         try {
             internalize_assertions(); // internalize assertions before invoking m_asserted_formulas.push_scope
@@ -3611,7 +3611,7 @@ namespace smt {
         if (!check_preamble(reset_cancel)) return l_undef;
         SASSERT(m_scope_lvl == 0);
         SASSERT(!m_setup.already_configured());
-        setup_context(m_fparams.m_auto_config);
+        setup_context(m_fparams.m_auto_config, false);
 
         if (m_fparams.m_threads > 1 && !m.has_trace_stream()) {
             parallel p(*this);
@@ -3644,7 +3644,10 @@ namespace smt {
         return CFG_LOGIC;
     }
 
-    void context::setup_context(bool use_static_features) {
+    void context::setup_context(bool use_static_features, bool has_assumptions) {
+        unsigned nf = m_asserted_formulas.get_num_formulas();
+        if (nf == 0 && !has_assumptions)
+           return;
         if (m_setup.already_configured() || inconsistent()) {
             m_relevancy_lvl = std::min(m_fparams.m_relevancy_lvl, m_relevancy_lvl);
             return;
@@ -3677,7 +3680,7 @@ namespace smt {
     lbool context::check(unsigned num_assumptions, expr * const * assumptions, bool reset_cancel) {
         if (!check_preamble(reset_cancel)) return l_undef;
         SASSERT(at_base_level());
-        setup_context(false);
+        setup_context(false, num_assumptions > 0);
         if (m_fparams.m_threads > 1 && !m.has_trace_stream()) {            
             expr_ref_vector asms(m, num_assumptions, assumptions);
             parallel p(*this);
@@ -3707,7 +3710,7 @@ namespace smt {
     lbool context::check(expr_ref_vector const& cube, vector<expr_ref_vector> const& clauses) {
         if (!check_preamble(true)) return l_undef;
         TRACE("before_search", display(tout););
-        setup_context(false);
+        setup_context(false, !cube.empty() || !clauses.empty());
         lbool r = l_undef;
         do {
             pop_to_base_lvl();
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 9ab1db60a..f9774b30a 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -1566,7 +1566,7 @@ namespace smt {
         void init();
         void flush();
         config_mode get_config_mode(bool use_static_features) const;
-        virtual void setup_context(bool use_static_features);
+        virtual void setup_context(bool use_static_features, bool has_assumptions);
         void setup_components();
         void pop_to_base_lvl();
         void pop_to_search_lvl();
diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index f1983364f..702535fd6 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -826,6 +826,16 @@ namespace smt {
         setup_fpa();
         setup_special_relations();
         setup_polymorphism();
+        setup_relevancy(st);
+    }
+
+    //
+    // quantifier free problems with bit-vectors should always use relevancy = 0
+    // there are some other cases where relevancy propagation is harmful.
+    //
+    void setup::setup_relevancy(static_features& st) {
+        if (st.m_has_bv && st.m_num_quantifiers == 0)
+             m_params.m_relevancy_lvl = 0;           
     }
 
     void setup::setup_unknown(static_features & st) {
diff --git a/src/smt/smt_setup.h b/src/smt/smt_setup.h
index acbea59cb..90f7419d4 100644
--- a/src/smt/smt_setup.h
+++ b/src/smt/smt_setup.h
@@ -109,6 +109,7 @@ namespace smt {
         void setup_lra_arith();
         void setup_fpa();
         void setup_str();
+        void setup_relevancy(static_features& st);
 
     public:
         setup(context & c, smt_params & params);