An Unknown Instance of Loop Invariant?

[sjxer723]

Hi, I tried to verify the following example.

void main(int argc, char **argv)
{
    unsigned int sn, i, size;
    __CPROVER_assume(i == 1);
    __CPROVER_assume(sn == 0);

    size = argc;

    while(i<= size)
    {
        i = i + 1;
        sn = sn +1;
    }

  assert(((i <= size) || (sn == size) || (sn == 0)));
}

It should be verified since i = sn+1 is guaranteed during the execution and the difference between i and size should be at most 1. However, when I run cls foo.c (foo.c is the name of the file), it reports UNKNOWN as follows,

** statistics: 
  number of solver instances: 178
  number of solver calls: 148
  number of summaries used: 2
  number of termination arguments computed: 0

[main.assertion.1] assertion i <= size || sn >= size || sn == (unsigned int)0: UNKNOWN

** 1 of 1 unknown
** 0 of 1 failed

May I know if I should enable other options to make it report SUCCESS or FAILURE? Thanks a lot!

[viktormalik]

Hi, by default, 2LS uses the intervals abstract domain which I believe is not sufficient in this case. Since you need to reason about a relation between two variables, you'll need something stronger, the zones domain (--zones) should do.