fix build warnings

src/api/java/NativeStatic.txt

@@ -154,7 +154,7 @@ static void decide_eh(void* _p, Z3_solver_callback cb, Z3_ast _val, unsigned bit
   info->jenv->CallVoidMethod(info->jobj, info->decide, (jlong)_val, bit, is_pos);
 }
 
-static jboolean on_binding_eh(void* _p, Z3_solver_callback cb, Z3_ast _q, Z3_ast _inst) {
+[[maybe_unused]] static jboolean on_binding_eh(void* _p, Z3_solver_callback cb, Z3_ast _q, Z3_ast _inst) {
   JavaInfo *info = static_cast<JavaInfo*>(_p);
   ScopedCB scoped(info, cb);
   return info->jenv->CallBooleanMethod(info->jobj, info->on_binding, (jlong)_q, (jlong)_inst);

src/ast/rewriter/seq_rewriter.cpp

@@ -4829,7 +4829,7 @@ br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) {
     unsigned lo_v = 0, hi_v = 0;
     if (re().is_range(a, lo_v, hi_v)) {
         unsigned max_c = u().max_char();
-        sort *srt = a->get_sort(), *seq_sort;
+        sort *srt = a->get_sort(), *seq_sort = nullptr;
         VERIFY(m_util.is_re(a, seq_sort));
         bool has_left = (lo_v > 0);
         bool has_right = (hi_v < max_c);

src/ast/rewriter/term_enumeration.cpp

@@ -236,7 +236,7 @@ private:
 class children_iterator {
 public:
     children_iterator(ast_manager& m, production const& prod, term_bank const& bank, unsigned current_cost)
-        : m(m), m_prod(prod), m_current_cost(current_cost), m_done(false)
+        : m(m), m_done(false)
     {
         m_arity = prod.domain.size();
         if (m_arity == 0) {
@@ -276,8 +276,6 @@ public:
 
 private:
     ast_manager& m;
-    production const& m_prod;
-    unsigned m_current_cost;
     unsigned m_arity;
     bool m_done;
     vector<cost_terms> m_candidates;

src/nlsat/nlsat_interval_set.cpp

@@ -261,7 +261,7 @@ namespace nlsat {
         new_set->m_full = full;
         new_set->m_ref_count  = 0;
         new_set->m_num_intervals = sz;
-        memcpy(new_set->m_intervals, buf.data(), sizeof(interval)*sz);
+        memcpy(static_cast<void*>(new_set->m_intervals), static_cast<const void*>(buf.data()), sizeof(interval)*sz);
         return new_set;
     }
 

src/smt/smt_model_checker.cpp

@@ -233,7 +233,6 @@ namespace smt {
             }
             else {
                 expr * sk_term = get_term_from_ctx(sk_value);
-                func_decl * f = nullptr;
                 if (sk_term != nullptr) {
                     TRACE(model_checker, tout << "sk term " << mk_pp(sk_term, m) << "\n");
                     sk_value = sk_term;

src/smt/smt_model_finder.cpp

@@ -1435,7 +1435,6 @@ namespace smt {
                     }
                 }
                 
-                unsigned max_count = 20;
                 for (auto t : tn.enum_terms(srt)) {
                     unsigned generation = 0; // todo - inherited from sub-term of t?
                     TRACE(model_finder, tout << "ho_var: adding term " << mk_ismt2_pp(t, m)

src/smt/theory_finite_set.cpp

@@ -437,7 +437,7 @@ namespace smt {
                     return lit == arg;
             };
             auto lit1 = clause.get(0);
-            auto lit2 = clause.get(1);
+            [[maybe_unused]] auto lit2 = clause.get(1);
             auto position = 0;
             if (is_complement_to(is_true, lit1, e))
                 position = 0;

src/test/ackermannize.cpp

@@ -175,7 +175,7 @@ static void test_ackr_bound_probe() {
 // by the BV solver back to a model for the original formula (with UF).
 // The two null-pointer guards in ackr_model_converter.cpp are exercised here.
 //
-static void test_ackermannize_bv_model() {
+[[maybe_unused]] static void test_ackermannize_bv_model() {
     Z3_config cfg = Z3_mk_config();
     Z3_context ctx = Z3_mk_context(cfg);
     Z3_del_config(cfg);

src/test/deep_api_bugs.cpp

@@ -297,7 +297,7 @@ static void test_bug_translate_null_target() {
     // Z3_translate(ctx, x, nullptr) would crash - no null check on target
     // The function checks c == target (line 1517) but doesn't check target != nullptr first
     // So mk_c(target) on line 1522 dereferences nullptr
-    Z3_error_code err = Z3_get_error_code(ctx);
+    Z3_get_error_code(ctx);
     std::cout << "  [BUG DOCUMENTED] Z3_translate(ctx, ast, nullptr) would crash\n";
     std::cout << "  No null check on target before mk_c(target) at api_ast.cpp:1522\n";
 
@@ -596,7 +596,6 @@ static void test_bug_array_sort_mismatch() {
 
     // Create Array(Int, Int)
     Z3_sort int_sort = Z3_mk_int_sort(ctx);
-    Z3_sort bool_sort = Z3_mk_bool_sort(ctx);
     Z3_sort arr_sort = Z3_mk_array_sort(ctx, int_sort, int_sort);
 
     Z3_ast arr = Z3_mk_const(ctx, Z3_mk_string_symbol(ctx, "a"), arr_sort);
@@ -651,7 +650,7 @@ static void test_bug_substitute_null_arrays() {
 
     // With num_exprs=0, null arrays should be fine
     Z3_ast r = Z3_substitute(ctx, x, 0, nullptr, nullptr);
-    Z3_error_code err = Z3_get_error_code(ctx);
+    Z3_get_error_code(ctx);
     if (r != nullptr) {
         std::cout << "  substitute(x, 0, null, null) OK: " << Z3_ast_to_string(ctx, r) << "\n";
     }

src/test/dlist.cpp

@@ -70,7 +70,7 @@ static void test_pop() {
     TestNode* list = nullptr;
     TestNode node1(1);
     TestNode::push_to_front(list, &node1);
-    TestNode* popped = TestNode::pop(list);
+    [[maybe_unused]] TestNode* popped = TestNode::pop(list);
     SASSERT(popped == &node1);
     SASSERT(list == nullptr);
     SASSERT(popped->next() == popped);

src/test/doc.cpp

@@ -303,14 +303,13 @@ class test_doc_cls {
         bool_vector to_merge(N, false);
         bit_vector discard_cols;
         discard_cols.resize(N, false);
-        unsigned num_bits = 1;
         union_find_default_ctx union_ctx;
         subset_ints equalities(union_ctx);
         unsigned lo = N;
         equalities.mk_var();
         for (unsigned i = 1; i < N; ++i) {
             to_merge[i] = (m_ran(2) == 0);
-            if (!to_merge[i]) ++num_bits; else lo = i;
+            if (to_merge[i]) lo = i;
             equalities.mk_var();
         }
         if (lo == N) return;

src/test/hashtable.cpp

@@ -38,7 +38,6 @@ int vals[N];
 
 static void tst1() {
     int_set h1;
-    int size = 0;
     for (int i = 1; i < N; i ++) {
         int v = rand() % (N / 2);
         h1.insert(v);
@@ -92,7 +91,7 @@ static void tst2() {
             ENSURE(contains(h1, elem));
             n++;
         }
-        ENSURE(n == h1.size());
+        ENSURE(n == static_cast<int>(h1.size()));
     }
     ENSURE(h1.size() == h2.size());
     // std::cout << "size: " << h1.size() << ", capacity: " << h1.capacity() << "\n"; std::cout.flush();
@@ -194,7 +193,7 @@ void test_hashtable_iterators() {
     ht.insert(3);
     
     int count = 0;
-    for (const auto& elem : ht) {
+    for ([[maybe_unused]] const auto& elem : ht) {
         ++count;
     }
     VERIFY(count == 3);

src/test/hilbert_basis.cpp

@@ -119,7 +119,7 @@ expr_ref hilbert_basis_validate::mk_validate(hilbert_basis& hb) {
         bool is_initial;
         hb.get_basis_solution(i, v, is_initial);
 
-        for (unsigned j = 0; xs.size() < v.size(); ++j) {
+        for (; xs.size() < v.size(); ) {
             xs.push_back(m.mk_fresh_const("x", a.mk_int()));
         }
 

src/test/memory.cpp

@@ -39,7 +39,7 @@ static void hit_me(char const* wm) {
                 Z3_mk_bv_sort(ctx,i);      
                 
             }
-            catch (std::bad_alloc) {
+            catch (const std::bad_alloc&) {
                 std::cout << "caught\n";
             }
         }

src/test/model_evaluator.cpp

@@ -81,12 +81,12 @@ void tst_model_evaluator() {
         SASSERT(fi2.num_entries() == 1);
 
         expr_ref removed_arg(a.mk_int(0), m);
-        expr* removed_args[1] = { removed_arg.get() };
+        [[maybe_unused]] expr* removed_args[1] = { removed_arg.get() };
         SASSERT(fi2.get_entry(removed_args) == nullptr);
 
         expr_ref kept_arg(a.mk_int(599), m);
         expr* kept_args[1] = { kept_arg.get() };
-        func_entry* kept = fi2.get_entry(kept_args);
+        [[maybe_unused]] func_entry* kept = fi2.get_entry(kept_args);
         SASSERT(kept != nullptr);
         SASSERT(kept->get_result() == one.get());
     }

src/test/object_allocator.cpp

@@ -73,7 +73,7 @@ static void tst2() {
     m.enable_concurrent(true);
 
     vector<std::pair<cell *, int> > object_coeff_pairs;
-    unsigned num_resets = 0;
+    [[maybe_unused]] unsigned num_resets = 0;
 
     for (unsigned i = 0; i < 100000; ++i) {
         unsigned idx = rand() % 6;

src/test/parametric_datatype.cpp

@@ -76,9 +76,9 @@ static void test_polymorphic_datatype_api() {
     std::cout << "triple_int_bool: " << Z3_sort_to_string(ctx, triple_int_bool) << "\n";
     
     // Get constructors and accessors from the instantiated datatype
-    Z3_func_decl mk_triple_int_bool = Z3_get_datatype_sort_constructor(ctx, triple_int_bool, 0);
+    [[maybe_unused]] Z3_func_decl mk_triple_int_bool = Z3_get_datatype_sort_constructor(ctx, triple_int_bool, 0);
     Z3_func_decl first_int_bool = Z3_get_datatype_sort_constructor_accessor(ctx, triple_int_bool, 0, 0);
-    Z3_func_decl second_int_bool = Z3_get_datatype_sort_constructor_accessor(ctx, triple_int_bool, 0, 1);
+    [[maybe_unused]] Z3_func_decl second_int_bool = Z3_get_datatype_sort_constructor_accessor(ctx, triple_int_bool, 0, 1);
     Z3_func_decl third_int_bool = Z3_get_datatype_sort_constructor_accessor(ctx, triple_int_bool, 0, 2);
     
     std::cout << "Got constructors and accessors from instantiated datatype\n";

src/test/sls_seq_plugin.cpp

@@ -199,7 +199,7 @@ struct test_seq {
     ptr_vector<expr> const& lhs(expr* eq) {
         auto& ev = get_eval(eq);
         if (ev.lhs.empty()) {
-            expr* x, * y;
+            expr* x = nullptr, * y = nullptr;
             VERIFY(m.is_eq(eq, x, y));
             seq.str.get_concat(x, ev.lhs);
             seq.str.get_concat(y, ev.rhs);

src/test/sls_test.cpp

@@ -239,7 +239,7 @@ namespace bv {
 }
 
 
-static void test_eval1() {
+[[maybe_unused]] static void test_eval1() {
     ast_manager m;
     reg_decl_plugins(m);
     bv_util bv(m);
@@ -262,7 +262,7 @@ static void test_eval1() {
     }
 }
 
-static void test_repair1() {
+[[maybe_unused]] static void test_repair1() {
     ast_manager m;
     reg_decl_plugins(m);
     bv_util bv(m);