./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/2SB.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/symbiotic.2023-11-28_20-34-48.files/SV-COMP24_unreach-call/2SB.yml/witness.yml --sets ana.specification /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/properties/unreach-call.prp --sets exp.architecture 32bit /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.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/memory-model/2SB.i:83:3-83:39 with factor 12
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:180:3-187:6 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:188:3-195:4 with factor 3
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:207:3-213:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:216:3-222:3 with factor 4
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:260:3-272:3 with factor 5
[Info] unrolling loop at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:326:3-365:3 with factor 5
[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] function __VERIFIER_nondet_step uses mod, enable congruence domain recursively for:
[Info]   "down":
[Info]     __VERIFIER_nondet_uchar
[Info]   "up":
[Info]     main
[Info] function __VERIFIER_nondet_operations uses mod, enable congruence domain recursively for:
[Info]   "down":
[Info]     __VERIFIER_nondet_uchar
[Info]   "up":
[Info]     __VERIFIER_nondet_headerT
[Info]     randomise_input
[Info]     set_and_randomise_input
[Info]     main
[Info] function tso_core_write uses mod, enable congruence domain recursively for:
[Info]   "down":
[Info]   "up":
[Info]     main
[Info] function stepWriteBuffer uses mod, enable congruence domain recursively for:
[Info]   "down":
[Info]   "up":
[Info]     main
[Info] function check_buffer uses mod, enable congruence domain recursively for:
[Info]   "down":
[Info]   "up":
[Info]     tso_core_read
[Info]     main
[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] abort, __VERIFIER_nondet_headerT, i, count, tmp, key, a, count, j, k, size, i, i___0, j___0, a, top, expression, i, event_i0, event_i1, event_i2, event_i3, litmus_input, operations_total, tmp, user_action, global_time, wrbuffer, rd_address, data, response, checked, i, address, ch_tail, data, wrBuffer, data, user_action, global_time, user_action, wrBuffer, global_time, tail, i, wrBuffer, i, g_history, litmus_input, i, i___0, cpu0_operations, cpu1_operations, header, header___0, litmus_input, tmp, tmp, litmus_input, input_action, wrBuffer0, wrBuffer1, cpu0Writes_issued, cpu1Writes_issued, tmp___0, result
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] couldn't parse entry: find uuid
[Info][Unsound] Unknown value in {&g_history[0]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:88:3-88:25)
[Info][Unsound] Unknown value in {&wrBuffer0} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:89:3-89:30)
[Info][Unsound] Unknown value in {&wrBuffer1} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:90:3-90:30)
[Info][Unsound] Unknown value in {&litmus_input} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:92:3-92:41)
[Info][Unsound] Unknown value in {&litmus_input} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:198:3-198:45)
[Info][Unsound] Unknown value in {&litmus_input} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:199:3-199:32)
[Info][Unsound] Unknown value in {&litmus_input} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:200:3-200:45)
[Info][Unsound] Unknown value in {&wrBuffer1} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:161:9-161:50)
[Info][Unsound] Unknown value in {&wrBuffer1} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:149:13-149:91)
[Info][Unsound] Unknown value in {&g_history[0]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:149:13-149:91)
[Info][Unsound] Unknown value in {&wrBuffer1} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:282:7-282:55)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:288:3-288:20)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:150:13-150:37)
[Info][Unsound] Unknown value in {&g_history[0]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:144:13-144:66)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:240:3-240:20)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:145:13-145:37)
[Info][Unsound] Unknown value in {&wrBuffer1} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:138:13-138:78)
[Info][Unsound] Unknown value in {&g_history[0]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:138:13-138:78)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:234:3-234:20)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:139:13-139:37)
[Info][Unsound] Unknown value in {&wrBuffer0} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:130:9-130:50)
[Info][Unsound] Unknown value in {&wrBuffer0} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:118:13-118:91)
[Info][Unsound] Unknown value in {&g_history[0]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:118:13-118:91)
[Info][Unsound] Unknown value in {&wrBuffer0} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:282:7-282:55)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:119:13-119:37)
[Info][Unsound] Unknown value in {&g_history[0]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:113:13-113:66)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:114:13-114:37)
[Info][Unsound] Unknown value in {&wrBuffer0} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:107:13-107:78)
[Info][Unsound] Unknown value in {&g_history[0]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:107:13-107:78)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:108:13-108:37)
[Info][Unsound] Unknown value in {&g_history[0]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:174:5-174:45)
[Info][Unsound] Unknown value in {&g_history[0]} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:204:3-204:42)
[Warning][Deadcode] Function 'main' has dead code:
  on line 164 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:164-164)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 218
  dead: 1
  total lines: 219
[Warning][Deadcode][CWE-571] condition 'i___0 < 9' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:188:7-188:36)
[Warning][Deadcode][CWE-571] condition 'i___0 < cpu1_operations' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:189:9-189:28)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:153:20-153:24)
[Warning][Deadcode][CWE-571] condition 'i < 2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:216:6-216:28)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:156:18-156:22)
[Warning][Deadcode][CWE-571] condition 'event_i1 == -1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:338:16-342:31)
[Warning][Deadcode][CWE-570] condition 'i < 2' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:216:6-216:28)
[Warning][Deadcode][CWE-571] condition 'i___0 < 9' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:188:7-188:36)
[Warning][Deadcode][CWE-570] condition 'i___0 < cpu1_operations' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:189:9-189:28)
[Warning][Deadcode][CWE-571] condition 'event_i2 == -1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:347:16-352:31)
[Warning][Deadcode][CWE-571] condition 'event_i3 == -1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:357:16-361:31)
[Warning][Deadcode][CWE-570] condition 'i___0 < cpu1_operations' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:189:9-189:28)
[Warning][Deadcode][CWE-571] condition 'i < 9' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:326:7-326:35)
[Warning][Deadcode][CWE-571] condition 'i < 9' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:180:7-180:35)
[Warning][Deadcode][CWE-571] condition 'i < cpu0_operations' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:181:9-181:28)
[Warning][Deadcode][CWE-571] condition 'i < 9' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:326:7-326:35)
[Warning][Deadcode][CWE-571] condition '(unsigned int )tmp___0 == 3U' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:159:7-159:31)
[Warning][Deadcode][CWE-571] condition 'i < 9' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:180:7-180:35)
[Warning][Deadcode][CWE-571] condition 'i < cpu0_operations' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:181:9-181:28)
[Warning][Deadcode][CWE-571] condition 'i < 9' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:207:6-207:34)
[Warning][Deadcode][CWE-570] condition 'tmp >= 10U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:83:3-83:39)
[Warning][Deadcode][CWE-571] condition 'i < 9' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:180:7-180:35)
[Warning][Deadcode][CWE-571] condition 'i < 9' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:207:6-207:34)
[Warning][Deadcode][CWE-570] condition 'tmp >= 10U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:83:3-83:39)
[Warning][Deadcode][CWE-570] condition 'i < cpu0_operations' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:181:9-181:28)
[Warning][Deadcode][CWE-571] condition 'i < 2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:260:6-260:26)
[Warning][Deadcode][CWE-570] condition 'tmp >= 10U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:83:3-83:39)
[Warning][Deadcode][CWE-571] condition 'i < 9' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:207:6-207:34)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:122:20-122:24)
[Warning][Deadcode][CWE-570] condition 'tmp >= 10U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:83:3-83:39)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:125:18-125:22)
[Warning][Deadcode][CWE-570] condition 'tmp >= 10U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:83:3-83:39)
[Warning][Deadcode][CWE-571] condition 'i < 9' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:207:6-207:34)
[Warning][Deadcode][CWE-570] condition 'i < cpu0_operations' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:181:9-181:28)
[Warning][Deadcode][CWE-571] condition 'i < 2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:260:6-260:26)
[Warning][Deadcode][CWE-570] condition 'tmp >= 10U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:83:3-83:39)
[Warning][Deadcode][CWE-571] condition 'event_i1 != -1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:367:16-373:16)
[Warning][Deadcode][CWE-571] condition 'i < 9' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:326:7-326:35)
[Warning][Deadcode][CWE-571] condition 'event_i3 != -1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:367:16-373:16)
[Warning][Deadcode][CWE-570] condition 'tmp >= 10U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:83:3-83:39)
[Warning][Deadcode][CWE-571] condition '1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:367:16-373:16)
[Warning][Deadcode][CWE-571] condition 'i < 9' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:326:7-326:35)
[Warning][Deadcode][CWE-570] condition 'tmp >= 10U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:83:3-83:39)
[Warning][Deadcode][CWE-571] condition 'i___0 < 9' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:188:7-188:36)
[Warning][Deadcode][CWE-571] condition 'i < 9' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:326:7-326:35)
[Warning][Deadcode][CWE-571] condition 'i___0 < cpu1_operations' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:189:9-189:28)
[Warning][Deadcode][CWE-570] condition 'tmp >= 10U' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:83:3-83:39)
[Warning][Deadcode][CWE-570] condition 'i < 2' (possibly inserted by CIL) is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:260:6-260:26)
[Warning][Deadcode][CWE-571] condition 'event_i0 == -1' is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:328:16-333:31)
[Warning][Deadcode][CWE-571] condition 'i < 2' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:216:6-216:28)
[Warning][Deadcode][CWE-571] condition 'tmp >= 10U' (possibly inserted by CIL) is always true (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/memory-model/2SB.i:83:3-83:39)
[Info][Witness] witness validation summary:
  confirmed: 0
  unconfirmed: 0
  refuted: 0
  error: 1
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 1
SV-COMP result: ERROR (witness error)
