Fatal failure in cvc5::internal::theory::TheoryEngineModelBuilder::buildModel() at src/theory/theory_model_builder.cpp:1089

cvc5 / cvc5-projects

1 stars 0 forks source link

Fatal failure in cvc5::internal::theory::TheoryEngineModelBuilder::buildModel() at src/theory/theory_model_builder.cpp:1089 #702

Open cvc5-bot opened 2 months ago

cvc5-bot commented 2 months ago

cvc5/cvc5@e5639007e62fc5b3fbcde5c6e8193de92d979651 murxla/murxla@b301fd498044c54fb64ce430fd8db68e9f67e4f2

(declare-const x (Set Int))
(assert (= (set.choose x) (int.pow2 (div (set.choose x) (set.choose x)))))
(assert (set.member (set.card x) x))
(check-sat)

error:

Fatal failure within bool cvc5::internal::theory::TheoryEngineModelBuilder::buildModel(cvc5::internal::theory::TheoryModel*) at ../src/theory/theory_model_builder.cpp:1089
Check failure

 false

ajreynol commented 2 months ago

Seems to be caused by a cyclic dependency involving x during model construction.