Erik Helin pointed out to me that the change to the assertion text from "assert(...)" to "vmassert(...)" might break some existing JBS RULE comments for matching known failures. I'll look at how bad this really is, but it seems likely that the thing to do is to revert the message text back to using "assert" rather than "vmassert".