Assertion error at tsolvers/egraph/EgraphSolver.cc:1763, tsolvers/TSolverHandler.cc:125

[rainoftime]

Hi, for the following formula,
opensmt 6617993

(set-logic QF_UF)
(declare-fun uf3 (Bool Bool Bool) Bool)
(declare-fun uf6 (Bool Bool Bool Bool Bool Bool) Bool)
(declare-fun uf7 (Bool Bool Bool Bool Bool Bool Bool) Bool)
(declare-fun v0 () Bool)
(declare-fun v1 () Bool)
(declare-fun v2 () Bool)
(declare-fun v3 () Bool)
(declare-fun v4 () Bool)
(declare-fun v5 () Bool)
(declare-fun v6 () Bool)
(declare-fun v7 () Bool)
(assert (not (distinct v6 v1)))
(push 1)
(assert (uf7 (not (distinct v6 v1)) (=> v5 (distinct v6 v1)) (uf6 v3 v3 v6 v0 v2 v0) (=> v5 (distinct v6 v1)) (uf7 v3 v1 v1 v2 v5 v4 v5) (or v3 (= (=> v5 (distinct v6 v1)) (uf3 v4 v2 v7))) (= (=> v5 (distinct v6 v1)) (uf3 v4 v2 v7))))
(check-sat)
(pop 1)
(check-sat)

sat
opensmt: /opensmt/src/tsolvers/egraph/EgraphSolver.cc:1763: void Egraph::explainConstants(ERef, ERef): Assertion `logic.isConstant(getEnode(enr_qroot).getTerm())' failed.
Aborted

[rainoftime]

opensmt/src/tsolvers/TSolverHandler.cc:125: TSolver* TSolverHandler::getReasoningSolverFor(PTRef) const: Assertion `false' failed.
Aborted

(set-logic QF_UF)
(declare-fun uf4 (Bool Bool Bool Bool) Bool)
(declare-fun uf7 (Bool Bool Bool Bool Bool Bool Bool) Bool)
(declare-fun v3 () Bool)
(declare-fun v8 () Bool)
(declare-fun v11 () Bool)
(declare-fun v17 () Bool)
(check-sat)
(check-sat)
(assert (uf7 (=> v3 v11) true true true true v8 true))
(push 1)
(declare-sort S2 0)
(declare-sort S3 0)
(assert (= v3 v17))
(declare-sort S4 0)
(push 1)
(assert false)
(check-sat)
(pop 1)
(check-sat)
(check-sat)
(pop 1)
(push 1)
(declare-sort S2 0)
(assert (uf4 (= (=> v3 v11) (not v8)) true true true))
(check-sat)
(declare-sort S2 0)
(declare-sort S3 0)
(declare-sort S4 0)
(declare-sort S2 0)
(check-sat)
(pop 1)
(assert (=> v3 v11))
(check-sat)