Reject declarations that clash with built-in signatures (#10411)

## Summary
- reject declarations and definitions whose argument sorts collide with
a built-in signature
- preserve overloads whose argument sorts remain distinguishable
- add SMT-LIB parser regression coverage

Fixes #10404

## Testing
- `test-z3 smt2print_parse`
- `test-z3 /a` (94 passed)

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: a8f87ede-b718-4fe9-9839-cc9eaaf9c3a7

src/cmd_context/cmd_context.cpp

@@ -373,6 +373,19 @@ bool cmd_context::contains_func_decl(symbol const& s, unsigned n, sort* const* d
     return m_func_decls.find(s, fs) && fs.contains(n, domain, range);
 }
 
+bool cmd_context::builtin_signature_collides(symbol const& s, unsigned arity, sort* const* domain) const {
+    expr_ref_vector args(m());
+    for (unsigned i = 0; i < arity; ++i)
+        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);
+    }
+    catch (ast_exception&) {
+        return false;
+    }
+}
+
 bool cmd_context::contains_macro(symbol const& s) const {
     macro_decls decls;
     return m_macros.find(s, decls) && !decls.empty();
@@ -938,11 +951,12 @@ void cmd_context::insert(symbol const & s, func_decl * f) {
     if (contains_macro(s, f)) {
         throw cmd_exception("invalid declaration, named expression already defined with this name ", s);
     }
-#if 0
-    if (m_builtin_decls.contains(s)) {
-        throw cmd_exception("invalid declaration, builtin symbol ", s);
+    if (builtin_signature_collides(s, f->get_arity(), f->get_domain())) {
+        std::string msg = "invalid declaration, builtin symbol '";
+        msg += s.str();
+        msg += "' has the same argument sorts";
+        throw cmd_exception(std::move(msg));
     }
-#endif
     func_decls & fs = m_func_decls.insert_if_not_there(s, func_decls());
     if (!fs.insert(m(), f)) {
         if (m_allow_duplicate_declarations)
@@ -980,11 +994,12 @@ void cmd_context::insert(symbol const & s, psort_decl * p) {
 
 void cmd_context::insert(symbol const & s, unsigned arity, sort *const* domain, expr * t) {
     expr_ref _t(t, m());
-#if 0
-    if (m_builtin_decls.contains(s)) {
-        throw cmd_exception("invalid macro/named expression, builtin symbol ", s);
+    if (builtin_signature_collides(s, arity, domain)) {
+        std::string msg = "invalid named expression, builtin symbol '";
+        msg += s.str();
+        msg += "' has the same argument sorts";
+        throw cmd_exception(std::move(msg));
     }
-#endif
     if (contains_macro(s, arity, domain)) {
         throw cmd_exception("named expression already defined");
     }
@@ -2570,4 +2585,3 @@ std::ostream & operator<<(std::ostream & out, cmd_context::status st) {
     }
     return out;
 }
-

src/cmd_context/cmd_context.h

@@ -364,6 +364,7 @@ protected:
     void mk_solver();
 
     bool contains_func_decl(symbol const& s, unsigned n, sort* const* domain, sort* range) const;
+    bool builtin_signature_collides(symbol const& s, unsigned arity, sort* const* domain) const;
 
     bool contains_macro(symbol const& s) const;
     bool contains_macro(symbol const& s, func_decl* f) const;
@@ -581,4 +582,3 @@ public:
 
 std::ostream & operator<<(std::ostream & out, cmd_context::status st);
 
-

src/test/smt2print_parse.cpp

@@ -257,6 +257,36 @@ void test_symbol_escape() {
     std::cout << "done evaluating\n";
 }
 
+void test_builtin_signature_clash() {
+    char const* rejected[] = {
+        "(declare-fun and (Bool Bool) Int)",
+        "(define-fun not ((a Bool)) Bool false)",
+        "(declare-const true Bool)",
+        "(define-fun = ((a Int) (b Int)) Bool true)",
+        "(define-fun ite ((c Bool) (a Int) (b Int)) Int 0)",
+        "(define-fun + ((a Int) (b Int)) Int 0)",
+        "(define-fun-rec and ((a Bool) (b Bool)) Bool false)"
+    };
+
+    for (char const* spec : rejected) {
+        Z3_context ctx = Z3_mk_context(nullptr);
+        Z3_set_error_handler(ctx, setError);
+        is_error = false;
+        Z3_parse_smtlib2_string(ctx, spec, 0, nullptr, nullptr, 0, nullptr, nullptr);
+        ENSURE(is_error);
+        Z3_del_context(ctx);
+    }
+
+    Z3_context ctx = Z3_mk_context(nullptr);
+    Z3_set_error_handler(ctx, setError);
+    test_eval(ctx,
+              "(declare-fun and (Int Int) Int)\n"
+              "(assert (= (and 1 2) 0))\n"
+              "(check-sat)\n",
+              false);
+    Z3_del_context(ctx);
+}
+
 void tst_smt2print_parse() {
 
     // test basic datatypes  
@@ -326,6 +356,7 @@ void tst_smt2print_parse() {
     test_ho_choice_expression();
 
     test_symbol_escape();
+    test_builtin_signature_clash();
 
     // Regression test for GitHub issue #10166:
     // With (set-option :smtlib2_compliant true), a formula involving to_real