Z3 is a state-of-the art theorem prover from microsoft research. see the z3 package for a detailed description.

this package provides the jni library to invoke z3 via its java api.