In process mining, grammatical inference is used to extract information from large amounts of data. One problem in grammatical inference is exact DFA identification: finding a smallest DFA that accepts and rejects given words. Empirical experiments are used to compare new algorithms with the state of the art for exact DFA identification. To investigate to what extend the research field of formal verification is affected by the replication crisis, we replicate the existing experiments to see if their results are valid. We also run new experiments for exact DFA identification to test if the assumptions in existing papers are valid and to test if the performance of SAT and SMT solvers with new combinations of existing algorithms and symmetry breaking predicates can be improved. This thesis provides a program with all the state-of-the-art algorithms and symmetry breaking predicates of exact DFA identification, with which our experiments are easy to reproduce. With these experiments, we show that the replication crisis also affects the field of formal verification and replicating experiments can be made more attractive by also investigating new research questions with the replicated code.