# Best way to count specific elements in array / verification time depends on bound for quantified domain

 mikika Apr 8, 2014 at 12:30 PM 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 _(ghost _(pure) \integer count(int a[int], int upto, int i) _(requires 0 <= upto && 0 < i && i <= 2) _(returns (upto <= 0) ? 0 : count(a, upto-1, i) + (a[upto-1] == 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!