Hi Claude,
Le 04/02/2019 à 11:08, Claude Marché a écrit :
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, I am curio
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
particu
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