Turning buggy software A into buggy software B, with all bells and whistles (and bugs included). This is useful for doing large-scale restructuring of codebases. You can verify you aren’t adding (or removing) bugs.
Actually, bugs might surface during such restructuring. If the statement you're proving can be greatly simplified to something reasonable, if we omit this one weird special case, that indicates a bug in the specification.
Great advice! Thanks!
Especially when "this one weird special case" pulls in the entire binary layout because your code has a hole that allows an attacker to jump to a specified address