Re: [isabelle] z3 on a mac



Hi David,

I just updated the description of how to run Z3 on a Mac:

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

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.

Cheers,
Sascha


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_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.