build warnings

src/ast/ast.cpp

@@ -1670,7 +1670,7 @@ bool ast_manager::slow_not_contains(ast const * n) {
 }
 #endif
 
-#if 1
+#if 0
 static unsigned s_count = 0;
 
 static void track_id(ast_manager& m, ast* n, unsigned id) {

src/ast/rewriter/enum2bv_rewriter.cpp

@@ -225,6 +225,7 @@ struct enum2bv_rewriter::imp {
                     new_body_ref = mk_and(bounds);
                     break;
                 case lambda_k:
+                case choice_k:
                     UNREACHABLE();
                     break;
                 }

src/muz/base/dl_rule.h

@@ -86,6 +86,7 @@ namespace datalog {
             case forall_k: m_univ = true; break;
             case exists_k: m_exist = true; break;
             case lambda_k: m_lambda = true; break;
+            case choice_k: break;
             }
         }
         void operator()(app * n) { }

src/smt/theory_finite_set.cpp

@@ -171,7 +171,6 @@ namespace smt {
     void theory_finite_set::add_in_axioms(enode *in, var_data *d) {
         SASSERT(u.is_in(in->get_expr()));
         auto e = in->get_arg(0)->get_expr();
-        auto set1 = in->get_arg(1);
         for (enode *setop : d->m_parent_setops) {
             SASSERT(
                 any_of(enode::args(setop), [&](enode *arg) { return in->get_arg(1)->get_root() == arg->get_root(); }));
@@ -833,7 +832,6 @@ namespace smt {
         }
 
         app *mk_range_value(model_generator &mg, expr_ref_vector const &values) {
-            unsigned i = 0;
             arith_value av(th.m);
             av.init(&th.ctx);
             vector<std::tuple<rational, enode *, bool>> elems;

src/smt/theory_finite_set_size.cpp

@@ -201,7 +201,6 @@ namespace smt {
         for (auto [a, b] : th.m_diseqs) {
             auto x = th.get_enode(a);
             auto y = th.get_enode(b);
-            diseq d = {a, b};
             if (n2b.contains(x) && n2b.contains(y)) {
                 arith_util a(m);
                 auto d1 = mk_diff(x, y);

src/tactic/core/collect_statistics_tactic.cpp

@@ -119,6 +119,9 @@ protected:
             case lambda_k:
                 m_stats["lambda-variables"] += q->get_num_decls();
                 break;
+            case choice_k:
+                m_stats["choice-variables"] += q->get_num_decls();
+                break;
             }
             m_stats["patterns"] += q->get_num_patterns();
             m_stats["no-patterns"] += q->get_num_no_patterns();