Re: [isabelle] z3 on a mac



Hi David,

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

Indeed -- I can reproduce this. Isabelle2011 was released at a point where the Sledgehammer/SMT business was a bit flaky, unfortunately. More precisely, some changes were done to the integration of off-the-shelf solvers in January, and Sledgehammer was not tested against these. With the repository version of Isabelle (or the next release), you would get the aforementioned message.

Regards,

Jasmin






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