./deagle --no-assertions --datarace --32 /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i


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


Deagle version 2.1 64-bit x86_64 linux
which contains:
CBMC version 5.67.0 (SVCOMP2023_221122-2-g2121ef1a2) 64-bit x86_64 linux
Parsing /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i
Converting
Type-checking twostage_3
Generating GOTO Program
Adding CPROVER library (x86_64)
file <builtin-library-pthread_mutex_unlock> line 17: 
reason for conflict at #this.__data: number of members is different (6/8)

struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  signed int __kind;
  unsigned int __nusers;
  union $anon0;
}
struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  unsigned int __nusers;
  signed int __kind;
  signed short int __spins;
  signed short int __elision;
  __pthread_list_t __list;
}
warning: pointer parameter types differ between declaration and definition "pthread_mutex_unlock"
old definition in module twostage_3 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i line 1074
signed int (pthread_mutex_t *)
new definition in module <built-in-library> file <builtin-library-pthread_mutex_unlock> line 17
signed int (pthread_mutex_t *mutex)
file <builtin-library-pthread_create> line 20: warning: pointer parameter types differ between declaration and definition "pthread_create"
old definition in module twostage_3 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i line 956
signed int (pthread_t *, const pthread_attr_t *, void * (*)(void *), void *)
new definition in module <built-in-library> file <builtin-library-pthread_create> line 20
signed int (pthread_t *thread, const pthread_attr_t *attr, void * (*start_routine)(void *), void *arg)
file <builtin-library-pthread_mutex_lock> line 17: 
reason for conflict at #this.__data: number of members is different (6/8)

struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  signed int __kind;
  unsigned int __nusers;
  union $anon0;
}
struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  unsigned int __nusers;
  signed int __kind;
  signed short int __spins;
  signed short int __elision;
  __pthread_list_t __list;
}
warning: pointer parameter types differ between declaration and definition "pthread_mutex_lock"
old definition in module twostage_3 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i line 1069
signed int (pthread_mutex_t *)
new definition in module <built-in-library> file <builtin-library-pthread_mutex_lock> line 17
signed int (pthread_mutex_t *mutex)
file <builtin-library-fprintf> line 12: 
reason for conflict at #this: number of members is different (30/29)

struct _IO_FILE {
  signed int _flags;
  char * _IO_read_ptr;
  char * _IO_read_end;
  char * _IO_read_base;
  char * _IO_write_base;
  char * _IO_write_ptr;
  char * _IO_write_end;
  char * _IO_buf_base;
  char * _IO_buf_end;
  char * _IO_save_base;
  char * _IO_backup_base;
  char * _IO_save_end;
  struct _IO_marker * _markers;
  struct _IO_FILE * _chain;
  signed int _fileno;
  signed int _flags2;
  __off_t _old_offset;
  unsigned short int _cur_column;
  signed char _vtable_offset;
  char [1] _shortbuf;
  _IO_lock_t * _lock;
  unsigned int $pad21;
  __off64_t _offset;
  void * __pad1;
  void * __pad2;
  void * __pad3;
  void * __pad4;
  size_t __pad5;
  signed int _mode;
  char [40] _unused2;
}
struct _IO_FILE {
  signed int _flags;
  char * _IO_read_ptr;
  char * _IO_read_end;
  char * _IO_read_base;
  char * _IO_write_base;
  char * _IO_write_ptr;
  char * _IO_write_end;
  char * _IO_buf_base;
  char * _IO_buf_end;
  char * _IO_save_base;
  char * _IO_backup_base;
  char * _IO_save_end;
  struct _IO_marker * _markers;
  struct _IO_FILE * _chain;
  signed int _fileno;
  signed int _flags2;
  __off_t _old_offset;
  unsigned short int _cur_column;
  signed char _vtable_offset;
  char [1] _shortbuf;
  _IO_lock_t * _lock;
  __off64_t _offset;
  struct _IO_codecvt * _codecvt;
  struct _IO_wide_data * _wide_data;
  struct _IO_FILE * _freeres_list;
  void * _freeres_buf;
  size_t __pad5;
  signed int _mode;
  char [40] _unused2;
}
warning: pointer parameter types differ between declaration and definition "fprintf"
old definition in module twostage_3 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i line 210
signed int (FILE *, const char *, ...)
new definition in module <built-in-library> file <builtin-library-fprintf> line 12
signed int (FILE *stream, const char * restrict format, ...)
file <builtin-library-pthread_mutex_init> line 27: 
reason for conflict at #this.__data: number of members is different (6/8)

struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  signed int __kind;
  unsigned int __nusers;
  union $anon0;
}
struct __pthread_mutex_s {
  signed int __lock;
  unsigned int __count;
  signed int __owner;
  unsigned int __nusers;
  signed int __kind;
  signed short int __spins;
  signed short int __elision;
  __pthread_list_t __list;
}
warning: pointer parameter types differ between declaration and definition "pthread_mutex_init"
old definition in module twostage_3 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i line 1062
signed int (pthread_mutex_t *, const pthread_mutexattr_t *)
new definition in module <built-in-library> file <builtin-library-pthread_mutex_init> line 27
signed int (pthread_mutex_t *mutex, const pthread_mutexattr_t *mutexattr)
file /usr/include/stdio.h line 145: warning: conflicting pointer types for variable "stderr"
old definition in module twostage_3 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i line 182
struct _IO_FILE {
  signed int _flags;
  char * _IO_read_ptr;
  char * _IO_read_end;
  char * _IO_read_base;
  char * _IO_write_base;
  char * _IO_write_ptr;
  char * _IO_write_end;
  char * _IO_buf_base;
  char * _IO_buf_end;
  char * _IO_save_base;
  char * _IO_backup_base;
  char * _IO_save_end;
  struct _IO_marker * _markers;
  struct _IO_FILE * _chain;
  signed int _fileno;
  signed int _flags2;
  __off_t _old_offset;
  unsigned short int _cur_column;
  signed char _vtable_offset;
  char [1] _shortbuf;
  _IO_lock_t * _lock;
  unsigned int $pad21;
  __off64_t _offset;
  void * __pad1;
  void * __pad2;
  void * __pad3;
  void * __pad4;
  size_t __pad5;
  signed int _mode;
  char [40] _unused2;
} *
new definition in module <built-in-library> file /usr/include/stdio.h line 145
struct _IO_FILE {
  signed int _flags;
  char * _IO_read_ptr;
  char * _IO_read_end;
  char * _IO_read_base;
  char * _IO_write_base;
  char * _IO_write_ptr;
  char * _IO_write_end;
  char * _IO_buf_base;
  char * _IO_buf_end;
  char * _IO_save_base;
  char * _IO_backup_base;
  char * _IO_save_end;
  struct _IO_marker * _markers;
  struct _IO_FILE * _chain;
  signed int _fileno;
  signed int _flags2;
  __off_t _old_offset;
  unsigned short int _cur_column;
  signed char _vtable_offset;
  char [1] _shortbuf;
  _IO_lock_t * _lock;
  __off64_t _offset;
  struct _IO_codecvt * _codecvt;
  struct _IO_wide_data * _wide_data;
  struct _IO_FILE * _freeres_list;
  void * _freeres_buf;
  size_t __pad5;
  signed int _mode;
  char [40] _unused2;
} *
Removal of function pointers and virtual functions
file <builtin-library-__spawned_thread> line 34 function __spawned_thread: replacing function pointer by 2 possible targets
Generic Property Instrumentation
Running with 8 object bits, 24 offset bits (default)
Starting Bounded Model Checking
argc''s upper bound is 1073741824
Use SV-COMP unwinding strategy: 2
Deagle's solver is set!!!!!!
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 0
**** WARNING: no body for function __isoc99_sscanf
[Debug][Analyzer] Base EvalInt argc query answering bot instead of Unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1275:5)
[Debug][Analyzer] Base EvalInt argc != 1 query answering bot instead of Unknown (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1275:5)
[Warning][Unknown] Spawning functions from unknown function: iTThreads (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1280:13)
[Warning][Unknown] Not creating a thread from iTThreads because its type is int  (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1280:13)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(iTThreads,
                                     NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1280:13)
