The equality operator in SMT-LIB generally requires, unsurprisingly, that its operands be of the same type. For example, this is an error:
(set-logic QF_LIRA)
(declare-fun a () Bool)
(declare-fun b () Real)
(assert (= a b))
(check-sat)
However, I expected this to be likewise an error:
(set-logic QF_LIRA)
(declare-fun a () Int)
(declare-fun b () Real)
(assert (= a b))
(check-sat)
But Yices and Z3 both accept it without complaint.
What am I missing?
Strictly speaking, such mixing-and-matching is not allowed by SMTLib. (See page 37 of https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf, where it clearly states = must take two arguments of the same sort.)
However, most solvers are "lenient" in their processing; i.e., they introduce coercions when they think it "makes sense." I personally find that problematic: Coercions are hardly ever useful (especially in a language that's meant to be generated by tools in general), and sometimes they can hide bugs where the user wanted to say one thing but said the wrong thing, and the system somehow assigned a meaning to it. (You can compare this to mixing and matching of arithmetic with different types in many programming languages. But I digress.)
Having said that, you can ask most solvers to be "more compliant:"
$ z3 smtlib2_compliant=true a.smt2
success
success
success
(error "line 4 column 14: Sort mismatch at argument #1 for function (declare-fun = (Real Real) Bool) supplied sort is Int")
sat
Note the smtlib2_compliant parameter on the command line. Similarly, cvc5 can be made more strict too:
$ cvc5 --strict-parsing a.smt2
(error "Parse Error: a.smt2:4.15: Subexpressions must have the same type:
Equation: (= a b)
Type 1: Int
Type 2: Real
")
Note that I explicitly had to pass --strict-parsing argument, as it also inserts the coercion without that flag.
My personal opinion is that they should all be compliant at all times; but the state of the affairs is that most solvers introduce these coercions leading to confusion at best, and hiding bugs at worst. For instance, you don't really know if it "downcasts" (i.e., truncates in some way) the real to an integer and checks the equality; or if it "upcasts" the integer to a real. There's no easy way to tell which one has happened without actually checking the code itself. (In this particular case, both solvers upcast the integer to a real; so it's sound.)