./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/loop-industry-pattern/ofuf_1.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/loop-industry-pattern/ofuf_1.c:251:1-258:1 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:295:1-302:1 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:333:1-340:1 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:377:1-380:1 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:401:1-418:1 with factor 2
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:431:1-441:1 with factor 8
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:10:5-12:5 with factor 12
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:21:9-27:9 with factor 4
[Info] unrolling loop at lib/libc/stub/src/stdlib.c:40:3-45:3 with factor 6
[Info] Setting "ana.int.interval" to true
[Info] function Id_MCDC_113 is recursive, disable interval and interval_set contexts
[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] Id_MCDC_107, avoid_zero, i, count, tmp, key, a, count, j, k, size, i, i___0, j___0, a, top, expression, Id_MCDC_121, Id_MCDC_176, Id_MCDC_158, Id_MCDC_150, Id_MCDC_145, tmp___2, Id_MCDC_35, Id_MCDC_141, Id_MCDC_146, Id_MCDC_156, tmp, Id_MCDC_134, Id_MCDC_100, Id_MCDC_101, tmp, tmp___0, Id_MCDC_111, Id_MCDC_139, Id_MCDC_140, Id_MCDC_136, Id_MCDC_137, Id_MCDC_108, Id_MCDC_109, Id_MCDC_135, Id_MCDC_138, tmp, Id_MCDC_100, Id_MCDC_134, Id_MCDC_101, tmp, tmp___0, y, cond
[Info] Enabled widening thresholds
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
[Info][Imprecise] Invalidating expressions: & Id_MCDC_176 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:477:1-477:35)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:435:1-435:86)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:435:1-435:86)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:435:1-435:86)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:435:1-435:86)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:319:1-319:29)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:321:1-321:55)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:299:1-299:56)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:299:1-299:56)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:299:1-299:56)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:299:1-299:56)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:299:1-299:56)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:299:1-299:56)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:299:1-299:56)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:299:1-299:56)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:323:10-323:54)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:323:10-323:54)
[Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:3:1-3:72)
[Warning][Deadcode] Function 'assume_abort_if_not' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:5:1-7:1)
[Warning][Deadcode] Function 'Id_MCDC_114' is uncalled: 12 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:325:1-355:1)
[Warning][Deadcode] Function 'Id_MCDC_107' has dead code:
  on line 227 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:227-227)
  on line 229 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:229-229)
  on line 231 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:231-231)
  on lines 236..237 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:236-237)
  on lines 239..240 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:239-240)
  on lines 242..243 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:242-243)
  on lines 245..246 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:245-246)
  on line 248 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:248-248)
  on line 251 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:251-251)
  on lines 253..254 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:253-254)
  on line 256 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:256-256)
  on line 259 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:259-259)
  on line 261 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:261-261)
  on line 265 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:265-265)
  on line 270 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:270-270)
  on line 272 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:272-272)
[Warning][Deadcode] Function 'Id_MCDC_113' has dead code:
  on line 311 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:311-311)
[Warning][Deadcode] Function 'Id_MCDC_115' has dead code:
  on line 390 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:390-390)
  on line 392 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:392-392)
  on lines 394..396 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:394-396)
  on line 398 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:398-398)
  on lines 400..401 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:400-401)
  on line 403 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:403-403)
  on line 405 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:405-405)
  on lines 407..414 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:407-414)
  on line 416 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:416-416)
  on lines 419..420 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:419-420)
  on line 423 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:423-423)
[Warning][Deadcode] Function '__VERIFIER_assert' has dead code:
  on line 489 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:489-489)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 80
  dead: 60 (15 in uncalled functions)
  total lines: 140
[Warning][Deadcode][CWE-571] condition '(int )Id_MCDC_150 < 4' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:377:4-377:55)
[Warning][Deadcode][CWE-571] condition '(long long )(Id_MCDC_135 / Id_MCDC_136) >= 0LL' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:298:2-298:208)
[Warning][Deadcode][CWE-571] condition '(long long )(Id_MCDC_135 / Id_MCDC_136) <= 4294967295LL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:298:2-298:208)
[Warning][Deadcode][CWE-571] condition '(int )Id_MCDC_150 < 4' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:377:4-377:55)
[Warning][Deadcode][CWE-571] condition '(int )Id_MCDC_150 < 4' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:377:4-377:55)
[Warning][Deadcode][CWE-570] condition '(int )Id_MCDC_150 < 4' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:377:4-377:55)
[Warning][Deadcode][CWE-570] condition 'Id_MCDC_111 < 2U' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:309:4-309:19)
[Warning][Deadcode][CWE-570] condition '! Id_MCDC_121' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:487:5-487:20)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_158 < 4U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:431:4-431:55)
[Warning][Deadcode][CWE-571] condition '(unsigned long )Id_MCDC_134 == (unsigned long )((void *)0)' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:223:4-223:33)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_158 < 4U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:431:4-431:55)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_137 != 0U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:295:7-295:23)
[Warning][Deadcode][CWE-571] condition '(long long )(Id_MCDC_135 / Id_MCDC_136) >= 0LL' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:298:2-298:208)
[Warning][Deadcode][CWE-571] condition '(long long )(Id_MCDC_135 / Id_MCDC_136) <= 4294967295LL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:298:2-298:208)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_141 <= 6147U' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:381:4-381:25)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_158 < 4U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:431:4-431:55)
[Warning][Deadcode][CWE-571] condition '(int )Id_MCDC_156 < 4' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:383:4-383:55)
[Warning][Deadcode][CWE-571] condition 'tmp != 0U' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:386:4-386:117)
[Warning][Deadcode][CWE-571] condition 'Id_MCDC_158 < 4U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:431:4-431:55)
[Warning][Deadcode][CWE-571] condition '(long long )(Id_MCDC_135 / Id_MCDC_136) >= 0LL' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:298:2-298:208)
[Warning][Deadcode][CWE-571] condition '(long long )(Id_MCDC_135 / Id_MCDC_136) <= 4294967295LL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:298:2-298:208)
[Warning][Deadcode][CWE-570] condition 'Id_MCDC_158 < 4U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:431:4-431:55)
[Warning][Deadcode][CWE-571] condition '(long long )(Id_MCDC_135 / Id_MCDC_136) >= 0LL' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:298:2-298:208)
[Warning][Deadcode][CWE-571] condition '(long long )(Id_MCDC_135 / Id_MCDC_136) <= 4294967295LL' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:298:2-298:208)
[Warning][Deadcode][CWE-571] condition '(int )Id_MCDC_150 < 4' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/loop-industry-pattern/ofuf_1.c:377:4-377:55)
SV-COMP result: true
[Info][Witness] witness generation summary:
  total generation entries: 1
