./goblint --conf conf/bench-yaml-validate.json --enable dbg.timing.enabled --enable witness.invariant.loop-head --enable witness.invariant.after-lock --disable witness.invariant.other --disable witness.invariant.accessed --ana.base.privatization mine --witness.yaml.unassume /mnt/thread-witnesses/replication/bench/thread-witnesses/mt/../../../results/mt/ourtool.2023-01-31_08-56-44.files/write+lock/pfscan_comb.yml/witness.yml --witness.yaml.validate /mnt/thread-witnesses/replication/bench/thread-witnesses/mt/../../../results/mt/ourtool.2023-01-31_08-56-44.files/mine/pfscan_comb.yml/witness.yml /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c /mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c


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


[Info][Imprecise] Invalidating expressions: AddrOf(Var(rlb,
                                     NoOffset)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1023:3-1023:22)
[Info][Unsound] Unknown address in (void (*)(int  ))1 has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1026:3-1026:32)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1026:3-1026:32)
[Info][Imprecise] Invalidating expressions: Const(Int(13,int,13)), CastE(TPtr(TFun(TVoid(), : TInt(int, ), ), ), Const(Int(1,int,1))) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1026:3-1026:32)
[Info][Witness] unassume invariant: ((((ignore_case <= 1 && 1 <= i) && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1031:3-1031:8)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1124:7-1125:47)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1124:7-1125:47)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(FILE, TComp(struct _IO_FILE, _flags : TInt(int, ), _IO_read_ptr : TPtr(TInt(char, ), ), _IO_read_end : TPtr(TInt(char, ), ), _IO_read_base : TPtr(TInt(char, ), ), _IO_write_base : TPtr(TInt(char, ), ), _IO_write_ptr : TPtr(TInt(char, ), ), _IO_write_end : TPtr(TInt(char, ), ), _IO_buf_base : TPtr(TInt(char, ), ), _IO_buf_end : TPtr(TInt(char, ), ), _IO_save_base : TPtr(TInt(char, ), ), _IO_backup_base : TPtr(TInt(char, ), ), _IO_save_end : TPtr(TInt(char, ), ), _markers : TPtr(TComp(struct _IO_marker, _next : TPtr(TCompLoop(struct _IO_marker, _, ), ), _sbuf : TPtr(TCompLoop(struct _IO_FILE, _, ), ), _pos : TInt(int, ), , ), ), _chain : TPtr(TCompLoop(struct _IO_FILE, _, ), ), _fileno : TInt(int, ), _flags2 : TInt(int, ), _old_offset : TNamed(__off_t, TInt(long, ), ), _cur_column : TInt(unsigned short, ), _vtable_offset : TInt(signed char, ), _shortbuf : TArray(TInt(char, ), Some(Const(Int(1,int,1))), ), _lock : TPtr(TNamed(_IO_lock_t, TVoid(), ), ), _offset : TNamed(__off64_t, TNamed(__quad_t, TInt(long long, ), ), ), __pad1 : TPtr(TVoid(), ), __pad2 : TPtr(TVoid(), ), __pad3 : TPtr(TVoid(), ), __pad4 : TPtr(TVoid(), ), __pad5 : TNamed(size_t, TInt(unsigned int, ), ), _mode : TInt(int, ), _unused2 : TArray(TInt(char, ), Some(MinusA(MinusA(*(Const(Int(f,unsigned long,None)), sizeof(TInt(int, ))), *(Const(Int(4,unsigned long,None)), sizeof(TPtr(TVoid(), )))), sizeof(TNamed(size_t, TInt(unsigned int, ), )))), ), , ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1124:7-1125:47)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1101:9-1101:13)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(nworkers, NoOffset)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1107:9-1108:37)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp___2, NoOffset)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1107:9-1108:37)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1116:11-1117:40)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1116:11-1117:40)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1116:11-1117:40)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1075:9-1075:13)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(maxlen, NoOffset)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1081:9-1082:35)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp___0, NoOffset)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1081:9-1082:35)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1090:11-1091:36)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1090:11-1091:36)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1090:11-1091:36)
[Info][Unsound] Unknown address given as function argument (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1066:7-1066:20)
[Info][Unsound] Unknown address in (FILE * __restrict  )out has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:987:3-988:17)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:987:3-988:17)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(out, NoOffset))) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:987:3-988:17)
[Info][Unsound] Unknown address in (FILE * __restrict  )out has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:991:3-991:109)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:991:3-991:109)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(out, NoOffset))) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:991:3-991:109)
[Info][Unsound] Unknown address in (FILE * __restrict  )out has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:992:3-992:98)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:992:3-992:98)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(out, NoOffset))) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:992:3-992:98)
[Info][Unsound] Unknown address in (FILE * __restrict  )out has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:993:3-993:95)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:993:3-993:95)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(out, NoOffset))) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:993:3-993:95)
[Info][Unsound] Unknown address in (FILE * __restrict  )out has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:994:3-994:105)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:994:3-994:105)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(out, NoOffset))) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:994:3-994:105)
[Info][Unsound] Unknown address in (FILE * __restrict  )out has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:995:3-995:110)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:995:3-995:110)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(out, NoOffset))) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:995:3-995:110)
[Info][Unsound] Unknown address in (FILE * __restrict  )out has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:996:3-996:105)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:996:3-996:105)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(out, NoOffset))) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:996:3-996:105)
[Info][Unsound] Unknown address in (FILE * __restrict  )out has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:997:3-997:116)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:997:3-997:116)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(out, NoOffset))) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:997:3-997:116)
[Info][Unsound] Unknown address in (FILE * __restrict  )out has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:998:3-998:113)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:998:3-998:113)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(out, NoOffset))) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:998:3-998:113)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1069:7-1069:16)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1063:7-1063:17)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1057:7-1057:15)
[Info][Unsound] Unknown address given as function argument (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1054:7-1054:28)
[Info][Unsound] Unknown address in (FILE * __restrict  )fp has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:491:3-492:46)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:491:3-492:46)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(fp, NoOffset))) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:491:3-492:46)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1128:7-1128:11)
[Info][Witness] unassume invariant: (((((((argc != 0 && ignore_case <= 1) && 2 <= argc) && 1 <= i) && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= debug) && -1 <= j (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1128:7-1128:11)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1034:11-1034:45)
[Info][Witness] unassume invariant: (((((((argc != 0 && ignore_case <= 1) && 2 <= argc) && 1 <= i) && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= debug) && -1 <= j (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1040:5-1040:10)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1130:5-1130:9)
[Info][Witness] unassume invariant: ((((ignore_case <= 1 && 1 <= i) && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1130:5-1130:9)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1051:7-1051:11)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1134:3-1134:7)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp___4, NoOffset)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1135:3-1135:52)
[Info][Unsound] Unknown address in {&tmp___4} has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1135:3-1135:52)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1135:3-1135:52)
[Info][Unsound] Unknown address given as function argument (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1137:3-1137:23)
[Info][Witness] unassume invariant: (((ignore_case <= 1 && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:636:3-636:10)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:637:10-637:13)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:638:9-638:24)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:703:7-703:28)
[Info][Witness] unassume invariant: (((ignore_case <= 1 && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:703:7-703:28)
[Info][Unsound] Unknown address in {&rp} has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:695:7-695:41)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:695:7-695:41)
[Info][Witness] unassume invariant: ((((((((((base != 0 && len <= 3) && base <= 127) && base <= 16) && ignore_case <= 1) && 8 <= base) && 0 <= len) && 0 <= base) && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:510:3-510:10)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp___5, NoOffset)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:530:11-530:42)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp___6, NoOffset)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:532:13-532:44)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:546:5-546:16)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp___0, NoOffset)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:561:9-561:40)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp___1, NoOffset)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:563:11-563:42)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:565:13-565:40)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:566:13-566:35)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:566:13-566:35)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:554:9-554:33)
[Info][Witness] unassume invariant: ((((((((((base != 0 && len <= 3) && base <= 127) && base <= 16) && ignore_case <= 1) && 8 <= base) && 0 <= len) && 0 <= base) && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:572:5-572:11)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:696:7-696:42)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:696:7-696:42)
[Info][Witness] unassume invariant: (((ignore_case <= 1 && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:696:7-696:42)
[Info][Unsound] Unknown address in {&rp} has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:681:7-681:39)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:681:7-681:39)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:682:7-682:41)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:682:7-682:41)
[Info][Witness] unassume invariant: (((ignore_case <= 1 && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:682:7-682:41)
[Info][Unsound] Unknown address in {&rp} has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:675:7-675:40)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:675:7-675:40)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:676:7-676:41)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:676:7-676:41)
[Info][Witness] unassume invariant: (((ignore_case <= 1 && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:676:7-676:41)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:668:7-668:34)
[Info][Witness] unassume invariant: (((ignore_case <= 1 && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:669:7-669:12)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:662:7-662:34)
[Info][Witness] unassume invariant: (((ignore_case <= 1 && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:663:7-663:12)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:656:7-656:35)
[Info][Witness] unassume invariant: (((ignore_case <= 1 && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:657:7-657:12)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:650:7-650:35)
[Info][Witness] unassume invariant: (((ignore_case <= 1 && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:651:7-651:12)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:643:7-643:22)
[Info][Witness] unassume invariant: (((ignore_case <= 1 && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:643:7-643:22)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:708:3-708:31)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:709:3-709:20)
[Info][Unsound] Unknown address given as function argument (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1138:3-1138:52)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:288:3-288:47)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:290:7-290:61)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:294:3-294:37)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:296:7-296:64)
[Info][Witness] unassume invariant: ((((((((bmb.icase <= 1 && ignore_case <= 1) && icase <= 1) && 0 <= bmb.icase) && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= i) && 0 <= icase) && 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:299:3-299:8)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp___1,
                                     NoOffset)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:302:7-302:40)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:303:7-303:52)
