Tool PredatorHP 3.14 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 apollon138 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-07 04:08:42 CET 2018-12-07 09:10:21 CET 2018-12-07 10:32:34 CET 2018-12-07 10:52:42 CET 2018-12-12 20:53:36 CET 2018-12-07 09:31:44 CET
Run set predatorhp.sv-comp19_prop-memsafety.MemSafety-Arrays cpa-seq-validate-violation-witnesses-predatorhp.sv-comp19_prop-memsafety.MemSafety-Arrays uautomizer-validate-violation-witnesses-predatorhp.sv-comp19_prop-memsafety.MemSafety-Arrays cpa-witness2test-validate-violation-witnesses-predatorhp.sv-comp19_prop-memsafety.MemSafety-Arrays fshell-witness2test-validate-violation-witnesses-predatorhp.sv-comp19_prop-memsafety.MemSafety-Arrays uautomizer-validate-correctness-witnesses-predatorhp.sv-comp19_prop-memsafety.MemSafety-Arrays
Options --witness error-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/predatorhp.2018-12-07_0408.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/predatorhp.2018-12-07_0408.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/predatorhp.2018-12-07_0408.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/predatorhp.2018-12-07_0408.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/predatorhp.2018-12-07_0408.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 .17 .31 36 1.1 .025  .45  error 0 wit inspect 4.1  2.2  250 0   0   false(valid-deref) 1 --- inspect 9.9   5.9   320   .62 0   error 0 --- inspect 4.1  2.3  250 0   0   true -32 --- inspect .69   .70   20    .074 0      - --- inspect
array-memsafety/bubblesort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .15 .29 34 1.5 .049  .39  timeout 0 wit inspect 93    76    2300 0   0   false(valid-deref) 1 --- inspect 7.9   4.5   310   .62 0   timeout 0 --- inspect 92    75    2700 0   0   true -32 --- inspect .60   .59   20    .066 0      - --- inspect
array-memsafety/count_down_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .16 .29 35 1.6 .049  0     error 0 wit inspect 4.5  2.5  250 0   0   false(valid-deref) 1 --- inspect 8.5   5.2   310   .62 0   error 0 --- inspect 4.0  2.3  250 0   0   false(valid-deref) 1 --- inspect .65   .65   20    .074 0      - --- inspect
array-memsafety/cstrcat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .15 .29 33 2.0 .049  0     false(valid-deref) 1 wit inspect 3.5  2.0  240 0   0   false(valid-deref) 1 --- inspect 7.6   4.4   300   .62 0   false(valid-deref) 1 --- inspect 3.7  2.2  250 0   0   false(valid-deref) 1 --- inspect .60   .60   20    .049 .0041 - --- inspect
array-memsafety/cstrchr_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .27 .30 48 1.7 .057  18     error 0 wit inspect 4.5  2.4  270 0   0   false(valid-deref) 1 --- inspect 11     6.7   370   .62 0   error 0 --- inspect 4.1  2.4  250 0   0   false(valid-deref) 1 --- inspect .65   .65   20    .078 0      - --- inspect
array-memsafety/cstrlen_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .14 .28 36 1.4 .057  .39  error 0 wit inspect 4.2  2.3  250 0   0   false(valid-deref) 1 --- inspect 10     6.4   340   .62 0   error 0 --- inspect 4.3  2.4  250 0   0   true -32 --- inspect .67   .68   20    .078 0      - --- inspect
array-memsafety/cstrncat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .26 .29 48 1.5 .049  19     false(valid-deref) 1 wit inspect 3.4  1.9  240 0   0   false(valid-deref) 1 --- inspect 8.2   5.0   310   .62 0   unknown 0 --- inspect 3.8  2.3  250 0   0   true -32 --- inspect .62   .63   20    .061 0      - --- inspect
array-memsafety/cstrncpy_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .16 .29 33 1.4 .049  0     false(valid-deref) 1 wit inspect 3.5  2.0  250 0   0   false(valid-deref) 1 --- inspect 7.1   4.1   310   .62 0   unknown 0 --- inspect 4.6  2.7  250 0   0   true -32 --- inspect .60   .60   20    .061 0      - --- inspect
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .27 .29 49 2.0 .057  18     error 0 wit inspect 4.3  2.4  250 0   0   false(valid-deref) 1 --- inspect 8.7   5.3   310   .62 0   error 0 --- inspect 4.1  2.3  250 0   0   false(valid-deref) 1 --- inspect .68   .68   20    .078 .025  - --- inspect
array-memsafety/diff_usafe_false-valid-deref.i false(valid-deref) 1 wit inspect .17 .29 36 1.4 .074  .46  timeout (exception) 0 wit inspect 95    77    2200 0   0   false(valid-deref) 1 --- inspect 7.2   4.6   310   .62 0   timeout (exception) 0 --- inspect 92    77    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 .23 .29 49 1.9 .049  19     error 0 wit inspect 4.0  2.3  250 0   0   false(valid-deref) 1 --- inspect 13     7.6   460   .62 0   error 0 --- inspect 4.2  2.3  250 0   0   false(valid-deref) 1 --- inspect .68   .68   20    .082 0      - --- inspect
array-memsafety/lis_unsafe_false-valid-deref.i unknown 0 --- inspect .15 .30 36 1.3 0      0     error (invalid witness file) 0 --- inspect .59 .37 40 0   0   error (2) 0 --- inspect .021 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .60 47 0   0   error (invalid witness file) 0 --- inspect .0059 .0077 .53 0     0      - --- inspect
array-memsafety/mult_array_unsafe_false-valid-deref.i out of memory (unknown) 0 --- inspect 19    9.4  15000 200   .41   .44  error (invalid witness file) 0 --- inspect .57 .35 41 0   0   error (2) 0 --- inspect .023 .024 5.7 0    0   error (invalid witness file) 0 --- inspect .99 .63 48 0   0   error (invalid witness file) 0 --- inspect .0019 .0024 .52 0     0      - --- inspect
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i false(valid-deref) 0 wit inspect .16 .31 36 2.7 .049  0     error 0 wit inspect 4.1  2.3  250 0   0   true -32 --- inspect 16     9.4   460   .62 0   error 0 --- inspect 3.9  2.2  250 0   0   true -32 --- inspect .65   .65   20    .078 0      - --- inspect
array-memsafety/reverse_array_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .15 .29 34 1.5 .025  0     error 0 wit inspect 4.5  2.4  270 0   0   false(valid-deref) 1 --- inspect 11     6.5   370   .62 0   error 0 --- inspect 4.0  2.3  250 0   0   true -32 --- inspect .65   .65   20    .078 0      - --- inspect
array-memsafety/selectionsort_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .16 .30 35 1.5 .049  0     timeout (exception) 0 wit inspect 94    78    2100 0   0   false(valid-deref) 1 --- inspect 8.2   4.6   320   .62 0   timeout 0 --- inspect 95    80    2500 0   0   true -32 --- inspect .62   .62   20    .066 0      - --- inspect
array-memsafety/stroeder1_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .17 .29 35 1.4 .049  0     false(valid-deref) 1 wit inspect 3.6  2.0  240 0   0   false(valid-deref) 1 --- inspect 7.6   4.4   310   .62 0   unknown 0 --- inspect 4.2  2.6  250 0   0   true -32 --- inspect .61   .61   20    .061 .0041 - --- inspect
array-memsafety/add_last-alloca_true-valid-memsafety_true-termination.i out of memory (unknown) 0 --- inspect 19    9.4  15000 210   .17   0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0   0  
array-memsafety/array01-alloca_true-valid-memsafety_true-termination.i out of memory (unknown) 0 --- inspect 19    9.4  15000 210   .38   .057 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .031 5.6 0   0  
array-memsafety/array02-alloca_true-valid-memsafety_true-termination.i out of memory (unknown) 0 --- inspect 19    9.4  15000 210   .37   0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .025 5.6 0   0  
array-memsafety/array03-alloca_true-valid-memsafety_true-termination.i out of memory (unknown) 0 --- inspect 19    9.5  15000 200   .34   0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
array-memsafety/bubblesort-alloca_true-valid-memsafety_true-termination.i out of memory (unknown) 0 --- inspect 19    9.4  15000 220   .52   0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
array-memsafety/count_down-alloca_true-valid-memsafety_true-termination.i out of memory (unknown) 0 --- inspect 19    9.5  15000 200   .83   18     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0   0  
array-memsafety/cstrcat-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect .32 .31 49 2.4 .0082 18     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
array-memsafety/cstrchr-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect .17 .30 35 1.3 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .029 .029 5.6 0   0  
array-memsafety/cstrcmp-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect .17 .29 33 2.3 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
array-memsafety/cstrcpy-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect .16 .29 32 1.5 .0082 0     - --- 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 .47 .33 49 1.3 .0041 18     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
array-memsafety/cstrlen-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect .36 .30 49 1.4 .0082 18     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0   0  
array-memsafety/cstrncat-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect .26 .29 49 2.2 .0082 19     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
array-memsafety/cstrncmp-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect .28 .31 33 2.1 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .022 5.6 0   0  
array-memsafety/cstrncpy-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect .17 .29 34 1.5 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
array-memsafety/cstrpbrk-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect .17 .29 35 1.5 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
array-memsafety/cstrspn-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect .31 .29 49 1.6 .0041 18     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0   0  
array-memsafety/diff-alloca_true-valid-memsafety_true-termination.i out of memory (unknown) 0 --- inspect 20    9.4  15000 190   .85   0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0   0  
array-memsafety/insertionsort-alloca_true-valid-memsafety_true-termination.i out of memory (unknown) 0 --- inspect 19    9.5  15000 220   .36   0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.7 0   0  
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety_true-termination.i out of memory (unknown) 0 --- inspect 19    9.4  15000 200   .086  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .027 5.6 0   0  
array-memsafety/lis-alloca_true-valid-memsafety_true-termination.i out of memory (unknown) 0 --- inspect 31    10    15000 290   .56   0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0   0  
array-memsafety/mult_array-alloca_true-valid-memsafety_true-termination.i out of memory (unknown) 0 --- inspect 20    9.5  15000 230   .49   19     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .023 5.6 0   0  
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect .15 .29 34 1.4 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect .15 .29 36 1.5 .0082 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 .16 .29 35 1.4 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0   0  
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect .15 .28 35 1.5 .0082 .44  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0   0  
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect .17 .30 35 1.3 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.5 0   0  
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect .20 .29 36 1.4 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .034 .035 5.5 0   0  
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect .21 .29 36 2.0 .0082 .078 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0   0  
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect .17 .29 36 2.3 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect .29 .29 49 1.7 .0082 18     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect .20 .31 36 1.7 .0041 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.7 0   0  
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect .21 .32 34 1.5 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0   0  
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect .14 .29 34 1.2 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0   0  
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect .22 .31 36 1.9 .0082 .13  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0   0  
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect .23 .33 35 1.4 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0   0  
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect .42 .32 49 1.4 .0082 19     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect .38 .30 49 1.5 .0082 18     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0   0  
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect .19 .30 36 1.6 .0041 .053 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect .19 .29 37 1.8 .0041 .46  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect .30 .29 50 2.3 .0041 19     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
array-memsafety/rec_strlen-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect .14 .28 36 1.3 .0082 .39  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .050 .052 5.5 0   0  
array-memsafety/selectionsort-alloca_true-valid-memsafety_true-termination.i out of memory (unknown) 0 --- inspect 19    9.4  15000 190   .037  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
array-memsafety/stroeder1-alloca_true-valid-memsafety_true-termination.i out of memory (unknown) 0 --- inspect 19    9.4  15000 200   .86   0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
array-memsafety/stroeder2-alloca_true-valid-memsafety_true-termination.i out of memory (unknown) 0 --- inspect 20    9.4  15000 220   .38   0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .022 5.6 0   0  
array-memsafety/strreplace-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect .17 .31 35 2.2 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .026 5.6 0   0  
array-memsafety/subseq-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect .17 .29 35 1.4 .0082 0     - --- 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 .18 .29 35 1.3 .0041 .45  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.6 0   0  
array-examples/relax_false-valid-deref.i unknown 0 --- inspect .14 .29 35 1.1 0      0     error (invalid witness file) 0 --- inspect .59 .36 40 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .66 48 0   0   error (invalid witness file) 0 --- inspect .0065 .0091 .53 0     0      - --- inspect
array-examples/sanfoundry_24_false-valid-deref.i timeout 0 --- inspect 900    450    4200 8700   .020  0     error (invalid witness file) 0 --- inspect .66 .42 40 0   0   error (2) 0 --- inspect .021 .022 5.8 0    0   error (invalid witness file) 0 --- inspect .99 .64 48 0   0   error (invalid witness file) 0 --- inspect .0033 .0088 .53 0     0      - --- inspect
array-examples/standard_strcpy_false-valid-deref_ground.i timeout 0 --- inspect 900    310    5500 8600   .0041 0     error (invalid witness file) 0 --- inspect .59 .36 40 0   0   error (2) 0 --- inspect .021 .022 5.7 0    0   error (invalid witness file) 0 --- inspect 1.0  .64 46 0   0   error (invalid witness file) 0 --- inspect .0053 .0066 .53 0     0      - --- inspect
array-examples/standard_strcpy_original_false-valid-deref.i timeout 0 --- inspect 900    450    4200 9800   .012  0     error (invalid witness file) 0 --- inspect .58 .35 41 0   0   error (2) 0 --- inspect .024 .024 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .66 48 0   0   error (invalid witness file) 0 --- inspect .0056 .0071 .52 0     0      - --- inspect
array-memsafety-realloc/array-realloc_false-valid-free.i unknown 0 --- inspect .19 .30 35 1.4 .033  0     error (invalid witness file) 0 --- inspect .59 .37 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .67 47 0   0   error (invalid witness file) 0 --- inspect .0016 .0022 .52 0     0      - --- inspect
array-memsafety-realloc/array-realloc_true-valid-memsafety.i unknown 0 --- inspect .18 .29 37 1.5 .033  0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 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 14 3000    1400    240000 30000   7.7   280   22 4 330 260   9900 0   0   22 -18 140 85   5200 9.3  0   22 1 330   260   11000 0   0   22 -282 9.7 9.7 310 1.0  .033  49 0 1.1 1.2 280 0   0  
    correct results 14 14 2.6  4.1  540 22   .69  76   4 4 14 7.8 980 0   0   14 14 130 75   4700 8.7  0   1 1 3.7 2.2 250 0   0   6 6 3.9 3.9 120 .43 .029  0
        correct true 0 0 0 0 0 0
        correct false 14 14 2.6  4.1  540 22   .69  76   4 4 14 7.8 980 0   0   14 14 130 75   4700 8.7  0   1 1 3.7 2.2 250 0   0   6 6 3.9 3.9 120 .43 .029  0
    correct-unconfimed results 1 0 .16 .31 36 2.7 .049 0   0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0
        correct-unconfirmed false 1 0 .16 .31 36 2.7 .049 0   0 0 0 0 0
    incorrect results 0 0 1 -32 16 9.4 460 .62 0   0 9 -288 5.7 5.7 180 .62 .0041 0
        incorrect true 0 0 1 -32 16 9.4 460 .62 0   0 9 -288 5.7 5.7 180 .62 .0041 0
        incorrect false 0 0 0 0 0 0
score (71 tasks, max score: 120) 14 4 -18 1 -282 0
Run set predatorhp.sv-comp19_prop-memsafety.MemSafety-Arrays cpa-seq-validate-violation-witnesses-predatorhp.sv-comp19_prop-memsafety.MemSafety-Arrays uautomizer-validate-violation-witnesses-predatorhp.sv-comp19_prop-memsafety.MemSafety-Arrays cpa-witness2test-validate-violation-witnesses-predatorhp.sv-comp19_prop-memsafety.MemSafety-Arrays fshell-witness2test-validate-violation-witnesses-predatorhp.sv-comp19_prop-memsafety.MemSafety-Arrays uautomizer-validate-correctness-witnesses-predatorhp.sv-comp19_prop-memsafety.MemSafety-Arrays