Tool PredatorHP 3.14 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 ULTIMATE Automizer 0.1.23-635dfa2a
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon* apollon001 apollon138 apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-07 04:08:42 CET 2018-12-07 09:10:21 CET 2018-12-07 10:32:34 CET 2018-12-07 10:52:42 CET 2018-12-12 20:53:36 CET 2018-12-07 09:31:44 CET
Run set predatorhp.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-predatorhp.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-predatorhp.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-witness2test-validate-violation-witnesses-predatorhp.sv-comp19_prop-memsafety.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-predatorhp.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-predatorhp.sv-comp19_prop-memsafety.MemSafety-LinkedLists
Options --witness error-witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const -witness ../../results-verified/predatorhp.2018-12-07_0408.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/predatorhp.2018-12-07_0408.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true -witness ../../results-verified/predatorhp.2018-12-07_0408.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/predatorhp.2018-12-07_0408.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/predatorhp.2018-12-07_0408.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .74 .30 50 6.5 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1200   .64 0  
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .79 .29 46 7.2 .0041 .074 - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     1100   .73 0  
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .83 .28 52 7.3 .0041 .15  - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     860     2500   1.1  0  
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .82 .28 47 7.8 .0041 .074 - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     1500   .63 0  
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .62 .28 36 6.1 .049  .15  false(valid-deref) 1 wit inspect 4.4 2.4 250 0   0   error (7) 0 --- inspect 16   9.7 310 .68 0   timeout 0 --- inspect 92   66   3500 0     0   true -32 --- inspect .68 .68 20 .094 0     - --- inspect
heap-manipulation/tree_false-valid-deref.i false(valid-deref) 1 wit inspect .17 .30 38 1.4 .049  .53  false(valid-deref) 1 wit inspect 4.2 2.3 250 0   0   error (7) 0 --- inspect 17   9.8 310 .68 0   timeout 0 --- inspect 95   72   3200 0     0   false(valid-deref) 1 --- inspect .69 .69 20 .094 0     - --- inspect
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .19 .32 37 1.4 .098  0     false(valid-memtrack) 1 wit inspect 4.6 2.5 250 0   0   true -32 --- inspect 13   7.5 400 .62 0   timeout 0 --- inspect 97   67   4000 .012 0   true -32 --- inspect .68 .68 20 .090 0     - --- inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .16 .30 37 1.3 .098  .14  false(valid-memtrack) 1 wit inspect 4.5 2.5 250 0   0   error (7) 0 --- inspect 18   10   310 .68 0   timeout 0 --- inspect 92   68   3500 0     0   true -32 --- inspect .71 .71 20 .094 0     - --- inspect
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .25 .29 50 1.8 .049  19     false(valid-memtrack) 1 wit inspect 4.6 2.5 260 0   0   error (7) 0 --- inspect 17   9.5 320 .68 0   timeout (exception) 0 --- inspect 95   71   3300 0     0   false(valid-deref) -16 --- inspect .66 .66 20 .086 0     - --- inspect
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .19 .32 34 1.3 .049  .13  false(valid-memtrack) 1 wit inspect 4.4 2.4 250 0   0   error (7) 0 --- inspect 16   9.4 310 .68 0   timeout 0 --- inspect 98   75   3200 .89  0   false(valid-deref) -16 --- inspect .66 .66 20 .086 0     - --- inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900    450    1800 6600   .012  .19  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0  
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .35 .32 50 1.4 .098  19     timeout 0 wit inspect 98   66   2900 0   0   unknown 0 --- inspect 17   10   300 .68 0   timeout (exception) 0 --- inspect 91   67   3200 0     0   false(valid-deref) -16 --- inspect .65 .65 20 .078 0     - --- inspect
list-properties/list_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .16 .29 36 1.4 .098  .13  false(valid-memtrack) 1 wit inspect 4.3 2.4 250 0   0   unknown 0 --- inspect 16   9.3 310 .68 0   timeout 0 --- inspect 94   69   3300 0     0   false(valid-deref) -16 --- inspect .65 .65 20 .078 0     - --- inspect
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .16 .29 32 1.8 .098  0     timeout 0 wit inspect 93   66   2800 0   0   unknown 0 --- inspect 16   8.8 320 .68 0   timeout (exception) 0 --- inspect 92   67   3300 0     0   true -32 --- inspect .66 .66 20 .074 0     - --- inspect
list-properties/simple_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .26 .29 50 1.7 .098  19     false(valid-memtrack) 1 wit inspect 4.4 2.4 250 0   0   unknown 0 --- inspect 22   13   390 .68 0   timeout (exception) 0 --- inspect 92   68   3200 0     0   true -32 --- inspect .69 .69 20 .078 0     - --- inspect
list-properties/splice_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .39 .32 51 1.3 .049  19     false(valid-memtrack) 1 wit inspect 4.3 2.4 250 0   0   unknown 0 --- inspect 18   10   310 .68 0   timeout (exception) 0 --- inspect 92   66   3500 0     0   true -32 --- inspect .66 .66 20 .082 0     - --- inspect
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i true 2 wit inspect .64 .31 61 4.8 .012  .34  - --- inspect - --- inspect - --- inspect - --- inspect error (7) 0 --- inspect 32     18     540   .68 0  
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i true 2 wit inspect .63 .31 58 4.8 .012  .28  - --- inspect - --- inspect - --- inspect - --- inspect error (7) 0 --- inspect 34     19     550   .75 0  
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i true 2 wit inspect .60 .32 59 5.2 .012  .28  - --- inspect - --- inspect - --- inspect - --- inspect error (7) 0 --- inspect 33     18     520   .68 0  
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .61 .28 78 4.2 .074  19     true -32 wit inspect 9.4 4.9 410 0   0   error (7) 0 --- inspect 31   18   520 .68 0   unknown 0 --- inspect 7.7 4.1 380 0     0   true -32 --- inspect 1.2  1.2  22 .73  0     - --- inspect
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .60 .28 78 4.1 .074  19     true -32 wit inspect 10   5.4 420 0   0   error (7) 0 --- inspect 32   18   520 .68 0   unknown 0 --- inspect 7.9 4.2 370 0     0   true -32 --- inspect 1.2  1.2  22 .72  0     - --- inspect
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .55 .29 60 4.1 .074  .13  true -32 wit inspect 9.7 5.1 420 0   0   error (7) 0 --- inspect 31   18   530 .68 0   unknown 0 --- inspect 7.7 4.1 370 0     0   true -32 --- inspect 1.2  1.2  22 .73  0     - --- inspect
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .63 .28 78 4.9 .074  19     true -32 wit inspect 9.5 5.0 410 0   0   error (7) 0 --- inspect 32   18   520 .71 0   unknown 0 --- inspect 7.7 4.1 370 0     0   true -32 --- inspect 1.2  1.2  22 .47  0     - --- inspect
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .54 .29 59 4.6 .074  .35  true -32 wit inspect 9.1 4.8 410 0   0   error (7) 0 --- inspect 31   18   530 .68 0   unknown 0 --- inspect 7.8 4.2 370 0     0   true -32 --- inspect 1.2  1.2  22 .73  0     - --- inspect
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .50 .29 59 5.1 .074  .24  true -32 wit inspect 9.7 5.0 410 0   0   error (7) 0 --- inspect 31   17   530 .68 0   unknown 0 --- inspect 7.9 4.2 370 0     0   true -32 --- inspect 1.2  1.2  22 .73  .086 - --- inspect
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .50 .29 60 6.1 .074  .39  true -32 wit inspect 9.7 5.1 420 0   0   error (7) 0 --- inspect 29   17   520 .68 0   unknown 0 --- inspect 7.7 4.2 370 0     0   true -32 --- inspect 1.2  1.2  22 .73  0     - --- inspect
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .60 .29 78 4.5 .074  19     true -32 wit inspect 9.2 4.8 410 0   0   error (7) 0 --- inspect 30   17   520 .68 0   unknown 0 --- inspect 7.5 4.0 370 0     0   true -32 --- inspect 1.2  1.2  22 .73  0     - --- inspect
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .55 .30 59 4.1 .074  .28  true -32 wit inspect 9.6 5.0 420 0   0   error (7) 0 --- inspect 32   18   520 .71 0   unknown 0 --- inspect 8.7 4.6 370 0     0   true -32 --- inspect 1.2  1.2  22 .73  0     - --- inspect
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .57 .31 58 5.1 .074  0     true -32 wit inspect 9.3 4.9 410 0   0   error (7) 0 --- inspect 31   18   540 .68 0   unknown 0 --- inspect 8.0 4.3 370 0     0   true -32 --- inspect 1.2  1.2  22 .72  0     - --- inspect
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .62 .28 52 7.0 .0041 18     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     890     1500   .63 0  
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .77 .31 40 7.0 .0041 .13  - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     890     1000   .64 0  
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900    300    860 5900   .0041 .13  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .64 .30 36 7.2 .0041 .13  - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     870     900   1.0  0  
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900    300    3200 5300   .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900    300    3100 4900   .0041 18     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.5 0    0  
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .70 .31 38 7.7 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     900     1300   1.5  0  
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .66 .29 40 6.5 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     860     1900   .64 0  
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .52 .28 49 5.6 .0041 18     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     1500   .66 0  
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900    450    310 6800   .057  18     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .73 .28 37 6.7 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     870     2200   .70 0  
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .74 .28 37 8.0 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     840     910   .64 0  
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900    300    720 6100   .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0    0  
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .63 .30 38 7.1 .0041 .13  - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     870     1100   .64 0  
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900    300    3200 5300   .0041 .13  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .052 .053 5.5 0    0  
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900    300    3200 6500   .0041 .012 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .69 .29 39 7.8 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     850     1900   .66 0  
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .67 .29 39 7.0 .0041 .13  - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     830     2200   .78 0  
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .61 .31 49 4.3 .0041 18     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     2300   .65 0  
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .24 .29 37 2.1 .098  0     false(valid-deref) 1 wit inspect 5.2 2.8 260 0   0   error (7) 0 --- inspect 17   9.6 310 .68 0   timeout 0 --- inspect 98   76   3300 .045 0   true -32 --- inspect .67 .67 20 .086 0     - --- inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .17 .29 36 1.5 .098  0     false(valid-deref) 1 wit inspect 5.2 2.8 260 0   0   error (7) 0 --- inspect 18   11   320 .68 0   timeout (exception) 0 --- inspect 92   64   3600 0     0   false(valid-deref) 1 --- inspect .67 .67 20 .094 0     - --- inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .23 .30 35 2.0 .098  .012 false(valid-deref) 1 wit inspect 5.0 2.7 250 0   0   error (7) 0 --- inspect 16   9.4 310 .68 0   timeout 0 --- inspect 92   76   2900 0     0   true -32 --- inspect .65 .65 20 .086 0     - --- inspect
list-simple/dll2c_append_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .33 .31 49 1.4 .033  19     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     830   .65 0  
list-simple/dll2c_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .18 .31 37 1.4 .033  .066 - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     880   .65 0  
list-simple/dll2c_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .35 .31 49 1.5 .033  19     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     890   1.7  0  
list-simple/dll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .18 .30 37 1.5 .033  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     930   .63 0  
list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .18 .29 36 1.3 .033  .52  - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     870   .69 0  
list-simple/dll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .16 .29 37 1.5 .033  .45  - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1100   .64 0  
list-simple/dll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .37 .30 49 1.3 .033  19     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     1400   1.1  0  
list-simple/dll2c_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .31 .29 49 1.6 .033  19     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     900     830   .77 0  
list-simple/dll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .16 .29 36 1.6 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 310     280     1200   .62 0  
list-simple/dll2c_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .19 .30 37 1.3 .012  .23  - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 370     340     1100   .62 0  
list-simple/dll2n_append_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .18 .30 36 1.4 .033  0     - --- inspect - --- inspect - --- inspect - --- inspect error (7) 0 --- inspect 820     790     2300   .63 0  
list-simple/dll2n_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .19 .29 36 1.2 .033  .066 - --- inspect - --- inspect - --- inspect - --- inspect timeout (error (7)) 0 --- inspect 960     920     2300   .68 0  
list-simple/dll2n_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .30 .29 49 1.5 .033  19     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     940     1300   .99 0  
list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .18 .28 37 2.3 .033  .46  - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     2200   1.5  0  
list-simple/dll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .17 .29 37 1.3 .033  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     900   .69 0  
list-simple/dll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .18 .30 35 2.2 .033  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     780   1.4  0  
list-simple/dll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .16 .30 36 1.5 .033  .057 - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     1200   .82 0  
list-simple/dll2n_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .19 .29 35 4.0 .037  .066 - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 170     140     1000   .62 0  
list-simple/dll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .29 .29 49 1.5 .012  18     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     1400   1.0  0  
list-simple/dll2n_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .17 .30 35 1.3 .012  .057 - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     1300   .97 0  
list-simple/sll2c_append_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .26 .29 49 3.7 .033  19     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1400   1.3  0  
list-simple/sll2c_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .16 .29 35 1.6 .033  .078 - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1400   .64 0  
list-simple/sll2c_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .34 .30 49 1.3 .033  19     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1100   .65 0  
list-simple/sll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .19 .31 37 2.6 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1100   1.3  0  
list-simple/sll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .18 .30 37 1.6 .033  .14  - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1500   .63 0  
list-simple/sll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .20 .31 37 1.3 .033  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1300   .64 0  
list-simple/sll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .15 .29 36 1.5 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     900     750   .70 0  
list-simple/sll2c_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .16 .29 36 1.5 .012  .053 - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 380     340     670   .62 0  
list-simple/sll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .21 .29 49 1.8 .012  18     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     950   .71 0  
list-simple/sll2c_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .26 .29 49 1.9 .012  18     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     900     1100   1.5  0  
list-simple/sll2n_append_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .17 .29 36 1.3 .033  .13  - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     940     1800   .72 0  
list-simple/sll2n_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .18 .29 35 1.3 .033  .066 - --- inspect - --- inspect - --- inspect - --- inspect error (7) 0 --- inspect 770     740     2200   .68 0  
list-simple/sll2n_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .19 .30 36 1.3 .033  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     840   .72 0  
list-simple/sll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .17 .29 36 1.4 .033  .078 - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     960   .73 0  
list-simple/sll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .18 .29 37 1.4 .033  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     940     770   1.6  0  
list-simple/sll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .18 .31 36 1.3 .033  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     940     850   1.1  0  
list-simple/sll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .16 .30 37 1.5 .033  .053 - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     920   .71 0  
list-simple/sll2n_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .17 .29 35 1.3 .037  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 390     360     780   .62 0  
list-simple/sll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .16 .29 36 1.4 .012  .066 - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 500     470     940   .62 0  
list-simple/sll2n_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .16 .29 35 1.4 .012  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 620     590     790   .62 0  
list-ext3-properties/dll_circular_traversal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .39 .30 36 4.3 .0082 .066 - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1200   1.6  0  
list-ext3-properties/dll_nondet_free_order_true-valid-memsafety.i true 2 wit inspect .16 .29 36 1.7 .037  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     940     1900   .66 0  
list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .18 .29 48 2.3 .012  18     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     890     2100   .18 0  
list-ext3-properties/sll_circular_traversal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .33 .29 49 1.2 .033  18     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1100   1.4  0  
list-ext3-properties/sll_length_check_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 1.8  1.3  50 19   .029  18     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     890     2600   .71 0  
list-ext3-properties/sll_nondet_insert_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .74 .56 61 7.4 .033  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     1100   1.1  0  
list-ext3-properties/sll_of_sll_nondet_append_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.4  1.5  86 41   .0041 18     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     940     620   .63 0  
list-ext3-properties/sll_shallow_copy_true-valid-memsafety.i unknown 0 --- inspect .14 .29 35 1.1 0      .39  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0    0  
list-ext3-properties/dll_circular_traversal_false-valid-deref.i false(valid-deref) 1 wit inspect .16 .29 35 1.6 .074  .14  false(valid-deref) 1 wit inspect 5.5 2.9 280 0   0   true -32 --- inspect 8.4 5.1 310 .62 0   unknown 0 --- inspect 4.7 2.7 250 0     0   false(valid-deref) 1 --- inspect .68 .68 20 .082 .025 - --- inspect
list-ext3-properties/sll_circular_traversal_false-valid-deref.i false(valid-deref) 1 wit inspect .19 .29 50 2.3 .074  19     false(valid-deref) 1 wit inspect 4.9 2.7 250 0   0   timeout 0 --- inspect 97   85   790 .69 0   unknown 0 --- inspect 5.0 2.8 260 0     0   false(valid-deref) 1 --- inspect .65 .65 20 .082 0     - --- inspect
list-ext3-properties/dll_nondet_free_order_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .39 .32 51 1.4 .098  19     false(valid-memtrack) 1 wit inspect 4.5 2.5 260 0   0   unknown 0 --- inspect 29   18   550 .68 0   unknown 0 --- inspect 4.7 2.8 260 0     0   false(valid-deref) -16 --- inspect .66 .66 20 .086 0     - --- inspect
list-ext3-properties/sll_shallow_copy_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .15 .29 35 1.5 .086  .057 false(valid-memtrack) 1 wit inspect 4.2 2.3 250 0   0   unknown 0 --- inspect 23   14   430 .68 0   unknown 0 --- inspect 4.4 2.6 250 0     0   true -32 --- inspect .65 .65 20 .070 0     - --- inspect
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
total 103 148 7300   2700   21000 48000 3.6  540 28 -304 360 220 14000 0   0   28 -64 700 440 12000 19   0   28 0 1400 1000 52000 .95 0   28 -684 24   24   580 8.5  .11  75 14 56000 53000 84000 55   0  
    correct results 82 148 33   27   3500 300 2.6  410 16 16 74 40 4100 0   0   0 0 4 4 2.7 2.7 81 .35 .025 7 14 2700 2500 6400 4.4 0  
        correct true 66 132 29   22   2800 270 1.4  320 0 0 0 0 7 14 2700 2500 6400 4.4 0  
        correct false 16 16 3.9 4.8 650 30 1.3  94 16 16 74 40 4100 0   0   0 0 4 4 2.7 2.7 81 .35 .025 0
    correct-unconfimed results 12 0 6.2 3.5 750 50 .93 95 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0
        correct-unconfirmed false 12 0 6.2 3.5 750 50 .93 95 0 0 0 0 0
    incorrect results 0 10 -320 96 50 4100 0   0   2 -64 22 13 710 1.2 0   0 24 -688 21   21   500 8.2  .086 0
        incorrect true 0 10 -320 96 50 4100 0   0   2 -64 22 13 710 1.2 0   0 19 -608 18   18   400 7.8  .086 0
        incorrect false 0 0 0 0 5 -80 3.3 3.3 100 .41 0     0
score (103 tasks, max score: 178) 148 -304 -64 0 -684 14
Run set predatorhp.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-predatorhp.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-predatorhp.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-witness2test-validate-violation-witnesses-predatorhp.sv-comp19_prop-memsafety.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-predatorhp.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-predatorhp.sv-comp19_prop-memsafety.MemSafety-LinkedLists