From 36323f723b62db3a933f7a8e959a33c36362647d Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Fri, 16 Jan 2026 16:00:42 -0800 Subject: [PATCH] Fix 13 compiler warnings: sign-comparison and unused parameters (#8215) * Initial plan * Fix 13 compiler warnings: sign-comparison and unused parameters Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/api/julia/z3jl.cpp | 6 +++--- src/ast/sls/sls_arith_base.cpp | 2 +- src/math/interval/dep_intervals.h | 2 +- src/math/interval/interval.h | 2 +- src/math/lp/cross_nested.h | 2 +- src/sat/sat_lookahead.cpp | 2 +- src/smt/diff_logic.h | 4 ++-- src/smt/smt_case_split_queue.cpp | 2 +- src/smt/theory_arith_core.h | 2 +- src/smt/theory_dense_diff_logic_def.h | 2 +- 10 files changed, 13 insertions(+), 13 deletions(-) diff --git a/src/api/julia/z3jl.cpp b/src/api/julia/z3jl.cpp index 0470e5a6d..6bc53f78e 100644 --- a/src/api/julia/z3jl.cpp +++ b/src/api/julia/z3jl.cpp @@ -400,7 +400,7 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m) .MM(solver, units) .method("trail", static_cast(&solver::trail)) .method("trail", [](solver &s, jlcxx::ArrayRef levels) { - int sz = levels.size(); + int sz = static_cast(levels.size()); z3::array _levels(sz); for (int i = 0; i < sz; ++i) { _levels[i] = levels[i]; @@ -629,7 +629,7 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m) .MM(context, set_rounding_mode) .method("enumeration_sort", [](context& c, char const * name, jlcxx::ArrayRef names, func_decl_vector &cs, func_decl_vector &ts) { - int sz = names.size(); + int sz = static_cast(names.size()); std::vector _names; for (int i = 0; i < sz; ++i) { const char *x = jl_string_data(names[i]); @@ -639,7 +639,7 @@ JLCXX_MODULE define_julia_module(jlcxx::Module &m) }) .method("tuple_sort", [](context& c, char const * name, jlcxx::ArrayRef names, jlcxx::ArrayRef sorts, func_decl_vector &projs) { - int sz = names.size(); + int sz = static_cast(names.size()); std::vector _sorts; std::vector _names; for (int i = 0; i < sz; ++i) { diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp index eeb866ba3..27d7c8a5b 100644 --- a/src/ast/sls/sls_arith_base.cpp +++ b/src/ast/sls/sls_arith_base.cpp @@ -1972,7 +1972,7 @@ namespace sls { return 0.0000001; else if (result == 0) return 0.000002; - for (int i = m_prob_break.size(); i <= breaks; ++i) + for (int i = static_cast(m_prob_break.size()); i <= breaks; ++i) m_prob_break.push_back(std::pow(m_config.cb, -i)); return m_prob_break[breaks]; } diff --git a/src/math/interval/dep_intervals.h b/src/math/interval/dep_intervals.h index f5851c1f0..eab62821a 100644 --- a/src/math/interval/dep_intervals.h +++ b/src/math/interval/dep_intervals.h @@ -74,7 +74,7 @@ private: // For imprecise types (e.g., floats) it should set the rounding mode. void round_to_minus_inf() {} void round_to_plus_inf() {} - void set_rounding(bool to_plus_inf) {} + void set_rounding(bool /*to_plus_inf*/) {} // Getters mpq const& lower(interval const& a) const { return a.m_lower; } diff --git a/src/math/interval/interval.h b/src/math/interval/interval.h index 0d036a16e..1300e5666 100644 --- a/src/math/interval/interval.h +++ b/src/math/interval/interval.h @@ -53,7 +53,7 @@ public: // For imprecise types (e.g., floats) it should set the rounding mode. void round_to_minus_inf() {} void round_to_plus_inf() {} - void set_rounding(bool to_plus_inf) {} + void set_rounding(bool /*to_plus_inf*/) {} // Getters numeral const & lower(interval const & a) const { return a.m_lower; } diff --git a/src/math/lp/cross_nested.h b/src/math/lp/cross_nested.h index e944be739..67a6363d0 100644 --- a/src/math/lp/cross_nested.h +++ b/src/math/lp/cross_nested.h @@ -168,7 +168,7 @@ public: TRACE(nla_cn, tout << "save c=" << **c << "; front:"; print_front(front, tout) << "\n";); nex* copy_of_c = *c; auto copy_of_front = copy_front(front); - int alloc_size = m_nex_creator.size(); + int alloc_size = static_cast(m_nex_creator.size()); for (lpvar j : vars) { if (m_var_is_fixed(j)) { // it does not make sense to explore fixed multupliers diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 108f1b31f..21c379a84 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -2200,7 +2200,7 @@ namespace sat { backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision); return l_undef; } - int prev_nfreevars = m_freevars.size(); + int prev_nfreevars = static_cast(m_freevars.size()); double prev_psat = m_config.m_cube_cutoff == adaptive_psat_cutoff ? psat_heur() : dbl_max; // MN. only compute PSAT if enabled literal lit = choose(); if (inconsistent()) { diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h index 877bb6c89..7683d8316 100644 --- a/src/smt/diff_logic.h +++ b/src/smt/diff_logic.h @@ -224,7 +224,7 @@ class dl_graph { SASSERT(m_assignment.size() == m_parent.size()); SASSERT(m_assignment.size() <= m_heap.get_bounds()); SASSERT(m_in_edges.size() == m_out_edges.size()); - int n = m_out_edges.size(); + int n = static_cast(m_out_edges.size()); for (dl_var id = 0; id < n; ++id) { const edge_id_vector & e_ids = m_out_edges[id]; for (edge_id e_id : e_ids) { @@ -1195,7 +1195,7 @@ public: scc_id.reset(); m_roots.reset(); m_unfinished.reset(); - int n = m_assignment.size(); + int n = static_cast(m_assignment.size()); m_unfinished_set.resize(n, false); m_dfs_time.resize(n, -1); scc_id.resize(n, -1); diff --git a/src/smt/smt_case_split_queue.cpp b/src/smt/smt_case_split_queue.cpp index b1ff7347e..d43dd0fb8 100644 --- a/src/smt/smt_case_split_queue.cpp +++ b/src/smt/smt_case_split_queue.cpp @@ -1030,7 +1030,7 @@ namespace { void add_to_queue2(expr * e) { - int idx = m_queue2.size(); + int idx = static_cast(m_queue2.size()); GOAL_START(); m_queue2.push_back(queue_entry(e, get_generation(e))); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 680cb04e8..498fa03f4 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -2174,7 +2174,7 @@ namespace smt { bool is_pos = !is_neg; if (x_i != x_j && ((is_pos && above_lower(x_j)) || (is_neg && below_upper(x_j)))) { int num = get_num_non_free_dep_vars(x_j, best_so_far); - int col_sz = m_columns[x_j].size(); + int col_sz = static_cast(m_columns[x_j].size()); if (num < best_so_far || (num == best_so_far && col_sz < best_col_sz)) { result = x_j; out_a_ij = a_ij; diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h index ee8044e4c..d7fe745a0 100644 --- a/src/smt/theory_dense_diff_logic_def.h +++ b/src/smt/theory_dense_diff_logic_def.h @@ -620,7 +620,7 @@ namespace smt { template bool theory_dense_diff_logic::check_matrix() const { - int sz = m_matrix.size(); + int sz = static_cast(m_matrix.size()); for (theory_var i = 0; i < sz; ++i) { for (theory_var j = 0; j < sz; ++j) { cell const & c = m_matrix[i][j];