Tool 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*
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-05 05:46:16 CET 2018-12-06 09:44:44 CET 2018-12-06 10:50:29 CET 2018-12-06 10:57:45 CET 2018-12-12 19:32:16 CET 2018-12-06 09:52:34 CET
Run set cpa-seq.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-cpa-seq.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-witness2test-validate-violation-witnesses-cpa-seq.sv-comp19_prop-memsafety.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp19_prop-memsafety.MemSafety-LinkedLists
Options -svcomp19 -heap 10000M -benchmark -timelimit 900s -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/cpa-seq.2018-12-05_0546.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cpa-seq.2018-12-05_0546.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/cpa-seq.2018-12-05_0546.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cpa-seq.2018-12-05_0546.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cpa-seq.2018-12-05_0546.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 timeout 0 wit inspect 900   740   4600 8700 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     1100   .70 0  
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i error (recursion) 0 wit inspect 4.3 1.6 290 37 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     1100   1.6  0  
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 910   260   11000 6000 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     860     2500   .71 0  
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 910   580   5000 7300 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     1500   .60 0  
heap-manipulation/tree_false-unreach-call_false-valid-deref.i timeout 0 wit inspect 920   260   11000 5300 0   0   error (1) 0 --- inspect .93 .56 44 0   0   timeout 0 --- inspect 97     80     760   .65 0   unknown 0 --- inspect 1.1  .69 50 0   0      error (1) 0 --- inspect .074  .074  11    0     0     - --- inspect
heap-manipulation/tree_false-valid-deref.i timeout 0 wit inspect 930   350   11000 7600 0   0   error (1) 0 --- inspect .95 .55 45 0   0   false(valid-deref) 1 --- inspect 9.6   5.3   330   .62 0   unknown 0 --- inspect 1.1  .70 50 0   0      error (1) 0 --- inspect .071  .071  11    0     0     - --- inspect
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i timeout (segmentation fault) 0 --- inspect 910   240   11000 5900 0   0   error (invalid witness file) 0 --- inspect .61 .37 40 0   0   error (2) 0 --- inspect .023 .024 5.7 0    0   error (invalid witness file) 0 --- inspect .96 .63 47 0   0      error (invalid witness file) 0 --- inspect .0049 .0057 .39 0     0     - --- inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 970   280   11000 6500 0   0   error (invalid witness file) 0 --- inspect .67 .41 42 0   0   error (invalid witness file) 0 --- inspect 5.3   2.9   270   .61 0   error (invalid witness file) 0 --- inspect .98 .64 49 0   0      error (invalid witness file) 0 --- inspect .0019 .0024 .54 0     0     - --- inspect
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   330   11000 6500 0   0   error (1) 0 --- inspect .88 .54 44 0   0   timeout 0 --- inspect 96     62     710   1.1  0   unknown 0 --- inspect 1.0  .64 49 0   0      error (1) 0 --- inspect .095  .094  11    0     .025 - --- inspect
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 920   350   11000 6600 0   0   error (1) 0 --- inspect .79 .47 47 0   0   timeout 0 --- inspect 97     70     790   .72 0   unknown 0 --- inspect 1.1  .70 50 0   0      error (1) 0 --- inspect .075  .077  11    0     0     - --- inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 910   280   11000 6200 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     850     1300   .81 0  
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 970   300   11000 6600 0   0   error (invalid witness file) 0 --- inspect .68 .41 44 0   0   error (invalid witness file) 0 --- inspect 5.4   2.9   270   .61 0   error (invalid witness file) 0 --- inspect .96 .63 48 0   0      error (invalid witness file) 0 --- inspect .0044 .0054 .52 0     0     - --- inspect
list-properties/list_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 910   330   11000 7000 0   0   error (1) 0 --- inspect .82 .49 45 0   0   unknown 0 --- inspect 30     19     540   .68 0   unknown 0 --- inspect 1.0  .66 49 0   0      error (1) 0 --- inspect .069  .069  11    0     0     - --- inspect
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 930   330   11000 6700 0   0   error (1) 0 --- inspect .69 .41 44 0   0   unknown 0 --- inspect 23     13     390   .75 0   unknown 0 --- inspect 1.0  .65 50 0   0      error (1) 0 --- inspect .071  .071  11    0     0     - --- inspect
list-properties/simple_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   320   11000 6500 0   0   error (1) 0 --- inspect .80 .48 44 0   0   unknown 0 --- inspect 29     17     480   .71 0   unknown 0 --- inspect 1.0  .65 49 0   0      error (1) 0 --- inspect .077  .077  11    0     0     - --- inspect
list-properties/splice_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 910   280   11000 6600 0   0   error (1) 0 --- inspect .94 .56 47 0   0   unknown 0 --- inspect 23     13     370   .71 0   unknown 0 --- inspect 1.1  .68 50 0   0      error (1) 0 --- inspect .079  .080  11    0     0     - --- inspect
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i true 2 wit inspect 6.8 2.0 300 54 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (7) 0 --- inspect 35     19     520   .71 0  
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i true 2 wit inspect 6.4 2.0 300 60 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (7) 0 --- inspect 31     18     530   .75 0  
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i true 2 wit inspect 6.6 2.0 290 56 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (7) 0 --- inspect 34     19     520   .71 0  
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 7.0 2.1 300 65 0   0   false(valid-memtrack) 1 wit inspect 8.3  4.4  310 0   0   error (7) 0 --- inspect 31     18     520   .68 0   unknown 0 --- inspect 7.8  4.3  280 0   .0041 error (2) 0 --- inspect 1.0    1.0    21    .13  0     - --- inspect
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 6.8 2.1 300 56 0   0   false(valid-memtrack) 1 wit inspect 9.0  4.7  310 0   0   error (7) 0 --- inspect 31     17     540   .23 0   unknown 0 --- inspect 7.6  4.4  280 0   3.1    error (2) 0 --- inspect 1.0    1.0    21    .13  0     - --- inspect
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 6.7 2.1 300 58 0   0   false(valid-memtrack) 1 wit inspect 8.8  4.6  310 0   0   error (7) 0 --- inspect 33     19     520   .68 0   unknown 0 --- inspect 7.7  4.4  290 0   .0041 error (2) 0 --- inspect 1.0    1.0    21    .13  0     - --- inspect
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 7.1 2.1 310 55 0   0   false(valid-memtrack) 1 wit inspect 8.0  4.2  320 0   0   error (7) 0 --- inspect 33     18     520   .71 0   unknown 0 --- inspect 7.8  4.4  290 0   3.1    error (2) 0 --- inspect 1.0    1.0    21    .13  0     - --- inspect
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 7.0 2.1 300 61 0   0   false(valid-memtrack) 1 wit inspect 9.0  4.7  310 0   0   error (7) 0 --- inspect 33     19     530   .71 0   unknown 0 --- inspect 7.1  4.0  280 0   .012  error (2) 0 --- inspect 1.0    1.0    21    .13  0     - --- inspect
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 6.7 2.1 300 59 0   0   false(valid-memtrack) 1 wit inspect 9.2  4.8  310 0   0   error (7) 0 --- inspect 34     19     520   .68 0   unknown 0 --- inspect 7.8  4.3  280 0   3.6    error (2) 0 --- inspect 1.0    1.0    21    .13  .012 - --- inspect
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 6.8 2.0 310 54 0   0   false(valid-memtrack) 1 wit inspect 8.2  4.3  310 0   0   error (7) 0 --- inspect 32     18     530   .71 0   unknown 0 --- inspect 7.7  4.3  280 0   3.3    error (2) 0 --- inspect 1.0    1.0    21    .13  0     - --- inspect
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 6.8 2.1 300 56 0   0   false(valid-memtrack) 1 wit inspect 8.5  4.5  330 0   0   error (7) 0 --- inspect 32     18     530   .71 0   unknown 0 --- inspect 8.2  4.6  300 0   0      error (2) 0 --- inspect 1.0    1.0    21    .13  0     - --- inspect
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 7.0 2.1 300 62 0   0   false(valid-memtrack) 1 wit inspect 8.1  4.3  320 0   0   error (7) 0 --- inspect 35     19     520   .71 0   unknown 0 --- inspect 7.6  4.3  280 0   .0041 error (2) 0 --- inspect 1.0    1.0    21    .13  0     - --- inspect
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 7.2 2.1 310 58 0   0   false(valid-memtrack) 1 wit inspect 9.8  5.2  320 0   0   error (7) 0 --- inspect 31     18     540   .71 0   unknown 0 --- inspect 7.5  4.3  290 0   .0041 error (2) 0 --- inspect 1.0    1.0    21    .13  .086 - --- inspect
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 970   280   11000 5900 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect 5.4   3.0   260   .61 0  
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   370   9300 4800 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     990   .68 0  
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 920   350   11000 6000 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     870     2300   .90 0  
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 970   230   11000 5700 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect 5.3   3.2   260   .65 0  
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 930   280   11000 6400 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     860     2100   2.1  0  
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 970   280   11000 6300 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect 6.6   4.0   260   .66 0  
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i timeout (segmentation fault) 0 --- inspect 920   330   11000 5800 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i timeout (segmentation fault) 0 --- inspect 910   340   11000 6800 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0    0  
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 940   290   11000 6200 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     1400   1.5  0  
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 910   270   11000 6400 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     890     2000   .63 0  
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   360   10000 4700 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     870     2200   1.7  0  
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 910   370   9300 4600 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     830     1300   .63 0  
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 920   360   11000 6100 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     870     2200   .72 0  
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 970   230   11000 5800 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect 5.3   2.9   270   .65 0  
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 920   390   11000 6400 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     860     1100   .69 0  
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 970   410   12000 7300 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .047 .049 5.5 0    0  
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 930   350   11000 6800 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     860     2200   1.8  0  
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i timeout (segmentation fault) 0 --- inspect 920   350   11000 7000 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.6 0    0  
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 930   300   11000 6600 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     2200   2.0  0  
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i timeout 0 wit inspect 930   420   12000 7400 0   0   error (1) 0 --- inspect .74 .45 44 0   0   timeout (false(valid-deref)) 0 --- inspect 92     62     830   .62 0   unknown 0 --- inspect 1.0  .66 49 0   0      error (1) 0 --- inspect .082  .081  11    0     0     - --- inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i timeout (segmentation fault) 0 --- inspect 930   280   11000 5600 0   0   error (invalid witness file) 0 --- inspect .57 .36 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .96 .64 47 0   0      error (invalid witness file) 0 --- inspect .0046 .0059 .54 0     0     - --- inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i timeout (segmentation fault) 0 --- inspect 920   400   12000 7400 0   0   error (invalid witness file) 0 --- inspect .76 .46 42 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .99 .65 47 0   0      error (invalid witness file) 0 --- inspect .0016 .0021 .53 0     0     - --- inspect
list-simple/dll2c_append_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.2 1.5 280 39 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     940   .65 0  
list-simple/dll2c_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.2 1.5 290 35 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     970   2.0  0  
list-simple/dll2c_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.3 1.5 280 44 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     940     910   .74 0  
list-simple/dll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.4 1.5 290 38 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     930   1.9  0  
list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.2 1.5 280 36 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     820   .71 0  
list-simple/dll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.1 1.4 290 36 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     810   1.7  0  
list-simple/dll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.0 1.4 280 33 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     1200   .71 0  
list-simple/dll2c_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.2 1.6 280 35 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     900     720   .90 0  
list-simple/dll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.3 1.5 280 38 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 340     300     960   .62 0  
list-simple/dll2c_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.3 1.5 280 38 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 350     320     1100   .62 0  
list-simple/dll2n_append_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.3 1.5 280 34 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout (error (7)) 0 --- inspect 920     880     2200   .68 0  
list-simple/dll2n_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.1 1.5 260 35 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     2100   .68 0  
list-simple/dll2n_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.2 1.5 280 40 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1100   .65 0  
list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.5 1.5 290 38 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1800   .63 0  
list-simple/dll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.3 1.5 280 34 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     780   .68 0  
list-simple/dll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.2 1.5 280 37 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     770   .70 0  
list-simple/dll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.2 1.5 280 38 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     1100   1.3  0  
list-simple/dll2n_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.2 1.5 280 34 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 170     140     970   .62 0  
list-simple/dll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.1 1.5 260 35 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     1800   .66 0  
list-simple/dll2n_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.2 1.5 280 36 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     1300   .63 0  
list-simple/sll2c_append_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.2 1.5 280 35 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1400   .63 0  
list-simple/sll2c_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.3 1.5 280 38 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1400   1.7  0  
list-simple/sll2c_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.1 1.5 280 35 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1300   .64 0  
list-simple/sll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.3 1.5 280 35 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1100   .63 0  
list-simple/sll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.2 1.5 280 38 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1400   1.7  0  
list-simple/sll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.0 1.5 260 38 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1400   .63 0  
list-simple/sll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.2 1.5 280 39 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     900     730   .70 0  
list-simple/sll2c_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.2 1.5 280 34 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 380     340     690   .62 0  
list-simple/sll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.5 1.5 290 35 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     900   .70 0  
list-simple/sll2c_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.1 1.5 290 41 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     880   .72 0  
list-simple/sll2n_append_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.1 1.4 260 34 0   0   - --- inspect - --- inspect - --- inspect - --- inspect error (7) 0 --- inspect 710     680     2200   .71 0  
list-simple/sll2n_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.2 1.5 280 37 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     940     2300   .72 0  
list-simple/sll2n_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.4 1.5 280 38 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     940     1000   .72 0  
list-simple/sll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.4 1.5 280 40 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1000   1.8  0  
list-simple/sll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.2 1.5 280 34 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     790   .70 0  
list-simple/sll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.0 1.4 280 36 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     850   .72 0  
list-simple/sll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.2 1.5 280 40 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     900     920   .69 0  
list-simple/sll2n_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.1 1.4 280 37 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 380     350     890   .62 0  
list-simple/sll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.2 1.5 280 40 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 510     480     1200   .62 0  
list-simple/sll2n_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.3 1.5 280 37 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 630     600     920   .62 0  
list-ext3-properties/dll_circular_traversal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.7 1.6 290 38 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     2900   .63 0  
list-ext3-properties/dll_nondet_free_order_true-valid-memsafety.i true 2 wit inspect 4.2 1.5 280 37 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     940     1900   .63 0  
list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.4 1.5 290 38 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     890     2000   1.6  0  
list-ext3-properties/sll_circular_traversal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.1 1.5 270 37 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1300   .64 0  
list-ext3-properties/sll_length_check_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 21   5.5 1200 150 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     890     2400   1.2  0  
list-ext3-properties/sll_nondet_insert_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 280   150   5900 2100 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     1200   1.0  0  
list-ext3-properties/sll_of_sll_nondet_append_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 910   430   7000 5500 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     940     630   1.7  0  
list-ext3-properties/sll_shallow_copy_true-valid-memsafety.i true 2 wit inspect 4.0 1.5 280 35 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 16     10     500   .62 0  
list-ext3-properties/dll_circular_traversal_false-valid-deref.i false(valid-deref) 1 wit inspect 4.7 1.6 280 39 0   0   false(valid-deref) 1 wit inspect 7.6  4.1  260 0   0   timeout 0 --- inspect 97     86     3000   .98 0   unknown 0 --- inspect 6.1  3.4  270 0   0      false(valid-deref) 1 --- inspect .70   .73   21    .082 .025 - --- inspect
list-ext3-properties/sll_circular_traversal_false-valid-deref.i false(valid-deref) 1 wit inspect 4.6 1.6 290 41 0   0   false(valid-deref) 1 wit inspect 6.2  3.3  260 0   0   out of memory 0 --- inspect 69     45     7000   .68 0   unknown 0 --- inspect 5.9  3.3  280 0   .25   false(valid-deref) 1 --- inspect .72   .72   21    .082 0     - --- inspect
list-ext3-properties/dll_nondet_free_order_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 4.2 1.6 290 36 0   0   false(valid-memtrack) 1 wit inspect 4.9  2.6  260 0   0   unknown 0 --- inspect 18     11     350   .71 0   unknown 0 --- inspect 4.8  2.9  260 0   3.4    false(valid-deref) -16 --- inspect .69   .69   21    .086 .025 - --- inspect
list-ext3-properties/sll_shallow_copy_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 3.9 1.5 280 33 0   0   false(valid-memtrack) 1 wit inspect 4.4  2.4  250 0   0   true -32 --- inspect 13     7.9   450   .66 0   unknown 0 --- inspect 4.3  2.5  250 0   0      true -32 --- inspect .64   .64   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 114 36000 13000 430000 250000 0   0   28 14 120 65 4800 0   0   28 -31 1000   680   22000 17    0   28 0 110 65 4600 0   17 28 -46 14    14    400 1.6   .17  75 16 56000 53000 90000 65   0  
    correct results 64 114 600 250 25000 4800 0   0   14 14 110 58 4200 0   0   1 1 9.6 5.3 330 .62 0   0 2 2 1.4  1.4  42 .16  .025 8 16 2800 2500 7100 5.0 0  
        correct true 50 100 520 220 21000 4000 0   0   0 0 0 0 8 16 2800 2500 7100 5.0 0  
        correct false 14 14 86 27 4200 730 0   0   14 14 110 58 4200 0   0   1 1 9.6 5.3 330 .62 0   0 2 2 1.4  1.4  42 .16  .025 0
    incorrect results 0 0 1 -32 13   7.9 450 .66 0   0 2 -48 1.3  1.3  41 .16  .025 0
        incorrect true 0 0 1 -32 13   7.9 450 .66 0   0 1 -32 .64 .64 20 .070 0     0
        incorrect false 0 0 0 0 1 -16 .69 .69 21 .086 .025 0
score (103 tasks, max score: 178) 114 14 -31 0 -46 16
Run set cpa-seq.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-cpa-seq.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-witness2test-validate-violation-witnesses-cpa-seq.sv-comp19_prop-memsafety.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp19_prop-memsafety.MemSafety-LinkedLists