would this not pass if I only checked for conditions being scalar during the semantic analysis and never do any checking if something is an integer during the verification phase? The project description states that only integer types are allowed during verification.

Remember you need to

ensure that these restrictions are fulfilled while building the formulas and throw any exception, if that is not the

The test likely expects that you throw an exception, judging from its name. This is the only place where exceptions are expected (if you use them in your type checker, you catch them later on).

If you ensure this, then you should throw an exception (during verification formula construction) if any pointer is ever declared, or if & or * are used. This should then ensure that only integer types are used. Of course, you must also reject if any of the other conditions of page 10 are violated.

During the type check, just check that all conditions are scalar.