Tool ULTIMATE Automizer 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*
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:39:25 CET 2017-12-03 05:43:13 CET 2017-12-03 06:05:52 CET 2017-12-03 06:06:56 CET 2017-12-03 05:47:48 CET
Run set uautomizer.sv-comp18.MemSafety-Heap cpa-seq-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.MemSafety-Heap uautomizer-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.MemSafety-Heap fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.MemSafety-Heap uautomizer-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.MemSafety-Heap
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/uautomizer.2017-12-03_0439.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/uautomizer.2017-12-03_0439.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/uautomizer.2017-12-03_0439.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/uautomizer.2017-12-03_0439.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   1100 9900 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
memsafety/test-0137_false-valid-deref.i false(valid-deref) 1 wit inspect 46   970 470 timeout 0 wit inspect 92    2400 true -32 wit inspect 15     570   false(valid-deref) 1 wit inspect .70   19    - wit inspect
memsafety/test-0235_false-valid-deref.i timeout 0 wit inspect 900   880 11000 error (invalid witness file) 0 wit inspect .59 42 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect
memsafety/960521-1_false-valid-free.i timeout 0 wit inspect 900   1000 9800 error (invalid witness file) 0 wit inspect .81 42 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0011 .34 - wit inspect
memsafety/test-0158_false-valid-free.i false(valid-free) 1 wit inspect 6.5 290 58 true -32 wit inspect 3.3  250 true -32 wit inspect 7.7   270   false(valid-free) 1 wit inspect .67   18    - wit inspect
memsafety/test-0232_false-valid-free.i error (7) 0 wit inspect 320   870 4000 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0012 .30 - wit inspect
memsafety/20020406-1_false-valid-memtrack.i error (7) 0 wit inspect 710   2700 7500 error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .023 5.0 error (invalid witness file) 0 wit inspect .0033 .34 - wit inspect
memsafety/20051113-1.c_false-valid-memtrack.i timeout 0 wit inspect 900   1000 13000 error (invalid witness file) 0 wit inspect .77 42 error (2) 0 wit inspect .026 5.0 error (invalid witness file) 0 wit inspect .0013 .30 - wit inspect
memsafety/lockfree-3.1_false-valid-memtrack.i unknown 0 wit inspect 68   970 590 error (invalid witness file) 0 wit inspect .76 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0030 .31 - wit inspect
memsafety/lockfree-3.2_false-valid-memtrack.i unknown 0 wit inspect 20   570 160 error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect
memsafety/lockfree-3.3_false-valid-memtrack.i unknown 0 wit inspect 110   3000 1100 error (invalid witness file) 0 wit inspect .51 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0037 .26 - wit inspect
memsafety/test-0019_false-valid-memtrack_true-termination.i unknown 0 wit inspect 19   510 150 error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .049 4.9 error (invalid witness file) 0 wit inspect .0016 .29 - wit inspect
memsafety/test-0102_false-valid-memtrack.i error (7) 0 wit inspect 140   1100 1700 error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect
memsafety/test-0158_false-valid-memtrack_true-termination.i unknown 0 wit inspect 11   330 89 error (invalid witness file) 0 wit inspect .57 45 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0017 .26 - wit inspect
memsafety/test-0220_false-valid-memtrack.i timeout 0 wit inspect 900   760 13000 error (invalid witness file) 0 wit inspect .78 42 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect
memsafety/test-0232_false-valid-memtrack.i unknown 0 wit inspect 61   690 630 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .0011 .29 - wit inspect
memsafety/test-0234_false-valid-memtrack.i timeout 0 wit inspect 900   780 10000 error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .0019 .26 - wit inspect
memsafety/test-0235_false-valid-memtrack.i timeout 0 wit inspect 900   790 12000 error (invalid witness file) 0 wit inspect .40 42 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect
memsafety/960521-1_true-valid-memsafety.i timeout 0 wit inspect 900   1300 9400 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 5.0
memsafety/lockfree-3.0_true-valid-memsafety.i timeout 0 wit inspect 900   10000 7800 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
memsafety/test-0019_true-valid-memsafety_true-termination.i true 2 wit inspect 22   580 210 - wit inspect - wit inspect - wit inspect true 2 wit inspect 28     500  
memsafety/test-0102_true-valid-memsafety.i error (7) 0 wit inspect 150   1100 1700 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .029 5.0
memsafety/test-0134_true-valid-memsafety.i timeout 0 wit inspect 900   1100 9300 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
memsafety/test-0158_true-valid-memsafety_true-termination.i true 2 wit inspect 14   370 120 - wit inspect - wit inspect - wit inspect true 2 wit inspect 16     380  
memsafety/test-0214_true-valid-memsafety_false-termination.i timeout 0 wit inspect 900   1400 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 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 error (7) 0 wit inspect 670   1400 9500 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.9
memsafety/test-0219_true-valid-memsafety.i timeout 0 wit inspect 900   750 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
memsafety/test-0232_true-valid-memsafety.i error (7) 0 wit inspect 270   850 3400 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
memsafety/test-0234_true-valid-memsafety.i timeout 0 wit inspect 900   820 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
memsafety/test-0235_true-valid-memsafety.i timeout 0 wit inspect 900   790 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
memsafety/test-0236_true-valid-memsafety.i timeout 0 wit inspect 900   800 14000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
memsafety/test-0237_true-valid-memsafety.i timeout 0 wit inspect 900   790 10000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
memsafety/test-0504_true-valid-memsafety.i timeout 0 wit inspect 900   1100 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
memsafety/test-0513_true-valid-memsafety.i timeout 0 wit inspect 900   840 10000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
memsafety/test-0521_true-valid-memsafety.i timeout 0 wit inspect 900   1700 8700 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
memsafety/test-memleak_nexttime_true-valid-memsafety_true-termination.i error (7) 0 wit inspect 170   990 1900 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 5.0
memsafety-ext/dll_extends_pointer_true-valid-memsafety.i timeout 0 wit inspect 900   1600 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
memsafety-ext/skiplist_2lvl_true-valid-memsafety.i timeout 0 wit inspect 900   1000 10000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
memsafety-ext/skiplist_3lvl_true-valid-memsafety.i timeout 0 wit inspect 900   950 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
memsafety-ext/tree_cnstr_true-valid-memsafety_false-termination.i timeout 0 wit inspect 900   1300 9700 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
memsafety-ext/tree_dsw_true-valid-memsafety_false-termination.i timeout 0 wit inspect 900   920 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
memsafety-ext/tree_of_cslls_true-valid-memsafety.i timeout 0 wit inspect 900   920 10000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
memsafety-ext/tree_parent_ptr_true-valid-memsafety_false-termination.i error (7) 0 wit inspect 600   810 7700 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
memsafety-ext/tree_stack_true-valid-memsafety_false-termination.i timeout 0 wit inspect 900   980 14000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
memsafety-ext2/split_list_test05_false-valid-deref.i timeout 0 wit inspect 900   4000 11000 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0021 .26 - wit inspect
memsafety-ext2/complex_data_creation_test01_false-valid-memtrack.i timeout 0 wit inspect 900   3000 11000 error (invalid witness file) 0 wit inspect .79 42 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .0013 .28 - wit inspect
memsafety-ext2/complex_data_creation_test02_false-valid-memtrack.i timeout 0 wit inspect 900   1900 11000 error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
memsafety-ext2/length_test03_false-valid-memtrack.i timeout 0 wit inspect 900   1600 14000 error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0013 .35 - wit inspect
memsafety-ext2/optional_data_creation_test04_false-valid-memtrack.i timeout 0 wit inspect 900   930 11000 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .0031 .30 - wit inspect
memsafety-ext2/complex_data_creation_test01_true-valid-memsafety.i timeout 0 wit inspect 900   3000 10000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
memsafety-ext2/complex_data_creation_test02_true-valid-memsafety.i timeout 0 wit inspect 900   1600 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 5.0
memsafety-ext2/length_test03_true-valid-memsafety.i timeout 0 wit inspect 900   1500 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
memsafety-ext2/optional_data_creation_test04_true-valid-memsafety.i timeout 0 wit inspect 900   1000 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
memsafety-ext2/split_list_test05_true-valid-memsafety.i timeout 0 wit inspect 900   3400 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) 1 wit inspect 9.2 470 76 false(valid-deref) 1 wit inspect 3.5  260 true -32 wit inspect 7.6   270   error (2) 0 wit inspect .68   18    - wit inspect
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i timeout 0 wit inspect 900   1500 12000 error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 18   540 170 false(valid-deref) 1 wit inspect 3.5  250 false(valid-free) -16 wit inspect 6.2   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 12   520 110 false(valid-free) 1 wit inspect 3.6  250 false(valid-free) 1 wit inspect 4.3   290   false(valid-free) 1 wit inspect .68   18    - wit inspect
list-ext-properties/test-0158_1_false-valid-free.i false(valid-free) 1 wit inspect 7.0 310 62 false(valid-free) 1 wit inspect 4.2  250 true -32 wit inspect 7.5   260   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 150   920 2100 error (invalid witness file) 0 wit inspect .57 45 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0014 .27 - wit inspect
list-ext-properties/test-0158_1_false-valid-memtrack_true-termination.i unknown 0 wit inspect 11   350 100 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect
list-ext-properties/test-0232_1_false-valid-memtrack_true-termination.i unknown 0 wit inspect 56   700 590 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0033 .34 - wit inspect
list-ext-properties/960521-1_1_true-valid-memsafety.i timeout 0 wit inspect 900   1200 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
list-ext-properties/list-ext_1_true-valid-memsafety.i error (7) 0 wit inspect 300   810 3400 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
list-ext-properties/list-ext_flag_1_true-valid-memsafety.i timeout 0 wit inspect 900   2300 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
list-ext-properties/simple-ext_1_true-valid-memsafety.i error (7) 0 wit inspect 400   920 4000 - 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 120   900 1300 - wit inspect - wit inspect - wit inspect true 2 wit inspect 150     800  
list-ext-properties/test-0158_1_true-valid-memsafety_true-termination.i true 2 wit inspect 14   380 110 - wit inspect - wit inspect - wit inspect true 2 wit inspect 19     360  
list-ext-properties/test-0214_1_true-valid-memsafety.i error (7) 0 wit inspect 860   1300 10000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
list-ext-properties/test-0217_1_true-valid-memsafety.i timeout 0 wit inspect 900   1400 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 error (7) 0 wit inspect 270   830 3300 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.9
list-ext-properties/test-0504_1_true-valid-memsafety.i timeout 0 wit inspect 900   1200 10000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
list-ext-properties/test-0513_1_true-valid-memsafety.i timeout 0 wit inspect 900   860 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
memory-alloca/c.03-alloca_true-valid-memsafety.i true 2 wit inspect 9.5 530 73 - wit inspect - wit inspect - wit inspect true 2 wit inspect 14     510  
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c false(valid-deref) 1 wit inspect 5.7 280 49 false(valid-deref) 1 wit inspect 3.0  240 true -32 wit inspect 8.9   290   timeout 0 wit inspect 96      18    - wit inspect
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-write.c false(valid-deref) 1 wit inspect 6.4 300 53 false(valid-deref) 1 wit inspect 4.3  240 false(valid-deref) 1 wit inspect 6.0   260   timeout 0 wit inspect 96      18    - wit inspect
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-read.c false(valid-deref) 1 wit inspect 4.9 280 41 false(valid-deref) 1 wit inspect 2.8  240 false(valid-deref) 1 wit inspect 5.5   260   true -32 wit inspect .67   18    - wit inspect
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-write.c false(valid-deref) 1 wit inspect 5.1 290 40 false(valid-deref) 1 wit inspect 2.8  240 false(valid-deref) 1 wit inspect 5.4   270   true -32 wit inspect .61   18    - wit inspect
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c timeout 0 wit inspect 900   5400 10000 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-write.c false(valid-deref) 1 wit inspect 730   5500 9200 false(valid-deref) 1 wit inspect 8.4  290 false(valid-deref) 1 wit inspect 34     2900   false(valid-deref) 1 wit inspect .69   26    - wit inspect
ldv-memsafety/memset2_false-valid-deref-write.c false(valid-deref) 1 wit inspect 4.8 280 35 false(valid-deref) 1 wit inspect 3.8  240 true -32 wit inspect 5.3   270   false(valid-deref) 1 wit inspect .59   18    - wit inspect
ldv-memsafety/memset3_false-valid-deref-write.c false(valid-deref) 1 wit inspect 4.7 290 43 false(valid-deref) 1 wit inspect 2.6  250 true -32 wit inspect 5.7   260   false(valid-deref) 1 wit inspect .60   18    - wit inspect
ldv-memsafety/memsetNonZero2_false-valid-deref-write.c false(valid-deref) 1 wit inspect 4.4 280 38 false(valid-deref) 1 wit inspect 2.6  240 true -32 wit inspect 6.7   270   false(valid-deref) 1 wit inspect .61   18    - wit inspect
ldv-memsafety/memsetNonZero3_false-valid-deref-write.c false(valid-deref) 1 wit inspect 4.7 280 43 false(valid-deref) 1 wit inspect 2.9  250 true -32 wit inspect 5.4   260   false(valid-deref) 1 wit inspect .67   18    - wit inspect
ldv-memsafety/memsetNonZero_false-valid-deref-write.c false(valid-deref) 1 wit inspect 4.7 280 43 false(valid-deref) 1 wit inspect 1.9  250 true -32 wit inspect 5.7   250   false(valid-deref) 1 wit inspect .59   18    - wit inspect
ldv-memsafety/memset_false-valid-deref-write.c false(valid-deref) 1 wit inspect 4.7 280 40 false(valid-deref) 1 wit inspect 2.7  250 true -32 wit inspect 3.9   270   false(valid-deref) 1 wit inspect .60   18    - wit inspect
ldv-memsafety/ArraysOfVariableLength2_true-valid-memsafety.c timeout 0 wit inspect 900   5100 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.9
ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c true 2 wit inspect 8.6 470 65 - wit inspect - wit inspect - wit inspect true 2 wit inspect 11     450  
ldv-memsafety/ArraysOfVariableLength5_true-valid-memsafety.c true 2 wit inspect 9.6 530 73 - wit inspect - wit inspect - wit inspect true 2 wit inspect 13     500  
ldv-memsafety/ArraysOfVariableLength6_true-valid-memsafety_true-termination.c true 2 wit inspect 8.4 470 67 - wit inspect - wit inspect - wit inspect true 2 wit inspect 12     460  
ldv-memsafety/ArraysOfVariableLength_true-valid-memsafety.c true 2 wit inspect 10   520 85 - wit inspect - wit inspect - wit inspect true 2 wit inspect 14     490  
ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety_true-termination.c true 2 wit inspect 8.6 460 76 - wit inspect - wit inspect - wit inspect true 2 wit inspect 13     450  
ldv-memsafety/StructInitialization1_true-valid-memsafety.c error (7) 0 wit inspect 3.6 220 32 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
ldv-memsafety/StructInitialization2_true-valid-memsafety.c error (7) 0 wit inspect 3.6 220 32 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 5.0
ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c true 2 wit inspect 3.9 230 32 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7   210  
ldv-memsafety/memset2_true-valid-memsafety_true-termination.c true 2 wit inspect 6.3 310 50 - 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 6.4 300 55 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.3   290  
ldv-memsafety/memsetNonZero2_true-valid-memsafety_true-termination.c true 2 wit inspect 6.3 300 51 - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.6   330  
ldv-memsafety/memsetNonZero3_true-valid-memsafety_true-termination.c true 2 wit inspect 6.2 310 51 - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.3   290  
ldv-memsafety/memsetNonZero_true-valid-memsafety_true-termination.c true 2 wit inspect 6.5 300 56 - wit inspect - wit inspect - wit inspect true 2 wit inspect 12     300  
ldv-memsafety/memset_true-valid-memsafety_true-termination.c true 2 wit inspect 6.3 300 55 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.8   300  
ldv-memsafety/memleaks_test14_3_false-valid-deref.i false(valid-deref) 0 wit inspect 34   860 310 true -32 wit inspect 3.8  250 true -32 wit inspect 9.0   340   error (1) 0 wit inspect .61   19    - wit inspect
ldv-memsafety/memleaks_test22_3_false-valid-deref.i timeout 0 wit inspect 900   3300 8700 error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
ldv-memsafety/memleaks_test22_5_false-valid-deref.i timeout 0 wit inspect 900   3100 8800 error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0012 .31 - wit inspect
ldv-memsafety/memleaks_test23_2_false-valid-deref.i false(valid-deref) 0 wit inspect 310   1200 3200 true -32 wit inspect 6.6  260 true -32 wit inspect 9.3   340   error (1) 0 wit inspect .61   19    - wit inspect
ldv-memsafety/memleaks_test23_4_false-valid-deref.i false(valid-deref) 0 wit inspect 97   1200 1100 true -32 wit inspect 4.0  250 true -32 wit inspect 11     550   error (1) 0 wit inspect .60   19    - wit inspect
ldv-memsafety/memleaks_test11_1_false-valid-free.i false(valid-free) 1 wit inspect 650   880 8600 false(valid-free) 1 wit inspect 5.9  250 true -32 wit inspect 58     560   error (1) 0 wit inspect .62   19    - wit inspect
ldv-memsafety/memleaks_test12_false-valid-free.i timeout 0 wit inspect 900   1400 9000 error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0012 .29 - wit inspect
ldv-memsafety/memleaks_test17_2_false-valid-free.i timeout 0 wit inspect 900   2400 11000 error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect
ldv-memsafety/memleaks_test19_false-valid-free.i false(valid-free) 1 wit inspect 130   990 1500 false(valid-free) 1 wit inspect 4.3  270 false(valid-free) 1 wit inspect 9.9   370   error (1) 0 wit inspect .60   19    - wit inspect
ldv-memsafety/memleaks_test1_false-valid-free.i false(valid-free) 1 wit inspect 5.9 290 45 false(valid-free) 1 wit inspect 3.6  250 true -32 wit inspect 5.8   260   error (1) 0 wit inspect .60   18    - wit inspect
ldv-memsafety/memleaks_test3_false-valid-free.i false(valid-free) 1 wit inspect 4.4 250 38 false(valid-free) 1 wit inspect 4.2  270 false(valid-free) 1 wit inspect 5.8   260   error (1) 0 wit inspect .60   18    - wit inspect
ldv-memsafety/memleaks_test6_2_false-valid-free.i false(valid-free) 1 wit inspect 12   540 110 false(valid-free) 1 wit inspect 3.8  260 false(valid-free) 1 wit inspect 8.4   290   error (1) 0 wit inspect .60   18    - wit inspect
ldv-memsafety/memleaks_test8_2_false-valid-free.i false(valid-free) 1 wit inspect 6.0 290 52 false(valid-free) 1 wit inspect 4.1  270 false(valid-free) 1 wit inspect 6.9   260   error (1) 0 wit inspect .63   18    - wit inspect
ldv-memsafety/memleaks_test10_false-valid-memtrack_true-termination.i timeout 0 wit inspect 900   880 13000 error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .026 5.0 error (invalid witness file) 0 wit inspect .0012 .35 - wit inspect
ldv-memsafety/memleaks_test11_2_false-valid-memtrack_true-termination.i timeout 0 wit inspect 900   860 13000 error (invalid witness file) 0 wit inspect .77 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
ldv-memsafety/memleaks_test13_1_false-valid-memtrack_true-termination.i unknown 0 wit inspect 29   680 280 error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
ldv-memsafety/memleaks_test13_2_false-valid-memtrack.i unknown 0 wit inspect 230   1000 2800 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
ldv-memsafety/memleaks_test14_1_false-valid-memtrack_true-termination.i unknown 0 wit inspect 26   570 250 error (invalid witness file) 0 wit inspect .40 42 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0013 .28 - wit inspect
ldv-memsafety/memleaks_test14_2_false-valid-memtrack.i unknown 0 wit inspect 190   1100 2000 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect
ldv-memsafety/memleaks_test15_false-valid-memtrack.i timeout 0 wit inspect 900   990 12000 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0033 .34 - wit inspect
ldv-memsafety/memleaks_test16_1_false-valid-memtrack_true-termination.i unknown 0 wit inspect 15   370 120 error (invalid witness file) 0 wit inspect .52 45 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0034 .26 - wit inspect
ldv-memsafety/memleaks_test16_2_false-valid-memtrack_true-termination.i unknown 0 wit inspect 10   290 84 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect
ldv-memsafety/memleaks_test17_1_false-valid-memtrack.i timeout 0 wit inspect 900   2400 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 .33 - wit inspect
ldv-memsafety/memleaks_test17_3_false-valid-memtrack.i error (7) 0 wit inspect 620   840 7200 error (invalid witness file) 0 wit inspect .77 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
ldv-memsafety/memleaks_test18_1_false-valid-memtrack_true-termination.i unknown 0 wit inspect 61   540 750 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0012 .35 - wit inspect
ldv-memsafety/memleaks_test18_2_false-valid-memtrack_true-termination.i timeout 0 wit inspect 900   1400 10000 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
ldv-memsafety/memleaks_test18_3_false-valid-memtrack_true-termination.i timeout 0 wit inspect 900   1000 12000 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
ldv-memsafety/memleaks_test1_false-valid-memtrack_true-termination.i unknown 0 wit inspect 9.8 280 90 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .017 4.9 error (invalid witness file) 0 wit inspect .0011 .33 - wit inspect
ldv-memsafety/memleaks_test20_false-valid-memtrack_true-termination.i unknown 0 wit inspect 11   320 89 error (invalid witness file) 0 wit inspect .78 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0014 .35 - wit inspect
ldv-memsafety/memleaks_test21_false-valid-memtrack_true-termination.i unknown 0 wit inspect 9.9 280 89 error (invalid witness file) 0 wit inspect .72 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect
ldv-memsafety/memleaks_test22_1_false-valid-memtrack_true-termination.i unknown 0 wit inspect 230   850 2700 error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0013 .27 - wit inspect
ldv-memsafety/memleaks_test22_2_false-valid-memtrack_true-termination.i unknown 0 wit inspect 45   710 430 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 .34 - wit inspect
ldv-memsafety/memleaks_test22_4_false-valid-memtrack_true-termination.i unknown 0 wit inspect 240   920 2800 error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect
ldv-memsafety/memleaks_test4_false-valid-memtrack_true-termination.i unknown 0 wit inspect 13   350 120 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0037 .30 - wit inspect
ldv-memsafety/memleaks_test5_1_false-valid-memtrack_true-termination.i unknown 0 wit inspect 10   290 80 error (invalid witness file) 0 wit inspect .52 44 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .0013 .32 - wit inspect
ldv-memsafety/memleaks_test5_2_false-valid-memtrack_true-termination.i unknown 0 wit inspect 12   350 110 error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .0018 .28 - wit inspect
ldv-memsafety/memleaks_test6_1_false-valid-memtrack_true-termination.i unknown 0 wit inspect 39   550 370 error (invalid witness file) 0 wit inspect .39 42 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0027 .34 - wit inspect
ldv-memsafety/memleaks_test6_3_false-valid-memtrack_true-termination.i unknown 0 wit inspect 80   550 970 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0011 .29 - wit inspect
ldv-memsafety/memleaks_test7_false-valid-memtrack_true-termination.i unknown 0 wit inspect 20   560 180 error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect
ldv-memsafety/memleaks_test8_1_false-valid-memtrack_true-termination.i unknown 0 wit inspect 10   300 77 error (invalid witness file) 0 wit inspect .81 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
ldv-memsafety/memleaks_test9_1_false-valid-memtrack_true-termination.i unknown 0 wit inspect 12   350 110 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect
ldv-memsafety/memleaks_test9_2_false-valid-memtrack_true-termination.i unknown 0 wit inspect 10   290 80 error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect .0012 .28 - wit inspect
ldv-memsafety/memleaks_test10_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   890 9300 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
ldv-memsafety/memleaks_test11_true-valid-memsafety_true-termination.i true 2 wit inspect 530   1100 7100 - wit inspect - wit inspect - wit inspect true 2 wit inspect 880     1100  
ldv-memsafety/memleaks_test12_true-valid-memsafety.i timeout 0 wit inspect 900   1300 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
ldv-memsafety/memleaks_test13_true-valid-memsafety.i true 2 wit inspect 71   1200 660 - wit inspect - wit inspect - wit inspect true 2 wit inspect 85     980  
ldv-memsafety/memleaks_test14_true-valid-memsafety.i true 2 wit inspect 60   1100 640 - wit inspect - wit inspect - wit inspect true 2 wit inspect 90     1000  
ldv-memsafety/memleaks_test15_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   840 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 5.0
ldv-memsafety/memleaks_test16_true-valid-memsafety_true-termination.i true 2 wit inspect 8.6 470 76 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.8   450  
ldv-memsafety/memleaks_test17_1_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   2400 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
ldv-memsafety/memleaks_test17_2_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   1800 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
ldv-memsafety/memleaks_test18_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   1100 13000 - 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 310   960 3800 - wit inspect - wit inspect - wit inspect true 2 wit inspect 370     870  
ldv-memsafety/memleaks_test1_true-valid-memsafety_true-termination.i true 2 wit inspect 6.8 320 52 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.4   280  
ldv-memsafety/memleaks_test20_true-valid-memsafety_true-termination.i true 2 wit inspect 8.8 480 73 - wit inspect - wit inspect - wit inspect true 2 wit inspect 11     480  
ldv-memsafety/memleaks_test21_true-valid-memsafety_true-termination.i true 2 wit inspect 8.7 450 65 - wit inspect - wit inspect - wit inspect true 2 wit inspect 11     430  
ldv-memsafety/memleaks_test22_1_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   2600 9700 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
ldv-memsafety/memleaks_test22_2_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   3000 10000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
ldv-memsafety/memleaks_test22_3_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900   3100 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
ldv-memsafety/memleaks_test23_1_true-valid-memsafety.i timeout 0 wit inspect 900   1200 10000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
ldv-memsafety/memleaks_test23_3_true-valid-memsafety.i timeout 0 wit inspect 900   1300 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.4 370 66 - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.0   340  
ldv-memsafety/memleaks_test4_true-valid-memsafety_true-termination.i true 2 wit inspect 23   540 220 - wit inspect - wit inspect - wit inspect true 2 wit inspect 29     510  
ldv-memsafety/memleaks_test5_true-valid-memsafety_true-termination.i true 2 wit inspect 8.3 420 71 - wit inspect - wit inspect - wit inspect true 2 wit inspect 11     410  
ldv-memsafety/memleaks_test6_true-valid-memsafety_true-termination.i true 2 wit inspect 14   600 110 - wit inspect - wit inspect - wit inspect true 2 wit inspect 17     570  
ldv-memsafety/memleaks_test7_true-valid-memsafety_true-termination.i true 2 wit inspect 12   520 110 - wit inspect - wit inspect - wit inspect true 2 wit inspect 17     540  
ldv-memsafety/memleaks_test8_true-valid-memsafety_true-termination.i true 2 wit inspect 7.4 360 60 - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.3   340  
ldv-memsafety/memleaks_test9_true-valid-memsafety_true-termination.i true 2 wit inspect 7.8 360 58 - wit inspect - wit inspect - wit inspect true 2 wit inspect 11     350  
ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety_true-termination.i unknown 0 wit inspect 3.5 220 28 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
ldv-memsafety-bitfields/test-bitfields-2.1_true-valid-memsafety_true-termination.i unknown 0 wit inspect 3.4 220 31 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety_true-termination.i unknown 0 wit inspect 3.3 220 27 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 5.0
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 .019 5.0
ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i unknown 0 wit inspect 3.4 220 27 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .047 4.9
ldv-memsafety-bitfields/test-bitfields-1_false-valid-deref.i unknown 0 wit inspect 3.4 220 29 error (invalid witness file) 0 wit inspect .83 42 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i unknown 0 wit inspect 3.5 220 30 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .0037 .26 - wit inspect
ldv-memsafety-bitfields/test-bitfields-3.1_false-valid-deref.i unknown 0 wit inspect 3.5 230 30 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0017 .26 - wit inspect
ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i unknown 0 wit inspect 3.3 220 28 error (invalid witness file) 0 wit inspect .64 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0013 .30 - wit inspect
ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i unknown 0 wit inspect 3.6 220 29 error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .0011 .33 - 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 87 70000 190000 860000 90 -107 230 11000 90 -519 270   11000 90 -53 210   510 90 64 1900 16000
    correct results 55 87 3000 31000 37000 21 21 78 5300 9 9 86   5100 11 11 7.1 210 32 64 1900 16000
        correct true 32 64 1300 16000 16000 0 0 0 32 64 1900 16000
        correct false 23 23 1700 15000 21000 21 21 78 5300 9 9 86   5100 11 11 7.1 210 0
    correct-unconfimed results 3 0 440 3300 4500 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 3 0 440 3300 4500 0 0 0 0
    incorrect results 0 4 -128 18 1000 17 -528 180   5600 2 -64 1.3 37 0
        incorrect true 0 4 -128 18 1000 16 -512 170   5300 2 -64 1.3 37 0
        incorrect false 0 0 1 -16 6.2 280 0 0
score (180 tasks, max score: 270) 87 -107 -519 -53 64
Run set uautomizer.sv-comp18.MemSafety-Heap cpa-seq-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.MemSafety-Heap uautomizer-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.MemSafety-Heap fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.MemSafety-Heap uautomizer-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.MemSafety-Heap