Issue with tactic `qsat`

[merlinsun]

Hi, For this following instance, z3 https://github.com/Z3Prover/z3/commit/8f4ffc7caf19ba9c7b4c63935ef19cef215e847f incorrectly returns unsat with (check-sat-using qsat).

$ z3 small.smt2 
sat
unsat
$ cat small.smt2 
(declare-const x (Array Bool Bool))
(declare-fun a () (Array Bool Bool))
(assert (forall ((v (Array (Array Bool Bool) Real))) (= 0.0 (select (store v x 0.0) a))))
(check-sat)
(check-sat-using qsat)

[NikolajBjorner]

It is related to qel.

z3 7217.smt2 /v:2 smt.qsat_use_qel=false

[hgvk94]

Yes. It has to do with arrays indexed by other arrays and arrays indexed by finite types. The current MBP (and the earlier one) does not support this fragment. Its going to take a while to actually fix it. The current implementation was done so that it doesn't break on Leo's benchmarks from Solidity (which have arrays indexed by other arrays). So we can't fully disable it for the fragment either.

[NikolajBjorner]

we could add a filter that rules out qel on formulas outside of supported fragment. What is the specification of the filter?