Tool DepthK 3.1 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* [apollon001; apollon005; apollon039; apollon053; apollon087; apollon091] [apollon007; apollon009; apollon073; apollon078] 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-05 09:36:33 CET 2018-12-06 10:02:56 CET 2018-12-06 11:08:44 CET 2018-12-06 11:42:46 CET 2018-12-12 19:35:41 CET 2018-12-06 10:24:56 CET
Run set depthk.sv-comp19_prop-memsafety.MemSafety-Arrays cpa-seq-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-Arrays uautomizer-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-Arrays cpa-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-Arrays fshell-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-Arrays uautomizer-validate-correctness-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-Arrays
Options -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/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/depthk.2018-12-05_0936.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/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/depthk.2018-12-05_0936.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/depthk.2018-12-05_0936.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)
array-memsafety/add_last_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .22 .22 34 2.2 1.0  0      false(valid-deref) 1 wit inspect 4.5  2.5  260 0   0   false(valid-deref) 1 --- inspect 9.3   5.6   320   .62 0   unknown 0 --- inspect 4.5  2.6  260 0   .13 true -32 --- inspect .64   .64   20    .074 0    - --- inspect
array-memsafety/bubblesort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .14 .14 33 1.7 1.0  0      true -32 wit inspect 4.1  2.3  250 0   0   false(valid-deref) 1 --- inspect 7.7   4.4   310   .62 0   unknown 0 --- inspect 3.6  2.1  250 0   0    true -32 --- inspect .60   .63   20    .061 0    - --- inspect
array-memsafety/count_down_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .22 .22 34 2.2 1.0  0      false(valid-deref) 1 wit inspect 5.2  2.8  250 0   0   false(valid-deref) 1 --- inspect 9.1   5.1   320   .62 0   unknown 0 --- inspect 4.3  2.6  250 0   0    false(valid-deref) 1 --- inspect .66   .66   20    .074 0    - --- inspect
array-memsafety/cstrcat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .14 .14 33 1.7 1.0  0      false(valid-deref) 1 wit inspect 3.5  2.0  240 0   0   false(valid-deref) 1 --- inspect 7.9   4.9   310   .66 0   false(valid-deref) 1 --- inspect 3.7  2.2  250 0   0    false(valid-deref) 1 --- inspect .59   .59   20    .049 0    - --- inspect
array-memsafety/cstrchr_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .20 .19 34 2.3 1.0  0      false(valid-deref) 1 wit inspect 4.6  2.5  260 0   0   true -32 --- inspect 13     8.3   510   .62 0   unknown 0 --- inspect 4.6  2.7  260 0   0    false(valid-deref) 1 --- inspect .66   .65   20    .078 0    - --- inspect
array-memsafety/cstrlen_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .55 .54 36 6.6 31    0      false(valid-deref) 1 wit inspect 4.4  2.4  250 0   0   false(valid-deref) 1 --- inspect 11     6.1   340   .62 0   unknown 0 --- inspect 4.4  2.5  260 0   .18 false(valid-deref) 1 --- inspect .65   .65   20    .078 0    - --- inspect
array-memsafety/cstrncat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .15 .15 33 1.6 .85 0      false(valid-deref) 1 wit inspect 3.9  2.1  240 0   0   false(valid-deref) 1 --- inspect 8.0   4.5   320   .62 0   false(valid-deref) 1 --- inspect 3.8  2.2  250 0   0    false(valid-deref) 1 --- inspect .59   .59   20    .061 0    - --- inspect
array-memsafety/cstrncpy_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .14 .14 33 1.6 1.0  0      true -32 wit inspect 3.7  2.1  250 0   0   false(valid-deref) 1 --- inspect 7.5   4.3   320   .66 0   unknown 0 --- inspect 3.6  2.1  250 0   0    error (2) 0 --- inspect .60   .60   20    .061 0    - --- inspect
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .22 .22 34 2.6 1.0  0      false(valid-deref) 1 wit inspect 4.5  2.5  250 0   0   false(valid-deref) 1 --- inspect 23     17     480   .62 0   unknown 0 --- inspect 4.5  2.6  250 0   0    false(valid-deref) 1 --- inspect .65   .65   20    .078 0    - --- inspect
array-memsafety/diff_usafe_false-valid-deref.i false(valid-deref) 1 wit inspect .14 .14 33 1.6 1.0  0      timeout 0 wit inspect 96    78    2100 0   0   false(valid-deref) 1 --- inspect 7.0   4.4   310   .62 0   timeout (exception) 0 --- inspect 92    76    2600 0   0    false(valid-deref) 1 --- inspect .64   .64   20    .066 0    - --- inspect
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .28 .27 34 3.9 1.0  0      false(valid-deref) 1 wit inspect 4.5  2.4  260 0   0   false(valid-deref) 1 --- inspect 12     7.0   460   .62 0   unknown 0 --- inspect 4.4  2.5  250 0   0    true -32 --- inspect .65   .65   20    .082 0    - --- inspect
array-memsafety/lis_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .22 .22 34 2.6 1.0  0      false(valid-deref) 1 wit inspect 4.3  2.3  250 0   0   false(valid-deref) 1 --- inspect 14     8.3   450   .62 0   unknown 0 --- inspect 4.3  2.5  250 0   0    false(valid-deref) 1 --- inspect .65   .65   20    .078 0    - --- inspect
array-memsafety/mult_array_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .40 .40 38 4.9 1.0  0      false(valid-deref) 1 wit inspect 4.6  2.5  250 0   0   false(valid-deref) 1 --- inspect 8.8   5.0   320   .62 0   unknown 0 --- inspect 4.6  2.7  250 0   0    false(valid-deref) 1 --- inspect .66   .66   20    .078 0    - --- inspect
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .64 .63 36 8.0 26    0      true -32 wit inspect 4.4  2.4  250 0   0   false(valid-deref) 1 --- inspect 9.5   5.7   320   .62 0   unknown 0 --- inspect 4.2  2.4  250 0   0    false(valid-deref) 1 --- inspect .67   .67   20    .078 .30 - --- inspect
array-memsafety/reverse_array_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .20 .20 34 2.3 .85 0      false(valid-deref) 1 wit inspect 4.4  2.4  250 0   0   false(valid-deref) 1 --- inspect 12     6.9   360   .62 0   unknown 0 --- inspect 4.6  2.6  250 0   .25 true -32 --- inspect .67   .67   20    .078 0    - --- inspect
array-memsafety/selectionsort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .14 .14 33 2.0 1.0  0      timeout 0 wit inspect 95    78    2100 0   0   false(valid-deref) 1 --- inspect 7.8   4.8   310   .62 0   timeout 0 --- inspect 93    83    2300 0   0    false(valid-deref) 1 --- inspect .60   .61   20    .066 1.3  - --- inspect
array-memsafety/stroeder1_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .14 .14 34 1.9 1.0  0      false(valid-deref) 1 wit inspect 3.6  2.1  240 0   0   false(valid-deref) 1 --- inspect 7.7   4.5   310   .62 0   false(valid-deref) 1 --- inspect 4.9  2.8  250 0   0    false(valid-deref) 1 --- inspect .63   .63   20    .061 0    - --- inspect
array-memsafety/add_last-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 900    900    190 12000   2600    .012  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .019 .021 5.6 0    0  
array-memsafety/array01-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 900    900    260 12000   930    .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.7 0    0  
array-memsafety/array02-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 900    900    240 13000   650    .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.6 0    0  
array-memsafety/array03-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 900    900    770 11000   780    .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
array-memsafety/bubblesort-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 900    900    1100 9800   280    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0    0  
array-memsafety/count_down-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 900    900    220 13000   700    .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
array-memsafety/cstrcat-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 300    290    70 4200   2800    .012  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.6 0    0  
array-memsafety/cstrchr-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 130    130    42 1700   3000    .029  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
array-memsafety/cstrcmp-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 230    230    75 3300   3000    .025  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0  
array-memsafety/cstrcpy-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 150    150    46 2300   3000    .016  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
array-memsafety/cstrcspn-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 900    900    190 12000   1400    .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .023 5.6 0    0  
array-memsafety/cstrlen-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 66    66    42 840   3000    .041  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
array-memsafety/cstrncat-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 390    390    62 5200   3000    .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .022 5.7 0    0  
array-memsafety/cstrncmp-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 300    300    67 4600   3000    .016  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.6 0    0  
array-memsafety/cstrncpy-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 900    900    310 11000   2100    .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.6 0    0  
array-memsafety/cstrpbrk-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 900    900    180 12000   1300    .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .031 .038 5.6 0    0  
array-memsafety/cstrspn-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 900    900    180 11000   1300    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .026 5.6 0    0  
array-memsafety/diff-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 900    900    200 12000   470    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0    0  
array-memsafety/insertionsort-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 900    900    270 13000   740    .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.6 0    0  
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 890    900    790 9500   230    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
array-memsafety/lis-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 900    900    640 12000   320    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.7 0    0  
array-memsafety/mult_array-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 370    370    85 4900   3000    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 60    60    40 780   3000    .053  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 77    77    42 1100   3000    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 130    130    48 1800   3000    .025  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 58    58    40 690   3000    .057  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 150    150    46 1800   3000    .016  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0  
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 900    900    310 10000   2300    .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0    0  
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 300    300    75 3600   3000    .012  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 240    240    81 2900   2700    .025  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .023 5.5 0    0  
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 150    150    46 2000   2900    .025  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0  
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 900    900    230 11000   1400    .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 900    900    110 12000   3000    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0  
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 66    65    40 850   3000    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 370    370    65 4700   3000    .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 260    260    75 4000   3000    .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .040 .041 5.6 0    0  
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 900    900    310 10000   2200    .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 71    71    41 890   2800    .041  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 900    900    190 9700   1200    .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.6 0    0  
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 900    900    160 10000   430    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 900    900    240 11000   520    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
array-memsafety/rec_strlen-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect .59 .58 36 8.8 26    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 15     8.9   520   .66 0  
array-memsafety/selectionsort-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 900    900    220 12000   470    0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0    0  
array-memsafety/stroeder1-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 78    77    52 940   3000    .033  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.6 0    0  
array-memsafety/stroeder2-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 900    900    160 11000   1300    .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .026 5.6 0    0  
array-memsafety/strreplace-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 900    900    230 12000   460    .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.7 0    0  
array-memsafety/subseq-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 690    690    110 9000   3000    .012  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
array-memsafety/substring-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 900    900    220 10000   1200    .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0    0  
array-examples/relax_false-valid-deref.i false(valid-deref) 1 wit inspect .23 .23 35 2.6 1.0  0      false(valid-deref) 1 wit inspect 4.7  2.5  250 0   0   false(valid-deref) 1 --- inspect 10     5.7   330   .66 0   unknown 0 --- inspect 4.5  2.6  250 0   0    false(valid-deref) 1 --- inspect .67   .67   20    .090 0    - --- inspect
array-examples/sanfoundry_24_false-valid-deref.i unknown 0 --- inspect 90    90    71 1100   2900    .025  error (invalid witness file) 0 --- inspect .59 .36 41 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 .0019 .0025 .53 0     0    - --- inspect
array-examples/standard_strcpy_false-valid-deref_ground.i unknown 0 --- inspect 66    66    55 800   3000    .041  error (invalid witness file) 0 --- inspect .60 .37 41 0   0   error (2) 0 --- inspect .021 .023 5.7 0    0   error (invalid witness file) 0 --- inspect .94 .63 46 0   0    error (invalid witness file) 0 --- inspect .0021 .0026 .52 0     0    - --- inspect
array-examples/standard_strcpy_original_false-valid-deref.i unknown 0 --- inspect 53    53    54 670   3000    .053  error (invalid witness file) 0 --- inspect .77 .48 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .61 49 0   0    error (invalid witness file) 0 --- inspect .0021 .0027 .53 0     0    - --- inspect
array-memsafety-realloc/array-realloc_false-valid-free.i unknown 0 --- inspect 14    14    49 210   1000    .016  error (invalid witness file) 0 --- inspect .72 .44 41 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .91 .60 47 0   0    error (invalid witness file) 0 --- inspect .0048 .0060 .53 0     0    - --- inspect
array-memsafety-realloc/array-realloc_true-valid-memsafety.i unknown 0 --- inspect 37    36    74 530   1000    .012  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
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 71 20 27000    27000    10000 350000   110000 .69 22 -83 260 200   8300 0   0   22 -15 190 110   6400 11    0   22 3 260 200   9100 0   .57 22 -115 11   12   370 1.3  1.6 49 2 16 10   790 .66 0  
    correct results 19 20 5.0  4.9  650 61   100 0    13 13 57 31   3200 0   0   17 17 170 100   5900 11    0   3 3 12 7.2 740 0   0    13 13 8.3 8.3 260 .93 1.6 1 2 15 8.9 520 .66 0  
        correct true 1 2 .59 .58 36 8.8 26 0    0 0 0 0 1 2 15 8.9 520 .66 0  
        correct false 18 18 4.4  4.3  620 52   73 0    13 13 57 31   3200 0   0   17 17 170 100   5900 11    0   3 3 12 7.2 740 0   0    13 13 8.3 8.3 260 .93 1.6 0
    incorrect results 0 3 -96 12 6.8 740 0   0   1 -32 13 8.3 510 .62 0   0 4 -128 2.6 2.6 81 .29 0   0
        incorrect true 0 3 -96 12 6.8 740 0   0   1 -32 13 8.3 510 .62 0   0 4 -128 2.6 2.6 81 .29 0   0
        incorrect false 0 0 0 0 0 0
score (71 tasks, max score: 120) 20 -83 -15 3 -115 2
Run set depthk.sv-comp19_prop-memsafety.MemSafety-Arrays cpa-seq-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-Arrays uautomizer-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-Arrays cpa-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-Arrays fshell-witness2test-validate-violation-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-Arrays uautomizer-validate-correctness-witnesses-depthk.sv-comp19_prop-memsafety.MemSafety-Arrays