Re: [isabelle] sledgehammer in RC4

Am 11.11.2013 um 12:06 schrieb Makarius <makarius at>:

> On Sat, 9 Nov 2013, Randy Pollack wrote:
>> BTW, I fixed  Z3_NON_COMMERCIAL= yes, and did not get the ususal
>> Isabelle warning saying to do that.
>> What have I forgotten?
> I don't understand the "fixed Z3_NON_COMMERCIAL" part.  What was broken here?

No. The message did not show up because only two provers were run (E and SPASS). That's perfectly normal. The message is shown only if users attempt to run Z3.


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