[Why3-club] Several remarks and questions on Why3

David Hauzar david.hauzar at inria.fr
Thu Aug 18 17:59:07 CEST 2016


On 18.08.2016 17:20, David MENTRE wrote:
> Hello David,
>
> Le 18/08/2016 à 16:21, David Hauzar a écrit :
>>>  2. In my test file, counter example are correctly generated. However,
>>> in my real life example, no counter example is generated. It appears
>>> that in this latter case Z3 is killed by why3-cpulimit while in the
>>> former test case Z3 returns an output by itself before the time limit.
>>>
>>> Do you know a way to generate a counter-example when time limit is
>>> reached? By playing with Z3 options (e.g. using option -T)? Would it be
>>> the same with CVC4? How do you handle the case in SPARK?
>>
>> For both Z3 and CVC4, we are using resource limit (rlimit). However, the
>> counterexamples are not good when resource limit is reached. We thus
>> detect this (the prover answers "(:reason-unknown resourceout)" and do
>> not show counterexample in this case.
>
> So, if I understand you correctly, I should not try to get or use
> counter example when such a time-out or other limit is reached.

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

David




More information about the Why3-club mailing list