Thank you for your message. I will check it out. I have to test it
further, but I think that I have the same problem with all provers, not
only alt-ergo. I tried alt-ergo manually, but Z3, CVC4 are also used on
the same goal, and they fail.
Viorel Preoteasa
On 10/31/2019 12:41 PM, Johannes Kanig wrote:
Viorel Preoteasa writes:
Then all results are proved under 0.04s. Is there a succinct way to add all
lemmas for integer constants as assumptions?
FWIW, we (the SPARK team) wrote a transformation that inserts such
axioms in the proof task for all real constants in the transformation.
We did that specifically for alt-ergo. But we removed it because other
provers were better at the time even without these extra axioms, and we
had some other trouble because of this transformation.
If you are interested, you can find the code as follows:
- Checkout this repo:
https://github.com/AdaCore/why3
- see the contents of the old transformation:
git show 9bed9dea98f532afdf6eebfb3545ab7c58493daa:src/transform/gnat_float.ml
But note that the code is from 2015, so it probably won't compile with
today's Why3 and requires some modification.
--
Johannes Kanig, PhD
Senior Software Engineer
<ka...@adacore.com>
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
