Re: [isabelle] z3 on a mac
Sorry for the delay; I was traveling.
>> It took me some
>> digging to initially find that option last week; perhaps an explicit
>> comment on the website would be helpful to others?
> Not sure this is the right place. That web page is only for Mac users, whereas the problem you describe is platform-agnostic. Normally (i.e. with Isabelle2011 or better), if you neglect to set "Z3_NON_COMMERCIAL" to "yes", you will get an error when using the "smt" method or Sledgehammer:
> The SMT solver Z3 is not activated. To activate it, set the environment variable Z3_NON_COMMERCIAL to "yes".
> Didn't you get such a message?
I did not get this error message anywhere obvious. I'm an isabelle
noob, so perhaps it was somewhere I wasn't looking? I just got an
error related to Z3 remote, but not an indication what to change.
Thanks again for your help.
This archive was generated by a fusion of
Pipermail (Mailman edition) and