[ulber]

Not all theory fragments supported by Z3 are decidable: Z3 includes an incomplete decision procedure for non-linear real arithmetic [1].

[1] http://stackoverflow.com/a/13898524