From 037a4aa155a44b0d0771fa9c551794f61497ae52 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Tue, 17 Feb 2026 04:44:23 +0000 Subject: [PATCH] Fix C4267 build warnings in ast.h by adding static_cast for size_t to unsigned conversions Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/ast.h | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/ast/ast.h b/src/ast/ast.h index 15cd863fd..7fc86070d 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -2369,10 +2369,10 @@ public: proof * mk_transitivity(unsigned num_proofs, proof * const * proofs); proof * mk_transitivity(unsigned num_proofs, proof * const * proofs, expr * n1, expr * n2); proof * mk_transitivity(std::initializer_list const& proofs) { - return mk_transitivity(proofs.size(), proofs.begin()); + return mk_transitivity(static_cast(proofs.size()), proofs.begin()); } proof * mk_transitivity(std::initializer_list const& proofs, expr * n1, expr * n2) { - return mk_transitivity(proofs.size(), proofs.begin(), n1, n2); + return mk_transitivity(static_cast(proofs.size()), proofs.begin(), n1, n2); } proof * mk_monotonicity(func_decl * R, app * f1, app * f2, unsigned num_proofs, proof * const * proofs); proof * mk_congruence(app * f1, app * f2, unsigned num_proofs, proof * const * proofs); @@ -2405,10 +2405,10 @@ public: proof * mk_unit_resolution(unsigned num_proofs, proof * const * proofs); proof * mk_unit_resolution(unsigned num_proofs, proof * const * proofs, expr * new_fact); proof * mk_unit_resolution(std::initializer_list const& proofs) { - return mk_unit_resolution(proofs.size(), proofs.begin()); + return mk_unit_resolution(static_cast(proofs.size()), proofs.begin()); } proof * mk_unit_resolution(std::initializer_list const& proofs, expr * new_fact) { - return mk_unit_resolution(proofs.size(), proofs.begin(), new_fact); + return mk_unit_resolution(static_cast(proofs.size()), proofs.begin(), new_fact); } proof * mk_hypothesis(expr * h); proof * mk_lemma(proof * p, expr * lemma);