A simple regex constraint for which dZ3 returns unknown

[hiroshi-unno]

Hi,

For the following simple instance, z3 (https://github.com/Z3Prover/z3/commit/f7d9a5ba935163ddefd3e1883878556d713d6fee) without enabling z3str3 immediately returns unknown.

$ cat dz3_unknown.smt2
(assert (or (= re.all (re.union (str.to_re "y") (re.comp (str.to_re "x"))))
            (= re.all (re.union (str.to_re "x") (re.comp (str.to_re "y"))))))
(check-sat)
$ time z3 dz3_unknown.smt2
unknown

real    0m0.447s
user    0m0.427s
sys     0m0.020s
$ time z3 smt.string_solver=z3str3 dz3_unknown.smt2
sat

real    0m0.025s
user    0m0.009s
sys     0m0.016s