title: Z3 and DIMACS output
body: <p>Z3 currently supports the DIMACS format for input. Is there any way to output the DIMACS format for the problem before solution? I mean converting the problem to a system CNFs and output it in a DIMACS format.
  If not, any ideas towards this direction would be more than helpful.</p>