[Why3-club] Several remarks and questions on Why3
iguer.pro at gmail.com
Thu Aug 18 19:36:02 CEST 2016
I just tested the idea of having two timeouts in Alt-Ergo (one for proof
search and another for model search).
It's actually very easy to implement. I get something that seems to work
with about ten lines of code.
But for the moment, Alt-Ergo's output for models is not parsable by
Why3. We'll fix this in the future. In the
meantime, one can use --debug call_prover or click on "Prover Output"
tab of Why3 ide to see computed model.
Le 18/08/2016 à 18:08, Yannick Moy a écrit :
> -- David Hauzar (2016-08-18)
>> Yes. We asked CVC4 developers for the support of counterexample
>> generation when a time-out limit is reached. But it wouldn't be easy
>> to implement and in addition it seems not a priority for them. So
>> maybe it would help if you would ask also when you will have an
>> opportunity :)
> Last time we discussed these notions of soft time limit and hard time
> limit with CVC4 developers, Martin Brain suggested that instead we
> generate a version of the VC without axioms, so that only ground terms
> are present and a counterexample can be easily generated. The problem
> then is that it may likely be a spurious one. I believe the notions of
> soft/hard time limits that we proposed in our article is better, as
> it's easy for the prover to check that current ground terms do not
> contradict the counterexample. But this has not made it so far into CVC4.
> Yannick Moy, Senior Software Engineer, AdaCore
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Why3-club