./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/array-examples/data_structures_set_multi_proc_trivial_ground.i


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


[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/array-examples/data_structures_set_multi_proc_trivial_ground.i:22:3-24:3 with factor 25
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:33:2-36:2 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:40:5-42:5 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:47:2-50:2 with factor 8
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:56:7-58:7 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:62:5-64:5 with factor 12
[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] no thread creation -> disabling thread analyses "race, deadlock, maylocks, symb_locks, thread, threadid, threadJoins, threadreturn, mhp, region"
[Info] Enabled congruence domain.
[Info] Enabled octagon domain ONLY for:
[Info] __VERIFIER_assert, abort, i, count, tmp, key, a, count, j, k, size, i, i___0, j___0, a, top, expression, set, y, n, x, v, values, tmp, i, size, value, size, value, cond
[Info] Enabled widening thresholds
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! overflow) )
[Warning][Deadcode] Function 'reach_error' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:12:1-12:198)
[Warning][Deadcode] Function '__VERIFIER_assert' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:13:1-13:84)
[Warning][Deadcode] Function 'insert' is uncalled: 2 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:16:1-19:1)
[Warning][Deadcode] Function 'elem_exists' has dead code:
  on line 23 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:23-23)
[Warning][Deadcode] Function 'main' has dead code:
  on lines 40..41 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:40-41)
  on line 53 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:53-53)
  on lines 56..57 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:56-57)
  on lines 62..63 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:62-63)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 16
  dead: 12 (4 in uncalled functions)
  total lines: 28
[Warning][Deadcode][CWE-571] condition 'x < 100000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:33:6-33:29)
[Warning][Deadcode][CWE-571] condition 'x < 100000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:33:6-33:29)
[Warning][Deadcode][CWE-571] condition 'x < 100000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:33:6-33:29)
[Warning][Deadcode][CWE-571] condition 'x < 100000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:33:6-33:29)
[Warning][Deadcode][CWE-571] condition 'x < 100000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:33:6-33:29)
[Warning][Deadcode][CWE-571] condition 'v < 100000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:47:6-47:29)
[Warning][Deadcode][CWE-571] condition 'x < 100000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:33:6-33:29)
[Warning][Deadcode][CWE-571] condition 'v < 100000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:47:6-47:29)
[Warning][Deadcode][CWE-571] condition 'x < 100000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:33:6-33:29)
[Warning][Deadcode][CWE-571] condition 'v < 100000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:47:6-47:29)
[Warning][Deadcode][CWE-571] condition 'x < 100000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:33:6-33:29)
[Warning][Deadcode][CWE-571] condition 'v < 100000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:47:6-47:29)
[Warning][Deadcode][CWE-571] condition 'v < 100000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:47:6-47:29)
[Warning][Deadcode][CWE-571] condition 'v < 100000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:47:6-47:29)
[Warning][Deadcode][CWE-570] condition 'x < n' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:39:6-39:28)
[Warning][Deadcode][CWE-571] condition 'v < 100000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:47:6-47:29)
[Warning][Deadcode][CWE-570] condition 'i < size' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:22:7-22:32)
[Warning][Deadcode][CWE-571] condition 'v < 100000' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:47:6-47:29)
[Warning][Deadcode][CWE-570] condition 'x < n' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:61:7-61:29)
[Warning][Deadcode][CWE-570] condition 'tmp' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:52:10-52:47)
[Warning][Deadcode][CWE-570] condition 'x < n' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/array-examples/data_structures_set_multi_proc_trivial_ground.i:55:9-55:31)
SV-COMP result: true
[Info][Witness] witness generation summary:
  total generation entries: 1
