Tool 2LS 0.7.2-sv-comp19 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-04 22:44:17 CET 2018-12-06 09:36:46 CET 2018-12-06 10:26:50 CET 2018-12-06 10:31:50 CET 2018-12-12 19:28:33 CET 2018-12-06 09:46:05 CET
Run set 2ls.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-2ls.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-2ls.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-witness2test-validate-violation-witnesses-2ls.sv-comp19_prop-memsafety.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-2ls.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-2ls.sv-comp19_prop-memsafety.MemSafety-LinkedLists
Options --graphml-witness 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/2ls.2018-12-04_2244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/2ls.2018-12-04_2244.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/2ls.2018-12-04_2244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/2ls.2018-12-04_2244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/2ls.2018-12-04_2244.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 error (134) 0 --- inspect .23 .23 29 2.0 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.6 0    0  
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i error (5) 0 --- inspect 3.8  3.8  43 50   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.7 0    0  
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 880    880    4900 6200   .0082 .16  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900    900    4400 12000   .020  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
heap-manipulation/tree_false-unreach-call_false-valid-deref.i error (134) 0 --- inspect 110    110    1300 1100   .0082 .025 error (invalid witness file) 0 --- inspect .60 .38 40 0   0   error (2) 0 --- inspect .023 .026 5.7 0    0   error (invalid witness file) 0 --- inspect .96 .64 46 0   0   error (invalid witness file) 0 --- inspect .0050 .0063 .53 0     0     - --- inspect
heap-manipulation/tree_false-valid-deref.i false(valid-deref) 1 wit inspect 120    120    1400 1200   .0082 0     false(valid-deref) 1 wit inspect 5.2  2.8  250 0   0   error (7) 0 --- inspect 17     10     310   .71 0   timeout 0 --- inspect 92    69    3100 0   0   false(valid-deref) 1 --- inspect .71   .72   20    .094 .54  - --- inspect
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i error (5) 0 --- inspect .19 .19 26 2.0 .0082 0     error (invalid witness file) 0 --- inspect .72 .45 40 0   0   error (2) 0 --- inspect .022 .024 5.7 0    0   error (invalid witness file) 0 --- inspect .98 .62 48 0   0   error (invalid witness file) 0 --- inspect .0045 .0056 .53 0     0     - --- inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i error (5) 0 --- inspect 54    54    1000 610   .0082 0     error (invalid witness file) 0 --- inspect .78 .47 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .96 .63 47 0   0   error (invalid witness file) 0 --- inspect .0022 .0028 .53 0     0     - --- inspect
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect 18    18    360 200   .0082 .16  error (invalid witness file) 0 --- inspect .78 .48 41 0   0   error (2) 0 --- inspect .023 .025 5.6 0    0   error (invalid witness file) 0 --- inspect .96 .63 47 0   0   error (invalid witness file) 0 --- inspect .0017 .0029 .52 0     0     - --- inspect
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect 4.4  4.4  130 54   .0082 .16  error (invalid witness file) 0 --- inspect .59 .37 40 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0   error (invalid witness file) 0 --- inspect .95 .60 47 0   0   error (invalid witness file) 0 --- inspect .0017 .0024 .40 0     0     - --- inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .86 .86 37 11   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.6 0    0  
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .67 .67 32 8.8 .0082 0     timeout 0 wit inspect 98    68    2800 0   0   unknown 0 --- inspect 17     9.5   310   .71 0   timeout 0 --- inspect 95    69    3300 0   0   error (1) 0 --- inspect .60   .59   20    .016 0     - --- inspect
list-properties/list_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 2.9  2.9  72 34   .0082 0     false(valid-memtrack) 1 wit inspect 5.6  3.0  250 0   0   unknown 0 --- inspect 17     10     320   .63 0   timeout (exception) 0 --- inspect 92    68    3300 0   0   error (1) 0 --- inspect .57   .56   20    .016 0     - --- inspect
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect .44 .44 30 4.1 .0082 .16  error (invalid witness file) 0 --- inspect .69 .44 40 0   0   error (2) 0 --- inspect .023 .025 5.6 0    0   error (invalid witness file) 0 --- inspect .95 .62 47 0   0   error (invalid witness file) 0 --- inspect .0021 .0028 .53 0     0     - --- inspect
list-properties/simple_true-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect .37 .37 29 3.7 .0082 0     error (invalid witness file) 0 --- inspect .68 .42 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .95 .63 47 0   0   error (invalid witness file) 0 --- inspect .0048 .0075 .52 0     0     - --- inspect
list-properties/splice_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 2.3  2.3  72 26   .0082 0     false(valid-memtrack) 1 wit inspect 5.9  3.2  250 0   0   unknown 0 --- inspect 16     9.6   320   .68 0   timeout 0 --- inspect 92    65    3400 0   0   error (1) 0 --- inspect .59   .59   20    .016 0     - --- inspect
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .41 .41 42 3.3 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0    0  
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .42 .42 41 3.4 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .38 .38 41 4.8 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect .39 .39 42 3.8 .0082 0     error (invalid witness file) 0 --- inspect .73 .46 40 0   0   error (2) 0 --- inspect .023 .025 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .63 49 0   0   error (invalid witness file) 0 --- inspect .0017 .0022 .53 0     0     - --- inspect
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect .37 .37 42 3.7 .0082 0     error (invalid witness file) 0 --- inspect .63 .38 41 0   0   error (2) 0 --- inspect .020 .021 5.7 0    0   error (invalid witness file) 0 --- inspect 1.0  .64 48 0   0   error (invalid witness file) 0 --- inspect .0059 .0076 .53 0     0     - --- inspect
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect .39 .39 41 3.7 .0082 0     error (invalid witness file) 0 --- inspect .76 .46 41 0   0   error (2) 0 --- inspect .020 .020 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .62 47 0   0   error (invalid witness file) 0 --- inspect .0016 .0021 .53 0     0     - --- inspect
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect .38 .38 41 4.0 .0082 0     error (invalid witness file) 0 --- inspect .71 .43 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .95 .64 48 0   0   error (invalid witness file) 0 --- inspect .0055 .0069 .52 0     0     - --- inspect
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect .39 .39 42 3.6 .0082 0     error (invalid witness file) 0 --- inspect .59 .37 40 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .95 .61 48 0   0   error (invalid witness file) 0 --- inspect .0043 .0049 .40 0     0     - --- inspect
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect .37 .37 41 5.5 .0082 0     error (invalid witness file) 0 --- inspect .73 .44 40 0   0   error (2) 0 --- inspect .021 .022 5.7 0    0   error (invalid witness file) 0 --- inspect .91 .59 47 0   0   error (invalid witness file) 0 --- inspect .0022 .0028 .54 0     0     - --- inspect
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect .37 .37 42 4.4 .0082 0     error (invalid witness file) 0 --- inspect .69 .43 41 0   0   error (2) 0 --- inspect .021 .022 5.7 0    0   error (invalid witness file) 0 --- inspect .99 .64 48 0   0   error (invalid witness file) 0 --- inspect .0056 .0069 .52 0     0     - --- inspect
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect .38 .38 42 3.3 .0082 0     error (invalid witness file) 0 --- inspect .64 .39 41 0   0   error (2) 0 --- inspect .024 .025 5.6 0    0   error (invalid witness file) 0 --- inspect .95 .64 47 0   0   error (invalid witness file) 0 --- inspect .0019 .0023 .53 0     0     - --- inspect
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect .38 .38 42 4.5 .0082 0     error (invalid witness file) 0 --- inspect .62 .38 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .93 .60 47 0   0   error (invalid witness file) 0 --- inspect .0020 .0025 .52 0     0     - --- inspect
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect .40 .39 41 3.5 .0082 0     error (invalid witness file) 0 --- inspect .77 .47 41 0   0   error (2) 0 --- inspect .034 .036 5.5 0    0   error (invalid witness file) 0 --- inspect .95 .63 47 0   0   error (invalid witness file) 0 --- inspect .0016 .0020 .52 0     0     - --- inspect
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i error (5) 0 --- inspect 120    120    2200 1700   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .024 5.6 0    0  
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 2.5  2.5  82 33   .0082 .025 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .024 5.7 0    0  
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 61    61    1000 550   .0082 .16  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .037 .038 5.6 0    0  
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 10    10    270 120   .0082 .16  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .025 5.6 0    0  
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i error (5) 0 --- inspect 44    44    930 590   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0    0  
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i error (5) 0 --- inspect 54    54    990 540   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .024 5.8 0    0  
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 64    64    910 650   .0082 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 error (134) 0 --- inspect 47    47    570 410   .0082 .16  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 1.2  1.2  60 14   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.7 0    0  
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i error (5) 0 --- inspect 25    25    510 270   .0082 0     - --- 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 error (134) 0 --- inspect 51    51    840 400   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .026 5.6 0    0  
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 1.5  1.5  54 19   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .049 .050 5.5 0    0  
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 30    30    640 420   .0082 .16  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .052 .053 5.5 0    0  
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 5.8  5.8  150 61   .0082 .025 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.7 0    0  
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i error (5) 0 --- inspect 20    20    530 200   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .042 .043 5.5 0    0  
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i error (5) 0 --- inspect 24    24    590 270   .0082 0     - --- 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 error (134) 0 --- inspect 22    22    420 270   .0082 .025 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0    0  
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 24    24    340 190   .0082 .025 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0  
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .70 .70 34 8.1 .0082 .16  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .024 5.7 0    0  
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-memtrack) -16 wit inspect 6.1  6.1  210 84   .0082 0     false(valid-deref) 1 wit inspect 5.0  2.7  250 0   0   error (7) 0 --- inspect 17     9.9   310   .68 0   timeout (exception) 0 --- inspect 92    74    3000 0   0   error (1) 0 --- inspect .57   .57   20    .020 0     - --- inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 7.0  6.9  230 81   .0082 0     false(valid-deref) 1 wit inspect 6.3  3.4  260 0   0   error (7) 0 --- inspect 17     9.9   320   .68 0   timeout 0 --- inspect 94    65    3600 0   0   error (1) 0 --- inspect .60   .59   20    .020 0     - --- inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-memtrack) -16 wit inspect 2.8  2.8  110 31   .0082 0     false(valid-deref) 1 wit inspect 5.1  2.7  280 0   0   error (7) 0 --- inspect 17     10     310   .71 0   timeout (exception) 0 --- inspect 92    76    2800 0   0   error (1) 0 --- inspect .57   .57   20    .020 .025 - --- inspect
list-simple/dll2c_append_equal_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 2.9  2.9  97 40   .0082 .16  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .020 5.6 0    0  
list-simple/dll2c_append_unequal_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 3.1  3.1  99 39   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
list-simple/dll2c_insert_equal_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 5.0  5.0  140 59   .0082 .16  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0  
list-simple/dll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 3.8  3.8  120 57   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 1.1  1.1  49 18   .0082 .16  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .026 5.6 0    0  
list-simple/dll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 1.1  1.1  50 16   .0082 .025 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.6 0    0  
list-simple/dll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 7.5  7.5  370 91   .0082 .025 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0    0  
list-simple/dll2c_remove_all_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 1.2  1.2  56 14   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
list-simple/dll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.9  8.9  180 110   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 340     300     900   .62 0  
list-simple/dll2c_update_all_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 22    22    300 230   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .038 .040 5.6 0    0  
list-simple/dll2n_append_equal_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 15    15    330 180   .0082 .025 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.7 0    0  
list-simple/dll2n_append_unequal_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 13    13    300 150   .0082 .16  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .027 5.7 0    0  
list-simple/dll2n_insert_equal_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 17    17    340 160   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .031 .032 5.5 0    0  
list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 43    43    580 450   .0082 .025 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
list-simple/dll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 2.2  2.2  87 27   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .022 5.6 0    0  
list-simple/dll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 2.4  2.4  96 32   .0082 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 wit inspect 2.4  2.4  94 25   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     1200   .74 0  
list-simple/dll2n_remove_all_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .66 .66 35 8.0 .0082 .16  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
list-simple/dll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 80    80    740 680   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
list-simple/dll2n_update_all_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 82    82    690 670   .0082 .025 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
list-simple/sll2c_append_equal_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 2.1  2.1  72 26   .0082 .057 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .034 .037 5.6 0    0  
list-simple/sll2c_append_unequal_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 4.2  4.2  110 65   .0082 .16  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .020 5.6 0    0  
list-simple/sll2c_insert_equal_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 2.1  2.1  73 28   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .025 5.6 0    0  
list-simple/sll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 3.3  3.3  97 39   .0082 .16  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.7 0    0  
list-simple/sll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 1.8  1.8  65 19   .0082 .025 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.6 0    0  
list-simple/sll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 1.6  1.6  63 18   .0082 .16  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0  
list-simple/sll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .84 .84 40 12   .0082 .16  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
list-simple/sll2c_remove_all_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .91 .91 43 10   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
list-simple/sll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 5.1  5.1  120 72   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     920   .71 0  
list-simple/sll2c_update_all_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 7.2  7.2  130 72   .0082 .29  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .023 5.6 0    0  
list-simple/sll2n_append_equal_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 5.8  5.8  170 71   .0082 .16  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.6 0    0  
list-simple/sll2n_append_unequal_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 5.2  5.2  160 65   .0082 .16  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.7 0    0  
list-simple/sll2n_insert_equal_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 6.4  6.4  180 82   .0082 .16  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
list-simple/sll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 18    18    320 200   .0082 .16  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
list-simple/sll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 1.3  1.3  59 17   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.7 0    0  
list-simple/sll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 1.3  1.3  56 16   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
list-simple/sll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 1.6  1.6  71 20   .0082 .29  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
list-simple/sll2n_remove_all_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .40 .40 30 4.6 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.6 0    0  
list-simple/sll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 35    35    390 280   .0082 .16  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .025 5.6 0    0  
list-simple/sll2n_update_all_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 41    41    410 320   .0082 .16  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .020 5.6 0    0  
list-ext3-properties/dll_circular_traversal_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 4.0  4.0  87 47   .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
list-ext3-properties/dll_nondet_free_order_true-valid-memsafety.i error (5) 0 --- inspect .78 .78 37 8.7 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .023 5.6 0    0  
list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 2.5  2.5  75 30   .0082 .16  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
list-ext3-properties/sll_circular_traversal_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect 1.8  1.8  52 23   .0082 .025 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.7 0    0  
list-ext3-properties/sll_length_check_true-unreach-call_true-valid-memsafety.i out of memory 0 --- inspect 150    150    15000 1100   .020  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
list-ext3-properties/sll_nondet_insert_true-unreach-call_true-valid-memsafety.i out of memory 0 --- inspect 260    260    15000 2600   .012  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
list-ext3-properties/sll_of_sll_nondet_append_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900    900    4300 11000   .020  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0    0  
list-ext3-properties/sll_shallow_copy_true-valid-memsafety.i true 2 wit inspect .19 .19 26 1.8 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 17     11     530   .62 0  
list-ext3-properties/dll_circular_traversal_false-valid-deref.i error (134) 0 --- inspect 4.4  4.4  90 41   .0082 0     error (invalid witness file) 0 --- inspect .60 .37 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .96 .61 47 0   0   error (invalid witness file) 0 --- inspect .0054 .0071 .52 0     0     - --- inspect
list-ext3-properties/sll_circular_traversal_false-valid-deref.i error (134) 0 --- inspect 2.0  2.0  54 26   .0082 0     error (invalid witness file) 0 --- inspect .61 .38 41 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .98 .64 48 0   0   error (invalid witness file) 0 --- inspect .0041 .0053 .52 0     0     - --- inspect
list-ext3-properties/dll_nondet_free_order_false-valid-memtrack.i error (5) 0 --- inspect .74 .74 37 9.0 .0082 0     error (invalid witness file) 0 --- inspect .78 .48 42 0   0   error (2) 0 --- inspect .021 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .92 .62 47 0   0   error (invalid witness file) 0 --- inspect .0022 .0029 .53 0     0     - --- inspect
list-ext3-properties/sll_shallow_copy_false-valid-memtrack.i error (139) 0 --- inspect .19 .19 26 1.7 .0082 0     error (invalid witness file) 0 --- inspect .60 .37 40 0   0   error (2) 0 --- inspect .021 .023 5.7 0    0   error (invalid witness file) 0 --- inspect 1.0  .66 47 0   0   error (invalid witness file) 0 --- inspect .0056 .0071 .53 0     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 -20 4500    4500    68000 48000   .88   4.8 28 6 140 95 5200 0   0   28 0 120 69 2300 4.8 0   28 0 670 500 24000 0   0   28 1 4.3  4.3  150 .20  .57 75 4 2300 2100 4000 2.7 0  
    correct results 8 12 150    150    2200 1500   .066  0   6 6 33 18 1600 0   0   0 0 1 1 .71 .72 20 .094 .54 2 4 350 310 1400 1.2 0  
        correct true 4 8 17    17    410 210   .033  0   0 0 0 0 2 4 350 310 1400 1.2 0  
        correct false 4 4 140    140    1800 1300   .033  0   6 6 33 18 1600 0   0   0 0 1 1 .71 .72 20 .094 .54 0
    correct-unconfimed results 1 0 .67 .67 32 8.8 .0082 0   0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0
        correct-unconfirmed false 1 0 .67 .67 32 8.8 .0082 0   0 0 0 0 0
    incorrect results 2 -32 8.9  8.8  330 110   .016  0   0 0 0 0 0
        incorrect true 0 0 0 0 0 0
        incorrect false 2 -32 8.9  8.8  330 110   .016  0   0 0 0 0 0
score (103 tasks, max score: 178) -20 6 0 0 1 4
Run set 2ls.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-2ls.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-2ls.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-witness2test-validate-violation-witnesses-2ls.sv-comp19_prop-memsafety.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-2ls.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-2ls.sv-comp19_prop-memsafety.MemSafety-LinkedLists