Assertion violation at lib/datastructures/VariableBounds.tpp:535 (qe)

[rainoftime]

Hi, for the following formula,

(set-logic QF_LRA)
(declare-fun v1 () Bool)
(declare-fun v3 () Bool)
(declare-fun v8 () Bool)
(declare-fun r0 () Real)
(assert (= r0 773183.0))
(assert v1)
(assert (distinct v3 (>= (+ r0 117.0) 939.0)))
(declare-fun r5 () Real)
(assert v8)
(eliminate-quantifiers (exists r0 r5))

smtrat (commit 97e3c34) throws an assertion violation

Quantified Formula: QE(exists r0 r5) (-773183 + r0 = 0 and v1 and (822 + -1*r0 <= 0 xor v3) and v8)
smtrat-static: /home/peisen/test/tofuzz/smtrat/src/lib/datastructures/VariableBounds.tpp:535: const RationalInterval& smtrat::vb::VariableBounds<T>::getInterval(const carl::Variable&) const [with T = carl::Constraint<carl::MultivariatePolynomial<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> > >; smtrat::RationalInterval = carl::Interval<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >]: Assertion `mpConflictingVariable == __null' failed.