Hi,
For this String formula:

(declare-fun a () String)
(assert (not (= "" ( str.substr a 0 1))))
(assert (= "" ( str.substr a 1 1)))
(check-sat)

Z3 incorrectly reports unsat, while the latest release Z3-4.8.5 can give sat result with model:

(model
  (define-fun a () String
    "\x00")
)

After feeding this model to the formula, z3 can report sat.

OS: Ubuntu 18.04
Revision: aff4b30