Array encoding too weak to show congruence

[jcp19]

The following Gobra program fails to verify, even though it should:

package test

pure
decreases
func f(arr [3]int) int

requires a == b
func test(a [3]int, b [3]int) {
        assert f(a) == f(b)
}

Error:

Assert might fail. 
Assertion f(a) == f(b) might not hold.