./goblint --conf conf/svcomp-validate.json --witness.yaml.unassume /mnt/goblint-svcomp/benchexec/results/155-concurrency-fix-locations/goblint.2024-03-01_08-09-03.files/SV-COMP24_unreach-call/safestack_relacy.yml/witness.yml --witness.yaml.validate /mnt/goblint-svcomp/benchexec/results/155-concurrency-fix-locations/goblint.2024-03-01_08-09-03.files/SV-COMP24_unreach-call/safestack_relacy.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-complex/safestack_relacy.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
:-1: Warning: Incompatible declaration for pthread_rwlock_init (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1669 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i (0)) 
	Failed assumption that pthread_rwlock_t and pthread_rwlock_t are isomorphic 
	Failed assumption that union __anonunion_pthread_rwlock_t_691634051 and union __anonunion_pthread_rwlock_t_656928968 are isomorphic 
	Failed assumption that struct __anonstruct___data_436374932 and struct __pthread_rwlock_arch_t are isomorphic (different integer types int  and unsigned int )
struct __anonstruct___data_436374932 {
   int __lock ;
   unsigned int __nr_readers ;
   unsigned int __readers_wakeup ;
   unsigned int __writer_wakeup ;
   unsigned int __nr_readers_queued ;
   unsigned int __nr_writers_queued ;
   unsigned char __flags ;
   unsigned char __shared ;
   signed char __rwelision ;
   unsigned char __pad2 ;
   int __writer ;
};

struct __pthread_rwlock_arch_t {
   unsigned int __readers ;
   unsigned int __writers ;
   unsigned int __wrphase_futex ;
   unsigned int __writers_futex ;
   unsigned int __pad3 ;
   unsigned int __pad4 ;
   unsigned char __flags ;
   unsigned char __shared ;
   signed char __rwelision ;
   unsigned char __pad2 ;
   int __cur_writer ;
};

union __anonunion_pthread_rwlock_t_691634051 {
   struct __anonstruct___data_436374932 __data ;
   char __size[32] ;
   long __align ;
};

union __anonunion_pthread_rwlock_t_656928968 {
   struct __pthread_rwlock_arch_t __data ;
   char __size[32] ;
   long __align ;
};
 
:-1: Warning: Incompatible declaration for pthread_rwlock_destroy (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1672 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i (0)) 
	Failed assumption that pthread_rwlock_t and pthread_rwlock_t are isomorphic 
	Failed assumption that union __anonunion_pthread_rwlock_t_691634051 and union __anonunion_pthread_rwlock_t_656928968 are isomorphic 
	Failed assumption that struct __anonstruct___data_436374932 and struct __pthread_rwlock_arch_t are isomorphic (different integer types int  and unsigned int )
struct __anonstruct___data_436374932 {
   int __lock ;
   unsigned int __nr_readers ;
   unsigned int __readers_wakeup ;
   unsigned int __writer_wakeup ;
   unsigned int __nr_readers_queued ;
   unsigned int __nr_writers_queued ;
   unsigned char __flags ;
   unsigned char __shared ;
   signed char __rwelision ;
   unsigned char __pad2 ;
   int __writer ;
};

struct __pthread_rwlock_arch_t {
   unsigned int __readers ;
   unsigned int __writers ;
   unsigned int __wrphase_futex ;
   unsigned int __writers_futex ;
   unsigned int __pad3 ;
   unsigned int __pad4 ;
   unsigned char __flags ;
   unsigned char __shared ;
   signed char __rwelision ;
   unsigned char __pad2 ;
   int __cur_writer ;
};

union __anonunion_pthread_rwlock_t_691634051 {
   struct __anonstruct___data_436374932 __data ;
   char __size[32] ;
   long __align ;
};

union __anonunion_pthread_rwlock_t_656928968 {
   struct __pthread_rwlock_arch_t __data ;
   char __size[32] ;
   long __align ;
};
 
:-1: Warning: Incompatible declaration for pthread_rwlock_rdlock (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1674 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i (0)) 
	Failed assumption that pthread_rwlock_t and pthread_rwlock_t are isomorphic 
	Failed assumption that union __anonunion_pthread_rwlock_t_691634051 and union __anonunion_pthread_rwlock_t_656928968 are isomorphic 
	Failed assumption that struct __anonstruct___data_436374932 and struct __pthread_rwlock_arch_t are isomorphic (different integer types int  and unsigned int )
struct __anonstruct___data_436374932 {
   int __lock ;
   unsigned int __nr_readers ;
   unsigned int __readers_wakeup ;
   unsigned int __writer_wakeup ;
   unsigned int __nr_readers_queued ;
   unsigned int __nr_writers_queued ;
   unsigned char __flags ;
   unsigned char __shared ;
   signed char __rwelision ;
   unsigned char __pad2 ;
   int __writer ;
};

struct __pthread_rwlock_arch_t {
   unsigned int __readers ;
   unsigned int __writers ;
   unsigned int __wrphase_futex ;
   unsigned int __writers_futex ;
   unsigned int __pad3 ;
   unsigned int __pad4 ;
   unsigned char __flags ;
   unsigned char __shared ;
   signed char __rwelision ;
   unsigned char __pad2 ;
   int __cur_writer ;
};

union __anonunion_pthread_rwlock_t_691634051 {
   struct __anonstruct___data_436374932 __data ;
   char __size[32] ;
   long __align ;
};

union __anonunion_pthread_rwlock_t_656928968 {
   struct __pthread_rwlock_arch_t __data ;
   char __size[32] ;
   long __align ;
};
 
:-1: Warning: Incompatible declaration for pthread_rwlock_tryrdlock (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1676 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i (0)) 
	Failed assumption that pthread_rwlock_t and pthread_rwlock_t are isomorphic 
	Failed assumption that union __anonunion_pthread_rwlock_t_691634051 and union __anonunion_pthread_rwlock_t_656928968 are isomorphic 
	Failed assumption that struct __anonstruct___data_436374932 and struct __pthread_rwlock_arch_t are isomorphic (different integer types int  and unsigned int )
struct __anonstruct___data_436374932 {
   int __lock ;
   unsigned int __nr_readers ;
   unsigned int __readers_wakeup ;
   unsigned int __writer_wakeup ;
   unsigned int __nr_readers_queued ;
   unsigned int __nr_writers_queued ;
   unsigned char __flags ;
   unsigned char __shared ;
   signed char __rwelision ;
   unsigned char __pad2 ;
   int __writer ;
};

struct __pthread_rwlock_arch_t {
   unsigned int __readers ;
   unsigned int __writers ;
   unsigned int __wrphase_futex ;
   unsigned int __writers_futex ;
   unsigned int __pad3 ;
   unsigned int __pad4 ;
   unsigned char __flags ;
   unsigned char __shared ;
   signed char __rwelision ;
   unsigned char __pad2 ;
   int __cur_writer ;
};

union __anonunion_pthread_rwlock_t_691634051 {
   struct __anonstruct___data_436374932 __data ;
   char __size[32] ;
   long __align ;
};

union __anonunion_pthread_rwlock_t_656928968 {
   struct __pthread_rwlock_arch_t __data ;
   char __size[32] ;
   long __align ;
};
 
:-1: Warning: Incompatible declaration for pthread_rwlock_timedrdlock (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1678 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i (0)) 
	Failed assumption that pthread_rwlock_t and pthread_rwlock_t are isomorphic 
	Failed assumption that union __anonunion_pthread_rwlock_t_691634051 and union __anonunion_pthread_rwlock_t_656928968 are isomorphic 
	Failed assumption that struct __anonstruct___data_436374932 and struct __pthread_rwlock_arch_t are isomorphic (different integer types int  and unsigned int )
