support operations on reals in Z3, ignore read-only in Z3 for now