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

Jean-Christophe Filliatre Jean-Christophe.Filliatre at lri.fr
Wed Jul 11 18:15:05 CEST 2018


Hi,

I see two possible explanations (at least):

- the shortcut "z3" in your why3.conf file does refer to a particular Z3
binary (e.g. z3-4.4.1 in your PATH) while "z3" in your shell does refer
to a different version;

- the command for "z3" in your why3.conf does include a fixed
random_seed (42 most likely), while a mere "z3" command in your shell
typically runs Z3 with a randomized seed.

Hope this helps,
--
Jean-Christophe


On 11/07/2018 17:17, Ziqing Luo wrote:
> 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.
> 
> Thanks,
> Ziqing Luo
> University of Delaware
> 
> 
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
> 


More information about the Why3-club mailing list