diff --git a/src/api/java/NativeStatic.txt b/src/api/java/NativeStatic.txt
index 226643360..c8bd267b5 100644
--- a/src/api/java/NativeStatic.txt
+++ b/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);
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 166bd7015..44744c821 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/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);
diff --git a/src/ast/rewriter/term_enumeration.cpp b/src/ast/rewriter/term_enumeration.cpp
index 9b17ac1dc..7fb95a247 100644
--- a/src/ast/rewriter/term_enumeration.cpp
+++ b/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;
diff --git a/src/nlsat/nlsat_interval_set.cpp b/src/nlsat/nlsat_interval_set.cpp
index dc5740e10..160c8afb6 100644
--- a/src/nlsat/nlsat_interval_set.cpp
+++ b/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;
     }
 
diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index f0196baad..c6c914fe0 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/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;
diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index 3b9cc31b3..b5d2ee771 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/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)
diff --git a/src/smt/theory_finite_set.cpp b/src/smt/theory_finite_set.cpp
index 6f07961bf..dc1aae175 100644
--- a/src/smt/theory_finite_set.cpp
+++ b/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;
diff --git a/src/test/ackermannize.cpp b/src/test/ackermannize.cpp
index 7dbca06be..10a415bf8 100644
--- a/src/test/ackermannize.cpp
+++ b/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);
diff --git a/src/test/deep_api_bugs.cpp b/src/test/deep_api_bugs.cpp
index 206daf5e6..a977b9cc7 100644
--- a/src/test/deep_api_bugs.cpp
+++ b/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";
     }
diff --git a/src/test/dlist.cpp b/src/test/dlist.cpp
index e378ddec7..3e472b838 100644
--- a/src/test/dlist.cpp
+++ b/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);
diff --git a/src/test/doc.cpp b/src/test/doc.cpp
index 9ea741152..85acd1aeb 100644
--- a/src/test/doc.cpp
+++ b/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;
diff --git a/src/test/hashtable.cpp b/src/test/hashtable.cpp
index 1f0b3fb75..6874f2db1 100644
--- a/src/test/hashtable.cpp
+++ b/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);
diff --git a/src/test/hilbert_basis.cpp b/src/test/hilbert_basis.cpp
index 4aaca1355..01cb6166a 100644
--- a/src/test/hilbert_basis.cpp
+++ b/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()));
         }
 
diff --git a/src/test/memory.cpp b/src/test/memory.cpp
index 9a8d12b5d..58e8855b6 100644
--- a/src/test/memory.cpp
+++ b/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";
             }
         }
diff --git a/src/test/model_evaluator.cpp b/src/test/model_evaluator.cpp
index 77e13560b..571b229c4 100644
--- a/src/test/model_evaluator.cpp
+++ b/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());
     }
diff --git a/src/test/object_allocator.cpp b/src/test/object_allocator.cpp
index be07424e2..9f0aa351d 100644
--- a/src/test/object_allocator.cpp
+++ b/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;
diff --git a/src/test/parametric_datatype.cpp b/src/test/parametric_datatype.cpp
index 2a31803aa..005f6a8c9 100644
--- a/src/test/parametric_datatype.cpp
+++ b/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";
diff --git a/src/test/sls_seq_plugin.cpp b/src/test/sls_seq_plugin.cpp
index 4c8c5340c..94d1ce5bb 100644
--- a/src/test/sls_seq_plugin.cpp
+++ b/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);
diff --git a/src/test/sls_test.cpp b/src/test/sls_test.cpp
index 2ca2948d5..18955fe82 100644
--- a/src/test/sls_test.cpp
+++ b/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);