When splitting assertions, delete implicit assertions that would otherwise be converted to assumes

[keyboardDrummer]

Depends on adding a check Cmd to Boogie: boogie-org/boogie#947

I'm pausing this until we further clean up the Boogie encoding, so performance issues with this PR will be easier to debug.

One issue I ran into with BinaryTree.dfy is that calls to .Valid are inlined, leading to huge requires clauses. I think it would be great if there was a way to automatically produce a stack trace for failed assertions in Boogie, by splitting expressions and inlining functions.

One issue with this PR as it is, is that Boogie calls when they are inlined, are turned into regular assertions, not checks. The simplest solution is to add [an option] to Boogie so that the inlined call require clauses do become checks.

Description

When using splits, delete assertions that were generated and would otherwise be converted to assume commands

How has this been tested?

• The performance of ListCopy.dfy improves
• The performance of BinaryTree.dfy gets worse. When trying to debug this, the excessive overhead of the generated Boogie makes it much harder to debug. I see 263 lines of generated Boogie code just for the invocation var t := left.Remove(x);, which should only have left != null && left.Valid() as preconditions.
• The performance of SchorrWaite.dfy gets worse, needs investigation

Data

ListCopy

REMEMBER:
Total resources used is 566196
Max resources used by VC is 54969

FORGET
Total resources used is 517921
Max resources used by VC is 68623

Investigating the expensive 68623 VC, the removed assumptions did not seem useful for the assertion.

BinaryTree

REMEMBER:
Total resources used is 31925465
Max resources used by VC is 847874

FORGET:
Total resources used is 32131313
Max resources used by VC is 1545494

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.