Tool ESBMC ESBMC version 4.6.0 64-bit x86_64 linux 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* [apollon077; apollon078; apollon081; apollon164] [apollon052; apollon077; apollon078; apollon160] [apollon077; apollon078] [apollon040; apollon066; apollon077; apollon078; apollon139; apollon161]
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: [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] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 4, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33554 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-02 11:31:00 CET 2017-12-02 13:19:03 CET 2017-12-02 13:40:51 CET 2017-12-02 13:42:37 CET 2017-12-02 13:21:13 CET
Run set esbmc-kind.sv-comp18.MemSafety-Heap cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.MemSafety-Heap uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.MemSafety-Heap fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.MemSafety-Heap uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.MemSafety-Heap
Options -s kinduction -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-02_1131.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/esbmc-kind.2017-12-02_1131.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/esbmc-kind.2017-12-02_1131.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/esbmc-kind.2017-12-02_1131.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 false(valid-deref) 0 wit inspect 29     110 290    true -32 wit inspect 6.6  650 true -32 wit inspect 4.0   250   error (2) 0 wit inspect .82   21    - wit inspect
memsafety/test-0137_false-valid-deref.i false(valid-deref) 0 wit inspect 1.2   43 12    error (invalid witness file) 0 wit inspect 2.6  180 true -32 wit inspect 5.9   270   error (1) 0 wit inspect .62   19    - wit inspect
memsafety/test-0235_false-valid-deref.i out of memory 0 wit inspect 790     15000 6900    error (invalid witness file) 0 wit inspect .40 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0010 .26 - wit inspect
memsafety/960521-1_false-valid-free.i false(valid-free) 1 wit inspect 31     110 250    true -32 wit inspect 6.6  650 true -32 wit inspect 5.2   240   false(valid-free) 1 wit inspect .82   21    - wit inspect
memsafety/test-0158_false-valid-free.i false(valid-free) 1 wit inspect .39  29 3.7  true -32 wit inspect 2.4  250 true -32 wit inspect 5.2   230   false(valid-free) 1 wit inspect .64   19    - wit inspect
memsafety/test-0232_false-valid-free.i false(valid-free) 1 wit inspect .49  29 5.7  false(valid-free) 1 wit inspect 3.5  250 true -32 wit inspect 5.5   240   true -32 wit inspect .63   18    - wit inspect
memsafety/20020406-1_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 29     1100 320    error (recursion) 0 wit inspect 2.8  260 true -32 wit inspect 6.6   280   true -32 wit inspect .70   18    - wit inspect
memsafety/20051113-1.c_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 6.0   89 73    true -32 wit inspect 2.3  260 true -32 wit inspect 5.7   240   true -32 wit inspect .68   19    - wit inspect
memsafety/lockfree-3.1_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 2.2   44 27    timeout 0 wit inspect 96    2200 true -32 wit inspect 3.9   240   true -32 wit inspect .64   18    - wit inspect
memsafety/lockfree-3.2_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .11  27 1.3  timeout 0 wit inspect 91    2300 true -32 wit inspect 3.6   250   true -32 wit inspect .65   18    - wit inspect
memsafety/lockfree-3.3_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 8.4   89 110    timeout (exception) 0 wit inspect 92    2200 true -32 wit inspect 3.8   240   true -32 wit inspect .69   18    - wit inspect
memsafety/test-0019_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .18  28 1.8  true -32 wit inspect 3.6  270 true -32 wit inspect 5.3   230   true -32 wit inspect .67   18    - wit inspect
memsafety/test-0102_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 3.2   56 30    timeout 0 wit inspect 98    3200 true -32 wit inspect 4.3   260   false(valid-deref) -16 wit inspect .65   19    - wit inspect
memsafety/test-0158_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .11  27 .87 true -32 wit inspect 3.5  240 true -32 wit inspect 4.8   240   true -32 wit inspect .62   18    - wit inspect
memsafety/test-0220_false-valid-memtrack.i out of memory 0 wit inspect 310     15000 2800    error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
memsafety/test-0232_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .35  28 3.9  timeout 0 wit inspect 91    1800 true -32 wit inspect 5.3   240   true -32 wit inspect .64   18    - wit inspect
memsafety/test-0234_false-valid-memtrack.i timeout 0 wit inspect 900     8800 7700    error (invalid witness file) 0 wit inspect .43 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0035 .30 - wit inspect
memsafety/test-0235_false-valid-memtrack.i out of memory 0 wit inspect 780     15000 6700    error (invalid witness file) 0 wit inspect .43 44 error (2) 0 wit inspect .033 4.8 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
memsafety/960521-1_true-valid-memsafety.i timeout 0 wit inspect 900     9900 9700    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .028 4.8
memsafety/lockfree-3.0_true-valid-memsafety.i timeout 0 wit inspect 900     640 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.9
memsafety/test-0019_true-valid-memsafety_true-termination.i true 2 wit inspect .12  27 1.4  - wit inspect - wit inspect - wit inspect true 2 wit inspect 28     500  
memsafety/test-0102_true-valid-memsafety.i timeout 0 wit inspect 900     900 8200    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
memsafety/test-0134_true-valid-memsafety.i timeout 0 wit inspect 900     1900 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 5.0
memsafety/test-0158_true-valid-memsafety_true-termination.i true 2 wit inspect .18  27 1.6  - wit inspect - wit inspect - wit inspect true 2 wit inspect 17     390  
memsafety/test-0214_true-valid-memsafety_false-termination.i timeout 0 wit inspect 900     920 9400    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
memsafety/test-0217_true-valid-memsafety_false-termination.i out of memory 0 wit inspect 180     15000 1900    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
memsafety/test-0218_true-valid-memsafety_false-termination.i out of memory 0 wit inspect 130     15000 1500    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.8
memsafety/test-0219_true-valid-memsafety.i out of memory 0 wit inspect 120     15000 1700    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
memsafety/test-0232_true-valid-memsafety.i timeout 0 wit inspect 900     730 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
memsafety/test-0234_true-valid-memsafety.i timeout 0 wit inspect 900     8200 6300    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
memsafety/test-0235_true-valid-memsafety.i out of memory 0 wit inspect 770     15000 6600    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 5.0
memsafety/test-0236_true-valid-memsafety.i unknown 0 wit inspect .49  36 5.5  - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
memsafety/test-0237_true-valid-memsafety.i out of memory 0 wit inspect 110     15000 1400    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
memsafety/test-0504_true-valid-memsafety.i timeout 0 wit inspect 900     690 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
memsafety/test-0513_true-valid-memsafety.i timeout 0 wit inspect 900     1100 11000    - 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     1100 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
memsafety/test-memleak_nexttime_true-valid-memsafety_true-termination.i true 2 wit inspect .67  29 9.1  - wit inspect - wit inspect - wit inspect error (7) 0 wit inspect 230     890  
memsafety-ext/dll_extends_pointer_true-valid-memsafety.i timeout 0 wit inspect 900     370 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
memsafety-ext/skiplist_2lvl_true-valid-memsafety.i timeout 0 wit inspect 900     230 13000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
memsafety-ext/skiplist_3lvl_true-valid-memsafety.i timeout 0 wit inspect 900     210 11000    - 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     450 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 900     620 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.9
memsafety-ext/tree_of_cslls_true-valid-memsafety.i timeout 0 wit inspect 900     990 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
memsafety-ext/tree_parent_ptr_true-valid-memsafety_false-termination.i timeout 0 wit inspect 900     670 10000    - 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     2000 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
memsafety-ext2/split_list_test05_false-valid-deref.i out of memory 0 wit inspect 100     15000 1100    error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .038 4.8 error (invalid witness file) 0 wit inspect .0013 .28 - wit inspect
memsafety-ext2/complex_data_creation_test01_false-valid-memtrack.i timeout 0 wit inspect 900     1800 9600    error (invalid witness file) 0 wit inspect .41 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0010 .26 - wit inspect
memsafety-ext2/complex_data_creation_test02_false-valid-memtrack.i timeout 0 wit inspect 900     2300 11000    error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0010 .26 - wit inspect
memsafety-ext2/length_test03_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 7.4   54 72    error (invalid witness file) 0 wit inspect 1.9  180 true -32 wit inspect 6.0   250   error (1) 0 wit inspect .58   19    - wit inspect
memsafety-ext2/optional_data_creation_test04_false-valid-memtrack.i timeout 0 wit inspect 900     550 10000    error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0041 .28 - wit inspect
memsafety-ext2/complex_data_creation_test01_true-valid-memsafety.i timeout 0 wit inspect 900     1800 9900    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.9
memsafety-ext2/complex_data_creation_test02_true-valid-memsafety.i timeout 0 wit inspect 900     2100 11000    - 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     620 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
memsafety-ext2/optional_data_creation_test04_true-valid-memsafety.i timeout 0 wit inspect 900     450 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
memsafety-ext2/split_list_test05_true-valid-memsafety.i out of memory 0 wit inspect 110     15000 910    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .036 4.9
list-ext-properties/960521-1_1_false-valid-deref.i false(valid-deref) 0 wit inspect .25  29 2.3  true -32 wit inspect 8.5  760 true -32 wit inspect 5.0   230   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 130     210 1600    false(valid-deref) 1 wit inspect 3.9  280 true -32 wit inspect 4.2   250   false(valid-deref) 1 wit inspect .66   19    - wit inspect
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i false(valid-deref) 0 wit inspect .26  29 2.7  error (invalid witness file) 0 wit inspect 2.6  180 true -32 wit inspect 3.8   240   error (1) 0 wit inspect .60   18    - wit inspect
list-ext-properties/960521-1_1_false-valid-free.i false(valid-free) 1 wit inspect .26  29 2.2  true -32 wit inspect 12    680 true -32 wit inspect 5.2   230   false(valid-free) 1 wit inspect .64   18    - wit inspect
list-ext-properties/test-0158_1_false-valid-free.i false(valid-free) 0 wit inspect .38  28 3.2  true -32 wit inspect 2.4  250 true -32 wit inspect 3.4   240   error (2) 0 wit inspect .64   18    - wit inspect
list-ext-properties/test-0019_1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .27  28 2.9  true -32 wit inspect 3.3  240 true -32 wit inspect 5.1   240   true -32 wit inspect .63   18    - wit inspect
list-ext-properties/test-0158_1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .10  27 .88 true -32 wit inspect 2.4  250 true -32 wit inspect 4.8   230   true -32 wit inspect .65   18    - wit inspect
list-ext-properties/test-0232_1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .64  29 5.3  true -32 wit inspect 4.6  270 true -32 wit inspect 4.0   240   true -32 wit inspect .64   18    - wit inspect
list-ext-properties/960521-1_1_true-valid-memsafety.i true 2 wit inspect 6.2   39 75    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     1000  
list-ext-properties/list-ext_1_true-valid-memsafety.i true 2 wit inspect 200     210 2400    - wit inspect - wit inspect - wit inspect error (7) 0 wit inspect 350     810  
list-ext-properties/list-ext_flag_1_true-valid-memsafety.i true 2 wit inspect 60     110 810    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     2200  
list-ext-properties/simple-ext_1_true-valid-memsafety.i true 2 wit inspect 230     190 2400    - wit inspect - wit inspect - wit inspect error (7) 0 wit inspect 500     880  
list-ext-properties/test-0019_1_true-valid-memsafety_true-termination.i true 2 wit inspect .12  27 1.4  - 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 .18  27 1.9  - wit inspect - wit inspect - wit inspect true 2 wit inspect 17     380  
list-ext-properties/test-0214_1_true-valid-memsafety.i timeout 0 wit inspect 900     4700 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
list-ext-properties/test-0217_1_true-valid-memsafety.i timeout 0 wit inspect 900     2900 9800    - 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 100     240 1100    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     910  
list-ext-properties/test-0504_1_true-valid-memsafety.i true 2 wit inspect 160     160 1900    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     1200  
list-ext-properties/test-0513_1_true-valid-memsafety.i true 2 wit inspect 12     170 150    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     760  
memory-alloca/c.03-alloca_true-valid-memsafety.i timeout 0 wit inspect 900     650 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c false(valid-deref) 1 wit inspect .19  29 1.9  false(valid-deref) 1 wit inspect 3.4  250 true -32 wit inspect 5.1   230   timeout 0 wit inspect 96      18    - wit inspect
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-write.c false(valid-deref) 1 wit inspect .17  29 1.7  false(valid-deref) 1 wit inspect 3.1  260 true -32 wit inspect 3.5   240   timeout 0 wit inspect 96      18    - wit inspect
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-read.c false(valid-deref) 1 wit inspect .11  28 .65 false(valid-deref) 1 wit inspect 1.9  240 true -32 wit inspect 3.4   230   true -32 wit inspect .57   19    - wit inspect
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-write.c false(valid-deref) 1 wit inspect .077 28 .99 false(valid-deref) 1 wit inspect 2.2  250 true -32 wit inspect 3.3   230   true -32 wit inspect .58   18    - wit inspect
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c false(valid-deref) 1 wit inspect 2.8   44 40    false(valid-deref) 1 wit inspect 5.2  410 true -32 wit inspect 3.2   230   false(valid-deref) 1 wit inspect .58   18    - wit inspect
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-write.c false(valid-deref) 1 wit inspect 2.8   45 40    false(valid-deref) 1 wit inspect 5.5  420 true -32 wit inspect 5.4   250   false(valid-deref) 1 wit inspect .58   18    - wit inspect
ldv-memsafety/memset2_false-valid-deref-write.c false(valid-deref) 1 wit inspect 1.6   44 20    true -32 wit inspect 1.9  250 true -32 wit inspect 4.5   230   false(valid-deref) 1 wit inspect .58   18    - wit inspect
ldv-memsafety/memset3_false-valid-deref-write.c false(valid-deref) 1 wit inspect 18     350 230    true -32 wit inspect 1.9  240 true -32 wit inspect 3.3   230   false(valid-deref) 1 wit inspect .57   18    - wit inspect
ldv-memsafety/memsetNonZero2_false-valid-deref-write.c false(valid-deref) 1 wit inspect 1.6   44 23    true -32 wit inspect 2.1  270 true -32 wit inspect 3.3   230   false(valid-deref) 1 wit inspect .58   18    - wit inspect
ldv-memsafety/memsetNonZero3_false-valid-deref-write.c false(valid-deref) 1 wit inspect 18     350 260    true -32 wit inspect 2.0  250 true -32 wit inspect 4.6   230   false(valid-deref) 1 wit inspect .58   18    - wit inspect
ldv-memsafety/memsetNonZero_false-valid-deref-write.c false(valid-deref) 1 wit inspect 18     350 260    true -32 wit inspect 2.1  270 true -32 wit inspect 4.7   240   false(valid-deref) 1 wit inspect .60   18    - wit inspect
ldv-memsafety/memset_false-valid-deref-write.c false(valid-deref) 1 wit inspect 18     350 220    true -32 wit inspect 3.2  240 true -32 wit inspect 4.6   240   false(valid-deref) 1 wit inspect .58   18    - wit inspect
ldv-memsafety/ArraysOfVariableLength2_true-valid-memsafety.c timeout 0 wit inspect 900     2800 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c true 2 wit inspect 1.1   29 17    - wit inspect - wit inspect - wit inspect true 2 wit inspect 11     450  
ldv-memsafety/ArraysOfVariableLength5_true-valid-memsafety.c true 2 wit inspect 2.7   42 41    - wit inspect - wit inspect - wit inspect true 2 wit inspect 15     480  
ldv-memsafety/ArraysOfVariableLength6_true-valid-memsafety_true-termination.c true 2 wit inspect 1.1   30 17    - wit inspect - wit inspect - wit inspect true 2 wit inspect 11     470  
ldv-memsafety/ArraysOfVariableLength_true-valid-memsafety.c true 2 wit inspect 83     840 920    - wit inspect - wit inspect - wit inspect true 2 wit inspect 14     510  
ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety_true-termination.c true 2 wit inspect 3.0   45 39    - wit inspect - wit inspect - wit inspect true 2 wit inspect 14     460  
ldv-memsafety/StructInitialization1_true-valid-memsafety.c true 2 wit inspect .11  29 1.3  - wit inspect - wit inspect - wit inspect error (7) 0 wit inspect 3.6   200  
ldv-memsafety/StructInitialization2_true-valid-memsafety.c true 2 wit inspect .10  29 1.2  - wit inspect - wit inspect - wit inspect error (7) 0 wit inspect 3.6   210  
ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c true 2 wit inspect .082 26 .95 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1   220  
ldv-memsafety/memset2_true-valid-memsafety_true-termination.c true 2 wit inspect 1.7   44 25    - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.7   280  
ldv-memsafety/memset3_true-valid-memsafety_true-termination.c true 2 wit inspect 19     360 220    - wit inspect - wit inspect - wit inspect true 2 wit inspect 10     280  
ldv-memsafety/memsetNonZero2_true-valid-memsafety_true-termination.c true 2 wit inspect 1.7   44 24    - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.5   290  
ldv-memsafety/memsetNonZero3_true-valid-memsafety_true-termination.c true 2 wit inspect 19     360 290    - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.1   290  
ldv-memsafety/memsetNonZero_true-valid-memsafety_true-termination.c true 2 wit inspect 19     360 260    - wit inspect - wit inspect - wit inspect true 2 wit inspect 11     300  
ldv-memsafety/memset_true-valid-memsafety_true-termination.c true 2 wit inspect 19     360 280    - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.7   290  
ldv-memsafety/memleaks_test14_3_false-valid-deref.i false(valid-deref) 0 wit inspect 1.5   34 15    true -32 wit inspect 3.2  260 true -32 wit inspect 5.8   250   error (1) 0 wit inspect .62   18    - wit inspect
ldv-memsafety/memleaks_test22_3_false-valid-deref.i false(valid-deref) 0 wit inspect 2.1   30 17    true -32 wit inspect 2.8  260 true -32 wit inspect 5.4   240   error (1) 0 wit inspect .58   19    - wit inspect
ldv-memsafety/memleaks_test22_5_false-valid-deref.i false(valid-deref) 0 wit inspect 2.1   30 20    true -32 wit inspect 4.2  260 true -32 wit inspect 5.5   250   error (1) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/memleaks_test23_2_false-valid-deref.i timeout 0 wit inspect 900     2600 8900    error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .037 4.9 error (invalid witness file) 0 wit inspect .0011 .27 - wit inspect
ldv-memsafety/memleaks_test23_4_false-valid-deref.i timeout 0 wit inspect 900     2600 10000    error (invalid witness file) 0 wit inspect .43 41 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
ldv-memsafety/memleaks_test11_1_false-valid-free.i false(valid-free) 0 wit inspect 1.6   33 14    true -32 wit inspect 4.3  260 true -32 wit inspect 5.2   250   error (1) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/memleaks_test12_false-valid-free.i unknown 0 wit inspect 15     180 180    error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0010 .26 - wit inspect
ldv-memsafety/memleaks_test17_2_false-valid-free.i false(valid-free) 0 wit inspect 15     120 160    true -32 wit inspect 4.4  270 true -32 wit inspect 3.9   240   error (1) 0 wit inspect .59   19    - wit inspect
ldv-memsafety/memleaks_test19_false-valid-free.i false(valid-free) 1 wit inspect .29  30 2.4  false(valid-free) 1 wit inspect 3.9  260 true -32 wit inspect 3.6   240   error (1) 0 wit inspect .59   18    - wit inspect
ldv-memsafety/memleaks_test1_false-valid-free.i false(valid-free) 1 wit inspect .12  29 1.5  false(valid-free) 1 wit inspect 2.6  250 true -32 wit inspect 6.3   260   error (1) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/memleaks_test3_false-valid-free.i false(valid-free) 1 wit inspect .15  29 1.3  false(valid-free) 1 wit inspect 2.6  250 false(valid-free) 1 wit inspect 3.4   260   error (1) 0 wit inspect .58   19    - wit inspect
ldv-memsafety/memleaks_test6_2_false-valid-free.i false(valid-free) 1 wit inspect .30  29 3.3  false(valid-free) 1 wit inspect 4.0  250 true -32 wit inspect 5.2   240   error (1) 0 wit inspect .63   18    - wit inspect
ldv-memsafety/memleaks_test8_2_false-valid-free.i false(valid-free) 1 wit inspect .18  29 1.3  false(valid-free) 1 wit inspect 4.0  250 false(valid-free) 1 wit inspect 7.6   270   error (1) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/memleaks_test10_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .78  32 7.4  true -32 wit inspect 4.7  260 true -32 wit inspect 5.2   240   error (1) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/memleaks_test11_2_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect 1.1   32 17    true -32 wit inspect 4.1  260 true -32 wit inspect 4.0   250   error (1) 0 wit inspect .59   18    - wit inspect
ldv-memsafety/memleaks_test13_1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .23  29 2.7  true -32 wit inspect 2.7  260 true -32 wit inspect 5.8   260   error (1) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/memleaks_test13_2_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 1.5   34 16    true -32 wit inspect 5.0  260 true -32 wit inspect 3.9   250   error (1) 0 wit inspect .63   19    - wit inspect
ldv-memsafety/memleaks_test14_1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .26  29 2.3  true -32 wit inspect 3.9  260 true -32 wit inspect 3.6   240   error (1) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/memleaks_test14_2_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 2.0   34 18    true -32 wit inspect 2.9  260 true -32 wit inspect 5.5   240   error (1) 0 wit inspect .58   19    - wit inspect
ldv-memsafety/memleaks_test15_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 2.1   37 24    true -32 wit inspect 2.9  260 true -32 wit inspect 4.2   260   error (1) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/memleaks_test16_1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .24  29 2.1  true -32 wit inspect 4.2  260 true -32 wit inspect 4.8   240   error (1) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/memleaks_test16_2_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .14  29 1.5  true -32 wit inspect 2.5  250 true -32 wit inspect 3.4   240   error (1) 0 wit inspect .58   19    - wit inspect
ldv-memsafety/memleaks_test17_1_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 11     120 140    true -32 wit inspect 5.7  260 true -32 wit inspect 3.9   260   error (1) 0 wit inspect .59   19    - wit inspect
ldv-memsafety/memleaks_test17_3_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 18     84 190    true -32 wit inspect 3.9  270 true -32 wit inspect 5.3   240   error (1) 0 wit inspect .59   19    - wit inspect
ldv-memsafety/memleaks_test18_1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .35  31 4.4  true -32 wit inspect 5.3  260 true -32 wit inspect 4.9   230   error (1) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/memleaks_test18_2_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect 48     97 590    true -32 wit inspect 6.0  310 true -32 wit inspect 5.1   230   error (1) 0 wit inspect .58   19    - wit inspect
ldv-memsafety/memleaks_test18_3_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect 13     37 160    true -32 wit inspect 88    2200 true -32 wit inspect 3.4   230   error (1) 0 wit inspect .62   18    - wit inspect
ldv-memsafety/memleaks_test1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .12  28 1.0  true -32 wit inspect 2.4  250 true -32 wit inspect 5.0   230   error (1) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/memleaks_test20_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .11  28 1.3  true -32 wit inspect 2.6  260 true -32 wit inspect 4.7   230   error (1) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/memleaks_test21_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .11  28 1.1  true -32 wit inspect 2.6  250 true -32 wit inspect 5.2   230   error (1) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/memleaks_test22_1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect 1.8   30 24    true -32 wit inspect 2.8  260 true -32 wit inspect 4.2   270   error (1) 0 wit inspect .63   19    - wit inspect
ldv-memsafety/memleaks_test22_2_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .59  29 7.7  true -32 wit inspect 4.2  260 true -32 wit inspect 5.1   240   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 2.0   30 22    true -32 wit inspect 4.1  260 true -32 wit inspect 4.2   260   error (1) 0 wit inspect .58   19    - wit inspect
ldv-memsafety/memleaks_test4_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .23  29 1.9  true -32 wit inspect 2.9  260 true -32 wit inspect 3.4   240   error (1) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/memleaks_test5_1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .11  28 1.1  true -32 wit inspect 3.9  260 true -32 wit inspect 3.3   240   error (1) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/memleaks_test5_2_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .11  28 1.0  true -32 wit inspect 3.7  260 true -32 wit inspect 4.8   230   error (1) 0 wit inspect .59   18    - wit inspect
ldv-memsafety/memleaks_test6_1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .25  29 2.9  true -32 wit inspect 3.6  250 true -32 wit inspect 5.2   250   error (1) 0 wit inspect .63   18    - wit inspect
ldv-memsafety/memleaks_test6_3_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .22  29 2.0  true -32 wit inspect 4.6  250 true -32 wit inspect 3.6   240   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 .21  29 2.1  true -32 wit inspect 2.7  260 true -32 wit inspect 5.2   250   error (1) 0 wit inspect .59   18    - wit inspect
ldv-memsafety/memleaks_test8_1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .091 28 1.0  true -32 wit inspect 2.6  270 true -32 wit inspect 4.8   230   error (1) 0 wit inspect .60   18    - wit inspect
ldv-memsafety/memleaks_test9_1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .11  28 .88 true -32 wit inspect 2.6  250 true -32 wit inspect 3.2   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 .11  28 .90 true -32 wit inspect 2.5  250 true -32 wit inspect 5.0   230   error (1) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/memleaks_test10_true-valid-memsafety_true-termination.i true 2 wit inspect .90  31 12    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     840  
ldv-memsafety/memleaks_test11_true-valid-memsafety_true-termination.i true 2 wit inspect .85  32 10    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     1200  
ldv-memsafety/memleaks_test12_true-valid-memsafety.i unknown 0 wit inspect 12     180 160    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.8
ldv-memsafety/memleaks_test13_true-valid-memsafety.i true 2 wit inspect .85  33 11    - wit inspect - wit inspect - wit inspect true 2 wit inspect 99     1000  
ldv-memsafety/memleaks_test14_true-valid-memsafety.i true 2 wit inspect .76  32 8.8  - wit inspect - wit inspect - wit inspect true 2 wit inspect 65     990  
ldv-memsafety/memleaks_test15_true-valid-memsafety_true-termination.i true 2 wit inspect 9.4   39 120    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     1100  
ldv-memsafety/memleaks_test16_true-valid-memsafety_true-termination.i true 2 wit inspect .13  28 .95 - wit inspect - wit inspect - wit inspect true 2 wit inspect 12     460  
ldv-memsafety/memleaks_test17_1_true-valid-memsafety_true-termination.i true 2 wit inspect 70     140 790    - wit inspect - wit inspect - wit inspect error (7) 0 wit inspect 890     2300  
ldv-memsafety/memleaks_test17_2_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900     400 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
ldv-memsafety/memleaks_test18_true-valid-memsafety_true-termination.i true 2 wit inspect 68     110 890    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     1300  
ldv-memsafety/memleaks_test19_true-valid-memsafety_true-termination.i true 2 wit inspect .15  28 1.5  - wit inspect - wit inspect - wit inspect true 2 wit inspect 350     870  
ldv-memsafety/memleaks_test1_true-valid-memsafety_true-termination.i true 2 wit inspect .11  28 1.2  - wit inspect - wit inspect - wit inspect true 2 wit inspect 10     280  
ldv-memsafety/memleaks_test20_true-valid-memsafety_true-termination.i true 2 wit inspect .11  28 1.3  - wit inspect - wit inspect - wit inspect true 2 wit inspect 15     470  
ldv-memsafety/memleaks_test21_true-valid-memsafety_true-termination.i true 2 wit inspect .13  28 .74 - wit inspect - wit inspect - wit inspect true 2 wit inspect 11     430  
ldv-memsafety/memleaks_test22_1_true-valid-memsafety_true-termination.i true 2 wit inspect .68  28 7.8  - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     1800  
ldv-memsafety/memleaks_test22_2_true-valid-memsafety_true-termination.i true 2 wit inspect .82  28 9.8  - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     4100  
ldv-memsafety/memleaks_test22_3_true-valid-memsafety_true-termination.i true 2 wit inspect .85  28 9.7  - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     3000  
ldv-memsafety/memleaks_test23_1_true-valid-memsafety.i timeout 0 wit inspect 900     2500 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
ldv-memsafety/memleaks_test23_3_true-valid-memsafety.i timeout 0 wit inspect 900     2600 8900    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.8
ldv-memsafety/memleaks_test3_true-valid-memsafety_true-termination.i true 2 wit inspect .13  28 1.0  - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.1   350  
ldv-memsafety/memleaks_test4_true-valid-memsafety_true-termination.i true 2 wit inspect .14  28 1.6  - wit inspect - wit inspect - wit inspect true 2 wit inspect 30     520  
ldv-memsafety/memleaks_test5_true-valid-memsafety_true-termination.i true 2 wit inspect .10  28 1.0  - wit inspect - wit inspect - wit inspect true 2 wit inspect 10     410  
ldv-memsafety/memleaks_test6_true-valid-memsafety_true-termination.i true 2 wit inspect .13  28 1.3  - wit inspect - wit inspect - wit inspect true 2 wit inspect 21     480  
ldv-memsafety/memleaks_test7_true-valid-memsafety_true-termination.i true 2 wit inspect .11  28 1.2  - wit inspect - wit inspect - wit inspect true 2 wit inspect 17     530  
ldv-memsafety/memleaks_test8_true-valid-memsafety_true-termination.i true 2 wit inspect .099 28 1.1  - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.2   350  
ldv-memsafety/memleaks_test9_true-valid-memsafety_true-termination.i true 2 wit inspect .13  28 1.1  - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.0   350  
ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety_true-termination.i true 2 wit inspect .13  26 .85 - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 3.7   200  
ldv-memsafety-bitfields/test-bitfields-2.1_true-valid-memsafety_true-termination.i true 2 wit inspect .15  26 1.6  - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 3.8   200  
ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety_true-termination.i true 2 wit inspect .18  26 1.8  - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 3.7   200  
ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i true 2 wit inspect .25  26 2.9  - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 4.2   200  
ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i true 2 wit inspect .34  27 3.5  - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 3.5   200  
ldv-memsafety-bitfields/test-bitfields-1_false-valid-deref.i false(valid-deref) 0 wit inspect .21  28 2.6  error (invalid witness file) 0 wit inspect 1.7  190 unknown 0 wit inspect 3.7   200   error (1) 0 wit inspect .52   18    - wit inspect
ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i false(valid-deref) 0 wit inspect .20  27 1.7  true -32 wit inspect 3.3  240 unknown 0 wit inspect 3.6   200   true -32 wit inspect .62   18    - wit inspect
ldv-memsafety-bitfields/test-bitfields-3.1_false-valid-deref.i false(valid-deref) 0 wit inspect .32  26 4.3  true -32 wit inspect 2.9  240 unknown 0 wit inspect 2.5   200   true -32 wit inspect .58   18    - wit inspect
ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i false(valid-deref) 0 wit inspect .34  27 4.0  true -32 wit inspect 2.7  240 unknown 0 wit inspect 3.6   200   error (2) 0 wit inspect .58   18    - wit inspect
ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i false(valid-free) 1 wit inspect .18  26 1.8  false(valid-free) 1 wit inspect 2.1  250 unknown 0 wit inspect 2.5   210   error (2) 0 wit inspect .58   18    - 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 129 36000 230000 410000 90 -1746 820 35000 90 -2302 360 19000 90 -516 240    1500 90 60 15000 40000
    correct results 76 129 1300 7100 16000 14 14 48 3900 2 2 11 530 12 12 7.4  220 30 60 1000 14000
        correct true 53 106 1100 4800 13000 0 0 0 30 60 1000 14000
        correct false 23 23 240 2300 3000 14 14 48 3900 2 2 11 530 12 12 7.4  220 0
    correct-unconfimed results 56 0 220 3300 2400 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 56 0 220 3300 2400 0 0 0 0
    incorrect results 0 55 -1760 290 18000 72 -2304 330 17000 17 -528 11    310 0
        incorrect true 0 55 -1760 290 18000 72 -2304 330 17000 16 -512 10    290 0
        incorrect false 0 0 0 1 -16 .65 19 0
score (180 tasks, max score: 270) 129 -1746 -2302 -516 60
Run set esbmc-kind.sv-comp18.MemSafety-Heap cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.MemSafety-Heap uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.MemSafety-Heap fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.MemSafety-Heap uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.MemSafety-Heap