From 9c1f85e564feff0ef93f0d7fed6a1b86fed8987a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 9 May 2014 11:03:11 -0700
Subject: [PATCH] addressing compiler warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/interp/iz3base.h                 | 2 +-
 src/math/simplex/sparse_matrix_def.h | 1 -
 src/smt/theory_pb.cpp                | 6 ------
 src/smt/theory_wmaxsat.cpp           | 1 -
 src/tactic/arith/card2bv_tactic.cpp  | 1 -
 5 files changed, 1 insertion(+), 10 deletions(-)

diff --git a/src/interp/iz3base.h b/src/interp/iz3base.h
index d82e721ae..550c563af 100755
--- a/src/interp/iz3base.h
+++ b/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);
diff --git a/src/math/simplex/sparse_matrix_def.h b/src/math/simplex/sparse_matrix_def.h
index 277165138..f4c25658e 100644
--- a/src/math/simplex/sparse_matrix_def.h
+++ b/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);
 
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index f19eb706c..1ae3634aa 100644
--- a/src/smt/theory_pb.cpp
+++ b/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);
diff --git a/src/smt/theory_wmaxsat.cpp b/src/smt/theory_wmaxsat.cpp
index 556f5047a..2c33d28da 100644
--- a/src/smt/theory_wmaxsat.cpp
+++ b/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);
diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp
index bba8705e0..26bea6343 100644
--- a/src/tactic/arith/card2bv_tactic.cpp
+++ b/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;