Tool CBMC Path 5.10 () 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:45:10 CET 2018-12-06 08:53:36 CET 2018-12-06 10:12:52 CET 2018-12-06 10:22:39 CET 2018-12-12 19:23:37 CET 2018-12-06 09:28:06 CET
Run set cbmc-path.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-cbmc-path.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-cbmc-path.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-witness2test-validate-violation-witnesses-cbmc-path.sv-comp19_prop-memsafety.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-cbmc-path.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-cbmc-path.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/cbmc-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc-path.2018-12-04_2245.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/cbmc-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cbmc-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc-path.2018-12-04_2245.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 out of memory 0 --- inspect 450     450     15000   5700    2100     .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .026 5.5 0    0     
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .14  .14  9.5 1.3  .012 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0    0     
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .11  .10  9.0 1.1  .012 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0     
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i out of memory 0 --- inspect 360     360     15000   4800    1900     0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .031 .033 5.6 0    0     
heap-manipulation/tree_false-unreach-call_false-valid-deref.i error (134) 0 --- inspect .14  .13  7.4 .96 .012 0      error (invalid witness file) 0 --- inspect .74 .45 42 0   0   error (2) 0 --- inspect .024 .024 5.6 0    0   error (invalid witness file) 0 --- inspect .96 .62 48 0   0   error (invalid witness file) 0 --- inspect .0056 .0073 .52 0     0    - --- inspect
heap-manipulation/tree_false-valid-deref.i error (134) 0 --- inspect .13  .13  7.8 1.1  .012 0      error (invalid witness file) 0 --- inspect .60 .37 41 0   0   error (2) 0 --- inspect .023 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .61 47 0   0   error (invalid witness file) 0 --- inspect .0022 .0028 .53 0     0    - --- inspect
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i out of memory 0 --- inspect 620     620     15000   7800    2500     0      error (invalid witness file) 0 --- inspect .57 .34 40 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .63 47 0   0   error (invalid witness file) 0 --- inspect .0018 .0023 .53 0     0    - --- inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect .11  .11  8.1 .91 .041 0      error (invalid witness file) 0 --- inspect .76 .48 42 0   0   error (2) 0 --- inspect .020 .020 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .63 47 0   0   error (invalid witness file) 0 --- inspect .0039 .0050 .53 0     0    - --- inspect
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect .11  .11  8.3 1.1  .057 0      error (invalid witness file) 0 --- inspect .73 .45 41 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .95 .61 48 0   0   error (invalid witness file) 0 --- inspect .0060 .0076 .54 0     0    - --- inspect
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect .092 .093 7.8 .88 .049 0      error (invalid witness file) 0 --- inspect .62 .38 40 0   0   error (2) 0 --- inspect .022 .024 5.6 0    0   error (invalid witness file) 0 --- inspect .95 .62 47 0   0   error (invalid witness file) 0 --- inspect .0017 .0022 .54 0     0    - --- inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i out of memory 0 --- inspect 580     580     15000   7700    2300     .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0     
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect .065 .066 7.8 .60 .012 0      error (invalid witness file) 0 --- inspect .76 .47 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .93 .59 47 0   0   error (invalid witness file) 0 --- inspect .0050 .0061 .53 0     0    - --- inspect
list-properties/list_true-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect .071 .070 7.8 .70 .029 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 .95 .63 47 0   0   error (invalid witness file) 0 --- inspect .0058 .0074 .53 0     0    - --- inspect
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect .064 .064 7.6 .52 .012 0      error (invalid witness file) 0 --- inspect .70 .43 42 0   0   error (2) 0 --- inspect .024 .025 5.8 0    0   error (invalid witness file) 0 --- inspect 1.2  .77 46 0   0   error (invalid witness file) 0 --- inspect .0038 .0050 .41 0     0    - --- inspect
list-properties/simple_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .17  .16  7.3 1.1  .18  0      timeout 0 wit inspect 98    66    2800 0   0   true -32 --- inspect 10     5.7   300   .66 0   timeout 0 --- inspect 92    68    3500 0   0   true -32 --- inspect .64   .65   20    .078 .90 - --- inspect
list-properties/splice_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .10  .098 7.2 .91 .061 0      timeout 0 wit inspect 94    64    3100 0   0   unknown 0 --- inspect 16     9.2   330   .71 0   timeout 0 --- inspect 93    65    3500 0   0   true -32 --- inspect .66   .66   20    .082 .13 - --- inspect
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .48  .48  29   7.1  .012 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0    0     
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .47  .47  29   5.9  .012 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .027 5.7 0    0     
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .52  .52  28   6.2  .012 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 .48  .48  29   5.4  .012 0      error (invalid witness file) 0 --- inspect .62 .39 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .93 .61 47 0   0   error (invalid witness file) 0 --- inspect .0053 .0066 .53 0     0    - --- inspect
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect .48  .48  28   5.7  .012 0      error (invalid witness file) 0 --- inspect .69 .42 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .64 48 0   0   error (invalid witness file) 0 --- inspect .0041 .0068 .53 0     0    - --- inspect
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect .47  .47  28   6.3  .012 0      error (invalid witness file) 0 --- inspect .75 .47 41 0   0   error (2) 0 --- inspect .023 .024 5.7 0    0   error (invalid witness file) 0 --- inspect .99 .66 48 0   0   error (invalid witness file) 0 --- inspect .0048 .0065 .52 0     0    - --- inspect
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect .48  .48  29   6.4  .012 0      error (invalid witness file) 0 --- inspect .68 .41 41 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .65 49 0   0   error (invalid witness file) 0 --- inspect .0055 .0070 .54 0     0    - --- inspect
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect .52  .52  29   5.4  .012 0      error (invalid witness file) 0 --- inspect .61 .38 42 0   0   error (2) 0 --- inspect .027 .028 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .60 47 0   0   error (invalid witness file) 0 --- inspect .0064 .0081 .53 0     0    - --- inspect
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect .47  .47  29   7.0  .012 0      error (invalid witness file) 0 --- inspect .74 .45 41 0   0   error (2) 0 --- inspect .025 .026 5.6 0    0   error (invalid witness file) 0 --- inspect .95 .64 47 0   0   error (invalid witness file) 0 --- inspect .0021 .0028 .53 0     0    - --- inspect
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect .48  .48  29   5.0  .012 0      error (invalid witness file) 0 --- inspect .64 .40 42 0   0   error (2) 0 --- inspect .023 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .61 46 0   0   error (invalid witness file) 0 --- inspect .0049 .0065 .53 0     0    - --- inspect
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect .47  .47  28   6.7  .012 0      error (invalid witness file) 0 --- inspect .76 .46 41 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .97 .65 47 0   0   error (invalid witness file) 0 --- inspect .0047 .022  .53 0     0    - --- inspect
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect .47  .47  28   5.6  .012 0      error (invalid witness file) 0 --- inspect .65 .39 42 0   0   error (2) 0 --- inspect .024 .024 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .60 47 0   0   error (invalid witness file) 0 --- inspect .0021 .0032 .53 0     0    - --- inspect
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect .47  .47  29   6.0  .012 0      error (invalid witness file) 0 --- inspect .77 .47 41 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0   error (invalid witness file) 0 --- inspect .95 .62 47 0   0   error (invalid witness file) 0 --- inspect .0015 .0016 .39 0     0    - --- inspect
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .13  .13  8.5 .96 .053 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .028 5.7 0    0     
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .11  .11  8.4 1.2  .10  0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.6 0    0     
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .14  .14  8.3 .94 .053 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .026 5.6 0    0     
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .13  .14  9.6 1.2  .16  0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.7 0    0     
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .12  .12  8.9 1.1  .11  0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .026 5.7 0    0     
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .12  .12  8.1 1.1  .041 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0     
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .17  .17  9.4 1.3  .14  0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.7 0    0     
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .12  .12  9.4 1.4  .11  0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0     
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .11  .11  8.0 1.0  .041 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.6 0    0     
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .11  .11  8.2 1.0  .053 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 error (134) 0 --- inspect .13  .12  8.4 1.0  .012 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.7 0    0     
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .12  .12  7.8 .95 .090 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.8 0    0     
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .17  .16  7.4 1.4  .053 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .029 5.8 0    0     
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .12  .12  9.0 1.4  .14  0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0     
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .13  .13  8.5 1.1  .090 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.7 0    0     
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .10  .10  7.6 1.4  .037 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.5 0    0     
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .11  .11  8.6 1.0  .12  0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.7 0    0     
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .11  .11  8.4 1.1  .086 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0     
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .12  .12  7.6 .95 .037 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .028 5.8 0    0     
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i error (134) 0 --- inspect .11  .11  8.4 1.7  .11  0      error (invalid witness file) 0 --- inspect .69 .42 40 0   0   error (2) 0 --- inspect .028 .029 5.7 0    0   error (invalid witness file) 0 --- inspect .96 .62 47 0   0   error (invalid witness file) 0 --- inspect .0057 .0068 .52 0     0    - --- inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i error (134) 0 --- inspect .10  .10  8.2 1.1  .053 0      error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .69 47 0   0   error (invalid witness file) 0 --- inspect .0041 .0050 .54 0     0    - --- inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i error (134) 0 --- inspect .11  .11  8.2 1.0  .090 0      error (invalid witness file) 0 --- inspect .60 .39 41 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .98 .64 47 0   0   error (invalid witness file) 0 --- inspect .0055 .0070 .53 0     0    - --- inspect
list-simple/dll2c_append_equal_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 870     880     12000   13000    4100     .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.6 0    0     
list-simple/dll2c_append_unequal_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 870     880     7100   14000    4000     .0041 - --- 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 (42) 0 --- inspect 880     880     12000   11000    3900     .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0     
list-simple/dll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 870     880     7200   11000    4000     .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0     
list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     12000   11000    4200     .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .025 5.7 0    0     
list-simple/dll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     7200   10000    4000     .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0    0     
list-simple/dll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 1.5   1.5   16   18    5.9   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     1400   1.6  0     
list-simple/dll2c_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 1.7   1.7   16   23    8.4   0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     900     860   .70 .0082
list-simple/dll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 710     710     5800   10000    3600     .0082 - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 360     320     1200   .62 0     
list-simple/dll2c_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 720     720     5800   8200    3600     .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 400     350     1000   .62 0     
list-simple/dll2n_append_equal_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     14000   12000    2900     0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0     
list-simple/dll2n_append_unequal_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     15000   12000    2900     0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .025 5.6 0    0     
list-simple/dll2n_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 650     650     6300   9000    2200     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     940     1100   1.5  0     
list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 640     640     6200   7800    2200     .0041 - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1500   1.6  0     
list-simple/dll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 290     290     2800   3500    1000     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     950   1.6  0     
list-simple/dll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 290     290     2800   3400    1000     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     940     1100   1.5  3.7   
list-simple/dll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 24     24     98   300    98     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     1100   .74 0     
list-simple/dll2n_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.6   2.6   27   35    15     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 190     160     1000   .62 0     
list-simple/dll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 230     230     1900   3300    830     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     1800   1.6  0     
list-simple/dll2n_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 260     260     2200   3200    900     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     1300   1.6  0     
list-simple/sll2c_append_equal_true-unreach-call_true-valid-memsafety.i out of memory 0 --- inspect 440     440     15000   6300    2000     .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .024 5.6 0    0     
list-simple/sll2c_append_unequal_true-unreach-call_true-valid-memsafety.i out of memory 0 --- inspect 400     400     15000   5100    1800     .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .024 5.6 0    0     
list-simple/sll2c_insert_equal_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     12000   11000    4000     .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.6 0    0     
list-simple/sll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 780     780     6500   12000    3700     .0041 - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     1200   1.5  0     
list-simple/sll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i out of memory 0 --- inspect 440     440     15000   6500    2000     .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .029 5.7 0    0     
list-simple/sll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i out of memory 0 --- inspect 510     510     15000   7200    2400     .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0     
list-simple/sll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     3700   12000    4600     .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .049 .050 5.5 0    0     
list-simple/sll2c_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 31     31     150   450    200     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 440     390     770   .52 0     
list-simple/sll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 660     660     5500   6200    3500     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     870   .80 0     
list-simple/sll2c_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 630     630     5500   9100    3400     .0041 - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     900     1000   .71 0     
list-simple/sll2n_append_equal_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     13000   11000    3000     .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .027 5.6 0    0     
list-simple/sll2n_append_unequal_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     13000   11000    3000     .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.6 0    0     
list-simple/sll2n_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 290     290     2800   3500    1100     .0041 - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     920   2.2  0     
list-simple/sll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 280     280     2800   4000    1100     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1300   .80 0     
list-simple/sll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 270     270     2600   3900    980     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     800   1.6  0     
list-simple/sll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 270     270     2600   3400    980     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     790   .70 .0082
list-simple/sll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 21     21     98   280    99     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     900     980   1.6  0     
list-simple/sll2n_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .65  .65  12   10    3.2   0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 350     330     930   .62 0     
list-simple/sll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 230     230     2200   3300    970     .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 520     480     1100   .62 0     
list-simple/sll2n_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 230     230     2200   2900    910     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 660     610     980   .62 0     
list-ext3-properties/dll_circular_traversal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 19     19     160   290    86     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     3000   1.5  0     
list-ext3-properties/dll_nondet_free_order_true-valid-memsafety.i error (134) 0 --- inspect .087 .086 8.1 .94 .029 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .025 5.7 0    0     
list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     7400   11000    2300     0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0     
list-ext3-properties/sll_circular_traversal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 15     15     150   190    75     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1200   1.6  0     
list-ext3-properties/sll_length_check_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 870     880     7100   12000    3800     .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0     
list-ext3-properties/sll_nondet_insert_true-unreach-call_true-valid-memsafety.i out of memory 0 --- inspect 760     760     15000   11000    3700     .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.7 0    0     
list-ext3-properties/sll_of_sll_nondet_append_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .084 .084 9.2 .81 .012 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0     
list-ext3-properties/sll_shallow_copy_true-valid-memsafety.i true 2 wit inspect .13  .13  8.8 1.9  .21  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 17     11     520   .66 0     
list-ext3-properties/dll_circular_traversal_false-valid-deref.i error (42) 0 --- inspect 880     880     15000   12000    3600     .0041 error (invalid witness file) 0 --- inspect .60 .38 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .63 47 0   0   error (invalid witness file) 0 --- inspect .0055 .0066 .53 0     0    - --- inspect
list-ext3-properties/sll_circular_traversal_false-valid-deref.i out of memory 0 --- inspect 830     830     15000   11000    3600     .0082 error (invalid witness file) 0 --- inspect .78 .47 41 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .65 48 0   0   error (invalid witness file) 0 --- inspect .0053 .0066 .53 0     0    - --- inspect
list-ext3-properties/dll_nondet_free_order_false-valid-memtrack.i error (134) 0 --- inspect .079 .079 9.2 1.2  .029 0      error (invalid witness file) 0 --- inspect .60 .37 42 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .67 49 0   0   error (invalid witness file) 0 --- inspect .0016 .0020 .53 0     0    - --- inspect
list-ext3-properties/sll_shallow_copy_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .091 .087 8.5 .83 .029 0      true -32 wit inspect 5.2  2.8  250 0   0   unknown 0 --- inspect 18     11     330   .68 0   unknown 0 --- inspect 4.7  2.6  270 0   0   true -32 --- inspect .65   .65   20    .070 1.1  - --- 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 54 26000    26000    380000 350000   110000    .14  28 -32 210   140   7200 0   0   28 -32 45 26   1100 2.0  0   28 0 210 150 8400 0   0   28 -96 2.1 2.1 74 .23 2.1 75 16 21000 20000 31000 30   3.7
    correct results 27 54 7500    7500    67000 99000   33000    .033 0 0 0 0 8 16 2900 2700 7500 4.9 0  
        correct true 27 54 7500    7500    67000 99000   33000    .033 0 0 0 0 8 16 2900 2700 7500 4.9 0  
        correct false 0 0 0 0 0 0
    correct-unconfimed results 3 0 .36 .35 23 2.8 .27 0     0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0
        correct-unconfirmed false 3 0 .36 .35 23 2.8 .27 0     0 0 0 0 0
    incorrect results 0 1 -32 5.2 2.8 250 0   0   1 -32 10 5.7 300 .66 0   0 3 -96 1.9 2.0 61 .23 2.1 0
        incorrect true 0 1 -32 5.2 2.8 250 0   0   1 -32 10 5.7 300 .66 0   0 3 -96 1.9 2.0 61 .23 2.1 0
        incorrect false 0 0 0 0 0 0
score (103 tasks, max score: 178) 54 -32 -32 0 -96 16
Run set cbmc-path.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-cbmc-path.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-cbmc-path.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-witness2test-validate-violation-witnesses-cbmc-path.sv-comp19_prop-memsafety.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-cbmc-path.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-cbmc-path.sv-comp19_prop-memsafety.MemSafety-LinkedLists