Refutation soundness issue on UF formula

[rainoftime]

Hi, for the following formula,

(set-logic UF)
(declare-sort S0 0)
(assert (forall ((q2 Bool) (q3 S0) (q4 S0) (q5 S0) (q6 S0) (q7 Bool)) (not (distinct true true false false false true true true))))
(check-sat)

Alt-Ergo SMT-COMP 2020 version (https://www.starexec.org/starexec/secure/details/solver.jsp?id=28859) yields unsat,

But both cvc4 and z3 return sat.

Command: --no-locs-in-answers --threads-number=1 -i smtlib2

[rainoftime]

(set-logic NIA)
(assert (not (exists ((q0 Int) (q1 Bool)) (distinct false false true false))))
(check-sat)

[ACoquereau]

Hello @rainoftime ,
Thanks to point out this bug, it has recently been fixed in #343.