Tool PeSCo 1.7-svn b8d6131600+ 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* [apollon004; apollon069; apollon137; apollon154] [apollon004; apollon006; apollon021; apollon061; apollon109; apollon155] 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-06 12:44:04 CET 2018-12-08 07:39:30 CET 2018-12-08 12:16:42 CET 2018-12-08 13:32:07 CET 2018-12-12 20:37:42 CET 2018-12-08 09:11:31 CET
Run set pesco.sv-comp19_prop-memsafety.MemSafety-Arrays cpa-seq-validate-violation-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-Arrays uautomizer-validate-violation-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-Arrays cpa-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-Arrays fshell-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-Arrays uautomizer-validate-correctness-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-Arrays
Options -svcomp19-pesco -heap 10000M -stack 2048k -benchmark -timelimit 900s -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/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/pesco.2018-12-06_1244.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/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/pesco.2018-12-06_1244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/pesco.2018-12-06_1244.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 error 0 wit inspect 3.6 1.3 280 31 0   0   error (1) 0 --- inspect .72 .44 44 0   0   false(valid-deref) 1 --- inspect 9.5   5.4   330   .66 0   unknown 0 --- inspect 1.0  .65 49 0   0   error (1) 0 --- inspect .071  .072  11    0     0   - --- inspect
array-memsafety/bubblesort_unsafe_false-valid-deref.i timeout (segmentation fault) 0 --- inspect 920   600   12000 8700 0   0   error (invalid witness file) 0 --- inspect .66 .42 40 0   0   error (2) 0 --- inspect .025 .026 5.6 0    0   error (invalid witness file) 0 --- inspect .91 .59 48 0   0   error (invalid witness file) 0 --- inspect .0048 .0054 .39 0     0   - --- inspect
array-memsafety/count_down_unsafe_false-valid-deref.i error 0 wit inspect 3.6 1.4 270 32 0   0   error (1) 0 --- inspect .74 .45 46 0   0   false(valid-deref) 1 --- inspect 8.3   4.9   310   .62 0   unknown 0 --- inspect 1.0  .66 50 0   0   error (1) 0 --- inspect .072  .073  12    0     0   - --- inspect
array-memsafety/cstrcat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 2.7 1.2 250 23 0   0   false(valid-deref) 1 wit inspect 3.5  2.0  240 0   0   false(valid-deref) 1 --- inspect 8.8   5.0   320   .62 0   false(valid-deref) 1 --- inspect 3.9  2.3  240 0   0   false(valid-deref) 1 --- inspect .62   .62   20    .049 0   - --- inspect
array-memsafety/cstrchr_unsafe_false-valid-deref.i error 0 wit inspect 3.7 1.4 280 34 0   0   error (1) 0 --- inspect .69 .42 44 0   0   false(valid-deref) 1 --- inspect 15     9.6   520   .62 0   unknown 0 --- inspect 1.0  .66 50 0   0   error (1) 0 --- inspect .11   .12   11    0     0   - --- inspect
array-memsafety/cstrlen_unsafe_false-valid-deref.i error 0 wit inspect 3.7 1.4 280 34 0   0   error (1) 0 --- inspect .74 .46 46 0   0   false(valid-deref) 1 --- inspect 11     6.5   390   .62 0   unknown 0 --- inspect .98 .63 49 0   0   error (1) 0 --- inspect .072  .073  11    0     0   - --- inspect
array-memsafety/cstrncat_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 2.9 1.2 250 26 0   0   false(valid-deref) 1 wit inspect 3.9  2.2  240 0   0   false(valid-deref) 1 --- inspect 8.0   5.0   320   .62 0   unknown 0 --- inspect 3.7  2.3  250 0   0   true -32 --- inspect .60   .60   20    .061 0   - --- inspect
array-memsafety/cstrncpy_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 2.8 1.2 250 25 0   0   false(valid-deref) 1 wit inspect 3.8  2.1  250 0   0   true -32 --- inspect 6.7   3.8   300   .66 0   unknown 0 --- inspect 4.0  2.5  250 0   0   true -32 --- inspect .62   .63   20    .061 0   - --- inspect
array-memsafety/cstrpbrk_unsafe_false-valid-deref.i error 0 wit inspect 3.7 1.4 280 31 0   0   error (1) 0 --- inspect .69 .42 45 0   0   false(valid-deref) 1 --- inspect 25     19     490   .62 0   unknown 0 --- inspect 1.1  .68 51 0   0   error (1) 0 --- inspect .074  .073  11    0     0   - --- inspect
array-memsafety/diff_usafe_false-valid-deref.i timeout (exception) 0 wit inspect 900   660   9900 11000 0   0   error (1) 0 --- inspect .77 .46 44 0   0   false(valid-deref) 1 --- inspect 7.7   4.8   310   .66 0   unknown 0 --- inspect 1.1  .69 51 0   0   error (1) 0 --- inspect .070  .070  12    0     0   - --- inspect
array-memsafety/knapsack_alloca_unsafe_false-valid-deref.i error 0 wit inspect 3.7 1.4 280 36 0   0   error (1) 0 --- inspect .70 .44 44 0   0   false(valid-deref) 1 --- inspect 9.2   5.2   320   .66 0   unknown 0 --- inspect 1.1  .70 50 0   0   error (1) 0 --- inspect .076  .075  11    0     0   - --- inspect
array-memsafety/lis_unsafe_false-valid-deref.i error 0 wit inspect 3.6 1.4 280 33 0   0   error (1) 0 --- inspect .70 .43 44 0   0   false(valid-deref) 1 --- inspect 15     8.8   460   .66 0   unknown 0 --- inspect 1.0  .67 51 0   0   error (1) 0 --- inspect .067  .067  12    0     0   - --- inspect
array-memsafety/mult_array_unsafe_false-valid-deref.i error 0 wit inspect 3.7 1.5 280 33 0   0   error (1) 0 --- inspect .68 .43 44 0   0   false(valid-deref) 1 --- inspect 9.3   5.7   330   .62 0   unknown 0 --- inspect 1.1  .70 50 0   0   error (1) 0 --- inspect .070  .069  11    0     0   - --- inspect
array-memsafety/reverse_array_alloca_unsafe_false-valid-deref.i error 0 wit inspect 3.6 1.4 270 30 0   0   error (1) 0 --- inspect .69 .42 44 0   0   false(valid-deref) 1 --- inspect 11     6.2   340   .66 0   unknown 0 --- inspect 1.1  .71 50 0   0   error (1) 0 --- inspect .069  .070  11    0     0   - --- inspect
array-memsafety/reverse_array_unsafe_false-valid-deref.i error 0 wit inspect 3.6 1.4 250 34 0   0   error (1) 0 --- inspect .85 .52 45 0   0   false(valid-deref) 1 --- inspect 9.7   5.4   320   .62 0   unknown 0 --- inspect 1.0  .65 50 0   0   error (1) 0 --- inspect .068  .068  12    0     0   - --- inspect
array-memsafety/selectionsort_unsafe_false-valid-deref.i timeout 0 wit inspect 900   680   8900 8300 0   0   error (1) 0 --- inspect .69 .41 46 0   0   false(valid-deref) 1 --- inspect 7.7   4.4   310   .62 0   unknown 0 --- inspect 1.0  .66 49 0   0   error (1) 0 --- inspect .081  .081  11    0     0   - --- inspect
array-memsafety/stroeder1_unsafe_false-valid-deref.i false(valid-deref) 1 wit inspect 2.8 1.2 250 25 0   0   false(valid-deref) 1 wit inspect 3.5  2.0  250 0   0   false(valid-deref) 1 --- inspect 7.3   4.6   310   .62 0   unknown 0 --- inspect 3.9  2.3  250 0   0   true -32 --- inspect .61   .61   20    .070 0   - --- inspect
array-memsafety/add_last-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.8 1.4 280 30 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960 880   1200 .75 0  
array-memsafety/array01-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.6 1.4 260 32 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 14 7.9 430 .66 0  
array-memsafety/array02-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.6 1.4 270 32 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 13 7.9 440 .66 0  
array-memsafety/array03-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.7 1.4 280 33 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 13 8.0 450 .62 0  
array-memsafety/bubblesort-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.3 1.3 250 32 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 13 7.2 400 .66 0  
array-memsafety/count_down-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.5 1.3 270 36 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 16 9.4 510 .62 0  
array-memsafety/cstrcat-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.8 1.5 260 35 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960 920   2600 .70 0  
array-memsafety/cstrchr-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.7 1.4 280 32 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 17 10   500 .66 0  
array-memsafety/cstrcmp-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.8 1.4 280 30 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 36 23   560 .62 0  
array-memsafety/cstrcpy-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.7 1.4 280 31 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 22 14   600 .62 0  
array-memsafety/cstrcspn-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.6 1.3 280 32 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 31 19   530 .66 0  
array-memsafety/cstrlen-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.6 1.4 280 31 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 19 11   460 .62 0  
array-memsafety/cstrncat-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.8 1.5 280 33 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960 910   2600 1.6  0  
array-memsafety/cstrncmp-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.7 1.4 280 33 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 37 24   700 .66 0  
array-memsafety/cstrncpy-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.7 1.4 280 35 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 24 16   640 .66 0  
array-memsafety/cstrpbrk-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.7 1.4 280 31 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 64 50   810 .62 0  
array-memsafety/cstrspn-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.7 1.4 260 34 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 69 53   660 .62 0  
array-memsafety/diff-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.9 1.4 280 34 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 25 16   610 .62 0  
array-memsafety/insertionsort-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.7 1.4 280 32 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 18 11   470 .62 0  
array-memsafety/java_BubbleSort-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.7 1.4 280 29 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 14 8.5 460 .66 0  
array-memsafety/lis-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.8 1.4 280 40 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 28 17   700 .66 0  
array-memsafety/mult_array-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.8 1.4 280 35 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 27 21   460 .62 0  
array-memsafety/openbsd_cbzero-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.8 1.4 280 31 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 15 9.0 500 .66 0  
array-memsafety/openbsd_cmemchr-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.8 1.4 280 32 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 16 9.3 500 .62 0  
array-memsafety/openbsd_cmemrchr-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.7 1.4 280 34 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 28 21   520 .62 0  
array-memsafety/openbsd_cmemset-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.4 1.4 250 30 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 17 10   510 .62 0  
array-memsafety/openbsd_cstpcpy-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.3 1.3 250 34 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 22 14   480 .66 0  
array-memsafety/openbsd_cstpncpy-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.7 1.4 280 32 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 65 42   840 .62 0  
array-memsafety/openbsd_cstrcat-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.8 1.4 280 37 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960 910   2800 .70 0  
array-memsafety/openbsd_cstrcmp-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.5 1.4 250 35 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 36 24   700 .66 0  
array-memsafety/openbsd_cstrcpy-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.6 1.4 250 31 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 18 11   520 .66 0  
array-memsafety/openbsd_cstrcspn-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.8 1.4 280 31 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 38 26   580 .66 0  
array-memsafety/openbsd_cstrlcpy-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.8 1.4 280 38 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 40 25   730 .62 0  
array-memsafety/openbsd_cstrlen-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.7 1.4 270 36 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 14 8.7 470 .66 0  
array-memsafety/openbsd_cstrncat-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.8 1.4 280 33 0   0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960 900   2100 .73 0  
array-memsafety/openbsd_cstrncmp-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.7 1.4 280 31 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 39 26   710 .66 0  
array-memsafety/openbsd_cstrncpy-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.7 1.4 280 33 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 34 22   740 .66 0  
array-memsafety/openbsd_cstrnlen-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.8 1.5 280 33 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 17 10   520 .62 0  
array-memsafety/openbsd_cstrpbrk-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.4 1.4 250 34 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 35 25   550 .62 0  
array-memsafety/openbsd_cstrspn-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.7 1.4 280 31 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 32 21   550 .62 0  
array-memsafety/openbsd_cstrstr-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.6 1.4 250 31 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 850 810   1200 .62 0  
array-memsafety/rec_strlen-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.6 1.4 280 36 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 16 10   470 .66 0  
array-memsafety/selectionsort-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.7 1.4 280 37 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 24 14   490 .66 0  
array-memsafety/stroeder1-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.7 1.4 280 30 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 14 8.2 440 .62 0  
array-memsafety/stroeder2-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.4 1.4 250 32 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 13 7.5 460 .66 0  
array-memsafety/strreplace-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.7 1.4 280 31 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 21 14   550 .62 0  
array-memsafety/subseq-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.5 1.4 250 30 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 44 33   700 .62 0  
array-memsafety/substring-alloca_true-valid-memsafety_true-termination.i error 0 wit inspect 3.9 1.5 280 32 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 240 210   1200 .62 0  
array-examples/relax_false-valid-deref.i error 0 wit inspect 3.8 1.4 280 32 0   0   error (1) 0 --- inspect .83 .51 46 0   0   false(valid-deref) 1 --- inspect 10     5.8   330   .62 0   unknown 0 --- inspect 1.1  .68 51 0   0   error (1) 0 --- inspect .083  .082  11    0     0   - --- inspect
array-examples/sanfoundry_24_false-valid-deref.i timeout 0 wit inspect 900   860   4800 13000 0   0   error (1) 0 --- inspect .69 .43 45 0   0   timeout 0 --- inspect 97     67     950   1.5  0   unknown 0 --- inspect 1.3  .80 50 0   0   error (1) 0 --- inspect .072  .073  12    0     0   - --- inspect
array-examples/standard_strcpy_false-valid-deref_ground.i timeout 0 wit inspect 900   770   5200 12000 0   0   error (1) 0 --- inspect .69 .43 45 0   0   timeout 0 --- inspect 96     68     810   .73 0   unknown 0 --- inspect 1.0  .67 51 0   0   error (1) 0 --- inspect .083  .082  11    0     0   - --- inspect
array-examples/standard_strcpy_original_false-valid-deref.i timeout 0 wit inspect 900   760   5200 12000 0   0   error (1) 0 --- inspect .78 .45 45 0   0   timeout 0 --- inspect 97     68     950   .72 0   unknown 0 --- inspect .99 .65 49 0   0   error (1) 0 --- inspect .071  .071  11    0     0   - --- inspect
array-memsafety-realloc/array-realloc_false-valid-free.i true -32 wit inspect 11   6.4 460 110 0   0   error (1) 0 --- inspect .72 .43 44 0   0   false(valid-free) 1 --- inspect 12     6.7   390   .66 0   unknown 0 --- inspect .98 .62 50 0   0   error (1) 0 --- inspect .075  .075  11    0     0   - --- inspect
array-memsafety-realloc/array-realloc_true-valid-memsafety.i false(valid-free) -16 wit inspect 4.2 1.5 290 33 0   0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 11 6.7 360 .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 -44 5700   4400   64000 66000 0   0   22 4 28 16   1800 0   0   22 -15 480   320   9100 14    0   22 1 34   21   1900 0   0   22 -95 3.7  3.8  270 .24  0   49 88 7000 6300 37000 33 0  
    correct results 4 4 11   4.9 990 99 0   0   4 4 15 8.2 980 0   0   17 17 190   110   6100 11    0   1 1 3.9 2.3 240 0   0   1 1 .62 .62 20 .049 0   44 88 2200 1800 26000 28 0  
        correct true 0 0 0 0 0 44 88 2200 1800 26000 28 0  
        correct false 4 4 11   4.9 990 99 0   0   4 4 15 8.2 980 0   0   17 17 190   110   6100 11    0   1 1 3.9 2.3 240 0   0   1 1 .62 .62 20 .049 0   0
    incorrect results 2 -48 15   7.8 750 140 0   0   0 1 -32 6.7 3.8 300 .66 0   0 3 -96 1.8  1.8  61 .19  0   0
        incorrect true 1 -32 11   6.4 460 110 0   0   0 1 -32 6.7 3.8 300 .66 0   0 3 -96 1.8  1.8  61 .19  0   0
        incorrect false 1 -16 4.2 1.5 290 33 0   0   0 0 0 0 0
score (71 tasks, max score: 120) -44 4 -15 1 -95 88
Run set pesco.sv-comp19_prop-memsafety.MemSafety-Arrays cpa-seq-validate-violation-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-Arrays uautomizer-validate-violation-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-Arrays cpa-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-Arrays fshell-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-Arrays uautomizer-validate-correctness-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-Arrays