I'll remember to try to compile this with warnings enabled next time :-)
This is currently *very* experimental and needs to be more fully integrated with the main verification code.