[Why3-club] Several remarks and questions on Why3

David MENTRE dmentre at linux-france.org
Thu Aug 18 17:20:16 CEST 2016


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.

Thanks!
david



More information about the Why3-club mailing list