z3 solver: z3-SMT on Mac platform

Question

I need to work on Z3 SMT solver for my Master Thesis. I have already check the tutorials for Z3-SMT which is based on SMT-Lib input. But I could only install z3-Py which needs the knowledge of Python. I wanted to know if there is a possibility to install z3 using SMT front end on Mac OSX. If yes, can you please help to do that?

Answer 1

The simplest way to run SMT-LIB scripts is to use the rise4fun interface: http://rise4fun.com/Z3

That said, you may need to run Z3 offline for large problems or in other programs. It sounds like you've already installed Z3 since you have z3py working. If you have succeeded in installing z3py, then you can also run Z3, as z3py depends on Z3 (technically a z3 library, but you probably have both the library and the executable installed if you got the source from codeplex and compiled it). For compilation and installation instructions for all platforms see: https://z3.codeplex.com/SourceControl/latest#README

Once installed, you can execute the z3 executable on an SMT-LIB2 file called test.smt using ./z3 -smt2 test.smt (or just z3 -smt2 test.smt if you put it on the path).