Tool CBMC 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:48:40 CET 2018-12-06 08:59:15 CET 2018-12-06 10:10:50 CET 2018-12-06 10:22:39 CET 2018-12-12 19:29:48 CET 2018-12-06 09:23:57 CET
Run set cbmc.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-cbmc.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-cbmc.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-memsafety.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-cbmc.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.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc.2018-12-04_2248.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.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc.2018-12-04_2248.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 (42) 0 --- inspect 880     880     3800   8000    1.7   0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0     
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     2500   8400    2.4   0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .024 5.6 0    0     
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i out of memory 0 --- inspect 310     310     13000   3200    12     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .028 5.6 0    0     
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     4500   11000    1.9   0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .028 5.6 0    0     
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(valid-memtrack) -16 wit inspect .25  .25  18   2.9  .012 0     timeout 0 wit inspect 94   66   2700 0   0     error (7) 0 --- inspect 19   11   310 .71 0     timeout (exception) 0 --- inspect 92   64   3600 0     0   false(valid-deref) 1 --- inspect .66 .66 21 .094 .22   - --- inspect
heap-manipulation/tree_false-valid-deref.i false(valid-deref) 1 wit inspect .26  .26  18   2.8  .012 0     false(valid-deref) 1 wit inspect 5.7 3.1 250 0   0     error (7) 0 --- inspect 17   10   310 .68 0     timeout (exception) 0 --- inspect 92   70   3000 0     0   false(valid-deref) 1 --- inspect .68 .70 20 .094 0      - --- inspect
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .14  .14  10   1.7  .012 0     error (recursion) 0 wit inspect 5.0 2.7 250 0   0     unknown 0 --- inspect 37   20   510 .71 0     timeout 0 --- inspect 98   66   4200 .016 0   true -32 --- inspect .69 .71 21 .090 .025  - --- inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .23  .22  18   3.5  .012 0     timeout 0 wit inspect 94   69   2700 0   0     error (7) 0 --- inspect 17   10   320 .71 0     timeout (exception) 0 --- inspect 92   66   3400 0     0   true -32 --- inspect .70 .70 21 .094 .025  - --- inspect
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .23  .22  13   2.3  .012 0     timeout 0 wit inspect 95   64   2500 0   .057 error (7) 0 --- inspect 17   9.8 310 .68 0     timeout (exception) 0 --- inspect 92   68   3500 0     0   error (1) 0 --- inspect .58 .58 21 .020 0      - --- inspect
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .15  .15  11   1.6  .012 0     timeout 0 wit inspect 93   65   2600 0   0     error (7) 0 --- inspect 16   9.4 310 .68 0     timeout 0 --- inspect 93   69   3300 0     0   error (1) 0 --- inspect .57 .57 21 .020 0      - --- inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     5000   10000    2.5   0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .028 5.7 0    0     
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .11  .11  7.1 .80 .012 0     timeout 0 wit inspect 96   67   2800 0   0     true -32 --- inspect 8.5 4.8 310 .62 0     timeout (exception) 0 --- inspect 91   66   3500 0     0   true -32 --- inspect .66 .66 20 .078 .26   - --- inspect
list-properties/list_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .16  .16  10   1.5  .012 0     timeout 0 --- inspect 96   68   2800 0   0     unknown 0 --- inspect 19   11   340 .68 0     timeout (exception) 0 --- inspect 92   68   3400 0     0   true -32 --- inspect .66 .66 21 .078 0      - --- inspect
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .083 .079 6.7 .55 .012 0     timeout 0 wit inspect 93   63   3200 0   0     true -32 --- inspect 7.9 4.6 300 .66 0     timeout 0 --- inspect 92   67   3300 0     0   true -32 --- inspect .66 .66 20 .074 .025  - --- inspect
list-properties/simple_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .080 .079 7.7 1.1  .012 0     timeout 0 wit inspect 93   64   2800 0   0     true -32 --- inspect 8.1 4.5 300 .66 0     timeout 0 --- inspect 98   74   3300 .020 0   true -32 --- inspect .67 .69 20 .078 0      - --- inspect
list-properties/splice_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .12  .11  9.0 1.3  .012 0     timeout 0 wit inspect 94   63   3000 0   0     unknown 0 --- inspect 17   10   310 .75 0     timeout (exception) 0 --- inspect 92   66   3600 0     0   true -32 --- inspect .66 .66 20 .082 0      - --- inspect
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i true 2 wit inspect 120     120     970   1200    8.1   0     - --- inspect - --- inspect - --- inspect - --- inspect error (7) 0 --- inspect 240     150     770   .68 0     
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i true 2 wit inspect 99     99     940   1000    6.2   0     - --- inspect - --- inspect - --- inspect - --- inspect error (7) 0 --- inspect 210     120     800   .68 0     
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i true 2 wit inspect 110     110     960   1100    7.4   0     - --- inspect - --- inspect - --- inspect - --- inspect error (7) 0 --- inspect 220     140     780   .68 0     
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 79     79     1700   870    1.8   0     true -32 wit inspect 13   6.5 450 0   0     error (7) 0 --- inspect 32   18   550 .68 0     unknown 0 --- inspect 9.7 5.1 430 0     0   error (2) 0 --- inspect 1.0  1.0  21 .13  .098  - --- inspect
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 82     82     1700   940    1.8   0     true -32 wit inspect 14   7.3 440 0   0     error (7) 0 --- inspect 33   19   530 .75 0     unknown 0 --- inspect 9.8 5.2 430 0     0   error (2) 0 --- inspect 1.0  1.0  21 .13  0      - --- inspect
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 84     84     1700   860    1.8   0     true -32 wit inspect 12   6.2 440 0   0     error (7) 0 --- inspect 38   20   510 .68 0     unknown 0 --- inspect 10   5.5 420 0     0   error (2) 0 --- inspect 1.0  1.0  21 .13  0      - --- inspect
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 78     78     1700   960    1.8   0     true -32 wit inspect 14   7.3 450 0   0     error (7) 0 --- inspect 32   18   510 .75 0     unknown 0 --- inspect 9.7 5.1 430 0     0   error (2) 0 --- inspect 1.0  1.0  21 .13  0      - --- inspect
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 82     82     1700   820    1.8   0     true -32 wit inspect 14   7.5 450 0   0     error (7) 0 --- inspect 39   21   520 .71 0     unknown 0 --- inspect 9.4 5.0 420 0     0   error (2) 0 --- inspect 1.0  1.0  21 .13  .0041 - --- inspect
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 82     82     1700   980    1.8   .012 true -32 wit inspect 13   6.6 440 0   0     error (7) 0 --- inspect 33   19   530 .75 0     unknown 0 --- inspect 10   5.3 430 0     0   error (2) 0 --- inspect 1.0  1.0  21 .13  0      - --- inspect
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 83     83     1700   830    1.8   0     true -32 wit inspect 14   7.2 450 0   0     error (7) 0 --- inspect 29   17   530 .68 0     unknown 0 --- inspect 10   5.5 420 0     0   error (2) 0 --- inspect 1.0  1.0  21 .13  0      - --- inspect
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 81     81     1700   870    1.8   0     true -32 wit inspect 13   6.8 440 0   0     error (7) 0 --- inspect 31   18   530 .68 0     unknown 0 --- inspect 10   5.3 420 0     0   error (2) 0 --- inspect 1.0  1.0  21 .13  0      - --- inspect
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 82     82     1700   870    1.8   0     true -32 wit inspect 16   8.0 450 0   0     error (7) 0 --- inspect 39   21   540 .75 0     unknown 0 --- inspect 9.9 5.2 420 0     0   error (2) 0 --- inspect 1.0  1.0  21 .13  0      - --- inspect
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 82     82     1700   990    1.9   0     true -32 wit inspect 12   6.2 450 0   0     error (7) 0 --- inspect 30   17   520 .75 0     unknown 0 --- inspect 10   5.5 420 0     0   error (2) 0 --- inspect 1.0  1.0  21 .13  0      - --- inspect
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     680   12000    14     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0     
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i out of memory 0 --- inspect 250     250     15000   3000    4.6   0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0     
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     3700   10000    5.7   0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .028 5.6 0    0     
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     4100   13000    10     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .026 5.6 0    0     
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     2600   7800    1.7   0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0     
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     2800   6400    2.1   0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0     
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     5300   13000    5.6   .13  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0     
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     1500   7800    4.2   0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.6 0    0     
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     610   9500    3.9   0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .029 5.6 0    0     
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     600   10000    17     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0    0     
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     1100   6100    .77  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .027 5.6 0    0     
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i out of memory 0 --- inspect 220     220     15000   2800    3.8   0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0    0     
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 870     880     3900   11000    5.6   0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0     
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     4200   12000    8.5   0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .028 5.6 0    0     
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     2100   12000    2.1   0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .027 5.6 0    0     
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     1300   8300    1.1   0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.6 0    0     
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     2400   11000    17     0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.7 0    0     
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     2000   9200    7.8   0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .027 5.6 0    0     
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     500   10000    3.0   0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0     
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-memtrack) -16 wit inspect .18  .18  15   2.2  .012 0     timeout 0 wit inspect 94   76   1900 0   0     error (7) 0 --- inspect 17   10   310 .68 0     timeout 0 --- inspect 97   75   3100 0     0   error (1) 0 --- inspect .56 .56 21 .020 0      - --- inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) 0 wit inspect .16  .15  11   1.8  .012 0     timeout 0 wit inspect 98   73   2400 0   0     error (7) 0 --- inspect 21   13   310 .75 0     timeout (exception) 0 --- inspect 92   65   3800 0     0   error (1) 0 --- inspect .60 .60 21 .020 0      - --- inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-memtrack) -16 wit inspect .14  .14  11   1.7  .012 0     timeout 0 wit inspect 94   70   2600 0   0     error (7) 0 --- inspect 19   11   310 .71 0     timeout 0 --- inspect 98   76   3200 .020 0   error (1) 0 --- inspect .56 .56 20 .020 0      - --- inspect
list-simple/dll2c_append_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .33  .33  8.8 3.8  .11  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     860   .66 0     
list-simple/dll2c_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .34  .33  8.9 3.6  .11  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     1000   1.2  0     
list-simple/dll2c_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .32  .32  8.7 3.7  .11  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1100   .66 0     
list-simple/dll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .35  .35  9.5 4.8  .11  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     940   1.2  0     
list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .32  .32  8.5 4.0  .11  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     860   1.3  0     
list-simple/dll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .31  .31  8.8 4.2  .11  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     790   .63 0     
list-simple/dll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .27  .27  7.4 3.3  .074 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     1400   .91 0     
list-simple/dll2c_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .29  .28  7.2 3.3  .074 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     900     820   .71 0     
list-simple/dll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .23  .23  7.7 3.3  .086 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 320     280     1200   .62 0     
list-simple/dll2c_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .25  .25  7.7 2.7  .086 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 400     350     1100   .62 0     
list-simple/dll2n_append_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .29  .29  9.9 3.9  .12  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout (error (7)) 0 --- inspect 910     880     2300   .68 0     
list-simple/dll2n_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .32  .32  10   3.5  .12  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     1400   1.3  0     
list-simple/dll2n_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .30  .30  9.4 3.5  .10  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     940     1300   .63 0     
list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .32  .32  11   4.9  .11  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1300   .65 0     
list-simple/dll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .27  .27  9.2 3.4  .098 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     950   1.3  .0082
list-simple/dll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .28  .28  9.7 3.7  .10  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     850   .62 0     
list-simple/dll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .27  .27  9.4 3.1  .098 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     1100   .68 0     
list-simple/dll2n_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .24  .24  6.9 2.3  .061 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 210     180     970   .62 0     
list-simple/dll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .23  .22  7.8 2.4  .074 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     900     1700   .63 0     
list-simple/dll2n_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .24  .23  8.3 2.7  .078 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     1500   1.3  0     
list-simple/sll2c_append_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .29  .29  8.9 3.7  .12  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1200   1.2  0     
list-simple/sll2c_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .34  .34  9.5 4.0  .14  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1200   .63 0     
list-simple/sll2c_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .28  .27  8.2 3.5  .098 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1100   1.5  0     
list-simple/sll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .31  .30  8.7 3.7  .11  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     1000   .63 0     
list-simple/sll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .29  .28  9.0 3.8  .12  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1700   .63 0     
list-simple/sll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .30  .30  9.1 4.7  .12  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1400   .63 0     
list-simple/sll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .34  .33  9.3 3.4  .13  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     880     730   1.6  0     
list-simple/sll2c_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .27  .27  8.3 2.7  .098 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 440     390     650   .62 0     
list-simple/sll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .22  .22  7.4 3.0  .086 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     900     880   1.6  0     
list-simple/sll2c_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .23  .22  7.7 2.9  .082 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     900     860   1.6  0     
list-simple/sll2n_append_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .27  .27  10   3.1  .11  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1700   .72 0     
list-simple/sll2n_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .29  .28  10   3.3  .12  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     940     2200   1.3  0     
list-simple/sll2n_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .25  .25  9.3 3.2  .098 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     940     870   .72 0     
list-simple/sll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .28  .28  10   3.4  .11  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     940     1100   1.1  0     
list-simple/sll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .24  .23  8.6 3.5  .098 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     940     860   .72 0     
list-simple/sll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .26  .26  9.5 3.9  .10  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     860   .69 0     
list-simple/sll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .24  .24  9.3 3.0  .098 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     900     950   1.1  0     
list-simple/sll2n_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .19  .18  6.7 1.9  .057 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 340     320     740   .62 0     
list-simple/sll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .22  .22  7.9 2.8  .082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 520     480     940   .62 0     
list-simple/sll2n_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .20  .20  8.1 2.7  .078 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 640     600     880   .62 0     
list-ext3-properties/dll_circular_traversal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .29  .28  9.9 3.2  .12  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     2800   1.2  0     
list-ext3-properties/dll_nondet_free_order_true-valid-memsafety.i true 2 wit inspect .21  .20  7.3 2.3  .061 0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1900   .63 0     
list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .32  .32  12   3.8  .17  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     880     1900   .70 0     
list-ext3-properties/sll_circular_traversal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .26  .25  8.8 2.7  .12  0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     1200   .62 0     
list-ext3-properties/sll_length_check_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 5.4   5.4   78   72    1.3   0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     890     2500   .69 0     
list-ext3-properties/sll_nondet_insert_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 18     18     230   250    1.5   0     - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     1300   .63 0     
list-ext3-properties/sll_of_sll_nondet_append_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     4000   12000    2.9   0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0     
list-ext3-properties/sll_shallow_copy_true-valid-memsafety.i true 2 wit inspect .097 .097 6.9 .87 .016 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 20     13     510   .66 0     
list-ext3-properties/dll_circular_traversal_false-valid-deref.i false(valid-deref) 1 wit inspect .23  .22  9.6 2.8  .13  0     true -32 wit inspect 5.5 2.9 260 0   0     timeout 0 --- inspect 97   86   2900 .68 0     unknown 0 --- inspect 5.4 3.0 270 0     0   false(valid-deref) 1 --- inspect .66 .66 22 .082 0      - --- inspect
list-ext3-properties/sll_circular_traversal_false-valid-deref.i false(valid-deref) 1 wit inspect .23  .22  9.0 2.3  .12  0     true -32 wit inspect 5.9 3.2 270 0   0     out of memory 0 --- inspect 72   45   7000 .65 .012 unknown 0 --- inspect 6.9 3.8 260 0     0   false(valid-deref) 1 --- inspect .67 .67 22 .082 0      - --- inspect
list-ext3-properties/dll_nondet_free_order_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .18  .17  6.9 2.6  .053 0     true -32 wit inspect 6.4 3.4 260 0   0     unknown 0 --- inspect 21   12   360 .68 0     unknown 0 --- inspect 5.2 2.9 260 0     0   true -32 --- inspect .65 .65 20 .086 0      - --- inspect
list-ext3-properties/sll_shallow_copy_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .078 .075 6.7 .80 .012 0     true -32 wit inspect 5.4 2.9 270 0   0     unknown 0 --- inspect 18   10   320 .75 0     unknown 0 --- inspect 4.2 2.4 250 0     0   true -32 --- inspect .66 .66 20 .070 .13   - --- 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 55 21000    21000    120000 240000   190     .14  28 -447 1300   900   38000 0   .057 28 -96 790 480 20000 20   .012 28 0 1400 1000 53000 .057 0   28 -284 22   22   580 2.5  .79 75 16 41000 39000 60000 43   .0082
    correct results 53 103 360    360    3600 3800   29     0     1 1 5.7 3.1 250 0   0     0 0 4 4 2.7 2.7 84 .35 .22 8 16 2900 2600 7100 5.0 0     
        correct true 50 100 360    360    3600 3800   29     0     0 0 0 0 8 16 2900 2600 7100 5.0 0     
        correct false 3 3 .72 .70 37 7.9 .26  0     1 1 5.7 3.1 250 0   0     0 0 4 4 2.7 2.7 84 .35 .22 0
    correct-unconfimed results 22 0 820    820    17000 9000   18     .012 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0
        correct-unconfirmed false 22 0 820    820    17000 9000   18     .012 0 0 0 0 0
    incorrect results 3 -48 .58 .57 43 6.8 .037 0     14 -448 160   82   5500 0   0     3 -96 24 14 920 1.9 0     0 9 -288 6.0 6.0 180 .73 .47 0
        incorrect true 0 14 -448 160   82   5500 0   0     3 -96 24 14 920 1.9 0     0 9 -288 6.0 6.0 180 .73 .47 0
        incorrect false 3 -48 .58 .57 43 6.8 .037 0     0 0 0 0 0
score (103 tasks, max score: 178) 55 -447 -96 0 -284 16
Run set cbmc.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-cbmc.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-cbmc.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-memsafety.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-cbmc.sv-comp19_prop-memsafety.MemSafety-LinkedLists