`get-interpolants`'s output doesn't respect the smtlib standard proposal.

[btwael]

The description of get-interpolants command is given in this proposal. While opensmt respects most of it, it violates how result (interpolants) must be shown.

In the standard proposal, if get-interpolants must produce two interpolants I1 and I2 (I1 and I2 are formulas), they are printed as follow:

(I1
 I2)

opensmt prints instead the following:

I1
I2

[blishko]

Hi @btwael , thanks for reporting this! We based our get-interpolants command on that proposal, but we did not cover all its aspects.

Makes sense to improve our compliance to the proposal.

[aehyvari]

Hi @btwael, thanks again for pointing this out. Hopefully now that #215 is merged, the issue is fixed.

[btwael]

Hi @blishko, hi @aehyvari, Thank you for your fast reply and solution.

In deed, your commit solves the problem when outputing a sequence of interpolants as I showed in the example above. However for binary interpolation, the output is still not respecting the proposal.

For binary interpolation, the solver is supposed to output one interpolant I1 as follow:

(I1)

opensmt is printing

I1

To be more concrete, in one given exemple, opensmt outputs:

(not (<= 0 (+ (* -1 x) y)))

while we expected:

((not (<= 0 (+ (* -1 x) y))))

Thank you very much.

[aehyvari]

@btwael hopefully it now works as the standard dictates. Let me know if there are other problems!

[btwael]

Perfect, thank you very much, this works as supposed.

[blishko]

Seems resolved to everyone's satisfaction.