Open DavePearce opened 2 months ago
(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.
(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.