z3 - Proving simple property of a function over array -

suppose have following annotated c-code:

int a[3] = {0}; /*@ requires \valid(a+(0..2));     assigns a[0..2];     ensures \forall int j; 0 <= j < 3 ==> (a[j] == j); */ int main() {     int = 0;     /*@ loop assigns i, a[0..(i-1)];         loop invariant inv1: 0 <= <= 3;         loop invariant inv2:         \forall int k; 0 < k <= ==> a[k-1] == k-1; */     while (i < l) {       a[i] = i;       i++;     }     //@ assert final_i: == 3;     //@ assert final_a: a[1] == 1; } 

neither z3 nor alt-ergo able prove assert final_a , post condition; z3 not able prove loop invariant also;

output alt-ergo:

# ~/queue $ frama-c -wp -wp-prover alt-ergo test2.c  [kernel] parsing framac_share/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] parsing test2.c (with preprocessing) [wp] running wp plugin... [wp] collecting axiomatic usage [wp] warning: missing rte guards [wp] 14 goals scheduled [wp] [qed] goal typed_main_pre : valid [wp] [qed] goal typed_main_loop_inv_inv1_established : valid [wp] [qed] goal typed_main_loop_inv_inv2_established : valid [wp] [qed] goal typed_main_assert_final_i : valid [wp] [alt-ergo] goal typed_main_loop_inv_inv1_preserved : valid (qed:1ms) (14ms) (15) [wp] [qed] goal typed_main_loop_assign_part1 : valid [wp] [alt-ergo] goal typed_main_loop_inv_inv2_preserved : valid (45ms) (51) [wp] [qed] goal typed_main_loop_assign_part2 : valid [wp] [qed] goal typed_main_loop_assign_part3 : valid [wp] [qed] goal typed_main_assign_part1 : valid [wp] [qed] goal typed_main_assign_part3 : valid [wp] [alt-ergo] goal typed_main_assign_part2 : valid (20ms) (12) [wp] [alt-ergo] goal typed_main_assert_final_a : unknown (3.5s) [wp] [alt-ergo] goal typed_main_post : timeout (qed:1ms) [wp] proved goals:   12 / 14      qed:             9  (0ms-1ms)      alt-ergo:        3  (14ms-45ms) (51) (interrupted: 1) (unknown: 1) 

output z3:

$ frama-c -wp -wp-prover z3 test2.c                                                                                       [kernel] parsing framac_share/libc/__fc_builtin_for_normalization.i (no preprocessing) [kernel] parsing test2.c (with preprocessing) [wp] running wp plugin... [wp] collecting axiomatic usage [wp] warning: missing rte guards [wp] 14 goals scheduled [wp] [qed] goal typed_main_pre : valid [wp] [qed] goal typed_main_loop_inv_inv1_established : valid [wp] [qed] goal typed_main_loop_inv_inv2_established : valid [wp] [qed] goal typed_main_assert_final_i : valid [wp] [z3] goal typed_main_loop_inv_inv1_preserved : valid (20ms) [wp] [qed] goal typed_main_loop_assign_part1 : valid [wp] [qed] goal typed_main_loop_assign_part2 : valid [wp] [qed] goal typed_main_loop_assign_part3 : valid [wp] [qed] goal typed_main_assign_part1 : valid [wp] [z3] goal typed_main_assert_final_a : unknown (356ms) [wp] [qed] goal typed_main_assign_part3 : valid [wp] [z3] goal typed_main_post : unknown (911ms) [wp] [z3] goal typed_main_assign_part2 : valid (10ms) [wp] [z3] goal typed_main_loop_inv_inv2_preserved : unknown (1.3s) [wp] proved goals:   11 / 14      qed:             9       z3:              2  (10ms-20ms) (unknown: 3) 

what missing?

if change inv2 loop invariant to:

        loop invariant inv2:         \forall int k; 0 <= k < ==> a[k] == k; 

.. alt-ergo able prove final_a assertion , main() postconditions.