Re: [isabelle] z3 on a mac



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/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:

    http://www4.in.tum.de/~boehmes/z3/mac/z3

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.