Re: [isabelle] z3 on a mac

Thanks for all the help.  The Isabelle community is amazing. The
updates worked with two small tweaks.
  - The script on the webpage uses 'Wine Files/drive_c/Program
Files/Microsoft Research/Z3/bin/z3.exe'.  On my machine z3 installs
with the same path except Z3-2.19 instead of just Z3.
  - I still needed to edit contrib/z3/etc/settings and uncomment
Z3_NON_COMMERCIAL="yes" for it to work. I don't know if it is
intentionally left uncommented in your tar file. It took me some
digging to initially find that option last week; perhaps  an explicit
comment on the website would be helpful to others?

A couple of bizarre things happened when trying to get it to work
today. I note these in case someone else experiences them.
 - When I started up wine today it asked to self-update. I said yes.
/Applications/Wine.appContents/MacOS/startwine went away. Reinstalling
wine from the dpkg fixed. .
 - The [[smt_trace]] option is really cool. I didn't know about that widget.
 - z3 seems to be successfully invoked. The first time I ran it to prove:

lemma reallysimple : "(a \<and> b)= (b \<and> a)"
using [[smt_trace]]
sledgehammer [provers=z3,verbose=true,debug=true]

z3 didn't produce a solution. However, it has reliably since then.
I'm not sure why, but it's worked reliably since then. I'm chalking it
up to first time initialization tasks.

Take care,

On Fri, Jul 1, 2011 at 9:40 AM, Jasmin Blanchette
<jasmin.blanchette at> wrote:
> Hi David,
> Am 30.06.2011 um 16:32 schrieb David Brumley:
>> Anyone run into this? I looked at the z3 documentation, but couldn't
>> find an error 109 on the list.
> I was able to get an error 109 on the Mac as well, even after following Sascha's online instructions. To investigate this, try adding
>    declare [[smt_trace]]
> at the beginning of the .thy file, and send us the trace output.
> SMT: Solver:
>  /Users/blanchet/isabelle/contrib/z3-2.15/x86-darwin/z3: line 11: winepath: command not found
>  fixme:heap:HeapSetInformation 0x0 1 0x0 0
>  Error: input file was not specified.
>  For usage information: z3 /h
> If this is also your problem (and it probably is), either (1) make sure "/Applications/" is in your "PATH" before you launch Proof General or jEdit, or (2) update your "z3" script with the very latest version from Sascha's web page:
> I hope this helps. Please let us know if it doesn't, so we can iron out these issues once and for all.
> Cheers,
> Jasmin

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