search

cvc5 / cvc5-projects

1 stars 0 forks source link

Fatal failure in cvc5::internal::theory::quantifiers::fmcheck::FullModelChecker::doExhaustiveInstantiation() at src/theory/quantifiers/fmf/full_model_check.cpp:664 #561

Open cvc5-bot opened 1 year ago

cvc5-bot commented 1 year ago

cvc5/cvc5@b314d8d5c5a094bf5bbd734a4e0a128be7b7097d murxla/murxla@4cd7f07cb1ee987bce25d14313703cde087eda65

(set-option :assign-function-values false)
(declare-const x String)
(assert ((_ divisible 2951425250) (str.to_int x)))
(check-sat)

error:

Fatal failure within virtual int cvc5::internal::theory::quantifiers::fmcheck::FullModelChecker::doExhaustiveInstantiation(cvc5::internal::theory::quantifiers::FirstOrderModel*, cvc5::internal::Node, int) at ../src/theory/quantifiers/fmf/full_model_check.cpp:664
Check failure

 !mcond.empty()
ajreynol commented 1 year ago

Involves old implementation of FMF. We should consider reimplementing this using the utilities for enumerative instantiation + instantiation evaluation.