Z3 crash?

Mar 31, 2011 at 12:28 PM
Edited Mar 31, 2011 at 12:29 PM


i'm work with Boogie and when i try the example in Rise4Fun, the Fibonacci, i get the follow result.

Boogie program verifier version, Copyright (c) 2003-2010, Microsoft.

Advisory: F SKIPPED because of internal error: unexpected prover output: z3 crashed and produced no output

Boogie program verifier finished with 0 verified, 0 errors, 1 inconclusive


This for the Boogie binary and source.

Am I doing something wrong?

Mar 31, 2011 at 11:00 PM

Unfortunately, we've got into a state where some of the latest versions of Z3 don't work with Boogie.  This will be fixed with the next release of Z3, which at that time will also require a new version of Boogie.  Until then, use Z3 version 2.15 (and be sure to uninstall all newer versions of Z3 you may currently have, since Boogie tries to use the latest one it finds).

I'm guessing this is the problem.  If you use the /trace flag with Boogie, it will tell you which Z3 it's trying to use.

Apr 4, 2011 at 2:39 PM

thanks, with the Z3 2.15 , the boogie finished without errors.

Oct 31, 2011 at 1:43 PM

Is this issue still an issue? I think version 2.15 is rather old, even the major number changed meanwhile. Do you still need version 2.15?

Oct 31, 2011 at 7:59 PM

No, as of last Friday, Boogie now expects Z3 version 3.2.  To get that version of Boogie today, either synch and build from sources or pick up the latest nightly build (click the Download tab, select Other Downloads -> Planned -> nightly builds).