model_validate smt.array.extensional invalid model on Set logic formula

[muchang]

Hi,
For this formula:

(set-option :model_validate true)
(set-option :smt.array.extensional false)
(declare-fun a () (Set Int))
(declare-fun b () (Set Int))
(assert (distinct a b))
(push)
(check-sat)

Z3 gives an invalid model:

[627] % z3 small.smt2
sat
(error "line 7 column 10: an invalid model was generated")
[628] % 
[628] % cat small.smt2
(set-option :model_validate true)
(set-option :smt.array.extensional false)
(declare-fun a () (Set Int))
(declare-fun b () (Set Int))
(assert (distinct a b))
(push)
(check-sat)
[629] %

OS: Ubuntu 18.04
Commit: 9be7bda

[rainoftime]

The case is interesting. Seems z3 uses array theory to "simulate" set operations (at the level of C API).

[NikolajBjorner]

I don't think it is sane to disable extensionality when you rely on it.