fix debian amd64 warnings

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

src/math/simplex/sparse_matrix.h

@@ -48,7 +48,7 @@ namespace simplex {
             }
         };
 
-        static const int dead_id = -1;
+        static const unsigned dead_id = UINT_MAX;
 
         /**
            \brief A row_entry is:  m_var*m_coeff

src/muz/rel/udoc_relation.cpp

@@ -559,7 +559,6 @@ namespace datalog {
         filter_identical_fn(const relation_base & _r, unsigned col_cnt, const unsigned *identical_cols)
             : m_cols(col_cnt), m_equalities(union_ctx) {
             udoc_relation const& r = get(_r);
-            doc_manager& dm = r.get_dm();
             m_size = r.column_num_bits(identical_cols[0]);
             m_empty_bv.resize(r.get_num_bits(), false);            
             for (unsigned i = 0; i < col_cnt; ++i) {

src/opt/mus.cpp

@@ -54,7 +54,8 @@ struct mus::imp {
     
     
     unsigned add_soft(expr* cls) {
-        SASSERT(is_uninterp_const(cls) || m.is_not(cls) && is_uninterp_const(to_app(cls)->get_arg(0)));
+        SASSERT(is_uninterp_const(cls) || 
+                (m.is_not(cls) && is_uninterp_const(to_app(cls)->get_arg(0))));
         unsigned idx = m_cls2expr.size();
         m_expr2cls.insert(cls, idx);
         m_cls2expr.push_back(cls);

src/sat/sat_sls.cpp

@@ -273,7 +273,7 @@ namespace sat {
             clause const& c = *m_clauses[i];
             bool is_sat = c.satisfied_by(m_model);
             SASSERT(is_sat != m_false.contains(i));
-            SASSERT(is_sat == m_num_true[i] > 0);
+            SASSERT(is_sat == (m_num_true[i] > 0));
         }        
     }
 

src/sat/tactic/goal2sat.cpp

@@ -36,7 +36,7 @@ Notes:
 #include"model_v2_pp.h"
 #include"tactic.h"
 #include"ast_pp.h"
-#include<strstream>
+#include<sstream>
 
 struct goal2sat::imp {
     struct frame {

src/shell/opt_frontend.cpp

@@ -89,11 +89,11 @@ class wcnf {
     ast_manager&   m;
     stream_buffer& in;
 
-    app_ref read_clause(unsigned& weight) {
+    app_ref read_clause(int& weight) {
         int     parsed_lit;
         int     var;    
         parsed_lit = in.parse_int();
-        weight = static_cast<unsigned>(parsed_lit);
+        weight = parsed_lit;
         app_ref result(m), p(m);
         expr_ref_vector ors(m);
         while (true) { 
@@ -137,7 +137,7 @@ public:
                 parse_spec(num_vars, num_clauses, max_weight);
             }
             else {
-                unsigned weight = 0;
+                int weight = 0;
                 app_ref cls = read_clause(weight);
                 if (weight == max_weight) {
                     opt.add_hard_constraint(cls);

src/smt/theory_arith_core.h

@@ -72,7 +72,7 @@ namespace smt {
             m_value        .push_back(inf_numeral());
         }
         m_old_value        .push_back(inf_numeral());
-        SASSERT(m_var_occs.size() == r);
+        SASSERT(m_var_occs.size() == static_cast<unsigned>(r));
         m_var_occs         .push_back(atoms());
         SASSERT(m_var_occs.back().empty());
         m_unassigned_atoms .push_back(0);

src/smt/theory_wmaxsat.cpp

@@ -55,7 +55,8 @@ void theory_wmaxsat::get_assignment(svector<bool>& result) {
     }
     else {
         std::sort(m_cost_save.begin(), m_cost_save.end());
-        for (unsigned i = 0, j = 0; i < m_vars.size(); ++i) {
+        unsigned j = 0;
+        for (theory_var i = 0; i < m_vars.size(); ++i) {
             if (j < m_cost_save.size() && m_cost_save[j] == i) {
                 result.push_back(false);
                 ++j;
@@ -120,7 +121,7 @@ bool_var theory_wmaxsat::register_var(app* var, bool attach) {
         theory_var v = mk_var(x);
         ctx.attach_th_var(x, this, v);
         m_bool2var.insert(bv, v);
-        SASSERT(v == m_var2bool.size());
+        SASSERT(v == static_cast<theory_var>(m_var2bool.size()));
         m_var2bool.push_back(bv);
         SASSERT(ctx.bool_var2enode(bv));
     }

src/tactic/sls/bvsls_opt_engine.cpp

@@ -318,7 +318,8 @@ mpz bvsls_opt_engine::find_best_move(
         }
 
         // reset to what it was before
-        double check = incremental_score(fd, old_value);
+        //double check = 
+        incremental_score(fd, old_value);
         m_obj_evaluator.update(fd, old_value);
     }
 
@@ -363,4 +364,4 @@ bool bvsls_opt_engine::randomize_wrt_hard() {
     }
 
     return false;
-}
+}