Open sjxer723 opened 2 months ago
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.
Hi, I tried to verify the following example.
It should be verified since
i = sn+1
is guaranteed during the execution and the difference betweeni
andsize
should be at most 1. However, when I runcls foo.c
(foo.c is the name of the file), it reports UNKNOWN as follows,May I know if I should enable other options to make it report SUCCESS or FAILURE? Thanks a lot!