2022-03-09 11:25:39
/home/simmo/dev/goblint/sv-comp/analyzer/goblint --conf /home/simmo/dev/goblint/sv-comp/goblint-bench/index/conf/td3.json -v --disable dbg.compare_runs.glob --enable solverdiffs --compare_runs original increment restart.c
Custom include dirs:
  1. /home/simmo/dev/goblint/sv-comp/goblint/includes (exists=true)
Preprocessing files.
Preprocessor cpp: is_bad=false
'cpp' '--undef' '__BLOCKS__' '-I' '/home/simmo/dev/goblint/sv-comp/goblint/includes' '/home/simmo/dev/goblint/sv-comp/goblint/includes/stdlib.c' '-o' '.goblint/preprocessed/stdlib.i'
'cpp' '--undef' '__BLOCKS__' '-I' '/home/simmo/dev/goblint/sv-comp/goblint/includes' '/home/simmo/dev/goblint/sv-comp/goblint/includes/pthread.c' '-o' '.goblint/preprocessed/pthread.i'
'cpp' '--undef' '__BLOCKS__' '-I' '/home/simmo/dev/goblint/sv-comp/goblint/includes' 'restart.c' '-o' '.goblint/preprocessed/restart.i'
Parsing files.
Frontc is parsing .goblint/preprocessed/stdlib.i
Converting CABS->CIL
Frontc is parsing .goblint/preprocessed/pthread.i
Converting CABS->CIL
Frontc is parsing .goblint/preprocessed/restart.i
Converting CABS->CIL
Pre-merging (0) .goblint/preprocessed/stdlib.i
Pre-merging (1) .goblint/preprocessed/pthread.i
Pre-merging (2) .goblint/preprocessed/restart.i
Final merging phase (0): .goblint/preprocessed/stdlib.i
Final merging phase (1): .goblint/preprocessed/pthread.i
Final merging phase (2): .goblint/preprocessed/restart.i
Constructors: 
Adding constructors to: main
And now...  the Goblin!
Startfuns: [main]
Exitfuns: []
Otherfuns: []
Using new format for phases!
Activated analyses for phase 0: expRelation, base, threadid, threadflag, threadreturn, escape, mutex, access, mallocWrapper
Activated transformations for phase 0: 
Generating the control flow graph.
Initializing 1 globals.
Executing 2 assigns.
Unmarshalling original/solver.marshalled... If type of content changed, this will result in a segmentation fault!
Unmarshalling increment/solver.marshalled... If type of content changed, this will result in a segmentation fault!

Comparing precision of original (left) with increment (right) as EqConstrSys:
either varinfo * std option * std or varinfo:((g, ), (int )): original more precise than increment
  original: lifted Set (std) and Set (varinfo * std option * std):{110, false, restart.c:7:5-7:14, & g, thread:[main, t_fun1], 110, true, restart.c:27:13-27:18, & g, thread:[main]}
  more precise than
  increment: lifted Set (std) and Set (varinfo * std option * std):{110, false, restart.c:7:5-7:14, & g, thread:[main, t_fun1], 110, true, restart.c:13:5-13:10, & g, thread:[main, t_fun2], 110, true, restart.c:27:13-27:18, & g, thread:[main]}
  reverse diff: Set (std): {110, false, restart.c:7:5-7:14, & g, thread:[main, t_fun1], 110, true, restart.c:13:5-13:10, & g, thread:[main, t_fun2], 110, true, restart.c:27:13-27:18, & g, thread:[main]} not leq {110, false, restart.c:7:5-7:14, & g, thread:[main, t_fun1], 110, true, restart.c:27:13-27:18, & g, thread:[main]}
    because 110, true, restart.c:13:5-13:10, & g, thread:[main, t_fun2]

Comparison summary: original more precise than increment    (more precise: 1, less precise: 0, total: 46)

[Warning][Unknown] Calculated state for undefined function: unexpected node Statement pthread_create((pthread_t * __restrict  )(& id2), (pthread_attr_t const   * __restrict  )((void *)0), & t_fun2, (void * __restrict  )((void *)0));
[Warning][Unknown] Calculated state for undefined function: unexpected node Statement return ((void *)0);
[Warning][Unknown] Calculated state for undefined function: unexpected node Statement return (0);
[Warning][Race] Memory location g@restart.c:4:5-4:6 (race with conf. 110):
  read with thread:[main, t_fun1] (conf. 110) (restart.c:7:5-7:14)
  write with thread:[main] (conf. 110) (restart.c:27:13-27:18)

Summary for all memory locations:
	safe:            0
	vulnerable:      0
	unsafe:          1
	-------------------
	total:           1

vars = 0    evals = 0    narrow_reuses = 0    aborts = 0

Timings:
TOTAL                           0.022 s
  parse                           0.009 s
  convert to CIL                  0.005 s
  analysis                        0.008 s
    global_inits                    0.001 s
    warn_global                     0.001 s
      access                          0.001 s
Timing used
Memory statistics: total=30.83MB, max=7.32MB, minor=28.85MB, major=6.73MB, promoted=4.75MB
    minor collections=14  major collections=2 compactions=0