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-LinkedLists cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.MemSafety-LinkedLists
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
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 310    15000 2900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    12000 5700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    3000 8900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    780 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .68 29 6.5 timeout 0 wit inspect 92    3200 true -32 wit inspect 6.2   260   false(valid-deref) 1 wit inspect .67   18    - wit inspect
heap-manipulation/tree_false-valid-deref.i false(valid-deref) 1 wit inspect .20 27 1.9 false(valid-deref) 1 wit inspect 2.5  250 true -32 wit inspect 4.4   270   false(valid-deref) 1 wit inspect .67   18    - wit inspect
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .41 29 4.5 error (recursion) 0 wit inspect 2.5  250 true -32 wit inspect 5.9   250   true -32 wit inspect .65   18    - wit inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .64 30 7.5 timeout 0 wit inspect 93    2700 true -32 wit inspect 6.3   260   true -32 wit inspect .65   18    - wit inspect
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .78 30 7.2 error (invalid witness file) 0 wit inspect 2.0  180 true -32 wit inspect 4.1   250   error (1) 0 wit inspect .62   18    - wit inspect
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .74 29 6.2 error (invalid witness file) 0 wit inspect 3.2  170 true -32 wit inspect 4.2   250   error (1) 0 wit inspect .57   18    - wit inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    600 10000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .24 28 2.5 error (invalid witness file) 0 wit inspect 2.7  170 true -32 wit inspect 3.6   240   error (1) 0 wit inspect .57   18    - wit inspect
list-properties/list_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .44 29 4.4 timeout 0 wit inspect 91    2500 true -32 wit inspect 5.4   240   false(valid-deref) -16 wit inspect .64   18    - wit inspect
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .26 28 2.1 timeout 0 wit inspect 91    3000 true -32 wit inspect 3.5   230   true -32 wit inspect .64   19    - wit inspect
list-properties/simple_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .27 28 2.6 error (invalid witness file) 0 wit inspect 2.9  170 true -32 wit inspect 3.5   230   error (1) 0 wit inspect .57   18    - wit inspect
list-properties/splice_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .18 29 1.8 error (invalid witness file) 0 wit inspect 1.7  180 true -32 wit inspect 5.6   250   error (1) 0 wit inspect .57   18    - wit inspect
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i true 2 wit inspect .21 40 2.2 - wit inspect - wit inspect - wit inspect true 2 wit inspect 170     1700  
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i true 2 wit inspect .21 40 2.0 - wit inspect - wit inspect - wit inspect true 2 wit inspect 110     1600  
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i true 2 wit inspect .20 40 2.2 - wit inspect - wit inspect - wit inspect true 2 wit inspect 190     2000  
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 8.7  260 130   error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0011 .29 - wit inspect
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 6.5  250 92   error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .025 4.8 error (invalid witness file) 0 wit inspect .0010 .26 - wit inspect
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 8.7  250 100   error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0010 .28 - wit inspect
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 6.6  260 90   error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0036 .29 - wit inspect
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 8.7  250 120   error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 6.8  250 83   error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 8.7  250 96   error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .046 4.9 error (invalid witness file) 0 wit inspect .0010 .29 - wit inspect
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 9.3  260 110   error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0010 .26 - wit inspect
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 8.9  260 100   error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 8.9  250 110   error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0010 .29 - wit inspect
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    400 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    2700 10000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    380 8400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    580 9300   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    390 13000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.8
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    480 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 5.0
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    1100 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    670 8700   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    600 10000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    410 13000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 5.0
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    230 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    2700 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    390 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .023 4.9
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    460 10000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    410 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.8
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    420 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    610 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .025 4.9
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    520 10000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .86 29 8.0 false(valid-deref) 1 wit inspect 2.9  260 true -32 wit inspect 6.1   250   true -32 wit inspect .69   18    - wit inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .82 30 7.9 false(valid-deref) 1 wit inspect 2.8  260 true -32 wit inspect 6.5   270   error (2) 0 wit inspect .63   18    - wit inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .80 29 7.9 false(valid-deref) 1 wit inspect 4.1  250 true -32 wit inspect 5.7   250   true -32 wit inspect .66   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 51 11 21000    49000 250000   24 4 400 14000 24 -448 71 3600 24 -174 8.8  260 27 6 470 5400
    correct results 8 11 4.0  270 39   4 4 12 1000 0 2 2 1.3  37 3 6 470 5300
        correct true 3 6 .62 120 6.4 0 0 0 3 6 470 5300
        correct false 5 5 3.4  150 32   4 4 12 1000 0 2 2 1.3  37 0
    correct-unconfimed results 9 0 4.0  260 39   0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 9 0 4.0  260 39   0 0 0 0
    incorrect results 0 0 14 -448 71 3500 6 -176 3.9  110 0
        incorrect true 0 0 14 -448 71 3500 5 -160 3.3  92 0
        incorrect false 0 0 0 1 -16 .64 18 0
score (51 tasks, max score: 78) 11 4 -448 -174 6
Run set esbmc-kind.sv-comp18.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.MemSafety-LinkedLists