Add some tests checking that the verifier rejects cases where a definition