z3 driver should not unfold definitions
currently the Z3 driver, unlike the one for CVC4, eliminates all definitions. The comment in the driver file tends to say that some proofs may be lost if definitions are not eliminated, but this fact should reviewed with newer versions of provers.
On the other hand, not eliminating definition may gain better counterexamples.