Suitability of Finite State Automata to Model String Constraints in Probablistic Symbolic Execution