Don't know how to verify Grover's search!

[alan23273850]

My command is why3 prove -P alt-ergo $(DIRS) grover.mlw, where the version of alt-ergo has been 2.0 and 2.2.

In these versions, the result is always Timeout (5.00s).

Is there an official demo of verifying Grover's search, or how to reset the timeout of why3? Thanks!

[Qbricks]

Dear Alan,

Thank you for your interest

• can you try to launch "why3 ide" from the public_readme branch? It should load the grover.why3session.xml file, with a proof demo...?
• Also, in Why3 Ide, you can define the timeouts for the provers in "File -> Preferences -> Time limit".

[alan23273850]

Thanks for your response! The grover.why3session.xml file says that the experiment should be totally successful; however, my result (Split VC strategy) shows that some preconditions still timeout at 5 seconds. Is there any way to configure the ide to make the experiment pass? Or Is there any way to reproduce the grover.why3session.xml? Thank you again!

[Qbricks]

Hi,

I am not sure that your session actually loads the proof file, in the ide can you see at some point some proof trees, similar as in the attached image?

Also, from the demo Alt-Ergo should manage maybe 80->90% of proof obligations, but some are filled through additive SMT solvers (CVC3/CVC/Z3) : I guess when the session loading problem is filled then if you want to fully complete the proofs you may need these solvers also.