./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/benchexec/results/156-concurrency-fix-locations-all-locals/goblint.2024-03-01_08-44-30.files/SV-COMP24_unreach-call/twostage_3.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/benchexec/results/156-concurrency-fix-locations-all-locals/goblint.2024-03-01_08-44-30.files/SV-COMP24_unreach-call/twostage_3.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/pthread/twostage_3.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] Enabled congruence domain.
[Info] Enabled widening thresholds
[Info] Enabled octagon domain for:
[Info] fprintf, exit, i, key, count, a, tmp, count, i, j, i___0, j___0, k, size, r, top, err, lock___0, err, lock___0, err, i, argc, tPool, rPool, t1, t2, t1, __x, __x, __x
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] unassume invariant: (((4294967294LL - (long long )err) - (long long )i >= 0LL && (4294967295LL + (long long )err) - (long long )i >= 0LL) && (4294967295LL - (long long )err) + (long long )i >= 0LL) && (4294967296LL + (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1277:1-1328:1)
[Info][Witness] unassume invariant: (((((((((((4294967294LL - (long long )err) - (long long )i >= 0LL && (2147483650LL - (long long )argc) - (long long )err >= 0LL) && (2147483650LL - (long long )argc) - (long long )i >= 0LL) && (4294967295LL + (long long )err) - (long long )i >= 0LL) && (2147483646LL + (long long )argc) - (long long )err >= 0LL) && (2147483646LL + (long long )argc) - (long long )i >= 0LL) && (4294967295LL - (long long )err) + (long long )i >= 0LL) && (2147483651LL - (long long )argc) + (long long )err >= 0LL) && (2147483651LL - (long long )argc) + (long long )i >= 0LL) && (4294967296LL + (long long )err) + (long long )i >= 0LL) && (2147483647LL + (long long )argc) + (long long )err >= 0LL) && (2147483647LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1279:9-1279:18)
[Info][Witness] unassume invariant: (((argc != 1 && (4294967294LL - (long long )err) - (long long )i >= 0LL) && (4294967295LL + (long long )err) - (long long )i >= 0LL) && (4294967295LL - (long long )err) + (long long )i >= 0LL) && (4294967296LL + (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1279:9-1279:18)
[Info][Witness] unassume invariant: (((4294967294LL - (long long )err) - (long long )i >= 0LL && (4294967295LL + (long long )err) - (long long )i >= 0LL) && (4294967295LL - (long long )err) + (long long )i >= 0LL) && (4294967296LL + (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1280:13-1280:22)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )stderr (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1281:13-1281:62)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1281:13-1281:62)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1281:13-1281:62)
[Info][Witness] unassume invariant: ((((((((((((argc != 3 && argc != 1) && (4294967294LL - (long long )err) - (long long )i >= 0LL) && (4294967294LL - (long long )argc) - (long long )err >= 0LL) && (4294967294LL - (long long )argc) - (long long )i >= 0LL) && (4294967295LL + (long long )err) - (long long )i >= 0LL) && (4294967295LL + (long long )argc) - (long long )err >= 0LL) && (4294967295LL + (long long )argc) - (long long )i >= 0LL) && (4294967295LL - (long long )err) + (long long )i >= 0LL) && (4294967295LL - (long long )argc) + (long long )err >= 0LL) && (4294967295LL - (long long )argc) + (long long )i >= 0LL) && (4294967296LL + (long long )err) + (long long )i >= 0LL) && (4294967296LL + (long long )argc) + (long long )err >= 0LL) && (4294967296LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1281:13-1281:62)
[Info][Witness] unassume invariant: (((((((((((4294967294LL - (long long )err) - (long long )i >= 0LL && (2147483650LL - (long long )argc) - (long long )err >= 0LL) && (2147483650LL - (long long )argc) - (long long )i >= 0LL) && (4294967295LL + (long long )err) - (long long )i >= 0LL) && (2147483646LL + (long long )argc) - (long long )err >= 0LL) && (2147483646LL + (long long )argc) - (long long )i >= 0LL) && (4294967295LL - (long long )err) + (long long )i >= 0LL) && (2147483651LL - (long long )argc) + (long long )err >= 0LL) && (2147483651LL - (long long )argc) + (long long )i >= 0LL) && (4294967296LL + (long long )err) + (long long )i >= 0LL) && (2147483647LL + (long long )argc) + (long long )err >= 0LL) && (2147483647LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1282:13-1282:21)
[Info][Witness] unassume invariant: (((((((((((4294967294LL - (long long )err) - (long long )i >= 0LL && (2147483650LL - (long long )argc) - (long long )err >= 0LL) && (2147483650LL - (long long )argc) - (long long )i >= 0LL) && (4294967295LL + (long long )err) - (long long )i >= 0LL) && (2147483644LL + (long long )argc) - (long long )err >= 0LL) && (2147483644LL + (long long )argc) - (long long )i >= 0LL) && (4294967295LL - (long long )err) + (long long )i >= 0LL) && (2147483651LL - (long long )argc) + (long long )err >= 0LL) && (2147483651LL - (long long )argc) + (long long )i >= 0LL) && (4294967296LL + (long long )err) + (long long )i >= 0LL) && (2147483645LL + (long long )argc) + (long long )err >= 0LL) && (2147483645LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1280:13-1280:22)
[Info][Imprecise] Invalidating expressions: & iTThreads (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1284:13-1284:46)
[Info][Witness] unassume invariant: (((((((((((argc == 3 && (4294967294LL - (long long )err) - (long long )i >= 0LL) && (2147483650LL - (long long )argc) - (long long )err >= 0LL) && (2147483650LL - (long long )argc) - (long long )i >= 0LL) && (4294967295LL + (long long )err) - (long long )i >= 0LL) && (2147483644LL + (long long )argc) - (long long )err >= 0LL) && (2147483644LL + (long long )argc) - (long long )i >= 0LL) && (4294967295LL - (long long )err) + (long long )i >= 0LL) && (2147483651LL - (long long )argc) + (long long )err >= 0LL) && (2147483651LL - (long long )argc) + (long long )i >= 0LL) && (4294967296LL + (long long )err) + (long long )i >= 0LL) && (2147483645LL + (long long )argc) + (long long )err >= 0LL) && (2147483645LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1284:13-1284:46)
[Info][Imprecise] Invalidating expressions: & iRThreads (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1285:13-1285:46)
[Info][Witness] unassume invariant: (((((((((((4294967294LL - (long long )err) - (long long )i >= 0LL && (2147483650LL - (long long )argc) - (long long )err >= 0LL) && (2147483650LL - (long long )argc) - (long long )i >= 0LL) && (4294967295LL + (long long )err) - (long long )i >= 0LL) && (2147483646LL + (long long )argc) - (long long )err >= 0LL) && (2147483646LL + (long long )argc) - (long long )i >= 0LL) && (4294967295LL - (long long )err) + (long long )i >= 0LL) && (2147483651LL - (long long )argc) + (long long )err >= 0LL) && (2147483651LL - (long long )argc) + (long long )i >= 0LL) && (4294967296LL + (long long )err) + (long long )i >= 0LL) && (2147483647LL + (long long )argc) + (long long )err >= 0LL) && (2147483647LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1285:13-1285:46)
[Info][Witness] unassume invariant: (((((((((((4294967294LL - (long long )err) - (long long )i >= 0LL && (2147483650LL - (long long )argc) - (long long )err >= 0LL) && (2147483650LL - (long long )argc) - (long long )i >= 0LL) && (4294967295LL + (long long )err) - (long long )i >= 0LL) && (2147483646LL + (long long )argc) - (long long )err >= 0LL) && (2147483646LL + (long long )argc) - (long long )i >= 0LL) && (4294967295LL - (long long )err) + (long long )i >= 0LL) && (2147483651LL - (long long )argc) + (long long )err >= 0LL) && (2147483651LL - (long long )argc) + (long long )i >= 0LL) && (4294967296LL + (long long )err) + (long long )i >= 0LL) && (2147483647LL + (long long )argc) + (long long )err >= 0LL) && (2147483647LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1288:9-1288:49)
[Info][Witness] unassume invariant: (((((((((((4294967294LL - (long long )err) - (long long )i >= 0LL && (2147483650LL - (long long )argc) - (long long )err >= 0LL) && (2147483650LL - (long long )argc) - (long long )i >= 0LL) && (4294967295LL + (long long )err) - (long long )i >= 0LL) && (2147483646LL + (long long )argc) - (long long )err >= 0LL) && (2147483646LL + (long long )argc) - (long long )i >= 0LL) && (4294967295LL - (long long )err) + (long long )i >= 0LL) && (2147483651LL - (long long )argc) + (long long )err >= 0LL) && (2147483651LL - (long long )argc) + (long long )i >= 0LL) && (4294967296LL + (long long )err) + (long long )i >= 0LL) && (2147483647LL + (long long )argc) + (long long )err >= 0LL) && (2147483647LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1288:9-1288:49)
[Info][Witness] unassume invariant: (((((((((((4294967294LL - (long long )err) - (long long )i >= 0LL && (2147483650LL - (long long )argc) - (long long )err >= 0LL) && (2147483650LL - (long long )argc) - (long long )i >= 0LL) && (4294967295LL + (long long )err) - (long long )i >= 0LL) && (2147483646LL + (long long )argc) - (long long )err >= 0LL) && (2147483646LL + (long long )argc) - (long long )i >= 0LL) && (4294967295LL - (long long )err) + (long long )i >= 0LL) && (2147483651LL - (long long )argc) + (long long )err >= 0LL) && (2147483651LL - (long long )argc) + (long long )i >= 0LL) && (4294967296LL + (long long )err) + (long long )i >= 0LL) && (2147483647LL + (long long )argc) + (long long )err >= 0LL) && (2147483647LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1289:7-1289:15)
[Info][Witness] unassume invariant: (((((((((((4294967294LL - (long long )err) - (long long )i >= 0LL && (2147483650LL - (long long )argc) - (long long )err >= 0LL) && (2147483650LL - (long long )argc) - (long long )i >= 0LL) && (4294967295LL + (long long )err) - (long long )i >= 0LL) && (2147483646LL + (long long )argc) - (long long )err >= 0LL) && (2147483646LL + (long long )argc) - (long long )i >= 0LL) && (4294967295LL - (long long )err) + (long long )i >= 0LL) && (2147483651LL - (long long )argc) + (long long )err >= 0LL) && (2147483651LL - (long long )argc) + (long long )i >= 0LL) && (4294967296LL + (long long )err) + (long long )i >= 0LL) && (2147483647LL + (long long )argc) + (long long )err >= 0LL) && (2147483647LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1291:5-1291:68)
[Info][Witness] unassume invariant: (((((((((((4294967294LL - (long long )err) - (long long )i >= 0LL && (2147483650LL - (long long )argc) - (long long )err >= 0LL) && (2147483650LL - (long long )argc) - (long long )i >= 0LL) && (4294967295LL + (long long )err) - (long long )i >= 0LL) && (2147483646LL + (long long )argc) - (long long )err >= 0LL) && (2147483646LL + (long long )argc) - (long long )i >= 0LL) && (4294967295LL - (long long )err) + (long long )i >= 0LL) && (2147483651LL - (long long )argc) + (long long )err >= 0LL) && (2147483651LL - (long long )argc) + (long long )i >= 0LL) && (4294967296LL + (long long )err) + (long long )i >= 0LL) && (2147483647LL + (long long )argc) + (long long )err >= 0LL) && (2147483647LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1292:5-1292:68)
[Info][Imprecise] Invalidating expressions: & err (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1293:9-1293:64)
[Info][Witness] unassume invariant: (((((((((((4294967294LL - (long long )err) - (long long )i >= 0LL && (2147483650LL - (long long )argc) - (long long )err >= 0LL) && (2147483650LL - (long long )argc) - (long long )i >= 0LL) && (4294967295LL + (long long )err) - (long long )i >= 0LL) && (2147483646LL + (long long )argc) - (long long )err >= 0LL) && (2147483646LL + (long long )argc) - (long long )i >= 0LL) && (4294967295LL - (long long )err) + (long long )i >= 0LL) && (2147483651LL - (long long )argc) + (long long )err >= 0LL) && (2147483651LL - (long long )argc) + (long long )i >= 0LL) && (4294967296LL + (long long )err) + (long long )i >= 0LL) && (2147483647LL + (long long )argc) + (long long )err >= 0LL) && (2147483647LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1293:9-1293:64)
[Info][Witness] unassume invariant: ((((((((((((2147483647LL + (long long )argc) + (long long )err >= 0LL && (4294967296LL + (long long )err) + (long long )i >= 0LL) && (2147483651LL - (long long )argc) + (long long )err >= 0LL) && (4294967295LL - (long long )err) + (long long )i >= 0LL) && (2147483646LL + (long long )argc) - (long long )err >= 0LL) && (4294967295LL + (long long )err) - (long long )i >= 0LL) && (2147483650LL - (long long )argc) - (long long )err >= 0LL) && (4294967294LL - (long long )err) - (long long )i >= 0LL) || ((((((((-1LL + (long long )argc) + (long long )err >= 0LL && (2147483648LL + (long long )err) + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )err >= 0LL) && (2147483648LL - (long long )err) + (long long )i >= 0LL) && (-1LL + (long long )argc) - (long long )err >= 0LL) && (2147483647LL + (long long )err) - (long long )i >= 0LL) && (3LL - (long long )argc) - (long long )err >= 0LL) && (2147483647LL - (long long )err) - (long long )i >= 0LL)) && (2147483650LL - (long long )argc) - (long long )i >= 0LL) && (2147483646LL + (long long )argc) - (long long )i >= 0LL) && (2147483651LL - (long long )argc) + (long long )i >= 0LL) && (2147483647LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1293:9-1293:64)
[Info][Witness] unassume invariant: (((((((((((err != 0 && (4294967294LL - (long long )err) - (long long )i >= 0LL) && (2147483650LL - (long long )argc) - (long long )err >= 0LL) && (2147483650LL - (long long )argc) - (long long )i >= 0LL) && (4294967295LL + (long long )err) - (long long )i >= 0LL) && (2147483646LL + (long long )argc) - (long long )err >= 0LL) && (2147483646LL + (long long )argc) - (long long )i >= 0LL) && (4294967295LL - (long long )err) + (long long )i >= 0LL) && (2147483651LL - (long long )argc) + (long long )err >= 0LL) && (2147483651LL - (long long )argc) + (long long )i >= 0LL) && (4294967296LL + (long long )err) + (long long )i >= 0LL) && (2147483647LL + (long long )argc) + (long long )err >= 0LL) && (2147483647LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1293:9-1293:64)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )stderr (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1294:9-1294:63)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1294:9-1294:63)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1294:9-1294:63)
[Info][Witness] unassume invariant: (((((((((((err != 0 && (4294967294LL - (long long )err) - (long long )i >= 0LL) && (4294967294LL - (long long )argc) - (long long )err >= 0LL) && (4294967294LL - (long long )argc) - (long long )i >= 0LL) && (4294967295LL + (long long )err) - (long long )i >= 0LL) && (4294967295LL + (long long )argc) - (long long )err >= 0LL) && (4294967295LL + (long long )argc) - (long long )i >= 0LL) && (4294967295LL - (long long )err) + (long long )i >= 0LL) && (4294967295LL - (long long )argc) + (long long )err >= 0LL) && (4294967295LL - (long long )argc) + (long long )i >= 0LL) && (4294967296LL + (long long )err) + (long long )i >= 0LL) && (4294967296LL + (long long )argc) + (long long )err >= 0LL) && (4294967296LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1294:9-1294:63)
[Info][Witness] unassume invariant: ((((((((((((2147483647LL + (long long )argc) + (long long )err >= 0LL && (4294967296LL + (long long )err) + (long long )i >= 0LL) && (2147483651LL - (long long )argc) + (long long )err >= 0LL) && (4294967295LL - (long long )err) + (long long )i >= 0LL) && (2147483646LL + (long long )argc) - (long long )err >= 0LL) && (4294967295LL + (long long )err) - (long long )i >= 0LL) && (2147483650LL - (long long )argc) - (long long )err >= 0LL) && (4294967294LL - (long long )err) - (long long )i >= 0LL) || ((((((((-1LL + (long long )argc) + (long long )err >= 0LL && (2147483648LL + (long long )err) + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )err >= 0LL) && (2147483648LL - (long long )err) + (long long )i >= 0LL) && (-1LL + (long long )argc) - (long long )err >= 0LL) && (2147483647LL + (long long )err) - (long long )i >= 0LL) && (3LL - (long long )argc) - (long long )err >= 0LL) && (2147483647LL - (long long )err) - (long long )i >= 0LL)) && (2147483650LL - (long long )argc) - (long long )i >= 0LL) && (2147483646LL + (long long )argc) - (long long )i >= 0LL) && (2147483651LL - (long long )argc) + (long long )i >= 0LL) && (2147483647LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1295:9-1295:17)
[Info][Imprecise] Invalidating expressions: & err (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1297:9-1297:64)
[Info][Witness] unassume invariant: ((((((((((((2147483647LL + (long long )argc) + (long long )err >= 0LL && (4294967296LL + (long long )err) + (long long )i >= 0LL) && (2147483651LL - (long long )argc) + (long long )err >= 0LL) && (4294967295LL - (long long )err) + (long long )i >= 0LL) && (2147483646LL + (long long )argc) - (long long )err >= 0LL) && (4294967295LL + (long long )err) - (long long )i >= 0LL) && (2147483650LL - (long long )argc) - (long long )err >= 0LL) && (4294967294LL - (long long )err) - (long long )i >= 0LL) || ((((((((-1LL + (long long )argc) + (long long )err >= 0LL && (2147483648LL + (long long )err) + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )err >= 0LL) && (2147483648LL - (long long )err) + (long long )i >= 0LL) && (-1LL + (long long )argc) - (long long )err >= 0LL) && (2147483647LL + (long long )err) - (long long )i >= 0LL) && (3LL - (long long )argc) - (long long )err >= 0LL) && (2147483647LL - (long long )err) - (long long )i >= 0LL)) && (2147483650LL - (long long )argc) - (long long )i >= 0LL) && (2147483646LL + (long long )argc) - (long long )i >= 0LL) && (2147483651LL - (long long )argc) + (long long )i >= 0LL) && (2147483647LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1297:9-1297:64)
[Info][Witness] unassume invariant: (((((((((((2147483650LL - (long long )argc) - (long long )i >= 0LL && (2147483647LL - (long long )err) - (long long )i >= 0LL) && (3LL - (long long )argc) - (long long )err >= 0LL) && (2147483647LL + (long long )err) - (long long )i >= 0LL) && (2147483646LL + (long long )argc) - (long long )i >= 0LL) && (-1LL + (long long )argc) - (long long )err >= 0LL) && (2147483651LL - (long long )argc) + (long long )i >= 0LL) && (2147483648LL - (long long )err) + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )err >= 0LL) && (2147483648LL + (long long )err) + (long long )i >= 0LL) && (2147483647LL + (long long )argc) + (long long )i >= 0LL) && (-1LL + (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1297:9-1297:64)
[Info][Witness] unassume invariant: (((((((((((err != 0 && (4294967294LL - (long long )err) - (long long )i >= 0LL) && (2147483650LL - (long long )argc) - (long long )err >= 0LL) && (2147483650LL - (long long )argc) - (long long )i >= 0LL) && (4294967295LL + (long long )err) - (long long )i >= 0LL) && (2147483646LL + (long long )argc) - (long long )err >= 0LL) && (2147483646LL + (long long )argc) - (long long )i >= 0LL) && (4294967295LL - (long long )err) + (long long )i >= 0LL) && (2147483651LL - (long long )argc) + (long long )err >= 0LL) && (2147483651LL - (long long )argc) + (long long )i >= 0LL) && (4294967296LL + (long long )err) + (long long )i >= 0LL) && (2147483647LL + (long long )argc) + (long long )err >= 0LL) && (2147483647LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1297:9-1297:64)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )stderr (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1298:9-1298:63)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1298:9-1298:63)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1298:9-1298:63)
[Info][Witness] unassume invariant: (((((((((((err != 0 && (4294967294LL - (long long )err) - (long long )i >= 0LL) && (4294967294LL - (long long )argc) - (long long )err >= 0LL) && (4294967294LL - (long long )argc) - (long long )i >= 0LL) && (4294967295LL + (long long )err) - (long long )i >= 0LL) && (4294967295LL + (long long )argc) - (long long )err >= 0LL) && (4294967295LL + (long long )argc) - (long long )i >= 0LL) && (4294967295LL - (long long )err) + (long long )i >= 0LL) && (4294967295LL - (long long )argc) + (long long )err >= 0LL) && (4294967295LL - (long long )argc) + (long long )i >= 0LL) && (4294967296LL + (long long )err) + (long long )i >= 0LL) && (4294967296LL + (long long )argc) + (long long )err >= 0LL) && (4294967296LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1298:9-1298:63)
[Info][Witness] unassume invariant: (((((((((((2147483650LL - (long long )argc) - (long long )i >= 0LL && (2147483647LL - (long long )err) - (long long )i >= 0LL) && (3LL - (long long )argc) - (long long )err >= 0LL) && (2147483647LL + (long long )err) - (long long )i >= 0LL) && (2147483646LL + (long long )argc) - (long long )i >= 0LL) && (-1LL + (long long )argc) - (long long )err >= 0LL) && (2147483651LL - (long long )argc) + (long long )i >= 0LL) && (2147483648LL - (long long )err) + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )err >= 0LL) && (2147483648LL + (long long )err) + (long long )i >= 0LL) && (2147483647LL + (long long )argc) + (long long )i >= 0LL) && (-1LL + (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1299:9-1299:17)
[Info][Witness] unassume invariant: ((((((((((((((((((((((-1LL + (long long )argc) + (long long )i >= 0LL && (0LL - (long long )err) + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )i >= 0LL) && (long long )err + (long long )i >= 0LL) && (-1LL + (long long )argc) - (long long )i >= 0LL) && (0LL - (long long )err) - (long long )i >= 0LL) && (3LL - (long long )argc) - (long long )i >= 0LL) && (long long )err - (long long )i >= 0LL) && 0 == i) && i == 0) || (((((1 <= i && i <= 100000) && (-2LL + (long long )argc) + (long long )i >= 0LL) && (-1LL + (long long )err) + (long long )i >= 0LL) && (-1LL - (long long )err) + (long long )i >= 0LL) && (2LL - (long long )argc) + (long long )i >= 0LL)) && (argc == 1 || argc == 3)) && argc != 0) && argc % 2 == 1) && err == 0) && (3LL - (long long )argc) - (long long )err >= 0LL) && (-1LL + (long long )argc) - (long long )err >= 0LL) && (3LL - (long long )argc) + (long long )err >= 0LL) && (-1LL + (long long )argc) + (long long )err >= 0LL) && argc <= 127) && argc <= 3) && 1 <= argc) && 0 <= argc (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1303:9-1303:35)
[Info][Witness] unassume invariant: ((((((((-1LL + (long long )argc) + (long long )i >= 0LL && (2147483647LL + (long long )argc) + (long long )err >= 0LL) && (2147483648LL + (long long )err) + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )i >= 0LL) && (2147483647LL - (long long )err) + (long long )i >= 0LL) && (2147483651LL - (long long )argc) + (long long )err >= 0LL) && (2147483646LL + (long long )argc) - (long long )err >= 0LL) && (2147483650LL - (long long )argc) - (long long )err >= 0LL) || (((((-1LL + (long long )argc) + (long long )err >= 0LL && (3LL - (long long )argc) + (long long )err >= 0LL) && (-1LL + (long long )argc) - (long long )err >= 0LL) && (3LL - (long long )argc) - (long long )err >= 0LL) && (((((((((((-1LL + (long long )argc) + (long long )i >= 0LL && (0LL - (long long )err) + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )i >= 0LL) && (long long )err + (long long )i >= 0LL) && (-1LL + (long long )argc) - (long long )i >= 0LL) && (0LL - (long long )err) - (long long )i >= 0LL) && (3LL - (long long )argc) - (long long )i >= 0LL) && (long long )err - (long long )i >= 0LL) && 0 == i) && i == 0) || ((((((1 <= i && i <= 99999) && (-2LL + (long long )argc) + (long long )i >= 0LL) && (-1LL + (long long )err) + (long long )i >= 0LL) && (-1LL - (long long )err) + (long long )i >= 0LL) && (2LL - (long long )argc) + (long long )i >= 0LL) && i != 0))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1303:9-1303:35)
[Info][Imprecise] Invalidating expressions: & err (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1304:13-1304:85)
[Info][Witness] unassume invariant: ((((((((-1LL + (long long )argc) + (long long )i >= 0LL && (2147483647LL + (long long )argc) + (long long )err >= 0LL) && (2147483648LL + (long long )err) + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )i >= 0LL) && (2147483647LL - (long long )err) + (long long )i >= 0LL) && (2147483651LL - (long long )argc) + (long long )err >= 0LL) && (2147483646LL + (long long )argc) - (long long )err >= 0LL) && (2147483650LL - (long long )argc) - (long long )err >= 0LL) || (((((-1LL + (long long )argc) + (long long )err >= 0LL && (3LL - (long long )argc) + (long long )err >= 0LL) && (-1LL + (long long )argc) - (long long )err >= 0LL) && (3LL - (long long )argc) - (long long )err >= 0LL) && (((((((((((-1LL + (long long )argc) + (long long )i >= 0LL && (0LL - (long long )err) + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )i >= 0LL) && (long long )err + (long long )i >= 0LL) && (-1LL + (long long )argc) - (long long )i >= 0LL) && (0LL - (long long )err) - (long long )i >= 0LL) && (3LL - (long long )argc) - (long long )i >= 0LL) && (long long )err - (long long )i >= 0LL) && 0 == i) && i == 0) || ((((((1 <= i && i <= 99999) && (-2LL + (long long )argc) + (long long )i >= 0LL) && (-1LL + (long long )err) + (long long )i >= 0LL) && (-1LL - (long long )err) + (long long )i >= 0LL) && (2LL - (long long )argc) + (long long )i >= 0LL) && i != 0))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1304:13-1304:85)
[Info][Witness] unassume invariant: t1 == -1 && -1 == t1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1245:9-1245:16)
[Info][Witness] unassume invariant: -1 == t1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1246:5-1246:34)
[Info][Witness] unassume invariant: -1 == t1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1247:5-1247:19)
[Info][Witness] unassume invariant: -1 == t1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1248:5-1248:36)
[Warning][Unknown] unlocking mutex ((alloc@sid:60@tid:[main])) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1248:5-1248:36)
[Info][Witness] unassume invariant: -1 == t1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1249:5-1249:34)
[Info][Witness] unassume invariant: ((t1 == 0 || t1 == 1) && t1 <= 1) && 0 <= t1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1250:5-1250:20)
[Warning][Unknown] unlocking mutex ((alloc@sid:60@tid:[main])) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1251:5-1251:36)
[Info][Witness] unassume invariant: ((t1 == 0 || t1 == 1) && t1 <= 1) && 0 <= t1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1252:5-1252:34)
[Warning][Unknown] unlocking mutex ((alloc@sid:62@tid:[main])) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1254:5-1254:36)
[Info][Witness] unassume invariant: (((((((err != 0 && (2147483650LL - (long long )argc) - (long long )err >= 0LL) && (2147483646LL + (long long )argc) - (long long )err >= 0LL) && (2147483651LL - (long long )argc) + (long long )err >= 0LL) && (2147483647LL - (long long )err) + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )i >= 0LL) && (2147483648LL + (long long )err) + (long long )i >= 0LL) && (2147483647LL + (long long )argc) + (long long )err >= 0LL) && (-1LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1304:13-1304:85)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )stderr (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1305:13-1305:79)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1305:13-1305:79)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1305:13-1305:79)
[Info][Witness] unassume invariant: (((((((((((err != 0 && (4294967294LL - (long long )err) - (long long )i >= 0LL) && (4294967294LL - (long long )argc) - (long long )err >= 0LL) && (4294967294LL - (long long )argc) - (long long )i >= 0LL) && (4294967295LL + (long long )err) - (long long )i >= 0LL) && (4294967295LL + (long long )argc) - (long long )err >= 0LL) && (4294967295LL + (long long )argc) - (long long )i >= 0LL) && (4294967295LL - (long long )err) + (long long )i >= 0LL) && (4294967295LL - (long long )argc) + (long long )err >= 0LL) && (4294967295LL - (long long )argc) + (long long )i >= 0LL) && (4294967296LL + (long long )err) + (long long )i >= 0LL) && (4294967296LL + (long long )argc) + (long long )err >= 0LL) && (4294967296LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1305:13-1305:79)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1305:13-1305:79)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1303:9-1303:35)
[Info][Witness] unassume invariant: ((((((((((((((((((((((-1LL + (long long )argc) + (long long )i >= 0LL && (0LL - (long long )err) + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )i >= 0LL) && (long long )err + (long long )i >= 0LL) && (-1LL + (long long )argc) - (long long )i >= 0LL) && (0LL - (long long )err) - (long long )i >= 0LL) && (3LL - (long long )argc) - (long long )i >= 0LL) && (long long )err - (long long )i >= 0LL) && 0 == i) && i == 0) || (((((1 <= i && i <= 100000) && (-2LL + (long long )argc) + (long long )i >= 0LL) && (-1LL + (long long )err) + (long long )i >= 0LL) && (-1LL - (long long )err) + (long long )i >= 0LL) && (2LL - (long long )argc) + (long long )i >= 0LL)) && (argc == 1 || argc == 3)) && argc != 0) && argc % 2 == 1) && err == 0) && (3LL - (long long )argc) - (long long )err >= 0LL) && (-1LL + (long long )argc) - (long long )err >= 0LL) && (3LL - (long long )argc) + (long long )err >= 0LL) && (-1LL + (long long )argc) + (long long )err >= 0LL) && argc <= 127) && argc <= 3) && 1 <= argc) && 0 <= argc (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1303:9-1303:35)
[Info][Witness] unassume invariant: ((((((((((((((-1LL + (long long )argc) + (long long )i >= 0LL && (0LL - (long long )err) + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )i >= 0LL) && (long long )err + (long long )i >= 0LL) && (-1LL + (long long )argc) - (long long )i >= 0LL) && (0LL - (long long )err) - (long long )i >= 0LL) && (3LL - (long long )argc) - (long long )i >= 0LL) && (long long )err - (long long )i >= 0LL) && 0 == i) && i == 0) || ((((((1 <= i && i <= 100000) && (-2LL + (long long )argc) + (long long )i >= 0LL) && (-1LL + (long long )err) + (long long )i >= 0LL) && (-1LL - (long long )err) + (long long )i >= 0LL) && (2LL - (long long )argc) + (long long )i >= 0LL) && i != 0)) && (3LL - (long long )argc) - (long long )err >= 0LL) && (-1LL + (long long )argc) - (long long )err >= 0LL) && (3LL - (long long )argc) + (long long )err >= 0LL) && (-1LL + (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1303:9-1303:35)
[Info][Witness] unassume invariant: ((((((((((((((((((((((-1LL + (long long )argc) - (long long )i >= 0LL && (0LL - (long long )err) - (long long )i >= 0LL) && (3LL - (long long )argc) - (long long )i >= 0LL) && (long long )err - (long long )i >= 0LL) && 0 == i) && i == 0) || (0 <= i && i <= 100000)) && (argc == 1 || argc == 3)) && argc != 0) && argc % 2 == 1) && err == 0) && (3LL - (long long )argc) - (long long )err >= 0LL) && (-1LL + (long long )argc) - (long long )err >= 0LL) && (long long )err + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )err >= 0LL) && (3LL - (long long )argc) + (long long )i >= 0LL) && (0LL - (long long )err) + (long long )i >= 0LL) && (-1LL + (long long )argc) + (long long )err >= 0LL) && (-1LL + (long long )argc) + (long long )i >= 0LL) && argc <= 127) && argc <= 3) && 1 <= argc) && 0 <= argc (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1309:9-1309:35)
[Info][Witness] unassume invariant: ((((((((2147483647LL + (long long )argc) + (long long )err >= 0LL && (2147483648LL + (long long )err) + (long long )i >= 0LL) && (2147483647LL - (long long )err) + (long long )i >= 0LL) && (2147483651LL - (long long )argc) + (long long )err >= 0LL) && (2147483646LL + (long long )argc) - (long long )err >= 0LL) && (2147483650LL - (long long )argc) - (long long )err >= 0LL) || (((((((-1LL + (long long )argc) + (long long )err >= 0LL && (0LL - (long long )err) + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )err >= 0LL) && (long long )err + (long long )i >= 0LL) && (-1LL + (long long )argc) - (long long )err >= 0LL) && (3LL - (long long )argc) - (long long )err >= 0LL) && (((((((-1LL + (long long )argc) - (long long )i >= 0LL && (0LL - (long long )err) - (long long )i >= 0LL) && (3LL - (long long )argc) - (long long )i >= 0LL) && (long long )err - (long long )i >= 0LL) && 0 == i) && i == 0) || (0 <= i && i <= 99999)))) && (3LL - (long long )argc) + (long long )i >= 0LL) && (-1LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1309:9-1309:35)
[Info][Imprecise] Invalidating expressions: & err (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1310:13-1310:85)
[Info][Witness] unassume invariant: ((((((((2147483647LL + (long long )argc) + (long long )err >= 0LL && (2147483648LL + (long long )err) + (long long )i >= 0LL) && (2147483647LL - (long long )err) + (long long )i >= 0LL) && (2147483651LL - (long long )argc) + (long long )err >= 0LL) && (2147483646LL + (long long )argc) - (long long )err >= 0LL) && (2147483650LL - (long long )argc) - (long long )err >= 0LL) || (((((((-1LL + (long long )argc) + (long long )err >= 0LL && (0LL - (long long )err) + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )err >= 0LL) && (long long )err + (long long )i >= 0LL) && (-1LL + (long long )argc) - (long long )err >= 0LL) && (3LL - (long long )argc) - (long long )err >= 0LL) && (((((((-1LL + (long long )argc) - (long long )i >= 0LL && (0LL - (long long )err) - (long long )i >= 0LL) && (3LL - (long long )argc) - (long long )i >= 0LL) && (long long )err - (long long )i >= 0LL) && 0 == i) && i == 0) || (0 <= i && i <= 99999)))) && (3LL - (long long )argc) + (long long )i >= 0LL) && (-1LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1310:13-1310:85)
[Info][Witness] unassume invariant: (((4294967294LL - (long long )t1) - (long long )t2 >= 0LL && (4294967295LL + (long long )t1) - (long long )t2 >= 0LL) && (4294967295LL - (long long )t1) + (long long )t2 >= 0LL) && (4294967296LL + (long long )t1) + (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1257:1-1276:1)
[Info][Witness] unassume invariant: ((((t1 == -1 && -1 == t1) && (2147483646LL - (long long )t1) - (long long )t2 >= 0LL) && (2147483648LL + (long long )t1) - (long long )t2 >= 0LL) && (2147483647LL - (long long )t1) + (long long )t2 >= 0LL) && (2147483649LL + (long long )t1) + (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1258:9-1258:16)
[Info][Witness] unassume invariant: ((((((t2 == -1 && t1 == t2) && -1 == t2) && -1 == t1) && (long long )t1 - (long long )t2 >= 0LL) && (-2LL - (long long )t1) - (long long )t2 >= 0LL) && (0LL - (long long )t1) + (long long )t2 >= 0LL) && (2LL + (long long )t1) + (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1259:9-1259:16)
[Info][Witness] unassume invariant: (((((t1 == t2 && -1 == t2) && -1 == t1) && (long long )t1 - (long long )t2 >= 0LL) && (-2LL - (long long )t1) - (long long )t2 >= 0LL) && (0LL - (long long )t1) + (long long )t2 >= 0LL) && (2LL + (long long )t1) + (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1260:5-1260:34)
[Info][Witness] unassume invariant: (((((t1 == t2 && -1 == t2) && -1 == t1) && (long long )t1 - (long long )t2 >= 0LL) && (-2LL - (long long )t1) - (long long )t2 >= 0LL) && (0LL - (long long )t1) + (long long )t2 >= 0LL) && (2LL + (long long )t1) + (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1261:9-1261:24)
[Info][Witness] unassume invariant: (((((t1 == t2 && -1 == t2) && -1 == t1) && (long long )t1 - (long long )t2 >= 0LL) && (-2LL - (long long )t1) - (long long )t2 >= 0LL) && (0LL - (long long )t1) + (long long )t2 >= 0LL) && (2LL + (long long )t1) + (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1262:9-1262:40)
[Warning][Unknown] unlocking mutex ((alloc@sid:60@tid:[main])) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1262:9-1262:40)
[Info][Witness] unassume invariant: (((t1 == 0 || t1 == 1) && -1 == t2) && t1 <= 1) && 0 <= t1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1265:5-1265:20)
[Info][Witness] unassume invariant: -1 == t2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1266:5-1266:36)
[Warning][Unknown] unlocking mutex ((alloc@sid:60@tid:[main])) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1266:5-1266:36)
[Info][Witness] unassume invariant: -1 == t2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1267:5-1267:34)
[Info][Witness] unassume invariant: (t2 <= 255 && t2 <= 2) && 0 <= t2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1268:5-1268:20)
[Info][Witness] unassume invariant: (((((t1 == 0 || t1 == 1) && t2 <= 255) && t2 <= 2) && t1 <= 1) && 0 <= t2) && 0 <= t1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1269:5-1269:36)
[Warning][Unknown] unlocking mutex ((alloc@sid:62@tid:[main])) which may not be held (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1269:5-1269:36)
[Info][Witness] unassume invariant: (1LL + (long long )t1) - (long long )t2 >= 0LL && (-1LL - (long long )t1) + (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1270:9-1270:23)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )stderr (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1271:9-1271:40)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1271:9-1271:40)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1271:9-1271:40)
[Info][Witness] unassume invariant: (((4294967294LL - (long long )t1) - (long long )t2 >= 0LL && (4294967295LL + (long long )t1) - (long long )t2 >= 0LL) && (4294967295LL - (long long )t1) + (long long )t2 >= 0LL) && (4294967296LL + (long long )t1) + (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1271:9-1271:40)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1271:9-1271:40)
[Info][Witness] unassume invariant: (((((((err != 0 && (2147483650LL - (long long )argc) - (long long )err >= 0LL) && (2147483646LL + (long long )argc) - (long long )err >= 0LL) && (2147483651LL - (long long )argc) + (long long )err >= 0LL) && (2147483647LL - (long long )err) + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )i >= 0LL) && (2147483648LL + (long long )err) + (long long )i >= 0LL) && (2147483647LL + (long long )argc) + (long long )err >= 0LL) && (-1LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1310:13-1310:85)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )stderr (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1311:13-1311:77)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1311:13-1311:77)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1311:13-1311:77)
[Info][Witness] unassume invariant: (((((((((((err != 0 && (4294967294LL - (long long )err) - (long long )i >= 0LL) && (4294967294LL - (long long )argc) - (long long )err >= 0LL) && (4294967294LL - (long long )argc) - (long long )i >= 0LL) && (4294967295LL + (long long )err) - (long long )i >= 0LL) && (4294967295LL + (long long )argc) - (long long )err >= 0LL) && (4294967295LL + (long long )argc) - (long long )i >= 0LL) && (4294967295LL - (long long )err) + (long long )i >= 0LL) && (4294967295LL - (long long )argc) + (long long )err >= 0LL) && (4294967295LL - (long long )argc) + (long long )i >= 0LL) && (4294967296LL + (long long )err) + (long long )i >= 0LL) && (4294967296LL + (long long )argc) + (long long )err >= 0LL) && (4294967296LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1311:13-1311:77)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1311:13-1311:77)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1309:9-1309:35)
[Info][Witness] unassume invariant: ((((((((((((((((((((((-1LL + (long long )argc) - (long long )i >= 0LL && (0LL - (long long )err) - (long long )i >= 0LL) && (3LL - (long long )argc) - (long long )i >= 0LL) && (long long )err - (long long )i >= 0LL) && 0 == i) && i == 0) || (0 <= i && i <= 100000)) && (argc == 1 || argc == 3)) && argc != 0) && argc % 2 == 1) && err == 0) && (3LL - (long long )argc) - (long long )err >= 0LL) && (-1LL + (long long )argc) - (long long )err >= 0LL) && (long long )err + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )err >= 0LL) && (3LL - (long long )argc) + (long long )i >= 0LL) && (0LL - (long long )err) + (long long )i >= 0LL) && (-1LL + (long long )argc) + (long long )err >= 0LL) && (-1LL + (long long )argc) + (long long )i >= 0LL) && argc <= 127) && argc <= 3) && 1 <= argc) && 0 <= argc (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1309:9-1309:35)
[Info][Witness] unassume invariant: ((((((((((((((-1LL + (long long )argc) - (long long )i >= 0LL && (0LL - (long long )err) - (long long )i >= 0LL) && (3LL - (long long )argc) - (long long )i >= 0LL) && (long long )err - (long long )i >= 0LL) && 0 == i) && i == 0) || (0 <= i && i <= 100000)) && (3LL - (long long )argc) - (long long )err >= 0LL) && (-1LL + (long long )argc) - (long long )err >= 0LL) && (long long )err + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )err >= 0LL) && (3LL - (long long )argc) + (long long )i >= 0LL) && (0LL - (long long )err) + (long long )i >= 0LL) && (-1LL + (long long )argc) + (long long )err >= 0LL) && (-1LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1309:9-1309:35)
[Info][Witness] unassume invariant: ((((((((((((((((((((((-1LL + (long long )argc) - (long long )i >= 0LL && (0LL - (long long )err) - (long long )i >= 0LL) && (3LL - (long long )argc) - (long long )i >= 0LL) && (long long )err - (long long )i >= 0LL) && 0 == i) && i == 0) || (0 <= i && i <= 100000)) && (argc == 1 || argc == 3)) && argc != 0) && argc % 2 == 1) && err == 0) && (3LL - (long long )argc) - (long long )err >= 0LL) && (-1LL + (long long )argc) - (long long )err >= 0LL) && (long long )err + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )err >= 0LL) && (3LL - (long long )argc) + (long long )i >= 0LL) && (0LL - (long long )err) + (long long )i >= 0LL) && (-1LL + (long long )argc) + (long long )err >= 0LL) && (-1LL + (long long )argc) + (long long )i >= 0LL) && argc <= 127) && argc <= 3) && 1 <= argc) && 0 <= argc (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1315:9-1315:35)
[Info][Witness] unassume invariant: ((((((((2147483647LL + (long long )argc) + (long long )err >= 0LL && (2147483648LL + (long long )err) + (long long )i >= 0LL) && (2147483647LL - (long long )err) + (long long )i >= 0LL) && (2147483651LL - (long long )argc) + (long long )err >= 0LL) && (2147483646LL + (long long )argc) - (long long )err >= 0LL) && (2147483650LL - (long long )argc) - (long long )err >= 0LL) || (((((((0 <= i && i <= 99999) && (-1LL + (long long )argc) + (long long )err >= 0LL) && (0LL - (long long )err) + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )err >= 0LL) && (long long )err + (long long )i >= 0LL) && (-1LL + (long long )argc) - (long long )err >= 0LL) && (3LL - (long long )argc) - (long long )err >= 0LL)) && (3LL - (long long )argc) + (long long )i >= 0LL) && (-1LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1315:9-1315:35)
[Info][Imprecise] Invalidating expressions: & err (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1316:13-1316:61)
[Info][Witness] unassume invariant: ((((((((2147483647LL + (long long )argc) + (long long )err >= 0LL && (2147483648LL + (long long )err) + (long long )i >= 0LL) && (2147483647LL - (long long )err) + (long long )i >= 0LL) && (2147483651LL - (long long )argc) + (long long )err >= 0LL) && (2147483646LL + (long long )argc) - (long long )err >= 0LL) && (2147483650LL - (long long )argc) - (long long )err >= 0LL) || (((((((0 <= i && i <= 99999) && (-1LL + (long long )argc) + (long long )err >= 0LL) && (0LL - (long long )err) + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )err >= 0LL) && (long long )err + (long long )i >= 0LL) && (-1LL + (long long )argc) - (long long )err >= 0LL) && (3LL - (long long )argc) - (long long )err >= 0LL)) && (3LL - (long long )argc) + (long long )i >= 0LL) && (-1LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1316:13-1316:61)
[Info][Witness] unassume invariant: (((((((err != 0 && (2147483650LL - (long long )argc) - (long long )err >= 0LL) && (2147483646LL + (long long )argc) - (long long )err >= 0LL) && (2147483651LL - (long long )argc) + (long long )err >= 0LL) && (2147483647LL - (long long )err) + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )i >= 0LL) && (2147483648LL + (long long )err) + (long long )i >= 0LL) && (2147483647LL + (long long )argc) + (long long )err >= 0LL) && (-1LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1316:13-1316:61)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )stderr (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1317:13-1317:61)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1317:13-1317:61)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1317:13-1317:61)
[Info][Witness] unassume invariant: (((((((((((err != 0 && (4294967294LL - (long long )err) - (long long )i >= 0LL) && (4294967294LL - (long long )argc) - (long long )err >= 0LL) && (4294967294LL - (long long )argc) - (long long )i >= 0LL) && (4294967295LL + (long long )err) - (long long )i >= 0LL) && (4294967295LL + (long long )argc) - (long long )err >= 0LL) && (4294967295LL + (long long )argc) - (long long )i >= 0LL) && (4294967295LL - (long long )err) + (long long )i >= 0LL) && (4294967295LL - (long long )argc) + (long long )err >= 0LL) && (4294967295LL - (long long )argc) + (long long )i >= 0LL) && (4294967296LL + (long long )err) + (long long )i >= 0LL) && (4294967296LL + (long long )argc) + (long long )err >= 0LL) && (4294967296LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1317:13-1317:61)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1317:13-1317:61)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1315:9-1315:35)
[Info][Witness] unassume invariant: ((((((((((((((((((((((-1LL + (long long )argc) - (long long )i >= 0LL && (0LL - (long long )err) - (long long )i >= 0LL) && (3LL - (long long )argc) - (long long )i >= 0LL) && (long long )err - (long long )i >= 0LL) && 0 == i) && i == 0) || (0 <= i && i <= 100000)) && (argc == 1 || argc == 3)) && argc != 0) && argc % 2 == 1) && err == 0) && (3LL - (long long )argc) - (long long )err >= 0LL) && (-1LL + (long long )argc) - (long long )err >= 0LL) && (long long )err + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )err >= 0LL) && (3LL - (long long )argc) + (long long )i >= 0LL) && (0LL - (long long )err) + (long long )i >= 0LL) && (-1LL + (long long )argc) + (long long )err >= 0LL) && (-1LL + (long long )argc) + (long long )i >= 0LL) && argc <= 127) && argc <= 3) && 1 <= argc) && 0 <= argc (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1315:9-1315:35)
[Info][Witness] unassume invariant: ((((((((((((((-1LL + (long long )argc) - (long long )i >= 0LL && (0LL - (long long )err) - (long long )i >= 0LL) && (3LL - (long long )argc) - (long long )i >= 0LL) && (long long )err - (long long )i >= 0LL) && 0 == i) && i == 0) || (0 <= i && i <= 100000)) && (3LL - (long long )argc) - (long long )err >= 0LL) && (-1LL + (long long )argc) - (long long )err >= 0LL) && (long long )err + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )err >= 0LL) && (3LL - (long long )argc) + (long long )i >= 0LL) && (0LL - (long long )err) + (long long )i >= 0LL) && (-1LL + (long long )argc) + (long long )err >= 0LL) && (-1LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1315:9-1315:35)
[Info][Witness] unassume invariant: ((((((((((((((((((((((-1LL + (long long )argc) - (long long )i >= 0LL && (0LL - (long long )err) - (long long )i >= 0LL) && (3LL - (long long )argc) - (long long )i >= 0LL) && (long long )err - (long long )i >= 0LL) && 0 == i) && i == 0) || (0 <= i && i <= 100000)) && (argc == 1 || argc == 3)) && argc != 0) && argc % 2 == 1) && err == 0) && (3LL - (long long )argc) - (long long )err >= 0LL) && (-1LL + (long long )argc) - (long long )err >= 0LL) && (long long )err + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )err >= 0LL) && (3LL - (long long )argc) + (long long )i >= 0LL) && (0LL - (long long )err) + (long long )i >= 0LL) && (-1LL + (long long )argc) + (long long )err >= 0LL) && (-1LL + (long long )argc) + (long long )i >= 0LL) && argc <= 127) && argc <= 3) && 1 <= argc) && 0 <= argc (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1321:9-1321:35)
[Info][Witness] unassume invariant: ((((((((2147483647LL + (long long )argc) + (long long )err >= 0LL && (2147483648LL + (long long )err) + (long long )i >= 0LL) && (2147483647LL - (long long )err) + (long long )i >= 0LL) && (2147483651LL - (long long )argc) + (long long )err >= 0LL) && (2147483646LL + (long long )argc) - (long long )err >= 0LL) && (2147483650LL - (long long )argc) - (long long )err >= 0LL) || (((((((0 <= i && i <= 99999) && (-1LL + (long long )argc) + (long long )err >= 0LL) && (0LL - (long long )err) + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )err >= 0LL) && (long long )err + (long long )i >= 0LL) && (-1LL + (long long )argc) - (long long )err >= 0LL) && (3LL - (long long )argc) - (long long )err >= 0LL)) && (3LL - (long long )argc) + (long long )i >= 0LL) && (-1LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1321:9-1321:35)
[Info][Imprecise] Invalidating expressions: & err (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1322:13-1322:61)
[Info][Witness] unassume invariant: ((((((((2147483647LL + (long long )argc) + (long long )err >= 0LL && (2147483648LL + (long long )err) + (long long )i >= 0LL) && (2147483647LL - (long long )err) + (long long )i >= 0LL) && (2147483651LL - (long long )argc) + (long long )err >= 0LL) && (2147483646LL + (long long )argc) - (long long )err >= 0LL) && (2147483650LL - (long long )argc) - (long long )err >= 0LL) || (((((((0 <= i && i <= 99999) && (-1LL + (long long )argc) + (long long )err >= 0LL) && (0LL - (long long )err) + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )err >= 0LL) && (long long )err + (long long )i >= 0LL) && (-1LL + (long long )argc) - (long long )err >= 0LL) && (3LL - (long long )argc) - (long long )err >= 0LL)) && (3LL - (long long )argc) + (long long )i >= 0LL) && (-1LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1322:13-1322:61)
[Info][Witness] unassume invariant: (((((((err != 0 && (2147483650LL - (long long )argc) - (long long )err >= 0LL) && (2147483646LL + (long long )argc) - (long long )err >= 0LL) && (2147483651LL - (long long )argc) + (long long )err >= 0LL) && (2147483647LL - (long long )err) + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )i >= 0LL) && (2147483648LL + (long long )err) + (long long )i >= 0LL) && (2147483647LL + (long long )argc) + (long long )err >= 0LL) && (-1LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1322:13-1322:61)
[Info][Imprecise] Invalidating expressions: (FILE * __restrict  )stderr (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1323:13-1323:61)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1323:13-1323:61)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1323:13-1323:61)
[Info][Witness] unassume invariant: (((((((((((err != 0 && (4294967294LL - (long long )err) - (long long )i >= 0LL) && (4294967294LL - (long long )argc) - (long long )err >= 0LL) && (4294967294LL - (long long )argc) - (long long )i >= 0LL) && (4294967295LL + (long long )err) - (long long )i >= 0LL) && (4294967295LL + (long long )argc) - (long long )err >= 0LL) && (4294967295LL + (long long )argc) - (long long )i >= 0LL) && (4294967295LL - (long long )err) + (long long )i >= 0LL) && (4294967295LL - (long long )argc) + (long long )err >= 0LL) && (4294967295LL - (long long )argc) + (long long )i >= 0LL) && (4294967296LL + (long long )err) + (long long )i >= 0LL) && (4294967296LL + (long long )argc) + (long long )err >= 0LL) && (4294967296LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1323:13-1323:61)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1323:13-1323:61)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1321:9-1321:35)
[Info][Witness] unassume invariant: ((((((((((((((((((((((-1LL + (long long )argc) - (long long )i >= 0LL && (0LL - (long long )err) - (long long )i >= 0LL) && (3LL - (long long )argc) - (long long )i >= 0LL) && (long long )err - (long long )i >= 0LL) && 0 == i) && i == 0) || (0 <= i && i <= 100000)) && (argc == 1 || argc == 3)) && argc != 0) && argc % 2 == 1) && err == 0) && (3LL - (long long )argc) - (long long )err >= 0LL) && (-1LL + (long long )argc) - (long long )err >= 0LL) && (long long )err + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )err >= 0LL) && (3LL - (long long )argc) + (long long )i >= 0LL) && (0LL - (long long )err) + (long long )i >= 0LL) && (-1LL + (long long )argc) + (long long )err >= 0LL) && (-1LL + (long long )argc) + (long long )i >= 0LL) && argc <= 127) && argc <= 3) && 1 <= argc) && 0 <= argc (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1321:9-1321:35)
[Info][Witness] unassume invariant: (((((((3LL - (long long )argc) - (long long )err >= 0LL && (-1LL + (long long )argc) - (long long )err >= 0LL) && (long long )err + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )err >= 0LL) && (3LL - (long long )argc) + (long long )i >= 0LL) && (0LL - (long long )err) + (long long )i >= 0LL) && (-1LL + (long long )argc) + (long long )err >= 0LL) && (-1LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1321:9-1321:35)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:415:1-419:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:420:1-424:1)
[Warning][Deadcode] Function '__uint16_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:425:1-429:1)
[Warning][Deadcode] Function '__uint32_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:430:1-434:1)
[Warning][Deadcode] Function '__uint64_identity' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:435:1-439:1)
[Warning][Deadcode] Function 'lock' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1329:1-1335:1)
[Warning][Deadcode] Function 'unlock' is uncalled: 4 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1336:1-1342:1)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 65
  dead: 13 (13 in uncalled functions)
  total lines: 78
