Fix implicit conversion warnings: use UINT_MAX instead of -1 for unsi… (#8342)

* Fix implicit conversion warnings: use UINT_MAX instead of -1 for unsigned variables

Replace implicit conversion from negative literal to unsigned type
with explicit UINT_MAX constant to eliminate compiler warnings.

Fixed 10 instances across 6 files:
- src/ast/rewriter/bv_rewriter.cpp: 1 instance
- src/ast/sls/sls_bv_tracker.h: 2 instances
- src/math/lp/dioph_eq.cpp: 3 instances
- src/math/lp/lp_primal_core_solver.h: 2 instances
- src/muz/transforms/dl_mk_array_instantiation.cpp: 1 instance
- src/muz/transforms/dl_mk_synchronize.cpp: 1 instance

These changes preserve the exact same runtime behavior (UINT_MAX
equals the wrapped value of -1 for unsigned types) while making
the code more explicit and warning-free.

* Update bv_rewriter.cpp

---------

Co-authored-by: github-actions[bot] <github-actions[bot]@users.noreply.github.com>

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

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