Explain unit lemma reasons in interpolation

[rainoftime]

Hi, for the following formula

(set-logic QF_LIA)
(declare-const v5 Bool)
(declare-const i0 Int)
(declare-const i1 Int)
(declare-const i4 Int)
(declare-const i5 Int)
(assert (or (= (> (- (- 738 36)) i1) (distinct i1 738)) (and (> (- (- 738 36)) i1) (distinct i0 i4) (distinct i1 738) v5) (= (> (- (- 738 36)) i1) (distinct i1 738))))
(check-sat)
(check-sat-assuming-model (i1 i4 i5) (38480 38075 25214))

yices 9d0f44b

sat
yices_smt2: mcsat/nra/nra_plugin.c:1531: nra_plugin_get_assumption_conflict: Assertion `lemma_reasons.size == 0' failed.

[dddejan]

This is related to explaining under unit lemmas which is currently not supported. This needs the assumption model to be passed to NRA explanation mechanism.