Z3 theorem prover: new formula

Closes #289.