From 4e2847dea4e84f2ab4309b3de28309ca8eda41ce Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Mon, 16 Jan 2017 15:46:28 -0500
Subject: [PATCH] Revert "scale theory-aware priority by bvar_inc"

This reverts commit aa8bf2668f9942af6ef819e1a9f9af87a227c14e.
---
 src/smt/smt_case_split_queue.cpp | 19 +++++++------------
 src/smt/smt_context.h            |  1 -
 2 files changed, 7 insertions(+), 13 deletions(-)

diff --git a/src/smt/smt_case_split_queue.cpp b/src/smt/smt_case_split_queue.cpp
index 2bc3e32df..c7ef655f2 100644
--- a/src/smt/smt_case_split_queue.cpp
+++ b/src/smt/smt_case_split_queue.cpp
@@ -42,23 +42,18 @@ namespace smt {
     struct theory_aware_act_lt {
         svector<double> const & m_activity;
         theory_var_priority_map const & m_theory_var_priority;
-        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) {}
+        theory_aware_act_lt(svector<double> const & act, theory_var_priority_map const & a):m_activity(act),m_theory_var_priority(a) {}
         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 *= m_bvar_inc;
+  	        p_v1 = 0.0;
+	    }
             if (!m_theory_var_priority.find(v2, p_v2)) {
                 p_v2 = 0.0;
             }
-            p_v2 *= m_bvar_inc;
-            // add clause activity
-            p_v1 += m_activity[v1];
-            p_v2 += m_activity[v2];
+	    // add clause activity
+	    p_v1 += m_activity[v1];
+	    p_v2 += m_activity[v2];
             return p_v1 > p_v2;
         }
     };
@@ -1244,7 +1239,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, ctx.get_bvar_inc())) {
+            m_queue(1024, theory_aware_act_lt(ctx.get_activity_vector(), m_theory_var_priority)) {
         }
 
         virtual void activity_increased_eh(bool_var v) {
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 9a8e01b93..2aae6c8a5 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -824,7 +824,6 @@ 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".