How are Int sort (of SMT-LIB 2.0 Ints theory) and dynamically declared sorts defined in z3?
set, smt, types, z3
Solution
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.
Problem
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`) ?