Fatal failure in cvc5::internal::theory::quantifiers::SynthVerify::verify() at src/theory/quantifiers/sygus/synth_verify.cpp:148

[cvc5-bot]

cvc5/cvc5@67344121d30875f957e207dab7bb612460025c95 murxla/murxla@4174d484f477ee02fec04c89a7ff2f60e2a02a8f

#include <cvc5/cvc5.h>

using namespace cvc5;
int main(void)
{
Solver solver;
solver.setOption("incremental", "false");
solver.setOption("produce-abducts", "true");
Sort s0 = solver.getBooleanSort();
Sort s1 = solver.mkBagSort(s0);
Term t2 = solver.mkConst(s1, "_x2");
Op o3 = solver.mkOp(BAG_CARD);
Term t4 = solver.mkTerm(o3, {t2});
Sort s5 = t4.getSort();
Op o6 = solver.mkOp(DIVISIBLE, "3341361203");
Term t7 = solver.mkTerm(o6, {t4});
Term t8 = solver.getAbduct(t7);

return 0;
}

error:

Fatal failure within cvc5::internal::Result cvc5::internal::theory::quantifiers::SynthVerify::verify(cvc5::internal::Node, const std::vector<cvc5::internal::NodeTemplate<true> >&, std::vector<cvc5::internal::NodeTemplate<true> >&) at ../src/theory/quantifiers/sygus/synth_verify.cpp:148
Check failure

 r.getStatus() == Result::UNKNOWN

[ajreynol]

This may be caused by incorrect models for bag cardinality.