use usize to suppress the data loss warnings

Signed-off-by: Lev Nachmanson <[email protected]>

Author: levnach

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()) {

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