Tool DIVINE 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-10 10:00:20 CET 2018-12-10 10:48:16 CET 2018-12-10 11:10:44 CET 2018-12-10 11:13:11 CET 2018-12-12 20:23:24 CET 2018-12-10 10:51:28 CET
Run set divine-explicit.sv-comp19_prop-memsafety.MemSafety-Arrays cpa-seq-validate-violation-witnesses-divine-explicit.sv-comp19_prop-memsafety.MemSafety-Arrays uautomizer-validate-violation-witnesses-divine-explicit.sv-comp19_prop-memsafety.MemSafety-Arrays cpa-witness2test-validate-violation-witnesses-divine-explicit.sv-comp19_prop-memsafety.MemSafety-Arrays fshell-witness2test-validate-violation-witnesses-divine-explicit.sv-comp19_prop-memsafety.MemSafety-Arrays uautomizer-validate-correctness-witnesses-divine-explicit.sv-comp19_prop-memsafety.MemSafety-Arrays
Options --no-symbolic -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/divine-explicit.2018-12-10_1000.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/divine-explicit.2018-12-10_1000.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/divine-explicit.2018-12-10_1000.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/divine-explicit.2018-12-10_1000.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/divine-explicit.2018-12-10_1000.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 unknown 0 --- inspect 8.5 8.5 450 100 0   0      error (invalid witness file) 0 --- inspect .59 .38 40 0   0   error (2) 0 --- inspect .027 .028 5.6 0    0   error (invalid witness file) 0 --- inspect .96 .62 47 0   0   error (invalid witness file) 0 --- inspect .0062 .0085 .52 0     0   - --- inspect
array-memsafety/bubblesort_unsafe_false-valid-deref.i unknown 0 --- inspect 8.2 8.2 430 96 0   0      error (invalid witness file) 0 --- inspect .59 .37 40 0   0   error (2) 0 --- inspect .031 .032 5.5 0    0   error (invalid witness file) 0 --- inspect .93 .61 47 0   0   error (invalid witness file) 0 --- inspect .0052 .0063 .52 0     0   - --- inspect
array-memsafety/count_down_unsafe_false-valid-deref.i unknown 0 --- inspect 8.4 8.4 450 100 0   0      error (invalid witness file) 0 --- inspect .60 .38 40 0   0   error (2) 0 --- inspect .054 .055 5.5 0    0   error (invalid witness file) 0 --- inspect .98 .66 47 0   0   error (invalid witness file) 0 --- inspect .0064 .0080 .52 0     0   - --- inspect
array-memsafety/cstrcat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 8.3 8.3 430 110 0   .0041 false(valid-deref) 1 wit inspect 3.6  2.1  240 0   0   false(valid-deref) 1 --- inspect 6.8   4.4   310   .62 0   false(valid-deref) 1 --- inspect 3.7  2.2  250 0   2.4 false(valid-deref) 1 --- inspect .60   .59   20    .049 0   - --- inspect
array-memsafety/cstrchr_unsafe_false-valid-deref.i unknown 0 --- inspect 8.3 8.3 450 120 0   0      error (invalid witness file) 0 --- inspect .62 .37 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .93 .60 46 0   0   error (invalid witness file) 0 --- inspect .0059 .0095 .52 0     0   - --- inspect
array-memsafety/cstrlen_unsafe_false-valid-deref.i unknown 0 --- inspect 8.4 8.4 440 110 0   0      error (invalid witness file) 0 --- inspect .60 .38 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .95 .63 47 0   0   error (invalid witness file) 0 --- inspect .0061 .0086 .52 0     0   - --- inspect
array-memsafety/cstrncat_unsafe_false-valid-deref.i unknown 0 --- inspect 8.1 8.1 430 110 0   .0041 error (invalid witness file) 0 --- inspect .60 .37 42 0   0   error (2) 0 --- inspect .045 .047 5.5 0    0   error (invalid witness file) 0 --- inspect .93 .61 47 0   0   error (invalid witness file) 0 --- inspect .0063 .0078 .52 0     0   - --- inspect
array-memsafety/cstrncpy_unsafe_false-valid-deref.i unknown 0 --- inspect 8.4 8.3 430 110 0   0      error (invalid witness file) 0 --- inspect .60 .37 41 0   0   error (2) 0 --- inspect .041 .042 5.5 0    0   error (invalid witness file) 0 --- inspect .99 .66 49 0   0   error (invalid witness file) 0 --- inspect .0048 .0061 .52 0     0   - --- inspect
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i unknown 0 --- inspect 8.5 8.5 440 120 0   0      error (invalid witness file) 0 --- inspect .60 .38 41 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .97 .64 48 0   0   error (invalid witness file) 0 --- inspect .0052 .0068 .52 0     0   - --- inspect
array-memsafety/diff_usafe_false-valid-deref.i unknown 0 --- inspect 8.1 8.1 430 97 0   0      error (invalid witness file) 0 --- inspect .60 .38 40 0   0   error (2) 0 --- inspect .051 .052 5.5 0    0   error (invalid witness file) 0 --- inspect .94 .63 47 0   0   error (invalid witness file) 0 --- inspect .0051 .0062 .53 0     0   - --- inspect
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i unknown 0 --- inspect 8.4 8.4 440 110 0   0      error (invalid witness file) 0 --- inspect .61 .36 42 0   0   error (2) 0 --- inspect .019 .020 5.6 0    0   error (invalid witness file) 0 --- inspect .93 .61 47 0   0   error (invalid witness file) 0 --- inspect .0064 .0079 .52 0     0   - --- inspect
array-memsafety/lis_unsafe_false-valid-deref.i unknown 0 --- inspect 8.3 8.3 450 120 0   0      error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .023 .024 5.6 0    0   error (invalid witness file) 0 --- inspect .97 .63 48 0   0   error (invalid witness file) 0 --- inspect .0046 .0058 .40 0     0   - --- inspect
array-memsafety/mult_array_unsafe_false-valid-deref.i unknown 0 --- inspect 8.4 8.4 450 110 0   0      error (invalid witness file) 0 --- inspect .59 .36 40 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0   error (invalid witness file) 0 --- inspect .99 .69 48 0   0   error (invalid witness file) 0 --- inspect .0050 .0064 .52 0     0   - --- inspect
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i unknown 0 --- inspect 8.5 8.5 450 91 0   0      error (invalid witness file) 0 --- inspect .63 .38 41 0   0   error (2) 0 --- inspect .048 .049 5.5 0    0   error (invalid witness file) 0 --- inspect .92 .58 47 0   0   error (invalid witness file) 0 --- inspect .0061 .0076 .52 0     0   - --- inspect
array-memsafety/reverse_array_unsafe_false-valid-deref.i unknown 0 --- inspect 8.3 8.3 450 120 0   0      error (invalid witness file) 0 --- inspect .63 .40 42 0   0   error (2) 0 --- inspect .043 .044 5.6 0    0   error (invalid witness file) 0 --- inspect .93 .62 46 0   0   error (invalid witness file) 0 --- inspect .0018 .0024 .54 0     0   - --- inspect
array-memsafety/selectionsort_unsafe_false-valid-deref.i unknown 0 --- inspect 8.1 8.1 430 98 0   0      error (invalid witness file) 0 --- inspect .61 .37 42 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 .0057 .013  .53 0     0   - --- inspect
array-memsafety/stroeder1_unsafe_false-valid-deref.i unknown 0 --- inspect 8.2 8.2 430 120 0   .10   error (invalid witness file) 0 --- inspect .65 .40 41 0   0   error (2) 0 --- inspect .021 .022 5.7 0    0   error (invalid witness file) 0 --- inspect .93 .62 47 0   0   error (invalid witness file) 0 --- inspect .0050 .0061 .52 0     0   - --- inspect
array-memsafety/add_last-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.5 8.4 440 120 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.7 0   0  
array-memsafety/array01-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.3 8.3 450 90 0   .10   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .020 5.6 0   0  
array-memsafety/array02-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.4 8.4 450 100 0   0      - --- 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 8.2 8.2 450 91 0   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 unknown 0 --- inspect 8.3 8.3 450 120 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .031 5.5 0   0  
array-memsafety/count_down-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.3 8.3 440 100 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .050 .050 5.5 0   0  
array-memsafety/cstrcat-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.4 8.4 450 120 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .051 .052 5.5 0   0  
array-memsafety/cstrchr-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.3 8.3 440 100 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .050 .052 5.7 0   0  
array-memsafety/cstrcmp-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.4 8.4 450 100 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .045 .049 5.5 0   0  
array-memsafety/cstrcpy-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.3 8.3 450 100 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.8 0   0  
array-memsafety/cstrcspn-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.4 8.4 450 110 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .045 .047 5.5 0   0  
array-memsafety/cstrlen-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.3 8.3 450 99 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
array-memsafety/cstrncat-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.3 8.4 450 81 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
array-memsafety/cstrncmp-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.4 8.4 450 110 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0   0  
array-memsafety/cstrncpy-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.4 8.5 450 110 0   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 8.3 8.4 450 120 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .024 5.6 0   0  
array-memsafety/cstrspn-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.2 8.2 450 110 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .039 .041 5.6 0   0  
array-memsafety/diff-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.5 8.5 450 100 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .027 5.7 0   0  
array-memsafety/insertionsort-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.4 8.4 450 96 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.6 8.6 440 110 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.8 0   0  
array-memsafety/lis-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.2 8.2 450 120 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0   0  
array-memsafety/mult_array-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.4 8.4 450 120 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .020 5.6 0   0  
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.3 8.4 450 100 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .031 5.6 0   0  
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.4 8.4 450 100 0   .13   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .020 5.6 0   0  
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.5 8.5 440 110 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.3 8.3 450 130 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .054 .055 5.5 0   0  
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.3 8.4 450 120 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.4 8.4 450 96 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .029 5.6 0   0  
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.5 8.5 450 100 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .035 .036 5.6 0   0  
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.3 8.3 450 92 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .024 5.6 0   0  
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.2 8.3 450 92 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.4 8.4 450 110 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.5 8.5 450 110 0   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 8.5 8.5 450 100 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .029 5.6 0   0  
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.2 8.2 440 110 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.6 0   0  
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.3 8.4 450 98 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0   0  
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.4 8.4 450 100 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.6 0   0  
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.4 8.4 450 100 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .035 .036 5.5 0   0  
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.5 8.5 450 110 0   .10   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .029 5.6 0   0  
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.5 8.5 450 110 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .049 .053 5.5 0   0  
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.5 8.5 450 93 0   .025  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0   0  
array-memsafety/rec_strlen-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.4 8.4 450 110 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .030 5.6 0   0  
array-memsafety/selectionsort-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.4 8.4 450 100 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
array-memsafety/stroeder1-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.4 8.4 450 110 0   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 unknown 0 --- inspect 8.3 8.3 450 100 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .049 .049 5.5 0   0  
array-memsafety/strreplace-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.4 8.4 440 120 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0   0  
array-memsafety/subseq-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.3 8.3 450 110 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .024 5.6 0   0  
array-memsafety/substring-alloca_true-valid-memsafety_true-termination.i unknown 0 --- inspect 8.4 8.4 450 100 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0   0  
array-examples/relax_false-valid-deref.i unknown 0 --- inspect 8.3 8.3 450 100 0   0      error (invalid witness file) 0 --- inspect .61 .37 40 0   0   error (2) 0 --- inspect .051 .052 5.5 0    0   error (invalid witness file) 0 --- inspect .97 .64 47 0   0   error (invalid witness file) 0 --- inspect .0016 .0022 .41 0     0   - --- inspect
array-examples/sanfoundry_24_false-valid-deref.i unknown 0 --- inspect 8.3 8.3 430 88 0   0      error (invalid witness file) 0 --- inspect .61 .37 41 0   0   error (2) 0 --- inspect .045 .046 5.5 0    0   error (invalid witness file) 0 --- inspect .99 .69 48 0   0   error (invalid witness file) 0 --- inspect .0051 .0065 .39 0     0   - --- inspect
array-examples/standard_strcpy_false-valid-deref_ground.i unknown 0 --- inspect 8.0 8.0 430 110 0   0      error (invalid witness file) 0 --- inspect .61 .37 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .93 .61 47 0   0   error (invalid witness file) 0 --- inspect .0051 .0070 .54 0     0   - --- inspect
array-examples/standard_strcpy_original_false-valid-deref.i unknown 0 --- inspect 8.2 8.2 430 100 0   0      error (invalid witness file) 0 --- inspect .62 .37 42 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .60 47 0   0   error (invalid witness file) 0 --- inspect .0053 .0066 .53 0     0   - --- inspect
array-memsafety-realloc/array-realloc_false-valid-free.i unknown 0 --- inspect 8.3 8.4 450 100 0   0      error (invalid witness file) 0 --- inspect .59 .36 40 0   0   error (2) 0 --- inspect .028 .029 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .67 48 0   0   error (invalid witness file) 0 --- inspect .0058 .013  .53 0     0   - --- inspect
array-memsafety-realloc/array-realloc_true-valid-memsafety.i unknown 0 --- inspect 8.4 8.4 440 110 0   0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .044 .046 5.5 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 1 590   590   31000 7500 0   .47   22 1 16   10   1100 0   0   22 1 7.5 5.1 420 .62 0   22 1 24   15   1200 0   2.4 22 1 .70 .75 31 .049 0   49 0 1.4 1.4 270 0   0  
    correct results 1 1 8.3 8.3 430 110 0   .0041 1 1 3.6 2.1 240 0   0   1 1 6.8 4.4 310 .62 0   1 1 3.7 2.2 250 0   2.4 1 1 .60 .59 20 .049 0   0
        correct true 0 0 0 0 0 0
        correct false 1 1 8.3 8.3 430 110 0   .0041 1 1 3.6 2.1 240 0   0   1 1 6.8 4.4 310 .62 0   1 1 3.7 2.2 250 0   2.4 1 1 .60 .59 20 .049 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 (71 tasks, max score: 120) 1 1 1 1 1 0
Run set divine-explicit.sv-comp19_prop-memsafety.MemSafety-Arrays cpa-seq-validate-violation-witnesses-divine-explicit.sv-comp19_prop-memsafety.MemSafety-Arrays uautomizer-validate-violation-witnesses-divine-explicit.sv-comp19_prop-memsafety.MemSafety-Arrays cpa-witness2test-validate-violation-witnesses-divine-explicit.sv-comp19_prop-memsafety.MemSafety-Arrays fshell-witness2test-validate-violation-witnesses-divine-explicit.sv-comp19_prop-memsafety.MemSafety-Arrays uautomizer-validate-correctness-witnesses-divine-explicit.sv-comp19_prop-memsafety.MemSafety-Arrays