[Info][Witness] unassume invariant: ((((((((bmb.icase <= 1 && ignore_case <= 1) && icase <= 1) && 0 <= bmb.icase) && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= i) && 0 <= icase) && 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:307:5-307:9)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:240:3-240:47)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:242:7-242:56)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:200:3-200:24)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:201:3-201:12)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:202:3-202:12)
[Info][Witness] unassume invariant: ((((((((bmb.icase <= 1 && ignore_case <= 1) && i <= 2147483645) && g <= 2147483646) && 0 <= bmb.icase) && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= f) && 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:202:3-202:12)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:218:15-218:69)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:218:15-218:69)
[Info][Witness] unassume invariant: (((((((((((bmb.icase <= 1 && ignore_case <= 1) && i <= 2147483645) && g <= 2147483645) && f <= 2147483645) && 0 <= bmb.icase) && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= i) && 0 <= f) && 0 <= debug) && -2147483647 <= g (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:224:9-224:13)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:205:11-205:48)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:205:11-205:48)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:205:11-205:48)
[Info][Witness] unassume invariant: (((((((((((bmb.icase <= 1 && ignore_case <= 1) && i <= 2147483645) && g <= 2147483645) && f <= 2147483645) && 0 <= bmb.icase) && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= i) && 0 <= f) && 0 <= debug) && -2147483647 <= g (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:215:7-215:12)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:226:7-226:26)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:206:9-206:52)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:206:9-206:52)
[Info][Witness] unassume invariant: ((((((((bmb.icase <= 1 && ignore_case <= 1) && i <= 2147483645) && g <= 2147483646) && 0 <= bmb.icase) && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= f) && 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:228:5-228:9)
[Info][Witness] unassume invariant: ((((((bmb.icase <= 1 && ignore_case <= 1) && 0 <= bmb.icase) && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= i) && 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:246:3-246:8)
[Info][Witness] unassume invariant: ((((((bmb.icase <= 1 && ignore_case <= 1) && 0 <= bmb.icase) && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= i) && 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:249:5-249:9)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:252:3-252:12)
[Info][Witness] unassume invariant: (((((((bmb.icase <= 1 && ignore_case <= 1) && i <= 2147483646) && 0 <= bmb.icase) && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= j) && 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:252:3-252:12)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:259:16-259:31)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:259:16-259:31)
[Info][Witness] unassume invariant: ((((((((bmb.icase <= 1 && ignore_case <= 1) && i <= 2147483646) && 0 <= bmb.icase) && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= j) && 0 <= debug) && -1 <= i (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:263:11-263:15)
[Info][Witness] unassume invariant: ((((((((bmb.icase <= 1 && ignore_case <= 1) && i <= 2147483646) && 0 <= bmb.icase) && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= j) && 0 <= debug) && -1 <= i (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:257:11-257:31)
[Info][Witness] unassume invariant: ((((((((bmb.icase <= 1 && ignore_case <= 1) && i <= 2147483646) && 0 <= bmb.icase) && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= j) && 0 <= debug) && -1 <= i (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:254:9-254:16)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:259:16-259:31)
[Info][Witness] unassume invariant: (((((((bmb.icase <= 1 && ignore_case <= 1) && i <= 2147483646) && 0 <= bmb.icase) && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= j) && 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:267:5-267:9)
[Info][Witness] unassume invariant: ((((((((bmb.icase <= 1 && ignore_case <= 1) && i <= 2147483646) && 0 <= bmb.icase) && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= j) && 0 <= i) && 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:269:3-269:8)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:270:10-270:20)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:271:5-271:52)
[Info][Witness] unassume invariant: ((((((((bmb.icase <= 1 && ignore_case <= 1) && i <= 2147483646) && 0 <= bmb.icase) && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= j) && 0 <= i) && 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:272:5-272:9)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:270:10-270:20)
[Info][Witness] unassume invariant: (((((((bmb.icase <= 1 && ignore_case <= 1) && i <= 256) && 0 <= bmb.icase) && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= i) && 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:180:3-180:8)
[Info][Witness] unassume invariant: (((((((bmb.icase <= 1 && ignore_case <= 1) && i <= 256) && 0 <= bmb.icase) && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= i) && 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:183:5-183:9)
[Info][Witness] unassume invariant: (((((((bmb.icase <= 1 && ignore_case <= 1) && i <= 2147483646) && 0 <= bmb.icase) && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= i) && 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:185:3-185:8)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:186:10-186:19)
[Info][Witness] unassume invariant: (((((((bmb.icase <= 1 && ignore_case <= 1) && i <= 2147483646) && 0 <= bmb.icase) && 0 <= ignore_case) && 0 <= line_f) && 0 <= verbose) && 0 <= i) && 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:188:5-188:9)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:186:10-186:19)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1140:5-1141:31)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1140:5-1141:31)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(FILE,
                                            TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1140:5-1141:31)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1144:3-1144:64)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1144:3-1144:64)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1146:5-1147:33)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1146:5-1147:33)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1146:5-1147:33)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1149:3-1149:35)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1203:3-1203:53)
[Info][Unsound] Unknown value in {&((alloc@sid:911@tid:[main](#top)), /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1204:3-1204:25)[def_exc:0; intervals:[0,0]]} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1204:3-1204:25)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1205:7-1205:59)
[Info][Unsound] Unknown value in {&pab} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1150:3-1150:27)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(pab,
                                     NoOffset)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1150:3-1150:27)
[Info][Unsound] Unknown value in {&pab} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1151:3-1151:34)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(pab, NoOffset)), Const(Int(0,int,0)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1151:3-1151:34)
[Info][Witness] unassume invariant: 2 <= i && 0 <= j (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1153:3-1153:8)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp___6, NoOffset)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1155:5-1156:72)
[Info][Unsound] Unknown address in {&path} has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:968:5-968:47)
[Info][Unsound] Unknown address in {&((alloc@sid:911@tid:[main](#top)), /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1204:3-1204:25)[def_exc:0; intervals:[0,0]]} has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:968:5-968:47)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:968:5-968:47)
[Info][Witness] unassume invariant: (((pqb.closed <= 1 && 0 <= pqb.nextout) && 0 <= pqb.nextin) && 0 <= pqb.closed) && 0 <= n_matches (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1257:3-1257:32)
[Info][Witness] unassume invariant: (((pqb.closed <= 1 && 0 <= pqb.nextout) && 0 <= pqb.nextin) && 0 <= pqb.closed) && 0 <= n_matches (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1266:5-1266:110)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1270:6-1270:21)
[Info][Unsound] Unknown address given as function argument (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:972:5-972:20)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(fd,
                                     NoOffset)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:857:3-857:39)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:857:3-857:39)
[Info][Witness] unassume invariant: (((((fd != 0 && fd <= -1) && pqb.closed <= 1) && 0 <= pqb.nextout) && 0 <= pqb.nextin) && 0 <= pqb.closed) && 0 <= n_matches (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:860:7-860:39)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:861:7-861:31)
[Info][Unsound] Unknown address in {&tmp} has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:861:7-861:31)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:861:7-861:31)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp___0, NoOffset)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:862:7-862:31)
[Info][Unsound] Unknown address in {&tmp___0} has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:862:7-862:31)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:862:7-862:31)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:862:7-862:31)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:862:7-862:31)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:863:7-864:33)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:863:7-864:33)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:863:7-864:33)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:863:7-864:33)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:434:3-434:37)
[Info][Witness] unassume invariant: ((((pqb.closed <= 1 && 0 <= fd) && 0 <= pqb.nextout) && 0 <= pqb.nextin) && 0 <= pqb.closed) && 0 <= n_matches (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:872:7-872:39)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp___1, NoOffset)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:873:7-873:35)
[Info][Unsound] Unknown address in {&tmp___1} has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:873:7-873:35)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:873:7-873:35)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp___2, NoOffset)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:874:7-874:35)
[Info][Unsound] Unknown address in {&tmp___2} has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:874:7-874:35)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:874:7-874:35)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:874:7-874:35)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:874:7-874:35)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:875:7-876:33)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:875:7-876:33)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:875:7-876:33)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:875:7-876:33)
[Info][Imprecise] Invalidating expressions: Lval(Var(fd, NoOffset)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:879:5-879:14)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:882:3-882:34)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:884:5-885:38)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:884:5-885:38)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:884:5-885:38)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:884:5-885:38)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp___4, NoOffset)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:887:3-887:51)
[Info][Unsound] Unknown address in {&tmp___4} has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:887:3-887:51)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:887:3-887:51)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:889:7-889:56)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:889:7-889:56)
[Info][Witness] unassume invariant: ((((pqb.closed <= 1 && 0 <= fd) && 0 <= pqb.nextout) && 0 <= pqb.nextin) && 0 <= pqb.closed) && 0 <= n_matches (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:891:7-891:39)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp___5, NoOffset)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:892:7-892:35)
[Info][Unsound] Unknown address in {&tmp___5} has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:892:7-892:35)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:892:7-892:35)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp___6, NoOffset)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:893:7-893:35)
[Info][Unsound] Unknown address in {&tmp___6} has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:893:7-893:35)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:893:7-893:35)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:893:7-893:35)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:893:7-893:35)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:894:7-895:33)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:894:7-895:33)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:894:7-895:33)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:894:7-895:33)
[Info][Imprecise] Invalidating expressions: Lval(Var(fd, NoOffset)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:898:5-898:14)
[Info][Unsound] Unknown address given as function argument (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:902:5-902:68)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:359:13-359:53)
[Info][Witness] unassume invariant: i <= 2147483646 && 0 <= nm (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:365:7-365:11)
[Info][Witness] unassume invariant: 0 <= nm (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:348:3-348:8)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:388:9-388:39)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:388:9-388:39)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp___2,
                                     NoOffset)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:385:9-385:48)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:385:9-385:48)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:385:9-385:48)
