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

Merge pull request #8668 from Z3Prover/copilot/fix-build-warnings

Browse source 
Fix C4267 warnings in ast.h initializer_list overloads
This commit is contained in:
Nikolaj Bjorner 2026-02-16 20:50:47 -08:00 • committed by GitHub
commit c0e8698bae
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
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);