struct __anonstruct___data_436374932 {
   int __lock ;
   unsigned int __nr_readers ;
   unsigned int __readers_wakeup ;
   unsigned int __writer_wakeup ;
   unsigned int __nr_readers_queued ;
   unsigned int __nr_writers_queued ;
   unsigned char __flags ;
   unsigned char __shared ;
   signed char __rwelision ;
   unsigned char __pad2 ;
   int __writer ;
};

struct __pthread_rwlock_arch_t {
   unsigned int __readers ;
   unsigned int __writers ;
   unsigned int __wrphase_futex ;
   unsigned int __writers_futex ;
   unsigned int __pad3 ;
   unsigned int __pad4 ;
   unsigned char __flags ;
   unsigned char __shared ;
   signed char __rwelision ;
   unsigned char __pad2 ;
   int __cur_writer ;
};

union __anonunion_pthread_rwlock_t_691634051 {
   struct __anonstruct___data_436374932 __data ;
   char __size[32] ;
   long __align ;
};

union __anonunion_pthread_rwlock_t_656928968 {
   struct __pthread_rwlock_arch_t __data ;
   char __size[32] ;
   long __align ;
};
 
:-1: Warning: Incompatible declaration for pthread_rwlock_wrlock (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1681 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i (0)) 
	Failed assumption that pthread_rwlock_t and pthread_rwlock_t are isomorphic 
	Failed assumption that union __anonunion_pthread_rwlock_t_691634051 and union __anonunion_pthread_rwlock_t_656928968 are isomorphic 
	Failed assumption that struct __anonstruct___data_436374932 and struct __pthread_rwlock_arch_t are isomorphic (different integer types int  and unsigned int )
struct __anonstruct___data_436374932 {
   int __lock ;
   unsigned int __nr_readers ;
   unsigned int __readers_wakeup ;
   unsigned int __writer_wakeup ;
   unsigned int __nr_readers_queued ;
   unsigned int __nr_writers_queued ;
   unsigned char __flags ;
   unsigned char __shared ;
   signed char __rwelision ;
   unsigned char __pad2 ;
   int __writer ;
};

struct __pthread_rwlock_arch_t {
   unsigned int __readers ;
   unsigned int __writers ;
   unsigned int __wrphase_futex ;
   unsigned int __writers_futex ;
   unsigned int __pad3 ;
   unsigned int __pad4 ;
   unsigned char __flags ;
   unsigned char __shared ;
   signed char __rwelision ;
   unsigned char __pad2 ;
   int __cur_writer ;
};

union __anonunion_pthread_rwlock_t_691634051 {
   struct __anonstruct___data_436374932 __data ;
   char __size[32] ;
   long __align ;
};

union __anonunion_pthread_rwlock_t_656928968 {
   struct __pthread_rwlock_arch_t __data ;
   char __size[32] ;
   long __align ;
};
 
:-1: Warning: Incompatible declaration for pthread_rwlock_trywrlock (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1683 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i (0)) 
	Failed assumption that pthread_rwlock_t and pthread_rwlock_t are isomorphic 
	Failed assumption that union __anonunion_pthread_rwlock_t_691634051 and union __anonunion_pthread_rwlock_t_656928968 are isomorphic 
	Failed assumption that struct __anonstruct___data_436374932 and struct __pthread_rwlock_arch_t are isomorphic (different integer types int  and unsigned int )
struct __anonstruct___data_436374932 {
   int __lock ;
   unsigned int __nr_readers ;
   unsigned int __readers_wakeup ;
   unsigned int __writer_wakeup ;
   unsigned int __nr_readers_queued ;
   unsigned int __nr_writers_queued ;
   unsigned char __flags ;
   unsigned char __shared ;
   signed char __rwelision ;
   unsigned char __pad2 ;
   int __writer ;
};

struct __pthread_rwlock_arch_t {
   unsigned int __readers ;
   unsigned int __writers ;
   unsigned int __wrphase_futex ;
   unsigned int __writers_futex ;
   unsigned int __pad3 ;
   unsigned int __pad4 ;
   unsigned char __flags ;
   unsigned char __shared ;
   signed char __rwelision ;
   unsigned char __pad2 ;
   int __cur_writer ;
};

union __anonunion_pthread_rwlock_t_691634051 {
   struct __anonstruct___data_436374932 __data ;
   char __size[32] ;
   long __align ;
};

union __anonunion_pthread_rwlock_t_656928968 {
   struct __pthread_rwlock_arch_t __data ;
   char __size[32] ;
   long __align ;
};
 
:-1: Warning: Incompatible declaration for pthread_rwlock_timedwrlock (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1685 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i (0)) 
	Failed assumption that pthread_rwlock_t and pthread_rwlock_t are isomorphic 
	Failed assumption that union __anonunion_pthread_rwlock_t_691634051 and union __anonunion_pthread_rwlock_t_656928968 are isomorphic 
	Failed assumption that struct __anonstruct___data_436374932 and struct __pthread_rwlock_arch_t are isomorphic (different integer types int  and unsigned int )
struct __anonstruct___data_436374932 {
   int __lock ;
   unsigned int __nr_readers ;
   unsigned int __readers_wakeup ;
   unsigned int __writer_wakeup ;
   unsigned int __nr_readers_queued ;
   unsigned int __nr_writers_queued ;
   unsigned char __flags ;
   unsigned char __shared ;
   signed char __rwelision ;
   unsigned char __pad2 ;
   int __writer ;
};

struct __pthread_rwlock_arch_t {
   unsigned int __readers ;
   unsigned int __writers ;
   unsigned int __wrphase_futex ;
   unsigned int __writers_futex ;
   unsigned int __pad3 ;
   unsigned int __pad4 ;
   unsigned char __flags ;
   unsigned char __shared ;
   signed char __rwelision ;
   unsigned char __pad2 ;
   int __cur_writer ;
};

union __anonunion_pthread_rwlock_t_691634051 {
   struct __anonstruct___data_436374932 __data ;
   char __size[32] ;
   long __align ;
};

union __anonunion_pthread_rwlock_t_656928968 {
   struct __pthread_rwlock_arch_t __data ;
   char __size[32] ;
   long __align ;
};
 
:-1: Warning: Incompatible declaration for pthread_rwlock_unlock (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1688 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i (0)) 
	Failed assumption that pthread_rwlock_t and pthread_rwlock_t are isomorphic 
	Failed assumption that union __anonunion_pthread_rwlock_t_691634051 and union __anonunion_pthread_rwlock_t_656928968 are isomorphic 
	Failed assumption that struct __anonstruct___data_436374932 and struct __pthread_rwlock_arch_t are isomorphic (different integer types int  and unsigned int )
struct __anonstruct___data_436374932 {
   int __lock ;
   unsigned int __nr_readers ;
   unsigned int __readers_wakeup ;
   unsigned int __writer_wakeup ;
   unsigned int __nr_readers_queued ;
   unsigned int __nr_writers_queued ;
   unsigned char __flags ;
   unsigned char __shared ;
   signed char __rwelision ;
   unsigned char __pad2 ;
   int __writer ;
};

