From 454d20d23e85fbe9535c6dd46ff650d783b95e59 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 1 May 2018 10:06:54 -0700
Subject: [PATCH] fix build errors

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/ast_smt2_pp.cpp           | 1 -
 src/sat/sat_big.cpp               | 1 -
 src/sat/sat_big.h                 | 1 -
 src/sat/sat_scc.cpp               | 1 -
 src/solver/parallel_tactic.cpp    | 9 +++++++--
 src/tactic/arith/eq2bv_tactic.cpp | 4 ++--
 6 files changed, 9 insertions(+), 8 deletions(-)

diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp
index 4f9a72174..a2958e3c9 100644
--- a/src/ast/ast_smt2_pp.cpp
+++ b/src/ast/ast_smt2_pp.cpp
@@ -1146,7 +1146,6 @@ public:
 
 
     void operator()(func_decl * f, expr * e, format_ref & r, char const* cmd) {
-        unsigned arity = f->get_arity();
         unsigned len;
         format * fname = m_env.pp_fdecl_name(f, len);
         register_var_names(f->get_arity());        
diff --git a/src/sat/sat_big.cpp b/src/sat/sat_big.cpp
index 27b87d4c9..35898a110 100644
--- a/src/sat/sat_big.cpp
+++ b/src/sat/sat_big.cpp
@@ -177,7 +177,6 @@ namespace sat {
     }
 
     unsigned big::reduce_tr(solver& s) {
-        unsigned num_lits = s.num_vars() * 2;
         unsigned idx = 0;
         unsigned elim = 0;
         m_del_bin.reset();
diff --git a/src/sat/sat_big.h b/src/sat/sat_big.h
index f2adf9ad8..898ddd1e8 100644
--- a/src/sat/sat_big.h
+++ b/src/sat/sat_big.h
@@ -34,7 +34,6 @@ namespace sat {
         svector<int>           m_left, m_right;
         literal_vector         m_root, m_parent;
         bool                   m_learned;
-        bool                   m_binary;   // is the BIG produced from binary clauses or hyper-binary resolution?
 
         svector<std::pair<literal, literal>> m_del_bin;
         
diff --git a/src/sat/sat_scc.cpp b/src/sat/sat_scc.cpp
index 8a2029df2..e430bcb47 100644
--- a/src/sat/sat_scc.cpp
+++ b/src/sat/sat_scc.cpp
@@ -237,7 +237,6 @@ namespace sat {
     }
 
     unsigned scc::reduce_tr(bool learned) {        
-        unsigned num_lits = m_solver.num_vars() * 2;
         init_big(learned);
         unsigned num_elim = m_big.reduce_tr(m_solver);
         m_num_elim_bin += num_elim;
diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp
index ac147672e..61e97e040 100644
--- a/src/solver/parallel_tactic.cpp
+++ b/src/solver/parallel_tactic.cpp
@@ -162,11 +162,16 @@ class parallel_tactic : public tactic {
         expr_ref_vector m_vars;
         expr_ref_vector m_cube;
     public:
-        cube_var(expr_ref_vector& c, expr_ref_vector& vs):
+        cube_var(expr_ref_vector const& c, expr_ref_vector const& vs):
             m_vars(vs), m_cube(c) {}
 
+        cube_var(cube_var const& other):
+            m_vars(other.m_vars), m_cube(other.m_cube) {}
+
         cube_var operator()(ast_translation& tr) {
-            return cube_var(tr(m_cube), tr(m_vars));
+            expr_ref_vector vars(tr(m_vars));
+            expr_ref_vector cube(tr(m_cube));
+            return cube_var(cube, vars);
         }
 
         expr_ref_vector const& cube() const { return m_cube; }
diff --git a/src/tactic/arith/eq2bv_tactic.cpp b/src/tactic/arith/eq2bv_tactic.cpp
index 57fd51271..616ba69c9 100644
--- a/src/tactic/arith/eq2bv_tactic.cpp
+++ b/src/tactic/arith/eq2bv_tactic.cpp
@@ -113,13 +113,13 @@ class eq2bv_tactic : public tactic {
             return v;
         }
 
-        virtual void display(std::ostream & out) {
+        void display(std::ostream & out) override {
             for (auto const& kv : m_map) {
                 out << "(model-set " << kv.m_key->get_name() << " " << kv.m_value->get_name() << ")\n";
             }
         }
 
-        virtual void get_units(obj_map<expr, bool>& units) { units.reset(); }
+        void get_units(obj_map<expr, bool>& units) override { units.reset(); }
 
     };