From ad9d9d12fb1385ab79c864aeb4096e690f21c75a Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 20 Jun 2025 21:55:35 +0000 Subject: [PATCH] Add normalization for to_int expressions in division by zero contexts Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/rewriter/arith_rewriter.cpp | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 33fc9c4fa..350cba748 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -1137,13 +1137,21 @@ br_status arith_rewriter::mk_div_core(expr * arg1, expr * arg2, expr_ref & resul set_curr_sort(arg1->get_sort()); numeral v1, v2; bool is_int; + + // Special handling for division by zero with to_int expressions + // Ensure (div (to_int x) 0) is treated consistently with (div x 0) + expr* to_int_arg; + if (m_util.is_to_int(arg1, to_int_arg) && m_util.is_numeral(arg2, v2, is_int) && v2.is_zero()) { + // Convert (div (to_int x) 0) to (to_int (div x 0)) for consistent handling + expr_ref div_expr(m_util.mk_div(to_int_arg, arg2), m); + result = m_util.mk_to_int(div_expr); + return BR_REWRITE2; + } + if (m_util.is_numeral(arg2, v2, is_int)) { SASSERT(!is_int); if (v2.is_zero()) { - // For division by zero, create a consistent uninterpreted function - // This ensures that (div a 0) and (div (to_int a) 0) are handled consistently - result = m_util.mk_div0(arg1, arg2); - return BR_DONE; + return BR_FAILED; } else if (m_util.is_numeral(arg1, v1, is_int)) { result = m_util.mk_numeral(v1/v2, false);