Fatal failure in cvc5::internal::RemoveTermFormulas::runCurrentInternal() at src/smt/term_formula_removal.cpp:273

[cvc5-bot]

cvc5/cvc5@acff956
murxla/murxla@1e767a5

set-murxla-options --cvc5
71298 new
64703 set-option produce-models true
29836 set-option incremental true
69840 mk-sort SORT_STRING
return s3
81476 mk-sort SORT_SEQ s3
return s6
77695 mk-special-value s6 "seq.empty"
return t1
87078 mk-const s6 "_x29"
return t2
4740 mk-term OP_DISTINCT SORT_BOOL 2 t2 t1
return t3 s8
84486 mk-term OP_SEQ_LENGTH SORT_INT 1 t2
return t4 s5
19958 mk-term OP_RE_ALLCHAR SORT_REGLAN 0
return t5 s1
80154 mk-term OP_INT_IS_DIV SORT_BOOL 1 t4 1 40577120
return t7 s8
35815 assert-formula t3
37255 assert-formula t7
61588 check-sat
36596 cvc5-block-model-values 5 t4 t1 t5 t1 t5
18853 check-sat

error:

Fatal failure within cvc5::internal::Node cvc5::internal::RemoveTermFormulas::runCurrentInternal(cvc5::internal::TNode, bool, cvc5::internal::TrustNode&, uint32_t, cvc5::internal::TConvProofGenerator*) at ../src/smt/term_formula_removal.cpp:273
Check failure

 node.getKind()!=Kind::WITNESS