diff --git a/src/smt/smt_case_split_queue.cpp b/src/smt/smt_case_split_queue.cpp
index c7ef655f2..2bc3e32df 100644
--- a/src/smt/smt_case_split_queue.cpp
+++ b/src/smt/smt_case_split_queue.cpp
@@ -42,18 +42,23 @@ namespace smt {
     struct theory_aware_act_lt {
         svector<double> const & m_activity;
         theory_var_priority_map const & m_theory_var_priority;
-        theory_aware_act_lt(svector<double> const & act, theory_var_priority_map const & a):m_activity(act),m_theory_var_priority(a) {}
+        double const & m_bvar_inc;
+        theory_aware_act_lt(svector<double> const & act,
+                theory_var_priority_map const & a,
+                double const & bvar_inc):m_activity(act),m_theory_var_priority(a),m_bvar_inc(bvar_inc) {}
         bool operator()(bool_var v1, bool_var v2) const {
             double p_v1, p_v2;
             if (!m_theory_var_priority.find(v1, p_v1)) {
-  	        p_v1 = 0.0;
-	    }
+                p_v1 = 0.0;
+            }
+            p_v1 *= m_bvar_inc;
             if (!m_theory_var_priority.find(v2, p_v2)) {
                 p_v2 = 0.0;
             }
-	    // add clause activity
-	    p_v1 += m_activity[v1];
-	    p_v2 += m_activity[v2];
+            p_v2 *= m_bvar_inc;
+            // add clause activity
+            p_v1 += m_activity[v1];
+            p_v2 += m_activity[v2];
             return p_v1 > p_v2;
         }
     };
@@ -1239,7 +1244,7 @@ namespace smt {
             m_context(ctx),
             m_params(p),
             m_theory_var_priority(),
-            m_queue(1024, theory_aware_act_lt(ctx.get_activity_vector(), m_theory_var_priority)) {
+            m_queue(1024, theory_aware_act_lt(ctx.get_activity_vector(), m_theory_var_priority, ctx.get_bvar_inc())) {
         }
 
         virtual void activity_increased_eh(bool_var v) {
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 2aae6c8a5..9a8e01b93 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -824,6 +824,7 @@ namespace smt {
          * or some other axiom that means at least one of them must be assigned 'true'.
          */
         void mk_th_case_split(unsigned num_lits, literal * lits);
+        double get_bvar_inc() const { return m_bvar_inc; }
 
         /*
          * Provide a hint to the branching heuristic about the priority of a "theory-aware literal".