struct __pthread_rwlock_arch_t {
   unsigned int __readers ;
   unsigned int __writers ;
   unsigned int __wrphase_futex ;
   unsigned int __writers_futex ;
   unsigned int __pad3 ;
   unsigned int __pad4 ;
   unsigned char __flags ;
   unsigned char __shared ;
   signed char __rwelision ;
   unsigned char __pad2 ;
   int __cur_writer ;
};

union __anonunion_pthread_rwlock_t_691634051 {
   struct __anonstruct___data_436374932 __data ;
   char __size[32] ;
   long __align ;
};

union __anonunion_pthread_rwlock_t_656928968 {
   struct __pthread_rwlock_arch_t __data ;
   char __size[32] ;
   long __align ;
};
 
:-1: Warning: Incompatible declaration for pthread_cond_init (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1707 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i (0)) 
	Failed assumption that pthread_cond_t and pthread_cond_t are isomorphic 
	Failed assumption that union __anonunion_pthread_cond_t_51417149 and union __anonunion_pthread_cond_t_951761805 are isomorphic (different number of fields in __anonstruct___data_282018390 and __pthread_cond_s: 8 != 7.)
union __anonunion_pthread_cond_t_51417149 {
   struct __anonstruct___data_282018390 __data ;
   char __size[48] ;
   long long __align ;
};

union __anonunion_pthread_cond_t_951761805 {
   struct __pthread_cond_s __data ;
   char __size[48] ;
   long long __align ;
};
 
:-1: Warning: Incompatible declaration for pthread_cond_destroy (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1710 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i (0)) 
	Failed assumption that pthread_cond_t and pthread_cond_t are isomorphic 
	Failed assumption that union __anonunion_pthread_cond_t_51417149 and union __anonunion_pthread_cond_t_951761805 are isomorphic (different number of fields in __anonstruct___data_282018390 and __pthread_cond_s: 8 != 7.)
union __anonunion_pthread_cond_t_51417149 {
   struct __anonstruct___data_282018390 __data ;
   char __size[48] ;
   long long __align ;
};

union __anonunion_pthread_cond_t_951761805 {
   struct __pthread_cond_s __data ;
   char __size[48] ;
   long long __align ;
};
 
:-1: Warning: Incompatible declaration for pthread_cond_signal (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1712 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i (0)) 
	Failed assumption that pthread_cond_t and pthread_cond_t are isomorphic 
	Failed assumption that union __anonunion_pthread_cond_t_51417149 and union __anonunion_pthread_cond_t_951761805 are isomorphic (different number of fields in __anonstruct___data_282018390 and __pthread_cond_s: 8 != 7.)
union __anonunion_pthread_cond_t_51417149 {
   struct __anonstruct___data_282018390 __data ;
   char __size[48] ;
   long long __align ;
};

union __anonunion_pthread_cond_t_951761805 {
   struct __pthread_cond_s __data ;
   char __size[48] ;
   long long __align ;
};
 
:-1: Warning: Incompatible declaration for pthread_cond_broadcast (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1714 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i (0)) 
	Failed assumption that pthread_cond_t and pthread_cond_t are isomorphic 
	Failed assumption that union __anonunion_pthread_cond_t_51417149 and union __anonunion_pthread_cond_t_951761805 are isomorphic (different number of fields in __anonstruct___data_282018390 and __pthread_cond_s: 8 != 7.)
union __anonunion_pthread_cond_t_51417149 {
   struct __anonstruct___data_282018390 __data ;
   char __size[48] ;
   long long __align ;
};

union __anonunion_pthread_cond_t_951761805 {
   struct __pthread_cond_s __data ;
   char __size[48] ;
   long long __align ;
};
 
:-1: Warning: Incompatible declaration for pthread_cond_wait (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1716 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i (0)) 
	Failed assumption that pthread_cond_t and pthread_cond_t are isomorphic 
	Failed assumption that union __anonunion_pthread_cond_t_51417149 and union __anonunion_pthread_cond_t_951761805 are isomorphic (different number of fields in __anonstruct___data_282018390 and __pthread_cond_s: 8 != 7.)
union __anonunion_pthread_cond_t_51417149 {
   struct __anonstruct___data_282018390 __data ;
   char __size[48] ;
   long long __align ;
};

union __anonunion_pthread_cond_t_951761805 {
   struct __pthread_cond_s __data ;
   char __size[48] ;
   long long __align ;
};
 
:-1: Warning: Incompatible declaration for pthread_cond_timedwait (from .goblint/preprocessed/pthread.i(2)).
 Previous was at /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1719 (from /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i (0)) 
	Failed assumption that pthread_cond_t and pthread_cond_t are isomorphic 
	Failed assumption that union __anonunion_pthread_cond_t_51417149 and union __anonunion_pthread_cond_t_951761805 are isomorphic (different number of fields in __anonstruct___data_282018390 and __pthread_cond_s: 8 != 7.)
union __anonunion_pthread_cond_t_51417149 {
   struct __anonstruct___data_282018390 __data ;
   char __size[48] ;
   long long __align ;
};

union __anonunion_pthread_cond_t_951761805 {
   struct __pthread_cond_s __data ;
   char __size[48] ;
   long long __align ;
};
 
