// This returns a copy of an array `a`, but in reverse order.
reverse(a:[]int | b:[]int) {
  assume (0 <= #a) && (#a = #b) ;
  var i:int {
      i := 0 ;
      while i < #a do {
        b[(#a-1)-i] := a[i];
        i := i + 1
      }
  } ;
  assert forall i :: ((0<=i) && (i<#a)) ==> (a[i] = b[(#a-1)-i])
}