Invalid model for QF_ALIA instance

[5hadowblad3]

Hi, for the following instance

(set-logic QF_ALIA)
(set-option :model_validate true)
(set-option :combined_solver.ignore_solver1 true)
(set-option :smt.array.extensional false)
(declare-const arr--3045560570942142408_-1212997213155739362-0 (Array (Array Int Int) Bool))
(declare-const arr--3045560570942142408_-1212997213155739362-1 (Array (Array Int Int) Bool))
(assert (distinct arr--3045560570942142408_-1212997213155739362-1 arr--3045560570942142408_-1212997213155739362-0))
(check-sat)
(exit)

commit cf0952c

[rainoftime]

According to #3556, smt.array.extensional should not be closed?

[NikolajBjorner]

right, don't disable extensionality when you actually need it!