How are Int sort (of SMT-LIB 2.0 Ints theory) and dynamically declared sorts defined in z3?

Question

Here is an SMT-LIB 2.0 benchmark which I executed with z3 :

(set-logic AUFLIA)
(declare-sort PZ 0)
(declare-fun MS (Int PZ) Bool)

(assert (forall ((x Int)) (exists ((X PZ)) 
            (and (MS x X) 
                 (forall ((y Int)) (=> (MS y X) (= y x)))))))
(check-sat)

I expected the result to be sat, with at least a model where PZ is the powerset of Z (integers) and MS is a predicate which tests the membership of an integer into a subset of Z (an element of the sort PZ).

But z3 answered unsat.

Could you help me understanding this result please ? Specifically, how does z3 interprets the sort Int ? Is it really considered infinite ? What about dynamically declared sort (here the sort PZ) ?

Answer 1

In Z3, Int is infinite. You are correct, the result must be sat. The unsat result is due to a bug in one of the Z3 modules. I've already fixed the bug. One temporary cache in the implementation was not being reset. The fix will be available in the next release. In the meantime, you can disable the buggy module by using the following command in the beginning of your script.

(set-option :mbqi false)

BTW, the bug only affects examples that contain literals of the form (= x y) where x and y are universal variables.

BTW, although your example is satisfiable, Z3 can't build a model for it (even after the bug fix). Actually, after the bug fix, Z3 produces the answer unknown. The model finder (used in Z3) is only capable of finding models where the interpretation of uninterpreted sorts (such as PZ) is finite. This limitation may change in the future.