Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Z3 on a Mac


view this post on Zulip Email Gateway (Aug 18 2022 at 17:51):

From: Gudmund Grov <ggrov@staffmail.ed.ac.uk>
Hello,

Has anyone used Z3 (with the smt method) on a Mac?

I've set the Z3_NON_COMMERCIAL variable to "yes", but the smt method fails
(with a "Failed to finish proof" message).

Note that the smt method works fine with cvc3 (when I set "declare [[ smt_solver = cvc3 ]]").

Thanks,

Gudmund

view this post on Zulip Email Gateway (Aug 18 2022 at 17:51):

From: Temesghen Kahsai <lememta@gmail.com>
I don't think there is a Z3 version for Mac.

Cheers,

Teme

view this post on Zulip Email Gateway (Aug 18 2022 at 17:51):

From: Sascha Boehme <boehmes@in.tum.de>
Hi,

You can follow this recipe to get Z3 running on a Mac:

http://www4.in.tum.de/~boehmes/z3.html

Please contact me in case of any problems.

Cheers,
Sascha

Gudmund Grov wrote:


Last updated: Nov 21 2024 at 12:39 UTC