Soundness bug in QF_S with smt.arith.solver=2

[wintered]

Seems neither related to (#4062 in which z3release gives sat with smt.arith.solver=2) nor to #4065 where z3 without options gives an incorrect answer.

$z3release smt.arith.solver=2 model_validate=true bug.smt2
sat
(error "line 3 column 10: an invalid model was generated")
$z3release model_validate=true bug.smt2                   
unsat
$cvc4 -q bug.smt2                                     
unsat
$cat bug.smt2
(declare-fun a () String) 
(assert (str.prefixof "B" (str.replace "A" a "" ))) 
(check-sat)

OS: Ubuntu 18.04
Commit: 8fe3caa

[NikolajBjorner]

fixed