Fatal failure in cvc5::internal::TheoryEngine::checkTheoryAssertionsWithModel() at src/theory/theory_engine.cpp:2109

[cvc5-bot]

cvc5/cvc5@231c532
murxla/murxla@51f5b5c

(declare-const x RoundingMode)
(set-option :debug-check-models true)
(set-option :bv-solver bitblast-internal)
(declare-const _x2 (Array RoundingMode RoundingMode))
(declare-const _x4 (Array RoundingMode RoundingMode))
(declare-const _x5 (Array RoundingMode RoundingMode))
(assert (and (set.choose (set.insert (distinct (set.member x (set.singleton x)) (set.member (select _x4 (select _x4 (select _x4 (select _x4 (select _x2 (select _x5 RTZ)))))) (set.singleton (select _x2 (select _x5 RTZ))))) (set.singleton (set.member x (set.singleton x))))) (set.member (select _x4 x) (set.singleton x))))
(check-sat)

error:

Fatal failure within void cvc5::internal::TheoryEngine::checkTheoryAssertionsWithModel(bool) at ../src/theory/theory_engine.cpp:2109
Internal error detected getValue((let ((_let_1 (select _x2 (select _x5 roundTowardZero)))) (= #b1 (bvcomp (RMBITBLAST _let_1) (RMBITBLAST (select _x4 (select _x4 (select _x4 (select _x4 _let_1))))))))): true