Paul, thanks for reporting the problem.
I fixed it: http://z3.codeplex.com/SourceControl/changeset/7eaa5562d8a9

Note that, (/ 1 2) is not really compliant with SMT 2.0 standard.
It should be (/ 1.0 2.0).
Z3 automatically adds a coercion.
After the fix, it will also accept (/ 1 2). However, other SMT solvers may refuse the input.

The fix is already available in the "unstable" (work-in-progress) branch, and will be available in the next release. If you don't want to use non officially released code. You can workaround the problem by using (/ 1.0 2.0) instead of (/ 1 2).

(/ 1 2) is fully compliant with the current version of SMTLIB 2.0.

Specifically, for AUFLIRA, see

http://smtlib.cs.uiowa.edu/logics/AUFLIRA.smt2

There it says:

 :extensions
 "For every operator op with declaration (op Real Real s) for some sort s,
  and every term t1, t2 of sort Int and t of sort Real, the expression 
  - (op t1 t) is syntactic sugar for (op (to_real t1) t)
  - (op t t1) is syntactic sugar for (op t (to_real t1))
  - (/ t1 t2) is syntactic sugar for (/ (to_real t1) (to_real t2))
 "

AUFNIRA has the same.

The SMTLIB 2 theory and logic definitions do seem to need some tidying up on this issue. While the Reals_Ints theory that AUFLIRA and AUFNIRA use does not allow (/ 1 2), the Reals theory does (in general, only when numerator and denominator have no common factors), and the *LRA logics that use Reals relax the common factor requirement, allowing (/ c n) for any integer c and positive integer n. However the *NRA logic do not include this relaxation.

My bad, I have not seen the extensions.