Tool CBMC 5.8 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; apollon091] 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] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 33553 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-01 08:19:34 CET 2017-12-01 08:48:13 CET 2017-12-01 09:05:59 CET 2017-12-01 09:09:10 CET 2017-12-01 08:49:56 CET
Run set cbmc.sv-comp18.MemSafety-Heap cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.MemSafety-Heap uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.MemSafety-Heap fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.MemSafety-Heap uautomizer-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.MemSafety-Heap
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.2017-12-01_0819.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/cbmc.2017-12-01_0819.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cbmc.2017-12-01_0819.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc.2017-12-01_0819.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 6.2  48 57   true -32 wit inspect 11    630 out of memory 0 wit inspect 72     7000   error (2) 0 wit inspect .76   23    - wit inspect
memsafety/test-0137_false-valid-deref.i false(valid-deref) 0 wit inspect .69 44 5.8 timeout (exception) 0 wit inspect 92    2500 true -32 wit inspect 14     570   error (2) 0 wit inspect .64   19    - wit inspect
memsafety/test-0235_false-valid-deref.i false(valid-deref) 0 wit inspect 23    790 230   true -32 wit inspect 6.5  280 timeout 0 wit inspect 96     6600   error (2) 0 wit inspect .80   26    - wit inspect
memsafety/960521-1_false-valid-free.i false(valid-free) 1 wit inspect 5.9  48 66   true -32 wit inspect 9.9  620 out of memory 0 wit inspect 54     7000   false(valid-free) 1 wit inspect .79   23    - wit inspect
memsafety/test-0158_false-valid-free.i false(valid-free) 1 wit inspect .48 36 4.4 false(valid-free) 1 wit inspect 3.7  250 false(valid-free) 1 wit inspect 8.6   280   false(valid-free) 1 wit inspect .66   18    - wit inspect
memsafety/test-0232_false-valid-free.i witness invalid (false(valid-free)) 0 wit inspect .53 37 4.6 timeout 0 wit inspect 93    2100 true -32 wit inspect 6.4   250   error (invalid witness file) 0 wit inspect .58   19    - wit inspect
memsafety/20020406-1_false-valid-memtrack.i false(unreach-call) 0 wit inspect .60 38 5.1 error (recursion) 0 wit inspect 4.4  250 true -32 wit inspect 35     2500   true -32 wit inspect .71   19    - wit inspect
memsafety/20051113-1.c_false-valid-memtrack.i false(unreach-call) 0 wit inspect 1.3  36 16   error (invalid witness file) 0 wit inspect 2.8  180 true -32 wit inspect 36     4200   true -32 wit inspect .66   19    - wit inspect
memsafety/lockfree-3.1_false-valid-memtrack.i false(unreach-call) 0 wit inspect 5.1  140 58   timeout 0 wit inspect 92    2300 unknown 0 wit inspect 55     3800   false(valid-deref) -16 wit inspect .66   19    - wit inspect
memsafety/lockfree-3.2_false-valid-memtrack.i false(unreach-call) 0 wit inspect .46 36 5.0 false(valid-memtrack) 1 wit inspect 35    1700 unknown 0 wit inspect 17     310   false(valid-deref) -16 wit inspect .66   18    - wit inspect
memsafety/lockfree-3.3_false-valid-memtrack.i false(unreach-call) 0 wit inspect 5.1  150 49   timeout 0 wit inspect 92    2300 out of memory 0 wit inspect 70     7000   false(valid-deref) -16 wit inspect .71   19    - wit inspect
memsafety/test-0019_false-valid-memtrack_true-termination.i false(unreach-call) 0 wit inspect .45 36 4.4 exception 0 wit inspect 2.7  170 unknown 0 wit inspect 11     260   error (255) 0 wit inspect .58   18    - wit inspect
memsafety/test-0102_false-valid-memtrack.i false(unreach-call) 0 wit inspect .58 36 6.3 exception 0 wit inspect 2.7  180 unknown 0 wit inspect 23     520   true -32 wit inspect .70   19    - wit inspect
memsafety/test-0158_false-valid-memtrack_true-termination.i false(unreach-call) 0 wit inspect .47 36 4.0 false(valid-memtrack) 1 wit inspect 3.5  260 unknown 0 wit inspect 9.5   260   true -32 wit inspect .66   18    - wit inspect
memsafety/test-0220_false-valid-memtrack.i false(unreach-call) 0 wit inspect .60 38 5.9 true -32 wit inspect 4.0  260 true -32 wit inspect 6.7   310   error (2) 0 wit inspect .71   19    - wit inspect
memsafety/test-0232_false-valid-memtrack.i false(unreach-call) 0 wit inspect .51 36 4.2 timeout 0 wit inspect 97    1200 true -32 wit inspect 4.2   270   true -32 wit inspect .64   18    - wit inspect
memsafety/test-0234_false-valid-memtrack.i false(unreach-call) 0 wit inspect 7.8  270 84   true -32 wit inspect 5.4  270 true -32 wit inspect 5.4   490   error (2) 0 wit inspect .70   21    - wit inspect
memsafety/test-0235_false-valid-memtrack.i false(unreach-call) 0 wit inspect 13    460 150   true -32 wit inspect 5.1  270 true -32 wit inspect 11     670   error (2) 0 wit inspect .76   25    - wit inspect
memsafety/960521-1_true-valid-memsafety.i out of memory 0 wit inspect 120    15000 1700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.9
memsafety/lockfree-3.0_true-valid-memsafety.i error (42) 0 wit inspect 870    2200 5200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
memsafety/test-0019_true-valid-memsafety_true-termination.i true 2 wit inspect .88 37 7.7 - wit inspect - wit inspect - wit inspect true 2 wit inspect 28     520  
memsafety/test-0102_true-valid-memsafety.i error (42) 0 wit inspect 870    2400 7000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
memsafety/test-0134_true-valid-memsafety.i error (42) 0 wit inspect 870    990 6900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
memsafety/test-0158_true-valid-memsafety_true-termination.i true 2 wit inspect .81 36 8.7 - wit inspect - wit inspect - wit inspect true 2 wit inspect 17     400  
memsafety/test-0214_true-valid-memsafety_false-termination.i error (42) 0 wit inspect 870    1800 4500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .031 4.8
memsafety/test-0217_true-valid-memsafety_false-termination.i error (134) 0 wit inspect 46    13000 550   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
memsafety/test-0218_true-valid-memsafety_false-termination.i error (42) 0 wit inspect 870    3700 6200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
memsafety/test-0219_true-valid-memsafety.i error (42) 0 wit inspect 870    1500 7300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
memsafety/test-0232_true-valid-memsafety.i error (42) 0 wit inspect 870    2200 6900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
memsafety/test-0234_true-valid-memsafety.i error (42) 0 wit inspect 870    1300 7000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.9
memsafety/test-0235_true-valid-memsafety.i error (42) 0 wit inspect 870    970 6500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
memsafety/test-0236_true-valid-memsafety.i error (42) 0 wit inspect 870    1400 6400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
memsafety/test-0237_true-valid-memsafety.i error (42) 0 wit inspect 870    1400 6500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
memsafety/test-0504_true-valid-memsafety.i error (42) 0 wit inspect 870    2100 6700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
memsafety/test-0513_true-valid-memsafety.i error (42) 0 wit inspect 870    1900 7500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.9
memsafety/test-0521_true-valid-memsafety.i error (134) 0 wit inspect 380    12000 3200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
memsafety/test-memleak_nexttime_true-valid-memsafety_true-termination.i true 2 wit inspect .88 36 8.1 - wit inspect - wit inspect - wit inspect error (7) 0 wit inspect 200     1500  
memsafety-ext/dll_extends_pointer_true-valid-memsafety.i error (42) 0 wit inspect 870    4100 5500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
memsafety-ext/skiplist_2lvl_true-valid-memsafety.i error (42) 0 wit inspect 870    420 7300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
memsafety-ext/skiplist_3lvl_true-valid-memsafety.i error (42) 0 wit inspect 870    620 7100   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
memsafety-ext/tree_cnstr_true-valid-memsafety_false-termination.i error (42) 0 wit inspect 870    2100 5400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
memsafety-ext/tree_dsw_true-valid-memsafety_false-termination.i error (42) 0 wit inspect 870    1700 5200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
memsafety-ext/tree_of_cslls_true-valid-memsafety.i error (42) 0 wit inspect 870    1200 8800   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
memsafety-ext/tree_parent_ptr_true-valid-memsafety_false-termination.i error (42) 0 wit inspect 870    2100 5500   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
memsafety-ext/tree_stack_true-valid-memsafety_false-termination.i error (42) 0 wit inspect 870    1500 6000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
memsafety-ext2/split_list_test05_false-valid-deref.i out of memory 0 wit inspect 370    15000 4400   error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0011 .31 - wit inspect
memsafety-ext2/complex_data_creation_test01_false-valid-memtrack.i false(unreach-call) 0 wit inspect 22    630 250   timeout 0 wit inspect 92    2900 out of memory 0 wit inspect 51     7000   error (1) 0 wit inspect .64   24    - wit inspect
memsafety-ext2/complex_data_creation_test02_false-valid-memtrack.i false(unreach-call) 0 wit inspect 3.1  110 35   timeout 0 wit inspect 92    2600 out of memory 0 wit inspect 51     7000   error (1) 0 wit inspect .63   22    - wit inspect
memsafety-ext2/length_test03_false-valid-memtrack.i false(unreach-call) 0 wit inspect 3.1  43 36   timeout 0 wit inspect 92    1400 unknown 0 wit inspect 37     1000   true -32 wit inspect .72   20    - wit inspect
memsafety-ext2/optional_data_creation_test04_false-valid-memtrack.i false(unreach-call) 0 wit inspect 19    280 260   timeout 0 wit inspect 93    2500 out of memory 0 wit inspect 47     7000   error (1) 0 wit inspect .68   22    - wit inspect
memsafety-ext2/complex_data_creation_test01_true-valid-memsafety.i error (42) 0 wit inspect 870    2500 8200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
memsafety-ext2/complex_data_creation_test02_true-valid-memsafety.i error (42) 0 wit inspect 870    1300 8800   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
memsafety-ext2/length_test03_true-valid-memsafety.i error (42) 0 wit inspect 870    2000 4000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.9
memsafety-ext2/optional_data_creation_test04_true-valid-memsafety.i error (134) 0 wit inspect 440    13000 4800   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
memsafety-ext2/split_list_test05_true-valid-memsafety.i out of memory 0 wit inspect 250    15000 3700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
list-ext-properties/960521-1_1_false-valid-deref.i false(valid-deref) 1 wit inspect .46 36 4.7 true -32 wit inspect 11    730 false(valid-deref) 1 wit inspect 5.2   280   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 110    380 1300   true -32 wit inspect 8.8  410 false(valid-free) -16 wit inspect 44     1700   false(valid-deref) 1 wit inspect .72   24    - wit inspect
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .49 36 5.4 timeout 0 wit inspect 91    2500 false(valid-free) -16 wit inspect 5.8   280   false(valid-deref) 1 wit inspect .65   19    - wit inspect
list-ext-properties/960521-1_1_false-valid-free.i false(valid-free) 1 wit inspect .49 36 4.4 true -32 wit inspect 14    800 false(valid-free) 1 wit inspect 6.4   270   false(valid-free) 1 wit inspect .65   18    - wit inspect
list-ext-properties/test-0158_1_false-valid-free.i false(valid-free) 1 wit inspect .44 36 4.1 false(valid-free) 1 wit inspect 3.8  250 false(valid-free) 1 wit inspect 5.3   290   false(valid-free) 1 wit inspect .65   18    - wit inspect
list-ext-properties/test-0019_1_false-valid-memtrack_true-termination.i false(unreach-call) 0 wit inspect .46 36 4.2 exception 0 wit inspect 2.6  170 unknown 0 wit inspect 12     300   error (255) 0 wit inspect .59   19    - wit inspect
list-ext-properties/test-0158_1_false-valid-memtrack_true-termination.i false(unreach-call) 0 wit inspect .47 36 3.7 false(valid-memtrack) 1 wit inspect 3.8  270 unknown 0 wit inspect 13     300   true -32 wit inspect .64   18    - wit inspect
list-ext-properties/test-0232_1_false-valid-memtrack_true-termination.i false(unreach-call) 0 wit inspect .51 36 4.4 true -32 wit inspect 5.6  250 true -32 wit inspect 5.1   250   true -32 wit inspect .66   18    - wit inspect
list-ext-properties/960521-1_1_true-valid-memsafety.i true 2 wit inspect 35    1200 400   - 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 110    290 1100   - wit inspect - wit inspect - wit inspect error (7) 0 wit inspect 320     780  
list-ext-properties/list-ext_flag_1_true-valid-memsafety.i true 2 wit inspect 48    140 620   - 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 52    270 650   - wit inspect - wit inspect - wit inspect error (7) 0 wit inspect 460     910  
list-ext-properties/test-0019_1_true-valid-memsafety_true-termination.i true 2 wit inspect .84 36 11   - wit inspect - wit inspect - wit inspect true 2 wit inspect 130     770  
list-ext-properties/test-0158_1_true-valid-memsafety_true-termination.i true 2 wit inspect .83 36 7.3 - wit inspect - wit inspect - wit inspect true 2 wit inspect 18     370  
list-ext-properties/test-0214_1_true-valid-memsafety.i true 2 wit inspect 610    480 5700   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     1300  
list-ext-properties/test-0217_1_true-valid-memsafety.i true 2 wit inspect 510    400 3900   - wit inspect - wit inspect - wit inspect error (7) 0 wit inspect 750     1200  
list-ext-properties/test-0232_1_true-valid-memsafety_true-termination.i true 2 wit inspect 9.1  62 120   - wit inspect - wit inspect - wit inspect error (7) 0 wit inspect 440     950  
list-ext-properties/test-0504_1_true-valid-memsafety.i true 2 wit inspect 5.6  80 78   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     1100  
list-ext-properties/test-0513_1_true-valid-memsafety.i true 2 wit inspect 11    290 130   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     790  
memory-alloca/c.03-alloca_true-valid-memsafety.i error (42) 0 wit inspect 870    1800 4900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-read.c false(valid-deref) 1 wit inspect .25 33 2.2 error 0 wit inspect 3.2  250 false(valid-deref) 1 wit inspect 4.4   270   error (2) 0 wit inspect .61   18    - wit inspect
ldv-memsafety/ArraysOfVariableLength2_false-valid-deref-write.c false(valid-deref) 1 wit inspect .27 33 2.1 false(valid-deref) 1 wit inspect 3.1  250 false(valid-deref) 1 wit inspect 7.6   270   error (2) 0 wit inspect .61   18    - wit inspect
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-read.c false(valid-deref) 1 wit inspect .26 33 2.1 false(valid-deref) 1 wit inspect 2.9  250 false(valid-deref) 1 wit inspect 5.0   260   error (2) 0 wit inspect .60   18    - wit inspect
ldv-memsafety/ArraysOfVariableLength_false-valid-deref-write.c false(valid-deref) 1 wit inspect .27 33 2.0 false(valid-deref) 1 wit inspect 2.8  240 false(valid-deref) 1 wit inspect 3.5   260   error (2) 0 wit inspect .63   18    - wit inspect
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-read.c false(valid-deref) 0 wit inspect 3.6  34 42   true -32 wit inspect 6.8  450 timeout 0 wit inspect 97     5300   error (2) 0 wit inspect 3.0    27    - wit inspect
ldv-memsafety/ArraysWithLenghtAtDeclaration_false-valid-deref-write.c false(valid-deref) 1 wit inspect 3.6  34 35   true -32 wit inspect 9.0  450 false(valid-deref) 1 wit inspect 38     2800   error (2) 0 wit inspect 3.0    27    - wit inspect
ldv-memsafety/memset2_false-valid-deref-write.c witness invalid (false(valid-deref)) 0 wit inspect .45 34 4.0 true -32 wit inspect 2.6  240 true -32 wit inspect 4.8   230   error (invalid witness file) 0 wit inspect .53   18    - wit inspect
ldv-memsafety/memset3_false-valid-deref-write.c witness invalid (false(valid-deref)) 0 wit inspect .41 34 4.6 true -32 wit inspect 2.9  250 true -32 wit inspect 4.5   230   error (invalid witness file) 0 wit inspect .52   18    - wit inspect
ldv-memsafety/memsetNonZero2_false-valid-deref-write.c witness invalid (false(valid-deref)) 0 wit inspect .46 34 4.0 true -32 wit inspect 2.8  240 true -32 wit inspect 4.9   220   error (invalid witness file) 0 wit inspect .53   18    - wit inspect
ldv-memsafety/memsetNonZero3_false-valid-deref-write.c witness invalid (false(valid-deref)) 0 wit inspect .43 34 4.3 true -32 wit inspect 3.1  240 true -32 wit inspect 4.3   220   error (invalid witness file) 0 wit inspect .52   18    - wit inspect
ldv-memsafety/memsetNonZero_false-valid-deref-write.c witness invalid (false(valid-deref)) 0 wit inspect .43 34 4.6 true -32 wit inspect 2.8  240 true -32 wit inspect 3.3   240   error (invalid witness file) 0 wit inspect .52   18    - wit inspect
ldv-memsafety/memset_false-valid-deref-write.c witness invalid (false(valid-deref)) 0 wit inspect .42 34 4.3 true -32 wit inspect 2.9  250 true -32 wit inspect 4.6   220   error (invalid witness file) 0 wit inspect .52   18    - wit inspect
ldv-memsafety/ArraysOfVariableLength2_true-valid-memsafety.c error (42) 0 wit inspect 870    5300 5400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
ldv-memsafety/ArraysOfVariableLength4_true-valid-memsafety_true-termination.c true 2 wit inspect 3.9  34 43   - wit inspect - wit inspect - wit inspect true 2 wit inspect 16     470  
ldv-memsafety/ArraysOfVariableLength5_true-valid-memsafety.c true 2 wit inspect 4.1  33 59   - wit inspect - wit inspect - wit inspect true 2 wit inspect 15     510  
ldv-memsafety/ArraysOfVariableLength6_true-valid-memsafety_true-termination.c true 2 wit inspect 3.9  35 42   - wit inspect - wit inspect - wit inspect true 2 wit inspect 18     480  
ldv-memsafety/ArraysOfVariableLength_true-valid-memsafety.c true 2 wit inspect 13    80 160   - wit inspect - wit inspect - wit inspect true 2 wit inspect 94     620  
ldv-memsafety/ArraysWithLenghtAtDeclaration_true-valid-memsafety_true-termination.c true 2 wit inspect 3.7  35 38   - wit inspect - wit inspect - wit inspect true 2 wit inspect 14     460  
ldv-memsafety/StructInitialization1_true-valid-memsafety.c true 2 wit inspect .44 33 3.9 - wit inspect - wit inspect - wit inspect error (7) 0 wit inspect 4.0   200  
ldv-memsafety/StructInitialization2_true-valid-memsafety.c true 2 wit inspect .44 33 3.4 - wit inspect - wit inspect - wit inspect error (7) 0 wit inspect 4.1   210  
ldv-memsafety/StructInitialization_true-valid-memsafety_true-termination.c true 2 wit inspect .44 33 4.1 - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 3.8   200  
ldv-memsafety/memset2_true-valid-memsafety_true-termination.c true 2 wit inspect .81 35 8.9 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.6   290  
ldv-memsafety/memset3_true-valid-memsafety_true-termination.c true 2 wit inspect .80 34 7.4 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.1   290  
ldv-memsafety/memsetNonZero2_true-valid-memsafety_true-termination.c true 2 wit inspect .82 35 7.5 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.8   290  
ldv-memsafety/memsetNonZero3_true-valid-memsafety_true-termination.c true 2 wit inspect .85 34 7.5 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.4   290  
ldv-memsafety/memsetNonZero_true-valid-memsafety_true-termination.c true 2 wit inspect .84 34 7.6 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.8   280  
ldv-memsafety/memset_true-valid-memsafety_true-termination.c true 2 wit inspect .81 34 6.5 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.1   290  
ldv-memsafety/memleaks_test14_3_false-valid-deref.i false(valid-deref) 0 wit inspect .53 37 6.5 true -32 wit inspect 4.7  250 true -32 wit inspect 11     360   error (1) 0 wit inspect .60   19    - wit inspect
ldv-memsafety/memleaks_test22_3_false-valid-deref.i false(valid-deref) 0 wit inspect .55 37 4.8 true -32 wit inspect 4.5  270 true -32 wit inspect 6.2   250   error (1) 0 wit inspect .63   19    - wit inspect
ldv-memsafety/memleaks_test22_5_false-valid-deref.i false(valid-deref) 0 wit inspect .54 37 5.5 true -32 wit inspect 4.7  270 true -32 wit inspect 6.1   260   error (1) 0 wit inspect .59   19    - wit inspect
ldv-memsafety/memleaks_test23_2_false-valid-deref.i false(valid-deref) 0 wit inspect 11    220 160   exception 0 wit inspect 2.9  180 true -32 wit inspect 11     340   error (1) 0 wit inspect .63   19    - wit inspect
ldv-memsafety/memleaks_test23_4_false-valid-deref.i false(valid-deref) 0 wit inspect 11    220 110   exception 0 wit inspect 3.1  200 true -32 wit inspect 12     570   error (1) 0 wit inspect .59   19    - wit inspect
ldv-memsafety/memleaks_test11_1_false-valid-free.i false(valid-free) 0 wit inspect .56 37 4.9 true -32 wit inspect 5.2  270 true -32 wit inspect 6.0   260   error (1) 0 wit inspect .60   19    - wit inspect
ldv-memsafety/memleaks_test12_false-valid-free.i error (6) 0 wit inspect .67 38 6.9 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
ldv-memsafety/memleaks_test17_2_false-valid-free.i false(valid-free) 0 wit inspect 3.2  65 33   true -32 wit inspect 5.6  270 true -32 wit inspect 5.7   330   error (1) 0 wit inspect .60   20    - wit inspect
ldv-memsafety/memleaks_test19_false-valid-free.i false(valid-free) 0 wit inspect .54 37 5.1 true -32 wit inspect 6.0  260 true -32 wit inspect 5.6   250   error (1) 0 wit inspect .61   19    - wit inspect
ldv-memsafety/memleaks_test1_false-valid-free.i false(valid-free) 0 wit inspect .50 37 4.0 true -32 wit inspect 3.9  260 true -32 wit inspect 4.7   230   error (1) 0 wit inspect .62   18    - wit inspect
ldv-memsafety/memleaks_test3_false-valid-free.i false(valid-free) 1 wit inspect .49 37 4.2 false(valid-free) 1 wit inspect 3.7  250 false(valid-free) 1 wit inspect 5.2   260   error (1) 0 wit inspect .61   18    - wit inspect
ldv-memsafety/memleaks_test6_2_false-valid-free.i false(valid-free) 0 wit inspect .49 37 5.4 true -32 wit inspect 4.7  260 true -32 wit inspect 3.7   250   error (1) 0 wit inspect .59   18    - wit inspect
ldv-memsafety/memleaks_test8_2_false-valid-free.i false(valid-free) 0 wit inspect .47 37 5.3 true -32 wit inspect 4.0  260 true -32 wit inspect 4.8   230   error (1) 0 wit inspect .62   18    - wit inspect
ldv-memsafety/memleaks_test10_false-valid-memtrack_true-termination.i false(unreach-call) 0 wit inspect .53 37 6.8 true -32 wit inspect 3.1  270 unknown 0 wit inspect 16     340   error (1) 0 wit inspect .63   19    - wit inspect
ldv-memsafety/memleaks_test11_2_false-valid-memtrack_true-termination.i false(unreach-call) 0 wit inspect .55 37 5.6 true -32 wit inspect 4.9  270 unknown 0 wit inspect 9.7   310   error (1) 0 wit inspect .60   19    - wit inspect
ldv-memsafety/memleaks_test13_1_false-valid-memtrack_true-termination.i false(unreach-call) 0 wit inspect .49 37 4.5 true -32 wit inspect 4.1  250 unknown 0 wit inspect 13     290   error (1) 0 wit inspect .62   19    - wit inspect
ldv-memsafety/memleaks_test13_2_false-valid-memtrack.i false(unreach-call) 0 wit inspect .57 39 5.6 true -32 wit inspect 4.2  250 unknown 0 wit inspect 13     370   error (1) 0 wit inspect .63   18    - wit inspect
ldv-memsafety/memleaks_test14_1_false-valid-memtrack_true-termination.i false(unreach-call) 0 wit inspect .49 37 4.3 true -32 wit inspect 4.0  260 true -32 wit inspect 5.2   240   error (1) 0 wit inspect .59   19    - wit inspect
ldv-memsafety/memleaks_test14_2_false-valid-memtrack.i false(unreach-call) 0 wit inspect .58 38 5.4 true -32 wit inspect 4.6  250 true -32 wit inspect 5.8   260   error (1) 0 wit inspect .59   19    - wit inspect
ldv-memsafety/memleaks_test15_false-valid-memtrack.i false(unreach-call) 0 wit inspect .54 37 5.7 true -32 wit inspect 5.1  260 timeout 0 wit inspect 97     610   error (1) 0 wit inspect .59   19    - wit inspect
ldv-memsafety/memleaks_test16_1_false-valid-memtrack_true-termination.i false(unreach-call) 0 wit inspect .49 37 4.1 false(valid-memtrack) 1 wit inspect 4.1  250 true -32 wit inspect 5.1   250   error (1) 0 wit inspect .62   18    - wit inspect
ldv-memsafety/memleaks_test16_2_false-valid-memtrack_true-termination.i false(unreach-call) 0 wit inspect .47 37 4.5 false(valid-memtrack) 1 wit inspect 3.8  260 unknown 0 wit inspect 11     260   error (1) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/memleaks_test17_1_false-valid-memtrack.i false(unreach-call) 0 wit inspect 3.6  72 47   true -32 wit inspect 5.8  280 out of memory 0 wit inspect 65     7000   error (1) 0 wit inspect .60   20    - wit inspect
ldv-memsafety/memleaks_test17_3_false-valid-memtrack.i false(unreach-call) 0 wit inspect 3.4  65 35   true -32 wit inspect 5.3  280 out of memory 0 wit inspect 71     7000   error (1) 0 wit inspect .60   20    - wit inspect
ldv-memsafety/memleaks_test18_1_false-valid-memtrack_true-termination.i false(unreach-call) 0 wit inspect .54 37 5.1 false(valid-memtrack) 1 wit inspect 4.1  250 unknown 0 wit inspect 14     290   error (1) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/memleaks_test18_2_false-valid-memtrack_true-termination.i false(unreach-call) 0 wit inspect 3.0  53 32   true -32 wit inspect 5.6  270 unknown 0 wit inspect 21     600   error (1) 0 wit inspect .60   19    - wit inspect
ldv-memsafety/memleaks_test18_3_false-valid-memtrack_true-termination.i false(unreach-call) 0 wit inspect 2.4  38 33   true -32 wit inspect 51    1900 out of memory 0 wit inspect 60     7000   error (1) 0 wit inspect .63   19    - wit inspect
ldv-memsafety/memleaks_test1_false-valid-memtrack_true-termination.i false(unreach-call) 0 wit inspect .50 37 4.0 false(valid-memtrack) 1 wit inspect 4.1  250 unknown 0 wit inspect 10     260   error (1) 0 wit inspect .61   18    - wit inspect
ldv-memsafety/memleaks_test20_false-valid-memtrack_true-termination.i false(unreach-call) 0 wit inspect .47 37 4.5 false(valid-memtrack) 1 wit inspect 4.1  260 unknown 0 wit inspect 8.5   270   error (1) 0 wit inspect .59   18    - wit inspect
ldv-memsafety/memleaks_test21_false-valid-memtrack_true-termination.i false(unreach-call) 0 wit inspect .50 37 3.7 false(valid-memtrack) 1 wit inspect 4.0  270 unknown 0 wit inspect 7.1   270   error (1) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/memleaks_test22_1_false-valid-memtrack_true-termination.i false(unreach-call) 0 wit inspect .54 37 6.0 true -32 wit inspect 4.4  260 true -32 wit inspect 17     560   error (1) 0 wit inspect .59   19    - wit inspect
ldv-memsafety/memleaks_test22_2_false-valid-memtrack_true-termination.i false(unreach-call) 0 wit inspect .55 37 5.1 true -32 wit inspect 3.9  250 true -32 wit inspect 6.8   360   error (1) 0 wit inspect .59   19    - wit inspect
ldv-memsafety/memleaks_test22_4_false-valid-memtrack_true-termination.i false(unreach-call) 0 wit inspect .53 38 5.1 true -32 wit inspect 4.3  250 true -32 wit inspect 4.1   260   error (1) 0 wit inspect .63   19    - wit inspect
ldv-memsafety/memleaks_test4_false-valid-memtrack_true-termination.i false(unreach-call) 0 wit inspect .52 37 4.8 true -32 wit inspect 4.2  260 unknown 0 wit inspect 9.7   260   error (1) 0 wit inspect .59   18    - wit inspect
ldv-memsafety/memleaks_test5_1_false-valid-memtrack_true-termination.i false(unreach-call) 0 wit inspect .47 37 4.4 true -32 wit inspect 3.8  260 true -32 wit inspect 5.2   230   error (1) 0 wit inspect .59   18    - wit inspect
ldv-memsafety/memleaks_test5_2_false-valid-memtrack_true-termination.i false(unreach-call) 0 wit inspect .49 37 4.2 true -32 wit inspect 4.0  270 true -32 wit inspect 4.5   230   error (1) 0 wit inspect .59   18    - wit inspect
ldv-memsafety/memleaks_test6_1_false-valid-memtrack_true-termination.i false(unreach-call) 0 wit inspect .54 37 4.9 true -32 wit inspect 4.3  260 unknown 0 wit inspect 8.8   280   error (1) 0 wit inspect .59   18    - wit inspect
ldv-memsafety/memleaks_test6_3_false-valid-memtrack_true-termination.i false(unreach-call) 0 wit inspect .49 38 5.0 true -32 wit inspect 5.7  260 unknown 0 wit inspect 11     280   error (1) 0 wit inspect .62   18    - wit inspect
ldv-memsafety/memleaks_test7_false-valid-memtrack_true-termination.i false(unreach-call) 0 wit inspect .51 37 4.3 true -32 wit inspect 4.9  260 true -32 wit inspect 3.6   240   error (1) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/memleaks_test8_1_false-valid-memtrack_true-termination.i false(unreach-call) 0 wit inspect .51 37 4.1 false(valid-memtrack) 1 wit inspect 4.1  270 unknown 0 wit inspect 10     260   error (1) 0 wit inspect .62   18    - wit inspect
ldv-memsafety/memleaks_test9_1_false-valid-memtrack_true-termination.i false(unreach-call) 0 wit inspect .51 37 4.4 false(valid-memtrack) 1 wit inspect 4.2  250 unknown 0 wit inspect 7.7   260   error (1) 0 wit inspect .61   18    - wit inspect
ldv-memsafety/memleaks_test9_2_false-valid-memtrack_true-termination.i false(unreach-call) 0 wit inspect .49 37 4.5 false(valid-memtrack) 1 wit inspect 4.3  270 unknown 0 wit inspect 10     260   error (1) 0 wit inspect .58   18    - wit inspect
ldv-memsafety/memleaks_test10_true-valid-memsafety_true-termination.i true 2 wit inspect 1.1  38 11   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     800  
ldv-memsafety/memleaks_test11_true-valid-memsafety_true-termination.i true 2 wit inspect 1.1  39 9.2 - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     1100  
ldv-memsafety/memleaks_test12_true-valid-memsafety.i error (6) 0 wit inspect .63 37 7.7 - 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 1.0  37 9.3 - wit inspect - wit inspect - wit inspect true 2 wit inspect 92     1100  
ldv-memsafety/memleaks_test14_true-valid-memsafety.i true 2 wit inspect 1.0  39 11   - wit inspect - wit inspect - wit inspect true 2 wit inspect 86     1000  
ldv-memsafety/memleaks_test15_true-valid-memsafety_true-termination.i true 2 wit inspect 1.1  41 12   - 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 .93 37 8.4 - wit inspect - wit inspect - wit inspect true 2 wit inspect 11     450  
ldv-memsafety/memleaks_test17_1_true-valid-memsafety_true-termination.i true 2 wit inspect 5.0  71 53   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     2300  
ldv-memsafety/memleaks_test17_2_true-valid-memsafety_true-termination.i error (134) 0 wit inspect 280    14000 1800   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
ldv-memsafety/memleaks_test18_true-valid-memsafety_true-termination.i true 2 wit inspect 3.8  53 43   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     1400  
ldv-memsafety/memleaks_test19_true-valid-memsafety_true-termination.i true 2 wit inspect .99 38 9.4 - wit inspect - wit inspect - wit inspect true 2 wit inspect 330     850  
ldv-memsafety/memleaks_test1_true-valid-memsafety_true-termination.i true 2 wit inspect .91 37 8.4 - wit inspect - wit inspect - wit inspect true 2 wit inspect 10     310  
ldv-memsafety/memleaks_test20_true-valid-memsafety_true-termination.i true 2 wit inspect .89 37 9.5 - wit inspect - wit inspect - wit inspect true 2 wit inspect 11     470  
ldv-memsafety/memleaks_test21_true-valid-memsafety_true-termination.i true 2 wit inspect .90 37 8.6 - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.6   440  
ldv-memsafety/memleaks_test22_1_true-valid-memsafety_true-termination.i true 2 wit inspect .97 37 12   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     3100  
ldv-memsafety/memleaks_test22_2_true-valid-memsafety_true-termination.i true 2 wit inspect 1.0  38 8.9 - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     3100  
ldv-memsafety/memleaks_test22_3_true-valid-memsafety_true-termination.i true 2 wit inspect 1.0  37 12   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     2700  
ldv-memsafety/memleaks_test23_1_true-valid-memsafety.i error (42) 0 wit inspect 870    10000 8200   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
ldv-memsafety/memleaks_test23_3_true-valid-memsafety.i error (42) 0 wit inspect 870    10000 8400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
ldv-memsafety/memleaks_test3_true-valid-memsafety_true-termination.i true 2 wit inspect .90 37 9.5 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.5   350  
ldv-memsafety/memleaks_test4_true-valid-memsafety_true-termination.i true 2 wit inspect .91 37 9.6 - wit inspect - wit inspect - wit inspect true 2 wit inspect 29     500  
ldv-memsafety/memleaks_test5_true-valid-memsafety_true-termination.i true 2 wit inspect .90 37 9.5 - wit inspect - wit inspect - wit inspect true 2 wit inspect 11     420  
ldv-memsafety/memleaks_test6_true-valid-memsafety_true-termination.i true 2 wit inspect .93 37 8.2 - wit inspect - wit inspect - wit inspect true 2 wit inspect 17     560  
ldv-memsafety/memleaks_test7_true-valid-memsafety_true-termination.i true 2 wit inspect .94 37 8.7 - wit inspect - wit inspect - wit inspect true 2 wit inspect 18     530  
ldv-memsafety/memleaks_test8_true-valid-memsafety_true-termination.i true 2 wit inspect .91 37 8.9 - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.8   350  
ldv-memsafety/memleaks_test9_true-valid-memsafety_true-termination.i true 2 wit inspect .97 37 8.9 - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.7   360  
ldv-memsafety-bitfields/test-bitfields-1_true-valid-memsafety_true-termination.i true 2 wit inspect .80 34 9.0 - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 3.9   210  
ldv-memsafety-bitfields/test-bitfields-2.1_true-valid-memsafety_true-termination.i true 2 wit inspect .79 35 8.4 - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 3.6   200  
ldv-memsafety-bitfields/test-bitfields-2_true-valid-memsafety_true-termination.i true 2 wit inspect .85 36 6.6 - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 3.8   200  
ldv-memsafety-bitfields/test-bitfields-3.1_true-valid-memsafety_true-termination.i true 2 wit inspect .85 35 8.0 - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 3.4   200  
ldv-memsafety-bitfields/test-bitfields-3_true-valid-memsafety_true-termination.i true 2 wit inspect .86 34 8.6 - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 3.7   210  
ldv-memsafety-bitfields/test-bitfields-1_false-valid-deref.i false(valid-deref) 0 wit inspect .45 34 3.6 true -32 wit inspect 2.9  240 unknown 0 wit inspect 3.4   200   error (2) 0 wit inspect .58   18    - wit inspect
ldv-memsafety-bitfields/test-bitfields-2_false-valid-deref.i witness invalid (false(valid-deref)) 0 wit inspect .46 35 3.9 true -32 wit inspect 2.0  250 unknown 0 wit inspect 4.2   200   error (invalid witness file) 0 wit inspect .52   18    - wit inspect
ldv-memsafety-bitfields/test-bitfields-3.1_false-valid-deref.i witness invalid (false(valid-deref)) 0 wit inspect .46 35 3.7 true -32 wit inspect 2.8  240 unknown 0 wit inspect 2.9   200   error (invalid witness file) 0 wit inspect .54   18    - wit inspect
ldv-memsafety-bitfields/test-bitfields-3_false-valid-deref.i witness invalid (false(valid-deref)) 0 wit inspect .47 35 3.8 true -32 wit inspect 3.1  240 unknown 0 wit inspect 3.4   210   error (invalid witness file) 0 wit inspect .53   18    - wit inspect
ldv-memsafety-bitfields/test-bitfields-2.1_false-valid-free.i witness invalid (false(valid-free)) 0 wit inspect .44 34 4.4 true -32 wit inspect 2.8  250 unknown 0 wit inspect 3.4   200   error (invalid witness file) 0 wit inspect .52   19    - 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 123 28000 180000 220000 90 -1646 1400 47000 90 -1142 1600 110000 90 -298 59   1700 90 58 16000 43000
    correct results 68 123 1600 5800 15000 18 18 99 6100 10 10 89 5200 6 6 4.1 120 29 58 1000 14000
        correct true 55 110 1500 5000 13000 0 0 0 29 58 1000 14000
        correct false 13 13 120 810 1500 18 18 99 6100 10 10 89 5200 6 6 4.1 120 0
    correct-unconfimed results 16 0 62 1800 680 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 16 0 62 1800 680 0 0 0 0
    incorrect results 0 52 -1664 310 17000 37 -1152 330 19000 11 -304 7.4 210 0
        incorrect true 0 52 -1664 310 17000 35 -1120 280 17000 8 -256 5.4 150 0
        incorrect false 0 0 2 -32 50 1900 3 -48 2.0 57 0
score (180 tasks, max score: 270) 123 -1646 -1142 -298 58
Run set cbmc.sv-comp18.MemSafety-Heap cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.MemSafety-Heap uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.MemSafety-Heap fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.MemSafety-Heap uautomizer-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.MemSafety-Heap