Parse (_ as-array xx) to better handle Z3 counterexamples (!862) · Merge requests · Why3 / why3

Guillaume Cluzel requested to merge smtv2_model_parser into master Apr 20, 2023

It looks like it has been broken one recently. I hope my solution is correct.

The noise comes from the fact that I had to create (real) unique ident and it changes what is displayed.

Edited Apr 20, 2023 by Guillaume Cluzel

Parse (_ as-array xx) to better handle Z3 counterexamples