Fixing bug #3211: unsound check of elimination sort.