fixes to build warnings

src/ast/euf/euf_ac_plugin.cpp

@@ -440,8 +440,9 @@ namespace euf {
             TRACE("plugin", tout << "propagate " << eq_id << ": " << eq_pp(*this, m_eqs[eq_id]) << "\n");
 
             // simplify eq using processed
-            for (auto other_eq : backward_iterator(eq_id))
-                TRACE("plugin", tout << "backward iterator " << eq_id << " vs " << other_eq << " " << is_processed(other_eq) << "\n");
+            TRACE("plugin", 
+                  for (auto other_eq : backward_iterator(eq_id))
+                      tout << "backward iterator " << eq_id << " vs " << other_eq << " " << is_processed(other_eq) << "\n"););
             for (auto other_eq : backward_iterator(eq_id))
                 if (is_processed(other_eq) && backward_simplify(eq_id, other_eq))
                     goto loop_start;

src/ast/euf/euf_egraph.cpp

@@ -107,8 +107,8 @@ namespace euf {
     void egraph::update_children(enode* n) {
         for (enode* child : enode_args(n)) 
             child->get_root()->add_parent(n);
-        for (enode* child : enode_args(n))  
-            SASSERT(child->get_root()->m_parents.back() == n);
+        DEBUG_CODE(for (enode* child : enode_args(n))  
+                       SASSERT(child->get_root()->m_parents.back() == n););
         m_updates.push_back(update_record(n, update_record::update_children()));
     }
 

src/math/lp/nla_divisions.cpp

@@ -19,15 +19,13 @@ Module Name:
 namespace nla {
 
     void divisions::add_idivision(lpvar q, lpvar x, lpvar y) {
-        const auto& lra = m_core.lra;
         if (x == null_lpvar || y == null_lpvar || q == null_lpvar)
             return;
         m_idivisions.push_back({q, x, y});
         m_core.trail().push(push_back_vector(m_idivisions));
     }
 
     void divisions::add_rdivision(lpvar q, lpvar x, lpvar y) {
-        auto& lra = m_core.lra;
         if (x == null_lpvar || y == null_lpvar || q == null_lpvar)
             return;
         m_rdivisions.push_back({ q, x, y });

src/muz/ddnf/ddnf.cpp

@@ -678,14 +678,9 @@ namespace datalog {
         }
 
         bool compile_rules1(rule_set const& rules, rule_set& new_rules) {
-            datalog::rule_set::iterator it  = rules.begin();
-            datalog::rule_set::iterator end = rules.end();
-            unsigned idx = 0;
-            for (; it != end; ++idx, ++it) {
-                if (!compile_rule1(**it, rules, new_rules)) {
+            for (auto const & r : rules) 
+                if (!compile_rule1(*r, rules, new_rules)) 
                     return false;
-                }
-            }
             return true;            
         }
 

src/muz/fp/datalog_parser.cpp

@@ -902,7 +902,6 @@ class dparser : public parser {
         unsigned arg_idx = 0;
         tok = m_lexer->next_token();
         while (tok != TK_EOS && tok != TK_ERROR) {
-            symbol alias;
             sort* s = nullptr;
 
             if(!f) {
@@ -939,7 +938,6 @@ class dparser : public parser {
                 }
                 s = f->get_domain(arg_idx);
 
-                symbol var_symbol;
                 tok = parse_arg(tok, s, args);
             }
 
@@ -1067,7 +1065,7 @@ class dparser : public parser {
 
     bool read_line(std::istream& strm, std::string& line) {
         line.clear();
-        char ch = strm.get();
+        int ch = strm.get();
         while (ch == ' ' || ch == '\t' || ch == '\n' || ch == '\r') {
             ch = strm.get();
         }

src/muz/rel/dl_product_relation.cpp

@@ -1030,6 +1030,7 @@ namespace datalog {
             }
             new_rels.push_back(irel);
         }
+        (void)old_remain;
         SASSERT(old_remain==0); //the new specification must be a superset of the old one
         m_relations = new_rels;
 

src/muz/spacer/spacer_unsat_core_plugin.cpp

@@ -97,7 +97,6 @@ namespace spacer {
         // XXX this assertion should be true so there is no need to check for it
         SASSERT (!m_ctx.is_closed (step));
         func_decl* d = step->get_decl();
-        symbol sym;
         TRACE("spacer.farkas",
               tout << "looking at: " << mk_pp(step, m) << "\n";);
         if (!m_ctx.is_closed(step) && is_farkas_lemma(m, step)) {
@@ -239,9 +238,8 @@ namespace spacer {
         SASSERT(m_ctx.is_b(step));
 
         func_decl* d = step->get_decl();
-        symbol sym;
         if (!m_ctx.is_closed(step) && // if step is not already interpolated
-           is_farkas_lemma(m, step)) {
+            is_farkas_lemma(m, step)) {
             SASSERT(d->get_num_parameters() == m.get_num_parents(step) + 2);
             SASSERT(m.has_fact(step));
 

src/opt/opt_cores.cpp

@@ -256,12 +256,11 @@ namespace opt {
     void cores::rotate_cores() {
         expr_ref_vector soft(m);
         soft.append(ctx.soft());
-        unsigned num_sat = 0, num_unsat = 0, num_undef = 0;        
+        unsigned num_sat = 0, num_undef = 0;        
         lbool is_sat = l_false;
         while (m.inc() && m_cores.size() < m_max_num_cores) {
             switch (is_sat) {
             case l_false: {
-                ++num_unsat;
                 auto core = unsat_core();
                 add_core(core);
                 if (core.empty())

src/opt/opt_lns.cpp

@@ -174,7 +174,6 @@ namespace opt {
     void lns::relax_cores() {
         if (!m_cores.empty() && m_cores_are_valid) {
             std::sort(m_cores.begin(), m_cores.end(), [&](expr_ref_vector const& a, expr_ref_vector const& b) { return a.size() < b.size(); });
-            unsigned num_disjoint = 0;
             vector<expr_ref_vector> new_cores;
             for (auto const& c : m_cores) {
                 bool in_core = false;
@@ -185,7 +184,6 @@ namespace opt {
                 for (auto* e : c)
                     m_in_core.mark(e);
                 new_cores.push_back(c);
-                ++num_disjoint;
             }
             IF_VERBOSE(2, verbose_stream() << "num cores: " << m_cores.size() << " new cores: " << new_cores.size() << "\n");
             ctx.relax_cores(new_cores);

src/parsers/smt2/smt2parser.cpp

@@ -942,7 +942,6 @@ namespace smt2 {
             }
             for (unsigned i = 0; i < sz; i++) {
                 pdatatype_decl * d = new_dt_decls[i];
-                symbol duplicated;
                 check_duplicate(d, line, pos);
                 if (!is_smt2_6) {
                     // datatypes are inserted up front in SMT2.6 mode, so no need to re-insert them.

src/sat/sat_clause_use_list.cpp

@@ -25,13 +25,13 @@ namespace sat {
         unsigned sz = 0;
         for (clause* c : m_clauses) 
             if (!c->was_removed())
-                sz++;
-        SASSERT(sz == m_size);
+                sz++;        
+        VERIFY(sz == m_size);
         unsigned redundant = 0;
         for (clause* c : m_clauses) 
             if (c->is_learned())
                 redundant++;
-        SASSERT(redundant == m_num_redundant);
+        VERIFY(redundant == m_num_redundant);
 
         return true;
     }

src/sat/sat_lookahead.cpp

@@ -1392,7 +1392,6 @@ namespace sat {
     void lookahead::propagate_clauses_searching(literal l) {
         // clauses where l is negative
         unsigned sz = m_nary_count[(~l).index()];
-        literal lit;
         SASSERT(m_search_mode == lookahead_mode::searching);
         for (nary* n : m_nary[(~l).index()]) {
             if (sz-- == 0) break;

src/shell/dimacs_frontend.cpp

@@ -110,7 +110,6 @@ static void track_clauses(sat::solver const& src,
         dst.mk_var(false, true);
     }
     sat::literal_vector lits;
-    sat::literal lit;
     sat::clause * const * it  = src.begin_clauses();
     sat::clause * const * end = src.end_clauses();
     svector<sat::solver::bin_clause> bin_clauses;

src/smt/diff_logic.h

@@ -569,6 +569,7 @@ class dl_graph {
     void traverse_neg_cycle2(bool try_relax, Functor & f) {
         static unsigned num_conflicts = 0;
         ++num_conflicts;
+        (void)num_conflicts;
         SASSERT(!is_feasible(m_edges[m_last_enabled_edge]));
         vector<numeral>  potentials;
         svector<edge_id> edges;

src/smt/dyn_ack.cpp

@@ -294,7 +294,6 @@ namespace smt {
 
     void dyn_ack_manager::gc() {
         TRACE("dyn_ack", tout << "dyn_ack GC\n";);
-        unsigned num_deleted = 0;
         m_to_instantiate.reset();
         m_qhead = 0;
         svector<app_pair>::iterator it  = m_app_pairs.begin();
@@ -318,7 +317,6 @@ namespace smt {
             // SASSERT(num_occs > 0);
             num_occs = static_cast<unsigned>(num_occs * m_params.m_dack_gc_inv_decay);
             if (num_occs <= 1) {
-                num_deleted++;
                 TRACE("dyn_ack", tout << "2) erasing:\n" << mk_pp(p.first, m) << "\n" << mk_pp(p.second, m) << "\n";);
                 m_app_pair2num_occs.erase(p.first, p.second);
                 m.dec_ref(p.first);
@@ -337,7 +335,6 @@ namespace smt {
         // app_pair_lt is not a total order on pairs of expressions.
         // So, we should use stable_sort to avoid different behavior in different platforms.
         std::stable_sort(m_to_instantiate.begin(), m_to_instantiate.end(), f);
-        // IF_VERBOSE(10, if (num_deleted > 0) verbose_stream() << "dynamic ackermann GC: " << num_deleted << "\n";);
     }
 
     class dyn_ack_clause_del_eh : public clause_del_eh {
@@ -519,7 +516,6 @@ namespace smt {
 
     void dyn_ack_manager::gc_triples() {
         TRACE("dyn_ack", tout << "dyn_ack GC\n";);
-        unsigned num_deleted = 0;
         m_triple.m_to_instantiate.reset();
         m_triple.m_qhead = 0;
         svector<app_triple>::iterator it  = m_triple.m_apps.begin();
@@ -544,7 +540,6 @@ namespace smt {
             // SASSERT(num_occs > 0);
             num_occs = static_cast<unsigned>(num_occs * m_params.m_dack_gc_inv_decay);
             if (num_occs <= 1) {
-                num_deleted++;
                 TRACE("dyn_ack", tout << "2) erasing:\n" << mk_pp(p.first, m) << "\n" << mk_pp(p.second, m) << "\n";);
                 m_triple.m_app2num_occs.erase(p.first, p.second, p.third);
                 m.dec_ref(p.first);
@@ -563,7 +558,6 @@ namespace smt {
         app_triple_lt f(m_triple.m_app2num_occs);
         // app_triple_lt is not a total order
         std::stable_sort(m_triple.m_to_instantiate.begin(), m_triple.m_to_instantiate.end(), f);
-        // IF_VERBOSE(10, if (num_deleted > 0) verbose_stream() << "dynamic ackermann GC: " << num_deleted << "\n";);
     }
 
 

src/smt/theory_arith_core.h

@@ -3030,7 +3030,7 @@ namespace smt {
     template<typename Ext>
     void theory_arith<Ext>::propagate_bounds() {
         TRACE("propagate_bounds_detail", display(tout););
-        unsigned num_prop = 0, count = 0;
+        unsigned count = 0;
         for (unsigned r_idx : m_to_check) {
             row & r = m_rows[r_idx];
             if (r.get_base_var() != null_theory_var) {
@@ -3039,34 +3039,19 @@ namespace smt {
                     int upper_idx;
                     is_row_useful_for_bound_prop(r, lower_idx, upper_idx);
 
-                    ++num_prop;
                     if (lower_idx >= 0) 
                         count += imply_bound_for_monomial(r, lower_idx, true);
                     else if (lower_idx == -1) 
                         count += imply_bound_for_all_monomials(r, true);
-                    else
-                        --num_prop;
 
-                    ++num_prop;
                     if (upper_idx >= 0) 
                         count += imply_bound_for_monomial(r, upper_idx, false);
                     else if (upper_idx == -1) 
                         count += imply_bound_for_all_monomials(r, false);
-                    else
-                        --num_prop;
 
                     // sneaking cheap eq detection in this loop
                     propagate_cheap_eq(r_idx);
                 }
-
-#if 0
-                theory_var v = r.get_base_var();
-                if (!is_int(v) || get_value(v).is_int()) {
-                    // If an integer value is not assigned to an integer value, then
-                    // bound propagation can diverge.
-                    m_in_to_check.remove(v);
-                }
-#endif
             }
         }
 

src/smt/theory_bv.cpp

@@ -1988,6 +1988,7 @@ namespace smt {
             while (curr != v);
 
             zero_one_bits const & _bits = m_zero_one_bits[v];
+            (void)num_bits;
             SASSERT(_bits.size() == num_bits);
             bool_vector already_found;
             already_found.resize(bv_sz, false);

src/smt/theory_lra.cpp

@@ -3495,10 +3495,8 @@ class theory_lra::imp {
 
     bool validate_eq(enode* x, enode* y) {
         static bool s_validating = false;
-        static unsigned s_count = 0;
         if (s_validating)
             return true;
-        ++s_count;
         flet<bool> _svalid(s_validating, true);
         context nctx(m, ctx().get_fparams(), ctx().get_params());
         add_background(nctx);

src/smt/theory_pb.cpp

@@ -2127,9 +2127,9 @@ namespace smt {
               tout << "sum: " << sum << " " << maxsum << " ";
               tout << ctx.get_assignment(c.lit()) << "\n";);
 
-        SASSERT(sum <= maxsum);
-        SASSERT((sum >= c.k()) == (ctx.get_assignment(c.lit()) == l_true));
-        SASSERT((maxsum < c.k()) == (ctx.get_assignment(c.lit()) == l_false));        
+        VERIFY(sum <= maxsum);
+        VERIFY((sum >= c.k()) == (ctx.get_assignment(c.lit()) == l_true));
+        VERIFY((maxsum < c.k()) == (ctx.get_assignment(c.lit()) == l_false));        
     }
 
     void theory_pb::validate_final_check(ineq& c) {

src/tactic/smtlogics/qfnra_tactic.cpp

@@ -25,14 +25,6 @@ Module Name:
 
 #include "tactic/smtlogics/qflra_tactic.h"
 
-static tactic * mk_qfnra_sat_solver(ast_manager& m, params_ref const& p, unsigned bv_size) {
-    params_ref nra2sat_p = p;
-    nra2sat_p.set_uint("nla2bv_max_bv_size", p.get_uint("nla2bv_max_bv_size", bv_size));   
-
-    return and_then(mk_nla2bv_tactic(m, nra2sat_p),
-                    mk_smt_tactic(m),
-                    mk_fail_if_undecided_tactic());
-}
 
 tactic * mk_multilinear_ls_tactic(ast_manager & m, params_ref const & p, unsigned ls_time = 60) {
     params_ref p_mls = p;

src/util/params.cpp

@@ -390,7 +390,6 @@ class params {
     void reset(char const * k);
 
     void validate(param_descrs const & p) {        
-        symbol suffix, prefix;
         for (params::entry& e : m_entries) {
             param_kind expected = p.get_kind_in_module(e.first);
             if (expected == CPK_INVALID) {