Re: [isabelle] z3 on a mac
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
at the beginning of the .thy file, and send us the trace output.
/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/Wine.app/Contents/Resources/bin" 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and