Tool DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CProver witness2test 0.1 ULTIMATE Automizer 0.1.23-3204b741
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* [apollon023; apollon077; apollon078; apollon117; apollon126] [apollon077; apollon078; apollon101; apollon157] [apollon045; apollon077; apollon078; apollon158] [apollon007; apollon009; apollon077; apollon078; apollon119]
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 33553 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-01 09:05:19 CET 2017-12-01 09:58:48 CET 2017-12-01 10:19:41 CET 2017-12-01 10:22:00 CET 2017-12-01 10:02:39 CET
Run set depthk.sv-comp18.MemSafety-Heap cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.MemSafety-Heap uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.MemSafety-Heap fshell-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.MemSafety-Heap uautomizer-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.MemSafety-Heap
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-12-01_0905.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -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 --full-output --validate ../../results-verified/depthk.2017-12-01_0905.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/depthk.2017-12-01_0905.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/depthk.2017-12-01_0905.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
memsafety/960521-1_false-valid-deref.i unknown 0 wit inspect 110    75 1300   error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0033 .29 - wit inspect
memsafety/test-0137_false-valid-deref.i false(valid-deref) 0 wit inspect .53 29 5.9 timeout 0 wit inspect 91    2400 true -32 wit inspect 4.3   270   error (2) 0 wit inspect .64   18    - wit inspect
memsafety/test-0235_false-valid-deref.i unknown 0 wit inspect 610    510 4900   error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .017 4.9 error (invalid witness file) 0 wit inspect .0011 .35 - wit inspect
memsafety/960521-1_false-valid-free.i unknown 0 wit inspect 110    77 1400   error (invalid witness file) 0 wit inspect .60 45 error (2) 0 wit inspect .017 4.8 error (invalid witness file) 0 wit inspect .0040 .26 - wit inspect
memsafety/test-0158_false-valid-free.i false(valid-deref) -16 wit inspect 16    490 120   true -32 wit inspect 2.3  250 true -32 wit inspect 3.7   260   error (1) 0 wit inspect .60   18    - wit inspect
memsafety/test-0232_false-valid-free.i false(valid-deref) -16 wit inspect 1.4  28 17   timeout 0 wit inspect 92    1600 true -32 wit inspect 3.9   250   true -32 wit inspect .64   18    - wit inspect
memsafety/20020406-1_false-valid-memtrack.i unknown 0 wit inspect 900    4800 6400   error (invalid witness file) 0 wit inspect .41 44 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .0036 .27 - wit inspect
memsafety/20051113-1.c_false-valid-memtrack.i unknown 0 wit inspect 530    170 7100   error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0022 .29 - wit inspect
memsafety/lockfree-3.1_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 7.3  39 92   timeout 0 wit inspect 92    2300 true -32 wit inspect 5.2   250   error (2) 0 wit inspect .66   18    - wit inspect
memsafety/lockfree-3.2_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 1.2  29 14   timeout 0 wit inspect 92    2300 true -32 wit inspect 5.7   240   error (2) 0 wit inspect .67   18    - wit inspect
memsafety/lockfree-3.3_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 39    76 550   timeout 0 wit inspect 92    2300 true -32 wit inspect 4.0   250   error (2) 0 wit inspect .65   19    - wit inspect
memsafety/test-0019_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .54 28 6.4 error (invalid witness file) 0 wit inspect 2.5  170 true -32 wit inspect 5.5   280   error (255) 0 wit inspect .59   18    - wit inspect
memsafety/test-0102_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 11    110 120   error (invalid witness file) 0 wit inspect 1.8  180 true -32 wit inspect 4.1   250   false(valid-deref) -16 wit inspect .66   18    - wit inspect
memsafety/test-0158_false-valid-memtrack_true-termination.i false(valid-memtrack) 1 wit inspect .46 28 4.7 false(valid-memtrack) 1 wit inspect 2.6  250 true -32 wit inspect 3.6   260   true -32 wit inspect .63   18    - wit inspect
memsafety/test-0220_false-valid-memtrack.i unknown 0 wit inspect 900    8300 7000   error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect
memsafety/test-0232_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .58 28 6.8 timeout 0 wit inspect 91    1700 true -32 wit inspect 3.9   250   true -32 wit inspect .65   18    - wit inspect
memsafety/test-0234_false-valid-memtrack.i unknown 0 wit inspect 620    510 4500   error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect
memsafety/test-0235_false-valid-memtrack.i unknown 0 wit inspect 620    510 5000   error (invalid witness file) 0 wit inspect .43 41 error (2) 0 wit inspect .048 4.9 error (invalid witness file) 0 wit inspect .0011 .30 - wit inspect
memsafety/960521-1_true-valid-memsafety.i unknown 0 wit inspect 110    72 1500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .026 4.8
memsafety/lockfree-3.0_true-valid-memsafety.i unknown 0 wit inspect 900    170 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
memsafety/test-0019_true-valid-memsafety_true-termination.i true 2 wit inspect .83 28 9.5 - wit inspect - wit inspect - wit inspect true 2 wit inspect 27     520  
memsafety/test-0102_true-valid-memsafety.i unknown 0 wit inspect 890    550 8700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
memsafety/test-0134_true-valid-memsafety.i unknown 0 wit inspect 890    290 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
memsafety/test-0158_true-valid-memsafety_true-termination.i true 2 wit inspect .88 28 12   - wit inspect - wit inspect - wit inspect true 2 wit inspect 17     400  
memsafety/test-0214_true-valid-memsafety_false-termination.i unknown 0 wit inspect 890    1900 5700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
memsafety/test-0217_true-valid-memsafety_false-termination.i unknown 0 wit inspect 890    1800 5100   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
memsafety/test-0218_true-valid-memsafety_false-termination.i unknown 0 wit inspect 890    1800 5200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .062 4.8
memsafety/test-0219_true-valid-memsafety.i unknown 0 wit inspect 900    8500 5700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
memsafety/test-0232_true-valid-memsafety.i unknown 0 wit inspect 890    260 9600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
memsafety/test-0234_true-valid-memsafety.i unknown 0 wit inspect 620    510 5500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
memsafety/test-0235_true-valid-memsafety.i unknown 0 wit inspect 590    510 6100   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
memsafety/test-0236_true-valid-memsafety.i unknown 0 wit inspect 710    510 5300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
memsafety/test-0237_true-valid-memsafety.i unknown 0 wit inspect 620    510 5900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
memsafety/test-0504_true-valid-memsafety.i unknown 0 wit inspect 890    380 8400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
memsafety/test-0513_true-valid-memsafety.i unknown 0 wit inspect 890    250 9100   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
memsafety/test-0521_true-valid-memsafety.i unknown 0 wit inspect 890    760 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.9
memsafety/test-memleak_nexttime_true-valid-memsafety_true-termination.i unknown 0 wit inspect 890    630 7300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
memsafety-ext/dll_extends_pointer_true-valid-memsafety.i unknown 0 wit inspect 890    210 7500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
memsafety-ext/skiplist_2lvl_true-valid-memsafety.i unknown 0 wit inspect 890    93 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
memsafety-ext/skiplist_3lvl_true-valid-memsafety.i unknown 0 wit inspect 890    110 9500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
memsafety-ext/tree_cnstr_true-valid-memsafety_false-termination.i unknown 0 wit inspect 890    160 13000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
memsafety-ext/tree_dsw_true-valid-memsafety_false-termination.i unknown 0 wit inspect 890    270 10000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
memsafety-ext/tree_of_cslls_true-valid-memsafety.i unknown 0 wit inspect 890    520 9600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
memsafety-ext/tree_parent_ptr_true-valid-memsafety_false-termination.i unknown 0 wit inspect 890    300 10000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
memsafety-ext/tree_stack_true-valid-memsafety_false-termination.i unknown 0 wit inspect 890    340 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
memsafety-ext2/split_list_test05_false-valid-deref.i unknown 0 wit inspect 900    15000 10000   error (invalid witness file) 0 wit inspect .41 42 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0010 .26 - wit inspect
memsafety-ext2/complex_data_creation_test01_false-valid-memtrack.i unknown 0 wit inspect 890    550 8200   error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0011 .33 - wit inspect
memsafety-ext2/complex_data_creation_test02_false-valid-memtrack.i unknown 0 wit inspect 890    490 8000   error (invalid witness file) 0 wit inspect .42 44 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .0029 .29 - wit inspect
memsafety-ext2/length_test03_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 10    48 130   timeout 0 wit inspect 91    1500 true -32 wit inspect 4.1   250   true -32 wit inspect .66   18    - wit inspect
memsafety-ext2/optional_data_creation_test04_false-valid-memtrack.i false(valid-deref) -16 wit inspect .81 29 9.7 timeout 0 wit inspect 92    2700 true -32 wit inspect 4.1   250   false(valid-deref) -16 wit inspect .69   18    - wit inspect
memsafety-ext2/complex_data_creation_test01_true-valid-memsafety.i unknown 0 wit inspect 890    590 6400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
memsafety-ext2/complex_data_creation_test02_true-valid-memsafety.i unknown 0 wit inspect 890    500 6900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
memsafety-ext2/length_test03_true-valid-memsafety.i unknown 0 wit inspect 890    200 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
memsafety-ext2/optional_data_creation_test04_true-valid-memsafety.i false(valid-deref) -16 wit inspect .82 29 10   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7   250  
memsafety-ext2/split_list_test05_true-valid-memsafety.i unknown 0 wit inspect 900    15000 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
list-ext-properties/960521-1_1_false-valid-deref.i false(valid-deref) 0 wit inspect 1.5  29 19   true -32 wit inspect 9.7  800 true -32 wit inspect 4.4   270   error (2) 0 wit inspect .66   18    - wit inspect
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 1.3  30 16   true -32 wit inspect 14    670 true -32 wit inspect 4.0   270   false(valid-deref) 1 wit inspect .69   18    - wit inspect
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 1.3  29 18   false(valid-deref) 1 wit inspect 4.3  250 true -32 wit inspect 4.5   270   false(valid-deref) 1 wit inspect .69   18    - wit inspect
list-ext-properties/960521-1_1_false-valid-free.i unknown 0 wit inspect 1.5  28 19   true -32 wit inspect 13    780 true -32 wit inspect 4.4   270   false(valid-free) 1 wit inspect .65   18    - wit inspect
list-ext-properties/test-0158_1_false-valid-free.i false(valid-deref) -16 wit inspect .54 28 8.5 false(valid-free) 1 wit inspect 4.3  250 true -32 wit inspect 6.0   270   error (2) 0 wit inspect .66   18    - wit inspect
list-ext-properties/test-0019_1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .52 28 7.6 error (invalid witness file) 0 wit inspect 2.8  180 true -32 wit inspect 9.4   530   error (255) 0 wit inspect .61   19    - wit inspect
list-ext-properties/test-0158_1_false-valid-memtrack_true-termination.i false(valid-memtrack) 1 wit inspect .45 28 5.9 false(valid-memtrack) 1 wit inspect 2.6  260 true -32 wit inspect 5.5   260   true -32 wit inspect .66   18    - wit inspect
list-ext-properties/test-0232_1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .57 28 7.1 true -32 wit inspect 7.5  360 true -32 wit inspect 5.5   250   true -32 wit inspect .65   18    - wit inspect
list-ext-properties/960521-1_1_true-valid-memsafety.i unknown 0 wit inspect 890    110 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
list-ext-properties/list-ext_1_true-valid-memsafety.i unknown 0 wit inspect 890    210 9700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
list-ext-properties/list-ext_flag_1_true-valid-memsafety.i unknown 0 wit inspect 890    200 8300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
list-ext-properties/simple-ext_1_true-valid-memsafety.i unknown 0 wit inspect 890    190 8700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
list-ext-properties/test-0019_1_true-valid-memsafety_true-termination.i true 2 wit inspect .87 28 12   - wit inspect - wit inspect - wit inspect true 2 wit inspect 150     790  
list-ext-properties/test-0158_1_true-valid-memsafety_true-termination.i true 2 wit inspect 1.1  28 14   - wit inspect - wit inspect - wit inspect true 2 wit inspect 12     380  
list-ext-properties/test-0214_1_true-valid-memsafety.i unknown 0 wit inspect 890    860 6900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 5.0
list-ext-properties/test-0217_1_true-valid-memsafety.i unknown 0 wit inspect 890    1100 6300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
list-ext-properties/test-0232_1_true-valid-memsafety_true-termination.i true 2 wit inspect 210    160 2200   - wit inspect - wit inspect - wit inspect error (7) 0 wit inspect 490     910  
list-ext-properties/test-0504_1_true-valid-memsafety.i unknown 0 wit inspect 890    440 8800   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
list-ext-properties/test-0513_1_true-valid-memsafety.i unknown 0 wit inspect 890    2600 10000   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     710  
memory-alloca/c.03-alloca_true-valid-memsafety.i unknown 0 wit inspect 160    70 1900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.9
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c false(valid-deref) 0 wit inspect .40 28 4.8 true -32 wit inspect 2.1  250 true -32 wit inspect 5.9   270   error (2) 0 wit inspect .59   18    - wit inspect
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-write.c unknown 0 wit inspect .35 27 3.7 true -32 wit inspect 3.0  250 true -32 wit inspect 4.5   270   error (2) 0 wit inspect .62   18    - wit inspect
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-read.c unknown 0 wit inspect .37 27 4.1 true -32 wit inspect 2.0  240 true -32 wit inspect 4.5   260   error (2) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-write.c unknown 0 wit inspect .36 27 3.5 true -32 wit inspect 2.0  250 true -32 wit inspect 6.2   280   error (2) 0 wit inspect .61   18    - wit inspect
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c false(valid-deref) 0 wit inspect 590    570 6000   true -32 wit inspect 8.6  360 true -32 wit inspect 13     840   error (2) 0 wit inspect .82   22    - wit inspect
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-write.c unknown 0 wit inspect 640    570 7200   true -32 wit inspect 8.7  460 true -32 wit inspect 8.8   870   error (2) 0 wit inspect .79   22    - wit inspect
ldv-memsafety/memset2_false-valid-deref-write.c unknown 0 wit inspect 75    29 1100   error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
ldv-memsafety/memset3_false-valid-deref-write.c unknown 0 wit inspect 270    38 3100   error (invalid witness file) 0 wit inspect .41 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
ldv-memsafety/memsetNonZero2_false-valid-deref-write.c unknown 0 wit inspect 75    29 920   error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .0036 .29 - wit inspect
ldv-memsafety/memsetNonZero3_false-valid-deref-write.c unknown 0 wit inspect 270    38 4100   error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
ldv-memsafety/memsetNonZero_false-valid-deref-write.c unknown 0 wit inspect 270    38 3800   error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect
ldv-memsafety/memset_false-valid-deref-write.c unknown 0 wit inspect 270    38 3200   error (invalid witness file) 0 wit inspect .43 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0011 .29 - wit inspect
ldv-memsafety/ArraysOfVariableLength2_true-valid-memsafety.c unknown 0 wit inspect 900    1800 9100   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c unknown 0 wit inspect 900    620 6900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .065 4.9
ldv-memsafety/ArraysOfVariableLength5_true-valid-memsafety.c true 2 wit inspect 690    580 5400   - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.5   510  
ldv-memsafety/ArraysOfVariableLength6_true-valid-memsafety_true-termination.c unknown 0 wit inspect 900    680 9800   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
ldv-memsafety/ArraysOfVariableLength_true-valid-memsafety.c unknown 0 wit inspect 900    640 8800   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety_true-termination.c true 2 wit inspect 680    570 8400   - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.8   440  
ldv-memsafety/StructInitialization1_true-valid-memsafety.c true 2 wit inspect 3.9  250 37   - wit inspect - wit inspect - wit inspect error (7) 0 wit inspect 3.8   210  
ldv-memsafety/StructInitialization2_true-valid-memsafety.c true 2 wit inspect 3.8  250 42   - wit inspect - wit inspect - wit inspect error (7) 0 wit inspect 3.9   200  
ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c true 2 wit inspect 3.2  230 30   - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9   210  
ldv-memsafety/memset2_true-valid-memsafety_true-termination.c true 2 wit inspect 41    250 610   - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.2   290  
ldv-memsafety/memset3_true-valid-memsafety_true-termination.c true 2 wit inspect 230    250 2800   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4   290  
ldv-memsafety/memsetNonZero2_true-valid-memsafety_true-termination.c true 2 wit inspect 40    230 540   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5   290  
ldv-memsafety/memsetNonZero3_true-valid-memsafety_true-termination.c true 2 wit inspect 230    250 2900   - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.3   300  
ldv-memsafety/memsetNonZero_true-valid-memsafety_true-termination.c true 2 wit inspect 230    250 3000   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5   300  
ldv-memsafety/memset_true-valid-memsafety_true-termination.c true 2 wit inspect 230    240 2500   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5   300  
ldv-memsafety/memleaks_test14_3_false-valid-deref.i false(valid-deref) 0 wit inspect .81 35 11   true -32 wit inspect 4.4  260 true -32 wit inspect 5.8   250   error (1) 0 wit inspect .62   19    - wit inspect
ldv-memsafety/memleaks_test22_3_false-valid-deref.i false(valid-deref) 0 wit inspect 34    36 400   true -32 wit inspect 2.8  260 true -32 wit inspect 4.0   250   error (1) 0 wit inspect .59   18    - wit inspect
ldv-memsafety/memleaks_test22_5_false-valid-deref.i false(valid-deref) 0 wit inspect 34    35 450   true -32 wit inspect 2.8  260 true -32 wit inspect 5.9   260   error (1) 0 wit inspect .58   19    - wit inspect
ldv-memsafety/memleaks_test23_2_false-valid-deref.i false(valid-deref) 0 wit inspect 540    350 6200   error (invalid witness file) 0 wit inspect 3.3  180 true -32 wit inspect 6.4   290   error (1) 0 wit inspect .61   19    - wit inspect
ldv-memsafety/memleaks_test23_4_false-valid-deref.i false(valid-deref) 0 wit inspect 590    320 6600   error (invalid witness file) 0 wit inspect 3.3  220 true -32 wit inspect 4.9   290   error (1) 0 wit inspect .59   19    - wit inspect
ldv-memsafety/memleaks_test11_1_false-valid-free.i false(valid-deref) -16 wit inspect 1.6  35 23   true -32 wit inspect 4.8  250 true -32 wit inspect 56     530   error (1) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/memleaks_test12_false-valid-free.i unknown 0 wit inspect 260    210 3200   error (invalid witness file) 0 wit inspect .41 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0011 .34 - wit inspect
ldv-memsafety/memleaks_test17_2_false-valid-free.i unknown 0 wit inspect 890    320 12000   error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
ldv-memsafety/memleaks_test19_false-valid-free.i false(valid-deref) -16 wit inspect .73 30 9.2 true -32 wit inspect 2.7  260 true -32 wit inspect 3.6   250   error (1) 0 wit inspect .59   18    - wit inspect
ldv-memsafety/memleaks_test1_false-valid-free.i false(valid-deref) -16 wit inspect .54 30 5.9 true -32 wit inspect 2.5  250 true -32 wit inspect 5.0   240   error (1) 0 wit inspect .60   18    - wit inspect
ldv-memsafety/memleaks_test3_false-valid-free.i false(valid-deref) -16 wit inspect .41 30 4.3 false(valid-free) 1 wit inspect 2.8  260 true -32 wit inspect 4.6   230   error (1) 0 wit inspect .62   18    - wit inspect
ldv-memsafety/memleaks_test6_2_false-valid-free.i false(valid-deref) -16 wit inspect .57 30 6.5 true -32 wit inspect 2.6  260 true -32 wit inspect 6.5   430   error (1) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/memleaks_test8_2_false-valid-free.i false(valid-deref) -16 wit inspect .55 30 6.5 true -32 wit inspect 3.9  250 true -32 wit inspect 4.4   240   error (1) 0 wit inspect .59   18    - wit inspect
ldv-memsafety/memleaks_test10_false-valid-memtrack_true-termination.i false(valid-deref) -16 wit inspect .88 30 9.5 true -32 wit inspect 4.7  260 timeout 0 wit inspect 97     610   error (1) 0 wit inspect .61   18    - wit inspect
ldv-memsafety/memleaks_test11_2_false-valid-memtrack_true-termination.i false(valid-deref) -16 wit inspect 1.2  32 16   true -32 wit inspect 2.7  260 true -32 wit inspect 12     510   error (1) 0 wit inspect .62   18    - wit inspect
ldv-memsafety/memleaks_test13_1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .50 30 5.7 true -32 wit inspect 2.6  250 true -32 wit inspect 3.5   240   error (1) 0 wit inspect .63   18    - wit inspect
ldv-memsafety/memleaks_test13_2_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 4.3  44 47   true -32 wit inspect 2.7  250 true -32 wit inspect 4.3   270   error (1) 0 wit inspect .59   18    - wit inspect
ldv-memsafety/memleaks_test14_1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .48 30 6.5 true -32 wit inspect 4.5  250 true -32 wit inspect 7.4   280   error (1) 0 wit inspect .61   18    - wit inspect
ldv-memsafety/memleaks_test14_2_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 3.8  45 46   true -32 wit inspect 4.8  260 true -32 wit inspect 26     560   error (1) 0 wit inspect .63   18    - wit inspect
ldv-memsafety/memleaks_test15_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 78    82 1000   true -32 wit inspect 4.8  260 true -32 wit inspect 6.0   280   error (1) 0 wit inspect .63   19    - wit inspect
ldv-memsafety/memleaks_test16_1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .50 30 5.7 true -32 wit inspect 4.1  260 true -32 wit inspect 3.4   230   error (1) 0 wit inspect .59   18    - wit inspect
ldv-memsafety/memleaks_test16_2_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .50 30 5.5 true -32 wit inspect 2.6  250 true -32 wit inspect 3.5   250   error (1) 0 wit inspect .63   18    - wit inspect
ldv-memsafety/memleaks_test17_1_false-valid-memtrack.i unknown 0 wit inspect 890    260 10000   error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0025 .29 - wit inspect
ldv-memsafety/memleaks_test17_3_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 370    180 4900   true -32 wit inspect 3.5  260 true -32 wit inspect 10     440   error (1) 0 wit inspect .59   18    - wit inspect
ldv-memsafety/memleaks_test18_1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .52 30 6.2 true -32 wit inspect 3.2  250 true -32 wit inspect 10     370   error (1) 0 wit inspect .60   18    - wit inspect
ldv-memsafety/memleaks_test18_2_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect 600    160 7400   true -32 wit inspect 3.2  260 true -32 wit inspect 9.2   390   error (1) 0 wit inspect .60   18    - wit inspect
ldv-memsafety/memleaks_test18_3_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect 10    36 140   true -32 wit inspect 36    1700 true -32 wit inspect 6.9   390   error (1) 0 wit inspect .62   19    - wit inspect
ldv-memsafety/memleaks_test1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .46 30 6.5 true -32 wit inspect 2.5  250 true -32 wit inspect 4.5   230   error (1) 0 wit inspect .62   18    - wit inspect
ldv-memsafety/memleaks_test20_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .48 30 5.5 true -32 wit inspect 2.6  260 true -32 wit inspect 4.6   230   error (1) 0 wit inspect .59   18    - wit inspect
ldv-memsafety/memleaks_test21_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .49 30 5.5 true -32 wit inspect 2.7  270 true -32 wit inspect 4.8   240   error (1) 0 wit inspect .59   18    - wit inspect
ldv-memsafety/memleaks_test22_1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect 30    34 430   true -32 wit inspect 3.0  280 true -32 wit inspect 4.1   260   error (1) 0 wit inspect .61   18    - wit inspect
ldv-memsafety/memleaks_test22_2_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect 16    30 170   true -32 wit inspect 2.7  260 true -32 wit inspect 18     470   error (1) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/memleaks_test22_4_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect 30    34 380   true -32 wit inspect 2.8  260 true -32 wit inspect 4.1   250   error (1) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/memleaks_test4_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .53 30 6.4 true -32 wit inspect 2.6  260 true -32 wit inspect 3.5   230   error (1) 0 wit inspect .62   18    - wit inspect
ldv-memsafety/memleaks_test5_1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .47 30 5.3 true -32 wit inspect 2.5  250 true -32 wit inspect 3.2   230   error (1) 0 wit inspect .63   18    - wit inspect
ldv-memsafety/memleaks_test5_2_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .46 30 6.1 true -32 wit inspect 4.0  260 true -32 wit inspect 4.7   240   error (1) 0 wit inspect .63   18    - wit inspect
ldv-memsafety/memleaks_test6_1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .49 30 7.4 true -32 wit inspect 2.8  260 true -32 wit inspect 10     440   error (1) 0 wit inspect .59   19    - wit inspect
ldv-memsafety/memleaks_test6_3_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .50 30 6.0 true -32 wit inspect 4.1  250 true -32 wit inspect 4.8   280   error (1) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/memleaks_test7_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .51 30 5.9 true -32 wit inspect 4.1  260 true -32 wit inspect 3.5   240   error (1) 0 wit inspect .60   18    - wit inspect
ldv-memsafety/memleaks_test8_1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .49 30 5.8 true -32 wit inspect 4.6  250 true -32 wit inspect 4.7   230   error (1) 0 wit inspect .61   18    - wit inspect
ldv-memsafety/memleaks_test9_1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .49 30 6.2 true -32 wit inspect 2.5  250 true -32 wit inspect 4.5   230   error (1) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/memleaks_test9_2_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .49 30 6.1 true -32 wit inspect 4.3  250 true -32 wit inspect 3.2   230   error (1) 0 wit inspect .60   18    - wit inspect
ldv-memsafety/memleaks_test10_true-valid-memsafety_true-termination.i false(valid-deref) -16 wit inspect .86 31 11   - wit inspect - wit inspect - wit inspect true 2 wit inspect 350     670  
ldv-memsafety/memleaks_test11_true-valid-memsafety_true-termination.i false(valid-deref) -16 wit inspect 1.3  34 16   - wit inspect - wit inspect - wit inspect true 2 wit inspect 56     520  
ldv-memsafety/memleaks_test12_true-valid-memsafety.i unknown 0 wit inspect 270    210 3600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
ldv-memsafety/memleaks_test13_true-valid-memsafety.i true 2 wit inspect 30    360 300   - wit inspect - wit inspect - wit inspect true 2 wit inspect 81     940  
ldv-memsafety/memleaks_test14_true-valid-memsafety.i true 2 wit inspect 20    290 170   - wit inspect - wit inspect - wit inspect true 2 wit inspect 69     990  
ldv-memsafety/memleaks_test15_true-valid-memsafety_true-termination.i false(valid-deref) -16 wit inspect 1.1  35 13   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8   260  
ldv-memsafety/memleaks_test16_true-valid-memsafety_true-termination.i true 2 wit inspect 1.0  30 13   - wit inspect - wit inspect - wit inspect true 2 wit inspect 10     460  
ldv-memsafety/memleaks_test17_1_true-valid-memsafety_true-termination.i unknown 0 wit inspect 890    270 9000   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     2400  
ldv-memsafety/memleaks_test17_2_true-valid-memsafety_true-termination.i unknown 0 wit inspect 890    280 7700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
ldv-memsafety/memleaks_test18_true-valid-memsafety_true-termination.i unknown 0 wit inspect 890    220 9100   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     1100  
ldv-memsafety/memleaks_test19_true-valid-memsafety_true-termination.i true 2 wit inspect 1.1  30 14   - wit inspect - wit inspect - wit inspect true 2 wit inspect 330     820  
ldv-memsafety/memleaks_test1_true-valid-memsafety_true-termination.i true 2 wit inspect .99 30 11   - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.8   300  
ldv-memsafety/memleaks_test20_true-valid-memsafety_true-termination.i true 2 wit inspect 1.0  30 13   - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.7   470  
ldv-memsafety/memleaks_test21_true-valid-memsafety_true-termination.i true 2 wit inspect 1.0  30 13   - wit inspect - wit inspect - wit inspect true 2 wit inspect 11     440  
ldv-memsafety/memleaks_test22_1_true-valid-memsafety_true-termination.i true 2 wit inspect 27    33 330   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     2700  
ldv-memsafety/memleaks_test22_2_true-valid-memsafety_true-termination.i true 2 wit inspect 37    36 470   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     4000  
ldv-memsafety/memleaks_test22_3_true-valid-memsafety_true-termination.i true 2 wit inspect 37    36 530   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     3300  
ldv-memsafety/memleaks_test23_1_true-valid-memsafety.i false(valid-deref) -16 wit inspect 470    340 5100   - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.5   320  
ldv-memsafety/memleaks_test23_3_true-valid-memsafety.i false(valid-deref) -16 wit inspect 210    200 1900   - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.6   340  
ldv-memsafety/memleaks_test3_true-valid-memsafety_true-termination.i true 2 wit inspect .97 30 11   - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.5   340  
ldv-memsafety/memleaks_test4_true-valid-memsafety_true-termination.i true 2 wit inspect 1.0  30 11   - wit inspect - wit inspect - wit inspect true 2 wit inspect 28     520  
ldv-memsafety/memleaks_test5_true-valid-memsafety_true-termination.i true 2 wit inspect 1.0  30 14   - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.1   410  
ldv-memsafety/memleaks_test6_true-valid-memsafety_true-termination.i true 2 wit inspect 1.0  30 11   - wit inspect - wit inspect - wit inspect true 2 wit inspect 18     550  
ldv-memsafety/memleaks_test7_true-valid-memsafety_true-termination.i true 2 wit inspect 1.1  30 13   - wit inspect - wit inspect - wit inspect true 2 wit inspect 11     540  
ldv-memsafety/memleaks_test8_true-valid-memsafety_true-termination.i true 2 wit inspect .99 30 12   - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.2   350  
ldv-memsafety/memleaks_test9_true-valid-memsafety_true-termination.i true 2 wit inspect 1.0  30 13   - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.2   360  
ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety_true-termination.i unknown 0 wit inspect 17    28 190   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
ldv-memsafety-bitfields/test-bitfields-2.1_true-valid-memsafety_true-termination.i unknown 0 wit inspect 18    28 210   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety_true-termination.i unknown 0 wit inspect 18    29 260   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i unknown 0 wit inspect 9.0  28 100   - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 2.4   200  
ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i false(valid-deref) -16 wit inspect 9.6  28 130   - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 2.4   210  
ldv-memsafety-bitfields/test-bitfields-1_false-valid-deref.i unknown 0 wit inspect 17    28 200   error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .0035 .34 - wit inspect
ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i unknown 0 wit inspect 18    28 230   error (invalid witness file) 0 wit inspect .43 43 error (2) 0 wit inspect .017 4.9 error (invalid witness file) 0 wit inspect .0041 .30 - wit inspect
ldv-memsafety-bitfields/test-bitfields-3.1_false-valid-deref.i unknown 0 wit inspect 38    28 420   error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0011 .28 - wit inspect
ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i false(valid-deref) 0 wit inspect 9.5  28 120   true -32 wit inspect 3.3  240 unknown 0 wit inspect 3.5   200   error (1) 0 wit inspect .54   18    - wit inspect
ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i unknown 0 wit inspect 19    28 240   error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
total 180 -234 56000   90000 570000 90 -1531 1000 36000 90 -2048 530 21000 90 -221 41   1200 90 66 7600 31000
    correct results 37 70 2800   4900 31000 5 5 17 1300 0 3 3 2.0 55 33 66 1300 15000
        correct true 33 66 2800   4700 31000 0 0 0 33 66 1300 15000
        correct false 4 4 3.5 120 44 5 5 17 1300 0 3 3 2.0 55 0
    correct-unconfimed results 45 0 3000   3000 35000 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 45 0 3000   3000 35000 0 0 0 0
    incorrect results 19 -304 720   1500 7400 48 -1536 230 16000 64 -2048 430 20000 8 -224 5.2 150 0
        incorrect true 0 48 -1536 230 16000 64 -2048 430 20000 6 -192 3.9 110 0
        incorrect false 19 -304 720   1500 7400 0 0 2 -32 1.4 37 0
score (180 tasks, max score: 270) -234 -1531 -2048 -221 66
Run set depthk.sv-comp18.MemSafety-Heap cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.MemSafety-Heap uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.MemSafety-Heap fshell-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.MemSafety-Heap uautomizer-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.MemSafety-Heap