[Why3-club] Several remarks and questions on Why3

Mohamed Iguernlala 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.

- Mohamed.

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
> http://lists.gforge.inria.fr/mailman/listinfo/why3-club

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20160818/b21c748d/attachment.html>

More information about the Why3-club mailing list