addressing compiler warnings

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

src/interp/iz3base.h

@@ -161,7 +161,7 @@ class iz3base : public iz3mgr, public scopes {
   stl_ext::hash_map<ast,ast> simplify_memo;
   stl_ext::hash_map<ast,int> frame_map;                      // map assertions to frames
 
-  int frames;                               // number of frames
+  // int frames;                               // number of frames
 
  protected:
   void add_frame_range(int frame, ast t);

src/math/simplex/sparse_matrix_def.h

@@ -325,7 +325,6 @@ namespace simplex {
     void sparse_matrix<Ext>::add(row row1, numeral const& n, row row2) {
         m_stats.m_add_rows++;
         _row & r1 = m_rows[row1.id()];
-        _row & r2 = m_rows[row2.id()];
         
         r1.save_var_pos(m_var_pos, m_var_pos_idx);
 

src/smt/theory_pb.cpp

@@ -406,7 +406,6 @@ namespace smt {
     }
 
     bool theory_pb::internalize_atom(app * atom, bool gate_ctx) {
-        ast_manager& m = get_manager();
         SASSERT(m_util.is_at_most_k(atom) || m_util.is_le(atom) || 
                 m_util.is_ge(atom) || m_util.is_at_least_k(atom) || 
                 m_util.is_eq(atom));
@@ -707,7 +706,6 @@ namespace smt {
     }
 
     void theory_pb::remove(ptr_vector<ineq>& ineqs, ineq* c) {
-        context& ctx = get_context();
         for (unsigned j = 0; j < ineqs.size(); ++j) {
             if (ineqs[j] == c) {                        
                 std::swap(ineqs[j], ineqs[ineqs.size()-1]);
@@ -1217,7 +1215,6 @@ namespace smt {
 
     void theory_pb::compile_ineq(ineq& c) {
         ++m_stats.m_num_compiles;
-        ast_manager& m = get_manager();
         context& ctx = get_context();
         // only cardinality constraints are compiled.
         SASSERT(c.m_compilation_threshold < UINT_MAX);
@@ -1551,8 +1548,6 @@ namespace smt {
             m_ineq_literals.push_back(c.lit());
         }
     }
-
-    static unsigned s_min_l_size = UINT_MAX;
         
     //
     // modeled after sat_solver/smt_context
@@ -1789,7 +1784,6 @@ namespace smt {
     // debug methods
 
     void theory_pb::validate_watch(ineq const& c) const {
-        context& ctx = get_context();
         scoped_mpz sum(m_mpz_mgr), max(m_mpz_mgr);
         for (unsigned i = 0; i < c.watch_size(); ++i) {
             sum += c.ncoeff(i);

src/smt/theory_wmaxsat.cpp

@@ -105,7 +105,6 @@ bool_var theory_wmaxsat::assert_weighted(expr* fml, rational const& w) {
 
 bool_var theory_wmaxsat::register_var(app* var, bool attach) {
     context & ctx = get_context();
-    ast_manager& m = get_manager();
     bool_var bv;
     SASSERT(!ctx.e_internalized(var));
     enode* x = ctx.mk_enode(var, false, true, true);

src/tactic/arith/card2bv_tactic.cpp

@@ -102,7 +102,6 @@ namespace pb {
         // 
         else if (f->get_family_id() == au.get_family_id()) {
             if (f->get_decl_kind() == OP_ADD) {
-                bool all_ite_01 = true;
                 unsigned bits = 0;
                 for (unsigned i = 0; i < sz; i++) {
                     rational val1, val2;