Re: [isabelle] z3 on a mac
I just updated the description of how to run Z3 on a Mac:
Especially, I added a section about how to run Z3 with Isabelle.
Please replace your setup (modification of etc/settings) with what is
described in section 4 of that webpage.
David Brumley wrote:
> 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?):
> 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)"
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and