Tool ULTIMATE Kojak 0.1.23-3204b741 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* [apollon037; apollon054; apollon077; apollon078; apollon115] apollon*
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]
Date of execution 2017-12-03 04:40:15 CET 2017-12-03 05:43:12 CET 2017-12-03 06:07:12 CET 2017-12-03 06:08:25 CET 2017-12-03 05:47:35 CET
Run set ukojak.sv-comp18.MemSafety-Heap cpa-seq-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.MemSafety-Heap uautomizer-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.MemSafety-Heap fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.MemSafety-Heap uautomizer-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.MemSafety-Heap
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-03_0440.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/ukojak.2017-12-03_0440.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/ukojak.2017-12-03_0440.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/ukojak.2017-12-03_0440.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 timeout 0 wit inspect 900   3500 11000 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect
memsafety/test-0137_false-valid-deref.i false(valid-deref) 1 wit inspect 450   2000 6500 timeout (exception) 0 wit inspect 92    2300 true -32 wit inspect 13     560   false(valid-deref) 1 wit inspect .67   19    - wit inspect
memsafety/test-0235_false-valid-deref.i timeout 0 wit inspect 900   1300 10000 error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .0037 .29 - wit inspect
memsafety/960521-1_false-valid-free.i timeout 0 wit inspect 900   3800 12000 error (invalid witness file) 0 wit inspect .57 45 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .0035 .27 - wit inspect
memsafety/test-0158_false-valid-free.i false(valid-free) 1 wit inspect 19   740 200 true -32 wit inspect 3.7  250 true -32 wit inspect 7.4   270   false(valid-free) 1 wit inspect .65   19    - wit inspect
memsafety/test-0232_false-valid-free.i timeout 0 wit inspect 900   2100 13000 error (invalid witness file) 0 wit inspect .76 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0026 .26 - wit inspect
memsafety/20020406-1_false-valid-memtrack.i timeout 0 wit inspect 900   1600 13000 error (invalid witness file) 0 wit inspect .56 46 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0010 .26 - wit inspect
memsafety/20051113-1.c_false-valid-memtrack.i timeout 0 wit inspect 900   2200 12000 error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0011 .33 - wit inspect
memsafety/lockfree-3.1_false-valid-memtrack.i timeout 0 wit inspect 900   5400 12000 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect
memsafety/lockfree-3.2_false-valid-memtrack.i unknown 0 wit inspect 37   680 410 error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0041 .26 - wit inspect
memsafety/lockfree-3.3_false-valid-memtrack.i timeout 0 wit inspect 900   5500 11000 error (invalid witness file) 0 wit inspect .54 40 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .0011 .34 - wit inspect
memsafety/test-0019_false-valid-memtrack_true-termination.i unknown 0 wit inspect 71   880 750 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .0035 .29 - wit inspect
memsafety/test-0102_false-valid-memtrack.i timeout 0 wit inspect 900   1600 15000 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0041 .26 - wit inspect
memsafety/test-0158_false-valid-memtrack_true-termination.i unknown 0 wit inspect 17   470 150 error (invalid witness file) 0 wit inspect .57 45 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .0036 .26 - wit inspect
memsafety/test-0220_false-valid-memtrack.i timeout 0 wit inspect 900   780 11000 error (invalid witness file) 0 wit inspect .52 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0035 .26 - wit inspect
memsafety/test-0232_false-valid-memtrack.i unknown 0 wit inspect 650   1800 8300 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .047 4.8 error (invalid witness file) 0 wit inspect .0041 .27 - wit inspect
memsafety/test-0234_false-valid-memtrack.i timeout 0 wit inspect 900   3400 11000 error (invalid witness file) 0 wit inspect .39 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0040 .26 - wit inspect
memsafety/test-0235_false-valid-memtrack.i timeout 0 wit inspect 900   1300 11000 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0013 .27 - wit inspect
memsafety/960521-1_true-valid-memsafety.i timeout 0 wit inspect 900   3700 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
memsafety/lockfree-3.0_true-valid-memsafety.i timeout 0 wit inspect 900   5500 12000 - 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 38   890 410 - wit inspect - wit inspect - wit inspect true 2 wit inspect 29     500  
memsafety/test-0102_true-valid-memsafety.i timeout 0 wit inspect 900   1700 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 5.0
memsafety/test-0134_true-valid-memsafety.i timeout 0 wit inspect 900   1900 15000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
memsafety/test-0158_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   1500 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
memsafety/test-0214_true-valid-memsafety_false-termination.i timeout 0 wit inspect 900   1500 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
memsafety/test-0217_true-valid-memsafety_false-termination.i timeout 0 wit inspect 900   1400 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
memsafety/test-0218_true-valid-memsafety_false-termination.i timeout 0 wit inspect 900   1300 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
memsafety/test-0219_true-valid-memsafety.i timeout 0 wit inspect 900   830 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
memsafety/test-0232_true-valid-memsafety.i timeout 0 wit inspect 900   1900 14000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
memsafety/test-0234_true-valid-memsafety.i timeout 0 wit inspect 900   810 10000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
memsafety/test-0235_true-valid-memsafety.i timeout 0 wit inspect 900   1200 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
memsafety/test-0236_true-valid-memsafety.i timeout 0 wit inspect 900   1200 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
memsafety/test-0237_true-valid-memsafety.i timeout 0 wit inspect 900   1100 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .030 4.8
memsafety/test-0504_true-valid-memsafety.i timeout 0 wit inspect 900   2500 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
memsafety/test-0513_true-valid-memsafety.i timeout 0 wit inspect 900   1700 14000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .047 4.8
memsafety/test-0521_true-valid-memsafety.i timeout 0 wit inspect 900   1400 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
memsafety/test-memleak_nexttime_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   1700 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
memsafety-ext/dll_extends_pointer_true-valid-memsafety.i timeout 0 wit inspect 900   2000 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
memsafety-ext/skiplist_2lvl_true-valid-memsafety.i timeout 0 wit inspect 900   11000 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
memsafety-ext/skiplist_3lvl_true-valid-memsafety.i timeout 0 wit inspect 900   12000 6100 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
memsafety-ext/tree_cnstr_true-valid-memsafety_false-termination.i timeout 0 wit inspect 900   3400 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
memsafety-ext/tree_dsw_true-valid-memsafety_false-termination.i timeout 0 wit inspect 910   2500 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
memsafety-ext/tree_of_cslls_true-valid-memsafety.i timeout 0 wit inspect 900   2400 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .028 4.9
memsafety-ext/tree_parent_ptr_true-valid-memsafety_false-termination.i timeout 0 wit inspect 900   2300 14000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
memsafety-ext/tree_stack_true-valid-memsafety_false-termination.i timeout 0 wit inspect 900   2200 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .028 4.8
memsafety-ext2/split_list_test05_false-valid-deref.i timeout 0 wit inspect 900   2100 12000 error (invalid witness file) 0 wit inspect .39 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0039 .26 - wit inspect
memsafety-ext2/complex_data_creation_test01_false-valid-memtrack.i timeout 0 wit inspect 900   1800 12000 error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0039 .26 - wit inspect
memsafety-ext2/complex_data_creation_test02_false-valid-memtrack.i timeout 0 wit inspect 900   1800 13000 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect
memsafety-ext2/length_test03_false-valid-memtrack.i timeout 0 wit inspect 900   1500 12000 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0041 .35 - wit inspect
memsafety-ext2/optional_data_creation_test04_false-valid-memtrack.i timeout 0 wit inspect 900   1600 11000 error (invalid witness file) 0 wit inspect .79 41 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect
memsafety-ext2/complex_data_creation_test01_true-valid-memsafety.i timeout 0 wit inspect 900   1800 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 5.0
memsafety-ext2/complex_data_creation_test02_true-valid-memsafety.i timeout 0 wit inspect 900   2300 14000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
memsafety-ext2/length_test03_true-valid-memsafety.i timeout 0 wit inspect 900   1700 14000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
memsafety-ext2/optional_data_creation_test04_true-valid-memsafety.i timeout 0 wit inspect 900   1700 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
memsafety-ext2/split_list_test05_true-valid-memsafety.i timeout 0 wit inspect 900   1800 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
list-ext-properties/960521-1_1_false-valid-deref.i false(valid-deref) 0 wit inspect 13   680 140 true -32 wit inspect 8.7  470 true -32 wit inspect 4.4   270   error (2) 0 wit inspect .74   18    - wit inspect
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i timeout 0 wit inspect 900   1600 14000 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0049 .28 - wit inspect
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 52   1100 670 timeout 0 wit inspect 92    2500 false(valid-free) -16 wit inspect 6.3   280   false(valid-deref) 1 wit inspect .65   18    - wit inspect
list-ext-properties/960521-1_1_false-valid-free.i false(valid-free) 1 wit inspect 28   870 300 true -32 wit inspect 12    480 false(valid-free) 1 wit inspect 5.9   270   false(valid-free) 1 wit inspect .69   18    - wit inspect
list-ext-properties/test-0158_1_false-valid-free.i false(valid-free) 0 wit inspect 29   830 340 true -32 wit inspect 2.3  260 true -32 wit inspect 5.0   270   error (2) 0 wit inspect .68   18    - wit inspect
list-ext-properties/test-0019_1_false-valid-memtrack_true-termination.i unknown 0 wit inspect 470   1900 7200 error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0011 .31 - wit inspect
list-ext-properties/test-0158_1_false-valid-memtrack_true-termination.i unknown 0 wit inspect 29   670 290 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect
list-ext-properties/test-0232_1_false-valid-memtrack_true-termination.i unknown 0 wit inspect 550   1800 6800 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0010 .36 - wit inspect
list-ext-properties/960521-1_1_true-valid-memsafety.i timeout 0 wit inspect 900   1800 9100 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
list-ext-properties/list-ext_1_true-valid-memsafety.i timeout 0 wit inspect 900   1500 14000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
list-ext-properties/list-ext_flag_1_true-valid-memsafety.i timeout 0 wit inspect 900   2400 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
list-ext-properties/simple-ext_1_true-valid-memsafety.i timeout 0 wit inspect 900   4400 14000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
list-ext-properties/test-0019_1_true-valid-memsafety_true-termination.i true 2 wit inspect 170   1700 2000 - wit inspect - wit inspect - wit inspect true 2 wit inspect 150     800  
list-ext-properties/test-0158_1_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   3100 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
list-ext-properties/test-0214_1_true-valid-memsafety.i timeout 0 wit inspect 900   1500 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 5.0
list-ext-properties/test-0217_1_true-valid-memsafety.i timeout 0 wit inspect 900   1600 14000 - 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 timeout 0 wit inspect 900   1700 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.9
list-ext-properties/test-0504_1_true-valid-memsafety.i timeout 0 wit inspect 900   2300 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
list-ext-properties/test-0513_1_true-valid-memsafety.i timeout 0 wit inspect 900   2200 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
memory-alloca/c.03-alloca_true-valid-memsafety.i timeout 0 wit inspect 900   2000 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c false(valid-deref) 0 wit inspect 6.8 430 59 true -32 wit inspect 2.8  250 true -32 wit inspect 8.6   290   timeout 0 wit inspect 96      18    - wit inspect
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-write.c false(valid-deref) 1 wit inspect 7.4 460 67 true -32 wit inspect 4.2  240 false(valid-deref) 1 wit inspect 5.8   270   timeout 0 wit inspect 96      19    - wit inspect
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-read.c false(valid-deref) 1 wit inspect 4.7 260 40 false(valid-deref) 1 wit inspect 3.2  240 false(valid-deref) 1 wit inspect 3.7   260   true -32 wit inspect .58   18    - wit inspect
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-write.c false(valid-deref) 1 wit inspect 4.9 260 41 false(valid-deref) 1 wit inspect 3.0  270 false(valid-deref) 1 wit inspect 5.4   260   true -32 wit inspect .58   18    - wit inspect
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c timeout 0 wit inspect 900   5500 13000 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .048 4.8 error (invalid witness file) 0 wit inspect .0010 .34 - wit inspect
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-write.c timeout 0 wit inspect 900   5500 11000 error (invalid witness file) 0 wit inspect .80 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0011 .34 - wit inspect
ldv-memsafety/memset2_false-valid-deref-write.c false(valid-deref) 1 wit inspect 4.5 260 41 true -32 wit inspect 2.6  210 true -32 wit inspect 4.9   260   false(valid-deref) 1 wit inspect .60   18    - wit inspect
ldv-memsafety/memset3_false-valid-deref-write.c false(valid-deref) 1 wit inspect 4.5 250 42 true -32 wit inspect 2.7  240 true -32 wit inspect 4.1   280   false(valid-deref) 1 wit inspect .58   18    - wit inspect
ldv-memsafety/memsetNonZero2_false-valid-deref-write.c false(valid-deref) 1 wit inspect 4.6 250 38 true -32 wit inspect 2.6  240 true -32 wit inspect 3.7   270   false(valid-deref) 1 wit inspect .59   18    - wit inspect
ldv-memsafety/memsetNonZero3_false-valid-deref-write.c false(valid-deref) 1 wit inspect 4.8 250 38 true -32 wit inspect 2.7  240 true -32 wit inspect 5.5   260   false(valid-deref) 1 wit inspect .58   18    - wit inspect
ldv-memsafety/memsetNonZero_false-valid-deref-write.c false(valid-deref) 1 wit inspect 4.6 260 33 true -32 wit inspect 2.7  240 true -32 wit inspect 3.6   260   false(valid-deref) 1 wit inspect .60   18    - wit inspect
ldv-memsafety/memset_false-valid-deref-write.c false(valid-deref) 1 wit inspect 4.4 260 33 true -32 wit inspect 2.5  240 true -32 wit inspect 5.0   270   false(valid-deref) 1 wit inspect .62   18    - wit inspect
ldv-memsafety/ArraysOfVariableLength2_true-valid-memsafety.c timeout 0 wit inspect 900   2200 14000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c timeout 0 wit inspect 900   5500 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
ldv-memsafety/ArraysOfVariableLength5_true-valid-memsafety.c timeout 0 wit inspect 900   5500 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
ldv-memsafety/ArraysOfVariableLength6_true-valid-memsafety_true-termination.c timeout 0 wit inspect 900   5500 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
ldv-memsafety/ArraysOfVariableLength_true-valid-memsafety.c timeout 0 wit inspect 900   5300 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety_true-termination.c timeout 0 wit inspect 900   5400 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
ldv-memsafety/StructInitialization1_true-valid-memsafety.c error (7) 0 wit inspect 3.5 220 30 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
ldv-memsafety/StructInitialization2_true-valid-memsafety.c error (7) 0 wit inspect 4.1 230 29 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c true 2 wit inspect 4.1 240 34 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3   210  
ldv-memsafety/memset2_true-valid-memsafety_true-termination.c true 2 wit inspect 29   880 280 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.3   290  
ldv-memsafety/memset3_true-valid-memsafety_true-termination.c true 2 wit inspect 63   1700 750 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.4   290  
ldv-memsafety/memsetNonZero2_true-valid-memsafety_true-termination.c true 2 wit inspect 27   870 320 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.9   290  
ldv-memsafety/memsetNonZero3_true-valid-memsafety_true-termination.c true 2 wit inspect 62   1600 690 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7   300  
ldv-memsafety/memsetNonZero_true-valid-memsafety_true-termination.c true 2 wit inspect 63   1700 730 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.3   290  
ldv-memsafety/memset_true-valid-memsafety_true-termination.c true 2 wit inspect 62   1600 840 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.3   290  
ldv-memsafety/memleaks_test14_3_false-valid-deref.i false(valid-deref) 0 wit inspect 300   1400 4500 true -32 wit inspect 4.0  270 true -32 wit inspect 8.3   340   error (1) 0 wit inspect .62   19    - wit inspect
ldv-memsafety/memleaks_test22_3_false-valid-deref.i false(valid-deref) 0 wit inspect 340   1400 5700 true -32 wit inspect 4.1  250 true -32 wit inspect 8.1   300   error (1) 0 wit inspect .59   19    - wit inspect
ldv-memsafety/memleaks_test22_5_false-valid-deref.i false(valid-deref) 0 wit inspect 340   1600 4300 true -32 wit inspect 4.5  250 true -32 wit inspect 5.2   300   error (1) 0 wit inspect .59   19    - wit inspect
ldv-memsafety/memleaks_test23_2_false-valid-deref.i timeout 0 wit inspect 900   1600 14000 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0035 .26 - wit inspect
ldv-memsafety/memleaks_test23_4_false-valid-deref.i timeout 0 wit inspect 900   1400 14000 error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0015 .29 - wit inspect
ldv-memsafety/memleaks_test11_1_false-valid-free.i false(valid-free) 0 wit inspect 190   1300 2300 true -32 wit inspect 2.7  250 true -32 wit inspect 62     580   error (1) 0 wit inspect .59   19    - wit inspect
ldv-memsafety/memleaks_test12_false-valid-free.i timeout 0 wit inspect 900   1500 12000 error (invalid witness file) 0 wit inspect .75 42 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0034 .34 - wit inspect
ldv-memsafety/memleaks_test17_2_false-valid-free.i timeout 0 wit inspect 900   2700 12000 error (invalid witness file) 0 wit inspect .80 42 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0012 .35 - wit inspect
ldv-memsafety/memleaks_test19_false-valid-free.i false(valid-free) 1 wit inspect 520   1300 6200 true -32 wit inspect 3.8  250 false(valid-free) 1 wit inspect 6.5   390   error (1) 0 wit inspect .59   19    - wit inspect
ldv-memsafety/memleaks_test1_false-valid-free.i false(valid-free) 0 wit inspect 6.9 340 63 true -32 wit inspect 3.7  250 true -32 wit inspect 6.0   260   error (1) 0 wit inspect .59   19    - wit inspect
ldv-memsafety/memleaks_test3_false-valid-free.i false(valid-free) 1 wit inspect 4.7 250 37 false(valid-free) 1 wit inspect 3.8  250 false(valid-free) 1 wit inspect 5.2   260   error (1) 0 wit inspect .59   19    - wit inspect
ldv-memsafety/memleaks_test6_2_false-valid-free.i false(valid-free) 1 wit inspect 48   1000 590 true -32 wit inspect 2.6  250 false(valid-free) 1 wit inspect 9.0   290   error (1) 0 wit inspect .59   19    - wit inspect
ldv-memsafety/memleaks_test8_2_false-valid-free.i false(valid-free) 1 wit inspect 7.6 470 70 false(valid-free) 1 wit inspect 4.8  270 false(valid-free) 1 wit inspect 6.7   270   error (1) 0 wit inspect .60   18    - wit inspect
ldv-memsafety/memleaks_test10_false-valid-memtrack_true-termination.i error (7) 0 wit inspect 430   1300 5000 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .0012 .29 - wit inspect
ldv-memsafety/memleaks_test11_2_false-valid-memtrack_true-termination.i error (7) 0 wit inspect 390   1300 5100 error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0041 .28 - wit inspect
ldv-memsafety/memleaks_test13_1_false-valid-memtrack_true-termination.i error (7) 0 wit inspect 52   1000 620 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .0011 .34 - wit inspect
ldv-memsafety/memleaks_test13_2_false-valid-memtrack.i error (7) 0 wit inspect 370   1300 4800 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
ldv-memsafety/memleaks_test14_1_false-valid-memtrack_true-termination.i error (7) 0 wit inspect 36   820 430 error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0036 .26 - wit inspect
ldv-memsafety/memleaks_test14_2_false-valid-memtrack.i error (7) 0 wit inspect 340   1400 4300 error (invalid witness file) 0 wit inspect .55 45 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0011 .29 - wit inspect
ldv-memsafety/memleaks_test15_false-valid-memtrack.i timeout 0 wit inspect 900   2300 14000 error (invalid witness file) 0 wit inspect .57 45 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0011 .29 - wit inspect
ldv-memsafety/memleaks_test16_1_false-valid-memtrack_true-termination.i error (7) 0 wit inspect 10   290 87 error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
ldv-memsafety/memleaks_test16_2_false-valid-memtrack_true-termination.i error (7) 0 wit inspect 10   270 87 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
ldv-memsafety/memleaks_test17_1_false-valid-memtrack.i timeout 0 wit inspect 900   1300 15000 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect
ldv-memsafety/memleaks_test17_3_false-valid-memtrack.i timeout 0 wit inspect 900   1500 11000 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect .0040 .34 - wit inspect
ldv-memsafety/memleaks_test18_1_false-valid-memtrack_true-termination.i error (7) 0 wit inspect 14   510 110 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .028 5.0 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect
ldv-memsafety/memleaks_test18_2_false-valid-memtrack_true-termination.i timeout 0 wit inspect 900   1400 12000 error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect
ldv-memsafety/memleaks_test18_3_false-valid-memtrack_true-termination.i timeout 0 wit inspect 900   4900 10000 error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect
ldv-memsafety/memleaks_test1_false-valid-memtrack_true-termination.i error (7) 0 wit inspect 9.3 260 78 error (invalid witness file) 0 wit inspect .79 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect
ldv-memsafety/memleaks_test20_false-valid-memtrack_true-termination.i error (7) 0 wit inspect 9.8 260 76 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0011 .36 - wit inspect
ldv-memsafety/memleaks_test21_false-valid-memtrack_true-termination.i error (7) 0 wit inspect 9.2 260 78 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0040 .26 - wit inspect
ldv-memsafety/memleaks_test22_1_false-valid-memtrack_true-termination.i error (7) 0 wit inspect 170   1300 2400 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect
ldv-memsafety/memleaks_test22_2_false-valid-memtrack_true-termination.i error (7) 0 wit inspect 42   870 460 error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0011 .35 - wit inspect
ldv-memsafety/memleaks_test22_4_false-valid-memtrack_true-termination.i error (7) 0 wit inspect 170   1300 2200 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
ldv-memsafety/memleaks_test4_false-valid-memtrack_true-termination.i error (7) 0 wit inspect 12   330 97 error (invalid witness file) 0 wit inspect .81 44 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .0012 .29 - wit inspect
ldv-memsafety/memleaks_test5_1_false-valid-memtrack_true-termination.i error (7) 0 wit inspect 9.2 260 76 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
ldv-memsafety/memleaks_test5_2_false-valid-memtrack_true-termination.i error (7) 0 wit inspect 9.8 270 77 error (invalid witness file) 0 wit inspect .76 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0011 .34 - wit inspect
ldv-memsafety/memleaks_test6_1_false-valid-memtrack_true-termination.i error (7) 0 wit inspect 33   820 410 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .0051 .26 - wit inspect
ldv-memsafety/memleaks_test6_3_false-valid-memtrack_true-termination.i error (7) 0 wit inspect 23   700 230 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0041 .26 - wit inspect
ldv-memsafety/memleaks_test7_false-valid-memtrack_true-termination.i error (7) 0 wit inspect 17   590 170 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect
ldv-memsafety/memleaks_test8_1_false-valid-memtrack_true-termination.i error (7) 0 wit inspect 9.3 260 73 error (invalid witness file) 0 wit inspect .75 42 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect
ldv-memsafety/memleaks_test9_1_false-valid-memtrack_true-termination.i error (7) 0 wit inspect 9.8 270 81 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .036 4.9 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
ldv-memsafety/memleaks_test9_2_false-valid-memtrack_true-termination.i error (7) 0 wit inspect 9.6 260 86 error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .0041 .30 - wit inspect
ldv-memsafety/memleaks_test10_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   1300 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
ldv-memsafety/memleaks_test11_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   1400 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
ldv-memsafety/memleaks_test12_true-valid-memsafety.i timeout 0 wit inspect 900   1600 9500 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
ldv-memsafety/memleaks_test13_true-valid-memsafety.i true 2 wit inspect 690   1400 8900 - wit inspect - wit inspect - wit inspect true 2 wit inspect 84     950  
ldv-memsafety/memleaks_test14_true-valid-memsafety.i true 2 wit inspect 690   1400 8600 - wit inspect - wit inspect - wit inspect true 2 wit inspect 100     980  
ldv-memsafety/memleaks_test15_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   1300 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
ldv-memsafety/memleaks_test16_true-valid-memsafety_true-termination.i true 2 wit inspect 7.9 380 74 - wit inspect - wit inspect - wit inspect true 2 wit inspect 11     450  
ldv-memsafety/memleaks_test17_1_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   2500 14000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
ldv-memsafety/memleaks_test17_2_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   1300 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
ldv-memsafety/memleaks_test18_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   1300 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
ldv-memsafety/memleaks_test19_true-valid-memsafety_true-termination.i true 2 wit inspect 550   1200 8900 - wit inspect - wit inspect - wit inspect true 2 wit inspect 330     880  
ldv-memsafety/memleaks_test1_true-valid-memsafety_true-termination.i true 2 wit inspect 6.4 350 53 - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.2   270  
ldv-memsafety/memleaks_test20_true-valid-memsafety_true-termination.i true 2 wit inspect 8.1 430 64 - wit inspect - wit inspect - wit inspect true 2 wit inspect 11     470  
ldv-memsafety/memleaks_test21_true-valid-memsafety_true-termination.i true 2 wit inspect 7.8 480 71 - wit inspect - wit inspect - wit inspect true 2 wit inspect 10     420  
ldv-memsafety/memleaks_test22_1_true-valid-memsafety_true-termination.i true 2 wit inspect 430   1300 6800 - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     2000  
ldv-memsafety/memleaks_test22_2_true-valid-memsafety_true-termination.i true 2 wit inspect 820   1400 11000 - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     4300  
ldv-memsafety/memleaks_test22_3_true-valid-memsafety_true-termination.i true 2 wit inspect 810   1300 11000 - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     2400  
ldv-memsafety/memleaks_test23_1_true-valid-memsafety.i timeout 0 wit inspect 900   1600 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
ldv-memsafety/memleaks_test23_3_true-valid-memsafety.i timeout 0 wit inspect 900   1500 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
ldv-memsafety/memleaks_test3_true-valid-memsafety_true-termination.i true 2 wit inspect 7.3 460 61 - wit inspect - wit inspect - wit inspect true 2 wit inspect 10     330  
ldv-memsafety/memleaks_test4_true-valid-memsafety_true-termination.i true 2 wit inspect 11   670 110 - wit inspect - wit inspect - wit inspect true 2 wit inspect 28     510  
ldv-memsafety/memleaks_test5_true-valid-memsafety_true-termination.i true 2 wit inspect 7.1 470 63 - wit inspect - wit inspect - wit inspect true 2 wit inspect 17     430  
ldv-memsafety/memleaks_test6_true-valid-memsafety_true-termination.i true 2 wit inspect 63   1200 700 - wit inspect - wit inspect - wit inspect true 2 wit inspect 27     550  
ldv-memsafety/memleaks_test7_true-valid-memsafety_true-termination.i true 2 wit inspect 40   910 440 - wit inspect - wit inspect - wit inspect true 2 wit inspect 16     540  
ldv-memsafety/memleaks_test8_true-valid-memsafety_true-termination.i true 2 wit inspect 7.5 480 64 - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.1   350  
ldv-memsafety/memleaks_test9_true-valid-memsafety_true-termination.i true 2 wit inspect 7.5 360 68 - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.2   350  
ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety_true-termination.i unknown 0 wit inspect 3.4 230 29 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
ldv-memsafety-bitfields/test-bitfields-2.1_true-valid-memsafety_true-termination.i unknown 0 wit inspect 3.6 230 27 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety_true-termination.i unknown 0 wit inspect 3.5 220 29 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i unknown 0 wit inspect 3.5 230 29 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 5.0
ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i unknown 0 wit inspect 3.4 220 29 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
ldv-memsafety-bitfields/test-bitfields-1_false-valid-deref.i unknown 0 wit inspect 3.5 220 28 error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0022 .26 - wit inspect
ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i unknown 0 wit inspect 3.4 220 29 error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
ldv-memsafety-bitfields/test-bitfields-3.1_false-valid-deref.i unknown 0 wit inspect 3.5 220 32 error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0012 .28 - wit inspect
ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i unknown 0 wit inspect 3.5 230 30 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .0010 .26 - wit inspect
ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i unknown 0 wit inspect 3.6 230 26 error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0035 .27 - 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 69 89000 290000 1200000 90 -604 310 14000 90 -520 210   7900 90 -54 210   480 90 46 3800 20000
    correct results 43 69 5900 36000 78000 4 4 15 1000 8 8 48   2300 10 10 6.2 180 23 46 890 11000
        correct true 26 52 4700 25000 63000 0 0 0 23 46 890 11000
        correct false 17 17 1200 10000 15000 4 4 15 1000 8 8 48   2300 10 10 6.2 180 0
    correct-unconfimed results 8 0 1200 8000 17000 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 8 0 1200 8000 17000 0 0 0 0
    incorrect results 0 19 -608 75 5100 17 -528 160   5300 2 -64 1.2 37 0
        incorrect true 0 19 -608 75 5100 16 -512 150   5000 2 -64 1.2 37 0
        incorrect false 0 0 1 -16 6.3 280 0 0
score (180 tasks, max score: 270) 69 -604 -520 -54 46
Run set ukojak.sv-comp18.MemSafety-Heap cpa-seq-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.MemSafety-Heap uautomizer-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.MemSafety-Heap fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.MemSafety-Heap uautomizer-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.MemSafety-Heap