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-LinkedLists cpa-seq-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.MemSafety-LinkedLists
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
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    6600 6100   - 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    9700 5400   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.8
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    1600 8000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    840 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(valid-memtrack) -16 wit inspect 1.2  32 11   error (invalid witness file) 0 wit inspect 2.7  170 true -32 wit inspect 4.3   250   error (1) 0 wit inspect .57   18    - wit inspect
heap-manipulation/tree_false-valid-deref.i false(valid-deref) 1 wit inspect .11 27 1.1 false(valid-deref) 1 wit inspect 3.3  250 true -32 wit inspect 6.3   250   false(valid-deref) 1 wit inspect .65   18    - wit inspect
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .75 30 6.5 error (invalid witness file) 0 wit inspect 3.2  180 true -32 wit inspect 6.1   250   error (1) 0 wit inspect .57   18    - wit inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 1.1  33 12   timeout 0 wit inspect 92    2600 true -32 wit inspect 6.1   270   true -32 wit inspect .69   18    - wit inspect
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 1.3  32 15   timeout 0 wit inspect 91    2500 true -32 wit inspect 5.6   250   false(valid-deref) -16 wit inspect .65   18    - wit inspect
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .93 32 10   timeout 0 wit inspect 97    2300 true -32 wit inspect 6.5   260   false(valid-deref) -16 wit inspect .65   18    - wit inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    500 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .21 28 1.8 timeout 0 wit inspect 91    2700 true -32 wit inspect 3.6   240   false(valid-deref) -16 wit inspect .67   18    - wit inspect
list-properties/list_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .19 29 1.7 timeout 0 wit inspect 92    2700 true -32 wit inspect 3.9   250   false(valid-deref) -16 wit inspect .65   18    - wit inspect
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .41 28 3.4 timeout 0 wit inspect 93    2900 true -32 wit inspect 3.5   230   true -32 wit inspect .68   18    - wit inspect
list-properties/simple_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .54 29 4.8 timeout 0 wit inspect 92    2900 true -32 wit inspect 5.2   240   true -32 wit inspect .64   18    - wit inspect
list-properties/splice_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .15 29 1.6 timeout 0 wit inspect 96    3400 true -32 wit inspect 5.3   240   true -32 wit inspect .64   18    - wit inspect
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i true 2 wit inspect .22 40 2.8 - wit inspect - wit inspect - wit inspect true 2 wit inspect 87     1600  
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i true 2 wit inspect .23 40 2.0 - wit inspect - wit inspect - wit inspect true 2 wit inspect 110     1500  
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i true 2 wit inspect .24 40 2.4 - wit inspect - wit inspect - wit inspect true 2 wit inspect 110     1500  
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 6.9  230 91   error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .017 4.9 error (invalid witness file) 0 wit inspect .0010 .26 - wit inspect
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 6.9  230 77   error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 6.8  230 83   error (invalid witness file) 0 wit inspect .55 45 error (2) 0 wit inspect .046 4.8 error (invalid witness file) 0 wit inspect .0029 .26 - wit inspect
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 6.7  230 92   error (invalid witness file) 0 wit inspect .44 41 error (2) 0 wit inspect .035 4.8 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 5.2  230 57   error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 4.7  230 56   error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0018 .26 - wit inspect
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 6.7  220 75   error (invalid witness file) 0 wit inspect .42 42 error (2) 0 wit inspect .046 4.9 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 5.4  230 68   error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 4.8  230 64   error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .039 5.0 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 4.8  230 56   error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .0010 .26 - wit inspect
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    380 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    2700 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    460 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    570 13000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    450 13000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    530 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    1100 10000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    730 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
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 .019 4.8
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    390 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    210 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .035 4.9
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    2600 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .017 4.8
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    460 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
forester-heap/sll-queue_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 .024 5.0
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    430 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 5.0
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    430 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.8
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    840 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    760 12000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .024 4.9
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    540 11000   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 1.5  32 14   false(valid-deref) 1 wit inspect 3.9  250 true -32 wit inspect 4.1   250   true -32 wit inspect .65   18    - wit inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .41 29 5.3 false(valid-deref) 1 wit inspect 3.7  250 true -32 wit inspect 6.3   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 .99 32 12   false(valid-deref) 1 wit inspect 2.7  260 true -32 wit inspect 4.2   250   true -32 wit inspect .65   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 -6 22000    37000 260000   24 4 770 24000 24 -448 71 3500 24 -255 9.0  260 27 6 310 4800
    correct results 7 10 3.7  240 40   4 4 14 1000 0 1 1 .65 18 3 6 310 4600
        correct true 3 6 .69 120 7.2 0 0 0 3 6 310 4600
        correct false 4 4 3.0  120 32   4 4 14 1000 0 1 1 .65 18 0
    correct-unconfimed results 9 0 5.6  270 57   0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 9 0 5.6  270 57   0 0 0 0
    incorrect results 1 -16 1.2  32 11   0 14 -448 71 3500 10 -256 6.6  180 0
        incorrect true 0 0 14 -448 71 3500 6 -192 3.9  110 0
        incorrect false 1 -16 1.2  32 11   0 0 4 -64 2.6  73 0
score (51 tasks, max score: 78) -6 4 -448 -255 6
Run set esbmc-incr.sv-comp18.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.MemSafety-LinkedLists