mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-17 06:11:44 +00:00
Code Activity

Fix C4267 build warnings in ast.h by adding static_cast for size_t to unsigned conversions

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-17 04:44:23 +00:00
parent 9d8f736270
commit 037a4aa155
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/ast/ast.h
View file

@ -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<proof*> const& proofs) {
return mk_transitivity(proofs.size(), proofs.begin());
return mk_transitivity(static_cast<unsigned>(proofs.size()), proofs.begin());
}
proof * mk_transitivity(std::initializer_list<proof*> const& proofs, expr * n1, expr * n2) {
return mk_transitivity(proofs.size(), proofs.begin(), n1, n2);
return mk_transitivity(static_cast<unsigned>(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<proof*> const& proofs) {
return mk_unit_resolution(proofs.size(), proofs.begin());
return mk_unit_resolution(static_cast<unsigned>(proofs.size()), proofs.begin());
}
proof * mk_unit_resolution(std::initializer_list<proof*> const& proofs, expr * new_fact) {
return mk_unit_resolution(proofs.size(), proofs.begin(), new_fact);
return mk_unit_resolution(static_cast<unsigned>(proofs.size()), proofs.begin(), new_fact);
}
proof * mk_hypothesis(expr * h);
proof * mk_lemma(proof * p, expr * lemma);