[Warning][Race] Memory location data2Value (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1239:12-1239:26)
  write with region:{data2Value} (conf. 110)  (exp: & data2Value) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1253:5-1253:24)
  write with [region:{data2Value}, thread:[main, funcA@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1304:13-1304:85]] (conf. 110)  (exp: & data2Value) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1253:5-1253:24)
  read with region:{data2Value} (conf. 110)  (exp: & data2Value) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1268:5-1268:20)
  read with [region:{data2Value}, thread:[main, funcB@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1310:13-1310:85]] (conf. 110)  (exp: & data2Value) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1268:5-1268:20)
[Warning][Race] Memory location data1Value (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1238:12-1238:26)
  write with region:{data1Value} (conf. 110)  (exp: & data1Value) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1247:5-1247:19)
  write with [region:{data1Value}, thread:[main, funcA@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1304:13-1304:85]] (conf. 110)  (exp: & data1Value) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1247:5-1247:19)
  read with region:{data1Value} (conf. 110)  (exp: & data1Value) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1250:5-1250:20)
  read with [region:{data1Value}, thread:[main, funcA@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1304:13-1304:85]] (conf. 110)  (exp: & data1Value) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1250:5-1250:20)
  read with region:{data1Value} (conf. 110)  (exp: & data1Value) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1261:9-1261:24)
  read with [region:{data1Value}, thread:[main, funcB@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1310:13-1310:85]] (conf. 110)  (exp: & data1Value) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1261:9-1261:24)
  read with region:{data1Value} (conf. 110)  (exp: & data1Value) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1265:5-1265:20)
  read with [region:{data1Value}, thread:[main, funcB@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1310:13-1310:85]] (conf. 110)  (exp: & data1Value) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1265:5-1265:20)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:20:73-20:74)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1312:13)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1312:13)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1312:13)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1312:13)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1312:13)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1312:13)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1312:13)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1312:13)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1312:13)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1312:13)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1312:13)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1312:13)
