z3 序列问题的策略

Question

对于无量词序列问题，我应该考虑哪些具体策略？我得到未知的可满足性解决问题，如下面的问题（找到一个包含一个值但不包含另一个值的序列）。 我使用的是 z3 的 4.8.5.0 版本。

(declare-const l (Seq Int))
(declare-const x Int)
(declare-const y Int)
(assert (not (seq.contains l (seq.unit y))))
(assert (seq.contains l (seq.unit x)))

(check-sat)

[结果未知]

Answer 1

序列逻辑最近经历了一系列变化。当我使用来自他们的 github 源的全新 z3 版本尝试您的基准测试时，它成功报告了sat。见这里：https://github.com/Z3Prover/z3

在接触新战术之前，如果你能使用github版本会很棒。