Tool ULTIMATE Automizer 0.1.23-3204b741 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-03 04:39:25 CET 2017-12-03 05:43:13 CET 2017-12-03 06:05:52 CET 2017-12-03 06:06:56 CET 2017-12-03 05:47:48 CET
Run set uautomizer.sv-comp18.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.MemSafety-LinkedLists
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/uautomizer.2017-12-03_0439.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/uautomizer.2017-12-03_0439.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/uautomizer.2017-12-03_0439.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/uautomizer.2017-12-03_0439.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 error (7) 0 wit inspect 410   1200 4800 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 5.0
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   1600 11000 - 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   1200 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   960 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.8
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 320   880 4400 false(valid-deref) 1 wit inspect 3.8  250 false(valid-deref) 1 wit inspect 8.5   320   true -32 wit inspect .68   19    - wit inspect
heap-manipulation/tree_false-valid-deref.i false(valid-deref) 1 wit inspect 5.7 300 47 false(valid-deref) 1 wit inspect 3.4  250 true -32 wit inspect 7.4   280   false(valid-deref) 1 wit inspect .68   18    - wit inspect
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   1000 11000 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .0013 .28 - wit inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 51   760 490 error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   860 10000 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0014 .30 - wit inspect
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i error (7) 0 wit inspect 230   880 2600 error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i error (7) 0 wit inspect 210   850 2400 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 13   320 100 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .0025 .31 - wit inspect
list-properties/list_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 20   540 190 error (invalid witness file) 0 wit inspect .82 43 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .0030 .34 - wit inspect
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 14   340 110 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0014 .32 - wit inspect
list-properties/simple_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 18   470 150 error (invalid witness file) 0 wit inspect .67 42 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .0033 .34 - wit inspect
list-properties/splice_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 13   320 110 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i true 2 wit inspect 160   1800 950 - wit inspect - wit inspect - wit inspect true 2 wit inspect 120     1500  
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i true 2 wit inspect 150   1900 850 - wit inspect - wit inspect - wit inspect true 2 wit inspect 170     1700  
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i true 2 wit inspect 140   1800 1000 - wit inspect - wit inspect - wit inspect true 2 wit inspect 110     1400  
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 430   1900 2900 error (invalid witness file) 0 wit inspect .70 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 430   1900 2700 error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 430   1900 3600 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 430   1900 2900 error (invalid witness file) 0 wit inspect .59 42 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 430   1900 3300 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .0011 .29 - wit inspect
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 430   1900 3700 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect .0038 .26 - wit inspect
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 440   1800 2500 error (invalid witness file) 0 wit inspect .42 42 error (2) 0 wit inspect .048 4.9 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 430   1800 3200 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 430   1800 3200 error (invalid witness file) 0 wit inspect .56 45 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 420   1900 3200 error (invalid witness file) 0 wit inspect .78 43 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   1600 12000 - 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   990 13000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .021 4.9
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   1100 12000 - 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   960 9300 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   1200 9200 - 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   880 10000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
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 .021 4.9
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   1200 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i error (7) 0 wit inspect 250   1300 2700 - 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   1600 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
forester-heap/sll-buckets_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 4.9
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   880 9200 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 750   1100 9000 - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     950  
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   950 9600 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   1200 11000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .022 4.8
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   900 10000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 5.0
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   3000 7600 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 5.0
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   1100 12000 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i error (7) 0 wit inspect 300   890 3400 - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.8
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 73   1100 760 false(valid-deref) 1 wit inspect 3.6  250 false(valid-deref) 1 wit inspect 8.7   310   true -32 wit inspect .65   19    - wit inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 130   760 1400 false(valid-deref) 1 wit inspect 4.0  250 true -32 wit inspect 9.7   320   false(valid-deref) 1 wit inspect .70   18    - wit inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 42   1000 450 false(valid-deref) 1 wit inspect 4.1  270 false(valid-deref) 1 wit inspect 7.1   300   true -32 wit inspect .69   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 51 13 27000 62000 290000 24 5 30 2100 24 -61 42 1600 24 -94 3.4 98 27 6 1400 5700
    correct results 9 13 1800 11000 19000 5 5 19 1300 3 3 24 930 2 2 1.4 37 3 6 400 4600
        correct true 4 8 1200 6500 12000 0 0 0 3 6 400 4600
        correct false 5 5 570 4100 7000 5 5 19 1300 3 3 24 930 2 2 1.4 37 0
    incorrect results 0 0 2 -64 17 600 3 -96 2.0 56 0
        incorrect true 0 0 2 -64 17 600 3 -96 2.0 56 0
        incorrect false 0 0 0 0 0
score (51 tasks, max score: 78) 13 5 -61 -94 6
Run set uautomizer.sv-comp18.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.MemSafety-LinkedLists