Using z3 v4.3.1 (master branch), compiled on 64bit Scientific Linux 6.3, I provide the SMTLIB 2 input
(assert (< 0 (/ 1 2)))
and get the response
(error "line 2 column 21: logic does not support nonlinear arithmetic")
This seems specific to AUFLIRA. I don't see this problem with AUFNIRA or LRA.