search

gmalecha / coq-smt-check

Invoke SMT solvers from Coq to check obligations
MIT License
10 stars 3 forks source link

Provide a way to print Z3 input for debugging #3

Open wangjwchn opened 7 years ago

wangjwchn commented 7 years ago

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 commented 7 years ago

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.