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

Don't reject re-declaration of internal auxiliary functions like /0

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

9
src/cmd_context/cmd_context.cpp
View file

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