mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-07 14:32:06 +00:00
Code Activity

Allow define-fun of internal /0, div0, mod0, ^0 functions

Browse source 
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>
This commit is contained in:
z3prover-ci-bot[bot] 2026-08-06 07:01:34 +00:00 • committed by GitHub
parent 9167020d83
commit 2e7487a3b5
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 10 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/cmd_context/cmd_context.cpp
View file

@ -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;