From 023b630b5a2b251346d5ce2ac47e692cd8edf820 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Tue, 2 Jun 2020 16:36:38 +0100
Subject: [PATCH] remove unused class fields in BV theory

---
 src/smt/theory_bv.cpp | 11 +++++------
 src/smt/theory_bv.h   |  8 ++++----
 2 files changed, 9 insertions(+), 10 deletions(-)

diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index 7378b291f..853961912 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -192,7 +192,7 @@ namespace smt {
         for (literal lit : bits) {
             expr_ref l(get_manager());
             ctx.literal2expr(lit, l);
-            r.push_back(l);
+            r.push_back(std::move(l));
         }
     }
 
@@ -315,11 +315,8 @@ namespace smt {
         unsigned sz             = bits.size();
         SASSERT(get_bv_size(n) == sz);
         m_bits[v].reset();
-        m_bits_expr.reset();
 
-        for (unsigned i = 0; i < sz; ++i)
-            m_bits_expr.push_back(bits.get(i));
-        ctx.internalize(m_bits_expr.c_ptr(), sz, true);
+        ctx.internalize(bits.c_ptr(), sz, true);
 
         for (unsigned i = 0; i < sz; i++) {
             expr * bit          = bits.get(i);
@@ -1163,7 +1160,7 @@ namespace smt {
             ctx.internalize(diff, true);
             literal arg = ctx.get_literal(diff);
             lits.push_back(arg);
-            exprs.push_back(diff);
+            exprs.push_back(std::move(diff));
         }
         m_stats.m_num_diseq_dynamic++;
         if (m.has_trace_stream()) {
@@ -1427,7 +1424,9 @@ namespace smt {
         m_find(*this),
         m_approximates_large_bvs(false) {
         memset(m_eq_activity, 0, sizeof(m_eq_activity));
+#if WATCH_DISEQ
         memset(m_diseq_activity, 0, sizeof(m_diseq_activity));
+#endif
     }
 
     theory_bv::~theory_bv() {
diff --git a/src/smt/theory_bv.h b/src/smt/theory_bv.h
index bf6a0425f..8d01071ff 100644
--- a/src/smt/theory_bv.h
+++ b/src/smt/theory_bv.h
@@ -124,11 +124,11 @@ namespace smt {
         value2var                m_fixed_var_table;
         
         unsigned char            m_eq_activity[256];
-        unsigned char            m_diseq_activity[256];
+        //unsigned char            m_diseq_activity[256];
         svector<std::pair<theory_var, theory_var>> m_replay_diseq;
-        vector<vector<std::pair<theory_var, theory_var>>> m_diseq_watch;
-        svector<bool_var> m_diseq_watch_trail;
-        unsigned_vector   m_diseq_watch_lim;
+        //vector<vector<std::pair<theory_var, theory_var>>> m_diseq_watch;
+        //svector<bool_var> m_diseq_watch_trail;
+        //unsigned_vector   m_diseq_watch_lim;
 
         literal_vector           m_tmp_literals;
         svector<var_pos>         m_prop_queue;