Thanks for finding all those bugs! I see the BI / SI / LI invariances you define are looking for program states that aren't present in the unoptimised program, while PI is looking for the absence of information that is in the unoptimised code. Do you think it will be possible to define and search for invariants that involve program states that are in the unoptimised program, but are presented in in the wrong way in the optimised program? For example variable values being presented at the wrong time, or stepping behaviour that misleads developers.
It'd be great to hunt those kinds of bugs, however it's hard to define what the "right" behaviour would be in those circumstances.