Tool symbiotic 5.0.0-KLEE:1faddfe0-dg:12c34aac-symbiotic:5e14b94d-minisat:3db58943-llvm-instrumentation:cd767593-stp:17249213 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*
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]
Date of execution 2017-12-02 23:08:57 CET 2017-12-03 00:45:11 CET 2017-12-03 01:25:52 CET 2017-12-03 01:32:11 CET 2017-12-03 00:52:42 CET
Run set symbiotic.sv-comp18.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.MemSafety-LinkedLists
Options --witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-02_2308.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/symbiotic.2017-12-02_2308.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/symbiotic.2017-12-02_2308.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/symbiotic.2017-12-02_2308.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 0 900    850 10000   - - - 0 .019 4.9
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i 0 900    2700 6500   - - - 0 .020 4.8
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i 0 900    990 12000   - - - 0 .018 4.9
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i 0 900    2900 11000   - - - 0 .024 4.8
heap-manipulation/tree_false-unreach-call_false-valid-deref.i 1 .32 13 3.6 1 5.3 270 -32 8.1 280 -32 .75 18 -
heap-manipulation/tree_false-valid-deref.i 1 .32 13 3.3 1 5.4 270 1 8.3 290 1 .68 18 -
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i 0 .34 13 3.5 0 5.3 270 -32 8.2 290 -32 .85 18 -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i 1 .27 14 3.0 1 4.1 250 -32 9.3 280 -32 .71 18 -
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i 1 .27 14 3.2 1 4.6 250 -32 4.9 280 -16 .77 18 -
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i 1 .26 13 3.8 1 4.3 270 -32 8.0 280 -16 .67 18 -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i 0 900    2800 11000   - - - 0 .020 4.8
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i 0 .27 11 3.2 0 92   2900 -32 6.3 270 -16 .74 18 -
list-properties/list_true-unreach-call_false-valid-memtrack.i 1 .29 15 3.0 1 5.0 250 -32 8.3 260 -16 .93 18 -
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i 0 .25 11 2.8 0 92   2900 -32 6.7 260 -32 .70 18 -
list-properties/simple_true-unreach-call_false-valid-memtrack.i 1 .27 11 2.8 1 3.7 250 -32 8.9 270 -32 .88 18 -
list-properties/splice_true-unreach-call_false-valid-memtrack.i 1 .26 11 3.6 1 3.7 250 -32 6.3 270 -32 .82 19 -
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i 2 5.2  870 68   - - - 2 130     1400  
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i 2 4.0  710 49   - - - 2 260     1600  
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i 2 4.6  830 67   - - - 2 120     1600  
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i 1 4.0  700 49   1 6.8 320 -32 44   780 -32 1.6  19 -
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i 1 4.0  700 49   1 7.4 320 -32 40   780 -32 1.2  19 -
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i 1 4.0  700 53   1 6.9 330 -32 43   790 -32 1.4  19 -
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i 1 4.0  700 62   1 7.0 330 -32 47   780 -32 1.2  19 -
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i 1 4.0  700 43   1 6.5 340 -32 32   780 -32 1.2  21 -
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i 1 4.0  700 48   1 8.3 320 -32 42   770 -32 1.5  19 -
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i 1 4.0  700 46   1 4.3 320 -32 42   800 -32 1.4  19 -
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i 1 4.0  700 54   1 6.8 310 -32 44   790 -32 1.3  19 -
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i 1 4.1  700 53   1 7.6 320 -32 46   780 -32 1.3  18 -
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i 1 4.0  700 53   1 8.6 330 -32 52   780 -32 1.5  19 -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i 0 900    2900 6000   - - - 0 .024 4.8
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i 0 900    3400 11000   - - - 0 .019 4.8
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i 0 900    3300 5500   - - - 0 .024 4.8
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i 0 900    3000 10000   - - - 0 .023 4.8
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i 0 900    3200 5400   - - - 0 .020 4.8
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i 0 900    2700 6800   - - - 0 .019 4.8
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i 0 900    3700 11000   - - - 0 .024 4.9
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i 0 900    2000 8300   - - - 0 .018 4.8
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i 0 900    2700 11000   - - - 0 .025 5.0
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i 0 900    3400 5500   - - - 0 .021 4.8
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i 0 900    3300 6700   - - - 0 .023 4.9
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i 0 900    3400 9900   - - - 0 .020 4.9
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i 0 900    3000 7400   - - - 0 .018 4.8
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i 0 900    3200 12000   - - - 0 .023 4.8
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i 0 900    2800 7000   - - - 0 .026 4.8
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i 0 900    3100 5900   - - - 0 .022 4.8
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i 0 900    3700 11000   - - - 0 .019 4.9
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i 0 900    2000 11000   - - - 0 .024 5.0
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i 0 900    2600 8900   - - - 0 .020 4.8
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i 1 .26 13 3.3 1 5.8 260 -32 6.9 280 -32 .84 18 -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i 1 .29 14 3.8 1 5.0 260 -32 8.5 290 1 .69 18 -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i 1 .26 13 3.0 1 5.7 250 -32 8.4 280 -32 .73 18 -
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 27 22000    77000 210000   24 21 310 12000 24 -735 540   12000 24 -638 24   450 27 6 510 4700
    correct results 24 27 57    9600 730   21 21 120 6100 1 1 8.3 290 2 2 1.4 37 3 6 510 4600
        correct true 3 6 14    2400 180   0 0 0 3 6 510 4600
        correct false 21 21 43    7200 550   21 21 120 6100 1 1 8.3 290 2 2 1.4 37 0
    correct-unconfimed results 3 0 .86 35 9.6 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 3 0 .86 35 9.6 0 0 0 0
    incorrect results 0 0 23 -736 530   11000 22 -640 23   410 0
        incorrect true 0 0 23 -736 530   11000 18 -576 20   340 0
        incorrect false 0 0 0 4 -64 3.1 74 0
score (51 tasks, max score: 78) 27 21 -735 -638 6
Run set symbiotic.sv-comp18.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.MemSafety-LinkedLists