Write a Blog >>

We introduce Test Fusion, a simple and effective methodology for validating Satisfiability Modulo Theory (SMT) solvers. Our key idea is to fuse two test formulas into a new equisatisfiable formula. The fused formula combines the structure of its ancestors and is feed to the SMT solver as a test seed. During four months of extensive testing, our test fusion-based tool FusionSMT found 50 bugs in Z3 and CVC4, out of which 40 bugs were fixed by the developers. Most of these bugs address soundness issues, i.e. SMT solvers giving incorrect results. Test fusion is a general methodology that is applicable beyond SMT solver testing.