Invalid interpolant computed when a mod operation is present in both partitions

[blishko]

For the following problem OpenSMT computes incorrect invariant:

(set-option :produce-interpolants 1)
;(set-option :certify-interpolants 1)
(set-logic QF_LIA)
(declare-fun x () Int)
(assert (!
(< (mod x 10) 5)
:named a))


(assert (!
(> (mod x 10) 6)
:named b))
(check-sat)
(get-interpolants a b)
(exit)

Interpolant computed:

((<= (- 4) (* (- 1) .mod_24_27)))

The problem is that OpenSMT keeps the internal auxiliary variable in the interpolant.

Suggested solution:
Add a post processing step to clean up the interpolant and replace the internal auxiliary variable with the term it represents.