./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpv.2023-12-02_00-12-47.files/SV-COMP24_unreach-call/2SB.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpv.2023-12-02_00-12-47.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())) )
[Error][Analyzer] About to crash!

Fatal error: exception Failure("Yaml_unix.of_file: /mnt/goblint-svcomp/sv-comp/svcomp24-witnesses/results-verified/cpv.2023-12-02_00-12-47.files/SV-COMP24_unreach-call/2SB.yml/witness.yml: No such file or directory")