[Success][Witness] invariant confirmed: err != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1312:13)
[Success][Witness] invariant confirmed: (2147483647LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1294:9)
[Warning][Witness] invariant unconfirmed: (2147483647LL + (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1294:9)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1294:9)
[Success][Witness] invariant confirmed: (2147483651LL - (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1294:9)
[Warning][Witness] invariant unconfirmed: (2147483651LL - (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1294:9)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1294:9)
[Success][Witness] invariant confirmed: (2147483646LL + (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1294:9)
[Warning][Witness] invariant unconfirmed: (2147483646LL + (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1294:9)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1294:9)
[Success][Witness] invariant confirmed: (2147483650LL - (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1294:9)
[Warning][Witness] invariant unconfirmed: (2147483650LL - (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1294:9)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1294:9)
[Success][Witness] invariant confirmed: err != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1294:9)
[Success][Witness] invariant confirmed: (2LL + (long long )t1) + (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1260:5)
[Success][Witness] invariant confirmed: (0LL - (long long )t1) + (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1260:5)
[Success][Witness] invariant confirmed: (-2LL - (long long )t1) - (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1260:5)
[Success][Witness] invariant confirmed: (long long )t1 - (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1260:5)
[Success][Witness] invariant confirmed: -1 == t1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1260:5)
[Success][Witness] invariant confirmed: -1 == t2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1260:5)
[Success][Witness] invariant confirmed: t1 == t2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1260:5)
[Success][Witness] invariant confirmed: t2 == -1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1260:5)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1323:13)
[Warning][Witness] invariant unconfirmed: (2147483647LL + (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1323:13)
[Warning][Witness] invariant unconfirmed: (2147483648LL + (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1323:13)
[Warning][Witness] invariant unconfirmed: (3LL - (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1323:13)
[Warning][Witness] invariant unconfirmed: (2147483647LL - (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1323:13)
[Warning][Witness] invariant unconfirmed: (2147483651LL - (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1323:13)
[Warning][Witness] invariant unconfirmed: (2147483646LL + (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1323:13)
[Warning][Witness] invariant unconfirmed: (2147483650LL - (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1323:13)
[Success][Witness] invariant confirmed: err != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1323:13)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1306:13)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1306:13)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1306:13)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1306:13)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1306:13)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1306:13)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1306:13)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1306:13)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1306:13)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1306:13)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1306:13)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1306:13)
[Success][Witness] invariant confirmed: err != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1306:13)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1321:5)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1321:5)
[Warning][Witness] invariant unconfirmed: (0LL - (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1321:5)
[Warning][Witness] invariant unconfirmed: (3LL - (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1321:5)
[Warning][Witness] invariant unconfirmed: (3LL - (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1321:5)
[Warning][Witness] invariant unconfirmed: (long long )err + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1321:5)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1321:5)
[Warning][Witness] invariant unconfirmed: (3LL - (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1321:5)
[Warning][Witness] invariant unconfirmed: ((((((-1LL + (long long )argc) - (long long )i >= 0LL && (0LL - (long long )err) - (long long )i >= 0LL) && (3LL - (long long )argc) - (long long )i >= 0LL) && (long long )err - (long long )i >= 0LL) && 0 == i) && i == 0) || (0 <= i && i <= 100000) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1321:5)
[Success][Witness] invariant confirmed: (2147483647LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1297:5)
[Success][Witness] invariant confirmed: (2147483651LL - (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1297:5)
[Success][Witness] invariant confirmed: (2147483646LL + (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1297:5)
[Success][Witness] invariant confirmed: (2147483650LL - (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1297:5)
[Warning][Witness] invariant unconfirmed: ((((((((2147483647LL + (long long )argc) + (long long )err >= 0LL && (4294967296LL + (long long )err) + (long long )i >= 0LL) && (2147483651LL - (long long )argc) + (long long )err >= 0LL) && (4294967295LL - (long long )err) + (long long )i >= 0LL) && (2147483646LL + (long long )argc) - (long long )err >= 0LL) && (4294967295LL + (long long )err) - (long long )i >= 0LL) && (2147483650LL - (long long )argc) - (long long )err >= 0LL) && (4294967294LL - (long long )err) - (long long )i >= 0LL) || ((((((((-1LL + (long long )argc) + (long long )err >= 0LL && (2147483648LL + (long long )err) + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )err >= 0LL) && (2147483648LL - (long long )err) + (long long )i >= 0LL) && (-1LL + (long long )argc) - (long long )err >= 0LL) && (2147483647LL + (long long )err) - (long long )i >= 0LL) && (3LL - (long long )argc) - (long long )err >= 0LL) && (2147483647LL - (long long )err) - (long long )i >= 0LL) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1297:5)
[Success][Witness] invariant confirmed: (2147483647LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1292:5)
[Success][Witness] invariant confirmed: (2147483647LL + (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1292:5)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1292:5)
[Success][Witness] invariant confirmed: (2147483651LL - (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1292:5)
[Success][Witness] invariant confirmed: (2147483651LL - (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1292:5)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1292:5)
[Success][Witness] invariant confirmed: (2147483646LL + (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1292:5)
[Success][Witness] invariant confirmed: (2147483646LL + (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1292:5)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1292:5)
[Success][Witness] invariant confirmed: (2147483650LL - (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1292:5)
[Success][Witness] invariant confirmed: (2147483650LL - (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1292:5)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1292:5)
[Success][Witness] invariant confirmed: 0 <= t2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1269:5)
[Success][Witness] invariant confirmed: t2 <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1269:5)
[Success][Witness] invariant confirmed: t2 <= 255 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1269:5)
[Success][Witness] invariant confirmed: (2LL + (long long )t1) + (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1262:9)
[Success][Witness] invariant confirmed: (0LL - (long long )t1) + (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1262:9)
[Success][Witness] invariant confirmed: (-2LL - (long long )t1) - (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1262:9)
[Success][Witness] invariant confirmed: (long long )t1 - (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1262:9)
[Success][Witness] invariant confirmed: -1 == t1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1262:9)
[Success][Witness] invariant confirmed: -1 == t2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1262:9)
[Success][Witness] invariant confirmed: t1 == t2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1262:9)
[Success][Witness] invariant confirmed: (2147483649LL + (long long )t1) + (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1259:5)
[Success][Witness] invariant confirmed: (2147483647LL - (long long )t1) + (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1259:5)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )t1) - (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1259:5)
[Success][Witness] invariant confirmed: (2147483646LL - (long long )t1) - (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1259:5)
[Success][Witness] invariant confirmed: -1 == t1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1259:5)
[Success][Witness] invariant confirmed: t1 == -1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1259:5)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1280:9)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1280:9)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1280:9)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1280:9)
[Success][Witness] invariant confirmed: argc != 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1280:9)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1322:9)
[Warning][Witness] invariant unconfirmed: (3LL - (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1322:9)
[Warning][Witness] invariant unconfirmed: ((((((2147483647LL + (long long )argc) + (long long )err >= 0LL && (2147483648LL + (long long )err) + (long long )i >= 0LL) && (2147483647LL - (long long )err) + (long long )i >= 0LL) && (2147483651LL - (long long )argc) + (long long )err >= 0LL) && (2147483646LL + (long long )argc) - (long long )err >= 0LL) && (2147483650LL - (long long )argc) - (long long )err >= 0LL) || (((((((0 <= i && i <= 99999) && (-1LL + (long long )argc) + (long long )err >= 0LL) && (0LL - (long long )err) + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )err >= 0LL) && (long long )err + (long long )i >= 0LL) && (-1LL + (long long )argc) - (long long )err >= 0LL) && (3LL - (long long )argc) - (long long )err >= 0LL) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1322:9)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1299:9)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1299:9)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1299:9)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1299:9)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1299:9)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1299:9)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1299:9)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1299:9)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1299:9)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1299:9)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1299:9)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1299:9)
[Success][Witness] invariant confirmed: err != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1299:9)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1295:9)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1295:9)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1295:9)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1295:9)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1295:9)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1295:9)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1295:9)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1295:9)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1295:9)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1295:9)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1295:9)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1295:9)
[Success][Witness] invariant confirmed: err != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1295:9)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1281:13)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1281:13)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1281:13)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1281:13)
[Success][Witness] invariant confirmed: (2LL + (long long )t1) + (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1261:5)
[Success][Witness] invariant confirmed: (0LL - (long long )t1) + (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1261:5)
[Success][Witness] invariant confirmed: (-2LL - (long long )t1) - (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1261:5)
[Success][Witness] invariant confirmed: (long long )t1 - (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1261:5)
[Success][Witness] invariant confirmed: -1 == t1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1261:5)
[Success][Witness] invariant confirmed: -1 == t2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1261:5)
[Success][Witness] invariant confirmed: t1 == t2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1261:5)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1303:5)
[Success][Witness] invariant confirmed: (2147483647LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1303:5)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1303:5)
[Warning][Witness] invariant unconfirmed: (3LL - (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1303:5)
[Success][Witness] invariant confirmed: (2147483648LL - (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1303:5)
[Success][Witness] invariant confirmed: (2147483651LL - (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1303:5)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1303:5)
[Success][Witness] invariant confirmed: (2147483646LL + (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1303:5)
[Success][Witness] invariant confirmed: (2147483647LL + (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1303:5)
[Warning][Witness] invariant unconfirmed: (3LL - (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1303:5)
[Success][Witness] invariant confirmed: (2147483647LL - (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1303:5)
[Success][Witness] invariant confirmed: (2147483650LL - (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1303:5)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1282:13)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1282:13)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1282:13)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1282:13)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1282:13)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1282:13)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1282:13)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1282:13)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1282:13)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1282:13)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1282:13)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1282:13)
[Success][Witness] invariant confirmed: argc != 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1282:13)
[Success][Witness] invariant confirmed: argc != 3 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1282:13)
[Success][Witness] invariant confirmed: 0 <= t1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1270:5)
[Success][Witness] invariant confirmed: 0 <= t2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1270:5)
[Success][Witness] invariant confirmed: t1 <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1270:5)
[Success][Witness] invariant confirmed: t2 <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1270:5)
[Success][Witness] invariant confirmed: t2 <= 255 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1270:5)
[Success][Witness] invariant confirmed: t1 == 0 || t1 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1270:5)
[Success][Witness] invariant confirmed: (2147483645LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1284:13)
[Success][Witness] invariant confirmed: (2147483645LL + (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1284:13)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1284:13)
[Success][Witness] invariant confirmed: (2147483651LL - (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1284:13)
[Success][Witness] invariant confirmed: (2147483651LL - (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1284:13)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1284:13)
[Success][Witness] invariant confirmed: (2147483644LL + (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1284:13)
[Success][Witness] invariant confirmed: (2147483644LL + (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1284:13)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1284:13)
[Success][Witness] invariant confirmed: (2147483650LL - (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1284:13)
[Success][Witness] invariant confirmed: (2147483650LL - (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1284:13)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1284:13)
[Success][Witness] invariant confirmed: (2147483645LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1285:13)
[Success][Witness] invariant confirmed: (2147483645LL + (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1285:13)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1285:13)
[Success][Witness] invariant confirmed: (2147483651LL - (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1285:13)
[Success][Witness] invariant confirmed: (2147483651LL - (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1285:13)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1285:13)
[Success][Witness] invariant confirmed: (2147483644LL + (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1285:13)
[Success][Witness] invariant confirmed: (2147483644LL + (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1285:13)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1285:13)
[Success][Witness] invariant confirmed: (2147483650LL - (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1285:13)
[Success][Witness] invariant confirmed: (2147483650LL - (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1285:13)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1285:13)
[Warning][Witness] invariant unconfirmed: argc == 3 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1285:13)
[Success][Witness] invariant confirmed: (2LL + (long long )t1) + (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1265:5)
[Success][Witness] invariant confirmed: (0LL - (long long )t1) + (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1265:5)
[Success][Witness] invariant confirmed: (-2LL - (long long )t1) - (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1265:5)
[Success][Witness] invariant confirmed: (long long )t1 - (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1265:5)
[Success][Witness] invariant confirmed: -1 == t1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1265:5)
[Success][Witness] invariant confirmed: -1 == t2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1265:5)
[Success][Witness] invariant confirmed: t1 == t2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1265:5)
[Success][Witness] invariant confirmed: 0 <= t1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1251:5)
[Success][Witness] invariant confirmed: t1 <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1251:5)
[Success][Witness] invariant confirmed: t1 == 0 || t1 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1251:5)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1309:5)
[Warning][Witness] invariant unconfirmed: (3LL - (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1309:5)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1309:5)
[Warning][Witness] invariant unconfirmed: (3LL - (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1309:5)
[Warning][Witness] invariant unconfirmed: ((((((((((-1LL + (long long )argc) + (long long )i >= 0LL && (0LL - (long long )err) + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )i >= 0LL) && (long long )err + (long long )i >= 0LL) && (-1LL + (long long )argc) - (long long )i >= 0LL) && (0LL - (long long )err) - (long long )i >= 0LL) && (3LL - (long long )argc) - (long long )i >= 0LL) && (long long )err - (long long )i >= 0LL) && 0 == i) && i == 0) || ((((((1 <= i && i <= 100000) && (-2LL + (long long )argc) + (long long )i >= 0LL) && (-1LL + (long long )err) + (long long )i >= 0LL) && (-1LL - (long long )err) + (long long )i >= 0LL) && (2LL - (long long )argc) + (long long )i >= 0LL) && i != 0) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1309:5)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1302:5)
[Success][Witness] invariant confirmed: (2147483647LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1302:5)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1302:5)
[Warning][Witness] invariant unconfirmed: (3LL - (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1302:5)
[Success][Witness] invariant confirmed: (2147483648LL - (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1302:5)
[Success][Witness] invariant confirmed: (2147483651LL - (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1302:5)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1302:5)
[Success][Witness] invariant confirmed: (2147483646LL + (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1302:5)
[Success][Witness] invariant confirmed: (2147483647LL + (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1302:5)
[Warning][Witness] invariant unconfirmed: (3LL - (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1302:5)
[Success][Witness] invariant confirmed: (2147483647LL - (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1302:5)
[Success][Witness] invariant confirmed: (2147483650LL - (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1302:5)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1301:5)
[Success][Witness] invariant confirmed: (2147483647LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1301:5)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1301:5)
[Warning][Witness] invariant unconfirmed: (3LL - (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1301:5)
[Success][Witness] invariant confirmed: (2147483648LL - (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1301:5)
[Success][Witness] invariant confirmed: (2147483651LL - (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1301:5)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1301:5)
[Success][Witness] invariant confirmed: (2147483646LL + (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1301:5)
[Success][Witness] invariant confirmed: (2147483647LL + (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1301:5)
[Warning][Witness] invariant unconfirmed: (3LL - (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1301:5)
[Success][Witness] invariant confirmed: (2147483647LL - (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1301:5)
[Success][Witness] invariant confirmed: (2147483650LL - (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1301:5)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1311:13)
[Warning][Witness] invariant unconfirmed: (2147483647LL + (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1311:13)
[Warning][Witness] invariant unconfirmed: (2147483648LL + (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1311:13)
[Warning][Witness] invariant unconfirmed: (3LL - (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1311:13)
[Warning][Witness] invariant unconfirmed: (2147483647LL - (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1311:13)
[Warning][Witness] invariant unconfirmed: (2147483651LL - (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1311:13)
[Warning][Witness] invariant unconfirmed: (2147483646LL + (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1311:13)
[Warning][Witness] invariant unconfirmed: (2147483650LL - (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1311:13)
[Success][Witness] invariant confirmed: err != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1311:13)
[Success][Witness] invariant confirmed: (2147483647LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1298:9)
[Warning][Witness] invariant unconfirmed: (2147483647LL + (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1298:9)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1298:9)
[Success][Witness] invariant confirmed: (2147483651LL - (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1298:9)
[Warning][Witness] invariant unconfirmed: (2147483651LL - (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1298:9)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1298:9)
[Success][Witness] invariant confirmed: (2147483646LL + (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1298:9)
[Warning][Witness] invariant unconfirmed: (2147483646LL + (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1298:9)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1298:9)
[Success][Witness] invariant confirmed: (2147483650LL - (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1298:9)
[Warning][Witness] invariant unconfirmed: (2147483650LL - (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1298:9)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1298:9)
[Success][Witness] invariant confirmed: err != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1298:9)
[Success][Witness] invariant confirmed: (2147483647LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1288:5)
[Success][Witness] invariant confirmed: (2147483647LL + (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1288:5)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1288:5)
[Success][Witness] invariant confirmed: (2147483651LL - (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1288:5)
[Success][Witness] invariant confirmed: (2147483651LL - (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1288:5)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1288:5)
[Success][Witness] invariant confirmed: (2147483646LL + (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1288:5)
[Success][Witness] invariant confirmed: (2147483646LL + (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1288:5)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1288:5)
[Success][Witness] invariant confirmed: (2147483650LL - (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1288:5)
[Success][Witness] invariant confirmed: (2147483650LL - (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1288:5)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1288:5)
[Success][Witness] invariant confirmed: -1 == t1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1248:5)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1324:13)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1324:13)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1324:13)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1324:13)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1324:13)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1324:13)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1324:13)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1324:13)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1324:13)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1324:13)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1324:13)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1324:13)
[Success][Witness] invariant confirmed: err != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1324:13)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1327:5)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1327:5)
[Warning][Witness] invariant unconfirmed: (0LL - (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1327:5)
[Warning][Witness] invariant unconfirmed: (3LL - (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1327:5)
[Warning][Witness] invariant unconfirmed: (3LL - (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1327:5)
[Warning][Witness] invariant unconfirmed: (long long )err + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1327:5)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1327:5)
[Warning][Witness] invariant unconfirmed: (3LL - (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1327:5)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1310:9)
[Warning][Witness] invariant unconfirmed: (3LL - (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1310:9)
[Warning][Witness] invariant unconfirmed: ((((((2147483647LL + (long long )argc) + (long long )err >= 0LL && (2147483648LL + (long long )err) + (long long )i >= 0LL) && (2147483647LL - (long long )err) + (long long )i >= 0LL) && (2147483651LL - (long long )argc) + (long long )err >= 0LL) && (2147483646LL + (long long )argc) - (long long )err >= 0LL) && (2147483650LL - (long long )argc) - (long long )err >= 0LL) || (((((((-1LL + (long long )argc) + (long long )err >= 0LL && (0LL - (long long )err) + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )err >= 0LL) && (long long )err + (long long )i >= 0LL) && (-1LL + (long long )argc) - (long long )err >= 0LL) && (3LL - (long long )argc) - (long long )err >= 0LL) && (((((((-1LL + (long long )argc) - (long long )i >= 0LL && (0LL - (long long )err) - (long long )i >= 0LL) && (3LL - (long long )argc) - (long long )i >= 0LL) && (long long )err - (long long )i >= 0LL) && 0 == i) && i == 0) || (0 <= i && i <= 99999))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1310:9)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1316:9)
[Warning][Witness] invariant unconfirmed: (3LL - (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1316:9)
[Warning][Witness] invariant unconfirmed: ((((((2147483647LL + (long long )argc) + (long long )err >= 0LL && (2147483648LL + (long long )err) + (long long )i >= 0LL) && (2147483647LL - (long long )err) + (long long )i >= 0LL) && (2147483651LL - (long long )argc) + (long long )err >= 0LL) && (2147483646LL + (long long )argc) - (long long )err >= 0LL) && (2147483650LL - (long long )argc) - (long long )err >= 0LL) || (((((((0 <= i && i <= 99999) && (-1LL + (long long )argc) + (long long )err >= 0LL) && (0LL - (long long )err) + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )err >= 0LL) && (long long )err + (long long )i >= 0LL) && (-1LL + (long long )argc) - (long long )err >= 0LL) && (3LL - (long long )argc) - (long long )err >= 0LL) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1316:9)
[Success][Witness] invariant confirmed: (-1LL - (long long )t1) + (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1275:5)
[Success][Witness] invariant confirmed: (1LL + (long long )t1) - (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1275:5)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1315:5)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1315:5)
[Warning][Witness] invariant unconfirmed: (0LL - (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1315:5)
[Warning][Witness] invariant unconfirmed: (3LL - (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1315:5)
[Warning][Witness] invariant unconfirmed: (3LL - (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1315:5)
[Warning][Witness] invariant unconfirmed: (long long )err + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1315:5)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1315:5)
[Warning][Witness] invariant unconfirmed: (3LL - (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1315:5)
[Warning][Witness] invariant unconfirmed: ((((((-1LL + (long long )argc) - (long long )i >= 0LL && (0LL - (long long )err) - (long long )i >= 0LL) && (3LL - (long long )argc) - (long long )i >= 0LL) && (long long )err - (long long )i >= 0LL) && 0 == i) && i == 0) || (0 <= i && i <= 100000) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1315:5)
[Success][Witness] invariant confirmed: (2147483647LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1293:5)
[Warning][Witness] invariant unconfirmed: (2147483647LL + (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1293:5)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1293:5)
[Success][Witness] invariant confirmed: (2147483651LL - (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1293:5)
[Warning][Witness] invariant unconfirmed: (2147483651LL - (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1293:5)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1293:5)
[Success][Witness] invariant confirmed: (2147483646LL + (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1293:5)
[Warning][Witness] invariant unconfirmed: (2147483646LL + (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1293:5)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1293:5)
[Success][Witness] invariant confirmed: (2147483650LL - (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1293:5)
[Warning][Witness] invariant unconfirmed: (2147483650LL - (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1293:5)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1293:5)
[Success][Witness] invariant confirmed: -1 == t1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1249:5)
[Success][Witness] invariant confirmed: (2LL + (long long )t1) + (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1263:9)
[Success][Witness] invariant confirmed: (0LL - (long long )t1) + (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1263:9)
[Success][Witness] invariant confirmed: (-2LL - (long long )t1) - (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1263:9)
[Success][Witness] invariant confirmed: (long long )t1 - (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1263:9)
[Success][Witness] invariant confirmed: -1 == t1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1263:9)
[Success][Witness] invariant confirmed: -1 == t2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1263:9)
[Success][Witness] invariant confirmed: t1 == t2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1263:9)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )t1) + (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1258:5)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )t1) + (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1258:5)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )t1) - (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1258:5)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )t1) - (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1258:5)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1305:13)
[Warning][Witness] invariant unconfirmed: (2147483647LL + (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1305:13)
[Warning][Witness] invariant unconfirmed: (2147483648LL + (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1305:13)
[Warning][Witness] invariant unconfirmed: (3LL - (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1305:13)
[Warning][Witness] invariant unconfirmed: (2147483647LL - (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1305:13)
[Warning][Witness] invariant unconfirmed: (2147483651LL - (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1305:13)
[Warning][Witness] invariant unconfirmed: (2147483646LL + (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1305:13)
[Warning][Witness] invariant unconfirmed: (2147483650LL - (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1305:13)
[Success][Witness] invariant confirmed: err != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1305:13)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1317:13)
[Warning][Witness] invariant unconfirmed: (2147483647LL + (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1317:13)
[Warning][Witness] invariant unconfirmed: (2147483648LL + (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1317:13)
[Warning][Witness] invariant unconfirmed: (3LL - (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1317:13)
[Warning][Witness] invariant unconfirmed: (2147483647LL - (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1317:13)
[Warning][Witness] invariant unconfirmed: (2147483651LL - (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1317:13)
[Warning][Witness] invariant unconfirmed: (2147483646LL + (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1317:13)
[Warning][Witness] invariant unconfirmed: (2147483650LL - (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1317:13)
[Success][Witness] invariant confirmed: err != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1317:13)
[Success][Witness] invariant confirmed: -1 == t1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1246:5)
[Success][Witness] invariant confirmed: t1 == -1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1246:5)
[Warning][Witness] invariant unconfirmed: ((((((((-1LL + (long long )argc) + (long long )i >= 0LL && (2147483647LL + (long long )argc) + (long long )err >= 0LL) && (2147483648LL + (long long )err) + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )i >= 0LL) && (2147483647LL - (long long )err) + (long long )i >= 0LL) && (2147483651LL - (long long )argc) + (long long )err >= 0LL) && (2147483646LL + (long long )argc) - (long long )err >= 0LL) && (2147483650LL - (long long )argc) - (long long )err >= 0LL) || (((((-1LL + (long long )argc) + (long long )err >= 0LL && (3LL - (long long )argc) + (long long )err >= 0LL) && (-1LL + (long long )argc) - (long long )err >= 0LL) && (3LL - (long long )argc) - (long long )err >= 0LL) && (((((((((((-1LL + (long long )argc) + (long long )i >= 0LL && (0LL - (long long )err) + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )i >= 0LL) && (long long )err + (long long )i >= 0LL) && (-1LL + (long long )argc) - (long long )i >= 0LL) && (0LL - (long long )err) - (long long )i >= 0LL) && (3LL - (long long )argc) - (long long )i >= 0LL) && (long long )err - (long long )i >= 0LL) && 0 == i) && i == 0) || ((((((1 <= i && i <= 99999) && (-2LL + (long long )argc) + (long long )i >= 0LL) && (-1LL + (long long )err) + (long long )i >= 0LL) && (-1LL - (long long )err) + (long long )i >= 0LL) && (2LL - (long long )argc) + (long long )i >= 0LL) && i != 0))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1304:9)
[Success][Witness] invariant confirmed: -1 == t1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1250:5)
[Success][Witness] invariant confirmed: -1 == t2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1267:5)
[Success][Witness] invariant confirmed: (2147483647LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1289:7)
[Success][Witness] invariant confirmed: (2147483647LL + (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1289:7)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1289:7)
[Success][Witness] invariant confirmed: (2147483651LL - (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1289:7)
[Success][Witness] invariant confirmed: (2147483651LL - (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1289:7)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1289:7)
[Success][Witness] invariant confirmed: (2147483646LL + (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1289:7)
[Success][Witness] invariant confirmed: (2147483646LL + (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1289:7)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1289:7)
[Success][Witness] invariant confirmed: (2147483650LL - (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1289:7)
[Success][Witness] invariant confirmed: (2147483650LL - (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1289:7)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1289:7)
[Success][Witness] invariant confirmed: 0 <= t1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1266:5)
[Success][Witness] invariant confirmed: t1 <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1266:5)
[Success][Witness] invariant confirmed: -1 == t2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1266:5)
[Success][Witness] invariant confirmed: t1 == 0 || t1 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1266:5)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1279:5)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1279:5)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1279:5)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1279:5)
[Success][Witness] invariant confirmed: 0 <= t1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1253:5)
[Success][Witness] invariant confirmed: t1 <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1253:5)
[Success][Witness] invariant confirmed: t1 == 0 || t1 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1253:5)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )t1) + (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1272:10)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )t1) + (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1272:10)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )t1) - (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1272:10)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )t1) - (long long )t2 >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1272:10)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1318:13)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1318:13)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1318:13)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1318:13)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1318:13)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1318:13)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1318:13)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1318:13)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1318:13)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1318:13)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1318:13)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1318:13)
[Success][Witness] invariant confirmed: err != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1318:13)
[Success][Witness] invariant confirmed: (2147483647LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1291:5)
[Success][Witness] invariant confirmed: (2147483647LL + (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1291:5)
[Success][Witness] invariant confirmed: (4294967296LL + (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1291:5)
[Success][Witness] invariant confirmed: (2147483651LL - (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1291:5)
[Success][Witness] invariant confirmed: (2147483651LL - (long long )argc) + (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1291:5)
[Success][Witness] invariant confirmed: (4294967295LL - (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1291:5)
[Success][Witness] invariant confirmed: (2147483646LL + (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1291:5)
[Success][Witness] invariant confirmed: (2147483646LL + (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1291:5)
[Success][Witness] invariant confirmed: (4294967295LL + (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1291:5)
[Success][Witness] invariant confirmed: (2147483650LL - (long long )argc) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1291:5)
[Success][Witness] invariant confirmed: (2147483650LL - (long long )argc) - (long long )err >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1291:5)
[Success][Witness] invariant confirmed: (4294967294LL - (long long )err) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1291:5)
[Success][Witness] invariant confirmed: -1 == t2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1268:5)
[Success][Witness] invariant confirmed: -1 == t1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1247:5)
[Warning][Witness] invariant unconfirmed: 0 <= argc (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1315:5)
[Warning][Witness] invariant unconfirmed: 1 <= argc (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1315:5)
[Warning][Witness] invariant unconfirmed: argc <= 3 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1315:5)
[Warning][Witness] invariant unconfirmed: argc <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1315:5)
[Warning][Witness] invariant unconfirmed: err == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1315:5)
[Warning][Witness] invariant unconfirmed: argc % 2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1315:5)
[Warning][Witness] invariant unconfirmed: argc != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1315:5)
[Warning][Witness] invariant unconfirmed: argc == 1 || argc == 3 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1315:5)
[Warning][Witness] invariant unconfirmed: 0 <= argc (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1309:5)
[Warning][Witness] invariant unconfirmed: 1 <= argc (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1309:5)
[Warning][Witness] invariant unconfirmed: argc <= 3 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1309:5)
[Warning][Witness] invariant unconfirmed: argc <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1309:5)
[Warning][Witness] invariant unconfirmed: (-1LL + (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1309:5)
[Warning][Witness] invariant unconfirmed: (0LL - (long long )err) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1309:5)
[Warning][Witness] invariant unconfirmed: (3LL - (long long )argc) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1309:5)
[Warning][Witness] invariant unconfirmed: (long long )err + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1309:5)
[Warning][Witness] invariant unconfirmed: err == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1309:5)
[Warning][Witness] invariant unconfirmed: argc % 2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1309:5)
[Warning][Witness] invariant unconfirmed: argc != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1309:5)
[Warning][Witness] invariant unconfirmed: argc == 1 || argc == 3 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1309:5)
[Warning][Witness] invariant unconfirmed: ((((((-1LL + (long long )argc) - (long long )i >= 0LL && (0LL - (long long )err) - (long long )i >= 0LL) && (3LL - (long long )argc) - (long long )i >= 0LL) && (long long )err - (long long )i >= 0LL) && 0 == i) && i == 0) || (0 <= i && i <= 100000) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1309:5)
[Warning][Witness] invariant unconfirmed: 0 <= argc (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1303:5)
[Warning][Witness] invariant unconfirmed: 1 <= argc (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1303:5)
[Warning][Witness] invariant unconfirmed: argc <= 3 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1303:5)
[Warning][Witness] invariant unconfirmed: argc <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1303:5)
[Warning][Witness] invariant unconfirmed: err == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1303:5)
[Warning][Witness] invariant unconfirmed: argc % 2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1303:5)
[Warning][Witness] invariant unconfirmed: argc != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1303:5)
[Warning][Witness] invariant unconfirmed: argc == 1 || argc == 3 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1303:5)
[Warning][Witness] invariant unconfirmed: ((((((((((-1LL + (long long )argc) + (long long )i >= 0LL && (0LL - (long long )err) + (long long )i >= 0LL) && (3LL - (long long )argc) + (long long )i >= 0LL) && (long long )err + (long long )i >= 0LL) && (-1LL + (long long )argc) - (long long )i >= 0LL) && (0LL - (long long )err) - (long long )i >= 0LL) && (3LL - (long long )argc) - (long long )i >= 0LL) && (long long )err - (long long )i >= 0LL) && 0 == i) && i == 0) || (((((1 <= i && i <= 100000) && (-2LL + (long long )argc) + (long long )i >= 0LL) && (-1LL + (long long )err) + (long long )i >= 0LL) && (-1LL - (long long )err) + (long long )i >= 0LL) && (2LL - (long long )argc) + (long long )i >= 0LL) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1303:5)
[Warning][Witness] invariant unconfirmed: 0 <= argc (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1321:5)
[Warning][Witness] invariant unconfirmed: 1 <= argc (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1321:5)
[Warning][Witness] invariant unconfirmed: argc <= 3 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1321:5)
[Warning][Witness] invariant unconfirmed: argc <= 127 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1321:5)
[Warning][Witness] invariant unconfirmed: err == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1321:5)
[Warning][Witness] invariant unconfirmed: argc % 2 == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1321:5)
[Warning][Witness] invariant unconfirmed: argc != 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1321:5)
[Warning][Witness] invariant unconfirmed: argc == 1 || argc == 3 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1321:5)
[Info][Witness] witness validation summary:
  confirmed: 314
  unconfirmed: 163
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 477
SV-COMP result: unknown
[Info][Race] Memory locations race summary:
  safe: 5
  vulnerable: 0
  unsafe: 2
  total memory locations: 7
