[Why3-club] encoding of real.From_Int in cvc4 driver
Claude.Marche at inria.fr
Mon Feb 4 11:08:10 CET 2019
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
Opened a ticket: https://gitlab.inria.fr/why3/why3/issues/268
Thanks for the suggestion.
More information about the Why3-club