Add warnings for explicit choose and old VC gen

[mario-bucev]

No description provided.

[vkuncak]

Another thing that might help users understand trusted proof base would be if we could print a record of the pipeline invoked in a given verification run, indicating in one line concise string whether any of the options that may increase trusted proof base were invoked in a given verification run:

• whether --admit-vcs was used (empty string if not)
• whether termination was turned off
• whether cache was used (empty if not)
• whether antialiasing and imperative elimination were used (empty if not)
• which smt solvers were invoked (including internal ones and princess, if used)
• whether type encoding did anything (empty string if not)
• whether non-library extern functions were used
• whether batch mode was on

[mario-bucev]

I like this idea. I'll check what should be done to integrate this feature, ideally within this PR.

[mario-bucev]

I've pushed what I hope corresponds to the above comment. Here is the concise summary printed for ScalaList (after the verification report):

[  Info  ] Verification pipeline summary:
[  Info  ]   cache, anti-aliasing, type encoding, choose injection, nativez3

With --extended-summary, we have extra information:

[  Info  ] Verification pipeline summary:
[  Info  ]   Cache used
[  Info  ]   Anti-aliasing phase transformed the following functions:
[  Info  ]     length
[  Info  ]   Type-encoding transformed the following:
[  Info  ]     -Functions:
[  Info  ]       ++, ::, head, length, map, tail
[  Info  ]     -Classes:
[  Info  ]       Cons, List, Nil
[  Info  ]   Choose injected in the following functions:
[  Info  ]     -User:
[  Info  ]       ++, ::, head, length, map, tail
[  Info  ]   Solvers used: nativez3
[  Info  ]   Processing mode: partial

The choose injected in functions ++, etc. are for their copies, not the original ones. How could we convey such information? (I'm thinking of something like "++ (derived from original ++)")

[vkuncak]

If the function was copied, that's similar from user point of view as if it was modified, so no need for that.