[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 at lri.fr
Wed Jul 11 18:15:05 CEST 2018
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,
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.
> Ziqing Luo
> University of Delaware
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
More information about the Why3-club