Tool 2LS 0.7.2-sv-comp19 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CProver witness2test 0.1 ULTIMATE Automizer 0.1.23-635dfa2a
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.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-04 22:44:17 CET 2018-12-06 09:36:46 CET 2018-12-06 10:26:50 CET 2018-12-12 19:28:33 CET 2018-12-06 09:46:05 CET
Run set 2ls.sv-comp19_prop-memsafety.MemSafety-MemCleanup cpa-seq-validate-violation-witnesses-2ls.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-violation-witnesses-2ls.sv-comp19_prop-memsafety.MemSafety-MemCleanup fshell-witness2test-validate-violation-witnesses-2ls.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-correctness-witnesses-2ls.sv-comp19_prop-memsafety.MemSafety-MemCleanup
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -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 -witness ../../results-verified/2ls.2018-12-04_2244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/2ls.2018-12-04_2244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/2ls.2018-12-04_2244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/2ls.2018-12-04_2244.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu wall mem energy blkio-w blkio-r
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup_true-termination.i false(valid-memcleanup) 1 wit inspect .39 .38 32 4.2 .0082 0     false(valid-memcleanup) 1 wit inspect 5.7  3.1  270 0   0   true -32 --- inspect 13     7.6   470   .62 0   error (1) 0 --- inspect .57   .57   20    .016 0      - --- inspect
heap-manipulation/bubble_sort_linux_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .19 .19 28 1.7 .0082 0     error (invalid witness file) 0 --- inspect .59 .37 41 0   0   error (2) 0 --- inspect .023 .025 5.7 0    0   error (invalid witness file) 0 --- inspect .0047 .0057 .54 0     0      - --- inspect
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i error (5) 0 --- inspect 3.8  3.8  43 46   .0082 0     error (invalid witness file) 0 --- inspect .61 .38 42 0   0   error (2) 0 --- inspect .023 .024 5.6 0    0   error (invalid witness file) 0 --- inspect .0051 .0062 .53 0     0      - --- inspect
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect 360    360    3000 3200   .0082 .16  error (invalid witness file) 0 --- inspect .62 .39 40 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .0043 .0049 .40 0     0      - --- inspect
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900    900    4500 10000   .020  .070 error (invalid witness file) 0 --- inspect .76 .49 42 0   0   error (2) 0 --- inspect .023 .025 5.7 0    0   error (invalid witness file) 0 --- inspect .0061 .0076 .52 0     0      - --- inspect
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect 110    110    1400 1300   .0082 .16  error (invalid witness file) 0 --- inspect .59 .36 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .0047 .0058 .53 0     0      - --- inspect
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 13    13    360 160   .0082 0     false(valid-memcleanup) 1 wit inspect 4.8  2.6  260 0   0   error (7) 0 --- inspect 18     11     310   .68 0   error (1) 0 --- inspect .57   .57   20    .020 0      - --- inspect
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 2.5  2.5  82 30   .0082 0     false(valid-memcleanup) 1 wit inspect 5.2  2.9  250 0   0   error (7) 0 --- inspect 16     9.4   310   .68 0   error (1) 0 --- inspect .57   .57   20    .020 0      - --- inspect
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 9.1  9.1  200 100   .0082 0     false(valid-memcleanup) 1 wit inspect 5.2  2.9  250 0   0   error (7) 0 --- inspect 17     9.9   310   .71 0   error (1) 0 --- inspect .59   .59   20    .020 0      - --- inspect
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect 11    11    270 98   .0082 0     error (invalid witness file) 0 --- inspect .71 .44 40 0   0   error (2) 0 --- inspect .022 .025 5.7 0    0   error (invalid witness file) 0 --- inspect .0061 .0079 .53 0     0      - --- inspect
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 0 wit inspect 20    20    380 200   .0082 0     timeout 0 --- inspect 97    71    2400 0   0   error (7) 0 --- inspect 17     9.7   310   .68 0   error (1) 0 --- inspect .57   .57   20    .020 .0041 - --- inspect
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect 32    32    410 320   .0082 0     error (invalid witness file) 0 --- inspect .76 .46 40 0   0   error (2) 0 --- inspect .021 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .0019 .0027 .53 0     0      - --- inspect
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 1.2  1.2  57 15   .0082 0     false(valid-memcleanup) 1 wit inspect 5.8  3.2  250 0   0   error (7) 0 --- inspect 18     10     310   .75 0   error (1) 0 --- inspect .57   .57   20    .020 .029  - --- inspect
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect 41    41    720 390   .0082 .16  error (invalid witness file) 0 --- inspect .66 .43 41 0   0   error (2) 0 --- inspect .021 .023 5.7 0    0   error (invalid witness file) 0 --- inspect .0013 .0015 .40 0     0      - --- inspect
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 1.5  1.5  53 18   .0082 0     false(valid-memcleanup) 1 wit inspect 4.3  2.4  250 0   0   error (7) 0 --- inspect 16     9.5   310   .71 0   error (1) 0 --- inspect .57   .57   20    .020 0      - --- inspect
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 5.1  5.1  110 54   .0082 0     false(valid-memcleanup) 1 wit inspect 5.4  3.0  250 0   0   error (7) 0 --- inspect 17     9.8   310   .68 0   error (1) 0 --- inspect .58   .58   20    .020 0      - --- inspect
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect 5.5  5.5  150 63   .0082 0     error (invalid witness file) 0 --- inspect .77 .47 42 0   0   error (2) 0 --- inspect .022 .024 5.6 0    0   error (invalid witness file) 0 --- inspect .0054 .0072 .53 0     0      - --- inspect
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i error (5) 0 --- inspect 23    23    580 260   .0082 0     error (invalid witness file) 0 --- inspect .75 .45 40 0   0   error (2) 0 --- inspect .023 .024 5.6 0    0   error (invalid witness file) 0 --- inspect .0047 .0058 .53 0     0      - --- inspect
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 0 wit inspect 2.6  2.6  92 35   .0082 0     timeout 0 wit inspect 94    62    2400 0   0   error (7) 0 --- inspect 17     9.8   310   .71 0   error (1) 0 --- inspect .57   .57   20    .020 0      - --- inspect
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect 16    16    250 180   .0082 .025 error (invalid witness file) 0 --- inspect .73 .45 40 0   0   error (2) 0 --- inspect .021 .029 5.7 0    0   error (invalid witness file) 0 --- inspect .0054 .0065 .53 0     0      - --- inspect
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .58 .58 32 7.7 .0082 0     false(valid-memcleanup) 1 wit inspect 5.6  3.1  250 0   0   error (7) 0 --- inspect 16     10     310   .71 0   error (1) 0 --- inspect .57   .57   20    .020 0      - --- inspect
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .82 .82 34 9.8 .0082 .16  error (invalid witness file) 0 --- inspect .62 .37 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .0027 .0044 .52 0     0      - --- inspect
list-properties/list_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 0 wit inspect 4.0  4.0  85 44   .0082 0     timeout 0 wit inspect 93    66    2800 0   0   false(valid-memtrack) 0 --- inspect 8.7   4.9   310   .62 0   error (1) 0 --- inspect .56   .56   20    .016 0      - --- inspect
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .64 .63 31 8.0 .0082 0     false(valid-memcleanup) 1 wit inspect 5.6  3.0  270 0   0   false(valid-memtrack) 0 --- inspect 8.8   5.1   310   .66 0   error (1) 0 --- inspect .57   .57   20    .016 .025  - --- inspect
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 0 wit inspect .33 .33 29 4.0 .0082 0     true -32 wit inspect 5.3  2.9  250 0   0   true -32 --- inspect 8.1   4.6   310   .62 0   error (1) 0 --- inspect .58   .58   20    .016 0      - --- inspect
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .64 .64 35 10   .0082 0     false(valid-memcleanup) 1 wit inspect 6.5  3.5  270 0   0   true -32 --- inspect 9.3   5.7   320   .62 0   error (1) 0 --- inspect .60   .60   20    .029 0      - --- inspect
list-properties/simple_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .40 .40 30 4.1 .0082 .16  error (invalid witness file) 0 --- inspect .67 .43 40 0   0   error (2) 0 --- inspect .022 .023 5.7 0    0   error (invalid witness file) 0 --- inspect .0052 .0069 .53 0     0      - --- inspect
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect 2.3  2.3  74 27   .0082 0     false(valid-memcleanup) 1 wit inspect 5.3  2.9  250 0   0   false(valid-memtrack) 0 --- inspect 8.7   4.9   320   .62 0   error (1) 0 --- inspect .57   .57   20    .016 0      - --- inspect
list-ext3-properties/dll_nullified_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect 3.7  3.7  77 36   .0082 0     error (invalid witness file) 0 --- inspect .78 .48 42 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .0031 .0041 .53 0     0      - --- inspect
list-ext3-properties/sll_length_check_false-unreach-call_false-valid-memcleanup.i out of memory 0 --- inspect 150    150    15000 1300   .020  0     error (invalid witness file) 0 --- inspect .75 .47 40 0   0   error (2) 0 --- inspect .022 .023 5.7 0    0   error (invalid witness file) 0 --- inspect .0048 .0071 .54 0     0      - --- inspect
list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i out of memory 0 --- inspect 260    260    15000 2600   .012  0     error (invalid witness file) 0 --- inspect .75 .46 41 0   0   error (2) 0 --- inspect .019 .020 5.8 0    0   error (invalid witness file) 0 --- inspect .0056 .0067 .53 0     0      - --- inspect
list-ext3-properties/sll_of_sll_nondet_append_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900    900    4600 11000   .020  0     error (invalid witness file) 0 --- inspect .70 .43 40 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0   error (invalid witness file) 0 --- inspect .0052 .0063 .53 0     0      - --- inspect
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu wall mem energy blkio-w blkio-r
total 32 11 2900 2900 48000 32000 .30  .87 32 -21 360   240   11000 0   0   32 -96 210 120 4900 10   0   32 0 8.7 8.7 310 .29 .057 0
    correct results 11 11 37 37 1100 430 .090 0    11 11 60   32   2800 0   0   0 0 0
        correct true 0 0 0 0 0
        correct false 11 11 37 37 1100 430 .090 0    11 11 60   32   2800 0   0   0 0 0
    correct-unconfimed results 4 0 27 27 590 280 .033 0    0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 4 0 27 27 590 280 .033 0    0 0 0 0
    incorrect results 0 1 -32 5.3 2.9 250 0   0   3 -96 30 18 1100 1.9 0   0 0
        incorrect true 0 1 -32 5.3 2.9 250 0   0   3 -96 30 18 1100 1.9 0   0 0
        incorrect false 0 0 0 0 0
score (32 tasks, max score: 32) 11 -21 -96 0 0
Run set 2ls.sv-comp19_prop-memsafety.MemSafety-MemCleanup cpa-seq-validate-violation-witnesses-2ls.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-violation-witnesses-2ls.sv-comp19_prop-memsafety.MemSafety-MemCleanup fshell-witness2test-validate-violation-witnesses-2ls.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-correctness-witnesses-2ls.sv-comp19_prop-memsafety.MemSafety-MemCleanup