Counterexamples support in new IDE
Several issues in one:
-
when selecting a proof attempt node, display the task of the parent in the task text window followed by the result of that prover, including a CEX if any. format: json if simpler, but ultimately a human-readable format
-
do not require "model" annotation for computing cex. possible solution: modify the parser so that every ident that comes from user input is given the "model" label and also "model_trace:id". (also we may need to add "model_vc" on post-conditions and such)
-
when selecting a proof attempt node, display the CEX, if any, interleaved with the source code
optional) signal the presence of a CEX in the status column of the proof tree (display the CEX in a tooltip when mouse moved on the correspond icon)