usage of array.Array should not enforce polymorphic VCs
In Why3 0.88, for a program importing array.Array
but wasn't using any other polymorphic types, the resulting tasks were not polymorphic and were consequently easier to discharge by SMT solvers.
Would it be possible to ignore the polymorphism of the new array type in Why3 1.0 ?