Hi Claire,
Le 31/01/2019 à 14:56, Claire Dross a écrit :
Hi Why3 team,
while working on the port of SPARK to the current master of why3, I
noticed that we have a difference between our current driver for smtlib
and the driver from why3 master. In gnatwhy3, we have some mappings, in
particular from real.From_Int to to_real. I don't see such a mapping for
CVC4 in the master of Why3. Is there a reason for that?
We didn't try such kind of mappings. I can't answer on whether they
would be useful, except by trying them and evaluate the results on our
benchmarks.
Opened a ticket: https://gitlab.inria.fr/why3/why3/issues/268
Thanks for the suggestion.
- Claude
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
