Attempting to redefine core symbols

[Heaven2024]

(declare-fun and (Bool Bool) Bool)
(assert (and true false))
(check-sat)

z3 xx.smt2
sat

I would like to know whether z3 allows the operation of this kind of definition,maybe it would be safer to ban this behavior?

[LeventErkok]

This has been discussed earlier, in the context of SMTLib: There's a record of it at SMT-LIB/SMT-LIB-2#3

Bottom line: Strictly speaking, this isn't allowed. Only theories can overload symbols, not user scripts. But z3 is being more liberal. Whether there's enough ROI to actually fix it is something only the developers can decide. Note that SMTLib is typically "generated" as opposed to "hand-written," so there's an argument that this should be caught at a higher-level and the flexibility here can be helpful for overloading symbols at theory level.

Another note: The upcoming SMTLib standard (v3?) will have modifications around polymorphism/overloading etc., which might make this sort of redefinitions more clear. Overloading at a base type (like Bool) might still be disallowed; but it makes perfect sense to overload at user-defined types, for instance.