Hello Claude,
thanks a lot for your quick response.
After sending the e-mail, I started to implement the workaround with
records and, indeed, contrary to what I wrote, "model_projections"
labels are useless in that case.
I can now post-process the why3 output to print the counter-example
model
Hello Denis,
As far as I know, the decomposition of the quantifications over tuples
is done quite early in the Why3 processing ("eval_match" in the WP calculus)
Using a record structure is probably a good workaround, and I don't
think you need to bother with any "model_projection" labels for
Dear list,
I'm stucked with an apparently simple problem of counter-examples printing and
I'd appreciate a lot if someone had a clue to help me.
I have a Why3 formalization that deals with Bool tuples. And I'd like to print
those tuples values when a counter-example is found.
Here's an example:
