Hi,
on the following formula Z3 reports unsat while Z3 master branch reports sat
(declare-fun a () Real)
(declare-fun b () Real)
(assert (or (distinct b 2.0) (not (= (/ (- b) (* 2.0 b)) 0.0))))
(assert (< (* a b) 0.0))
(push)
(check-sat)
OS: Ubuntu 18.04
Commit: 63aae5d