diff --git a/src/nlsat/nlsat_simplify.cpp b/src/nlsat/nlsat_simplify.cpp
index 64e3099a1..e1c10d5f5 100644
--- a/src/nlsat/nlsat_simplify.cpp
+++ b/src/nlsat/nlsat_simplify.cpp
@@ -66,7 +66,7 @@ namespace nlsat {
             polynomial_ref p(m_pm);
             ptr_buffer<poly> ps;
             buffer<bool> is_even;
-            unsigned num_atoms = m_atoms.size();
+            unsigned num_atoms = usize(m_atoms);
             for (unsigned j = 0; j < num_atoms; ++j) {
                 atom* a1 = m_atoms[j];
                 if (a1 && a1->is_ineq_atom()) {
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index dc6f388e5..97cac90fc 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -2616,7 +2616,7 @@ namespace nlsat {
 
         bool check_satisfied() {
             TRACE(nlsat, tout << "bk: b" << m_bk << ", xk: x" << m_xk << "\n"; if (m_xk != null_var) { m_display_var(tout, m_xk); tout << "\n"; });
-            unsigned num = m_atoms.size();
+            unsigned num = usize(m_atoms);
             if (m_bk != null_bool_var)
                 num = m_bk;
             for (bool_var b = 0; b < num; b++) {
@@ -3273,7 +3273,7 @@ namespace nlsat {
         }
 
         std::ostream& display_bool_assignment(std::ostream & out, bool eval_atoms = false) const {
-            unsigned sz = m_atoms.size();
+            unsigned sz = usize(m_atoms);
             if (!eval_atoms) {
                 for (bool_var b = 0; b < sz; b++) {
                     if (m_bvalues[b] == l_undef)
@@ -4011,7 +4011,7 @@ namespace nlsat {
         }
 
         std::ostream& display_smt2_bool_decls(std::ostream & out) const {
-            unsigned sz = m_atoms.size();
+            unsigned sz = usize(m_atoms);
             for (unsigned i = 0; i < sz; i++) {
                 if (m_atoms[i] == nullptr)
                     out << "(declare-fun b" << i << " () Bool)\n";