Should /noVerify skip the Boogie translation phase?

[cpitclaudel]

@fabiomadge pointed this out recently: /noVerify still performs the translation to Boogie. Same for {:verify false}, I believe.

It looks like this is because /noVerify is a Boogie flag. Could we check it at the Dafny level and skip all the work of translating to Boogie?

[parno]

If you skip the translation normally when given /noVerify, it'd be nice if providing /noVerify /print:filename.bpl still worked. If I'm trying to, for example, understand a problem in the Boogie translation, it would be tedious to wait for verification each time.

[cpitclaudel]

Agreed, maybe we need a different flag.

[MikaelMayer]

I think we might not need a different flag. We can just accommodate this use case, in which if we detect /print: we automatically do the translation as needed.