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@lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/why3-club > _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr https://lists.gforge.inria.fr/mailman/listinfo/why3-club
