[Why3-club] Several remarks and questions on Why3

Yannick Moy moy at adacore.com
Thu Aug 18 18:08:36 CEST 2016

-- 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

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

More information about the Why3-club mailing list