Re: [isabelle] z3 on a mac

Hi David,

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:
> 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_SOLVER="$Z3_HOME/z3"
> if [ -e "$Z3_HOME" ]
> then
>   Z3_INSTALLED="yes"
> fi
> And put the z3 shell script from
> 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.