[Warning][Integer > Overflow][CWE-190][CWE-191] Unsigned integer overflow and underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:390:7-390:38)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:391:11-391:73)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:391:11-391:73)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:391:11-391:73)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:392:9-392:62)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:392:9-392:62)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:396:7-396:19)
[Info][Witness] unassume invariant: 0 <= nm (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:396:7-396:19)
[Warning][Integer > Overflow][CWE-190][CWE-191] Signed integer overflow and underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:379:9-379:30)
[Info][Witness] unassume invariant: 0 <= nm (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:379:9-379:30)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:349:10-349:49)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:349:10-349:49)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:350:5-350:25)
[Info][Witness] unassume invariant: i <= 2147483646 && 0 <= nm (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:350:5-350:25)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:357:11-357:41)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:357:11-357:41)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:354:11-354:46)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:354:11-354:46)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:354:11-354:46)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:369:9-369:14)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:370:9-370:50)
[Info][Unsound] Unknown address given as function argument (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:370:9-370:50)
[Info][Witness] unassume invariant: (((pqb.closed <= 1 && 0 <= pqb.nextout) && 0 <= pqb.nextin) && 0 <= pqb.closed) && 0 <= n_matches (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:814:3-814:37)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:815:3-815:15)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:820:13-820:44)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:823:15-823:46)
[Info][Witness] unassume invariant: (((pqb.closed <= 1 && 0 <= pqb.nextout) && 0 <= pqb.nextin) && 0 <= pqb.closed) && 0 <= n_matches (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:833:3-833:35)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:834:3-834:81)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:835:3-835:37)
[Info][Unsound] Unknown address given as function argument (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:835:3-835:37)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:746:7-746:55)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:750:3-750:37)
[Info][Unsound] Unknown address given as function argument (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:750:3-750:37)
[Info][Witness] unassume invariant: (((pqb.closed <= 1 && 0 <= pqb.nextout) && 0 <= pqb.nextin) && 0 <= pqb.closed) && 0 <= n_matches (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:712:1-738:1)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp,
                                     NoOffset)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:718:7-718:28)
