Hi,
For this formula:
(declare-fun a () String)
(declare-fun b () Int)
(assert (distinct (str.replace "A" (int.to.str b) a)
(str.replace "" (int.to.str b) a)))
(assert (= (str.replace a (str.at a b) "") a))
(check-sat)
(get-model)
Z3 smt.string_solver=z3str3 gives an invalid model:
(model
(define-fun b () Int
1)
(define-fun a () String
"\x00\x00\x00")
)
if I feed this model to the formula, Z3 reports unsat.
OS: Ubuntu 18.04
Commit: 1aea0d2
Hi,
For this formula:
Z3 smt.string_solver=z3str3 gives an invalid model:
if I feed this model to the formula, Z3 reports unsat.
OS: Ubuntu 18.04
Commit: 1aea0d2