[Info] Enabled congruence domain.
[Info] Enabled widening thresholds
[Info] Enabled octagon domain for:
[Info] __VERIFIER_atomic_begin, __VERIFIER_atomic_end, i, key, count, a, tmp, count, i, j, i___0, j___0, k, size, r, top, i, elem, i, index, head1, tmp, tmp___0, next1, head1, tmp, tmp___0, tmp___1, tmp___2, i, pushCount, obj, v, old, obj, v, old, obj, expected, desired, ret, obj, v, t, obj, v
[Info] SV-COMP specification: CHECK( init(main()), LTL(G ! call(reach_error())) )
[Info][Witness] unassume invariant: ((((pushCount == 3 && 3 == pushCount) && (2147483650LL - (long long )i) - (long long )pushCount >= 0LL) && (2147483651LL + (long long )i) - (long long )pushCount >= 0LL) && (2147483644LL - (long long )i) + (long long )pushCount >= 0LL) && (2147483645LL + (long long )i) + (long long )pushCount >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1847:1-1857:1)
[Info][Witness] unassume invariant: (-1 <= v && v <= 3) || (0 <= v && v <= 2) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1798:5-1798:30)
[Info][Witness] unassume invariant: (stack.count == 3 && stack.head == 0) || (0 <= stack.head && stack.head <= 2) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1799:5-1799:13)
[Info][Witness] unassume invariant: (((3 == pushCount && (2147483650LL - (long long )i) - (long long )pushCount >= 0LL) && (2147483651LL + (long long )i) - (long long )pushCount >= 0LL) && (2147483644LL - (long long )i) + (long long )pushCount >= 0LL) && (2147483645LL + (long long )i) + (long long )pushCount >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1850:5-1850:42)
[Info][Witness] unassume invariant: (((3 == pushCount && (2147483650LL - (long long )i) - (long long )pushCount >= 0LL) && (2147483651LL + (long long )i) - (long long )pushCount >= 0LL) && (2147483644LL - (long long )i) + (long long )pushCount >= 0LL) && (2147483645LL + (long long )i) + (long long )pushCount >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1851:5-1851:33)
[Info][Witness] unassume invariant: ((((((((pushCount == 3 && stack.head == 0) && stack.count == 3) && 3 == pushCount) && (5LL - (long long )i) - (long long )pushCount >= 0LL) && (3LL + (long long )i) - (long long )pushCount >= 0LL) && (-1LL - (long long )i) + (long long )pushCount >= 0LL) && (-3LL + (long long )i) + (long long )pushCount >= 0LL) && i <= 2) && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1852:9-1852:39)
[Info][Witness] unassume invariant: (((((3 == pushCount && (4LL - (long long )i) - (long long )pushCount >= 0LL) && (3LL + (long long )i) - (long long )pushCount >= 0LL) && (-2LL - (long long )i) + (long long )pushCount >= 0LL) && (-3LL + (long long )i) + (long long )pushCount >= 0LL) && i <= 1) && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1852:9-1852:39)
[Info][Witness] unassume invariant: ((((((((pushCount == 3 && stack.head == 0) && stack.count == 3) && 3 == pushCount) && (5LL - (long long )i) - (long long )pushCount >= 0LL) && (3LL + (long long )i) - (long long )pushCount >= 0LL) && (-1LL - (long long )i) + (long long )pushCount >= 0LL) && (-3LL + (long long )i) + (long long )pushCount >= 0LL) && i <= 2) && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1852:9-1852:39)
[Info][Witness] unassume invariant: ((((pushCount == 3 && 3 == pushCount) && (5LL - (long long )i) - (long long )pushCount >= 0LL) && (1LL + (long long )i) - (long long )pushCount >= 0LL) && (-1LL - (long long )i) + (long long )pushCount >= 0LL) && (-5LL + (long long )i) + (long long )pushCount >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1852:9-1852:39)
[Info][Witness] unassume invariant: (((3 == pushCount && (5LL - (long long )i) - (long long )pushCount >= 0LL) && (1LL + (long long )i) - (long long )pushCount >= 0LL) && (-1LL - (long long )i) + (long long )pushCount >= 0LL) && (-5LL + (long long )i) + (long long )pushCount >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1856:5-1856:55)
[Info][Witness] unassume invariant: (((0 == i && stack.count == 3) && stack.head == 0) && i == 0) || (1 <= i && i <= 3) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1912:9-1912:27)
[Info][Witness] unassume invariant: (0 == i && i == 0) || (1 <= i && i <= 2) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1912:9-1912:27)
[Info][Witness] unassume invariant: ((((6442450942LL - (long long )elem) - (long long )i >= 0LL && (6442450943LL + (long long )elem) - (long long )i >= 0LL) && (2147483647LL - (long long )elem) + (long long )i >= 0LL) && (2147483648LL + (long long )elem) + (long long )i >= 0LL) && (unsigned long )arg <= 2UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1889:1-1907:1)
[Info][Witness] unassume invariant: ((((((unsigned long )arg == (unsigned long )idx && (6442450942LL - (long long )elem) - (long long )i >= 0LL) && (6442450943LL + (long long )elem) - (long long )i >= 0LL) && (2147483647LL - (long long )elem) + (long long )i >= 0LL) && (2147483648LL + (long long )elem) + (long long )i >= 0LL) && idx <= 2) && 0 <= idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1892:9-1892:31)
[Info][Witness] unassume invariant: ((((((unsigned long )arg == (unsigned long )idx && (2147483648LL + (long long )elem) - (long long )i >= 0LL) && (2147483648LL + (long long )elem) + (long long )i >= 0LL) && (unsigned long )arg <= 2UL) && idx <= 2) && i <= 2U) && 0 <= idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1893:9-1893:27)
[Info][Witness] unassume invariant: (((((unsigned long )arg == (unsigned long )idx && (unsigned long )arg <= 2UL) && idx <= 2) && i <= 1U) && 0 <= idx) && (unsigned long )arg == (unsigned long )idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1899:17-1899:26)
[Info][Witness] unassume invariant: (((((unsigned long )arg == (unsigned long )idx && (unsigned long )arg <= 2UL) && idx <= 2) && i <= 1U) && 0 <= idx) && (unsigned long )arg == (unsigned long )idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1893:9-1893:27)
[Info][Witness] unassume invariant: ((next1 <= 2 && head1 <= 2) && 0 <= next1) && 0 <= head1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1867:17-1867:72)
[Info][Witness] unassume invariant: (2147483648LL - (long long )t) + (long long )v >= 0LL && (2147483649LL + (long long )t) + (long long )v >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1806:1-1813:1)
[Info][Witness] unassume invariant: (2147483648LL - (long long )t) + (long long )v >= 0LL && (2147483649LL + (long long )t) + (long long )v >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1808:5-1808:30)
[Info][Witness] unassume invariant: ((t <= 2 && v <= 2) && -1 <= t) && -1 <= v (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1809:9-1809:17)
[Info][Witness] unassume invariant: t <= 2 && -1 <= t (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1811:5-1811:28)
[Info][Witness] unassume invariant: ((((unsigned long )obj == (unsigned long )(& stack.head) && (0 <= *obj && *obj <= 2)) || (unsigned long )obj == (unsigned long )(& stack.count)) && stack.head <= 2) && 0 <= stack.head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1802:1-1805:1)
[Info][Witness] unassume invariant: head1 <= 2 && 0 <= head1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1862:13-1862:45)
[Info][Witness] unassume invariant: ((next1 <= 2 && head1 <= 2) && 0 <= head1) && -1 <= next1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1863:13-1863:66)
[Info][Witness] unassume invariant: head1 <= 2 && 0 <= head1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1864:13-1864:23)
[Info][Witness] unassume invariant: ((unsigned long )obj == (unsigned long )(& stack.head) && (1LL + (long long )desired) - (long long )ret >= 0LL) && (long long )desired + (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1814:1-1830:1)
[Info][Witness] unassume invariant: ((((int )ret == 0 && (unsigned long )obj == (unsigned long )(& stack.head)) && 0 == (int )ret) && (long long )desired - (long long )ret >= 0LL) && (long long )desired + (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1816:11-1816:18)
[Info][Witness] unassume invariant: (((((((((0 <= *expected && *expected <= 2) || (0 <= *expected && *expected <= 2)) && (unsigned long )obj == (unsigned long )(& stack.head)) && 0 == (int )ret) && (long long )desired - (long long )ret >= 0LL) && (long long )desired + (long long )ret >= 0LL) && *obj <= 2) && stack.head <= 2) && 0 <= *obj) && 0 <= stack.head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1817:5-1817:30)
[Info][Witness] unassume invariant: (((((((unsigned long )obj == (unsigned long )(& stack.head) && 0 == (int )ret) && (long long )desired - (long long )ret >= 0LL) && (long long )desired + (long long )ret >= 0LL) && *obj <= 2) && desired <= 2) && 0 <= *obj) && 0 <= desired (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1818:8-1818:25)
[Info][Witness] unassume invariant: (((((unsigned long )obj == (unsigned long )(& stack.head) && 0 == (int )ret) && (long long )desired - (long long )ret >= 0LL) && (long long )desired + (long long )ret >= 0LL) && stack.head <= 2) && 0 <= stack.head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1820:9-1820:23)
[Info][Witness] unassume invariant: ((((int )ret == 0 || (int )ret == 1) && (unsigned long )obj == (unsigned long )(& stack.head)) && (1LL + (long long )desired) - (long long )ret >= 0LL) && (long long )desired + (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1821:9-1821:16)
[Info][Witness] unassume invariant: (((((((((0 <= *expected && *expected <= 2) || (0 <= *expected && *expected <= 2)) && (unsigned long )obj == (unsigned long )(& stack.head)) && 0 == (int )ret) && (long long )desired - (long long )ret >= 0LL) && (long long )desired + (long long )ret >= 0LL) && *obj <= 2) && stack.head <= 2) && 0 <= *obj) && 0 <= stack.head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1818:8-1818:25)
[Info][Witness] unassume invariant: (((unsigned long )obj == (unsigned long )(& stack.head) && 0 == (int )ret) && (long long )desired - (long long )ret >= 0LL) && (long long )desired + (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1825:9-1825:25)
[Info][Witness] unassume invariant: ((((int )ret == 0 || (int )ret == 1) && (unsigned long )obj == (unsigned long )(& stack.head)) && (1LL + (long long )desired) - (long long )ret >= 0LL) && (long long )desired + (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1826:9-1826:16)
[Info][Witness] unassume invariant: ((((int )ret == 0 || (int )ret == 1) && (unsigned long )obj == (unsigned long )(& stack.head)) && (1LL + (long long )desired) - (long long )ret >= 0LL) && (long long )desired + (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1828:5-1828:28)
[Info][Witness] unassume invariant: (((((unsigned long )obj == (unsigned long )(& stack.count) && 1 == v) && (2147483648LL - (long long )old) - (long long )v >= 0LL) && (2147483649LL + (long long )old) - (long long )v >= 0LL) && (2147483646LL - (long long )old) + (long long )v >= 0LL) && (2147483647LL + (long long )old) + (long long )v >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1839:1-1846:1)
[Info][Witness] unassume invariant: (((((unsigned long )obj == (unsigned long )(& stack.count) && 1 == v) && (2147483648LL - (long long )old) - (long long )v >= 0LL) && (2147483649LL + (long long )old) - (long long )v >= 0LL) && (2147483646LL - (long long )old) + (long long )v >= 0LL) && (2147483647LL + (long long )old) + (long long )v >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1841:5-1841:30)
[Info][Witness] unassume invariant: (v == 1 && (unsigned long )obj == (unsigned long )(& stack.count)) && 1 == v (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1842:9-1842:19)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1843:5-1843:20)
[Info][Witness] unassume invariant: (unsigned long )obj == (unsigned long )(& stack.count) && 1 == v (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1843:5-1843:20)
[Info][Witness] unassume invariant: (unsigned long )obj == (unsigned long )(& stack.count) && 1 == v (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1844:5-1844:28)
[Info][Witness] unassume invariant: head1 <= 2 && 0 <= head1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1869:17-1869:50)
[Info][Witness] unassume invariant: (((unsigned long )arg == (unsigned long )idx && elem <= 2) && i <= 1U) && -1 <= elem (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1898:13-1898:25)
[Info][Witness] unassume invariant: ((((((unsigned long )arg == (unsigned long )idx && (1LL + (long long )elem) - (long long )i >= 0LL) && (long long )elem + (long long )i >= 0LL) && elem <= 2) && idx <= 2) && 0 <= elem) && 0 <= idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1899:17-1899:26)
[Info][Witness] unassume invariant: ((((((unsigned long )arg == (unsigned long )idx && (1LL + (long long )elem) - (long long )i >= 0LL) && (long long )elem + (long long )i >= 0LL) && elem <= 2) && idx <= 2) && 0 <= elem) && 0 <= idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1902:9-1902:38)
[Info][Witness] unassume invariant: ((unsigned long )arg == (unsigned long )idx && (1LL + (long long )elem) - (long long )i >= 0LL) && (long long )elem + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1903:12-1903:45)
[Info][Witness] unassume invariant: ((((unsigned long )arg == (unsigned long )idx && (1LL + (long long )elem) - (long long )i >= 0LL) && (long long )elem + (long long )i >= 0LL) && elem <= 2) && 0 <= elem (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1903:12-1903:45)
[Info][Witness] unassume invariant: (2147483647LL - (long long )head1) + (long long )index >= 0LL && (2147483648LL + (long long )head1) + (long long )index >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1880:1-1888:1)
[Info][Witness] unassume invariant: ((((((head1 <= 2 && index <= 2) && 0 <= head1) && 0 <= index) && head1 <= 2) && index <= 2) && 0 <= head1) && 0 <= index (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1882:9-1882:41)
[Info][Witness] unassume invariant: ((((((head1 <= 2 && index <= 2) && 0 <= head1) && 0 <= index) && head1 <= 2) && index <= 2) && 0 <= head1) && 0 <= index (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1886:14-1886:73)
[Info][Witness] unassume invariant: (((((unsigned long )obj == (unsigned long )(& stack.count) && 1 == v) && (2147483648LL - (long long )old) - (long long )v >= 0LL) && (2147483649LL + (long long )old) - (long long )v >= 0LL) && (2147483646LL - (long long )old) + (long long )v >= 0LL) && (2147483647LL + (long long )old) + (long long )v >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1831:1-1838:1)
[Info][Witness] unassume invariant: (((((unsigned long )obj == (unsigned long )(& stack.count) && 1 == v) && (2147483648LL - (long long )old) - (long long )v >= 0LL) && (2147483649LL + (long long )old) - (long long )v >= 0LL) && (2147483646LL - (long long )old) + (long long )v >= 0LL) && (2147483647LL + (long long )old) + (long long )v >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1833:5-1833:30)
[Info][Witness] unassume invariant: (v == 1 && (unsigned long )obj == (unsigned long )(& stack.count)) && 1 == v (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1834:9-1834:19)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1835:5-1835:20)
[Info][Witness] unassume invariant: (unsigned long )obj == (unsigned long )(& stack.count) && 1 == v (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1835:5-1835:20)
[Info][Witness] unassume invariant: (unsigned long )obj == (unsigned long )(& stack.count) && 1 == v (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1836:5-1836:28)
[Info][Witness] unassume invariant: ((((((unsigned long )arg == (unsigned long )idx && (2147483648LL + (long long )elem) - (long long )i >= 0LL) && (2147483648LL + (long long )elem) + (long long )i >= 0LL) && (unsigned long )arg <= 2UL) && idx <= 2) && i <= 2U) && 0 <= idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1893:9-1893:27)
[Info][Witness] unassume invariant: ((unsigned long )arg == (unsigned long )idx && (2147483648LL + (long long )elem) - (long long )i >= 0LL) && (2147483644LL + (long long )elem) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1893:9-1893:27)
[Info][Witness] unassume invariant: (((0 == i && stack.count == 3) && stack.head == 0) && i == 0) || (1 <= i && i <= 3) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1912:9-1912:27)
[Info][Witness] unassume invariant: i == 3 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1912:9-1912:27)
[Info][Witness] unassume invariant: i <= 3 && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1915:9-1915:27)
[Info][Witness] unassume invariant: i <= 2 && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1915:9-1915:27)
[Info][Witness] unassume invariant: i <= 3 && 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1915:9-1915:27)
[Warning][Deadcode] Function '__bswap_32' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:352:1-356:1)
[Warning][Deadcode] Function '__bswap_64' is uncalled: 1 LLoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:357:1-361:1)
[Info][Deadcode] Logical lines of code (LLoC) summary:
  live: 76
  dead: 2 (2 in uncalled functions)
  total lines: 78
