Why can small size of array be proved, but can't large one?

Question

I tried to prove a example from frama-c-wp-tutorial That example is at Sect.6.2.4, but I modified some code.

#include <stdio.h>
#include <stdlib.h>
#include <stdbool.h>

#define size    150
/*@
    axiomatic Counter{
        logic integer counter{L}(bool arr[size], integer begin, integer end) reads arr[0 .. (size-1)];
        
        axiom count_empty_range{L}:
            \forall bool arr[size], integer begin, integer end;
                begin<0 || begin>=end || end>size
                    ==> counter{L}(arr, begin, end) == 0;
                    
        axiom count_others{L}:
            \forall bool arr[size], integer begin, integer end;
                0 <= begin < end <= size && arr[end-1] != true
                    ==> counter{L}(arr, begin, end) == counter{L}(arr, begin, end-1);
        
        axiom count_true{L}:
            \forall bool arr[size], integer begin, integer end;
                0 <= begin < end <= size && arr[end-1] == true
                    ==> counter{L}(arr, begin, end) == counter{L}(arr, begin, end-1) + 1;
    }
    
    lemma counter_range{L}:
        \forall bool arr[size], integer begin, integer end;
            0 <= begin < end <= size
                ==> 0 <= counter(arr, begin, end) <= end-begin;
*/

The result was obtained with Frama-c 25.0, Alt-Ergo 2.4.2, cvc4 1.8 and Z3 4.8.6.

$ frama-c -wp -wp-rte -wp-prover alt-ergo,cvc4,z3 test.c
[kernel] Parsing test.c (with preprocessing)
[wp] 1 goal scheduled
[wp] [Failed] Goal typed_lemma_counter_range
  Z3 4.8.6: Timeout (10s) (cached)
  CVC4 1.8: Timeout (10s) (cached)
  Alt-Ergo 2.4.2: Timeout (10s) (cached)
[wp] [Cache] found:3
[wp] Proved goals:    0 / 1
  Alt-Ergo 2.4.2:    0  (interrupted: 1) (cached: 1)
  CVC4 1.8:          0  (interrupted: 1) (cached: 1)
  Z3 4.8.6:          0  (interrupted: 1) (cached: 1)

The thing that I can't understand is it will be proved successfully if I change the size into 14 (or even less).Is there anything wrong?

Answer 1

I suspect that with a smaller size the provers are able to exhaustively unfold all possible instantiations of the axioms count_others and count_true until they can apply count_empty_range, while this becomes of course impossible for a larger value.

In fact, what you want to do is a proof by induction, something first order automated solvers can't really do. Fortunately, there's a tactic dedicated to that in WP's interactive prover in Frama-C's GUI (see WP manual, section 2.2). Namely, while editing the script corresponding to the proof of the lemma, you can select the end_0 variable, and then the induction tactic:

(NB: the list of tactics on the right side of the panel depends on the context, hence you won't see the induction tactic until you select an integer variable).

Launching the tactic should complete the proof. You can then save the script and replay it later with frama-c -wp -wp-rte -wp-prover script,alt-ergo,z3,cvc4 test.c