为什么CBMC的平仓次数更多？

Question

让我们考虑下面给出的代码，我想知道为什么当我们假设io的初始值大于2时，CBMC的松开程度超过了上限。

#include<assert.h>
     void main()
    {
      int i0;
    int o1;
    __CPROVER_assume(i0>=2);
    //assert(i0>=0);
    while(i0<=10)
    {
      i0=i0+1;
    }
    o1=i0+1;
    assert((o1 <= 1));
    }

CBMC输出：

 CBMC version 5.8 64-bit x86_64 linux
Parsing /tmp/in1_1524461553_1936466587.c
Converting
Type-checking in1_1524461553_1936466587
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
Unwinding loop main.0 iteration 1 file /tmp/in1_1524461553_1936466587.c line 9 function main thread 0
Unwinding loop main.0 iteration 2 file /tmp/in1_1524461553_1936466587.c line 9 function main thread 0
Unwinding loop main.0 iteration 3 file /tmp/in1_1524461553_1936466587.c line 9 function main thread 0
Unwinding loop main.0 iteration 4 file /tmp/in1_1524461553_1936466587.c line 9 function main thread 0
Unwinding loop main.0 iteration 5 file /tmp/in1_1524461553_1936466587.c line 9 function main thread 0
Unwinding loop main.0 iteration 6 file /tmp/in1_1524461553_1936466587.c line 9 function main thread 0
Unwinding loop main.0 iteration 7 file /tmp/in1_1524461553_1936466587.c line 9 function main thread 0
Unwinding loop main.0 iteration 8 file /tmp/in1_1524461553_1936466587.c line 9 function main thread 0
Unwinding loop main.0 iteration 9 file /tmp/in1_1524461553_1936466587.c line 9 function main thread 0
Unwinding loop main.0 iteration 10 file /tmp/in1_1524461553_1936466587.c line 9 function main thread 0
Unwinding loop main.0 iteration 11 file /tmp/in1_1524461553_1936466587.c line 9 function main thread 0
Unwinding loop main.0 iteration 12 file /tmp/in1_1524461553_1936466587.c line 9 function main thread 0
Unwinding loop main.0 iteration 13 file /tmp/in1_1524461553_1936466587.c 

Answer 1

我猜symex还不够聪明，没有意识到循环上的条件在某个迭代之后总是假的。它尝试在执行过程中对表达式进行一些简化，但并不是那么多。当它被转换为公式并传递给SAT求解器时，SAT求解器将很快发现循环的这些迭代条件永远不会得到满足，并丢弃公式的这些部分，因此它不应该影响正确性(当然，这可能意味着CBMC需要很长时间才能运行)。