$z3release bug.smt2                             
unsat
(error "line 5 column 10: model is not available")
$z3release proof=true bug.smt2                  
unsat
(error "line 5 column 10: model is not available")
$cvc4 -q --strings-exp --produce-models bug.smt2
sat
(
(define-fun a () String "aarr")
)
$cat bug.smt2                             
(declare-fun a () String)
(assert (str.< a "ar"))
(assert (str.prefixof "ar" (str.replace a "ar" "")))
(check-sat)
(get-model)
$z3release feed_model.smt2                      
sat
(
  (define-fun a () String
    "aarr")
)