Hi, For this formula, ``` (assert (= 0 1)) (assert (distinct 0 2)) (check-sat-using smtfd) ``` z3 gives an incorrect `sat` on this `unsat` formula. OS: Ubuntu 18.04 Revision: 805ac74