I'm using Z3 Python interface to create formulas for my experiments. I'm then sending that formula to a Z3 solver. If I'm correct Z3 uses its own solver!
How to use a different SAT/SMT solver with Z3py?
The way I use to do it in CBMC (C bounded model checker): Run the program and spit an intermediate DIMAC representation (in a file) and then use that file as an input to other SAT solvers. Can I do similar things in Z3. Thank you.
Sounds like you should really be using a solver agnostic SMT interface instead of Z3py. There have been several attempts to create such interfaces, with varying degrees of support for multiple solvers:
https://github.com/pysmt/pysmt is a solver agnostic Python API to SMT solvers. I haven't used it myself, but it does sound promising, especially if you want Python as your top-level API.
https://github.com/sosy-lab/java-smt is a similar project that uses Java as the host language.
http://leventerkok.github.io/sbv/ is my own attempt at providing a solver agnostic API for using SMT solvers, this one written in Haskell.
By no means this is an exhaustive list. I'm sure there are others as well, in various host languages, with varying degrees of maturity. Which one you should pick really depends on your host language preference, and the features afforded by each system; which may vary widely.
All SMT solvers support the SMT2 input format, so you can do the same with Z3 and other SMT solvers. Z3py can translate Solver and Goal objects to SMT2-compliant strings (some complicated variable declarations, e.g. some datatypes may be missing).
Z3py is a Z3-specific API (as the name indicates) it does not provide a way to use other SMT solvers.
