From b821aebbacf719acd4fa7e391589c99a3a9af709 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Fri, 20 Jun 2025 21:46:57 +0000 Subject: [PATCH] Fix division by zero handling inconsistency in arithmetic rewriter Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/rewriter/arith_rewriter.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 702030c49..33fc9c4fa 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -1140,7 +1140,10 @@ br_status arith_rewriter::mk_div_core(expr * arg1, expr * arg2, expr_ref & resul if (m_util.is_numeral(arg2, v2, is_int)) { SASSERT(!is_int); if (v2.is_zero()) { - return BR_FAILED; + // 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; } else if (m_util.is_numeral(arg1, v1, is_int)) { result = m_util.mk_numeral(v1/v2, false);