Aren't these models non-deterministic by nature?
I don't know why, but it is easy to imagine a scenario where non-determinism makes sense. For example the computer could say "I am supposed to do this floating point division. Let's see ... my very exact FP-Division unit is pretty hot at the moment. 82°C. Let's pass this calculation to the slightly less exact FP-Division unit then".
i think the kind of scenario you're describing does not occur in commercially sold hardware, because it poses problems not only for customers but also for verification engineers at the design house. also, in the specific case of floating-point division, it would violate the ieee-754 standard. it might happen in an experimental academic project