Fix compiler warnings under clang

src/sat/sat_solver/inc_sat_solver.cpp

@@ -687,7 +687,7 @@ class inc_sat_solver : public solver {
         return ensure_euf()->user_propagate_register_expr(e);
     }
 
-    void user_propagate_register_created(user_propagator::created_eh_t& r) {
+    void user_propagate_register_created(user_propagator::created_eh_t& r) override {
         ensure_euf()->user_propagate_register_created(r);
     }
 

src/sat/smt/pb_solver.cpp

@@ -1458,7 +1458,7 @@ namespace pb {
             return nullptr;
         }
         rational weight(0);
-        for (auto const [w, l] : wlits)
+        for (auto const &[w, l] : wlits)
             weight += w;
         if (weight < k) {
             if (lit == sat::null_literal)

src/smt/theory_lra.cpp

@@ -1563,6 +1563,7 @@ class theory_lra::imp {
                 return FC_CONTINUE;
             }
             for (expr* e : m_not_handled) {
+                (void) e; // just in case TRACE() is a no-op
                 TRACE("arith", tout << "unhandled operator " << mk_pp(e, m) << "\n";);        
                 st = FC_GIVEUP;
             }                

src/tactic/core/collect_statistics_tactic.cpp

@@ -110,7 +110,6 @@ class collect_statistics_tactic : public tactic {
         void operator()(quantifier * q) {
             m_stats["quantifiers"]++;
             SASSERT(is_app(q->get_expr()));
-            app * body = to_app(q->get_expr());
             switch (q->get_kind()) {
             case forall_k:
                 m_stats["forall-variables"] += q->get_num_decls();