Tool ULTIMATE Taipan 0.1.23-635dfa2a 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-08 14:19:36 CET 2018-12-09 20:52:23 CET 2018-12-09 21:15:16 CET 2018-12-09 21:17:48 CET 2018-12-12 21:23:28 CET 2018-12-09 20:55:36 CET
Run set utaipan.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-utaipan.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-utaipan.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-witness2test-validate-violation-witnesses-utaipan.sv-comp19_prop-memsafety.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-utaipan.sv-comp19_prop-memsafety.MemSafety-LinkedLists
Options --full-output -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/utaipan.2018-12-08_1419.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/utaipan.2018-12-08_1419.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/utaipan.2018-12-08_1419.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/utaipan.2018-12-08_1419.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/utaipan.2018-12-08_1419.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   820   1100 10000 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .046 .047 5.5 0    0  
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   840   1000 11000 .69 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.7 0    0  
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i error (7) 0 --- inspect 780   710   2200 9500 .68 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0  
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   860   860 11000 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
heap-manipulation/tree_false-unreach-call_false-valid-deref.i timeout 0 --- inspect 900   870   860 10000 .63 .025  error (invalid witness file) 0 --- inspect .59 .37 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .62 48 0   0   error (invalid witness file) 0 --- inspect .0057 .0071 .54 0     0   - --- inspect
heap-manipulation/tree_false-valid-deref.i false(valid-deref) 1 wit inspect 9.7 3.1 360 75 .66 0      false(valid-deref) 1 wit inspect 4.7  2.6  250 0   0   error (7) 0 --- inspect 20     12     320   .71 0   unknown 0 --- inspect 4.8  2.8  250 0   0   false(valid-deref) 1 --- inspect .66   .66   20    .094 0   - --- inspect
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i timeout 0 --- inspect 900   770   4000 11000 .70 .025  error (invalid witness file) 0 --- inspect .60 .38 42 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .97 .61 47 0   0   error (invalid witness file) 0 --- inspect .0045 .0063 .53 0     0   - --- inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i unknown 0 --- inspect 66   38   810 770 .75 0      error (invalid witness file) 0 --- inspect .59 .36 42 0   0   error (2) 0 --- inspect .024 .025 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .61 47 0   0   error (invalid witness file) 0 --- inspect .0050 .0078 .52 0     0   - --- inspect
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i timeout 0 --- inspect 900   860   1200 13000 .63 0      error (invalid witness file) 0 --- inspect .59 .36 40 0   0   error (2) 0 --- inspect .024 .024 5.6 0    0   error (invalid witness file) 0 --- inspect .99 .62 47 0   0   error (invalid witness file) 0 --- inspect .0058 .0088 .54 0     0   - --- inspect
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i timeout 0 --- inspect 900   810   1200 9700 .63 0      error (invalid witness file) 0 --- inspect .75 .46 40 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0   error (invalid witness file) 0 --- inspect .90 .58 46 0   0   error (invalid witness file) 0 --- inspect .0013 .0015 .41 0     0   - --- inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   790   1200 10000 .70 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .026 5.6 0    0  
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i unknown 0 --- inspect 18   6.4 380 150 .75 0      error (invalid witness file) 0 --- inspect .59 .35 41 0   0   error (2) 0 --- inspect .025 .026 5.6 0    0   error (invalid witness file) 0 --- inspect .96 .62 48 0   0   error (invalid witness file) 0 --- inspect .0015 .0018 .40 0     0   - --- inspect
list-properties/list_true-unreach-call_false-valid-memtrack.i unknown 0 --- inspect 25   11   520 220 .75 0      error (invalid witness file) 0 --- inspect .59 .36 40 0   0   error (2) 0 --- inspect .023 .024 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .69 46 0   0   error (invalid witness file) 0 --- inspect .0015 .0019 .40 0     0   - --- inspect
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i unknown 0 --- inspect 19   6.9 380 170 .75 0      error (invalid witness file) 0 --- inspect .57 .37 40 0   0   error (2) 0 --- inspect .024 .025 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .64 49 0   0   error (invalid witness file) 0 --- inspect .0057 .0072 .54 0     0   - --- inspect
list-properties/simple_true-unreach-call_false-valid-memtrack.i unknown 0 --- inspect 24   9.8 570 230 .75 15      error (invalid witness file) 0 --- inspect .61 .39 40 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .96 .63 47 0   0   error (invalid witness file) 0 --- inspect .0048 .0060 .53 0     0   - --- inspect
list-properties/splice_true-unreach-call_false-valid-memtrack.i unknown 0 --- inspect 19   6.9 380 140 .75 0      error (invalid witness file) 0 --- inspect .59 .35 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .99 .66 48 0   0   error (invalid witness file) 0 --- inspect .0021 .0027 .53 0     0   - --- inspect
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i error (7) 0 --- inspect 28   8.9 570 220 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .020 5.6 0    0  
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i error (7) 0 --- inspect 28   8.4 580 220 .75 .86   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0  
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i error (7) 0 --- inspect 29   9.3 590 220 .75 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .028 5.6 0    0  
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i error (7) 0 --- inspect 29   9.1 560 220 .75 0      error (invalid witness file) 0 --- inspect .58 .36 40 0   0   error (2) 0 --- inspect .020 .028 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .78 48 0   0   error (invalid witness file) 0 --- inspect .0032 .0035 .40 0     0   - --- inspect
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i error (7) 0 --- inspect 29   8.5 560 220 .75 0      error (invalid witness file) 0 --- inspect .65 .41 42 0   0   error (2) 0 --- inspect .019 .020 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .68 47 0   0   error (invalid witness file) 0 --- inspect .0049 .0064 .53 0     0   - --- inspect
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i error (7) 0 --- inspect 29   9.5 620 240 .75 0      error (invalid witness file) 0 --- inspect .64 .39 41 0   0   error (2) 0 --- inspect .022 .023 5.7 0    0   error (invalid witness file) 0 --- inspect 1.0  .66 47 0   0   error (invalid witness file) 0 --- inspect .0055 .0070 .52 0     0   - --- inspect
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i error (7) 0 --- inspect 27   8.4 590 230 .75 0      error (invalid witness file) 0 --- inspect .77 .47 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .98 .63 48 0   0   error (invalid witness file) 0 --- inspect .0019 .0031 .53 0     0   - --- inspect
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i error (7) 0 --- inspect 30   9.3 590 220 .75 0      error (invalid witness file) 0 --- inspect .62 .38 42 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .66 47 0   0   error (invalid witness file) 0 --- inspect .0017 .0021 .54 0     0   - --- inspect
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i error (7) 0 --- inspect 28   9.1 570 210 .75 0      error (invalid witness file) 0 --- inspect .61 .38 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .80 47 0   0   error (invalid witness file) 0 --- inspect .0044 .0058 .53 0     0   - --- inspect
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i error (7) 0 --- inspect 28   8.9 580 230 .75 0      error (invalid witness file) 0 --- inspect .60 .39 40 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .61 47 0   0   error (invalid witness file) 0 --- inspect .0055 .0068 .53 0     0   - --- inspect
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i error (7) 0 --- inspect 29   8.9 590 220 .75 0      error (invalid witness file) 0 --- inspect .69 .44 40 0   0   error (2) 0 --- inspect .023 .024 5.6 0    0   error (invalid witness file) 0 --- inspect .93 .60 47 0   0   error (invalid witness file) 0 --- inspect .0057 .0071 .53 0     0   - --- inspect
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i error (7) 0 --- inspect 29   9.2 590 220 .75 0      error (invalid witness file) 0 --- inspect .62 .38 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .63 48 0   0   error (invalid witness file) 0 --- inspect .0050 .0081 .53 0     0   - --- inspect
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i error (7) 0 --- inspect 28   8.2 570 210 .75 0      error (invalid witness file) 0 --- inspect .66 .43 41 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .98 .63 48 0   0   error (invalid witness file) 0 --- inspect .0051 .0067 .52 0     0   - --- inspect
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   800   1800 11000 .69 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0  
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   840   2100 11000 .70 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .026 5.6 0    0  
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   840   800 11000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .024 5.7 0    0  
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   770   960 11000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   760   790 9900 .64 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 timeout 0 --- inspect 900   820   730 12000 .63 .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   820   920 10000 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .024 5.6 0    0  
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   850   750 10000 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0  
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   830   1300 13000 .64 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 timeout 0 --- inspect 900   820   1600 9300 .70 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .043 .045 5.5 0    0  
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   850   1200 13000 .63 .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   810   1800 9800 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .042 .043 5.5 0    0  
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   800   1000 9900 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .024 5.7 0    0  
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   730   1000 12000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.6 0    0  
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   830   970 13000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0    0  
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   830   1000 10000 .63 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 timeout 0 --- inspect 900   740   950 11000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .055 .058 5.5 0    0  
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   810   920 9900 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.7 0    0  
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   800   2100 10000 .70 .31   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0    0  
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i timeout 0 --- inspect 900   820   800 11000 .64 0      error (invalid witness file) 0 --- inspect .60 .36 40 0   0   error (2) 0 --- inspect .043 .045 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .65 47 0   0   error (invalid witness file) 0 --- inspect .0059 .0076 .53 0     0   - --- inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 35   13   820 310 .66 0      false(valid-deref) 1 wit inspect 5.4  2.9  260 0   0   error (7) 0 --- inspect 22     12     320   .68 0   timeout 0 --- inspect 92    59    3600 0   0   false(valid-deref) 1 --- inspect .67   .67   20    .094 0   - --- inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i timeout 0 --- inspect 900   810   1000 11000 .64 0      error (invalid witness file) 0 --- inspect .72 .45 40 0   0   error (2) 0 --- inspect .030 .031 5.5 0    0   error (invalid witness file) 0 --- inspect 1.1  .70 47 0   0   error (invalid witness file) 0 --- inspect .0051 .0071 .53 0     0   - --- inspect
list-simple/dll2c_append_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   870   1800 12000 .73 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0    0  
list-simple/dll2c_append_unequal_true-unreach-call_true-valid-memsafety.i error (7) 0 --- inspect 900   860   2300 11000 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0  
list-simple/dll2c_insert_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   860   980 14000 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.6 0    0  
list-simple/dll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   860   860 12000 .69 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.8 0    0  
list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   870   1100 11000 .73 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.6 0    0  
list-simple/dll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   860   1700 11000 .73 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
list-simple/dll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   860   1100 12000 .72 55      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
list-simple/dll2c_remove_all_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   860   1000 13000 .73 15      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.7 0    0  
list-simple/dll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 910   160   14000 5300 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
list-simple/dll2c_update_all_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 910   360   14000 7100 .62 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0    0  
list-simple/dll2n_append_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   860   1100 13000 .70 .14   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .029 5.7 0    0  
list-simple/dll2n_append_unequal_true-unreach-call_true-valid-memsafety.i error (7) 0 --- inspect 820   790   2300 10000 .68 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .024 5.6 0    0  
list-simple/dll2n_insert_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   870   900 13000 .69 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   870   960 14000 .69 15      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .032 5.7 0    0  
list-simple/dll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   870   1000 9200 .70 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .024 5.6 0    0  
list-simple/dll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   870   1600 14000 .70 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .022 5.6 0    0  
list-simple/dll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   860   1600 12000 .69 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
list-simple/dll2n_remove_all_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   860   1600 12000 .69 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.7 0    0  
list-simple/dll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 830   780   1200 8900 .68 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     1500   .91 0  
list-simple/dll2n_update_all_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   840   1100 10000 .70 .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.7 0    0  
list-simple/sll2c_append_equal_true-unreach-call_true-valid-memsafety.i error (7) 0 --- inspect 860   830   2200 9900 .71 .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .023 5.6 0    0  
list-simple/sll2c_append_unequal_true-unreach-call_true-valid-memsafety.i error (7) 0 --- inspect 840   810   2300 10000 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
list-simple/sll2c_insert_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   880   790 13000 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
list-simple/sll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   870   810 12000 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .023 5.6 0    0  
list-simple/sll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   870   1300 11000 .73 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
list-simple/sll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   870   1400 12000 .73 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .026 5.6 0    0  
list-simple/sll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   840   730 11000 .73 .23   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.6 0    0  
list-simple/sll2c_remove_all_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   840   730 12000 .73 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0  
list-simple/sll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 910   260   13000 5300 .62 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .023 5.6 0    0  
list-simple/sll2c_update_all_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 910   720   12000 10000 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .028 5.6 0    0  
list-simple/sll2n_append_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   870   1600 11000 .73 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0    0  
list-simple/sll2n_append_unequal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   880   2200 11000 .72 16      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0    0  
list-simple/sll2n_insert_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   870   1100 11000 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0  
list-simple/sll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   870   990 12000 .73 .39   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .044 .045 5.5 0    0  
list-simple/sll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   870   1400 10000 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .025 5.6 0    0  
list-simple/sll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   870   1000 11000 .73 .39   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0  
list-simple/sll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   860   860 14000 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0  
list-simple/sll2n_remove_all_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   870   1200 11000 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.7 0    0  
list-simple/sll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   840   1100 11000 .70 20      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .027 5.6 0    0  
list-simple/sll2n_update_all_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   850   1200 9800 .70 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .024 5.6 0    0  
list-ext3-properties/dll_circular_traversal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   840   1200 11000 .69 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .024 5.6 0    0  
list-ext3-properties/dll_nondet_free_order_true-valid-memsafety.i timeout 0 --- inspect 900   860   2000 6700 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   850   1100 11000 .70 0      - --- 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 timeout 0 --- inspect 900   860   940 11000 .69 15      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .026 5.6 0    0  
list-ext3-properties/sll_length_check_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   860   1900 14000 .69 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .053 .056 5.5 0    0  
list-ext3-properties/sll_nondet_insert_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   820   1200 14000 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.7 0    0  
list-ext3-properties/sll_of_sll_nondet_append_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   870   910 12000 .69 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .029 5.6 0    0  
list-ext3-properties/sll_shallow_copy_true-valid-memsafety.i true 2 wit inspect 71   57   530 880 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 17     11     520   .62 0  
list-ext3-properties/dll_circular_traversal_false-valid-deref.i timeout 0 --- inspect 900   850   2200 10000 .63 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 .98 .66 47 0   0   error (invalid witness file) 0 --- inspect .0017 .0022 .53 0     0   - --- inspect
list-ext3-properties/sll_circular_traversal_false-valid-deref.i timeout 0 --- inspect 900   860   900 10000 .69 0      error (invalid witness file) 0 --- inspect .59 .37 41 0   0   error (2) 0 --- inspect .025 .026 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .76 47 0   0   error (invalid witness file) 0 --- inspect .0014 .0015 .40 0     0   - --- inspect
list-ext3-properties/dll_nondet_free_order_false-valid-memtrack.i unknown 0 --- inspect 410   360   950 5100 .68 0      error (invalid witness file) 0 --- inspect .59 .37 41 0   0   error (2) 0 --- inspect .042 .044 5.5 0    0   error (invalid witness file) 0 --- inspect 1.1  .69 47 0   0   error (invalid witness file) 0 --- inspect .0046 .0064 .53 0     0   - --- inspect
list-ext3-properties/sll_shallow_copy_false-valid-memtrack.i unknown 0 --- inspect 36   21   620 370 .75 0      error (invalid witness file) 0 --- inspect .58 .36 42 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .70 46 0   0   error (invalid witness file) 0 --- inspect .0057 .0071 .52 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 6 72000 65000 160000 880000 72   150   28 2 26 16   1600 0   0   28 0 43 25 780 1.4 0   28 0 120 79 5100 0   0   28 2 1.4 1.5 54 .19 0   75 2 980 920 2400 1.5  0  
    correct results 4 6 940 850 2900 10000 2.7 0   2 2 10 5.4 510 0   0   0 0 2 2 1.3 1.3 41 .19 0   1 2 17 11 520 .62 0  
        correct true 2 4 900 830 1700 9800 1.4 0   0 0 0 0 1 2 17 11 520 .62 0  
        correct false 2 2 44 17 1200 380 1.3 0   2 2 10 5.4 510 0   0   0 0 2 2 1.3 1.3 41 .19 0   0
    incorrect results 0 0 0 0 0 0
        incorrect true 0 0 0 0 0 0
        incorrect false 0 0 0 0 0 0
score (103 tasks, max score: 178) 6 2 0 0 2 2
Run set utaipan.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-utaipan.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-utaipan.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-witness2test-validate-violation-witnesses-utaipan.sv-comp19_prop-memsafety.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-utaipan.sv-comp19_prop-memsafety.MemSafety-LinkedLists