search

cvc5 / cvc5-projects

1 stars 0 forks source link

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

Open cvc5-bot opened 1 year ago

cvc5-bot commented 1 year ago

cvc5/cvc5@956404215a6e67d1c06d06e4fc912e89a9168c15 murxla/murxla@3c45751cb73ce5ff0157aff6783aec3c9000f0f7

(set-option :deep-restart all)
(declare-const x Real)
(assert (< (sin x) (arcsec 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:872
Check failure

 false
ajreynol commented 1 year ago

A deep restart is using internally generated skolems in this case, making them input literals, which is likely confusing the nl model setup.