Why does 0 = 0.5?

Question

I noticed some strange behavior with Z3 4.3.1 when working with .smt2 files.

If I do (assert (= 0 0.5)) it will be satisfiable. However, if I switch the order and do (assert (= 0.5 0)) it's not satisfiable.

My guess as to what is happening is that if the first parameter is an integer, it casts both of them to integers (rounding 0.5 down to 0), then does the comparison. If I change "0" to "0.0" it works as expected. This is in contrast to most programming languages I've worked with where if either of the parameters is a floating-point number, they are both cast to floating-point numbers and compared. Is this really the expected behavior in Z3?

Answer 1

Z3 is not the unique SMT solver that type-checks these examples:

• CVC4 accepts them as well (even with option --smtlib-strict), and answers UNSAT in both cases of my formulas above.

• Yices accepts them and answers UNSAT (after changing the logic to QF_LIA, because it does not support AUFLIRA).

• With (set-logic QF_LIA), Z3 emits an error: (error "line 3 column 17: logic does not support reals").

• Alt-Ergo says "typing error: Int and Real cannot be unified" in both cases. But Alt-Ergo's SMT2 parser is very limited and not heavily tested, as we concentrated on its native polymorphic language. So, it should not be taken as a reference.

I think that developers usually assume an "implicit" sub-typing relation between Int and Real. This is why these examples are successfully type-checked by Z3, CVC4 and Yices (and probably others as well).