Evaluation of String Constraint Solvers Using Dynamic Symbolic Execution