print-success: get-value response is not standards compliant

[LeventErkok]

For this input:

(set-option :print-success true)
(set-option :produce-models true)
(set-logic QF_BV)
(declare-fun x () (_ BitVec 8))
(check-sat)
(get-value (x))

Boolector 3.0.0 (freshly built out of github sources) prints:

success
success
success
success
sat
success
((x #b00000000))

This is not standards compliant, since the printing of success in response to get-value should not be there. (That is, after the sat response, we shouldn't see a success, but directly the printing of the valuation pair.) If you try it with other solvers (z3, yices, cvc4), you can see that success isn't printed after we see sat.

This might sound like nit-picking, but unfortunately, it breaks compatibility with tools that operate on top of SMT-solvers; and is a real issue for me. Would be great if it can be fixed!

[mpreiner]

Levent,

Thanks for pointing this out. This is now fixed on master.