Regression: theory mismatch no longer recognized when parsing SMTLIB, 0/1 are booleans.

[kfriedberger]

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.

[NikolajBjorner]

The motivation is to allow using Booleans as 0-1 integers. This is super convenient in many cases. You can:

(set-option :smtlib2_compliant true) (declare-fun x () Bool) (assert (= 5 x)) (check-sat) (get-model)

[kfriedberger]

The parsing of 0/1 as boolean values is a valid idea and not the problem.

When using the API with your option, via Native.setParamValue(config, "smtlib2_compliant", "true"), we get WARNING: parameter smtlib2_compliant can only be set for the shell, not binary API. How can we enforce well-typed formulas using the method parseSmtlib2String?

[kfriedberger]

If this issue can not be fixed with some option, we can update the tests in our appliction and will ignore this regression. Best.

[NikolajBjorner]

or simply allow this option from API use. The reason to disallow it would be that it doubles as printing "success" and thereby creating an output stream.

[NikolajBjorner]

but from where I sit, the more useful approach would be to allow the 0/1 reading. We already insert coercions for int -> real, and you could write (+ 0 true) before 13.3, so accepting (= 0 true) is a way to be consistent.