diff --git a/src/nlsat/nlsat_simple_checker.cpp b/src/nlsat/nlsat_simple_checker.cpp
index bca4e5adc..c44057234 100644
--- a/src/nlsat/nlsat_simple_checker.cpp
+++ b/src/nlsat/nlsat_simple_checker.cpp
@@ -257,8 +257,8 @@ namespace nlsat {
             for (unsigned i = 0; i < arith_var_num; ++i) {
                 vars_domain.push_back(Var_Domain(am));
             }
-            clauses_visited.resize(clauses.size());
-            literal_special_kind.resize(clauses.size());
+            clauses_visited.resize(static_cast<unsigned>(clauses.size()));
+            literal_special_kind.resize(static_cast<unsigned>(clauses.size()));
         }
         sign_kind to_sign_kind(atom::kind kd) {
             if (kd == atom::EQ)
@@ -1067,7 +1067,7 @@ else { // ( == 0) + (c > 0) -> > 0
    
         bool collect_var_domain() {
             // vector<unsigned> vec_id;
-            for (unsigned i = 0, sz = clauses.size(); i < sz; ++i) {
+            for (unsigned i = 0, sz = static_cast<unsigned>(clauses.size()); i < sz; ++i) {
                 if (clauses_visited[i].visited)
                     continue;
                 if (clauses[i]->size() > 1)
@@ -1099,7 +1099,7 @@ else { // ( == 0) + (c > 0) -> > 0
                     tout << "====== arith[" << i << "] ======\n";
                 }
             );
-            for (unsigned i = 0, sz = clauses.size(); i < sz; ++i) {
+            for (unsigned i = 0, sz = static_cast<unsigned>(clauses.size()); i < sz; ++i) {
                 // unsigned id = vec_id[i];
                 if (!collect_domain_axbsc_form(i, 0))
                     return false;
@@ -1520,7 +1520,7 @@ else { // ( == 0) + (c > 0) -> > 0
             return false;
         }
         bool check() {
-            for (unsigned i = 0, sz = clauses.size(); i < sz; ++i) {
+            for (unsigned i = 0, sz = static_cast<unsigned>(clauses.size()); i < sz; ++i) {
                 if (clauses_visited[i].visited)
                     continue;
                 if (!check_clause_satisfiable(i)) {
diff --git a/src/nlsat/nlsat_simplify.cpp b/src/nlsat/nlsat_simplify.cpp
index 64e3099a1..fdc7f984c 100644
--- a/src/nlsat/nlsat_simplify.cpp
+++ b/src/nlsat/nlsat_simplify.cpp
@@ -33,7 +33,7 @@ namespace nlsat {
             m_learned.clear();
             
             IF_VERBOSE(3, s.display(verbose_stream() << "before\n"));
-            unsigned sz = m_clauses.size();
+            unsigned sz = static_cast<unsigned>(m_clauses.size());
             while (true) {
 
                 subsumption_simplify();
@@ -51,7 +51,7 @@ namespace nlsat {
 
                 split_factors();
 
-                sz = m_clauses.size();
+                sz = static_cast<unsigned>(m_clauses.size());
             }
 
             IF_VERBOSE(3, s.display(verbose_stream() << "after\n"));
@@ -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 = static_cast<unsigned>(m_atoms.size());
             for (unsigned j = 0; j < num_atoms; ++j) {
                 atom* a1 = m_atoms[j];
                 if (a1 && a1->is_ineq_atom()) {
@@ -94,7 +94,7 @@ namespace nlsat {
 
         void update_clauses(u_map<literal> const& b2l) {
             literal_vector lits;
-            unsigned n = m_clauses.size();
+            unsigned n = static_cast<unsigned>(m_clauses.size());
 
             for (unsigned i = 0; i < n; ++i) {
                 clause* c = m_clauses[i];
@@ -334,7 +334,7 @@ namespace nlsat {
         }
 
         bool cleanup_removed() {
-            unsigned j = 0, sz = m_clauses.size();
+            unsigned j = 0, sz = static_cast<unsigned>(m_clauses.size());
             for (unsigned i = 0; i < sz; ++i) {
                 auto c = m_clauses[i];
                 if (c->is_removed())
diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp
index d5a5018b8..323b7dadc 100644
--- a/src/nlsat/nlsat_solver.cpp
+++ b/src/nlsat/nlsat_solver.cpp
@@ -2603,7 +2603,7 @@ namespace nlsat {
         }
 
         bool check_satisfied(clause_vector const & cs) {
-            unsigned sz = cs.size();
+            unsigned sz = static_cast<unsigned>(cs.size());
             for (unsigned i = 0; i < sz; i++) {
                 clause const & c = *(cs[i]);
                 if (!is_satisfied(c)) {
@@ -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 = static_cast<unsigned>(m_atoms.size());
             if (m_bk != null_bool_var)
                 num = m_bk;
             for (bool_var b = 0; b < num; b++) {
@@ -2713,7 +2713,7 @@ namespace nlsat {
             }
 
             void collect(clause_vector const & cs) {
-                unsigned sz = cs.size();
+                unsigned sz = static_cast<unsigned>(cs.size());
                 for (unsigned i = 0; i < sz; i++) 
                     collect(*(cs[i]));
             }
@@ -3045,7 +3045,7 @@ namespace nlsat {
             unsigned num = num_vars();
             for (unsigned i = 0; i < num; i++) {
                 clause_vector & ws = m_watches[i];
-                sort_clauses_by_degree(ws.size(), ws.data());
+                sort_clauses_by_degree(static_cast<unsigned>(ws.size()), ws.data());
             }
         }
 
@@ -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 = static_cast<unsigned>(m_atoms.size());
             if (!eval_atoms) {
                 for (bool_var b = 0; b < sz; b++) {
                     if (m_bvalues[b] == l_undef)
@@ -3945,7 +3945,7 @@ namespace nlsat {
         }
 
         std::ostream& display_mathematica(std::ostream & out, clause_vector const & cs) const {            
-            unsigned sz = cs.size();
+            unsigned sz = static_cast<unsigned>(cs.size());
             for (unsigned i = 0; i < sz; i++) {
                 if (i > 0) out << ",\n";
                 display_mathematica(out << " ", *(cs[i]));
@@ -4011,7 +4011,7 @@ namespace nlsat {
         }
 
         std::ostream& display_smt2_bool_decls(std::ostream & out) const {
-            unsigned sz = m_atoms.size();
+            unsigned sz = static_cast<unsigned>(m_atoms.size());
             for (unsigned i = 0; i < sz; i++) {
                 if (m_atoms[i] == nullptr)
                     out << "(declare-fun b" << i << " () Bool)\n";
diff --git a/src/nlsat/nlsat_variable_ordering_strategy.cpp b/src/nlsat/nlsat_variable_ordering_strategy.cpp
index 3b94e568c..e668cd654 100644
--- a/src/nlsat/nlsat_variable_ordering_strategy.cpp
+++ b/src/nlsat/nlsat_variable_ordering_strategy.cpp
@@ -131,7 +131,7 @@ namespace nlsat {
         }
 
         void collect(clause_vector const & cs) {
-            unsigned sz = cs.size();
+            unsigned sz = static_cast<unsigned>(cs.size());
             for (unsigned i = 0; i < sz; i++) 
                 collect(*(cs[i]));
         }