From e237100137117a2c5ec81de93ef05c298edc4cef Mon Sep 17 00:00:00 2001
From: Build Warning Fixer <build-warning-fixer@z3prover.github.io>
Date: Wed, 28 Jan 2026 23:27:48 +0000
Subject: [PATCH] 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 | 2 +-
 src/test/no_overflow.cpp     | 2 +-
 src/test/permutation.cpp     | 2 +-
 src/test/qe_arith.cpp        | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/test/model_based_opt.cpp b/src/test/model_based_opt.cpp
index 41bea54d5..98b3c2e88 100644
--- a/src/test/model_based_opt.cpp
+++ b/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|
diff --git a/src/test/no_overflow.cpp b/src/test/no_overflow.cpp
index d70c8c003..ef3b7f0f1 100644
--- a/src/test/no_overflow.cpp
+++ b/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);
diff --git a/src/test/permutation.cpp b/src/test/permutation.cpp
index 9e6a2d671..9839aae08 100644
--- a/src/test/permutation.cpp
+++ b/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]);
     }
 }
diff --git a/src/test/qe_arith.cpp b/src/test/qe_arith.cpp
index af32b2c47..27fccdf4d 100644
--- a/src/test/qe_arith.cpp
+++ b/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|