https://github.com/Z3Prover/z3
It is a Baby Symbloic Executor that keeps track of symbolic states with its path conditions.
- Built on Visitor pattern
- Symbolic Execution on WHILE lang.
Ex) Verbal Arithmetic SMT Solver determines a feasibility and gives a solution for the famous puzzle: Verbal Arithmetic