Assertion violation in LIA interpolation

[annabeks]

OpenSMT encounters an assertion violation in get-interpolant.

Issue originally discovered by running "golem -e tpa microwave35_000.smt2" .
It can be reproduced directly in OpenSMT on the attached smt2 file itp_coeff_bug.zip

Assertion fails in mkConst() when trying to create an integer constant with a rational value.

My understanding is that polyToPTRef() fails in normalizing the coefficient of a PTRef_Undef variable when type is Integer:
since in line 36, the coefficient of the Undef variable is discarded when computing the lcm, in line 47, coeff might be a fraction.