Added restriction so that SMT-LIB division matches OCaml/F# int division

Not sure how useful this is given that F*/SMT-LIB arbitrary precision
ints don't soundly match OCaml/F# bounded ints in more fundamental ways.
We'll need to return to this problem at some point.