Search code examples
z3

Tactics for z3 sequence problems

Are there specific tactics I should consider for quantifier-free sequence problems? I am getting unknown satisfiability solving problems like the one below (find a sequence containing one value but not another). I am using version 4.8.5.0 of z3.

(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)

[result is unknown]

Solution

  • Sequence logic recently went through a bunch of changes. When I try your benchmark with a fresh build of z3 from their github sources, it successfully reports sat. See here: https://github.com/Z3Prover/z3

    Before reaching out for new tactics, would be great if you can use the github version.