Does it mean that selecting the option "get counter example" is not supposed to 
change CVC4 proof search strategy?

Thanks,
Delphine


> On 5 Mar 2018, at 16:24, Guillaume Melquiond <guillaume.melqui...@inria.fr> 
> wrote:
> 
> Le 05/03/2018 à 11:43, Sandrine Blazy a écrit :
> 
>> None of my provers (Alt-Ergo, cvc3, cvc4, Eprover, Z3) is able to prove any 
>> of these 3 assertions. However, if I choose the "get counter-example" option 
>> in the preference window, then cvc4 manages to prove this test program.
>> Does it mean that I should always choose this "get counter-example" option, 
>> even if I am not using this feature ?
> 
> Launching a bisection, as Mohamed did, is quite informative in that case. If 
> only one prover is able to prove a goal, and if it is still the only one 
> after a bisection, then it might be a bug in the prover (or in Why3).
> 
> As to what a bisection is, it is a mechanism to remove all the useless 
> declarations from the context. Starting from an _already_ proved goal, Why3 
> repeatedly removes declaration as long as the goal stays proved, until it 
> reaches a (local) minimum. That way, if other provers were initially confused 
> by too large a context, they now have a second chance at proving the goal. If 
> they still fail, then either the original prover is much more powerful than 
> them, or there is something terribly wrong going on.
> 
> So, to answer the original question, no.
> 
> Best regards,
> 
> Guillaume.
> _______________________________________________
> Why3-club mailing list
> Why3-club@lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club

_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club

Reply via email to