Hi,
For this case, Z3 gives an incorrect answer:
[584] % z3 small.smt2
unknown
unknown
[585] % z3 smt.string_solver=z3str3 small.smt2
unsat
sat
[586] %
[586] % cat small.smt2
(assert (= (str.replace_all "" "" "") ""))
(check-sat-using horn)
(check-sat)
[587] %
OS: Ubuntu 18.04
Commit: f2d3160
Hi,
For this case, Z3 gives an incorrect answer:
OS: Ubuntu 18.04
Commit: f2d3160