Re: [isabelle] z3 on a mac



Hi,
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.

Take care,
David





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