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

Claire Dross dross at adacore.com
Mon Feb 4 12:16:54 CET 2019


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 curious about the results of this experiment.

-- 
Claire



More information about the Why3-club mailing list