
Hi all,
I have a program, where I count all elements of an array a, which are equal to a number i upto a specific bound. Afterwards, I want to find out, which value i had the highest occurrence.
Thereby, I noticed some strange behaviour of VCC or Z3. My precondition sets a bound B for the elements to be counted. Interestingly, this bound seems to have a high effect on the performance of the proof in VCC.
I attached a minimal example of my program. The use of ghost code is simply for performance reasons, since I want to examine only the abstract implementation and no concurrency is involved.
#include <vcc.h>
_(ghost _(pure) \integer count(int a[int], int upto, int i)
_(requires 0 <= upto && 0 < i && i <= 2)
_(returns (upto <= 0) ? 0 : count(a, upto1, i) + (a[upto1] == i ? 1 : 0));)
void main(int B _(ghost int a[int]))
_(requires \forall int i; (0 <= i && i < B ==> 0 < a[i] && a[i] <= 2))
_(requires 0 < B && B < 80)
{
_(ghost int b[int];)
_(assume \forall int k; (0 < k && k <= 2 ==> (b[k] == count(a, B, k))))
_(ghost int max = 0;)
_(ghost for (int i = 1; i <= 2; i++)
_(invariant \forall int k; 0 < k && k < i ==> b[k] <= max)
{
if (max <= b[i]) {
max = b[i];
}
})
}
So, I got two questions:
 Is there a better way to do the counting? I already examined the solutions for the VSTTE competition (when summing up all array elements), where you used different means (e.g. a map keeping track of all counting steps) to do this, but it did not seem to
help in my case.
 Why does the proof performance depend on a bound for a quantified domain or furthermore, how do I remove this dependency? Before shrinking down my example, the loop also contained the following invariant
_(invariant \forall int j; 0 <= j && j < B ==> b[a[j]] != 0)
which did also depend on the given bound. Is also experimented a bit using different hints and triggers, but could not get rid of the dependency yet. Does anybody have any explanations or suggestions for this matter?
I am thankful for any responses and help!

