Tool symbiotic 6.0.3-77d4af47 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* [apollon013; apollon098] 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 21:42:05 CET 2018-12-08 23:40:56 CET 2018-12-09 00:46:04 CET 2018-12-09 01:29:54 CET 2018-12-12 21:10:03 CET 2018-12-08 23:47:25 CET
Run set symbiotic.sv-comp19_prop-memsafety.MemSafety-Arrays cpa-seq-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-Arrays uautomizer-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-Arrays cpa-witness2test-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-Arrays fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-Arrays uautomizer-validate-correctness-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-Arrays
Options --witness 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/symbiotic.2018-12-07_2142.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/symbiotic.2018-12-07_2142.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/symbiotic.2018-12-07_2142.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/symbiotic.2018-12-07_2142.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/symbiotic.2018-12-07_2142.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 .21 .20 18 2.4 0     0    false(valid-deref) 1 wit inspect 4.4  2.4  250 0   .037  false(valid-deref) 1 --- inspect 8.6   4.9   310   .62 0   unknown 0 --- inspect 4.3  2.5  250 0   0      true -32 --- inspect .64   .64   20    .074 0     - --- inspect
array-memsafety/bubblesort_unsafe_false-valid-deref.i error(unknown, verification-finished) 0 --- inspect .18 .17 19 2.1 0     0    error (invalid witness file) 0 --- inspect .73 .45 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .95 .63 46 0   0      error (invalid witness file) 0 --- inspect .0016 .0019 .40 0     0     - --- inspect
array-memsafety/count_down_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .21 .21 17 2.9 0     0    false(valid-deref) 1 wit inspect 4.2  2.3  260 0   .59   false(valid-deref) 1 --- inspect 8.0   4.5   310   .62 0   unknown 0 --- inspect 4.2  2.4  250 0   0      false(valid-deref) 1 --- inspect .65   .65   20    .074 0     - --- inspect
array-memsafety/cstrcat_unsafe_false-valid-deref.i error(unknown, verification-finished) 0 --- inspect .15 .14 15 1.7 0     0    error (invalid witness file) 0 --- inspect .68 .42 41 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .92 .59 46 0   0      error (invalid witness file) 0 --- inspect .0017 .0021 .52 0     0     - --- inspect
array-memsafety/cstrchr_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .95 .94 17 12   0     0    error 0 wit inspect 4.5  2.4  250 0   0      true -32 --- inspect 9.1   5.1   320   .62 0   error 0 --- inspect 4.5  2.5  250 0   0      false(valid-deref) 1 --- inspect .70   .71   20    .078 0     - --- inspect
array-memsafety/cstrlen_unsafe_false-valid-deref.i false(valid-deref) 0 wit inspect .31 .30 18 3.1 0     0    error 0 wit inspect 5.2  2.8  250 0   0      true -32 --- inspect 8.3   5.1   310   .62 0   error 0 --- inspect 4.4  2.4  270 0   0      true -32 --- inspect .67   .67   20    .078 .025 - --- inspect
array-memsafety/cstrncat_unsafe_false-valid-deref.i error(unknown, verification-finished) 0 --- inspect .17 .16 16 1.7 0     0    error (invalid witness file) 0 --- inspect .59 .36 40 0   0      error (2) 0 --- inspect .022 .024 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .70 47 0   0      error (invalid witness file) 0 --- inspect .0048 .0061 .52 0     0     - --- inspect
array-memsafety/cstrncpy_unsafe_false-valid-deref.i error(unknown, verification-finished) 0 --- inspect .17 .17 18 2.4 0     0    error (invalid witness file) 0 --- inspect .57 .37 40 0   0      error (2) 0 --- inspect .022 .024 5.6 0    0   error (invalid witness file) 0 --- inspect .98 .63 47 0   0      error (invalid witness file) 0 --- inspect .0020 .0031 .53 0     0     - --- inspect
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .76 .76 18 10   0     0    error 0 wit inspect 5.3  2.8  270 0   0      true -32 --- inspect 9.1   5.2   330   .62 0   error 0 --- inspect 4.2  2.4  250 0   0      false(valid-deref) 1 --- inspect .65   .65   20    .078 0     - --- inspect
array-memsafety/diff_usafe_false-valid-deref.i error(unknown, verification-finished) 0 --- inspect .19 .18 18 2.0 0     0    error (invalid witness file) 0 --- inspect .59 .37 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .91 .60 47 0   0      error (invalid witness file) 0 --- inspect .0037 .0049 .40 0     0     - --- inspect
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .25 .24 18 4.3 0     0    false(valid-deref) 1 wit inspect 4.9  2.6  250 0   0      false(valid-deref) 1 --- inspect 9.1   5.2   330   .62 0   unknown 0 --- inspect 4.6  2.7  250 0   0      true -32 --- inspect 3.0    3.0    20    .082 0     - --- inspect
array-memsafety/lis_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .40 .39 18 5.3 0     0    false(valid-deref) 1 wit inspect 4.3  2.3  250 0   0      true -32 --- inspect 13     7.7   420   .62 0   unknown 0 --- inspect 5.7  3.2  250 0   0      false(valid-deref) 1 --- inspect .65   .64   20    .078 0     - --- inspect
array-memsafety/mult_array_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .31 .31 21 3.8 0     0    false(valid-deref) 1 wit inspect 4.5  2.4  250 0   .025  false(valid-deref) 1 --- inspect 8.7   5.0   320   .62 0   unknown 0 --- inspect 4.9  2.8  270 0   .086  false(valid-deref) 1 --- inspect .67   .69   20    .078 .025 - --- inspect
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .54 .53 18 8.0 0     .28 false(valid-deref) 1 wit inspect 4.5  2.4  250 0   .62   false(valid-deref) 1 --- inspect 11     6.0   330   .62 0   unknown 0 --- inspect 4.6  2.6  250 0   0      true -32 --- inspect .65   .64   20    .078 0     - --- inspect
array-memsafety/reverse_array_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect .23 .23 18 3.0 0     0    false(valid-deref) 1 wit inspect 4.4  2.4  250 0   0      false(valid-deref) 1 --- inspect 9.9   5.9   320   .62 0   unknown 0 --- inspect 4.3  2.4  250 0   0      true -32 --- inspect .64   .64   20    .078 0     - --- inspect
array-memsafety/selectionsort_unsafe_false-valid-deref.i error(unknown, verification-finished) 0 --- inspect .19 .18 17 1.9 0     0    error (invalid witness file) 0 --- inspect .60 .37 40 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .90 .59 47 0   0      error (invalid witness file) 0 --- inspect .0017 .0031 .53 0     0     - --- inspect
array-memsafety/stroeder1_unsafe_false-valid-deref.i error(unknown, verification-finished) 0 --- inspect .18 .17 18 2.3 0     0    error (invalid witness file) 0 --- inspect .66 .41 41 0   0      error (2) 0 --- inspect .022 .024 5.7 0    0   error (invalid witness file) 0 --- inspect .90 .58 46 0   0      error (invalid witness file) 0 --- inspect .0043 .0053 .52 0     0     - --- inspect
array-memsafety/add_last-alloca_true-valid-memsafety_true-termination.i true 2 wit inspect .22 .22 19 2.4 0     0    - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     860     1200   1.6  0  
array-memsafety/array01-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    1400 12000   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0    0  
array-memsafety/array02-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    6400 13000   .033 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0    0  
array-memsafety/array03-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    1300 10000   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0    0  
array-memsafety/bubblesort-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    130 12000   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0    0  
array-memsafety/count_down-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    470 7500   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0    0  
array-memsafety/cstrcat-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    320 13000   .016 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.7 0    0  
array-memsafety/cstrchr-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    350 11000   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0    0  
array-memsafety/cstrcmp-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    470 11000   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0  
array-memsafety/cstrcpy-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    300 13000   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.6 0    0  
array-memsafety/cstrcspn-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    380 13000   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
array-memsafety/cstrlen-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    390 11000   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0    0  
array-memsafety/cstrncat-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    140 9400   .020 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .024 5.8 0    0  
array-memsafety/cstrncmp-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    300 13000   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
array-memsafety/cstrncpy-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    340 9800   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .027 5.6 0    0  
array-memsafety/cstrpbrk-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    400 11000   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .027 5.6 0    0  
array-memsafety/cstrspn-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    390 14000   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.7 0    0  
array-memsafety/diff-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    1300 11000   .025 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 timeout (verification) 0 --- inspect 900    900    1400 9800   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.6 0    0  
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    880 11000   .025 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 timeout (verification) 0 --- inspect 900    900    460 12000   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0    0  
array-memsafety/mult_array-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    1100 12000   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0    0  
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    330 10000   .025 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 timeout (verification) 0 --- inspect 900    900    580 13000   .020 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .028 5.7 0    0  
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    270 12000   .025 0    - --- 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 timeout (verification) 0 --- inspect 900    900    1400 11000   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .023 5.6 0    0  
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    280 10000   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.7 0    0  
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    520 13000   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    340 13000   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.7 0    0  
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    200 11000   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0  
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    230 12000   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .025 5.6 0    0  
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    420 11000   .025 0    - --- 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 timeout (verification) 0 --- inspect 900    900    370 11000   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    350 13000   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.6 0    0  
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    140 10000   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    310 11000   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .025 5.6 0    0  
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    490 14000   .025 0    - --- 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 timeout (verification) 0 --- inspect 900    900    370 11000   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .022 5.6 0    0  
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    330 12000   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.7 0    0  
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    360 11000   .020 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0    0  
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    310 12000   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
array-memsafety/rec_strlen-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    570 11000   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0    0  
array-memsafety/selectionsort-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    1100 11000   .025 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 timeout (verification) 0 --- inspect 900    900    1400 13000   .025 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 timeout (verification) 0 --- inspect 900    900    1500 11000   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0    0  
array-memsafety/strreplace-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    350 12000   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
array-memsafety/subseq-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    430 11000   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.6 0    0  
array-memsafety/substring-alloca_true-valid-memsafety_true-termination.i timeout (verification) 0 --- inspect 900    900    390 14000   .025 0    - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
array-examples/relax_false-valid-deref.i witness invalid (false(valid-deref)) 0 --- inspect .67 .66 18 7.8 0     0    error (invalid witness file) 0 --- inspect .61 .38 40 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .95 .62 48 0   0      error (invalid witness file) 0 --- inspect .0017 .0020 .52 0     0     - --- inspect
array-examples/sanfoundry_24_false-valid-deref.i timeout (verification) 0 --- inspect 900    900    1100 11000   .025 0    error (invalid witness file) 0 --- inspect .70 .44 41 0   0      error (2) 0 --- inspect .023 .026 5.7 0    0   error (invalid witness file) 0 --- inspect .92 .59 47 0   0      error (invalid witness file) 0 --- inspect .0018 .0026 .53 0     0     - --- inspect
array-examples/standard_strcpy_false-valid-deref_ground.i false(valid-deref) 0 wit inspect 2.0  2.0  100 31   0     0    timeout 0 wit inspect 96    64    3400 0   0      true -32 --- inspect 11     6.4   340   .62 0   timeout 0 --- inspect 92    77    2300 0   0      true -32 --- inspect .59   .61   20    .057 0     - --- inspect
array-examples/standard_strcpy_original_false-valid-deref.i false(valid-deref) 0 wit inspect 2.1  2.1  100 29   0     0    timeout 0 wit inspect 98    64    3500 0   .0041 true -32 --- inspect 10     6.4   330   .62 0   timeout 0 --- inspect 92    77    2200 0   .0041 true -32 --- inspect .61   .61   20    .057 0     - --- inspect
array-memsafety-realloc/array-realloc_false-valid-free.i false(valid-free) 1 wit inspect .24 .23 17 2.3 0     0    true -32 wit inspect 5.3  2.8  260 0   0      false(valid-free) 1 --- inspect 12     6.4   350   .62 0   error 0 --- inspect 4.4  2.4  250 0   0      false(valid-free) 1 --- inspect .65   .65   20    .078 0     - --- inspect
array-memsafety-realloc/array-realloc_true-valid-memsafety.i true 2 wit inspect 1.3  1.3  19 18   0     0    - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 34     22     520   .62 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 43000   43000   34000 560000 1.2 .28 22 -25 250   160   10000 0   1.3 22 -185 130 74 4400 8.1 0   22 0 240 190 7700 0   .090 22 -218 11   11   270 .97 .049 49 2 1000 890 2000 2.2  0  
    correct results 12 14 5.6 5.5 220 75 0   .28 7 7 31   17   1700 0   1.3 7 7 67 38 2300 4.4 0   0 6 6 4.0 4.0 120 .46 .025 1 2 34 22 520 .62 0  
        correct true 2 4 1.5 1.5 38 21 0   0    0 0 0 0 1 2 34 22 520 .62 0  
        correct false 10 10 4.1 4.0 180 54 0   .28 7 7 31   17   1700 0   1.3 7 7 67 38 2300 4.4 0   0 6 6 4.0 4.0 120 .46 .025 0
    correct-unconfimed results 3 0 4.4 4.4 220 63 0   0    0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0
        correct-unconfirmed false 3 0 4.4 4.4 220 63 0   0    0 0 0 0 0
    incorrect results 0 1 -32 5.3 2.8 260 0   0   6 -192 61 36 2000 3.7 0   0 7 -224 6.8 6.8 140 .50 .025 0
        incorrect true 0 1 -32 5.3 2.8 260 0   0   6 -192 61 36 2000 3.7 0   0 7 -224 6.8 6.8 140 .50 .025 0
        incorrect false 0 0 0 0 0 0
score (71 tasks, max score: 120) 14 -25 -185 0 -218 2
Run set symbiotic.sv-comp19_prop-memsafety.MemSafety-Arrays cpa-seq-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-Arrays uautomizer-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-Arrays cpa-witness2test-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-Arrays fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-Arrays uautomizer-validate-correctness-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-Arrays