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-Heap cpa-seq-validate-violation-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-Heap uautomizer-validate-violation-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-Heap cpa-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-Heap fshell-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-Heap uautomizer-validate-correctness-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-Heap
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)
memsafety/960521-1_false-valid-deref.i 1 10   3.5 720 85 0   0     1 17    9.0  770 0   0   0 71   45   7000 .75 0     0 15    7.9  770 0   .11   0 .90  .90  28 .053 0      -
memsafety/test-0137_false-valid-deref.i 0 910   680   4700 8400 0   0     0 .76 .46 44 0   0   0 12   6.5 290 .71 0     0 1.0  .63 49 0   0      0 .10  .10  11 0     0      -
memsafety/test-0235_false-valid-deref.i 0 900   750   5000 8600 0   0     0 .82 .48 45 0   0   0 97   86   530 1.6  0     0 1.2  .74 52 0   0      0 .098 .097 11 0     0      -
memsafety/960521-1_false-valid-free.i 1 11   3.5 730 110 0   0     1 15    8.0  760 0   0   0 80   51   7000 1.4  0     0 18    9.3  780 0   0      0 .90  .90  28 .053 0      -
memsafety/test-0158_false-valid-free.i 1 4.1 1.5 280 32 0   0     1 5.3  2.9  250 0   0   1 11   6.2 360 .62 0     0 4.5  2.6  260 0   0      1 .66  .68  20 .070 .033  -
memsafety/test-0232_false-valid-free.i 0 910   550   4800 7400 0   0     0 .73 .45 44 0   0   0 96   78   900 1.5  0     0 1.1  .70 52 0   0      0 .098 .095 11 0     0      -
memsafety/20020406-1_false-valid-memtrack.i 0 4.6 1.5 290 43 0   0     0 .81 .50 44 0   0   0 97   85   860 1.5  0     0 1.3  .81 51 0   0      0 .070 .070 12 0     0      -
memsafety/20051113-1.c_false-valid-memtrack.i 1 4.3 1.6 280 37 0   0     1 6.5  3.5  260 0   0   -32 11   6.0 370 .62 0     0 4.9  2.8  260 0   0      0 .69  .68  21 .053 .025  -
memsafety/lockfree-3.1_false-valid-memtrack.i 0 910   500   5500 5300 0   0     0 .72 .44 46 0   0   0 96   60   810 1.6  0     0 1.0  .67 52 0   0      0 .070 .070 11 0     0      -
memsafety/lockfree-3.2_false-valid-memtrack.i 0 920   430   5700 4800 0   0     0 .77 .46 46 0   0   0 29   16   460 .68 0     0 1.1  .71 52 0   0      0 .068 .068 12 0     0      -
memsafety/lockfree-3.3_false-valid-memtrack.i 0 910   490   5400 6900 0   0     0 .78 .48 45 0   0   0 97   60   960 .82 0     0 1.0  .67 50 0   0      0 .099 .098 11 0     0      -
memsafety/test-0019_false-valid-memtrack_true-termination.i 1 3.4 1.4 260 34 0   0     1 4.4  2.4  250 0   0   0 16   9.5 310 .71 0     0 4.7  2.7  250 0   .0041 -32 .65  .65  20 .074 0      -
memsafety/test-0102_false-valid-memtrack.i 0 900   680   4700 9800 0   0     0 .71 .43 44 0   0   0 12   6.6 290 .75 0     0 1.0  .66 50 0   0      0 .068 .069 11 0     0      -
memsafety/test-0158_false-valid-memtrack_true-termination.i 1 3.4 1.4 260 34 0   0     1 4.2  2.4  250 0   0   0 15   8.4 310 .75 0     0 4.9  2.8  250 0   .070  -32 .66  .66  20 .066 0      -
memsafety/test-0220_false-valid-memtrack.i 0 910   640   4800 8000 0   0     0 .81 .48 44 0   0   0 96   85   550 .68 0     0 .99 .63 50 0   0      0 .11  .13  11 0     0      -
memsafety/test-0232_false-valid-memtrack.i 0 900   550   4800 6900 0   0     0 .70 .43 44 0   0   0 58   40   690 .68 0     0 1.0  .66 49 0   0      0 .067 .067 11 0     0      -
memsafety/test-0234_false-valid-memtrack.i 0 900   750   5000 11000 0   0     0 .82 .51 45 0   0   0 97   86   620 1.6  0     0 1.1  .68 50 0   0      0 .070 .070 11 0     0      -
memsafety/test-0235_false-valid-memtrack.i 0 900   750   4900 10000 0   0     0 .74 .46 45 0   0   0 97   87   530 1.6  0     0 1.0  .66 51 0   0      0 .080 .080 11 0     0      -
memsafety/960521-1_true-valid-memsafety.i 0 900   640   8800 10000 0   0     - - - - 0 960     930     930   .63 0  
memsafety/lockfree-3.0_true-valid-memsafety.i 0 920   430   5800 5900 0   0     - - - - 0 680     590     7000   .67 0  
memsafety/test-0019_true-valid-memsafety_true-termination.i 2 3.6 1.4 280 32 0   0     - - - - 2 23     14     510   .66 0  
memsafety/test-0102_true-valid-memsafety.i 0 900   680   4700 10000 0   0     - - - - 0 13     6.7   290   .71 0  
memsafety/test-0134_true-valid-memsafety.i 0 910   680   4700 9800 0   0     - - - - 0 12     6.6   300   .75 0  
memsafety/test-0158_true-valid-memsafety_true-termination.i 2 3.7 1.4 280 33 0   0     - - - - 2 12     6.9   330   .66 0  
memsafety/test-0214_true-valid-memsafety_false-termination.i 0 910   650   5500 8100 0   0     - - - - 0 960     910     1900   .67 0  
memsafety/test-0217_true-valid-memsafety_false-termination.i 0 910   550   11000 7900 0   0     - - - - 0 960     920     1800   .64 0  
memsafety/test-0218_true-valid-memsafety_false-termination.i 0 970   550   11000 8500 0   0     - - - - 0 .024 .026 5.7 0    0  
memsafety/test-0219_true-valid-memsafety.i 0 900   640   4900 9900 0   0     - - - - 0 960     930     1200   1.5  0  
memsafety/test-0232_true-valid-memsafety.i 0 900   550   4900 8900 0   0     - - - - 0 960     920     1300   .63 0  
memsafety/test-0234_true-valid-memsafety.i 0 910   750   4900 11000 0   0     - - - - 0 960     930     2300   .79 0  
memsafety/test-0235_true-valid-memsafety.i 0 900   750   5000 9700 0   0     - - - - 0 960     930     2300   .70 0  
memsafety/test-0236_true-valid-memsafety.i 0 900   790   4800 10000 0   0     - - - - 0 960     920     2200   1.1  0  
memsafety/test-0237_true-valid-memsafety.i 0 900   790   4800 9700 0   0     - - - - 0 960     930     1100   .75 0  
memsafety/test-0504_true-valid-memsafety.i 0 910   280   11000 6100 0   0     - - - - 0 960     870     3100   1.6  0  
memsafety/test-0513_true-valid-memsafety.i 0 910   250   11000 5600 0   0     - - - - 0 960     870     2000   1.7  0  
memsafety/test-0521_true-valid-memsafety.i 0 940   260   11000 6400 0   0     - - - - 0 960     880     2100   1.7  0  
memsafety/test-memleak_nexttime_true-valid-memsafety_true-termination.i 2 3.6 1.4 250 32 0   0     - - - - 0 960     880     1000   .64 0  
memsafety-ext/dll_extends_pointer_true-valid-memsafety.i 0 910   380   11000 6500 0   0     - - - - 0 960     890     910   .64 0  
memsafety-ext/skiplist_2lvl_true-valid-memsafety.i 0 970   480   12000 7700 0   0     - - - - 0 .026 .027 5.6 0    0  
memsafety-ext/skiplist_3lvl_true-valid-memsafety.i 0 970   500   11000 8000 0   0     - - - - 0 5.6   3.0   270   .65 0  
memsafety-ext/tree_cnstr_true-valid-memsafety_false-termination.i 0 930   350   11000 7000 0   0     - - - - 0 960     930     930   .72 0  
memsafety-ext/tree_dsw_true-valid-memsafety_false-termination.i 0 900   340   11000 6500 0   0     - - - - 0 960     930     1100   .95 0  
memsafety-ext/tree_of_cslls_true-valid-memsafety.i 0 910   370   11000 7400 0   0     - - - - 0 960     920     2000   .72 0  
memsafety-ext/tree_parent_ptr_true-valid-memsafety_false-termination.i 0 910   350   11000 7000 0   0     - - - - 0 960     920     860   .65 0  
memsafety-ext/tree_stack_true-valid-memsafety_false-termination.i 0 910   340   11000 6200 0   0     - - - - 0 960     900     2300   1.8  0  
memsafety-ext2/split_list_test05_false-valid-deref.i 0 900   650   12000 8900 0   0     0 .83 .51 46 0   0   0 96   74   900 1.5  0     0 1.1  .70 51 0   0      0 .074 .075 12 0     .029  -
memsafety-ext2/complex_data_creation_test01_false-valid-memtrack.i 1 4.5 1.6 270 38 0   0     1 6.3  3.4  270 0   0   0 97   79   2700 1.5  0     0 5.9  3.3  280 0   0      0 .58  .58  21 .020 0      -
memsafety-ext2/complex_data_creation_test02_false-valid-memtrack.i 0 900   260   11000 6500 0   0     0 .71 .44 44 0   0   0 96   72   670 1.8  0     0 1.0  .65 49 0   0      0 .069 .069 12 0     0      -
memsafety-ext2/length_test03_false-valid-memtrack.i 0 900   550   4800 6600 0   0     0 .68 .42 44 0   0   0 97   82   640 1.7  0     0 1.0  .66 50 0   0      0 .094 .093 11 0     0      -
memsafety-ext2/optional_data_creation_test04_false-valid-memtrack.i 0 900   580   5100 8400 0   0     0 .79 .47 44 0   0   0 96   77   790 1.5  0     0 1.1  .71 49 0   0      0 .067 .067 11 0     0      -
memsafety-ext2/complex_data_creation_test01_true-valid-memsafety.i 0 910   710   6400 9300 0   0     - - - - 0 960     880     990   .62 0  
memsafety-ext2/complex_data_creation_test02_true-valid-memsafety.i 0 920   260   11000 6400 0   0     - - - - 0 960     900     920   .72 0  
memsafety-ext2/length_test03_true-valid-memsafety.i 0 910   560   5000 6600 0   0     - - - - 0 960     920     1600   .71 0  
memsafety-ext2/optional_data_creation_test04_true-valid-memsafety.i 0 910   850   4200 9300 0   0     - - - - 0 .021 .022 5.6 0    0  
memsafety-ext2/split_list_test05_true-valid-memsafety.i 0 920   620   11000 9200 0   0     - - - - 0 960     920     2200   1.5  0  
list-ext-properties/960521-1_1_false-valid-deref.i 1 6.1 2.0 330 57 0   0     1 8.3  4.3  320 0   0   0 91   57   7000 1.6  0     0 7.7  4.2  330 0   0      0 .71  .71  23 .053 0      -
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i 1 6.6 2.0 310 54 0   0     1 8.8  4.6  350 0   0   -16 37   19   1200 .62 0     0 8.6  4.7  340 0   0      1 .91  .92  23 .082 0      -
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i 0 910   460   6500 4800 0   0     0 .71 .45 46 0   0   1 13   7.7 420 .66 0     0 1.0  .64 52 0   0      0 .068 .069 11 0     0      -
list-ext-properties/960521-1_1_false-valid-free.i 1 6.8 2.1 350 54 0   0     1 8.6  4.5  350 0   0   0 95   60   7000 1.4  .016 0 8.3  4.6  330 0   0      0 .74  .75  23 .053 0      -
list-ext-properties/test-0158_1_false-valid-free.i 1 3.5 1.4 250 29 0   0     1 4.9  2.7  270 0   0   1 12   7.2 340 .62 0     0 4.4  2.6  250 0   0      1 .66  .66  20 .074 0      -
list-ext-properties/test-0019_1_false-valid-memtrack_true-termination.i 1 3.8 1.4 280 34 0   0     1 4.9  2.7  270 0   0   0 16   9.7 330 .71 0     0 4.8  2.7  250 0   .12   -32 .65  .66  20 .074 0      -
list-ext-properties/test-0158_1_false-valid-memtrack_true-termination.i 1 3.7 1.4 280 33 0   0     1 4.4  2.4  250 0   0   0 15   8.5 300 .71 0     0 4.5  2.7  260 0   0      -32 .65  .65  20 .074 0      -
list-ext-properties/test-0232_1_false-valid-memtrack_true-termination.i 1 6.1 1.9 300 53 0   0     1 7.7  4.0  300 0   0   0 97   68   2400 1.7  0     0 8.2  4.5  300 0   0      -32 .69  .69  22 .082 .025  -
list-ext-properties/960521-1_1_true-valid-memsafety.i 2 11   3.1 690 93 0   0     - - - - 0 960     940     980   .62 0  
list-ext-properties/list-ext_1_true-valid-memsafety.i 2 38   14   1900 340 0   0     - - - - 0 960     850     1900   .64 0  
list-ext-properties/list-ext_flag_1_true-valid-memsafety.i 0 930   460   7400 5800 0   0     - - - - 0 960     880     2200   .74 0  
list-ext-properties/simple-ext_1_true-valid-memsafety.i 2 20   6.1 860 160 0   0     - - - - 0 960     900     2400   1.7  0  
list-ext-properties/test-0019_1_true-valid-memsafety_true-termination.i 2 3.8 1.4 280 38 0   0     - - - - 2 35     23     720   .66 0  
list-ext-properties/test-0158_1_true-valid-memsafety_true-termination.i 2 3.5 1.4 280 31 0   0     - - - - 2 10     6.3   340   .62 0  
list-ext-properties/test-0214_1_true-valid-memsafety.i 0 960   930   2500 8500 0   0     - - - - 0 960     920     1500   .65 0  
list-ext-properties/test-0217_1_true-valid-memsafety.i 0 910   510   5400 6100 0   0     - - - - 0 .025 .026 5.6 0    0  
list-ext-properties/test-0232_1_true-valid-memsafety_true-termination.i 2 8.9 2.6 480 79 0   0     - - - - 0 960     920     1300   .62 0  
list-ext-properties/test-0504_1_true-valid-memsafety.i 0 900   420   5900 4900 0   0     - - - - 0 960     910     1100   .63 0  
list-ext-properties/test-0513_1_true-valid-memsafety.i 2 4.8 1.6 280 43 0   0     - - - - 0 960     880     2200   .77 0  
memory-alloca/c.03-alloca_true-valid-memsafety.i 0 900   890   940 11000 0   0     - - - - 2 14     8.2   420   .66 0  
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c 1 2.9 1.2 250 28 0   0     1 3.8  2.2  250 0   0   1 9.2 5.1 310 .66 0     1 4.0  2.4  250 0   3.2    1 .64  .64  20 .082 .0041 -
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-write.c 1 2.8 1.2 250 24 0   0     1 3.8  2.1  250 0   0   1 11   6.2 310 .66 0     1 3.8  2.2  250 0   .13   1 .62  .61  20 .078 0      -
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-read.c 1 2.9 1.3 250 25 0   0     1 4.2  2.3  240 0   0   1 7.4 4.2 310 .66 0     1 3.7  2.2  250 0   .13   1 .62  .62  20 .070 0      -
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-write.c 1 2.8 1.2 240 27 0   0     1 3.8  2.1  250 0   0   1 7.4 4.2 310 .66 0     1 3.9  2.3  250 0   .13   1 .62  .62  20 .070 0      -
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c 1 9.6 2.7 440 80 0   0     1 13    6.8  550 0   0   0 97   62   6400 1.5  0     1 17    9.1  630 0   0      1 1.0   1.0   35 .094 0      -
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-write.c 1 9.7 2.7 490 89 0   0     1 17    8.6  600 0   0   0 95   65   7000 1.5  0     1 13    6.7  680 0   0      1 1.1   1.1   34 .094 0      -
ldv-memsafety/memset2_false-valid-deref-write.c 1 2.7 1.2 250 25 0   0     1 3.9  2.2  240 0   0   -32 6.7 3.9 300 .62 0     0 3.6  2.1  240 0   0      1 .60  .60  20 .049 0      -
ldv-memsafety/memset3_false-valid-deref-write.c 1 2.7 1.2 250 22 0   0     1 3.4  1.9  240 0   0   -32 6.9 4.3 300 .62 0     0 3.9  2.3  250 0   0      1 .59  .59  20 .049 0      -
ldv-memsafety/memsetNonZero2_false-valid-deref-write.c 1 2.9 1.3 240 23 0   0     1 4.0  2.2  240 0   0   -32 6.7 3.8 300 .66 0     0 3.6  2.1  250 0   0      1 .59  .59  20 .049 0      -
ldv-memsafety/memsetNonZero3_false-valid-deref-write.c 1 2.9 1.3 250 27 0   0     1 3.6  2.0  250 0   0   -32 6.7 4.3 300 .62 0     0 4.0  2.3  250 0   0      1 .58  .58  20 .049 0      -
ldv-memsafety/memsetNonZero_false-valid-deref-write.c 1 2.8 1.2 240 26 0   0     1 3.4  2.0  240 0   0   -32 6.9 3.9 300 .66 0     0 3.9  2.3  250 0   0      1 .60  .60  20 .049 0      -
ldv-memsafety/memset_false-valid-deref-write.c 1 2.7 1.2 250 27 0   0     1 4.0  2.2  240 0   0   -32 6.5 3.7 300 .62 0     0 3.7  2.1  240 0   0      1 .59  .59  20 .049 0      -
ldv-memsafety/ArraysOfVariableLength2_true-valid-memsafety.c 2 92   50   4700 960 0   0     - - - - 0 960     910     2400   1.6  0  
ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c 2 9.6 4.5 700 100 0   0     - - - - 2 35     26     580   .62 0  
ldv-memsafety/ArraysOfVariableLength5_true-valid-memsafety.c 2 7.6 2.3 470 69 0   0     - - - - 2 24     15     580   .62 0  
ldv-memsafety/ArraysOfVariableLength6_true-valid-memsafety_true-termination.c 2 9.6 4.2 790 88 0   0     - - - - 2 20     13     590   .66 0  
ldv-memsafety/ArraysOfVariableLength_true-valid-memsafety.c 2 50   26   3800 460 0   0     - - - - 2 23     13     500   .62 0  
ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety_true-termination.c 2 7.6 2.3 470 68 0   0     - - - - 2 23     13     590   .66 0  
ldv-memsafety/StructInitialization1_true-valid-memsafety.c 2 3.2 1.3 270 26 0   0     - - - - 2 12     6.6   350   .62 0  
ldv-memsafety/StructInitialization2_true-valid-memsafety.c 2 3.3 1.3 270 30 0   0     - - - - 2 12     6.8   350   .62 0  
ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c 2 3.0 1.2 270 28 0   0     - - - - 2 8.0   4.3   310   .66 0  
ldv-memsafety/memset2_true-valid-memsafety_true-termination.c 2 2.7 1.2 240 25 0   0     - - - - 2 12     7.0   340   .66 0  
ldv-memsafety/memset3_true-valid-memsafety_true-termination.c 2 2.7 1.2 250 23 0   0     - - - - 2 10     6.3   330   .66 0  
ldv-memsafety/memsetNonZero2_true-valid-memsafety_true-termination.c 2 2.7 1.2 240 25 0   0     - - - - 2 11     6.6   320   .66 0  
ldv-memsafety/memsetNonZero3_true-valid-memsafety_true-termination.c 2 2.7 1.2 250 23 0   0     - - - - 2 12     7.2   340   .66 0  
ldv-memsafety/memsetNonZero_true-valid-memsafety_true-termination.c 2 2.8 1.2 240 27 0   0     - - - - 2 13     7.6   330   .66 0  
ldv-memsafety/memset_true-valid-memsafety_true-termination.c 2 2.7 1.2 240 23 0   0     - - - - 2 12     7.3   330   .66 0  
ldv-memsafety/memleaks_test14_3_false-valid-deref.i 1 4.4 1.5 290 40 0   0     1 6.6  3.5  280 0   0   0 12   7.1 290 .71 0     0 5.1  3.0  260 0   0      0 .57  .60  20 .025 0      -
ldv-memsafety/memleaks_test22_3_false-valid-deref.i 1 4.8 1.6 290 43 0   0     1 5.3  2.8  260 0   0   -32 14   7.8 450 .66 0     0 5.4  3.1  260 0   0      0 .58  .58  21 .025 0      -
ldv-memsafety/memleaks_test22_5_false-valid-deref.i 1 4.8 1.6 290 42 0   0     1 6.2  3.3  260 0   0   -32 13   7.6 460 .66 0     0 5.5  3.1  270 0   0      0 .57  .57  21 .025 0      -
ldv-memsafety/memleaks_test23_2_false-valid-deref.i 1 5.3 1.7 290 46 0   0     1 5.3  2.8  260 0   0   -32 18   10   440 .71 0     0 5.4  3.2  270 0   0      0 .61  .61  21 .029 0      -
ldv-memsafety/memleaks_test23_4_false-valid-deref.i 1 5.1 1.7 290 44 0   0     1 5.5  2.9  280 0   0   -32 20   12   500 .62 0     0 5.1  3.0  270 0   0      0 .57  .57  21 .029 .033  -
ldv-memsafety/memleaks_test11_1_false-valid-free.i 1 4.5 1.6 290 43 0   0     1 6.6  3.6  260 0   0   -32 14   8.0 370 .62 0     0 5.5  3.2  270 0   3.1    0 .58  .58  21 .025 0      -
ldv-memsafety/memleaks_test12_false-valid-free.i 1 5.6 1.8 290 45 0   0     1 6.7  3.6  280 0   0   -32 13   7.0 430 .62 0     0 7.7  4.4  280 0   .016  0 .59  .59  21 .029 0      -
ldv-memsafety/memleaks_test17_2_false-valid-free.i 1 5.5 1.8 300 51 0   0     1 6.5  3.5  280 0   0   0 80   53   7000 .72 .033 0 6.7  3.8  300 0   0      0 .61  .62  22 .025 0      -
ldv-memsafety/memleaks_test19_false-valid-free.i 1 4.7 1.6 290 44 0   0     1 5.1  2.7  260 0   0   0 97   89   560 1.1  0     0 5.1  3.0  260 0   0      0 .58  .58  21 .025 0      -
ldv-memsafety/memleaks_test1_false-valid-free.i 1 4.1 1.5 290 39 0   0     1 4.9  2.6  250 0   0   1 13   7.7 390 .66 0     0 5.0  2.9  260 0   0      0 .61  .61  20 .025 0      -
ldv-memsafety/memleaks_test3_false-valid-free.i 1 4.3 1.5 290 38 0   0     1 5.6  3.0  250 0   0   1 11   5.9 350 .66 0     0 4.8  2.7  260 0   .070  0 .60  .61  20 .025 0      -
ldv-memsafety/memleaks_test6_2_false-valid-free.i 1 4.3 1.5 280 39 0   0     1 5.8  3.1  280 0   0   1 15   8.6 520 .66 0     0 5.3  3.0  270 0   0      0 .57  .57  20 .025 0      -
ldv-memsafety/memleaks_test8_2_false-valid-free.i 1 4.2 1.5 260 40 0   0     1 5.3  2.9  250 0   0   1 12   7.0 400 .66 0     0 5.1  3.0  260 0   0      0 .60  .60  20 .025 0      -
ldv-memsafety/memleaks_test10_false-valid-memtrack_true-termination.i 1 4.4 1.6 290 41 0   0     1 5.4  2.9  260 0   0   0 27   16   480 .71 0     0 5.3  3.1  260 0   0      0 .60  .60  21 .025 0      -
ldv-memsafety/memleaks_test11_2_false-valid-memtrack_true-termination.i 1 4.8 1.7 290 40 0   0     1 6.4  3.5  260 0   0   -32 11   6.2 350 .62 0     0 6.5  3.7  270 0   0      0 .60  .60  21 .025 .033  -
ldv-memsafety/memleaks_test13_1_false-valid-memtrack_true-termination.i 1 4.4 1.5 280 40 0   0     1 4.9  2.7  250 0   0   0 39   26   570 .71 0     0 6.1  3.6  260 0   0      0 .58  .58  20 .025 0      -
ldv-memsafety/memleaks_test13_2_false-valid-memtrack.i 1 4.7 1.6 290 36 0   0     1 5.3  2.8  250 0   0   0 42   28   630 .68 0     0 4.8  2.8  260 0   0      0 .59  .59  20 .025 0      -
ldv-memsafety/memleaks_test14_1_false-valid-memtrack_true-termination.i 1 4.3 1.5 290 39 0   0     1 4.9  2.7  250 0   0   0 13   7.1 300 .71 0     0 5.1  2.9  260 0   3.0    0 .57  .57  20 .025 0      -
ldv-memsafety/memleaks_test14_2_false-valid-memtrack.i 1 4.6 1.6 290 43 0   0     1 5.7  3.1  260 0   0   0 13   6.8 290 .75 0     0 4.9  2.9  260 0   0      0 .57  .57  21 .025 0      -
ldv-memsafety/memleaks_test15_false-valid-memtrack.i 1 4.8 1.6 290 41 0   0     1 5.8  3.2  260 0   0   -32 13   7.0 450 .62 0     0 6.2  3.6  290 0   0      0 .58  .58  21 .029 0      -
ldv-memsafety/memleaks_test16_1_false-valid-memtrack_true-termination.i 1 4.3 1.5 290 38 0   0     1 5.2  2.8  260 0   0   0 21   13   380 .75 0     0 5.5  3.2  260 0   0      0 .59  .59  20 .025 .033  -
ldv-memsafety/memleaks_test16_2_false-valid-memtrack_true-termination.i 1 4.2 1.5 290 39 0   0     1 5.0  2.7  260 0   0   0 22   12   370 .68 0     0 6.0  3.5  260 0   3.1    0 .58  .58  20 .025 0      -
ldv-memsafety/memleaks_test17_1_false-valid-memtrack.i 1 5.5 1.7 290 47 0   0     1 6.8  3.6  270 0   0   0 76   51   7000 1.2  0     0 6.4  3.6  290 0   0      0 .62  .62  22 .025 .033  -
ldv-memsafety/memleaks_test17_3_false-valid-memtrack.i 1 5.3 1.7 300 46 0   0     1 7.1  3.8  280 0   0   -32 19   11   530 .62 0     0 6.2  3.5  280 0   0      0 .59  .59  21 .025 .033  -
ldv-memsafety/memleaks_test18_1_false-valid-memtrack_true-termination.i 1 4.9 1.7 280 40 0   0     1 6.6  3.6  260 0   0   -32 12   7.0 360 .62 0     0 6.2  3.5  290 0   0      0 .58  .58  21 .025 0      -
ldv-memsafety/memleaks_test18_2_false-valid-memtrack_true-termination.i 1 5.3 1.7 290 46 0   0     1 6.0  3.2  270 0   0   -32 12   6.8 370 .62 0     0 5.6  3.2  270 0   0      0 .62  .62  21 .025 0      -
ldv-memsafety/memleaks_test18_3_false-valid-memtrack_true-termination.i 1 5.2 1.7 300 48 0   0     1 6.0  3.2  270 0   0   -32 11   6.4 360 .66 0     0 5.7  3.2  280 0   0      0 .59  .59  21 .025 0      -
ldv-memsafety/memleaks_test1_false-valid-memtrack_true-termination.i 1 4.3 1.6 280 36 0   0     1 4.8  2.6  250 0   0   0 21   12   360 .75 0     0 5.0  2.9  260 0   0      0 .59  .59  20 .025 0      -
ldv-memsafety/memleaks_test20_false-valid-memtrack_true-termination.i 1 4.4 1.5 290 35 0   0     1 5.0  2.7  250 0   0   0 22   12   380 .68 0     0 4.7  2.8  260 0   .41   0 .59  .61  21 .025 0      -
ldv-memsafety/memleaks_test21_false-valid-memtrack_true-termination.i 1 4.3 1.5 280 41 0   0     1 4.7  2.6  250 0   0   0 23   14   380 .68 0     0 4.8  2.8  260 0   0      0 .57  .58  20 .025 0      -
ldv-memsafety/memleaks_test22_1_false-valid-memtrack_true-termination.i 1 4.6 1.6 290 37 0   0     1 5.7  3.1  260 0   0   -32 13   7.3 440 .66 0     0 5.2  2.9  260 0   0      0 .60  .60  21 .025 0      -
ldv-memsafety/memleaks_test22_2_false-valid-memtrack_true-termination.i 1 4.0 1.5 270 37 0   0     1 4.9  2.7  250 0   0   -32 15   8.1 470 .62 0     0 4.9  2.8  260 0   0      0 .58  .58  20 .025 0      -
ldv-memsafety/memleaks_test22_4_false-valid-memtrack_true-termination.i 1 4.6 1.6 290 47 0   0     1 6.1  3.3  290 0   0   -32 12   6.7 450 .62 0     0 5.4  3.1  290 0   0      0 .57  .57  21 .025 0      -
ldv-memsafety/memleaks_test4_false-valid-memtrack_true-termination.i 1 4.3 1.5 290 41 0   0     1 6.0  3.3  260 0   0   0 22   12   380 .71 0     0 4.9  2.8  250 0   0      0 .60  .62  20 .025 0      -
ldv-memsafety/memleaks_test5_1_false-valid-memtrack_true-termination.i 1 4.2 1.5 290 40 0   0     1 5.5  3.0  250 0   0   0 21   13   370 .71 0     0 5.0  3.0  260 0   0      0 .56  .56  20 .025 .029  -
ldv-memsafety/memleaks_test5_2_false-valid-memtrack_true-termination.i 1 4.2 1.5 280 39 0   0     1 5.1  2.8  250 0   0   -32 13   7.7 400 .62 0     0 4.6  2.7  250 0   0      0 .57  .57  20 .025 .029  -
ldv-memsafety/memleaks_test6_1_false-valid-memtrack_true-termination.i 1 4.3 1.5 290 37 0   0     1 5.0  2.7  250 0   0   0 69   55   520 .71 0     0 4.9  2.9  260 0   0      0 .57  .57  20 .025 0      -
ldv-memsafety/memleaks_test6_3_false-valid-memtrack_true-termination.i 1 4.4 1.5 290 43 0   0     1 5.3  2.8  270 0   0   0 24   14   430 .68 0     0 4.8  2.8  260 0   0      0 .58  .58  21 .025 0      -
ldv-memsafety/memleaks_test7_false-valid-memtrack_true-termination.i 1 4.5 1.6 290 36 0   0     1 5.2  2.8  260 0   0   0 23   13   410 .68 0     0 5.1  2.9  260 0   0      0 .58  .58  20 .025 0      -
ldv-memsafety/memleaks_test8_1_false-valid-memtrack_true-termination.i 1 4.3 1.5 290 39 0   0     1 5.0  2.7  260 0   0   0 23   13   380 .71 0     0 4.8  2.8  250 0   0      0 .60  .60  20 .025 0      -
ldv-memsafety/memleaks_test9_1_false-valid-memtrack_true-termination.i 1 4.2 1.5 280 40 0   0     1 5.8  3.1  250 0   0   0 21   12   380 .68 0     0 5.0  2.9  260 0   0      0 .61  .61  21 .025 0      -
ldv-memsafety/memleaks_test9_2_false-valid-memtrack_true-termination.i 1 4.1 1.5 270 41 0   0     1 4.9  2.7  250 0   0   0 22   12   380 .71 0     0 4.8  2.8  260 0   0      0 .57  .57  20 .025 0      -
ldv-memsafety/memleaks_test10_true-valid-memsafety_true-termination.i 2 4.5 1.5 290 44 0   0     - - - - 0 960     920     820   .72 0  
ldv-memsafety/memleaks_test11_true-valid-memsafety_true-termination.i 2 4.8 1.6 290 44 0   0     - - - - 0 960     900     960   .72 0  
ldv-memsafety/memleaks_test12_true-valid-memsafety.i 2 6.1 1.9 300 50 0   0     - - - - 0 960     900     1800   .74 0  
ldv-memsafety/memleaks_test13_true-valid-memsafety.i 2 4.6 1.6 280 44 0   0     - - - - 2 94     65     910   .62 0  
ldv-memsafety/memleaks_test14_true-valid-memsafety.i 2 4.4 1.5 290 41 0   0     - - - - 0 13     7.0   290   .75 0  
ldv-memsafety/memleaks_test15_true-valid-memsafety_true-termination.i 2 4.8 1.6 290 42 0   0     - - - - 0 960     920     1100   .63 0  
ldv-memsafety/memleaks_test16_true-valid-memsafety_true-termination.i 2 4.4 1.5 290 36 0   0     - - - - 2 15     8.7   530   .62 0  
ldv-memsafety/memleaks_test17_1_true-valid-memsafety_true-termination.i 2 5.8 1.8 300 47 0   0     - - - - 0 960     900     2200   .70 0  
ldv-memsafety/memleaks_test17_2_true-valid-memsafety_true-termination.i 0 4.6 1.6 290 44 0   0     - - - - 0 960     890     1200   .66 0  
ldv-memsafety/memleaks_test18_true-valid-memsafety_true-termination.i 2 5.4 1.7 300 48 0   0     - - - - 0 960     930     1100   .65 0  
ldv-memsafety/memleaks_test19_true-valid-memsafety_true-termination.i 2 4.2 1.5 270 40 0   0     - - - - 0 960     910     830   1.7  0  
ldv-memsafety/memleaks_test1_true-valid-memsafety_true-termination.i 2 4.2 1.5 280 37 0   0     - - - - 2 13     7.5   450   .66 0  
ldv-memsafety/memleaks_test20_true-valid-memsafety_true-termination.i 2 4.4 1.6 290 41 0   0     - - - - 2 15     9.0   480   .62 0  
ldv-memsafety/memleaks_test21_true-valid-memsafety_true-termination.i 2 4.5 1.6 290 43 0   0     - - - - 2 13     8.1   530   .66 0  
ldv-memsafety/memleaks_test22_1_true-valid-memsafety_true-termination.i 2 4.5 1.6 280 40 0   0     - - - - 0 960     900     2700   .71 0  
ldv-memsafety/memleaks_test22_2_true-valid-memsafety_true-termination.i 2 4.8 1.6 290 41 0   0     - - - - 0 960     890     2300   .70 0  
ldv-memsafety/memleaks_test22_3_true-valid-memsafety_true-termination.i 2 4.8 1.7 290 36 0   0     - - - - 0 960     920     3900   .64 0  
ldv-memsafety/memleaks_test23_1_true-valid-memsafety.i 2 5.3 1.7 290 45 0   0     - - - - -16 170     150     720   .71 0  
ldv-memsafety/memleaks_test23_3_true-valid-memsafety.i 2 5.2 1.7 290 43 0   0     - - - - 0 960     890     2700   .73 0  
ldv-memsafety/memleaks_test3_true-valid-memsafety_true-termination.i 2 4.3 1.5 290 38 0   0     - - - - 2 14     8.3   480   .66 0  
ldv-memsafety/memleaks_test4_true-valid-memsafety_true-termination.i 2 4.4 1.6 290 39 0   0     - - - - 2 35     25     540   .66 0  
ldv-memsafety/memleaks_test5_true-valid-memsafety_true-termination.i 2 4.4 1.5 280 39 0   0     - - - - 2 16     9.6   520   .62 0  
ldv-memsafety/memleaks_test6_true-valid-memsafety_true-termination.i 2 4.4 1.5 290 39 0   0     - - - - 2 27     16     500   .66 0  
ldv-memsafety/memleaks_test7_true-valid-memsafety_true-termination.i 2 4.5 1.5 290 39 0   0     - - - - 2 22     13     550   .62 0  
ldv-memsafety/memleaks_test8_true-valid-memsafety_true-termination.i 2 4.3 1.5 290 41 0   0     - - - - 2 13     7.7   460   .66 0  
ldv-memsafety/memleaks_test9_true-valid-memsafety_true-termination.i 2 4.2 1.5 290 36 0   0     - - - - 2 14     8.0   480   .66 0  
ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety_true-termination.i 2 3.3 1.3 270 28 0   0     - - - - 0 10     6.0   280   .70 0  
ldv-memsafety-bitfields/test-bitfields-2.1_true-valid-memsafety_true-termination.i 2 3.0 1.2 270 26 0   0     - - - - 0 11     6.5   290   .74 0  
ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety_true-termination.i 2 3.2 1.2 270 29 0   0     - - - - 0 10     6.3   270   .74 0  
ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i 2 3.1 1.2 270 31 0   0     - - - - 0 11     6.3   270   .74 0  
ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i 2 3.2 1.3 280 27 0   0     - - - - 0 11     5.7   280   .73 0  
ldv-memsafety-bitfields/test-bitfields-1_false-valid-deref.i 1 3.2 1.2 260 29 0   0     1 4.0  2.2  250 0   0   0 10   5.5 260 .73 0     1 4.2  2.4  270 0   2.9    1 .61  .61  20 .053 0      -
ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i 1 3.2 1.3 270 29 0   0     1 3.8  2.1  250 0   0   0 10   5.9 280 .70 0     0 3.7  2.2  250 0   0      -32 .60  .62  20 .053 0      -
ldv-memsafety-bitfields/test-bitfields-3.1_false-valid-deref.i 1 2.7 1.2 250 27 0   .029 1 4.4  2.4  240 0   0   0 11   5.8 290 .66 0     0 3.8  2.1  240 0   0      -32 .60  .60  20 .061 0      -
ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i 1 3.1 1.2 270 28 0   0     1 4.5  2.5  240 0   0   0 11   6.0 290 .73 0     0 3.7  2.2  240 0   0      1 .60  .62  20 .061 0      -
ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i 1 3.1 1.3 270 29 0   0     1 3.9  2.2  250 0   0   0 11   6.3 290 .67 0     0 4.0  2.3  250 0   0      1 .59  .61  20 .053 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 180 183 46000 28000 410000 400000 0   .029 90 73 440 240 22000 0   0   90 -741 3300 2300 96000 77    .049 90 7 440 250 22000 0   16   90 -206 47   47   1700 3.0  .34  90 46 44000 41000 99000 67    0  
    correct results 128 183 770 300 49000 7000 0   .029 73 73 430 230 21000 0   0   11 11 120 70 4000 7.1  0     7 7 49 27 2600 0   6.5 18 18 12   12   400 1.2  .037 31 62 610 380 15000 20    0  
        correct true 55 110 440 180 27000 4000 0   0     0 0 0 0 31 62 610 380 15000 20    0  
        correct false 73 73 330 120 22000 3000 0   .029 73 73 430 230 21000 0   0   11 11 120 70 4000 7.1  0     7 7 49 27 2600 0   6.5 18 18 12   12   400 1.2  .037 0
    incorrect results 0 0 24 -752 310 180 10000 15    0     0 7 -224 4.5 4.5 140 .48 .025 1 -16 170 150 720 .71 0  
        incorrect true 0 0 23 -736 280 160 9000 15    0     0 7 -224 4.5 4.5 140 .48 .025 0
        incorrect false 0 0 1 -16 37 19 1200 .62 0     0 0 1 -16 170 150 720 .71 0  
score (180 tasks, max score: 270) 183 73 -741 7 -206 46
Run set pesco.sv-comp19_prop-memsafety.MemSafety-Heap cpa-seq-validate-violation-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-Heap uautomizer-validate-violation-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-Heap cpa-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-Heap fshell-witness2test-validate-violation-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-Heap uautomizer-validate-correctness-witnesses-pesco.sv-comp19_prop-memsafety.MemSafety-Heap