[Why3-club] encoding of real.From_Int in cvc4 driver

Claude Marché Claude.Marche at inria.fr
Mon Feb 4 11:08:10 CET 2019


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



More information about the Why3-club mailing list