[isabelle] z3 on a mac



Hi,
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
better place?):

Z3_COMPONENT="$COMPONENT"
Z3_HOME="$Z3_COMPONENT/$ISABELLE_PLATFORM"

Z3_NON_COMMERCIAL="yes"

Z3_SOLVER="$Z3_HOME/z3"
Z3_REMOTE_SOLVER="z3"

if [ -e "$Z3_HOME" ]
then
  Z3_INSTALLED="yes"
fi

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)"
sledgehammer [provers=z3,verbose=true,debug=true]

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.

Thanks,
David





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