Fix compiler warnings in test files

- Fix signed/unsigned conversion warnings in model_based_opt.cpp
- Fix signed/unsigned conversion warnings in qe_arith.cpp
- Fix signed/unsigned conversion warning in no_overflow.cpp
- Fix loop bug in permutation.cpp (loop condition was 'i < 0' instead of 'i < sz')

All changes use static_cast for explicit type conversions to eliminate
-Wsign-conversion and -Wsign-compare compiler warnings. The permutation.cpp
fix also corrects a logic bug where the verification loop would never execute.

src/test/model_based_opt.cpp

@@ -59,7 +59,7 @@ static void add_random_ineq(opt::model_based_opt& mbo,
         vars.push_back(var(x, rational(coeff)));
         value += coeff*values[x];
     }
-    unsigned abs_value = value < 0 ? - value : value;
+    unsigned abs_value = value < 0 ? static_cast<unsigned>(- value) : static_cast<unsigned>(value);
     // value + k <= 0
     // k <= - value
     // range for k is 2*|value|

src/test/no_overflow.cpp

@@ -591,7 +591,7 @@ void test_equiv(Equivalence_params params, unsigned bvsize, bool is_signed) {
         cond = Z3_mk_not(ctx, Z3_mk_eq(ctx, t2, Z3_mk_int(ctx, 0, bv)));
     }
 
-    unsigned extsize = params.extsize < 0 ? bvsize : params.extsize;
+    unsigned extsize = params.extsize < 0 ? bvsize : static_cast<unsigned>(params.extsize);
     if (is_signed) {
         min = Z3_mk_sign_ext(ctx, extsize, min);
         max = Z3_mk_sign_ext(ctx, extsize, max);

src/test/permutation.cpp

@@ -66,7 +66,7 @@ static void test_apply_permutation(unsigned sz, unsigned num_tries, unsigned max
         shuffle(p.size(), p.data(), g);
         apply_permutation_copy(sz, data.data(), p.data(), new_data.data());
         apply_permutation(sz, data.data(), p.data());
-        for (unsigned i = 0; i < 0; ++i)
+        for (unsigned i = 0; i < sz; ++i)
             ENSURE(data[i] == new_data[i]);
     }
 }

src/test/qe_arith.cpp

@@ -337,7 +337,7 @@ static void add_random_ineq(
         vars.push_back(var_t(x, rational(coeff)));
         value += coeff*values[x];
     }
-    unsigned abs_value = value < 0 ? - value : value;
+    unsigned abs_value = value < 0 ? static_cast<unsigned>(- value) : static_cast<unsigned>(value);
     // value + k <= 0
     // k <= - value
     // range for k is 2*|value|