z3str3 invalid model on QF_S formula with distinct str.replace

[muchang]

Hi, For this formula:

(declare-fun x () String)
(declare-fun y () String)
(assert (distinct (str.replace (str.replace x y x) x y) x))
(check-sat)
(get-model)

Z3 smt.string_solver=z3str3 gives an invalid model:

(model 
  (define-fun y () String
    "")
  (define-fun x () String
    "\x00")
)

if I feed this model to the formula, Z3 reports unsat.

OS: Ubuntu 18.04 Commit: c71da17

[mtrberzi]

This now times out as of the latest patch. Do you know what the correct answer to this case is? If it is UNSAT, a timeout here may be expected.

[zhendongsu]

It should be satisfiable. Below is the model from z3:

(model 
  (define-fun y () String
    "\x00\x00")
  (define-fun x () String
    "\x00")
)