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
From: Temesghen Kahsai <lememta@gmail.com>
I don't think there is a Z3 version for Mac.
Cheers,
Teme
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