From ee3ccabdd907b868ebf11d130a69b02d2d0200a5 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 06:02:39 +0000
Subject: [PATCH] Don't reject re-declaration of internal auxiliary functions
 like /0

The builtin-signature collision check (introduced in #10411) rejected any
declaration/definition whose name+argument-sorts resolve to a builtin. This
also caught internal auxiliary operators such as /0, div0, mod0 and ^0, which
z3's own model printer emits as define-fun. Feeding such a model back into z3
then failed to parse. Exclude functions that are is_considered_uninterpreted
(the internal aux ops) from the collision check while still rejecting genuine
builtins.

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

diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 8a0f856b66..24b771659a 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -379,11 +379,18 @@ 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;
     }
     catch (ast_exception&) {
         return false;
     }
+    // Internal auxiliary functions (e.g. division/mod/power by zero: '/0', 'div0',
+    // 'mod0', '^0') are emitted by the model printer and must be re-parseable, so
+    // they are not treated as colliding with a user declaration/definition.
+    if (is_app(result) && m().is_considered_uninterpreted(to_app(result)->get_decl()))
+        return false;
+    return true;
 }
 
 bool cmd_context::contains_macro(symbol const& s) const {