Re: [isabelle] Z3 on a Mac



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:
> 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
> -- 
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
> 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.