[isabelle] z3 on a mac
I saw the discussion the other day about z3 on a mac. Coincidentally I
was setting up z3 on my mac too (10.6.8 on a 2008 mac pro)
I followed the recipe for z3 under wine. z3 seems to run fine from
the command line. I added the following to etc/settings (is there a
if [ -e "$Z3_HOME" ]
And put the z3 shell script from
http://www4.in.tum.de/~boehmes/z3.html under contrib/x86-darwin/z3.
z3 runs fine from the command line (at least z3 /h seems to work).
However, when I run it from isabelle I get
SMT outcome: Solver terminated abnormally with error code 109
The simplest example I've tried is:
lemma really_simple : "(a \and b) = (b \and a)"
Complex lemmas have the same error.
Anyone run into this? I looked at the z3 documentation, but couldn't
find an error 109 on the list.
This archive was generated by a fusion of
Pipermail (Mailman edition) and