[Info][Unsound] Unknown address in {&tmp} has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:718:7-718:28)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:718:7-718:28)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:719:11-719:54)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:719:11-719:54)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:720:13-720:31)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:721:15-721:33)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:722:17-722:36)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:723:19-723:38)
[Info][Witness] unassume invariant: (((pqb.closed <= 1 && 0 <= pqb.nextout) && 0 <= pqb.nextin) && 0 <= pqb.closed) && 0 <= n_matches (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:734:5-734:10)
[Info][Witness] unassume invariant: (((pqb.closed <= 1 && 0 <= pqb.nextout) && 0 <= pqb.nextin) && 0 <= pqb.closed) && 0 <= n_matches (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:752:5-752:47)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:769:9-769:16)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:775:9-775:16)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:781:9-781:15)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:785:9-785:58)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:766:9-766:15)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:762:11-762:51)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:762:11-762:51)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:763:9-763:28)
[Info][Witness] unassume invariant: (((pqb.closed <= 1 && 0 <= pqb.nextout) && 0 <= pqb.nextin) && 0 <= pqb.closed) && 0 <= n_matches (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:789:7-789:13)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:755:13-755:38)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:761:7-761:28)
[Info][Unsound] Unknown address in {&tmp} has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:761:7-761:28)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:761:7-761:28)
[Info][Witness] unassume invariant: (((pqb.closed <= 1 && 0 <= pqb.nextout) && 0 <= pqb.nextin) && 0 <= pqb.closed) && 0 <= n_matches (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:792:5-792:46)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:795:13-795:38)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:801:7-801:54)
[Info][Witness] unassume invariant: (((pqb.closed <= 1 && 0 <= pqb.nextout) && 0 <= pqb.nextin) && 0 <= pqb.closed) && 0 <= n_matches (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:803:7-803:13)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:399:7-399:56)
[Info][Witness] unassume invariant: ((((pqb.closed <= 1 && 0 <= fd) && 0 <= pqb.nextout) && 0 <= pqb.nextin) && 0 <= pqb.closed) && 0 <= n_matches (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:904:5-904:37)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:905:5-905:60)
[Info][Unsound] Unknown address given as function argument (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:906:5-906:27)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp, NoOffset)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:718:7-718:28)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:720:13-720:31)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:721:15-721:33)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:722:17-722:36)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:723:19-723:38)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:769:9-769:16)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:775:9-775:16)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:781:9-781:15)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:785:9-785:58)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:766:9-766:15)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:763:9-763:28)
[Warning][Behavior > Undefined > NullPointerDereference][CWE-476] May dereference NULL pointer (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:801:7-801:54)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:910:3-910:37)
[Info][Imprecise] Invalidating expressions: Lval(Var(fd, NoOffset)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:911:3-911:12)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:973:5-973:23)
[Info][Unsound] Unknown address in stdout has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:975:3-975:17)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:975:3-975:17)
[Info][Imprecise] Invalidating expressions: Lval(Var(stdout, NoOffset)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:975:3-975:17)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:975:3-975:17)
[Info][Witness] unassume invariant: (((pqb.closed <= 1 && 0 <= pqb.nextout) && 0 <= pqb.nextin) && 0 <= pqb.closed) && 0 <= n_matches (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:976:3-976:37)
[Warning][Integer > Overflow][CWE-191] Signed integer underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:977:3-977:14)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1158:7-1159:27)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1158:7-1159:27)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(FILE,
                                            TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1158:7-1159:27)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1158:7-1159:27)
