[enhancement] solvers::z3::ScopedVerifyEquivalent (and Proc and check_ir_equivalence_main) should check assert equivalence

[allight]

What's hard to do? (limit 100 words)

If you have passes or transforms which add asserts changes done by opt should not change the circumstances that asserts trigger on. Currently none of these can be verified since our z3 translator does not support asserts.

This would have let us catch 3288 earlier for example. Edit: Nope that seems to be a different error. In any event this would still generally be useful.

Current best alternative workaround (limit 100 words)

Manual/none

Your view of the "best case XLS enhancement" (limit 100 words)

ScopedVerifyEquivalent (and maybe the devtools check_ir_equivalence_main) should do pre-transforms on their inputs to match up asserts with the same label on both sides and ensure they remain identical. Asserts with no corresponding assert on the other side should be checked they can never trigger.