Assertion violation at src/btordbg.c:322

[rainoftime]

Hi, for the following formula,
boolector 6fce0ac

(set-logic BV)
(declare-fun _substvar_7291_ () Bool)
(declare-fun _substvar_7499_ () Bool)
(declare-const bv_3-0 (_ BitVec 3))
(declare-const v16 Bool)
(assert (or (not (exists ((q58 Bool) (q59 (_ BitVec 6))) (=> (xor true q58 true q58 q58 false q58 false q58 true (exists ((q50 (_ BitVec 8)) (q51 (_ BitVec 1))) (not (distinct ((_ extract 0 0) bv_3-0) q51 (bvcomp (_ bv0 52) (_ bv0 52)))))) false))) v16 (forall ((q61 Bool) (q62 (_ BitVec 40)) (q63 (_ BitVec 5)) (q64 (_ BitVec 3))) (or _substvar_7291_ (not (exists ((q58 Bool) (q59 (_ BitVec 6))) (=> (xor true q58 true q58 q58 false q58 false q58 true (exists ((q50 (_ BitVec 8)) (q51 (_ BitVec 1))) (not (distinct ((_ extract 0 0) bv_3-0) q51 (bvcomp (_ bv0 52) (_ bv0 52)))))) false))) _substvar_7499_))))
(check-sat)

$ boolector xx.smt2
boolector: /home/peisen/test/tofuzz/boolector/src/btordbg.c:322: btor_dbg_precond_eq_exp: Assertion `btor_node_get_sort_id (real_e0) == btor_node_get_sort_id (real_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.