z3str3 invalid model on QF_SLIA formula

[muchang]

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

[mtrberzi]

This case times out as of the latest commit. Do you know the expected response from the solver?

[zhendongsu]

Both Z3 and CVC4 report sat. Below is the model from Z3:

(model 
  (define-fun b () Int
    (- 2))
  (define-fun a () String
    "\x00\x00\x00")
)