Uses clauses are not printed to file

[Dargones]

Since #561 has been reverted, uses clauses are no longer printed to a file. Among other things, this means that it is not always possible to manually reproduce the verification result reported by Boogie as a library.

Here is a concrete example of the problem in the context of Boogie being used as a dependency by Dafny. This Dafny program verifies because Dafny uses pruning but tells Boogie not to prune the axiom that defines function f:

function f():int { 0 }

method m(i:int) requires i != f() {
    assert i != 0;
}

However, if one were to ask Boogie to print the file generated from the Dafny program above, the result would be this (simplified):

function f():int;
axiom f() == 0;

procedure m(i:int) 
  requires i != f(); {assert i != 0;}

If I use /prune on this .bpl file, Boogie fails to verify it (I also supply the arguments recommended here).

[keyboardDrummer]

This (unfinished) PR might help towards resolving this issue: #600, as an alternative to #561

[shazqadeer]

I believe this issue has been fixed by PR #765 and #767 .