Assertion violation at smtrat-mcsat/explanations/onecellcad/OneCellCAD.h:969 (mcsat)

[rainoftime]

Hi, for the following formula,

(set-logic QF_NIA)
(declare-fun i4 () Int)
(declare-fun i9 () Int)
(declare-fun i16 () Int)
(assert (> (- i9) (* (* 686 i4) i16)))
(assert (> (/ i9 918) 918))
(check-sat)

smtrat (commit 97e3c34) throws an assertion violation

smtrat-static: /home/peisen/test/smtrat-asan/src/smtrat-mcsat/explanations/onecellcad/OneCellCAD.h:969: smtrat::mcsat::onecellcad::ShrinkResult smtrat::mcsat::onecellcad::OneCellCAD::shrinkCell(const smtrat::mcsat::onecellcad::TagPoly2&, smtrat::mcsat::onecellcad::CADCell&): Assertion `isPointInsideCell(cell)' 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.