Proof Errors

Specware will report an error if the claim to be proved does not occur in the spec, or if not all claims following using occur in the spec before the claim to be proved.

Snark will likely break into Lisp if the user inputs an incorrect option.