get-unsat-assumptions returns declarations instead of names

[daniel-larraz]

Consider this SMTLIB script:

(set-option :produce-unsat-assumptions true)

(set-logic QF_BV)

(declare-fun v1 () (_ BitVec 8))
(declare-fun a1 () Bool)
(declare-fun a2 () Bool)

(assert
 (=> a1 (= v1 #b00000000)))

(assert
 (=> a2 (= v1 #b00000001)))

(check-sat-assuming (a1 a2))

(get-unsat-assumptions)

boolector outputs:

unsat
((declare-fun a1 () (_ BitVec 1))
(declare-fun a2 () (_ BitVec 1))
)

Z3, CVC4, and Yices2 outputs:

unsat
(a1 a2)

Would it be possible to change boolector output format to the more standard one?

Notice also that the declarations use (_ BitVec 1) instead of Bool. This is not an issue if the standard format is used.

Thanks!