[Warning][Unknown] Spawning functions from unknown function: iRThreads (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1281:13)
[Warning][Unknown] Not creating a thread from iRThreads because its type is int  (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1281:13)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(iRThreads, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1281:13)
[Warning][Unknown] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1277:13)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1277:13)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(err, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1289:5)
[Warning][Unknown] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1290:9)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1290:9)
[Warning][Unknown] Invalidating expressions: AddrOf(Var(err, NoOffset)) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1293:5)
[Warning][Unknown] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1294:9)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TNamed(FILE, TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1294:9)
[Warning][Unknown] Unknown address in (FILE * __restrict  )stderr has escaped. (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1267:9)
[Warning][Unknown] Invalidating expressions: CastE(TPtr(TNamed(FILE,
                                            TCompLoop(struct _IO_FILE, _, ), ),  __restrict  ), Lval(Var(stderr, NoOffset))) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1267:9)
[Warning][Deadcode] Function "__bswap_32" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:415:1)
[Warning][Deadcode] Function "__bswap_64" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:420:1)
[Warning][Deadcode] Function "__uint16_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:425:1)
[Warning][Deadcode] Function "__uint32_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:430:1)
[Warning][Deadcode] Function "__uint64_identity" will never be called: 1LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:435:1)
[Warning][Deadcode] Function "lock" will never be called: 4LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1325:1)
[Warning][Deadcode] Function "unlock" will never be called: 4LoC (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1332:1)
[Warning][Race] Memory location data2Value@twostage_3.i:1239:12 (race with conf. 110):
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1264:5)
  write with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1249:5)
[Warning][Race] Memory location data1Value@twostage_3.i:1238:12 (race with conf. 110):
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1249:5)
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1257:5)
  read with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1261:5)
  write with {} (conf. 110) (/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i:1246:5)

Summary for all memory locations:
	safe:            2
	vulnerable:      0
	unsafe:          2
	-------------------
	total:           4
Unwinding loop main.0 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i line 1299 function main thread 0
Not unwinding loop main.0 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i line 1299 function main thread 0
Unwinding loop main.1 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i line 1305 function main thread 0
Not unwinding loop main.1 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i line 1305 function main thread 0
pointer handling for concurrency is unsound
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 0
Unwinding loop main.2 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i line 1311 function main thread 0
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 0
Not unwinding loop main.2 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i line 1311 function main thread 0
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 0
Unwinding loop main.3 iteration 1 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i line 1317 function main thread 0
aborting path on assume(false) at file <builtin-library-exit> line 7 function exit thread 0
Not unwinding loop main.3 iteration 2 file /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i line 1317 function main thread 0
aborting path on assume(false) at file <builtin-library-__spawned_thread> line 34 function __spawned_thread thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 2
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 3
aborting path on assume(false) at file <builtin-library-__spawned_thread> line 34 function __spawned_thread thread 4
aborting path on assume(false) at file <builtin-library-abort> line 6 function abort thread 4
Handling datarace, passing the problem to goblint first
getcwd: /mnt/goblint-svcomp/benchexec/tools-pldi/deagle
/mnt/goblint-svcomp/benchexec/tools-pldi/deagle/goblint/goblint /mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i | tee goblint/goblint_output: 0
Lines where datarace may occur: 1246 1247 1249 1250 1257 1258 1261 1262 1264 1265 1267 1268 1280 1281 
The number of races before goblint filter: 276
The number of races after goblint filter: 33
Race categories: 10
	1246(1) - 1246(1) data1Value:
		data1Value#2 data1Value#6
		data1Value#2 data1Value#12
		data1Value#6 data1Value#12
	1246(1) - 1249(1) data1Value:
		data1Value#2 data1Value#7
		data1Value#2 data1Value#13
		data1Value#6 data1Value#13
	1246(1) - 1257(1) data1Value:
		data1Value#2 data1Value#4
		data1Value#2 data1Value#8
		data1Value#2 data1Value#10
		data1Value#6 data1Value#8
		data1Value#6 data1Value#10
	1246(1) - 1261(1) data1Value:
		data1Value#2 data1Value#5
		data1Value#2 data1Value#9
		data1Value#2 data1Value#11
		data1Value#6 data1Value#9
		data1Value#6 data1Value#11
	1249(1) - 1246(1) data1Value:
		data1Value#3 data1Value#6
		data1Value#3 data1Value#12
		data1Value#7 data1Value#12
	1257(1) - 1246(1) data1Value:
		data1Value#4 data1Value#12
		data1Value#8 data1Value#12
	1261(1) - 1246(1) data1Value:
		data1Value#5 data1Value#12
		data1Value#9 data1Value#12
	1249(1) - 1249(1) data2Value:
		data2Value#2 data2Value#4
		data2Value#2 data2Value#7
		data2Value#4 data2Value#7
	1249(1) - 1264(1) data2Value:
		data2Value#2 data2Value#3
		data2Value#2 data2Value#5
		data2Value#2 data2Value#6
		data2Value#4 data2Value#5
		data2Value#4 data2Value#6
	1264(1) - 1249(1) data2Value:
		data2Value#3 data2Value#7
		data2Value#5 data2Value#7
