[733] % time z3release smt.arith.solver=2 small.smt2
sat
real  0m0.331s
user  0m0.317s
sys   0m0.004s
[734] % time z3release smt.arith.solver=6 small.smt2
unknown
real  0m45.052s
user  0m44.577s
sys   0m0.119s
[735] % 
[735] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (forall ((d Real)) (and (< a 0) (> b 0) (=> (> d 0) (>= d b) (= (div d 0) a)) (= c 0))))
(check-sat)
[736] %