search

cvc5 / cvc5-projects

1 stars 0 forks source link

Fatal Failure at src/theory/theory_model_builder.cpp:47 #176

Open wintered opened 4 years ago

wintered commented 4 years ago 
[611] % cvc4 -q small.smt2
unsat
[612] % cvc4 -q --sygus-inference small.smt2
Fatal failure within CVC4::Node CVC4::theory::TheoryEngineModelBuilder::Assigner::getNextAssignment() at src/theory/theory_model_builder.cpp:47
Check failure
 false
Aborted
[613] % 
[613] % cat small.smt2
(set-option :sets-ext true)
(declare-datatype a ((b) (c)))
(declare-fun d () (Set (Array a a)))
(assert (= (card d) 5))
(check-sat)
[614] %

OS: Ubuntu 18.04 Commit: 6b599f8

ajreynol commented 4 years ago

Appears to be related to our support for cardinality of sets of finite types.