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<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);