[Warning][Race] Memory location stack.array[?].Value (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1795:11-1795:16)
  write with region:{stack.array[?].Value} (conf. 110)  (exp: & stack.array[elem].Value) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1902:9-1902:38)
  write with [region:{stack.array[?].Value}, thread:[main, thread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1913:9-1913:68]] (conf. 110)  (exp: & stack.array[elem].Value) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1902:9-1902:38)
  read with region:{stack.array[?].Value} (conf. 110)  (exp: & stack.array[elem].Value) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1903:12-1903:45)
  read with [region:{stack.array[?].Value}, thread:[main, thread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1913:9-1913:68]] (conf. 110)  (exp: & stack.array[elem].Value) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1903:12-1903:45)
[Warning][Race] Memory location stack.count (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1795:11-1795:16)
  write with [region:{stack.count}, lock:{[__VERIFIER_atomic]}] (conf. 110)  (exp: & *obj) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1835:5-1835:20)
  write with [region:{stack.count}, lock:{[__VERIFIER_atomic]}, thread:[main, thread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1913:9-1913:68]] (conf. 110)  (exp: & *obj) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1835:5-1835:20)
  write with [region:{stack.count}, lock:{[__VERIFIER_atomic]}] (conf. 110)  (exp: & *obj) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1843:5-1843:20)
  write with [region:{stack.count}, lock:{[__VERIFIER_atomic]}, thread:[main, thread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1913:9-1913:68]] (conf. 110)  (exp: & *obj) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1843:5-1843:20)
  read with region:{stack.count} (conf. 110)  (exp: & *obj) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1804:12-1804:16)
  read with [region:{stack.count}, thread:[main, thread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1913:9-1913:68]] (conf. 110)  (exp: & *obj) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1804:12-1804:16)
