Hi,
For this case, Z3 gives an incorrect answer:
[517] % z3 model_validate=true small.smt2
sat
(error "line 4 column 10: an invalid model was generated")
[518] %
[518] % cvc4 --strings-exp -q small.smt2
unsat
[519] %
[519] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(assert (distinct (str.contains (str.replace "B" a b) b) (str.prefixof a (str.replace "B" b a))))
(check-sat)
[520] %
OS: Ubuntu 18.04
Commit: bcbe802
Hi,
For this case, Z3 gives an incorrect answer:
OS: Ubuntu 18.04
Commit: bcbe802