You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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!
The text was updated successfully, but these errors were encountered:
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!
The text was updated successfully, but these errors were encountered: