Provide a way to print Z3 input for debugging

[wangjwchn]

Hi @gmalecha ,
When I try to modify the coq-smt-check to add some new types, it is hard to debug without seeing the input of Z3. The best I can do is to write it into str_formatter, like this:

Format.fprintf Format.str_formatter "Z3 input\n" ;
RealInstance.write_instance Format.str_formatter inst;
debug (fun _ -> Pp.(str (Format.flush_str_formatter ())));

It can solve my problem to a certain degree, but it 's a temporary solution.
Is there a better way to deal with this?

[gmalecha]

At the moment, I don't think so. We can add another flag that outputs the problem (instead of just the result) to the Coq console.