fix build errors

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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());        

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();

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;
         

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;

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; }

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(); }
 
     };