Use of Boogie /prune flag in Dafny

[shazqadeer]

This issue is about another question regarding how Dafny uses Boogie. If an issue is not the right venue for such queries, let me know here and I will adjust in future.

A flag /prune was added not too long ago to Boogie for use in Dafny. At least, this is what I remember. Is this flag used regularly in Dafny? What is your experience with it?

My experience with the flag is mixed. I have been working on monomorphization of Boogie programs. When a polymorphic axiom (i.e., an axiom with a polymorphic universal quantifier at the top-level) is monomorphized, my code generates a collection of monomorphic axioms. I have been trying my code on Boogie programs generated from Dafny samples such as Composite, FlyingRobots, SchorrWaite, etc. which were supplied to me by Gaurav Parthasarathy. I naturally experimented with supplying the -prune flag to the monomorphized Boogie program expecting that irrelevant instances of an axiom will be pruned and I will get speedups. I notice that while I do get speed ups on several examples, most notably FlyingRobots, I also get error messages on other examples which indicates that too much pruning is being done.

One more question: I noticed that now there is syntax in Boogie for attaching axioms to constant declarations. This was news to me! Was this extension also done at the time of the /prune implementation?

[keyboardDrummer]

Is this flag used regularly in Dafny? What is your experience with it?

It's always used. We have some SMT inputs that went from 100K lines of input to 10K, and some Dafny users that saw orders of magnitude speedups in some of their verification runs.

Was this extension also done at the time of the /prune implementation?

It was

Discussion relevant to your other comments is here: boogie-org/boogie#560