From e503ead008ecd3d9a8ca4df612924493b450e40f Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Tue, 21 Apr 2026 20:37:53 +0000
Subject: [PATCH] Address review feedback for qe-lite BV case split changes

Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/53219443-a721-4e6d-a7c3-21a6387b3396

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/qe/lite/qe_lite_tactic.cpp | 30 +++++++++++++++---------------
 src/test/qe_arith.cpp          | 18 +-----------------
 2 files changed, 16 insertions(+), 32 deletions(-)

diff --git a/src/qe/lite/qe_lite_tactic.cpp b/src/qe/lite/qe_lite_tactic.cpp
index 5aea40a7e..3321196c3 100644
--- a/src/qe/lite/qe_lite_tactic.cpp
+++ b/src/qe/lite/qe_lite_tactic.cpp
@@ -2546,11 +2546,11 @@ private:
 
     bool mk_bv_default_case(unsigned bv_size, obj_hashtable<expr> const& values, expr_ref& value) {
         bv_util bv(m);
-        uint64_t max_num = values.size() + 1;
-        if (bv_size < 63)
-            max_num = std::min<uint64_t>(max_num, uint64_t(1) << bv_size);
-        for (uint64_t i = 0; i < max_num; ++i) {
-            value = bv.mk_numeral(rational(static_cast<unsigned>(i)), bv_size);
+        unsigned max_num = values.size() + 1;
+        if (bv_size < sizeof(unsigned) * 8)
+            max_num = std::min<unsigned>(max_num, (1u << bv_size));
+        for (unsigned i = 0; i < max_num; ++i) {
+            value = bv.mk_numeral(rational(i), bv_size);
             if (!values.contains(value))
                 return true;
         }
@@ -2577,11 +2577,9 @@ private:
         for (unsigned i = 0; i < num_decls; ++i) {
             if (!uv.contains(i))
                 continue;
-            sort* s = uv.contains(i);
-            if (!s)
-                return false;
+            sort* var_sort = q->get_decl_sort(num_decls - i - 1);
             bv_util bv(m);
-            if (!bv.is_bv_sort(s))
+            if (!bv.is_bv_sort(var_sort))
                 return false;
             obj_hashtable<expr> values;
             if (!collect_bv_eq_constants(body, i, values) || values.empty())
@@ -2593,7 +2591,7 @@ private:
             for (expr* v : values)
                 var_cases.values.push_back(v);
             expr_ref other(m);
-            if (mk_bv_default_case(bv.get_bv_size(s), values, other))
+            if (mk_bv_default_case(bv.get_bv_size(var_sort), values, other))
                 var_cases.values.push_back(other);
             if (var_cases.values.empty())
                 return false;
@@ -2625,15 +2623,17 @@ private:
             m_rewriter(inst);
             disjuncts.push_back(inst);
 
-            unsigned j = case_ix.size();
-            while (j > 0) {
-                --j;
+            // Increment mixed-radix counter over case_ix; if all positions wrap, stop.
+            bool wrapped = true;
+            for (unsigned j = case_ix.size(); j-- > 0; ) {
                 ++case_ix[j];
-                if (case_ix[j] < case_vars[j].values.size())
+                if (case_ix[j] < case_vars[j].values.size()) {
+                    wrapped = false;
                     break;
+                }
                 case_ix[j] = 0;
             }
-            if (j == 0 && case_ix[0] == 0)
+            if (wrapped)
                 break;
         }
 
diff --git a/src/test/qe_arith.cpp b/src/test/qe_arith.cpp
index 9cdfdf670..c944c0b25 100644
--- a/src/test/qe_arith.cpp
+++ b/src/test/qe_arith.cpp
@@ -13,7 +13,6 @@ Copyright (c) 2015 Microsoft Corporation
 #include "ast/reg_decl_plugins.h"
 #include "ast/rewriter/arith_rewriter.h"
 #include "ast/ast_pp.h"
-#include "ast/for_each_expr.h"
 #include "smt/smt_context.h"
 #include "ast/expr_abstract.h"
 #include "ast/rewriter/expr_safe_replace.h"
@@ -54,21 +53,6 @@ static expr_ref parse_smt2_assertion(ast_manager& m, char const* script) {
     return result;
 }
 
-namespace qe_arith_test {
-    struct find_q_proc {
-        quantifier* m_q = nullptr;
-        void operator()(var*) {}
-        void operator()(app*) {}
-        void operator()(quantifier* q) { m_q = q; }
-    };
-}
-
-static quantifier* find_quantifier(expr* n) {
-    qe_arith_test::find_q_proc p;
-    for_each_expr(p, n);
-    return p.m_q;
-}
-
 static void test_qe_lite_bv_eq_cases() {
     ast_manager m;
     reg_decl_plugins(m);
@@ -87,7 +71,7 @@ static void test_qe_lite_bv_eq_cases() {
     qe_lite qel(m, params_ref());
     proof_ref pr(m);
     qel(fml, pr);
-    VERIFY(find_quantifier(fml) == nullptr);
+    VERIFY(!has_quantifiers(fml));
 
     smt_params params;
     smt::context ctx(m, params);