stop displaying counterexamples sorted by lines in the source
The counterexamples are currently displayed by why3 in a manner that is somehow "sorted" by lines in the source. This display is anyway, generally, too much detailed by default.
The default way to display a counterexample should be to only display the values given as input to the function under proof. These values are exactly the ones that are collected as initial values for running the small-step RAC.
As options, and only when these options are set by the user, Why3 could display:
- the values of the variables at the location of the VC
- the values of the variables at the position of function calls and loops (the one that are collected for the giant-step RAC)
- the full set of values, as it is for now. But the values coming from other modules (in particular the standard library) could be filtered out