Does it mean that selecting the option "get counter example" is not supposed to
change CVC4 proof search strategy?
> On 5 Mar 2018, at 16:24, Guillaume Melquiond <guillaume.melqui...@inria.fr>
> 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,
> Why3-club mailing list
Why3-club mailing list