From 30df8e7ece0dac41ea5828b6ad33a90384ae4561 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 29 May 2026 10:14:16 -0700
Subject: [PATCH] build warnings

---
 src/ast/ast.cpp                               | 2 +-
 src/ast/rewriter/enum2bv_rewriter.cpp         | 1 +
 src/muz/base/dl_rule.h                        | 1 +
 src/smt/theory_finite_set.cpp                 | 2 --
 src/smt/theory_finite_set_size.cpp            | 1 -
 src/tactic/core/collect_statistics_tactic.cpp | 3 +++
 6 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index cf5e7af87..fca28a051 100644
--- a/src/ast/ast.cpp
+++ b/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) {
diff --git a/src/ast/rewriter/enum2bv_rewriter.cpp b/src/ast/rewriter/enum2bv_rewriter.cpp
index d2c5fd122..8210cdc93 100644
--- a/src/ast/rewriter/enum2bv_rewriter.cpp
+++ b/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;
                 }
diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h
index 0a8fd955c..87c2637a9 100644
--- a/src/muz/base/dl_rule.h
+++ b/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) { }
diff --git a/src/smt/theory_finite_set.cpp b/src/smt/theory_finite_set.cpp
index 44c51d7dc..7ca1d4216 100644
--- a/src/smt/theory_finite_set.cpp
+++ b/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;
diff --git a/src/smt/theory_finite_set_size.cpp b/src/smt/theory_finite_set_size.cpp
index 2bae076d6..d9c4a9ddf 100644
--- a/src/smt/theory_finite_set_size.cpp
+++ b/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);
diff --git a/src/tactic/core/collect_statistics_tactic.cpp b/src/tactic/core/collect_statistics_tactic.cpp
index 5e8af0b43..b689d8058 100644
--- a/src/tactic/core/collect_statistics_tactic.cpp
+++ b/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();