diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index 7e03b62d1..1db2534cb 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -24,7 +24,6 @@ Notes:
 #include "ast/ast_pp.h"
 
 
-
 void bv_rewriter::updt_local_params(params_ref const & _p) {
     bv_rewriter_params p(_p);
     m_hi_div0 = p.hi_div0();
@@ -683,7 +682,7 @@ unsigned bv_rewriter::propagate_extract(unsigned high, expr * arg, expr_ref & re
     bool all_numerals = true;
     unsigned removable = to_remove;
     numeral val;
-    unsigned curr_first_sz = -1;
+    unsigned curr_first_sz = UINT_MAX;
     // calculate how much can be removed
     for (unsigned i = 0; i < num; ++i) {
         expr * const curr = a->get_arg(i);
diff --git a/src/ast/sls/sls_bv_tracker.h b/src/ast/sls/sls_bv_tracker.h
index cf76e4f9a..a078de5a1 100644
--- a/src/ast/sls/sls_bv_tracker.h
+++ b/src/ast/sls/sls_bv_tracker.h
@@ -1037,7 +1037,7 @@ public:
         }
         m_temp_constants.reset();
 
-        unsigned pos = -1;
+        unsigned pos = UINT_MAX;
         if (m_ucb)
         {
             double max = -1.0;
@@ -1090,7 +1090,7 @@ public:
             return nullptr;
         m_temp_constants.reset();
         
-        unsigned cnt_unsat = 0, pos = -1;
+        unsigned cnt_unsat = 0, pos = UINT_MAX;
         for (unsigned i = 0; i < sz; ++i)
             if ((i != m_last_pos) && m_mpz_manager.neq(get_value(as[i]), m_one) && (get_random_uint(16) % ++cnt_unsat == 0)) pos = i;
 
diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp
index acc76bb11..96c85a91f 100644
--- a/src/math/lp/dioph_eq.cpp
+++ b/src/math/lp/dioph_eq.cpp
@@ -2111,7 +2111,7 @@ namespace lp {
         std::tuple<mpq, unsigned, int, unsigned> find_minimal_abs_coeff(unsigned ei) {
             bool first = true;
             mpq ahk;
-            unsigned k = -1;
+            unsigned k = UINT_MAX;
             int k_sign = 0;
             mpq t;
             for (const auto& p : m_e_matrix.m_rows[ei]) {
@@ -2485,12 +2485,12 @@ namespace lp {
         lia_move rewrite_eqs(std_vector<unsigned>& f_vector) {
             if (f_vector.size() == 0)
                 return lia_move::undef;
-            unsigned h = -1, kh = 0; // the initial value of kh does not matter, assign to remove the warning
+            unsigned h = UINT_MAX, kh = 0; // the initial value of kh does not matter, assign to remove the warning
             unsigned n = 0;  // number of choices for a fresh variable
             mpq min_ahk;
             int kh_sign = 0; // the initial values of kh_sign and h_markovich_number do not matter, assign to remove the warning
             unsigned h_markovich_number = 0;
-            unsigned ih = -1; // f_vector[ih] = h
+            unsigned ih = UINT_MAX; // f_vector[ih] = h
             for (unsigned i = 0; i < f_vector.size(); ++i) {
                 unsigned ei = f_vector[i];
                 SASSERT (belongs_to_f(ei));
diff --git a/src/math/lp/lp_primal_core_solver.h b/src/math/lp/lp_primal_core_solver.h
index 729b5cebc..d1ac780e8 100644
--- a/src/math/lp/lp_primal_core_solver.h
+++ b/src/math/lp/lp_primal_core_solver.h
@@ -191,8 +191,8 @@ namespace lp {
             // least one pivot operation
             int choice = -1;
             int nchoices = 0;
-            unsigned min_non_free_so_far = -1;
-            unsigned best_col_sz = -1;
+            unsigned min_non_free_so_far = UINT_MAX;
+            unsigned best_col_sz = UINT_MAX;
             unsigned bj = this->m_basis[i];
             bool bj_needs_to_grow = needs_to_grow(bj);
             for (unsigned k = 0; k < this->m_A.m_rows[i].size(); ++k) {
diff --git a/src/muz/transforms/dl_mk_array_instantiation.cpp b/src/muz/transforms/dl_mk_array_instantiation.cpp
index f694f5b5e..ed1c409ea 100644
--- a/src/muz/transforms/dl_mk_array_instantiation.cpp
+++ b/src/muz/transforms/dl_mk_array_instantiation.cpp
@@ -277,7 +277,7 @@ namespace datalog {
                 new_args.push_back(arg_correspondance[i][chosen[i]].get());
             }
             res.push_back(create_pred(old_pred, new_args));
-            unsigned pos=-1;
+            unsigned pos = UINT_MAX;
             do {
                 pos++;
                 if(pos==chosen.size()){
diff --git a/src/muz/transforms/dl_mk_synchronize.cpp b/src/muz/transforms/dl_mk_synchronize.cpp
index c24b0164d..81c01d7fc 100644
--- a/src/muz/transforms/dl_mk_synchronize.cpp
+++ b/src/muz/transforms/dl_mk_synchronize.cpp
@@ -290,7 +290,7 @@ namespace datalog {
         bool_vector new_tail_neg;
         new_tail.resize(product_tail_length);
         new_tail_neg.resize(product_tail_length);
-        unsigned tail_idx = -1;
+        unsigned tail_idx = UINT_MAX;
         if (has_recursion) {
             add_rec_tail(recursive_calls, new_tail, new_tail_neg, tail_idx);
         }