[Info][Witness] unassume invariant: 2 <= i && 0 <= j (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1162:5-1162:9)
[Info][Witness] unassume invariant: (2 <= i || ((((((((0 <= n_matches && 0 <= pqb.closed) && 0 <= pqb.nextin) && 0 <= pqb.nextout) && 3 <= argc) && 3 <= i) && pqb.closed <= 1) && pqb.closed != 0) && argc != 0)) && 0 <= j (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1154:10-1154:22)
[Info][Unsound] Unknown address given as function argument (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1168:7-1168:42)
[Info][Unsound] Unknown address given as function argument (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:950:3-950:59)
[Info][Unsound] Unknown address given as function argument (/mnt/thread-witnesses/replication/bench/pthread/pfscan_ftw.c:46:3-46:21)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:919:3-919:13)
[Warning][Integer > Overflow][CWE-191] Unsigned integer underflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:920:3-920:83)
[Warning][Integer > Overflow][CWE-190] Unsigned integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:920:3-920:83)
[Info][Imprecise] Invalidating expressions: AddrOf(Var(tmp,
                                     NoOffset)) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:923:3-923:21)
[Info][Unsound] Unknown address in {&tmp} has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:923:3-923:21)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:923:3-923:21)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:923:3-923:21)
[Info][Unsound] Unknown address given as function argument (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:924:3-924:33)
[Info][Unsound] Unknown address in {&((alloc@sid:911@tid:[main](#top)), /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1204:3-1204:25)[def_exc:0; intervals:[0,0]]} has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:924:3-924:33)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:924:3-924:33)
[Info][Witness] unassume invariant: (((pqb.closed <= 1 && 0 <= pqb.nextout) && 0 <= pqb.nextin) && 0 <= pqb.closed) && 0 <= n_matches (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1234:3-1234:32)
[Info][Witness] unassume invariant: (((pqb.closed <= 1 && 0 <= pqb.nextout) && 0 <= pqb.nextin) && 0 <= pqb.closed) && 0 <= n_matches (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1235:7-1235:17)
[Info][Witness] unassume invariant: (((pqb.closed <= 1 && 0 <= pqb.nextout) && 0 <= pqb.nextin) && 0 <= pqb.closed) && 0 <= n_matches (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1239:5-1239:110)
[Warning][Integer > Overflow][CWE-190] Signed integer overflow (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1242:4-1242:18)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:929:3-930:23)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:929:3-930:23)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(FILE,
                                            TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:929:3-930:23)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:929:3-930:23)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:933:3-934:23)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:933:3-934:23)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:933:3-934:23)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:933:3-934:23)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:937:3-938:23)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:937:3-938:23)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:937:3-938:23)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:937:3-938:23)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1168:7-1168:42)
[Info][Witness] unassume invariant: (2 <= i || ((((((((0 <= n_matches && 0 <= pqb.closed) && 0 <= pqb.nextin) && 0 <= pqb.nextout) && 3 <= argc) && 3 <= i) && pqb.closed <= 1) && pqb.closed != 0) && argc != 0)) && 0 <= j (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1169:11-1169:27)
[Info][Unsound] Unknown address in {&((alloc@sid:911@tid:[main](#top)), /mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1204:3-1204:25)[def_exc:0; intervals:[0,0]]} has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1176:3-1176:22)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1176:3-1176:22)
[Info][Witness] unassume invariant: (((pqb.closed <= 1 && 0 <= pqb.nextout) && 0 <= pqb.nextin) && 0 <= pqb.closed) && 0 <= n_matches (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1223:3-1223:32)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1178:5-1178:104)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1178:5-1178:104)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(FILE,
                                            TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1178:5-1178:104)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1178:5-1178:104)
[Info][Witness] unassume invariant: (((((pqb.closed <= 1 && 2 <= i) && 0 <= j) && 0 <= pqb.nextout) && 0 <= pqb.nextin) && 0 <= pqb.closed) && 0 <= n_matches (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1180:3-1180:37)
[Info][Witness] unassume invariant: (((((pqb.closed <= 1 && 2 <= i) && 0 <= j) && 0 <= pqb.nextout) && 0 <= pqb.nextin) && 0 <= pqb.closed) && 0 <= n_matches (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1182:5-1182:117)
[Info][Unsound] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1186:5-1187:70)
[Info][Unsound] Unknown value in {?} could be an escaped pointer address! (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1186:5-1187:70)
[Info][Imprecise] Invalidating expressions: CastE(TPtr(TNamed(FILE,
                                            TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1186:5-1187:70)
[Info][Unsound] Write to unknown address: privatization is unsound. (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1186:5-1187:70)
[Warning][Deadcode] Function 'bm_destroy' is uncalled: 5 LLoC (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:317:1-329:1)
[Warning][Deadcode] Function 'dehex' is uncalled: 21 LLoC (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:577:1-615:1)
[Warning][Deadcode] Function 'pqueue_destroy' is uncalled: 5 LLoC (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1283:1-1293:1)
[Warning][Deadcode] Function 'bm_search' has dead code:
  on lines 372..373 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:372-373)
  on line 375 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:375-375)
  on line 377 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:377-377)
  on line 381 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:381-381)
