Combination of sequences and quantifiers

[aengelke]

Is the combination of sequences and quantifiers (currently) supported? If not, it would be great to receive confirmation about this.

Example (I'm aware that this is overly complicated):

(declare-const x (Seq Int))
(declare-const y (Seq Int))
(assert (= (seq.len x) 10))
(assert (= (seq.len y) 10))
(assert (forall ((i Int)) (= (seq.at x i) (seq.at y i))))
(check-sat)
(check-sat-using (then qe smt))
; Result: unknown unknown

[NikolajBjorner]

There are no quantifier elimination algorithms for general sequences (Quine). There are some special classes, such as "queues". Ting Zhang's thesis considers these with length constraints. If you want to implement a quantifier elimination plugin for these cases you are welcome to add a pull request.