Assertion violation at src/btordbg.c:375

[rainoftime]

Hi, for the following formula,
boolector 6fce0ac

(set-logic BV)
(declare-fun _substvar_651_ () Bool)
(declare-const v6 Bool)
(declare-const v28 Bool)
(declare-const bv_41-0 (_ BitVec 41))
(assert (or (xor (forall ((q5 Bool) (q6 (_ BitVec 41)) (q7 (_ BitVec 8)) (q8 Bool) (q9 (_ BitVec 41))) (distinct (_ bv0 41) bv_41-0)) false true true true (= (exists ((q0 Bool) (q1 Bool) (q2 Bool) (q3 Bool)) (exists ((q0 Bool) (q1 Bool) (q2 Bool) (q3 Bool)) q0)) v6) true v28) _substvar_651_))
(check-sat)

$ boolector xx.smt2
boolector: /home/peisen/test/tofuzz/boolector/src/btordbg.c:375: btor_dbg_precond_regular_binary_bv_exp: Assertion `btor_node_get_sort_id (e0) == btor_node_get_sort_id (e1)' failed.
[btor>main] CAUGHT SIGNAL 6
unknown
Aborted

[mpreiner]

Boolector is not actively maintained and developed anymore. It was succeeded by Bitwuzla and the repository is now archived.