[Why3-club] A why-logic script that why3 cannot prove within 20 seconds but its generated z3 script can be proved quickly

Ziqing Luo ziqing at udel.edu
Wed Jul 11 17:17:34 CEST 2018

Hi Why3 Developers,

I'm confused by my recent experience with why3 :

I had a query written in why-logic "query.why".  I ran why3 on it with
command "why3 prove -P z3 -t 20 query.why" and got "Timeout (20 seconds)".

Then I tried command "why3 prove -P z3 query.why -o ." to let why3 generate
a z3 script for this query.  The generated z3 script can be proved by z3
within 1 seconds.

So I don't understand why why3 cannot prove it within 20 seconds ?

I'm attaching the .why file.

Ziqing Luo
University of Delaware
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20180711/68484ce0/attachment.html>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: query.why
Type: application/octet-stream
Size: 5100 bytes
Desc: not available
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20180711/68484ce0/attachment.obj>

More information about the Why3-club mailing list