Fatal failure in cvc5::internal::theory::arith::nl::NlModel::simpleCheckModelMsum() at src/theory/arith/nl/nl_model.cpp:894

[cvc5-bot]

cvc5/cvc5@c27f5d6
murxla/murxla@51c21ba

(set-logic QF_NIA)
(declare-const x Int)
(declare-const _x Int)
(assert (= x (* _x (mod (int.pow2 _x) x))))
(assert ((_ divisible 125436566) _x))
(check-sat)

error:

Fatal failure within bool cvc5::internal::theory::arith::nl::NlModel::simpleCheckModelMsum(const std::map<cvc5::internal::NodeTemplate<true>, cvc5::internal::NodeTemplate<true> >&, bool) at ../src/theory/arith/nl/nl_model.cpp:894
Check failure

 false

Related issue without safe-options: #643

[ajreynol]

This also is not an issue with safe-options, ddsmt likely over-minimized.