Unexpected `unknown` answer from CVC4 and Z3 on a simple fact about arrays
In the example below, the trivially valid assertion is not proved by CVC4 nor Z3 (but is proved by Alt-Ergo). It is highly unexpected and should be investigated.
use int.Int
use array.Array
let f (a:array int) : unit
requires { a.length > 0 }
=
a[0] <- 0;
assert { a[0] = 0 }