deal with warnings reported in https://launchpadlibrarian.net/522361319/buildlog_ubuntu-groovy-s390x.z3_4.8.10-1ubuntu4ppa1_BUILDING.txt.gz

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

src/ast/rewriter/expr_safe_replace.cpp

@@ -64,7 +64,6 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) {
         }
         else if (is_app(a)) {
             app* c = to_app(a);
-            unsigned n = c->get_num_args();
             m_args.reset();
             bool arg_differs = false, has_all_args = true;
             for (expr* arg : *c) {

src/nlsat/nlsat_interval_set.cpp

@@ -76,9 +76,9 @@ namespace nlsat {
         
         if (!i.m_lower_inf && !i.m_upper_inf) {
             auto s = am.compare(i.m_lower, i.m_upper);
+            (void)s;
             TRACE("nlsat_interval", tout << "lower: "; am.display_decimal(tout, i.m_lower); tout << ", upper: "; am.display_decimal(tout, i.m_upper);
                   tout << "\ns: " << s << "\n";);
-            (void)s;
             SASSERT(s <= 0);
             SASSERT(!is_zero(s) || !i.m_lower_open && !i.m_upper_open);            
         }

src/qe/qe.cpp

@@ -550,7 +550,6 @@ namespace qe {
 
         void nnf_and_or(bool is_and, app* a, bool p) {
             m_args.reset();
-            unsigned num_args = a->get_num_args();
             expr_ref tmp(m);
             bool visited = true;
             for (expr* arg : *a) {
@@ -1272,7 +1271,6 @@ namespace qe {
     }
 
     bool i_solver_context::has_plugin(app* x) {
-        ast_manager& m = get_manager();
         family_id fid = x->get_sort()->get_family_id();
         return 
             0 <= fid && 
@@ -1281,7 +1279,6 @@ namespace qe {
     }
     
     qe_solver_plugin& i_solver_context::plugin(app* x) {
-        ast_manager& m = get_manager();
         SASSERT(has_plugin(x));
         return *(m_plugins[x->get_sort()->get_family_id()]);               
     }

src/sat/sat_solver.cpp

@@ -3588,7 +3588,6 @@ namespace sat {
     void solver::unassign_vars(unsigned old_sz, unsigned new_lvl) {
         SASSERT(old_sz <= m_trail.size());
         SASSERT(m_replay_assign.empty());
-        unsigned i = m_trail.size();
         for (unsigned i = m_trail.size(); i-- > old_sz; ) {
             literal l  = m_trail[i];
             bool_var v = l.var();

src/sat/smt/q_ematch.cpp

@@ -264,7 +264,6 @@ namespace q {
     }
 
     void ematch::instantiate(binding& b, clause& c) {
-        quantifier* q = c.q();       
         if (m_stats.m_num_instantiations > ctx.get_config().m_qi_max_instances) 
             return;
         unsigned max_generation = b.m_max_generation;

src/sat/smt/q_mbi.cpp

@@ -513,7 +513,7 @@ namespace q {
 
     bool mbqi::first_offset(unsigned_vector& offsets, app_ref_vector const& vars) {
         offsets.reset();
-        for (app* v : vars) 
+        for (app* _ : vars) 
             offsets.push_back(0);
         for (unsigned i = 0; i < vars.size(); ++i) 
             if (!next_offset(offsets, vars, i, 0))

src/smt/dyn_ack.cpp

@@ -71,7 +71,6 @@ namespace smt {
 
         proof * mk_proof(conflict_resolution & cr) override {
             ast_manager & m   = cr.get_manager();
-            context & ctx     = cr.get_context();
             unsigned num_args = m_app1->get_num_args();
             proof_ref_vector prs(m);
             expr_ref_vector lits(m);

src/smt/theory_arith_eq.h

@@ -319,6 +319,7 @@ namespace smt {
     void theory_arith<Ext>::propagate_eq_to_core(theory_var x, theory_var y, antecedents& antecedents) {
         // Ignore equality if variables are already known to be equal.
         ast_manager& m = get_manager();
+        (void)m;
         if (is_equal(x, y))
             return;
         // I doesn't make sense to propagate an equality (to the core) of variables of different sort.

src/smt/theory_seq.cpp

@@ -1494,7 +1494,7 @@ bool theory_seq::internalize_term(app* term) {
     else {
         e = ctx.mk_enode(term, false, m.is_bool(term), true);
     }
-    theory_var v = mk_var(e);
+    mk_var(e);
     if (!ctx.relevancy()) {
         relevant_eh(term);
     }

src/smt/theory_str.cpp

@@ -307,7 +307,6 @@ namespace smt {
     }
 
     void theory_str::refresh_theory_var(expr * e) {
-        ast_manager & m = get_manager();
         enode * en = ensure_enode(e);
         theory_var v = mk_var(en); (void)v;
         TRACE("str", tout << "refresh " << mk_pp(e, get_manager()) << ": v#" << v << std::endl;);
@@ -318,7 +317,6 @@ namespace smt {
 
     theory_var theory_str::mk_var(enode* n) {
         TRACE("str", tout << "mk_var for " << mk_pp(n->get_owner(), get_manager()) << std::endl;);
-        ast_manager & m = get_manager();
         if (!(n->get_owner()->get_sort() == u.str.mk_string_sort())) {
             return null_theory_var;
         }
@@ -6543,7 +6541,6 @@ namespace smt {
     }
 
     void theory_str::handle_equality(expr * lhs, expr * rhs) {
-        ast_manager & m = get_manager();
         // both terms must be of sort String
         sort * lhs_sort = lhs->get_sort();
         sort * rhs_sort = rhs->get_sort();
@@ -7117,7 +7114,6 @@ namespace smt {
     }
 
     void theory_str::recursive_check_variable_scope(expr * ex) {
-        ast_manager & m = get_manager();
 
         if (is_app(ex)) {
             app * a = to_app(ex);
@@ -9205,8 +9201,6 @@ namespace smt {
     }
 
     bool theory_str::flatten(expr* ex, expr_ref_vector & flat) {
-        ast_manager & m = get_manager();
-        // TRACE("str", tout << "ex " << mk_pp(ex, m)  << " target " << target << " length " << length << " sublen " << mk_pp(sublen, m) << " extra " << mk_pp(extra, m) << std::endl;);
 
         sort * ex_sort = ex->get_sort();
         sort * str_sort = u.str.mk_string_sort();

src/tactic/bv/bv_bounds_tactic.cpp

@@ -163,9 +163,9 @@ namespace {
 
 
     struct undo_bound {
-        expr* e;
+        expr* e { nullptr };
         interval b;
-        bool fresh;
+        bool fresh { false };
         undo_bound(expr* e, const interval& b, bool fresh) : e(e), b(b), fresh(fresh) {}
     };