Currently the verifier performs two passes: one for establishing invariants, and one for checking that these invariants imply the assertions. Both passes iterate complete basic blocks (though the verification pass ignore loops).

If basic block can be arranged such that each hold (a) code to execute and (b) a set of assertions denoting the precondition for the code to execute safely, then the second pass need not look at the code at all, and the first pass need not look at the assertions at all (though assertions are also assumptions, so it could sometimes be faster to look at them).

This would require either avoiding simplification before assertions, or some sort of preprocessing that will collect the assertions backwards to the beginning of each block. This is a kind of abstract interpretation in which the abstract domain is a set of assertions, but for our purposes we won't need any sophisticated join, meet or widening - merely collecting the assertions would be enough for significant improvement.

From a class design point of view, this would allow splitting the domain to operations on code and operations on assertions.