-
Jean-Christophe Filliâtre authored
predicates permut over maps and arrays are given new semantics, as follows: - MapPermut: permut m1 m2 l u means that m1[l..u[ is a permutation of m2[l..u[ and values outside the interval [l..u[ are *ignored*. - ArrayPermut: permut_sub a1 a2 l u means that a1[l..u[ is a permutation of a2[l..u[ and other meaningful values are *identical*. - ArrayPermut: another predicate map_permut_sub has the same semantics as MapPermut.permut_sub, that is values outside of the interval [l..u[ are ignored
e79e9a4f