in the test suite, assert_one_fails / assert_fails will accept ill-typed code

[tjhance]

The assert_one_fails and assert_fails are almost always used to test for SMT failures. However, they will allow the test to pass if there's a 'mismatched type' error on the line marked 'FAILS'. This makes it easy to accidentally write a broken test case that doesn't test the intended thing.