[Warning][Deadcode] Function 'do_ftw' has dead code:
  on lines 953..955 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:953-955)
  on line 957 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:957-957)
[Warning][Deadcode] Logical lines of code (LLoC) summary:
  live: 522
  dead: 40 (31 in uncalled functions)
  total lines: 562
[Warning][Race] Memory location n_matches@/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:480:5-480:18 (race with conf. 110):
  write with [mhp:{tid=[main], {worker@/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1155:5-1156:72}}, lock:{matches_lock}] (conf. 110) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:815:3-815:15)
  write with [mhp:{tid=[main, worker@/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1155:5-1156:72]}, lock:{matches_lock}, thread:[main, worker@/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1155:5-1156:72]] (conf. 110) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:815:3-815:15)
  read with [mhp:{tid=[main]; created={[main, worker@/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1155:5-1156:72]}}, thread:[main]] (conf. 110) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1186:5-1187:70)
  read with [mhp:{tid=[main]; created={[main, worker@/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1155:5-1156:72]}}, thread:[main]] (conf. 110) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1189:3-1189:21)
[Warning][Deadcode][CWE-570] condition 'code < 0' is always false (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:952:7-952:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:967:10-967:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1258:10-1258:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:351:12-351:13)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:716:10-716:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1032:10-1032:11)
[Warning][Deadcode][CWE-571] condition 'mfun' is always true (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:368:11-368:15)
[Warning][Deadcode][CWE-570] condition 'c' is always false (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:371:13-371:14)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1041:12-1041:13)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:753:12-753:13)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:511:10-511:11)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:793:12-793:13)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:818:12-818:13)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:216:14-216:15)
[Warning][Deadcode][CWE-571] condition '1' (possibly inserted by CIL) is always true (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1164:10-1164:11)
[Warning][Deadcode][CWE-570] condition '! (tmp___8 == 0)' is always false (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1169:11-1169:27)
[Success][Witness] invariant confirmed: 0 <= n_matches (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:815:3)
[Success][Witness] invariant confirmed: fd <= -1 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:861:7)
[Success][Witness] invariant confirmed: fd != 0 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:861:7)
[Success][Witness] invariant confirmed: 0 <= fd (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:873:7)
[Success][Witness] invariant confirmed: 0 <= fd (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:892:7)
[Success][Witness] invariant confirmed: 0 <= fd (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:905:5)
[Success][Witness] invariant confirmed: -2147483640 <= pqb.qsize (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1224:3)
[Success][Witness] invariant confirmed: 0 <= pqb.closed (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1224:3)
[Success][Witness] invariant confirmed: 0 <= pqb.nextin (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1224:3)
[Success][Witness] invariant confirmed: 0 <= pqb.nextout (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1224:3)
[Success][Witness] invariant confirmed: 0 <= pqb.occupied (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1224:3)
[Success][Witness] invariant confirmed: pqb.closed <= 1 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1224:3)
[Success][Witness] invariant confirmed: -2147483640 <= pqb.qsize (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1235:7)
[Success][Witness] invariant confirmed: 0 <= pqb.closed (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1235:7)
[Success][Witness] invariant confirmed: 0 <= pqb.nextin (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1235:7)
[Success][Witness] invariant confirmed: 0 <= pqb.nextout (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1235:7)
[Success][Witness] invariant confirmed: 0 <= pqb.occupied (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1235:7)
[Success][Witness] invariant confirmed: pqb.closed <= 1 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1235:7)
[Success][Witness] invariant confirmed: 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:181:10)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:181:10)
[Success][Witness] invariant confirmed: 0 <= verbose (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:181:10)
[Success][Witness] invariant confirmed: 0 <= line_f (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:181:10)
[Success][Witness] invariant confirmed: 0 <= ignore_case (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:181:10)
[Success][Witness] invariant confirmed: 0 <= bmb.icase (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:181:10)
[Success][Witness] invariant confirmed: i <= 256 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:181:10)
[Success][Witness] invariant confirmed: ignore_case <= 1 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:181:10)
[Success][Witness] invariant confirmed: bmb.icase <= 1 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:181:10)
[Success][Witness] invariant confirmed: 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:186:10)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:186:10)
[Success][Witness] invariant confirmed: 0 <= verbose (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:186:10)
[Success][Witness] invariant confirmed: 0 <= line_f (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:186:10)
[Success][Witness] invariant confirmed: 0 <= ignore_case (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:186:10)
[Success][Witness] invariant confirmed: 0 <= bmb.icase (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:186:10)
[Success][Witness] invariant confirmed: i <= 2147483646 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:186:10)
[Success][Witness] invariant confirmed: ignore_case <= 1 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:186:10)
[Success][Witness] invariant confirmed: bmb.icase <= 1 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:186:10)
[Success][Witness] invariant confirmed: 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:203:10)
[Success][Witness] invariant confirmed: 0 <= f (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:203:10)
[Success][Witness] invariant confirmed: 0 <= verbose (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:203:10)
[Success][Witness] invariant confirmed: 0 <= line_f (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:203:10)
[Success][Witness] invariant confirmed: 0 <= ignore_case (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:203:10)
[Success][Witness] invariant confirmed: 0 <= bmb.icase (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:203:10)
[Success][Witness] invariant confirmed: g <= 2147483646 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:203:10)
[Success][Witness] invariant confirmed: i <= 2147483645 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:203:10)
[Success][Witness] invariant confirmed: ignore_case <= 1 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:203:10)
[Success][Witness] invariant confirmed: bmb.icase <= 1 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:203:10)
[Success][Witness] invariant confirmed: -2147483647 <= g (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:216:14)
[Success][Witness] invariant confirmed: 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:216:14)
[Success][Witness] invariant confirmed: 0 <= f (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:216:14)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:216:14)
[Success][Witness] invariant confirmed: 0 <= verbose (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:216:14)
[Success][Witness] invariant confirmed: 0 <= line_f (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:216:14)
[Success][Witness] invariant confirmed: 0 <= ignore_case (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:216:14)
[Success][Witness] invariant confirmed: 0 <= bmb.icase (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:216:14)
[Success][Witness] invariant confirmed: f <= 2147483645 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:216:14)
[Success][Witness] invariant confirmed: g <= 2147483645 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:216:14)
[Success][Witness] invariant confirmed: i <= 2147483645 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:216:14)
[Success][Witness] invariant confirmed: ignore_case <= 1 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:216:14)
[Success][Witness] invariant confirmed: bmb.icase <= 1 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:216:14)
[Success][Witness] invariant confirmed: 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:247:10)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:247:10)
[Success][Witness] invariant confirmed: 0 <= verbose (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:247:10)
[Success][Witness] invariant confirmed: 0 <= line_f (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:247:10)
[Success][Witness] invariant confirmed: 0 <= ignore_case (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:247:10)
[Success][Witness] invariant confirmed: 0 <= bmb.icase (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:247:10)
[Success][Witness] invariant confirmed: ignore_case <= 1 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:247:10)
[Success][Witness] invariant confirmed: bmb.icase <= 1 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:247:10)
[Success][Witness] invariant confirmed: 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:253:10)
[Success][Witness] invariant confirmed: 0 <= j (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:253:10)
[Success][Witness] invariant confirmed: 0 <= verbose (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:253:10)
[Success][Witness] invariant confirmed: 0 <= line_f (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:253:10)
[Success][Witness] invariant confirmed: 0 <= ignore_case (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:253:10)
[Success][Witness] invariant confirmed: 0 <= bmb.icase (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:253:10)
[Success][Witness] invariant confirmed: i <= 2147483646 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:253:10)
[Success][Witness] invariant confirmed: ignore_case <= 1 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:253:10)
[Success][Witness] invariant confirmed: bmb.icase <= 1 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:253:10)
[Success][Witness] invariant confirmed: -1 <= i (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:259:16)
[Success][Witness] invariant confirmed: 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:259:16)
[Success][Witness] invariant confirmed: 0 <= j (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:259:16)
[Success][Witness] invariant confirmed: 0 <= verbose (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:259:16)
[Success][Witness] invariant confirmed: 0 <= line_f (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:259:16)
[Success][Witness] invariant confirmed: 0 <= ignore_case (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:259:16)
[Success][Witness] invariant confirmed: 0 <= bmb.icase (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:259:16)
[Success][Witness] invariant confirmed: i <= 2147483646 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:259:16)
[Success][Witness] invariant confirmed: ignore_case <= 1 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:259:16)
[Success][Witness] invariant confirmed: bmb.icase <= 1 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:259:16)
[Success][Witness] invariant confirmed: 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:270:10)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:270:10)
[Success][Witness] invariant confirmed: 0 <= j (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:270:10)
[Success][Witness] invariant confirmed: 0 <= verbose (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:270:10)
[Success][Witness] invariant confirmed: 0 <= line_f (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:270:10)
[Success][Witness] invariant confirmed: 0 <= ignore_case (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:270:10)
[Success][Witness] invariant confirmed: 0 <= bmb.icase (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:270:10)
[Success][Witness] invariant confirmed: i <= 2147483646 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:270:10)
[Success][Witness] invariant confirmed: ignore_case <= 1 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:270:10)
[Success][Witness] invariant confirmed: bmb.icase <= 1 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:270:10)
[Success][Witness] invariant confirmed: 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:300:10)
[Success][Witness] invariant confirmed: 0 <= icase (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:300:10)
[Success][Witness] invariant confirmed: 0 <= i (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:300:10)
[Success][Witness] invariant confirmed: 0 <= verbose (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:300:10)
[Success][Witness] invariant confirmed: 0 <= line_f (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:300:10)
[Success][Witness] invariant confirmed: 0 <= ignore_case (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:300:10)
[Success][Witness] invariant confirmed: 0 <= bmb.icase (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:300:10)
[Success][Witness] invariant confirmed: icase <= 1 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:300:10)
[Success][Witness] invariant confirmed: ignore_case <= 1 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:300:10)
[Success][Witness] invariant confirmed: bmb.icase <= 1 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:300:10)
[Success][Witness] invariant confirmed: 0 <= nm (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:349:10)
[Success][Witness] invariant confirmed: 0 <= nm (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:351:12)
[Success][Witness] invariant confirmed: i <= 2147483646 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:351:12)
[Success][Witness] invariant confirmed: 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1032:10)
[Success][Witness] invariant confirmed: 0 <= verbose (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1032:10)
[Success][Witness] invariant confirmed: 0 <= line_f (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1032:10)
[Success][Witness] invariant confirmed: 0 <= ignore_case (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1032:10)
[Success][Witness] invariant confirmed: 1 <= i (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1032:10)
[Success][Witness] invariant confirmed: ignore_case <= 1 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1032:10)
[Success][Witness] invariant confirmed: -1 <= j (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1041:12)
[Success][Witness] invariant confirmed: 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1041:12)
[Success][Witness] invariant confirmed: 0 <= verbose (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1041:12)
[Success][Witness] invariant confirmed: 0 <= line_f (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1041:12)
[Success][Witness] invariant confirmed: 0 <= ignore_case (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1041:12)
[Success][Witness] invariant confirmed: 1 <= i (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1041:12)
[Success][Witness] invariant confirmed: 2 <= argc (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1041:12)
[Success][Witness] invariant confirmed: ignore_case <= 1 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1041:12)
[Success][Witness] invariant confirmed: argc != 0 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1041:12)
[Success][Witness] invariant confirmed: 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:511:10)
[Success][Witness] invariant confirmed: 0 <= verbose (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:511:10)
[Success][Witness] invariant confirmed: 0 <= line_f (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:511:10)
[Success][Witness] invariant confirmed: 0 <= ignore_case (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:511:10)
[Success][Witness] invariant confirmed: 0 <= base (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:511:10)
[Success][Witness] invariant confirmed: 0 <= len (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:511:10)
[Success][Witness] invariant confirmed: 8 <= base (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:511:10)
[Success][Witness] invariant confirmed: ignore_case <= 1 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:511:10)
[Success][Witness] invariant confirmed: base <= 16 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:511:10)
[Success][Witness] invariant confirmed: base <= 127 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:511:10)
[Success][Witness] invariant confirmed: len <= 3 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:511:10)
[Success][Witness] invariant confirmed: base != 0 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:511:10)
[Success][Witness] invariant confirmed: 0 <= j (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1154:10)
[Success][Witness] invariant confirmed: 2 <= i (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1154:10)
[Success][Witness] invariant confirmed: 0 <= debug (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:637:10)
[Success][Witness] invariant confirmed: 0 <= verbose (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:637:10)
[Success][Witness] invariant confirmed: 0 <= line_f (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:637:10)
[Success][Witness] invariant confirmed: 0 <= ignore_case (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:637:10)
[Success][Witness] invariant confirmed: ignore_case <= 1 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:637:10)
[Success][Witness] invariant confirmed: 0 <= j (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1164:10)
[Success][Witness] invariant confirmed: 2 <= i || (((((((((-2147483640 <= pqb.qsize && 0 <= pqb.closed) && 0 <= pqb.nextin) && 0 <= pqb.nextout) && 0 <= pqb.occupied) && 3 <= argc) && 3 <= i) && pqb.closed <= 1) && pqb.closed != 0) && argc != 0) (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1164:10)
[Success][Witness] invariant confirmed: 0 <= j (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1181:10)
[Success][Witness] invariant confirmed: 2 <= i (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1181:10)
[Success][Witness] invariant confirmed: -2147483640 <= pqb.qsize (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1238:10)
[Success][Witness] invariant confirmed: 0 <= pqb.closed (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1238:10)
[Success][Witness] invariant confirmed: 0 <= pqb.nextin (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1238:10)
[Success][Witness] invariant confirmed: 0 <= pqb.nextout (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1238:10)
[Success][Witness] invariant confirmed: 0 <= pqb.occupied (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1238:10)
[Success][Witness] invariant confirmed: pqb.closed <= 1 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1238:10)
[Success][Witness] invariant confirmed: -2147483640 <= pqb.qsize (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1258:10)
[Success][Witness] invariant confirmed: 0 <= pqb.closed (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1258:10)
[Success][Witness] invariant confirmed: 0 <= pqb.nextin (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1258:10)
[Success][Witness] invariant confirmed: 0 <= pqb.nextout (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1258:10)
[Success][Witness] invariant confirmed: 0 <= pqb.occupied (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1258:10)
[Success][Witness] invariant confirmed: pqb.closed <= 1 (/mnt/thread-witnesses/replication/bench/pthread/pfscan_comb.c:1258:10)
[Info][Witness] witness validation summary:
  confirmed: 159
  unconfirmed: 0
  refuted: 0
  error: 0
  unchecked: 0
  unsupported: 0
  disabled: 0
  total validation entries: 159
