Probabilistic symbolic execution is a static analysis technique aiming at quantifying the probability of a target event occurring during a program execution; it exploits symbolic execution to identify the conditions on the program inputs leading to the occurrence of the target event and then model counting to quantify their probability. While efficient methods exist for model counting of numeric constraints, only limited results have been obtained for counting string constraints. The constraints are indeed first encoded in a corresponding accepting automaton; then the number of accepting paths of the automaton is quantified via a convenient generating function. The encoding in the form of automata limits the expressiveness of the formalism used for constraint specification to constructs mappable into automata, for an exact model count. Furthermore, the encoding of disjunctions requires the parallel composition of the automata representing the disjuncts, leading to an exponential growth in the size of the resulting automata. This thesis introduces the usage of SMT solvers to count the models of a string constraint by leveraging a standard smtlib interface. Several algorithms for both exact and approximate model counting of string constraints are defined and compared. The different solutions are implemented on top of the SMT solver CVC4 and evaluated on a set of established benchmarks, demonstrating the increased expressiveness with respect to previous approaches and improved performance on several classes of problems.