ClassCastException on UF formula (get-proof)

[rainoftime]

Hi, for the following formula,

(set-option :produce-proofs true)
(set-logic UF)
(declare-const v2 Bool)
(assert (! (forall ((q0 Bool) (q1 Bool) (q2 Bool)) v2) :named IP_1))
(assert (! (not (forall ((q3 Bool) (q4 Bool) (q5 Bool) (q6 Bool)) (not (not q4)))) :named IP_3))
(check-sat-assuming (IP_1 IP_3))
(get-proof)

smtinterpol commit 47ca378 throws a cast exception

Unexpected Exception: java.lang.ClassCastException: de.uni_freiburg.informatik.ultimate.logic.AnnotatedTerm cannot be cast to de.uni_freiburg.informatik.ultimate.logic.ApplicationTerm
(error "java.lang.ClassCastException: de.uni_freiburg.informatik.ultimate.logic.AnnotatedTerm cannot be cast to de.uni_freiburg.informatik.ultimate.logic.ApplicationTerm")

[tanjaschindler]

Related to #82