[Info][Race] Memory locations race summary:
  safe: 38
  vulnerable: 0
  unsafe: 1
  total memory locations: 39

vars = 2024    evals = 5959    narrow_reuses = 332

Timings:
                                  cputime   walltime   allocated   count
Default                            2.153s     2.154s   4944.33MB      1×
  preprocess                         0.027s     0.026s      0.01MB      1×
  FrontC                             0.006s     0.006s      4.86MB      5×
  Cabs2cil                           0.007s     0.007s      7.36MB      5×
  mergeCIL                           0.004s     0.004s      4.02MB      1×
  analysis                           2.101s     2.102s   4921.52MB      1×
    createCFG                          0.002s     0.002s      2.12MB      1×
      handle                             0.001s     0.001s      0.63MB     53×
      iter_connect                       0.001s     0.001s      1.24MB     53×
        computeSCCs                        0.001s     0.001s      0.86MB     54×
    FrontC                             0.006s     0.007s      2.05MB    368×
    Cabs2cil                           0.082s     0.083s     44.39MB    425×
    global_inits                       0.006s     0.006s      8.82MB      1×
    solving                            1.872s     1.872s   4661.94MB      1×
      S.Dom.equal                        0.008s     0.015s      2.12MB   6291×
      base unassume                      0.232s     0.234s    510.26MB    810×
      cheap_full_reach                   0.002s     0.002s      0.93MB      1×
      postsolver                         0.236s     0.236s    538.54MB      1×
        postsolver_iter                    0.230s     0.230s    536.08MB      1×
    warn_global                        0.004s     0.004s      6.49MB      1×
      race                               0.002s     0.002s      1.81MB     39×
    result output                      0.001s     0.001s      0.01MB      1×
