There is a regression from Z3 v4.13.0 to v4.13.2.
We found it using the Java API. However, executing the binary also shows the issue:

Input 1

(declare-fun x () Bool)
(assert (= 0 x))
(check-sat)
(get-model)

Output with v4.13.0:

(error "line 2 column 14: Sorts Int and Bool are incompatible")
sat
((define-fun x () Bool false))

Output with v4.13.2:

sat
((define-fun x () Bool false))

i.e., no more error.

Input 2

(declare-fun x () Bool)
(assert (= 5 x))
(check-sat)
(get-model)

Output with v4.13.0:

(error "line 2 column 14: Sorts Int and Bool are incompatible")
sat
((define-fun x () Bool false))

Output with v4.13.2:

unsat
(error "line 4 column 10: model is not available")

i.e., no more error on theory mismatch, but unsat. Why? Because Boolean can be true|false which is is 1|0 and can not be equal to 5?

Would it be possible to keep the old behaviour?
We would like to get an error as soon as the user enters formulas with incompatible types.