[613] % time z3release smt.arith.solver=2 small.smt2
sat
sat
real  0m0.020s
user  0m0.012s
sys   0m0.004s
[614] % time z3release smt.arith.solver=6 small.smt2
sat
sat
real  0m23.188s
user  0m22.999s
sys   0m0.008s
[615] % 
[615] % cat small.smt2
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (> a 2))
(check-sat)
(assert (not (> 0 (+ (/ 1 c a)) (- 1))))
(check-sat)
[616] %