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* [apollon024; apollon065; apollon077; apollon078] [apollon077; apollon078; apollon093] [apollon077; apollon078] [apollon073; apollon077; apollon078; apollon091; apollon099; apollon124]
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 33553 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 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 00:00:31 CET 2017-12-02 01:15:07 CET 2017-12-02 01:40:08 CET 2017-12-02 01:42:26 CET 2017-12-02 01:17:53 CET
Run set esbmc-incr.sv-comp18.MemSafety-Heap cpa-seq-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.MemSafety-Heap uautomizer-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.MemSafety-Heap fshell-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.MemSafety-Heap uautomizer-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.MemSafety-Heap
Options -s incr -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-02_0000.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-incr.2017-12-02_0000.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/esbmc-incr.2017-12-02_0000.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/esbmc-incr.2017-12-02_0000.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 32     110 250    true -32 wit inspect 9.7  630 true -32 wit inspect 3.6   240   error (2) 0 wit inspect .80   21    - wit inspect
memsafety/test-0137_false-valid-deref.i false(valid-deref) 0 wit inspect .36  29 4.8  error (invalid witness file) 0 wit inspect 2.8  180 true -32 wit inspect 4.3   260   error (1) 0 wit inspect .58   18    - wit inspect
memsafety/test-0235_false-valid-deref.i out of memory 0 wit inspect 780     15000 6500    error (invalid witness file) 0 wit inspect .62 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0010 .26 - wit inspect
memsafety/960521-1_false-valid-free.i false(valid-free) 1 wit inspect 30     110 220    true -32 wit inspect 6.5  650 true -32 wit inspect 3.6   240   false(valid-free) 1 wit inspect .84   21    - wit inspect
memsafety/test-0158_false-valid-free.i false(valid-free) 1 wit inspect .39  29 3.9  true -32 wit inspect 3.4  250 true -32 wit inspect 4.9   230   false(valid-free) 1 wit inspect .65   19    - wit inspect
memsafety/test-0232_false-valid-free.i false(valid-free) 1 wit inspect .66  30 6.3  false(valid-free) 1 wit inspect 3.8  270 true -32 wit inspect 4.0   240   true -32 wit inspect .64   18    - wit inspect
memsafety/20020406-1_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 22     990 250    error (recursion) 0 wit inspect 3.0  260 true -32 wit inspect 4.4   270   true -32 wit inspect .70   18    - wit inspect
memsafety/20051113-1.c_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 6.0   88 66    true -32 wit inspect 3.8  250 true -32 wit inspect 5.4   240   true -32 wit inspect .65   19    - wit inspect
memsafety/lockfree-3.1_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 1.6   36 18    timeout 0 wit inspect 92    2300 true -32 wit inspect 5.4   240   true -32 wit inspect .65   18    - wit inspect
memsafety/lockfree-3.2_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .26  29 2.4  timeout 0 wit inspect 97    2400 true -32 wit inspect 3.9   250   true -32 wit inspect .64   19    - wit inspect
memsafety/lockfree-3.3_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 6.6   74 72    timeout 0 wit inspect 91    2300 true -32 wit inspect 3.8   240   true -32 wit inspect .66   18    - wit inspect
memsafety/test-0019_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .19  28 1.8  true -32 wit inspect 3.7  250 true -32 wit inspect 5.1   230   true -32 wit inspect .64   18    - wit inspect
memsafety/test-0102_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 11     200 110    timeout 0 wit inspect 92    3300 true -32 wit inspect 3.9   250   false(valid-deref) -16 wit inspect .66   19    - wit inspect
memsafety/test-0158_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .11  27 .78 true -32 wit inspect 2.3  250 true -32 wit inspect 5.0   230   true -32 wit inspect .62   18    - wit inspect
memsafety/test-0220_false-valid-memtrack.i out of memory 0 wit inspect 150     15000 1500    error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0010 .30 - wit inspect
memsafety/test-0232_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .28  28 2.7  timeout 0 wit inspect 91    1800 true -32 wit inspect 3.8   250   true -32 wit inspect .64   18    - wit inspect
memsafety/test-0234_false-valid-memtrack.i out of memory 0 wit inspect 790     15000 7200    error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
memsafety/test-0235_false-valid-memtrack.i out of memory 0 wit inspect 760     15000 5800    error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0010 .30 - wit inspect
memsafety/960521-1_true-valid-memsafety.i timeout 0 wit inspect 900     9900 9600    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
memsafety/lockfree-3.0_true-valid-memsafety.i timeout 0 wit inspect 900     700 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
memsafety/test-0019_true-valid-memsafety_true-termination.i true 2 wit inspect .12  27 1.7  - wit inspect - wit inspect - wit inspect true 2 wit inspect 20     520  
memsafety/test-0102_true-valid-memsafety.i timeout 0 wit inspect 900     2600 9900    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
memsafety/test-0134_true-valid-memsafety.i timeout 0 wit inspect 900     2600 8400    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.8
memsafety/test-0158_true-valid-memsafety_true-termination.i true 2 wit inspect .19  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     2500 8300    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
memsafety/test-0217_true-valid-memsafety_false-termination.i timeout 0 wit inspect 900     3600 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
memsafety/test-0218_true-valid-memsafety_false-termination.i timeout 0 wit inspect 900     2900 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .048 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 .020 4.9
memsafety/test-0232_true-valid-memsafety.i timeout 0 wit inspect 900     740 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.9
memsafety/test-0234_true-valid-memsafety.i out of memory 0 wit inspect 770     15000 6700    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
memsafety/test-0235_true-valid-memsafety.i out of memory 0 wit inspect 800     15000 6200    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
memsafety/test-0236_true-valid-memsafety.i out of memory 0 wit inspect 760     15000 7500    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
memsafety/test-0237_true-valid-memsafety.i out of memory 0 wit inspect 760     15000 6200    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
memsafety/test-0504_true-valid-memsafety.i timeout 0 wit inspect 900     880 9900    - 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     870 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.9
memsafety/test-0521_true-valid-memsafety.i timeout 0 wit inspect 900     1900 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
memsafety/test-memleak_nexttime_true-valid-memsafety_true-termination.i true 2 wit inspect .62  29 8.1  - wit inspect - wit inspect - wit inspect error (7) 0 wit inspect 240     900  
memsafety-ext/dll_extends_pointer_true-valid-memsafety.i timeout 0 wit inspect 900     430 10000    - 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     200 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
memsafety-ext/skiplist_3lvl_true-valid-memsafety.i timeout 0 wit inspect 900     280 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
memsafety-ext/tree_cnstr_true-valid-memsafety_false-termination.i timeout 0 wit inspect 900     450 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 5.0
memsafety-ext/tree_dsw_true-valid-memsafety_false-termination.i timeout 0 wit inspect 900     790 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.9
memsafety-ext/tree_of_cslls_true-valid-memsafety.i timeout 0 wit inspect 900     730 9800    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
memsafety-ext/tree_parent_ptr_true-valid-memsafety_false-termination.i timeout 0 wit inspect 900     490 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
memsafety-ext/tree_stack_true-valid-memsafety_false-termination.i timeout 0 wit inspect 900     460 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
memsafety-ext2/split_list_test05_false-valid-deref.i out of memory 0 wit inspect 150     15000 1000    error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
memsafety-ext2/complex_data_creation_test01_false-valid-memtrack.i timeout 0 wit inspect 900     2000 9400    error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
memsafety-ext2/complex_data_creation_test02_false-valid-memtrack.i timeout 0 wit inspect 900     4500 8600    error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0030 .29 - wit inspect
memsafety-ext2/length_test03_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 5.2   47 52    error (invalid witness file) 0 wit inspect 2.8  180 true -32 wit inspect 6.5   260   error (1) 0 wit inspect .58   19    - wit inspect
memsafety-ext2/optional_data_creation_test04_false-valid-memtrack.i timeout 0 wit inspect 900     480 10000    error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .037 4.8 error (invalid witness file) 0 wit inspect .0010 .26 - wit inspect
memsafety-ext2/complex_data_creation_test01_true-valid-memsafety.i timeout 0 wit inspect 900     1900 9100    - 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     4000 6400    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
memsafety-ext2/length_test03_true-valid-memsafety.i timeout 0 wit inspect 900     600 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
memsafety-ext2/optional_data_creation_test04_true-valid-memsafety.i timeout 0 wit inspect 900     490 9800    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
memsafety-ext2/split_list_test05_true-valid-memsafety.i out of memory 0 wit inspect 120     15000 1100    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.9
list-ext-properties/960521-1_1_false-valid-deref.i false(valid-deref) 0 wit inspect .48  29 4.6  true -32 wit inspect 11    730 true -32 wit inspect 3.6   230   error (2) 0 wit inspect .64   18    - wit inspect
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 150     210 1900    false(valid-deref) 1 wit inspect 3.7  260 true -32 wit inspect 4.2   250   false(valid-deref) 1 wit inspect .65   19    - wit inspect
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i false(valid-free) -16 wit inspect .41  29 3.8  error (invalid witness file) 0 wit inspect 1.8  170 true -32 wit inspect 4.0   260   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 .29  29 3.1  true -32 wit inspect 8.9  810 true -32 wit inspect 3.4   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 .32  28 3.3  true -32 wit inspect 3.3  250 true -32 wit inspect 5.0   230   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 3.0  true -32 wit inspect 2.5  250 true -32 wit inspect 5.0   230   true -32 wit inspect .63   19    - wit inspect
list-ext-properties/test-0158_1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .084 27 .99 true -32 wit inspect 3.4  250 true -32 wit inspect 5.0   230   true -32 wit inspect .63   18    - wit inspect
list-ext-properties/test-0232_1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .19  28 1.3  true -32 wit inspect 6.5  360 true -32 wit inspect 3.9   250   true -32 wit inspect .65   18    - wit inspect
list-ext-properties/960521-1_1_true-valid-memsafety.i true 2 wit inspect 5.9   38 72    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     1100  
list-ext-properties/list-ext_1_true-valid-memsafety.i true 2 wit inspect 170     210 2500    - wit inspect - wit inspect - wit inspect error (7) 0 wit inspect 350     770  
list-ext-properties/list-ext_flag_1_true-valid-memsafety.i true 2 wit inspect 54     110 690    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     2300  
list-ext-properties/simple-ext_1_true-valid-memsafety.i true 2 wit inspect 240     190 2600    - wit inspect - wit inspect - wit inspect error (7) 0 wit inspect 430     980  
list-ext-properties/test-0019_1_true-valid-memsafety_true-termination.i true 2 wit inspect .14  27 1.3  - wit inspect - wit inspect - wit inspect true 2 wit inspect 160     860  
list-ext-properties/test-0158_1_true-valid-memsafety_true-termination.i true 2 wit inspect .15  27 1.7  - wit inspect - wit inspect - wit inspect true 2 wit inspect 19     390  
list-ext-properties/test-0214_1_true-valid-memsafety.i timeout 0 wit inspect 900     3900 12000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
list-ext-properties/test-0217_1_true-valid-memsafety.i timeout 0 wit inspect 900     2800 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
list-ext-properties/test-0232_1_true-valid-memsafety_true-termination.i true 2 wit inspect 120     250 1400    - wit inspect - wit inspect - wit inspect error (7) 0 wit inspect 310     780  
list-ext-properties/test-0504_1_true-valid-memsafety.i true 2 wit inspect 230     190 3000    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     1000  
list-ext-properties/test-0513_1_true-valid-memsafety.i true 2 wit inspect 17     210 200    - 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     680 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c false(valid-deref) 1 wit inspect .19  29 1.8  false(valid-deref) 1 wit inspect 2.8  250 true -32 wit inspect 3.7   240   timeout 0 wit inspect 96      18    - wit inspect
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-write.c false(valid-deref) 1 wit inspect .087 28 .87 false(valid-deref) 1 wit inspect 2.0  250 true -32 wit inspect 3.6   240   timeout 0 wit inspect 96      18    - wit inspect
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-read.c false(valid-deref) 1 wit inspect .091 28 1.0  false(valid-deref) 1 wit inspect 2.9  240 true -32 wit inspect 3.2   240   true -32 wit inspect .57   18    - wit inspect
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-write.c false(valid-deref) 1 wit inspect .081 28 .82 false(valid-deref) 1 wit inspect 3.1  260 true -32 wit inspect 3.7   240   true -32 wit inspect .58   18    - wit inspect
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c false(valid-deref) 1 wit inspect 2.6   41 31    false(valid-deref) 1 wit inspect 5.3  410 true -32 wit inspect 4.9   230   false(valid-deref) 1 wit inspect .62   18    - wit inspect
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-write.c false(valid-deref) 1 wit inspect 2.5   43 35    false(valid-deref) 1 wit inspect 7.7  420 true -32 wit inspect 3.5   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.5   42 18    true -32 wit inspect 1.9  240 true -32 wit inspect 4.4   220   false(valid-deref) 1 wit inspect .59   18    - wit inspect
ldv-memsafety/memset3_false-valid-deref-write.c false(valid-deref) 1 wit inspect 18     340 260    true -32 wit inspect 1.9  250 true -32 wit inspect 3.1   220   false(valid-deref) 1 wit inspect .59   18    - wit inspect
ldv-memsafety/memsetNonZero2_false-valid-deref-write.c false(valid-deref) 1 wit inspect 1.5   42 21    true -32 wit inspect 2.7  240 true -32 wit inspect 3.2   230   false(valid-deref) 1 wit inspect .62   18    - wit inspect
ldv-memsafety/memsetNonZero3_false-valid-deref-write.c false(valid-deref) 1 wit inspect 18     340 190    true -32 wit inspect 2.7  240 true -32 wit inspect 4.6   220   false(valid-deref) 1 wit inspect .61   18    - wit inspect
ldv-memsafety/memsetNonZero_false-valid-deref-write.c false(valid-deref) 1 wit inspect 18     340 200    true -32 wit inspect 2.3  260 true -32 wit inspect 4.9   220   false(valid-deref) 1 wit inspect .58   18    - wit inspect
ldv-memsafety/memset_false-valid-deref-write.c false(valid-deref) 1 wit inspect 18     340 250    true -32 wit inspect 1.9  250 true -32 wit inspect 4.9   230   false(valid-deref) 1 wit inspect .58   18    - wit inspect
ldv-memsafety/ArraysOfVariableLength2_true-valid-memsafety.c timeout 0 wit inspect 900     2400 11000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c true 2 wit inspect 1.1   29 14    - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.1   460  
ldv-memsafety/ArraysOfVariableLength5_true-valid-memsafety.c true 2 wit inspect 2.5   41 34    - wit inspect - wit inspect - wit inspect true 2 wit inspect 15     490  
ldv-memsafety/ArraysOfVariableLength6_true-valid-memsafety_true-termination.c true 2 wit inspect 1.1   29 15    - wit inspect - wit inspect - wit inspect true 2 wit inspect 15     470  
ldv-memsafety/ArraysOfVariableLength_true-valid-memsafety.c true 2 wit inspect 80     820 960    - wit inspect - wit inspect - wit inspect true 2 wit inspect 15     540  
ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety_true-termination.c true 2 wit inspect 2.7   43 36    - wit inspect - wit inspect - wit inspect true 2 wit inspect 11     440  
ldv-memsafety/StructInitialization1_true-valid-memsafety.c true 2 wit inspect .10  29 1.0  - wit inspect - wit inspect - wit inspect error (7) 0 wit inspect 3.9   210  
ldv-memsafety/StructInitialization2_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/StructInitialization_true-valid-memsafety_true-termination.c true 2 wit inspect .12  26 .87 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0   210  
ldv-memsafety/memset2_true-valid-memsafety_true-termination.c true 2 wit inspect 1.6   43 18    - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.0   280  
ldv-memsafety/memset3_true-valid-memsafety_true-termination.c true 2 wit inspect 18     350 230    - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.2   280  
ldv-memsafety/memsetNonZero2_true-valid-memsafety_true-termination.c true 2 wit inspect 1.6   43 18    - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.9   300  
ldv-memsafety/memsetNonZero3_true-valid-memsafety_true-termination.c true 2 wit inspect 18     350 270    - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.7   290  
ldv-memsafety/memsetNonZero_true-valid-memsafety_true-termination.c true 2 wit inspect 18     350 270    - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.3   280  
ldv-memsafety/memset_true-valid-memsafety_true-termination.c true 2 wit inspect 18     350 230    - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7   290  
ldv-memsafety/memleaks_test14_3_false-valid-deref.i false(valid-deref) 0 wit inspect .91  29 10    true -32 wit inspect 2.7  260 true -32 wit inspect 3.9   250   error (1) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/memleaks_test22_3_false-valid-deref.i false(valid-deref) 0 wit inspect 2.0   30 23    true -32 wit inspect 3.0  260 true -32 wit inspect 4.0   260   error (1) 0 wit inspect .58   19    - wit inspect
ldv-memsafety/memleaks_test22_5_false-valid-deref.i false(valid-deref) 0 wit inspect 1.9   30 22    true -32 wit inspect 3.0  270 true -32 wit inspect 4.1   260   error (1) 0 wit inspect .58   19    - wit inspect
ldv-memsafety/memleaks_test23_2_false-valid-deref.i timeout 0 wit inspect 900     2200 8500    error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
ldv-memsafety/memleaks_test23_4_false-valid-deref.i timeout 0 wit inspect 900     2100 8800    error (invalid witness file) 0 wit inspect .43 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0010 .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 2.7  260 true -32 wit inspect 3.7   250   error (1) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/memleaks_test12_false-valid-free.i unknown 0 wit inspect 2.8   59 36    error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .0010 .28 - wit inspect
ldv-memsafety/memleaks_test17_2_false-valid-free.i false(valid-free) 0 wit inspect 12     120 120    true -32 wit inspect 6.0  270 true -32 wit inspect 5.3   240   error (1) 0 wit inspect .58   19    - wit inspect
ldv-memsafety/memleaks_test19_false-valid-free.i false(valid-free) 1 wit inspect .24  29 2.7  false(valid-free) 1 wit inspect 3.9  260 true -32 wit inspect 3.8   250   error (1) 0 wit inspect .62   18    - wit inspect
ldv-memsafety/memleaks_test1_false-valid-free.i false(valid-free) 1 wit inspect .13  29 1.5  false(valid-free) 1 wit inspect 2.7  250 true -32 wit inspect 6.6   260   error (1) 0 wit inspect .59   19    - wit inspect
ldv-memsafety/memleaks_test3_false-valid-free.i false(valid-free) 1 wit inspect .13  29 1.5  false(valid-free) 1 wit inspect 2.6  250 false(valid-free) 1 wit inspect 5.0   250   error (1) 0 wit inspect .59   18    - wit inspect
ldv-memsafety/memleaks_test6_2_false-valid-free.i false(valid-free) 1 wit inspect .33  29 2.9  false(valid-free) 1 wit inspect 2.6  250 true -32 wit inspect 3.6   240   error (1) 0 wit inspect .59   18    - wit inspect
ldv-memsafety/memleaks_test8_2_false-valid-free.i false(valid-free) 1 wit inspect .13  29 1.3  false(valid-free) 1 wit inspect 2.6  260 false(valid-free) 1 wit inspect 5.3   280   error (1) 0 wit inspect .59   18    - wit inspect
ldv-memsafety/memleaks_test10_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .68  32 8.2  true -32 wit inspect 2.9  250 true -32 wit inspect 3.7   260   error (1) 0 wit inspect .58   19    - wit inspect
ldv-memsafety/memleaks_test11_2_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect 1.3   33 11    true -32 wit inspect 4.4  260 true -32 wit inspect 4.0   260   error (1) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/memleaks_test13_1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .24  29 2.0  true -32 wit inspect 2.6  250 true -32 wit inspect 3.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 2.3   37 22    true -32 wit inspect 3.0  250 true -32 wit inspect 3.9   250   error (1) 0 wit inspect .58   19    - wit inspect
ldv-memsafety/memleaks_test14_1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .23  29 2.1  true -32 wit inspect 4.0  270 true -32 wit inspect 3.3   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.1   37 19    true -32 wit inspect 2.8  260 true -32 wit inspect 3.9   240   error (1) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/memleaks_test15_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 2.0   34 20    true -32 wit inspect 3.2  260 true -32 wit inspect 4.1   260   error (1) 0 wit inspect .60   18    - wit inspect
ldv-memsafety/memleaks_test16_1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .22  29 2.0  true -32 wit inspect 4.2  250 true -32 wit inspect 3.2   230   error (1) 0 wit inspect .59   18    - wit inspect
ldv-memsafety/memleaks_test16_2_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .12  29 1.4  true -32 wit inspect 4.2  270 true -32 wit inspect 3.3   230   error (1) 0 wit inspect .59   18    - wit inspect
ldv-memsafety/memleaks_test17_1_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 14     120 210    true -32 wit inspect 4.2  260 true -32 wit inspect 3.8   250   error (1) 0 wit inspect .59   19    - wit inspect
ldv-memsafety/memleaks_test17_3_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 12     82 140    true -32 wit inspect 5.4  270 true -32 wit inspect 3.7   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 .20  29 2.3  true -32 wit inspect 6.5  290 true -32 wit inspect 5.4   240   error (1) 0 wit inspect .59   18    - wit inspect
ldv-memsafety/memleaks_test18_2_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect 37     85 480    true -32 wit inspect 5.8  420 true -32 wit inspect 5.0   240   error (1) 0 wit inspect .59   19    - wit inspect
ldv-memsafety/memleaks_test18_3_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect 6.3   37 93    true -32 wit inspect 77    2300 true -32 wit inspect 4.7   230   error (1) 0 wit inspect .59   18    - wit inspect
ldv-memsafety/memleaks_test1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .095 28 .93 true -32 wit inspect 3.6  250 true -32 wit inspect 4.8   220   error (1) 0 wit inspect .59   18    - wit inspect
ldv-memsafety/memleaks_test20_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .092 28 1.1  true -32 wit inspect 3.7  250 true -32 wit inspect 5.2   250   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 .12  28 .84 true -32 wit inspect 3.5  250 true -32 wit inspect 5.0   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 2.1   30 19    true -32 wit inspect 2.8  260 true -32 wit inspect 5.8   250   error (1) 0 wit inspect .61   18    - wit inspect
ldv-memsafety/memleaks_test22_2_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .54  29 7.8  true -32 wit inspect 2.6  260 true -32 wit inspect 5.6   250   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.1   30 15    true -32 wit inspect 3.9  260 true -32 wit inspect 4.0   250   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 .19  29 2.3  true -32 wit inspect 2.8  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 .091 28 1.2  true -32 wit inspect 3.6  250 true -32 wit inspect 4.8   230   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 .090 28 1.2  true -32 wit inspect 4.6  260 true -32 wit inspect 4.5   230   error (1) 0 wit inspect .60   18    - wit inspect
ldv-memsafety/memleaks_test6_1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .30  29 2.5  true -32 wit inspect 4.1  260 true -32 wit inspect 5.2   240   error (1) 0 wit inspect .58   19    - wit inspect
ldv-memsafety/memleaks_test6_3_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .24  29 2.2  true -32 wit inspect 3.9  250 true -32 wit inspect 3.5   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 .23  29 2.5  true -32 wit inspect 3.8  250 true -32 wit inspect 5.0   240   error (1) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/memleaks_test8_1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .091 28 .92 true -32 wit inspect 2.6  250 true -32 wit inspect 3.4   230   error (1) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/memleaks_test9_1_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .12  28 .87 true -32 wit inspect 3.5  250 true -32 wit inspect 3.5   240   error (1) 0 wit inspect .60   20    - wit inspect
ldv-memsafety/memleaks_test9_2_false-valid-memtrack_true-termination.i false(valid-memtrack) 0 wit inspect .089 28 .93 true -32 wit inspect 2.5  250 true -32 wit inspect 3.3   230   error (1) 0 wit inspect .59   18    - wit inspect
ldv-memsafety/memleaks_test10_true-valid-memsafety_true-termination.i true 2 wit inspect .87  31 11    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     830  
ldv-memsafety/memleaks_test11_true-valid-memsafety_true-termination.i true 2 wit inspect .86  32 11    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     1100  
ldv-memsafety/memleaks_test12_true-valid-memsafety.i unknown 0 wit inspect 2.8   59 38    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
ldv-memsafety/memleaks_test13_true-valid-memsafety.i true 2 wit inspect 1.5   37 18    - wit inspect - wit inspect - wit inspect true 2 wit inspect 88     960  
ldv-memsafety/memleaks_test14_true-valid-memsafety.i true 2 wit inspect 2.7   41 32    - wit inspect - wit inspect - wit inspect true 2 wit inspect 82     1000  
ldv-memsafety/memleaks_test15_true-valid-memsafety_true-termination.i true 2 wit inspect 8.7   39 110    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     860  
ldv-memsafety/memleaks_test16_true-valid-memsafety_true-termination.i true 2 wit inspect .11  28 1.2  - wit inspect - wit inspect - wit inspect true 2 wit inspect 13     450  
ldv-memsafety/memleaks_test17_1_true-valid-memsafety_true-termination.i true 2 wit inspect 47     130 540    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     2000  
ldv-memsafety/memleaks_test17_2_true-valid-memsafety_true-termination.i timeout 0 wit inspect 900     370 10000    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
ldv-memsafety/memleaks_test18_true-valid-memsafety_true-termination.i true 2 wit inspect 48     100 640    - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     970  
ldv-memsafety/memleaks_test19_true-valid-memsafety_true-termination.i true 2 wit inspect .15  28 1.9  - wit inspect - wit inspect - wit inspect true 2 wit inspect 380     820  
ldv-memsafety/memleaks_test1_true-valid-memsafety_true-termination.i true 2 wit inspect .13  27 1.0  - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.4   280  
ldv-memsafety/memleaks_test20_true-valid-memsafety_true-termination.i true 2 wit inspect .099 28 1.3  - wit inspect - wit inspect - wit inspect true 2 wit inspect 12     450  
ldv-memsafety/memleaks_test21_true-valid-memsafety_true-termination.i true 2 wit inspect .13  28 1.1  - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.3   440  
ldv-memsafety/memleaks_test22_1_true-valid-memsafety_true-termination.i true 2 wit inspect .61  28 7.3  - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     1900  
ldv-memsafety/memleaks_test22_2_true-valid-memsafety_true-termination.i true 2 wit inspect .72  28 9.9  - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     4400  
ldv-memsafety/memleaks_test22_3_true-valid-memsafety_true-termination.i true 2 wit inspect .72  28 8.9  - 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     2200 9300    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.9
ldv-memsafety/memleaks_test23_3_true-valid-memsafety.i timeout 0 wit inspect 900     2100 8800    - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.9
ldv-memsafety/memleaks_test3_true-valid-memsafety_true-termination.i true 2 wit inspect .12  27 1.0  - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.3   340  
ldv-memsafety/memleaks_test4_true-valid-memsafety_true-termination.i true 2 wit inspect .13  28 1.5  - wit inspect - wit inspect - wit inspect true 2 wit inspect 27     500  
ldv-memsafety/memleaks_test5_true-valid-memsafety_true-termination.i true 2 wit inspect .13  28 1.2  - wit inspect - wit inspect - wit inspect true 2 wit inspect 10     420  
ldv-memsafety/memleaks_test6_true-valid-memsafety_true-termination.i true 2 wit inspect .11  28 .90 - wit inspect - wit inspect - wit inspect true 2 wit inspect 18     600  
ldv-memsafety/memleaks_test7_true-valid-memsafety_true-termination.i true 2 wit inspect .12  28 1.3  - wit inspect - wit inspect - wit inspect true 2 wit inspect 11     540  
ldv-memsafety/memleaks_test8_true-valid-memsafety_true-termination.i true 2 wit inspect .13  28 1.1  - wit inspect - wit inspect - wit inspect true 2 wit inspect 11     360  
ldv-memsafety/memleaks_test9_true-valid-memsafety_true-termination.i true 2 wit inspect .12  28 1.1  - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.4   350  
ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety_true-termination.i true 2 wit inspect .12  26 .93 - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 2.5   210  
ldv-memsafety-bitfields/test-bitfields-2.1_true-valid-memsafety_true-termination.i true 2 wit inspect .16  26 1.5  - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 3.0   200  
ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety_true-termination.i true 2 wit inspect .16  26 1.3  - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 3.8   190  
ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i true 2 wit inspect .21  27 2.7  - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 3.9   210  
ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i true 2 wit inspect .29  27 3.6  - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 2.6   210  
ldv-memsafety-bitfields/test-bitfields-1_false-valid-deref.i false(valid-deref) 0 wit inspect .25  28 1.8  error (invalid witness file) 0 wit inspect 2.3  170 unknown 0 wit inspect 3.5   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 .16  26 1.5  true -32 wit inspect 3.0  250 unknown 0 wit inspect 3.5   200   true -32 wit inspect .58   18    - wit inspect
ldv-memsafety-bitfields/test-bitfields-3.1_false-valid-deref.i false(valid-deref) 0 wit inspect .32  26 3.4  true -32 wit inspect 1.9  240 unknown 0 wit inspect 2.4   210   true -32 wit inspect .58   18    - wit inspect
ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i false(valid-deref) 0 wit inspect .25  27 3.6  true -32 wit inspect 2.0  240 unknown 0 wit inspect 3.7   210   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 .14  26 1.5  false(valid-free) 1 wit inspect 2.1  250 unknown 0 wit inspect 2.4   200   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 113 39000    240000 420000   90 -1746 810 35000 90 -2302 330 19000 90 -516 240    1500 90 60 14000 39000
    correct results 76 129 1400    7100 17000   14 14 48 3900 2 2 10 530 12 12 7.5  220 30 60 1000 14000
        correct true 53 106 1100    4800 14000   0 0 0 30 60 1000 14000
        correct false 23 23 260    2200 3100   14 14 48 3900 2 2 10 530 12 12 7.5  220 0
    correct-unconfimed results 55 0 190    3200 2100   0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 55 0 190    3200 2100   0 0 0 0
    incorrect results 1 -16 .41 29 3.8 55 -1760 280 18000 72 -2304 310 17000 17 -528 11    310 0
        incorrect true 0 55 -1760 280 18000 72 -2304 310 17000 16 -512 10    290 0
        incorrect false 1 -16 .41 29 3.8 0 0 1 -16 .66 19 0
score (180 tasks, max score: 270) 113 -1746 -2302 -516 60
Run set esbmc-incr.sv-comp18.MemSafety-Heap cpa-seq-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.MemSafety-Heap uautomizer-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.MemSafety-Heap fshell-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.MemSafety-Heap uautomizer-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.MemSafety-Heap