[Warning][Race] Memory location stack.head (race with conf. 110): (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1795:11-1795:16)
  write with [region:{stack.head}, lock:{[__VERIFIER_atomic]}] (conf. 110)  (exp: & *obj) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1820:9-1820:23)
  write with [region:{stack.head}, lock:{[__VERIFIER_atomic]}, thread:[main, thread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1913:9-1913:68]] (conf. 110)  (exp: & *obj) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1820:9-1820:23)
  read with region:{stack.head} (conf. 110)  (exp: & *obj) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1804:12-1804:16)
  read with [region:{stack.head}, thread:[main, thread@/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1913:9-1913:68]] (conf. 110)  (exp: & *obj) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1804:12-1804:16)
[Warning][Deadcode][CWE-570] condition '0' is always false (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:12:73-12:74)
[Success][Witness] invariant confirmed: 1 == v (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1836:5)
[Success][Witness] invariant confirmed: obj == & stack.count (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1836:5)
[Success][Witness] invariant confirmed: 1 == v (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1837:5)
[Success][Witness] invariant confirmed: obj == & stack.count (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1837:5)
[Warning][Witness] invariant unconfirmed: 0 <= index (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1885:9)
[Warning][Witness] invariant unconfirmed: 0 <= head1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1885:9)
[Warning][Witness] invariant unconfirmed: index <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1885:9)
[Warning][Witness] invariant unconfirmed: head1 <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1885:9)
[Warning][Witness] invariant unconfirmed: 0 <= head1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1870:17)
[Warning][Witness] invariant unconfirmed: head1 <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1870:17)
[Success][Witness] invariant confirmed: (2147483647LL + (long long )old) + (long long )v >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1841:5)
[Success][Witness] invariant confirmed: (2147483646LL - (long long )old) + (long long )v >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1841:5)
[Success][Witness] invariant confirmed: (2147483649LL + (long long )old) - (long long )v >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1841:5)
[Success][Witness] invariant confirmed: (2147483648LL - (long long )old) - (long long )v >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1841:5)
[Success][Witness] invariant confirmed: 1 == v (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1841:5)
[Success][Witness] invariant confirmed: obj == & stack.count (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1841:5)
[Warning][Witness] invariant unconfirmed: (long long )desired + (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1817:5)
[Warning][Witness] invariant unconfirmed: (long long )desired - (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1817:5)
[Success][Witness] invariant confirmed: (_Bool)0 == ret (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1817:5)
[Success][Witness] invariant confirmed: obj == & stack.head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1817:5)
[Success][Witness] invariant confirmed: ret == (_Bool)0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1817:5)
[Success][Witness] invariant confirmed: 1 == v (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1845:5)
[Success][Witness] invariant confirmed: obj == & stack.count (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1845:5)
[Success][Witness] invariant confirmed: (2147483645LL + (long long )i) + (long long )pushCount >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1851:5)
[Success][Witness] invariant confirmed: (2147483644LL - (long long )i) + (long long )pushCount >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1851:5)
[Success][Witness] invariant confirmed: (2147483651LL + (long long )i) - (long long )pushCount >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1851:5)
[Success][Witness] invariant confirmed: (2147483650LL - (long long )i) - (long long )pushCount >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1851:5)
[Success][Witness] invariant confirmed: 3 == pushCount (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1851:5)
[Warning][Witness] invariant unconfirmed: arg == idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1898:13)
[Success][Witness] invariant confirmed: 1 == v (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1843:5)
[Success][Witness] invariant confirmed: obj == & stack.count (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1843:5)
[Success][Witness] invariant confirmed: v == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1843:5)
[Success][Witness] invariant confirmed: 0 <= idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1902:9)
[Success][Witness] invariant confirmed: 0 <= elem (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1902:9)
[Success][Witness] invariant confirmed: idx <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1902:9)
[Warning][Witness] invariant unconfirmed: elem <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1902:9)
[Success][Witness] invariant confirmed: (long long )elem + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1902:9)
[Success][Witness] invariant confirmed: (1LL + (long long )elem) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1902:9)
[Warning][Witness] invariant unconfirmed: arg == idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1902:9)
[Warning][Witness] invariant unconfirmed: (2147483649LL + (long long )t) + (long long )v >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1809:5)
[Warning][Witness] invariant unconfirmed: (2147483648LL - (long long )t) + (long long )v >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1809:5)
[Warning][Witness] invariant unconfirmed: (-1 <= v && v <= 3) || (0 <= v && v <= 2) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1799:5)
[Success][Witness] invariant confirmed: 0 <= idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1903:9)
[Success][Witness] invariant confirmed: 0 <= elem (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1903:9)
[Success][Witness] invariant confirmed: idx <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1903:9)
[Warning][Witness] invariant unconfirmed: elem <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1903:9)
[Success][Witness] invariant confirmed: (long long )elem + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1903:9)
[Success][Witness] invariant confirmed: (1LL + (long long )elem) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1903:9)
[Warning][Witness] invariant unconfirmed: arg == idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1903:9)
[Warning][Witness] invariant unconfirmed: 0 <= head1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1863:9)
[Warning][Witness] invariant unconfirmed: head1 <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1863:9)
[Success][Witness] invariant confirmed: (long long )elem + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1903:48)
[Success][Witness] invariant confirmed: (1LL + (long long )elem) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1903:48)
[Warning][Witness] invariant unconfirmed: arg == idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1903:48)
[Warning][Witness] invariant unconfirmed: 0 <= stack.head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1804:5)
[Warning][Witness] invariant unconfirmed: stack.head <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1804:5)
[Warning][Witness] invariant unconfirmed: (obj == & stack.head && (0 <= *obj && *obj <= 2)) || obj == & stack.count (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1804:5)
[Warning][Witness] invariant unconfirmed: (long long )desired + (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1816:5)
[Warning][Witness] invariant unconfirmed: (1LL + (long long )desired) - (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1816:5)
[Success][Witness] invariant confirmed: obj == & stack.head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1816:5)
[Warning][Witness] invariant unconfirmed: 0 <= stack.head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1818:5)
[Warning][Witness] invariant unconfirmed: 0 <= *obj (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1818:5)
[Warning][Witness] invariant unconfirmed: stack.head <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1818:5)
[Warning][Witness] invariant unconfirmed: *obj <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1818:5)
[Warning][Witness] invariant unconfirmed: (long long )desired + (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1818:5)
[Warning][Witness] invariant unconfirmed: (long long )desired - (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1818:5)
[Success][Witness] invariant confirmed: (_Bool)0 == ret (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1818:5)
[Success][Witness] invariant confirmed: obj == & stack.head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1818:5)
[Warning][Witness] invariant unconfirmed: (0 <= *expected && *expected <= 2) || (0 <= *expected && *expected <= 2) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1818:5)
[Success][Witness] invariant confirmed: (-5LL + (long long )i) + (long long )pushCount >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1857:1)
[Success][Witness] invariant confirmed: (-1LL - (long long )i) + (long long )pushCount >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1857:1)
[Success][Witness] invariant confirmed: (1LL + (long long )i) - (long long )pushCount >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1857:1)
[Success][Witness] invariant confirmed: (5LL - (long long )i) - (long long )pushCount >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1857:1)
[Success][Witness] invariant confirmed: 3 == pushCount (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1857:1)
[Success][Witness] invariant confirmed: (0 == i && i == 0) || (1 <= i && i <= 2) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1913:9)
[Success][Witness] invariant confirmed: (2147483644LL + (long long )elem) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1906:5)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )elem) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1906:5)
[Warning][Witness] invariant unconfirmed: arg == idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1906:5)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )head1) + (long long )index >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1882:5)
[Success][Witness] invariant confirmed: (2147483647LL - (long long )head1) + (long long )index >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1882:5)
[Warning][Witness] invariant unconfirmed: -1 <= next1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1864:9)
[Warning][Witness] invariant unconfirmed: 0 <= head1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1864:9)
[Warning][Witness] invariant unconfirmed: head1 <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1864:9)
[Warning][Witness] invariant unconfirmed: next1 <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1864:9)
[Success][Witness] invariant confirmed: 0 <= idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1893:5)
[Success][Witness] invariant confirmed: idx <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1893:5)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )elem) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1893:5)
[Success][Witness] invariant confirmed: (2147483647LL - (long long )elem) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1893:5)
[Success][Witness] invariant confirmed: (6442450943LL + (long long )elem) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1893:5)
[Success][Witness] invariant confirmed: (6442450942LL - (long long )elem) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1893:5)
[Warning][Witness] invariant unconfirmed: arg == idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1893:5)
[Success][Witness] invariant confirmed: (unsigned long )arg <= 2UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1892:5)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )elem) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1892:5)
[Success][Witness] invariant confirmed: (2147483647LL - (long long )elem) + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1892:5)
[Success][Witness] invariant confirmed: (6442450943LL + (long long )elem) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1892:5)
[Success][Witness] invariant confirmed: (6442450942LL - (long long )elem) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1892:5)
[Warning][Witness] invariant unconfirmed: 0 <= head1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1874:17)
[Success][Witness] invariant confirmed: 0 <= next1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1874:17)
[Warning][Witness] invariant unconfirmed: head1 <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1874:17)
[Warning][Witness] invariant unconfirmed: next1 <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1874:17)
[Success][Witness] invariant confirmed: (2147483647LL + (long long )old) + (long long )v >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1842:5)
[Success][Witness] invariant confirmed: (2147483646LL - (long long )old) + (long long )v >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1842:5)
[Success][Witness] invariant confirmed: (2147483649LL + (long long )old) - (long long )v >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1842:5)
[Success][Witness] invariant confirmed: (2147483648LL - (long long )old) - (long long )v >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1842:5)
[Success][Witness] invariant confirmed: 1 == v (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1842:5)
[Success][Witness] invariant confirmed: obj == & stack.count (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1842:5)
[Warning][Witness] invariant unconfirmed: (long long )desired + (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1829:5)
[Warning][Witness] invariant unconfirmed: (1LL + (long long )desired) - (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1829:5)
[Success][Witness] invariant confirmed: obj == & stack.head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1829:5)
[Success][Witness] invariant confirmed: ret == (_Bool)0 || ret == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1829:5)
[Warning][Witness] invariant unconfirmed: -1 <= v (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1810:5)
[Warning][Witness] invariant unconfirmed: -1 <= t (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1810:5)
[Warning][Witness] invariant unconfirmed: v <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1810:5)
[Warning][Witness] invariant unconfirmed: t <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1810:5)
[Warning][Witness] invariant unconfirmed: 0 <= desired (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1820:9)
[Warning][Witness] invariant unconfirmed: 0 <= *obj (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1820:9)
[Warning][Witness] invariant unconfirmed: desired <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1820:9)
[Warning][Witness] invariant unconfirmed: *obj <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1820:9)
[Warning][Witness] invariant unconfirmed: (long long )desired + (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1820:9)
[Warning][Witness] invariant unconfirmed: (long long )desired - (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1820:9)
[Success][Witness] invariant confirmed: (_Bool)0 == ret (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1820:9)
[Success][Witness] invariant confirmed: obj == & stack.head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1820:9)
[Success][Witness] invariant confirmed: (2147483645LL + (long long )i) + (long long )pushCount >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1852:5)
[Success][Witness] invariant confirmed: (2147483644LL - (long long )i) + (long long )pushCount >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1852:5)
[Success][Witness] invariant confirmed: (2147483651LL + (long long )i) - (long long )pushCount >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1852:5)
[Success][Witness] invariant confirmed: (2147483650LL - (long long )i) - (long long )pushCount >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1852:5)
[Success][Witness] invariant confirmed: 3 == pushCount (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1852:5)
[Warning][Witness] invariant unconfirmed: 0 <= stack.head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1821:9)
[Warning][Witness] invariant unconfirmed: stack.head <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1821:9)
[Warning][Witness] invariant unconfirmed: (long long )desired + (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1821:9)
[Warning][Witness] invariant unconfirmed: (long long )desired - (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1821:9)
[Success][Witness] invariant confirmed: (_Bool)0 == ret (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1821:9)
[Success][Witness] invariant confirmed: obj == & stack.head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1821:9)
[Warning][Witness] invariant unconfirmed: (stack.count == 3 && stack.head == 0) || (0 <= stack.head && stack.head <= 2) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1800:5)
[Success][Witness] invariant confirmed: (2147483647LL + (long long )old) + (long long )v >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1834:5)
[Success][Witness] invariant confirmed: (2147483646LL - (long long )old) + (long long )v >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1834:5)
[Success][Witness] invariant confirmed: (2147483649LL + (long long )old) - (long long )v >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1834:5)
[Success][Witness] invariant confirmed: (2147483648LL - (long long )old) - (long long )v >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1834:5)
[Success][Witness] invariant confirmed: 1 == v (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1834:5)
[Success][Witness] invariant confirmed: obj == & stack.count (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1834:5)
[Warning][Witness] invariant unconfirmed: (long long )desired + (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1828:5)
[Warning][Witness] invariant unconfirmed: (1LL + (long long )desired) - (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1828:5)
[Success][Witness] invariant confirmed: obj == & stack.head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1828:5)
[Success][Witness] invariant confirmed: ret == (_Bool)0 || ret == (_Bool)1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1828:5)
[Success][Witness] invariant confirmed: i == 3 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1915:5)
[Success][Witness] invariant confirmed: (2147483645LL + (long long )i) + (long long )pushCount >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1850:5)
[Success][Witness] invariant confirmed: (2147483644LL - (long long )i) + (long long )pushCount >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1850:5)
[Success][Witness] invariant confirmed: (2147483651LL + (long long )i) - (long long )pushCount >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1850:5)
[Success][Witness] invariant confirmed: (2147483650LL - (long long )i) - (long long )pushCount >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1850:5)
[Success][Witness] invariant confirmed: 3 == pushCount (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1850:5)
[Success][Witness] invariant confirmed: pushCount == 3 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1850:5)
[Warning][Witness] invariant unconfirmed: -1 <= t (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1812:5)
[Warning][Witness] invariant unconfirmed: t <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1812:5)
[Success][Witness] invariant confirmed: 1 == v (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1844:5)
[Success][Witness] invariant confirmed: obj == & stack.count (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1844:5)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1916:9)
[Success][Witness] invariant confirmed: i <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1916:9)
[Warning][Witness] invariant unconfirmed: (long long )desired + (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1826:9)
[Warning][Witness] invariant unconfirmed: (long long )desired - (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1826:9)
[Success][Witness] invariant confirmed: (_Bool)0 == ret (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1826:9)
[Success][Witness] invariant confirmed: obj == & stack.head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1826:9)
[Warning][Witness] invariant unconfirmed: 0 <= head1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1866:13)
[Warning][Witness] invariant unconfirmed: head1 <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1866:13)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1854:9)
[Success][Witness] invariant confirmed: i <= 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1854:9)
[Success][Witness] invariant confirmed: (-3LL + (long long )i) + (long long )pushCount >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1854:9)
[Success][Witness] invariant confirmed: (-2LL - (long long )i) + (long long )pushCount >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1854:9)
[Success][Witness] invariant confirmed: (3LL + (long long )i) - (long long )pushCount >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1854:9)
[Success][Witness] invariant confirmed: (4LL - (long long )i) - (long long )pushCount >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1854:9)
[Success][Witness] invariant confirmed: 3 == pushCount (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1854:9)
[Success][Witness] invariant confirmed: 0 <= elem (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1904:9)
[Warning][Witness] invariant unconfirmed: elem <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1904:9)
[Success][Witness] invariant confirmed: (long long )elem + (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1904:9)
[Success][Witness] invariant confirmed: (1LL + (long long )elem) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1904:9)
[Warning][Witness] invariant unconfirmed: arg == idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1904:9)
[Success][Witness] invariant confirmed: 1 == v (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1835:5)
[Success][Witness] invariant confirmed: obj == & stack.count (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1835:5)
[Success][Witness] invariant confirmed: v == 1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1835:5)
[Success][Witness] invariant confirmed: (-5LL + (long long )i) + (long long )pushCount >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1856:5)
[Success][Witness] invariant confirmed: (-1LL - (long long )i) + (long long )pushCount >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1856:5)
[Success][Witness] invariant confirmed: (1LL + (long long )i) - (long long )pushCount >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1856:5)
[Success][Witness] invariant confirmed: (5LL - (long long )i) - (long long )pushCount >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1856:5)
[Success][Witness] invariant confirmed: 3 == pushCount (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1856:5)
[Success][Witness] invariant confirmed: pushCount == 3 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1856:5)
[Success][Witness] invariant confirmed: (2147483647LL + (long long )old) + (long long )v >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1833:5)
[Success][Witness] invariant confirmed: (2147483646LL - (long long )old) + (long long )v >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1833:5)
[Success][Witness] invariant confirmed: (2147483649LL + (long long )old) - (long long )v >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1833:5)
[Success][Witness] invariant confirmed: (2147483648LL - (long long )old) - (long long )v >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1833:5)
[Success][Witness] invariant confirmed: 1 == v (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1833:5)
[Success][Witness] invariant confirmed: obj == & stack.count (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1833:5)
[Warning][Witness] invariant unconfirmed: -1 <= elem (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1899:13)
[Success][Witness] invariant confirmed: i <= 1U (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1899:13)
[Warning][Witness] invariant unconfirmed: elem <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1899:13)
[Warning][Witness] invariant unconfirmed: arg == idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1899:13)
[Warning][Witness] invariant unconfirmed: 0 <= stack.head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1825:9)
[Warning][Witness] invariant unconfirmed: 0 <= *obj (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1825:9)
[Warning][Witness] invariant unconfirmed: stack.head <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1825:9)
[Warning][Witness] invariant unconfirmed: *obj <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1825:9)
[Warning][Witness] invariant unconfirmed: (long long )desired + (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1825:9)
[Warning][Witness] invariant unconfirmed: (long long )desired - (long long )ret >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1825:9)
[Success][Witness] invariant confirmed: (_Bool)0 == ret (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1825:9)
[Success][Witness] invariant confirmed: obj == & stack.head (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1825:9)
[Warning][Witness] invariant unconfirmed: (0 <= *expected && *expected <= 2) || (0 <= *expected && *expected <= 2) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1825:9)
[Warning][Witness] invariant unconfirmed: (2147483649LL + (long long )t) + (long long )v >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1808:5)
[Warning][Witness] invariant unconfirmed: (2147483648LL - (long long )t) + (long long )v >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1808:5)
[Success][Witness] invariant confirmed: 0 <= idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1896:9)
[Success][Witness] invariant confirmed: i <= 1U (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1896:9)
[Success][Witness] invariant confirmed: idx <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1896:9)
[Success][Witness] invariant confirmed: (unsigned long )arg <= 2UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1896:9)
[Warning][Witness] invariant unconfirmed: arg == idx (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1896:9)
[Warning][Witness] invariant unconfirmed: (((0 == i && stack.count == 3) && stack.head == 0) && i == 0) || (1 <= i && i <= 3) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1912:5)
[Warning][Witness] invariant unconfirmed: i <= 2U (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1893:5)
[Success][Witness] invariant confirmed: (unsigned long )arg <= 2UL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1893:5)
[Success][Witness] invariant confirmed: (2147483648LL + (long long )elem) - (long long )i >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1893:5)
[Warning][Witness] invariant unconfirmed: 0 <= index (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1883:5)
[Warning][Witness] invariant unconfirmed: 0 <= head1 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1883:5)
[Warning][Witness] invariant unconfirmed: index <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1883:5)
[Warning][Witness] invariant unconfirmed: head1 <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1883:5)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1852:5)
[Success][Witness] invariant confirmed: i <= 2 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1852:5)
[Success][Witness] invariant confirmed: (-3LL + (long long )i) + (long long )pushCount >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1852:5)
[Success][Witness] invariant confirmed: (-1LL - (long long )i) + (long long )pushCount >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1852:5)
[Success][Witness] invariant confirmed: (3LL + (long long )i) - (long long )pushCount >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1852:5)
[Success][Witness] invariant confirmed: (5LL - (long long )i) - (long long )pushCount >= 0LL (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1852:5)
[Warning][Witness] invariant unconfirmed: stack.count == 3 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1852:5)
[Warning][Witness] invariant unconfirmed: stack.head == 0 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1852:5)
[Success][Witness] invariant confirmed: pushCount == 3 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1852:5)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1915:5)
[Success][Witness] invariant confirmed: i <= 3 (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread-complex/safestack_relacy.i:1915:5)
[Info][Witness] witness validation summary:
  confirmed: 145
  unconfirmed: 89
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 234
SV-COMP result: unknown
[Info][Race] Memory locations race summary:
  safe: 2
  vulnerable: 0
  unsafe: 3
  total memory locations: 5
