A automatic theorem prover for SMT problems.