Model interpolants should be displayed in the SMT syntax

[BrunoDutertre]

Running yices-smt2 --incremental on tests/regress/mcsat/nra/assumptions/quadratic.smt2 will produce this output:

  unsat
  (or (>= (* -1 a) 0) (>= (+ (* -4 a c) (^ b 2)) 0)).
  unsat
  (or (>= (+ (* -4 a c) (^ b 2)) 0) (>= a 0))
  unsat
  (or (>= (* -1 c) 0) (/= b 0) (/= a 0))

That's correct, but the interpolant are printed using the Yices syntax. When processing SMT-LIB input, we should product SMT-LIB output.

[disteph]

True, but do we have an SMT2 pretty-printer for terms? I thought that was always missing? (That's why I made my own SMT2 pretty-printer in the OCaml bindings, with some mechanisms to recover the bvor, bvshifts, etc that were bitwise simplified; of course it'd be better inside Yices, but it's not a one-line fix...)

[BrunoDutertre]

This is all true. Converting yices internal terms to the SMT-LIB syntax is not trivial and we don't have that yet. I just wanted to record an issue so that we remember this as something to address in the future.