./goblint --conf conf/svcomp.json --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/no-overflow.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c


--------------------------------------------------------------------------------


[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[0;33m[Warning] --sets is deprecated, use --set instead.[0;0;00m
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:110:3-667:3 with factor 2
[Info] Setting "ana.int.interval" to true
[Info] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region, pthreadMutexType"
[Info] Enabled congruence domain.
[Info] Enabled octagon domain ONLY for:
[Info] abort, __assert_fail, i, count, tmp, key, a, count, i, j, i___0, j___0, k, size, r, top, expression, s, tmp, s__state, ret, blastFlag, cb, num1, buf, state, s__init_buf___0
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:78:3-78:32)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:93:3-93:40)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:94:7-94:22)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:95:9-95:24)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:313:77-313:105)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:233:81-233:100)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:404:81-404:99)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:406:85-406:103)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:415:85-415:143)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:415:85-415:143)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:416:87-416:105)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:357:77-357:115)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:358:81-358:119)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:358:81-358:119)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:366:83-366:91)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:373:89-373:148)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:373:89-373:148)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:374:91-374:150)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:374:91-374:150)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:379:91-379:112)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:342:81-342:139)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:342:81-342:139)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:313:77-313:105)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:233:81-233:100)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:313:77-313:105)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:342:81-342:139)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:342:81-342:139)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:357:77-357:115)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:358:81-358:119)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:358:81-358:119)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:366:83-366:91)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:373:89-373:148)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:373:89-373:148)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:374:91-374:150)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:374:91-374:150)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:379:91-379:112)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:404:81-404:99)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:406:85-406:103)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:415:85-415:143)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:415:85-415:143)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:416:87-416:105)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:584:79-584:148)
[Warning][Deadcode] Function 'ssl3_accept' has dead code:
  on line 220 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:220-220)
  on lines 239..243 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:239-243)
  on lines 248..249 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:248-249)
  on line 254 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:254-254)
  on lines 258..259 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:258-259)
  on lines 264..267 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:264-267)
  on lines 272..275 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:272-275)
  on lines 277..278 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:277-278)
  on line 395 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:395-395)
  on line 682 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:682-682)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 245
  dead: 23
  total lines: 268
[Warning][Deadcode][CWE-571] condition '! skip' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:638:11-638:17)
[Warning][Deadcode][CWE-571] condition 'got_new_session' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:582:81-582:96)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:110:10-110:11)
[Warning][Deadcode][CWE-570] condition 's__state == 12292' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:113:9-113:26)
[Warning][Deadcode][CWE-570] condition 's__state == 16384' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:116:11-116:28)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:110:10-110:11)
[Warning][Deadcode][CWE-570] condition 's__state == 8192' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:119:13-119:29)
[Warning][Deadcode][CWE-570] condition 's__state == 24576' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:122:15-122:32)
[Warning][Deadcode][CWE-570] condition 's__state == 8195' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:125:17-125:33)
[Warning][Deadcode][CWE-571] condition 'blastFlag == 0' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:302:81-302:95)
[Warning][Deadcode][CWE-570] condition 's__state == 8480' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:128:19-128:35)
[Warning][Deadcode][CWE-570] condition 's__state == 8481' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:131:21-131:37)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:110:10-110:11)
[Warning][Deadcode][CWE-570] condition 's__state == 8482' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:134:23-134:39)
[Warning][Deadcode][CWE-570] condition 's__state == 8195' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:125:17-125:33)
[Warning][Deadcode][CWE-571] condition 's__state == 8464' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:137:25-137:41)
[Warning][Deadcode][CWE-570] condition 'blastFlag == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:302:81-302:95)
[Warning][Deadcode][CWE-570] condition 's__state == 8481' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:131:21-131:37)
[Warning][Deadcode][CWE-570] condition 's__state == 8465' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:140:27-140:43)
[Warning][Deadcode][CWE-570] condition 'blastFlag == 0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:302:81-302:95)
[Warning][Deadcode][CWE-571] condition 'blastFlag == 1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:319:81-319:95)
[Warning][Deadcode][CWE-570] condition 's__state == 8497' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:149:33-149:49)
[Warning][Deadcode][CWE-570] condition 's__state == 8513' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:155:37-155:53)
[Warning][Deadcode][CWE-570] condition 's__state == 8529' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:161:41-161:57)
[Warning][Deadcode][CWE-570] condition 's__state == 8545' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:167:45-167:61)
[Warning][Deadcode][CWE-570] condition 's__state == 8561' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:173:49-173:65)
[Warning][Deadcode][CWE-570] condition 's__state == 8577' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:182:55-182:71)
[Warning][Deadcode][CWE-570] condition 's__state == 8593' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:188:59-188:75)
[Warning][Deadcode][CWE-570] condition 's__state == 8609' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:194:63-194:79)
[Warning][Deadcode][CWE-570] condition 's__state == 8641' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:200:67-200:83)
[Warning][Deadcode][CWE-570] condition 's__state == 8657' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:206:71-206:87)
[Warning][Deadcode][CWE-571] condition 'l + 1UL' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:369:85-369:92)
[Warning][Deadcode][CWE-570] condition 's__state == 8673' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:212:75-212:91)
[Warning][Deadcode][CWE-570] condition 's__state == 3' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:215:77-215:90)
[Warning][Deadcode][CWE-570] condition 'blastFlag == 2' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:539:81-539:95)
[Warning][Deadcode][CWE-571] condition 'l + 1UL' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:369:85-369:92)
[Warning][Deadcode][CWE-571] condition 's__version * 8 != 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:233:81-233:100)
[Warning][Deadcode][CWE-570] condition 'blastFlag == 4' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:561:81-561:95)
[Warning][Deadcode][CWE-571] condition 's__version * 8 != 3' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/bitvector/s3_srvr_2.BV.c.cil.c:233:81-233:100)
SV-COMP result: unknown
[Info][Witness] witness generation summary:
  total generation entries: 1
