From 9695ceafbc76c74aca0d677eb55b235813089694 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 14:35:18 -0700
Subject: [PATCH] [snapshot-regression-fix] Allow shadowing non-core nullary
 builtins (pi, euler) (#10424)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

## Summary

Fixes a regression detected by the snapshot-regression corpus.

- Originating discussion:
https://github.com/Z3Prover/bench/discussions/3514
- Benchmark ref: `iss-2795/bug-1.smt2`

## Divergence

```diff
--- bug-1.expected.out (expected)
+++ produced (current z3)
@@ -1 +1,2 @@
+(error "line 3 column 23: invalid declaration, builtin symbol 'pi' has the same argument sorts")
 unsat
```

The benchmark declares `(declare-fun pi () Real)`. The expected oracle
is `unsat`; current z3 instead errors out before solving.

## Root cause

Commit 2999517d5 (#10411, "Reject declarations that clash with built-in
signatures") added `cmd_context::builtin_signature_collides`, which
rejects any user declaration whose name resolves to a built-in
application. For **nullary** symbols there are no argument sorts to
distinguish an overload, so this also rejected declarations of
Z3-specific arithmetic *extension* constants such as `pi` and `euler`
(registered as `OP_PI` / `OP_E` in `arith_decl_plugin`). These are not
SMT-LIB reserved symbols and were historically allowed to be shadowed by
user declarations, which is what `iss-2795/bug-1.smt2` relies on.

## Fix

In `builtin_signature_collides`, keep rejecting:
- any collision with `arity > 0` (real overload clash), and
- nullary symbols that resolve into the **basic** theory family (genuine
reserved core constants such as `true`/`false`).

Allow nullary symbols that resolve into non-core theory plugins (e.g.
`pi`, `euler`) to be shadowed. The change is confined to
`src/cmd_context/cmd_context.cpp`.

## Validation

Rebuilt z3 (`make -j8` from `scripts/mk_make.py`) and re-ran the
benchmark:

```
$ ./z3 -T:20 inputs/issues/iss-2795/bug-1.smt2
unsat
```

which now matches the recorded oracle. Also confirmed the intended
#10411 rejections still fire:
- `(declare-fun and (Bool Bool) Int)` -> rejected
- `(declare-const true Bool)` -> rejected
- `(define-fun + ((a Int)(b Int)) Int 0)` -> rejected
- `(declare-fun pi () Real)` / `(declare-fun euler () Real)` -> now
accepted




> [!WARNING]
> <details>
> <summary>Firewall blocked 1 domain</summary>
>
> The following domain was blocked by the firewall during workflow
execution:
>
> - `pypi.org`
>> To allow these domains, add them to the `network.allowed` list in
your workflow frontmatter:
>
> ```yaml
> network:
>   allowed:
>     - defaults
>     - "pypi.org"
> ```
>
> See [Network
Configuration](https://github.github.com/gh-aw/reference/network/) for
more information.
>
> </details>


> Generated by [Fix a Z3 snapshot-regression
divergence](https://github.com/Z3Prover/bench/actions/runs/31074578887)
· 190.8 AIC · ⌖ 19.6 AIC · ⊞ 10.7K ·
[◷](https://github.com/search?q=repo%3AZ3Prover%2Fz3+%22gh-aw-workflow-id%3A+snapshot-regression-fixer%22&type=pullrequests)

<!-- gh-aw-agentic-workflow: Fix a Z3 snapshot-regression divergence,
engine: copilot, version: 1.0.65, model: claude-opus-4.8, id:
31074578887, workflow_id: snapshot-regression-fixer, run:
https://github.com/Z3Prover/bench/actions/runs/31074578887 -->

<!-- gh-aw-workflow-id: snapshot-regression-fixer -->
<!-- gh-aw-workflow-call-id: Z3Prover/bench/snapshot-regression-fixer
-->

Co-authored-by: z3prover-ci-bot[bot] <305651407+z3prover-ci-bot[bot]@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 src/cmd_context/cmd_context.cpp | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 8a0f856b66..90b9f00388 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -379,11 +379,22 @@ 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;
     }
+    // A function/overload collision (arity > 0) is always rejected: the user
+    // declaration would clash with a built-in of the same argument sorts.
+    if (arity > 0)
+        return true;
+    // For nullary symbols there are no argument sorts to distinguish an
+    // overload. Only genuine reserved core constants (e.g. true/false in the
+    // basic theory) block a user declaration. Z3-specific extension constants
+    // such as 'pi' and 'euler' are not SMT-LIB reserved symbols and may be
+    // shadowed by user declarations, as was historically permitted.
+    return is_app(result) && to_app(result)->get_family_id() == m().get_basic_family_id();
 }
 
 bool cmd_context::contains_macro(symbol const& s) const {