Inconsistent triggering behaviour in properties over arrays

[gottschali]

The pure function isSorted returns true if and only an array is sorted ascendingly.
When I test it with all binary arrays of length 4, isSorted(a) or !isSorted(a) can be asserted, except for the following non-sorted arrays:

[4]int{0, 0, 1, 0}
[4]int{0, 1, 0, 1}
[4]int{1, 1, 0, 1}

I find this behaviour confusing: why can I assert that [4]int{1, 1, 1, 0} is not sorted but the assertion might fail for [4]int{0, 0, 1, 0}.

Program:

package main

const N = 4

ghost
pure
ensures sorted == forall i, j int :: {arr[i], arr[j]} 0 <= i && i < j && j < N ==> arr[i] <= arr[j]
decreases
func isSorted(arr [N]int) (sorted bool) {
	return aux(arr, 1) == N
}

ghost
pure
requires 0 < idx && idx <= N
requires forall i, j int :: {arr[i], arr[j]} 0 <= i && i < j && j < idx ==> arr[i] <= arr[j]
ensures 0 < k && k <= N
ensures k < N ==> arr[k-1] > arr[k]
ensures (k == N) ==> forall i, j int :: {arr[i], arr[j]} 0 <= i && i < j && j < N ==> arr[i] <= arr[j]
decreases N - idx
func aux(arr [N]int, idx int) (k int) {
	return idx == N ? N : (arr[idx-1] <= arr[idx] ? aux(arr, idx + 1) : idx)
}

func c0() {
	a := [4]int{0, 0, 0, 0}
	assert isSorted(a)
}

func c1() {
	a := [4]int{0, 0, 0, 1}
	assert isSorted(a)
}

func c2() {
	a := [4]int{0, 0, 1, 0}
	assert !isSorted(a) // might not hold
}
func c3() {
	a := [4]int{0, 0, 1, 1}
	assert isSorted(a)
}
func c4() {
	a := [4]int{0, 1, 0, 0}
	assert !isSorted(a)
}
func c5() {
	a := [4]int{0, 1, 0, 1}
	assert !isSorted(a) // might not hold
}
func c6() {
	a := [4]int{0, 1, 1, 0}
	assert !isSorted(a)
}
func c7() {
	a := [4]int{0, 1, 1, 1}
	assert isSorted(a)
}
func c8() {
	a := [4]int{1, 0, 0, 0}
	assert !isSorted(a)
}
func c9() {
	a := [4]int{1, 0, 0, 1}
	assert !isSorted(a)
}
func c10() {
	a := [4]int{1, 0, 1, 0}
	assert !isSorted(a)
}
func c11() {
	a := [4]int{1, 0, 1, 1}
	assert !isSorted(a)
}
func c12() {
	a := [4]int{1, 1, 0, 0}
	assert !isSorted(a)
}
func c13() {
	a := [4]int{1, 1, 0, 1}
	assert !isSorted(a) // might not hold
}
func c14() {
	a := [4]int{1, 1, 1, 0}
	assert !isSorted(a)
}
func c15() {
	a := [4]int{1, 1, 1, 1}
	assert isSorted(a)
}