Tool SMACK 1.9.3 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-07 19:13:55 CET 2018-12-08 22:05:35 CET 2018-12-08 23:40:49 CET 2018-12-08 23:45:33 CET 2018-12-12 21:01:56 CET 2018-12-08 22:13:47 CET
Run set smack.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-smack.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-smack.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-witness2test-validate-violation-witnesses-smack.sv-comp19_prop-memsafety.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-smack.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-smack.sv-comp19_prop-memsafety.MemSafety-LinkedLists
Options -w 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/smack.2018-12-07_1913.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/smack.2018-12-07_1913.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/smack.2018-12-07_1913.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/smack.2018-12-07_1913.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/smack.2018-12-07_1913.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 --- inspect 750   930   660 6300 1.4 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0   0  
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 750   930   390 10000 1.5 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0   0  
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 750   930   610 6700 1.4 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .022 5.7 0   0  
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 750   930   290 7700 1.3 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0   0  
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 6.8 6.5 110 94 1.2 2.1 false(valid-deref) 1 wit inspect 5.3  2.8  280 0   0      error (7) 0 --- inspect 20     12     310   .71 0    timeout 0 --- inspect 96    65    3900 0      .029  false(valid-deref) 1 --- inspect .67   .67   20    .094 0   - --- inspect
heap-manipulation/tree_false-valid-deref.i false(valid-deref) 1 wit inspect 3.7 3.6 93 49 1.2 0   false(valid-deref) 1 wit inspect 5.1  2.8  250 0   0      error (7) 0 --- inspect 18     10     320   .75 0    timeout 0 --- inspect 97    73    3000 .0041 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) 0 wit inspect 760   760   230 8000 2.0 0   error (recursion) 0 wit inspect 5.4  2.9  250 0   0      true -32 --- inspect 9.1   5.3   310   .62 0    timeout (exception) 0 --- inspect 95    63    3900 0      .025  true -32 --- inspect .65   .64   20    .090 0   - --- inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i timeout 0 --- inspect 750   930   310 5300 1.2 0   error (invalid witness file) 0 --- inspect .59 .36 43 0   0      error (2) 0 --- inspect .019 .020 5.6 0    0    error (invalid witness file) 0 --- inspect .94 .60 47 0      0      error (invalid witness file) 0 --- inspect .0019 .0025 .54 0     0   - --- inspect
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 840   830   320 8100 2.0 0   timeout 0 wit inspect 94    76    2200 0   0      error (7) 0 --- inspect 21     12     310   .71 0    timeout (exception) 0 --- inspect 92    70    3300 0      0      false(valid-deref) -16 --- inspect .67   .67   20    .086 0   - --- inspect
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 840   830   300 9000 1.9 0   timeout 0 wit inspect 93    66    2700 0   .045  error (7) 0 --- inspect 18     10     310   .68 0    timeout (exception) 0 --- inspect 92    68    3300 0      0      false(valid-deref) -16 --- inspect .66   .68   20    .086 0   - --- inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 880   880   320 9600 1.9 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .027 5.6 0   0  
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 760   760   330 7700 1.8 0   timeout 0 wit inspect 93    65    2800 0   0      unknown 0 --- inspect 17     9.8   310   .75 0    timeout 0 --- inspect 98    69    3600 .012  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) 0 wit inspect 760   760   300 6600 1.9 0   timeout 0 wit inspect 97    80    2100 0   .061  true -32 --- inspect 8.2   5.1   310   .62 0    timeout (exception) 0 --- inspect 92    68    3300 0      0      false(valid-deref) -16 --- inspect .68   .69   20    .078 0   - --- inspect
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 760   760   330 7900 1.7 0   timeout 0 wit inspect 93    67    3300 0   0      true -32 --- inspect 10     5.8   310   .66 0    timeout 0 --- inspect 92    68    3300 0      0      true -32 --- inspect .65   .65   20    .074 0   - --- inspect
list-properties/simple_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 760   760   260 5900 1.7 0   timeout (exception) 0 wit inspect 93    65    3300 0   0      true -32 --- inspect 10     5.9   310   .66 0    timeout (exception) 0 --- inspect 92    68    3400 0      0      true -32 --- inspect .65   .65   20    .078 0   - --- inspect
list-properties/splice_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 760   760   350 9500 1.9 0   false(valid-memtrack) 1 wit inspect 4.6  2.5  270 0   0      unknown 0 --- inspect 18     10     320   .75 0    timeout 0 --- inspect 98    70    3600 .020  .56   true -32 --- inspect .64   .64   20    .082 0   - --- inspect
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i true 2 --- inspect 320   320   550 4100 7.3 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.6 0   0  
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i true 2 --- inspect 260   260   530 3100 7.1 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0   0  
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i true 2 --- inspect 210   210   540 3100 7.1 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .027 5.6 0   0  
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i timeout 0 --- inspect 750   930   670 8500 4.0 0   error (invalid witness file) 0 --- inspect .59 .35 40 0   0      error (2) 0 --- inspect .020 .020 5.6 0    0    error (invalid witness file) 0 --- inspect 1.1  .72 47 0      0      error (invalid witness file) 0 --- inspect .0017 .0021 .53 0     0   - --- inspect
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i timeout 0 --- inspect 750   930   680 9400 4.0 0   error (invalid witness file) 0 --- inspect .59 .36 41 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0    error (invalid witness file) 0 --- inspect .97 .64 47 0      0      error (invalid witness file) 0 --- inspect .0049 .0063 .54 0     0   - --- inspect
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i timeout 0 --- inspect 750   930   670 8500 4.0 0   error (invalid witness file) 0 --- inspect .58 .35 41 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0    error (invalid witness file) 0 --- inspect .96 .63 47 0      0      error (invalid witness file) 0 --- inspect .0024 .0037 .54 0     0   - --- inspect
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i timeout 0 --- inspect 750   930   680 8700 4.0 0   error (invalid witness file) 0 --- inspect .58 .36 41 0   .0041 error (2) 0 --- inspect .020 .021 5.6 0    0    error (invalid witness file) 0 --- inspect 1.3  .82 48 0      0      error (invalid witness file) 0 --- inspect .0015 .0017 .40 0     0   - --- inspect
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i timeout 0 --- inspect 750   930   670 8500 4.1 0   error (invalid witness file) 0 --- inspect .67 .42 40 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0    error (invalid witness file) 0 --- inspect .93 .61 48 0      0      error (invalid witness file) 0 --- inspect .0020 .0025 .53 0     0   - --- inspect
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i timeout 0 --- inspect 750   930   670 8700 4.1 0   error (invalid witness file) 0 --- inspect .59 .36 42 0   0      error (2) 0 --- inspect .031 .032 5.5 0    0    error (invalid witness file) 0 --- inspect 1.2  .78 47 0      0      error (invalid witness file) 0 --- inspect .0021 .0026 .52 0     0   - --- inspect
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i timeout 0 --- inspect 750   930   680 8700 4.0 1.8 error (invalid witness file) 0 --- inspect .65 .40 41 0   0      error (2) 0 --- inspect .026 .027 5.6 0    0    error (invalid witness file) 0 --- inspect .94 .60 47 0      0      error (invalid witness file) 0 --- inspect .0051 .0062 .52 0     0   - --- inspect
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i timeout 0 --- inspect 750   930   650 10000 4.1 0   error (invalid witness file) 0 --- inspect .58 .36 40 0   0      error (2) 0 --- inspect .021 .022 5.7 0    0    error (invalid witness file) 0 --- inspect .98 .63 46 0      0      error (invalid witness file) 0 --- inspect .0018 .0024 .53 0     0   - --- inspect
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i timeout 0 --- inspect 750   930   670 11000 4.1 0   error (invalid witness file) 0 --- inspect .61 .38 41 0   0      error (2) 0 --- inspect .023 .024 5.7 0    0    error (invalid witness file) 0 --- inspect .92 .61 47 0      0      error (invalid witness file) 0 --- inspect .0048 .0052 .41 0     0   - --- inspect
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i timeout 0 --- inspect 750   930   670 8500 4.2 0   error (invalid witness file) 0 --- inspect .60 .36 43 0   0      error (2) 0 --- inspect .027 .028 5.6 0    0    error (invalid witness file) 0 --- inspect .93 .60 48 0      0      error (invalid witness file) 0 --- inspect .0029 .0039 .53 0     0   - --- inspect
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 750   930   290 7300 1.3 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .025 5.6 0   0  
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 880   880   240 7900 1.9 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .028 5.6 0   0  
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 750   930   260 5800 1.2 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.7 0   0  
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 880   880   310 8000 2.2 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0   0  
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 750   930   300 7200 1.2 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.7 0   0  
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 750   930   300 7800 1.2 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.6 0   0  
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 880   880   310 8000 2.0 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0   0  
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 750   930   320 6600 1.2 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0   0  
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 880   880   330 9100 2.0 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.6 0   0  
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 750   930   280 7500 1.3 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .026 5.6 0   0  
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 750   930   340 5400 1.2 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0   0  
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 880   880   240 6100 1.9 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .023 5.6 0   0  
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 750   930   240 8900 1.1 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 880   880   300 8800 2.1 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.7 0   0  
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 750   930   290 6200 1.1 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 750   930   300 6600 1.1 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0   0  
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 880   880   330 7800 2.0 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.7 0   0  
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 750   930   340 8100 1.2 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.6 0   0  
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 880   880   290 9200 1.9 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .029 5.7 0   0  
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 0 wit inspect 5.3 5.0 110 72 1.1 0   timeout 0 wit inspect 94    62    2400 0   0      error (7) 0 --- inspect 18     10     310   .68 0    timeout 0 --- inspect 96    75    3200 .0041 0      true -32 --- inspect .66   .66   20    .086 0   - --- inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 5.6 5.6 110 74 1.3 0   false(valid-deref) 1 wit inspect 4.6  2.5  250 0   0      error (7) 0 --- inspect 17     10     310   .75 0    timeout 0 --- inspect 98    68    3900 .012  0      false(valid-deref) 1 --- inspect .66   .66   20    .094 0   - --- inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 0 wit inspect 4.9 5.0 99 60 1.1 0   timeout 0 wit inspect 95    69    2600 0   0      error (7) 0 --- inspect 18     11     310   .75 0    timeout 0 --- inspect 98    76    3200 .012  0      true -32 --- inspect .69   .68   20    .086 0   - --- inspect
list-simple/dll2c_append_equal_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 12   12   96 170 1.9 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0   0  
list-simple/dll2c_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 12   12   96 160 2.0 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.7 0   0  
list-simple/dll2c_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 12   12   100 150 2.0 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0   0  
list-simple/dll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 12   12   110 170 2.1 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .027 5.6 0   0  
list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 12   12   98 140 1.9 2.2 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.5 0   0  
list-simple/dll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 12   11   98 150 1.9 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .025 5.6 0   0  
list-simple/dll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 9.1 9.4 91 120 1.8 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .029 .030 5.6 0   0  
list-simple/dll2c_remove_all_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 9.0 9.4 91 130 1.8 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0   0  
list-simple/dll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 9.1 9.5 98 140 1.9 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .035 .036 5.5 0   0  
list-simple/dll2c_update_all_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 9.0 9.0 97 120 1.9 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .029 5.6 0   0  
list-simple/dll2n_append_equal_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 14   14   110 170 1.9 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .027 5.5 0   0  
list-simple/dll2n_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 15   16   110 210 1.9 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0   0  
list-simple/dll2n_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 12   12   100 160 2.0 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 13   14   110 170 2.0 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0   0  
list-simple/dll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 11   11   98 130 1.9 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .028 5.6 0   0  
list-simple/dll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 11   11   97 170 1.9 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
list-simple/dll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 9.0 9.4 90 120 1.8 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .024 5.6 0   0  
list-simple/dll2n_remove_all_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 8.1 8.9 86 88 1.7 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0   0  
list-simple/dll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 8.1 8.5 93 110 1.9 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .024 5.6 0   0  
list-simple/dll2n_update_all_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 8.5 9.0 95 110 1.9 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .027 5.6 0   0  
list-simple/sll2c_append_equal_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 10   10   100 140 1.9 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .028 5.7 0   0  
list-simple/sll2c_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 11   11   98 130 2.0 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .030 5.6 0   0  
list-simple/sll2c_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 9.5 9.4 99 110 1.9 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
list-simple/sll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 9.7 9.5 93 120 2.0 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.8 0   0  
list-simple/sll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 10   10   100 110 1.9 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0   0  
list-simple/sll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 9.9 10   100 140 1.9 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .027 5.7 0   0  
list-simple/sll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 8.4 8.9 96 93 1.9 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0   0  
list-simple/sll2c_remove_all_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 8.3 8.9 90 130 1.8 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .028 5.7 0   0  
list-simple/sll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 8.3 8.5 93 110 1.9 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .028 5.6 0   0  
list-simple/sll2c_update_all_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 8.3 8.5 93 100 1.9 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
list-simple/sll2n_append_equal_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 11   11   97 160 1.9 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0   0  
list-simple/sll2n_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 12   12   100 140 1.9 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
list-simple/sll2n_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 11   11   96 140 1.9 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .027 5.6 0   0  
list-simple/sll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 12   12   100 170 1.9 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .035 .036 5.6 0   0  
list-simple/sll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 10   10   93 120 1.8 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
list-simple/sll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i error (1) 0 --- inspect 5.5 5.4 94 65 1.1 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .024 5.6 0   0  
list-simple/sll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 9.1 9.4 91 130 1.8 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .025 5.6 0   0  
list-simple/sll2n_remove_all_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 7.8 8.3 85 95 1.7 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .028 5.6 0   0  
list-simple/sll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 8.4 8.9 95 89 1.9 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .028 5.7 0   0  
list-simple/sll2n_update_all_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 8.6 8.9 94 120 1.9 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0   0  
list-ext3-properties/dll_circular_traversal_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 21   22   130 300 1.8 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0   0  
list-ext3-properties/dll_nondet_free_order_true-valid-memsafety.i true 2 --- inspect 8.6 8.9 88 110 1.9 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.7 0   0  
list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 38   38   150 530 1.9 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0   0  
list-ext3-properties/sll_circular_traversal_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 18   18   110 220 1.8 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0   0  
list-ext3-properties/sll_length_check_true-unreach-call_true-valid-memsafety.i true 2 --- inspect 880   880   310 8100 1.8 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .027 5.6 0   0  
list-ext3-properties/sll_nondet_insert_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 750   930   270 8600 1.1 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.7 0   0  
list-ext3-properties/sll_of_sll_nondet_append_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 750   930   420 9200 1.2 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
list-ext3-properties/sll_shallow_copy_true-valid-memsafety.i true 2 --- inspect 6.7 7.7 78 92 1.6 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0   0  
list-ext3-properties/dll_circular_traversal_false-valid-deref.i false(valid-deref) 1 wit inspect 15   15   130 200 1.0 0   true -32 wit inspect 4.7  2.5  260 0   0      true -32 --- inspect 8.0   4.5   310   .66 .12 unknown 0 --- inspect 4.4  2.5  250 0      .0041 false(valid-deref) 1 --- inspect .65   .65   21    .082 0   - --- inspect
list-ext3-properties/sll_circular_traversal_false-valid-deref.i false(valid-deref) 1 wit inspect 14   14   110 190 1.0 0   true -32 wit inspect 5.5  2.9  260 0   0      true -32 --- inspect 8.0   4.9   320   .62 0    unknown 0 --- inspect 4.4  2.5  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 9.3 9.4 88 110 1.9 0   false(valid-memtrack) 1 wit inspect 5.4  3.0  260 0   0      true -32 --- inspect 8.7   4.8   310   .66 0    unknown 0 --- inspect 5.6  3.2  260 0      0      false(valid-deref) -16 --- inspect .66   .67   20    .086 0   - --- inspect
list-ext3-properties/sll_shallow_copy_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 7.4 8.2 86 89 1.6 0   true -32 wit inspect 4.2  2.3  250 0   0      true -32 --- inspect 9.0   5.2   300   .62 0    unknown 0 --- inspect 4.2  2.4  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 121 37000 42000 25000 380000 210   6.1 28 -91 800 580   24000 0   .11 28 -256 240 140 5400 12   .12 28 0 1300 920 46000 .066 .62 28 -299 11   11   350 1.4  0   75 0 1.8 1.9 420 0   0  
    correct results 64 121 11000 11000 9900 110000 130   4.3 5 5 25 14   1300 0   0    0 0 5 5 3.3 3.3 100 .45 0   0
        correct true 57 114 10000 10000 8900 99000 120   2.2 0 0 0 0 0
        correct false 7 7 810 810 990 10000 9.4 2.1 5 5 25 14   1300 0   0    0 0 5 5 3.3 3.3 100 .45 0   0
    correct-unconfimed results 10 0 5500 5500 2400 54000 17   0   0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0
        correct-unconfirmed false 10 0 5500 5500 2400 54000 17   0   0 0 0 0 0
    incorrect results 0 3 -96 14 7.7 760 0   0    8 -256 72 41 2500 5.1 .12 0 12 -304 7.9 7.9 240 .98 0   0
        incorrect true 0 3 -96 14 7.7 760 0   0    8 -256 72 41 2500 5.1 .12 0 7 -224 4.6 4.6 140 .57 0   0
        incorrect false 0 0 0 0 5 -80 3.3 3.4 100 .41 0   0
score (103 tasks, max score: 178) 121 -91 -256 0 -299 0
Run set smack.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-smack.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-smack.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-witness2test-validate-violation-witnesses-smack.sv-comp19_prop-memsafety.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-smack.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-smack.sv-comp19_prop-memsafety.MemSafety-LinkedLists