[SMT-LIB] SMT solver for Mac OS that accepts smtlib v2 format

[ThanhVu (Vu) Nguyen]

Hi,

I am wondering if there is some SMT solver for Mac OS (Snow Leopard +
Macport) that supports Linear arithmetic  and also accept smtlib2 as input
format.   So far I've tried cvc3 but I don't believe it supports smtlib2 and
I can't get cvc4 (nightly release) to build properly on Mac.     I have also
tried smtlib2parser which uses Yices 1 backend but it doesn't support the
(model) command.

Right now I am using Z3 which does all I want except doesn't run on Mac
natively.   I was able to run it via Wine but it is extremely slow that way.


Another question is if it is possible to get several models instead of just
1 if the formula is satisfied.   I could always get the model 1,  then put
back the negated result as assertion to get a different model 2 (if it
exists) and so on  -  just want to know if there's some better way.


Thanks,



Vu,