Block Splitting on Context

(suggested by @booleanfunction)

This would be a useful strategy to consider.  Can we split blocks on context such that each (virtual?) block only has a single context going into it.  The idea is that this reduces the work needed for Dafny.