range types should introduce an injectivity axiom
a range type declaration
type t = range < a b >
generates a function t'int
with an axiom
forall x:t. a <= t'int x <= b
but does NOT introduce any injectivity property such as
forall x y:t. t'int x = t'int y -> x = y (*1*)
Note that the form (1) is not easy to handle by solver. A potential interesting variant is introducing a reverse function
function t'ofInt int : t
with axiom
forall x:t. t'ofInt (t'int x) = x (*2*)
This variant has the advantage of avoiding a potential quadratic number of instanciations, as it is the case for (1)