Tool ULTIMATE Kojak 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 11:04:44 CET 2018-12-09 20:15:59 CET 2018-12-09 20:59:07 CET 2018-12-09 21:01:30 CET 2018-12-12 21:11:08 CET 2018-12-09 20:36:45 CET
Run set ukojak.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-ukojak.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-ukojak.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-witness2test-validate-violation-witnesses-ukojak.sv-comp19_prop-memsafety.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-ukojak.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/ukojak.2018-12-08_1104.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/ukojak.2018-12-08_1104.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/ukojak.2018-12-08_1104.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/ukojak.2018-12-08_1104.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/ukojak.2018-12-08_1104.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 790   1000 8200 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .026 5.7 0    0  
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 730   880 10000 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0    0  
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 790   1100 9800 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .029 5.5 0    0  
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 790   1000 7600 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0    0  
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 410 350   860 4000 .62 0      false(valid-deref) 1 wit inspect 5.8  3.1  280 0   0     error (7) 0 --- inspect 17     10     310   .68 0     unknown 0 --- inspect 4.6  2.7  250 0   0     true -32 --- inspect .69   .70   21    .094 0   - --- inspect
heap-manipulation/tree_false-valid-deref.i false(valid-deref) 1 wit inspect 10 3.3 380 74 .66 0      false(valid-deref) 1 wit inspect 4.6  2.5  250 0   0     error (7) 0 --- inspect 18     9.9   320   .68 0     unknown 0 --- inspect 4.5  2.7  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 790   1100 7300 .64 .025  error (invalid witness file) 0 --- inspect .73 .45 41 0   0     error (2) 0 --- inspect .021 .023 5.6 0    0     error (invalid witness file) 0 --- inspect .92 .59 47 0   0     error (invalid witness file) 0 --- inspect .0021 .0027 .52 0     0   - --- inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i error (7) 0 --- inspect 94 64   1100 1000 .71 0      error (invalid witness file) 0 --- inspect .70 .43 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0     error (invalid witness file) 0 --- inspect .97 .64 48 0   0     error (invalid witness file) 0 --- inspect .0061 .0077 .54 0     0   - --- inspect
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i error (7) 0 --- inspect 550 470   810 4500 .71 0      error (invalid witness file) 0 --- inspect .79 .49 42 0   0     error (2) 0 --- inspect .020 .021 5.6 0    0     error (invalid witness file) 0 --- inspect 1.0  .66 49 0   0     error (invalid witness file) 0 --- inspect .0050 .0065 .54 0     0   - --- inspect
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i error (7) 0 --- inspect 340 280   880 3300 .71 0      error (invalid witness file) 0 --- inspect .77 .46 41 0   0     error (2) 0 --- inspect .022 .022 5.6 0    0     error (invalid witness file) 0 --- inspect .96 .62 48 0   0     error (invalid witness file) 0 --- inspect .0017 .0022 .53 0     0   - --- inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 780   1100 7900 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .020 5.6 0    0  
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i unknown 0 --- inspect 29 13   590 240 .75 0      error (invalid witness file) 0 --- inspect .66 .42 40 0   0     error (2) 0 --- inspect .021 .023 5.6 0    0     error (invalid witness file) 0 --- inspect .91 .59 47 0   0     error (invalid witness file) 0 --- inspect .0058 .0075 .53 0     0   - --- inspect
list-properties/list_true-unreach-call_false-valid-memtrack.i unknown 0 --- inspect 44 24   700 390 .75 0      error (invalid witness file) 0 --- inspect .75 .46 41 0   0     error (2) 0 --- inspect .022 .023 5.6 0    0     error (invalid witness file) 0 --- inspect .97 .65 47 0   .094 error (invalid witness file) 0 --- inspect .0051 .0069 .53 0     0   - --- inspect
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i unknown 0 --- inspect 24 9.9 590 230 .75 0      error (invalid witness file) 0 --- inspect .64 .40 40 0   0     error (2) 0 --- inspect .024 .025 5.5 0    0     error (invalid witness file) 0 --- inspect .97 .64 48 0   0     error (invalid witness file) 0 --- inspect .0051 .0069 .41 0     0   - --- inspect
list-properties/simple_true-unreach-call_false-valid-memtrack.i unknown 0 --- inspect 36 18   680 350 .75 0      error (invalid witness file) 0 --- inspect .78 .48 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0     error (invalid witness file) 0 --- inspect .96 .63 47 0   0     error (invalid witness file) 0 --- inspect .0028 .0036 .53 0     0   - --- inspect
list-properties/splice_true-unreach-call_false-valid-memtrack.i unknown 0 --- inspect 25 10   520 190 .75 0      error (invalid witness file) 0 --- inspect .76 .46 40 0   0     error (2) 0 --- inspect .023 .024 5.6 0    0     error (invalid witness file) 0 --- inspect .91 .61 46 0   0     error (invalid witness file) 0 --- inspect .0054 .0066 .53 0     0   - --- inspect
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 780   2100 9400 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .030 5.6 0    0  
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 790   1700 8400 .63 .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .031 .032 5.6 0    0  
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 790   1800 8400 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .026 5.8 0    0  
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i timeout 0 --- inspect 900 790   1900 8300 .64 0      error (invalid witness file) 0 --- inspect .80 .49 41 0   0     error (2) 0 --- inspect .019 .020 5.6 0    0     error (invalid witness file) 0 --- inspect .96 .63 47 0   0     error (invalid witness file) 0 --- inspect .0049 .0089 .53 0     0   - --- inspect
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i timeout 0 --- inspect 900 790   1900 7700 .64 0      error (invalid witness file) 0 --- inspect .71 .43 40 0   0     error (2) 0 --- inspect .031 .032 5.6 0    0     error (invalid witness file) 0 --- inspect .94 .62 47 0   0     error (invalid witness file) 0 --- inspect .0066 .010  .53 0     0   - --- inspect
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i timeout 0 --- inspect 900 800   1800 8900 .64 0      error (invalid witness file) 0 --- inspect .78 .46 41 0   0     error (2) 0 --- inspect .021 .022 5.7 0    0     error (invalid witness file) 0 --- inspect 1.0  .67 49 0   0     error (invalid witness file) 0 --- inspect .0044 .0060 .54 0     0   - --- inspect
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i timeout 0 --- inspect 900 790   1800 7600 .64 0      error (invalid witness file) 0 --- inspect .66 .41 41 0   0     error (2) 0 --- inspect .022 .023 5.6 0    0     error (invalid witness file) 0 --- inspect .96 .62 47 0   0     error (invalid witness file) 0 --- inspect .0015 .0021 .53 0     0   - --- inspect
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i timeout 0 --- inspect 900 790   1900 9100 .64 0      error (invalid witness file) 0 --- inspect .61 .38 41 0   0     error (2) 0 --- inspect .023 .024 5.6 0    0     error (invalid witness file) 0 --- inspect .94 .62 47 0   0     error (invalid witness file) 0 --- inspect .0044 .0057 .53 0     0   - --- inspect
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i timeout 0 --- inspect 900 790   1700 8000 .64 0      error (invalid witness file) 0 --- inspect .57 .35 40 0   0     error (2) 0 --- inspect .024 .024 5.6 0    0     error (invalid witness file) 0 --- inspect .96 .63 47 0   0     error (invalid witness file) 0 --- inspect .0018 .0023 .41 0     0   - --- inspect
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i timeout 0 --- inspect 900 790   1800 8400 .65 0      error (invalid witness file) 0 --- inspect .68 .41 40 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0     error (invalid witness file) 0 --- inspect .95 .62 48 0   0     error (invalid witness file) 0 --- inspect .0050 .0062 .53 0     0   - --- inspect
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i timeout 0 --- inspect 900 790   1700 9700 .64 0      error (invalid witness file) 0 --- inspect .77 .46 41 0   0     error (2) 0 --- inspect .020 .021 5.6 0    0     error (invalid witness file) 0 --- inspect .97 .64 47 0   0     error (invalid witness file) 0 --- inspect .0029 .0036 .53 0     0   - --- inspect
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i timeout 0 --- inspect 900 780   2000 8400 .64 .086  error (invalid witness file) 0 --- inspect .73 .46 40 0   0     error (2) 0 --- inspect .021 .022 5.7 0    0     error (invalid witness file) 0 --- inspect 1.0  .65 48 0   0     error (invalid witness file) 0 --- inspect .0049 .0069 .52 0     0   - --- inspect
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i timeout 0 --- inspect 900 780   1800 6500 .64 0      error (invalid witness file) 0 --- inspect .63 .40 40 0   0     error (2) 0 --- inspect .028 .029 5.8 0    0     error (invalid witness file) 0 --- inspect .95 .61 46 0   0     error (invalid witness file) 0 --- inspect .0035 .0045 .52 0     0   - --- inspect
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 780   1000 9100 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .030 .031 5.6 0    0  
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 790   940 7600 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .024 5.6 0    0  
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 780   1000 9000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .030 5.6 0    0  
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 780   1000 8900 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0    0  
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 780   960 6400 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.6 0    0  
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 780   1000 7000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 790   940 6700 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .029 5.6 0    0  
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 790   950 6700 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 790   1000 7400 .64 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 timeout 0 --- inspect 900 780   1000 7600 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 800   1000 8000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .020 5.6 0    0  
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 790   990 8100 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0    0  
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 780   1000 8700 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.6 0    0  
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 780   1000 6500 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 780   1200 11000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.5 0    0  
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 790   1000 7600 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .027 5.6 0    0  
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 780   980 6800 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.7 0    0  
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 770   1100 7900 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.6 0    0  
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 790   1000 5400 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .025 5.6 0    0  
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 490 430   990 4200 .62 0      false(valid-deref) 1 wit inspect 5.6  3.0  250 0   0     error (7) 0 --- inspect 16     9.5   320   .68 0     unknown 0 --- inspect 4.6  2.7  250 0   0     true -32 --- inspect .66   .67   21    .078 0   - --- inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 470 400   940 3800 .62 0      false(valid-deref) 1 wit inspect 5.4  2.9  250 0   0     error (7) 0 --- inspect 18     9.9   320   .68 .033 timeout 0 --- inspect 97    60    3700 0   .029 false(valid-deref) 1 --- inspect .67   .67   20    .094 0   - --- inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 410 350   790 4000 .62 0      false(valid-deref) 1 wit inspect 4.9  2.7  260 0   .025 error (7) 0 --- inspect 17     9.6   310   .68 .025 unknown 0 --- inspect 4.7  2.7  260 0   0     true -32 --- inspect .65   .65   20    .086 0   - --- inspect
list-simple/dll2c_append_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 790   1000 8600 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0    0  
list-simple/dll2c_append_unequal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 790   1000 8300 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.5 0    0  
list-simple/dll2c_insert_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 790   900 7900 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .024 5.6 0    0  
list-simple/dll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 790   1100 7400 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .035 .036 5.6 0    0  
list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 800   1100 7700 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0    0  
list-simple/dll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 790   920 7400 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.7 0    0  
list-simple/dll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 790   950 8600 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .029 5.7 0    0  
list-simple/dll2c_remove_all_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 790   970 10000 .65 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .027 5.6 0    0  
list-simple/dll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 780   1100 6700 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.7 0    0  
list-simple/dll2c_update_all_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 780   1100 7000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .020 5.6 0    0  
list-simple/dll2n_append_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 790   1000 7800 .64 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 timeout 0 --- inspect 900 790   1000 8000 .63 .025  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .029 5.6 0    0  
list-simple/dll2n_insert_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 790   950 9000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.7 0    0  
list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 790   950 7500 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
list-simple/dll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 790   1000 7900 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
list-simple/dll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 790   1000 8200 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0    0  
list-simple/dll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 790   1000 7100 .64 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 790   1000 8200 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
list-simple/dll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 400 340   1100 4000 .62 0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     900     1600   .63 0  
list-simple/dll2n_update_all_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 780   1000 6800 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .023 5.6 0    0  
list-simple/sll2c_append_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 800   980 7200 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0    0  
list-simple/sll2c_append_unequal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 790   950 8500 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
list-simple/sll2c_insert_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 790   920 8300 .64 0      - --- 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 timeout 0 --- inspect 900 790   880 8000 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
list-simple/sll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 800   1000 10000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .024 5.7 0    0  
list-simple/sll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 800   980 8300 .64 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 790   960 7900 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0    0  
list-simple/sll2c_remove_all_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 800   1000 8800 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .025 5.6 0    0  
list-simple/sll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i error (7) 0 --- inspect 850 730   1000 7100 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0    0  
list-simple/sll2c_update_all_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 780   930 6700 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .029 5.7 0    0  
list-simple/sll2n_append_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 800   1000 7800 .64 .029  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
list-simple/sll2n_append_unequal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 800   1000 9600 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0    0  
list-simple/sll2n_insert_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 790   910 7400 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .029 5.6 0    0  
list-simple/sll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 800   830 8000 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .023 5.6 0    0  
list-simple/sll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 790   910 9400 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0  
list-simple/sll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 800   1000 7900 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.7 0    0  
list-simple/sll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 790   910 8200 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .028 5.6 0    0  
list-simple/sll2n_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 250 210   1000 2600 .62 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 380     360     870   .62 0  
list-simple/sll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 780   940 6800 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .028 5.7 0    0  
list-simple/sll2n_update_all_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 780   990 8700 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
list-ext3-properties/dll_circular_traversal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 790   1100 8700 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
list-ext3-properties/dll_nondet_free_order_true-valid-memsafety.i error (7) 0 --- inspect 390 330   1000 4500 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .025 5.6 0    0  
list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 790   1200 6900 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.6 0    0  
list-ext3-properties/sll_circular_traversal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 800   990 7900 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0  
list-ext3-properties/sll_length_check_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 790   890 7700 .63 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0  
list-ext3-properties/sll_nondet_insert_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 780   970 9200 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .029 5.6 0    0  
list-ext3-properties/sll_of_sll_nondet_append_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900 790   1000 7200 .64 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
list-ext3-properties/sll_shallow_copy_true-valid-memsafety.i true 2 wit inspect 50 39   720 550 .62 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 19     12     500   .62 0  
list-ext3-properties/dll_circular_traversal_false-valid-deref.i timeout 0 --- inspect 900 790   1100 8700 .63 0      error (invalid witness file) 0 --- inspect .67 .41 41 0   0     error (2) 0 --- inspect .021 .023 5.6 0    0     error (invalid witness file) 0 --- inspect .97 .62 48 0   0     error (invalid witness file) 0 --- inspect .0056 .0069 .40 0     0   - --- inspect
list-ext3-properties/sll_circular_traversal_false-valid-deref.i timeout 0 --- inspect 900 800   1100 8900 .63 0      error (invalid witness file) 0 --- inspect .74 .45 40 0   0     error (2) 0 --- inspect .021 .022 5.7 0    0     error (invalid witness file) 0 --- inspect .94 .61 47 0   0     error (invalid witness file) 0 --- inspect .0046 .0052 .39 0     0   - --- inspect
list-ext3-properties/dll_nondet_free_order_false-valid-memtrack.i error (7) 0 --- inspect 180 140   1000 1500 .71 0      error (invalid witness file) 0 --- inspect .81 .50 41 0   0     error (2) 0 --- inspect .021 .022 5.7 0    0     error (invalid witness file) 0 --- inspect .96 .63 48 0   0     error (invalid witness file) 0 --- inspect .0056 .0069 .52 0     0   - --- inspect
list-ext3-properties/sll_shallow_copy_false-valid-memtrack.i error (7) 0 --- inspect 19 7.6 500 170 .75 0      error (invalid witness file) 0 --- inspect .68 .42 41 0   0     error (2) 0 --- inspect .020 .020 5.6 0    0     error (invalid witness file) 0 --- inspect .98 .62 47 0   0     error (invalid witness file) 0 --- inspect .0013 .0014 .40 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 11 80000 70000 110000 720000 67   .17 28 5 43 24 2200 0   .025 28 0 86 49 1700 3.4 .057 28 0 140 86 5800 0   .12 28 -94 3.4 3.5 110 .45 0   75 4 1400 1300 3400 1.9 0  
    correct results 8 11 2500 2100 6800 23000 5.0 0    5 5 26 14 1300 0   .025 0 0 2 2 1.3 1.3 41 .19 0   2 4 400 370 1400 1.2 0  
        correct true 3 6 700 590 2800 7200 1.9 0    0 0 0 0 2 4 400 370 1400 1.2 0  
        correct false 5 5 1800 1500 4000 16000 3.1 0    5 5 26 14 1300 0   .025 0 0 2 2 1.3 1.3 41 .19 0   0
    incorrect results 0 0 0 0 3 -96 2.0 2.0 62 .26 0   0
        incorrect true 0 0 0 0 3 -96 2.0 2.0 62 .26 0   0
        incorrect false 0 0 0 0 0 0
score (103 tasks, max score: 178) 11 5 0 0 -94 4
Run set ukojak.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-ukojak.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-ukojak.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-witness2test-validate-violation-witnesses-ukojak.sv-comp19_prop-memsafety.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-ukojak.sv-comp19_prop-memsafety.MemSafety-LinkedLists