Satisfiability Modulo Theory (SMT) solvers are foundational tools for
many subareas of computer science, including formal verification,
programming languages, and software engineering. Their reliability and
robustness are crucial, especially for the safety-critical
domains. However, effectively validating SMT solvers has been a
longstanding challenge. The goal of Project Yin-Yang is to develop
novel, effective, practical methods and techniques to help make SMT
solvers more reliable, powerful, and usable.
To this end, we have introduced two novel, highly effective techniques
for stress-testing SMT solvers: semantic fusion 
and type-aware operator mutation . The key idea behind
semantic fusion is to systematically combine two existing
equisatisfiable (i.e., both satisfiable or unsatisfiable) formulas
into a new formula that, by construction, preserves
satisfiability. Type-aware operator mutation is a simple, general,
unusually effective approach for differentially testing SMT solvers by
generating diverse type-correct formulas.
YinYang and OpFuzz, the realizations of semantic fusion and type-aware
operator mutation, have demonstrated their remarkable effectiveness by
having already found 1,000+ bugs in Z3 and CVC4, the two
state-of-the-art SMT solvers.
We have maintained our continuous, extensive effort in stress-testing
Z3 and CVC4 to benefit the SMT solver developer, user, and research