$ z3release small.smt2
unsat
$ cvc4 --check-models --produce-models --incremental --strings-exp -q small.smt2 
Fatal failure within void CVC4::smt::CheckModels::checkModel(CVC4::smt::Model*, CVC4::context::CDList<CVC4::NodeTemplate<true> >*, bool) 
at CVC4/src/smt/check_models.cpp:131
Internal error detectedSmtEngine::checkModel(): ERRORS SATISFYING ASSERTIONS WITH MODEL:
assertion:     (not (str.in_re a (re.* (re.comp (str.to_re "")))))
simplifies to: false
expected `true'.
Run with `--check-models -v' for additional diagnostics.
Aborted
$ cat small.smt2
(declare-fun a () String)
(assert (str.in_re a (re.* (re.union (str.to_re "a") (str.to_re (str.replace_re_all "c" (re.* (re.range "a" "u")) a))))))
(assert (not (str.in_re a (re.* (re.comp (str.to_re ""))))))
(check-sat)