Runtime Symex: 2.46894s
Adding SC constraints
Shared __CPROVER_threads_exited: 8R/5W
Shared __CPROVER_next_thread_id: 7R/5W
Shared stdout: 7R/1W
Shared stderr: 21R/1W
Shared iTThreads: 3R/1W
Shared iRThreads: 4R/1W
Shared data1Value: 9R/4W
Shared data2Value: 3R/4W
Shared data1Lock: 30R/2W
Shared data2Lock: 24R/2W
Shared symex_dynamic::dynamic_object1: 15R/17W
Shared symex_dynamic::dynamic_object2: 12R/14W
Shared main::1::tPool!0@1[[0]]: 4R/1W
Shared main::1::tPool!0@1[[1]]: 4R/2W
Shared main::1::rPool!0@1[[0]]: 4R/2W
Shared fprintf::format!0@2: 3R/2W
Shared fprintf::format!0@3: 3R/2W
Shared fprintf::format!0@4: 3R/2W
Shared fprintf::format!0@5: 3R/2W
Shared fprintf::format!2@1: 3R/2W
Shared fprintf::format!3@1: 3R/2W
Shared fprintf::format!4@1: 3R/2W
size of program expression: 2208 steps
no slicing due to threads
Generated 0 VCC(s), 0 remaining after simplification
Runtime Postprocess Equation: 0.0189573s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.0392696s
Set Deagle solver's graph
Running propositional reduction
Post-processing
Runtime Post-process: 0.00472893s
Solving with Deagle's Closure solver
66948 variables, 242669 clauses
ClosureSolver finishes with 1029 conflicts, 1788364 decisions, and 6757792 propagations. 117 theory propagations and 17 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.7358s
Runtime decision procedure: 0.806379s
Running propositional reduction
Solving with Deagle's Closure solver
66948 variables, 236277 clauses
ClosureSolver finishes with 1034 conflicts, 1800140 decisions, and 6825389 propagations. 117 theory propagations and 18 cycles included.
SAT checker: instance is SATISFIABLE
Runtime Solver: 0.0100241s
Runtime decision procedure: 0.010054s
Running propositional reduction
Solving with Deagle's Closure solver
66948 variables, 236278 clauses
ClosureSolver finishes with 1036 conflicts, 1800142 decisions, and 6827250 propagations. 117 theory propagations and 18 cycles included.
SAT checker: instance is UNSATISFIABLE
Runtime Solver: 0.000228463s
Runtime decision procedure: 0.000240334s

** Results:
/mnt/goblint-svcomp/benchexec/sv-benchmarks/c/pthread/twostage_3.i function main
[nodatarace.assertion.0] line 1306 No data races on variable data1Value between line 1246 and line 1246: SUCCESS
[nodatarace.assertion.1] line 1306 No data races on variable data1Value between line 1246 and line 1249: FAILURE
[nodatarace.assertion.2] line 1306 No data races on variable data1Value between line 1246 and line 1257: SUCCESS
[nodatarace.assertion.3] line 1306 No data races on variable data1Value between line 1246 and line 1261: SUCCESS
[nodatarace.assertion.4] line 1306 No data races on variable data1Value between line 1249 and line 1246: FAILURE
[nodatarace.assertion.5] line 1306 No data races on variable data1Value between line 1257 and line 1246: SUCCESS
[nodatarace.assertion.6] line 1306 No data races on variable data1Value between line 1261 and line 1246: SUCCESS
[nodatarace.assertion.7] line 1306 No data races on variable data2Value between line 1249 and line 1249: SUCCESS
[nodatarace.assertion.8] line 1306 No data races on variable data2Value between line 1249 and line 1264: SUCCESS
[nodatarace.assertion.9] line 1306 No data races on variable data2Value between line 1264 and line 1249: SUCCESS

** 2 of 10 failed (3 iterations)
VERIFICATION FAILED
