Assertion violation at CArL-EP/src/carl/core/polynomialfunctions/FieldExtensions.h:163 (mcsat)

[rainoftime]

Hi, for the following formula,

(set-logic QF_NIA)
(declare-fun i0 () Int)
(declare-fun i1 () Int)
(declare-fun i3 () Int)
(assert (>= (* i1 (* i0 i1)) (- i3)))
(assert (= (- (* i1 (* i0 i1)) (- i3)) (- 994)))
(check-sat)

smtrat (commit 97e3c34) throws an assertion violation

carl.lazard: No factor is zero in assignment.
smtrat-static: /home/peisen/test/smtrat-asan/build/resources/src/CArL-EP/src/carl/core/polynomialfunctions/FieldExtensions.h:163: std::pair<bool, Poly> carl::FieldExtensions<Rational, Poly>::extend(carl::Variable, const carl::RealAlgebraicNumber<Num>&) [with Rational = __gmp_expr<__mpq_struct [1], __mpq_struct [1]>; Poly = carl::MultivariatePolynomial<__gmp_expr<__mpq_struct [1], __mpq_struct [1]> >]: Assertion `false' failed.

Build configuration:

set(SMTRAT_Strategy "MCSATOC" CACHE STRING "Used strategy in the solver")

[nafur]

Please stop submitting issues if you don't know what you are doing. Our MCSAT does not support integers.