Assertion violation at smtrat-cad/utils/CADConstraints.h:131 (qe)

[rainoftime]

Hi, for the following formula,

(set-logic QF_LRA)
(declare-fun v5 () Bool)
(declare-fun v11 () Bool)
(declare-fun v16 () Bool)
(declare-fun r2 () Real)
(declare-fun r3 () Real)
(declare-fun r8 () Real)
(declare-fun r9 () Real)
(assert (distinct v16 v11))
(check-sat)
(eliminate-quantifiers (exists r3 r8))
(assert (xor v5 (distinct v16 v11)))
(eliminate-quantifiers (exists r2 r9))

smtrat (commit 97e3c34) throws an assertion violation

Equivalent Quantifier-Free Formula: -1*v11 + v16 != 0
Quantified Formula: QE(exists r2 r9) (-1*v11 + v16 != 0 and (-1*v11 + v16 != 0 xor v5))
smtrat-static: /home/peisen/test/tofuzz/smtrat/src/smtrat-cad/utils/CADConstraints.h:131: std::size_t smtrat::cad::CADConstraints<BT>::add(const ConstraintT&) [with smtrat::cad::Backtracking BT = smtrat::cad::Backtracking::UNORDERED; std::size_t = long unsigned int; smtrat::ConstraintT = carl::Constraint<carl::MultivariatePolynomial<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> > >]: Assertion `r.second' failed.