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

2019-02-04 Thread Claire Dross
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

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

2019-02-04 Thread Claude Marché
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