[Why3-club] Several remarks and questions on Why3

David Hauzar david.hauzar at inria.fr
Thu Aug 18 16:21:56 CEST 2016


Hello David,

On 18.08.2016 10:04, David MENTRE wrote:
>  1. In function k in attached WhyML file, there are two "returns"
> clause. Two counter examples are generated (for line 26) but for the
> second one the counter example is on "s.x" variable while I expected it
> on "s.y". Indeed, in function k2 when I add a "model_vc" annotation,
> then the right counter example is generated on s.y. Would it be a bug?

Yes, this is a bug. Thank you for reporting it.

Note that the transformation split_goal_wp creates two identical tasks 
(up to labels storing the information whether a task speaks about "s.x" 
or "s.y") for the first and the second "returns". This bug demonstrate 
itself only if these two tasks are proved all at once. Applying this 
transformation on the VC in why3ide and proving the two tasks one by one 
works as expected. Also, when the two tasks are different (for example 
if the second returns is "returns { r -> r.y > 1 }"), it works as expected.

>  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. See the discussion in our paper 
Counterexamples from Proof Failures in SPARK:

"As expected, in this case the model is not guaranteed to be a true 
model. However, there are some cases where the model returned is 
trivially wrong because it is not even a model of the ground part of the 
goal. A suggestion for improvement is as follows: since the main source 
of incompleteness comes from the quantified hypotheses, there could be 
two different modes of operation, with two corresponding time limits. A 
first time limit, say a “soft” one, gives the time during which the 
solver is allowed to instantiate quantifiers as it wants. After this 
soft time limit is reached, a “hard” time limit should give the solver 
extra time to continue its search but in a specific mode where no new 
quantifier instantiation is performed. In this second mode, it is likely 
that the solver would terminate its search, and if a model is returned, 
it would be valid with respect to the ground part of the goal. If such 
modes were implemented in SMT solvers, it would be of major interest for 
counterexample generation."

Note that currently this information what is the reason that the prover 
answers unknown is got by Why3 but not outputted by why3 prove command.

David


More information about the Why3-club mailing list