cvc5 / cvc5-projects

1 stars 0 forks source link

Fatal failure in cvc5::internal::theory::sets::CardinalityExtension::checkNormalForm() at src/theory/sets/cardinality_extension.cpp:916 #555

Open cvc5-bot opened 1 year ago

cvc5-bot commented 1 year ago

cvc5/cvc5@b314d8d5c5a094bf5bbd734a4e0a128be7b7097d murxla/murxla@4cd7f07cb1ee987bce25d14313703cde087eda65

(set-option :sets-ext true)
(declare-const x (Set Bool))
(assert (set.member false x))
(assert (= (set.card (set.complement (set.singleton (as set.universe (Set Bool))))) (bag.count (distinct x (as set.universe (Set Bool))) (bag (set.choose (set.choose (set.singleton (set.complement (set.minus (as set.universe (Set Bool)) x))))) 1))))
(check-sat)

error:

Fatal failure within void cvc5::internal::theory::sets::CardinalityExtension::checkNormalForm(cvc5::internal::Node, std::vector<cvc5::internal::NodeTemplate<true> >&) at ../src/theory/sets/cardinality_extension.cpp:916
Check failure

 d_im.hasSent()
ajreynol commented 1 month ago

Involves cardinality with finite types.