How can I use DIG to find the relationships between elements of an array?

[jsforyu]

For example, the following program,the vtrace1 I added correct?

int main () 
{
    int a [100000];
    int b [100000];
    int res [100000];
    int i = 0;int x ;
    while ( i < 100000) 
    { 
        vtrace1(res,a,b,i);
        res [ i ] = a [ i ] + b [ i ]; 
        i ++; 
    } 
        //__VERIFIER_assert ( __forall (x , (!(( x < i ) && (x >= 0)) || ( res [ x ] == a [ x ] + b [ x ])) )); 
    return 0;
}

[nguyenthanhvuh]

For array relations, you will need to give DIG a tracefile directly. An example would be

file.tcs

# DIG will find the relation A[i1] = B[-2*i1 + 5]
vtrace1; array A; array B; array C
vtrace1; [7,1,-3]; [1,-3,5,1,0,7,1]; [8,5,6,6,2,1,4]
vtrace1; [7,1,-3]; [1,-3,5,1,0,7,1]; [1,7,8,8,9,10,3]