From 2e7487a3b50d4d95b7cc3fc6d6753392b1196068 Mon Sep 17 00:00:00 2001
From: "z3prover-ci-bot[bot]"
 <305651407+z3prover-ci-bot[bot]@users.noreply.github.com>
Date: Thu, 6 Aug 2026 07:01:34 +0000
Subject: [PATCH] Allow define-fun of internal /0, div0, mod0, ^0 functions

The builtin-signature collision check added in #10411 rejected user
define-fun/declare-fun of Z3's internal under-specified division,
modulo and power-by-zero functions (/0, div0, mod0, ^0). Z3 itself
emits these as define-fun declarations when printing models, so the
collision check broke round-tripping Z3's own output (issue #6524
benchmark). Exclude these internal functions from the collision check
while still rejecting genuine builtin overloads.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 src/cmd_context/cmd_context.cpp | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 8a0f856b66..704ca889c0 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -379,7 +379,16 @@ bool cmd_context::builtin_signature_collides(symbol const& s, unsigned arity, so
         args.push_back(m().mk_var(i, domain[i]));
     expr_ref result(m());
     try {
-        return try_mk_builtin_app(s, arity, args.data(), 0, nullptr, nullptr, result);
+        if (!try_mk_builtin_app(s, arity, args.data(), 0, nullptr, nullptr, result))
+            return false;
+        // Z3's under-specified division/modulo/power-by-zero functions ('/0',
+        // 'div0', 'mod0', '^0') are internal artifacts that Z3 itself emits as
+        // 'define-fun' declarations when printing models. Allow user
+        // definitions of these so that Z3 can parse back its own output.
+        arith_util au(m());
+        if (au.is_div0(result) || au.is_idiv0(result) || au.is_mod0(result) || au.is_power0(result))
+            return false;
+        return true;
     }
     catch (ast_exception&) {
         return false;