Tool ULTIMATE Automizer 0.1.23-635dfa2a 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-08 07:42:40 CET 2018-12-09 20:30:54 CET 2018-12-09 21:05:03 CET 2018-12-12 21:10:19 CET 2018-12-09 20:42:29 CET
Run set uautomizer.sv-comp19_prop-memsafety.MemSafety-MemCleanup cpa-seq-validate-violation-witnesses-uautomizer.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-violation-witnesses-uautomizer.sv-comp19_prop-memsafety.MemSafety-MemCleanup fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-correctness-witnesses-uautomizer.sv-comp19_prop-memsafety.MemSafety-MemCleanup
Options --full-output -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/uautomizer.2018-12-08_0742.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/uautomizer.2018-12-08_0742.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/uautomizer.2018-12-08_0742.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/uautomizer.2018-12-08_0742.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 true -32 wit inspect 16   6.3 530 140 .66 0     error (1) 0 --- inspect 1.1  .67 46 0   0      true -32 --- inspect 20     12     600   .62 0     error (1) 0 --- inspect .077  .078  11    0     .0041 - --- inspect
heap-manipulation/bubble_sort_linux_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   820   1100 12000 .64 0     error (invalid witness file) 0 --- inspect .63 .40 41 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0     error (invalid witness file) 0 --- inspect .0068 .010  .48 0     0      - --- inspect
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   840   1200 11000 .70 0     error (invalid witness file) 0 --- inspect .60 .36 40 0   .0041 error (2) 0 --- inspect .022 .022 5.6 0    0     error (invalid witness file) 0 --- inspect .0058 .0074 .53 0     0      - --- inspect
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i true -32 wit inspect 24   8.7 610 190 .66 0     error (1) 0 --- inspect 1.1  .68 46 0   0      true -32 --- inspect 31     19     690   .62 0     error (1) 0 --- inspect .078  .078  12    0     0      - --- inspect
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   850   2200 13000 .63 0     error (invalid witness file) 0 --- inspect .66 .41 40 0   0      error (2) 0 --- inspect .022 .024 5.7 0    0     error (invalid witness file) 0 --- inspect .0022 .0027 .41 0     0      - --- inspect
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   840   2300 11000 .70 0     error (invalid witness file) 0 --- inspect .81 .51 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     error (invalid witness file) 0 --- inspect .0050 .0063 .53 0     0      - --- inspect
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   830   1500 10000 .63 .016 error (invalid witness file) 0 --- inspect .74 .45 40 0   0      error (2) 0 --- inspect .020 .020 5.6 0    0     error (invalid witness file) 0 --- inspect .0060 .015  .52 0     0      - --- inspect
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   810   840 12000 .64 0     error (invalid witness file) 0 --- inspect .61 .38 40 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0     error (invalid witness file) 0 --- inspect .0020 .0025 .53 0     0      - --- inspect
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   850   2100 8800 .63 0     error (invalid witness file) 0 --- inspect .59 .36 41 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0     error (invalid witness file) 0 --- inspect .0050 .0077 .53 0     0      - --- inspect
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   810   960 9400 .63 0     error (invalid witness file) 0 --- inspect .79 .48 43 0   0      error (2) 0 --- inspect .022 .024 5.6 0    0     error (invalid witness file) 0 --- inspect .0048 .0059 .53 0     0      - --- inspect
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   780   1100 11000 .64 .016 error (invalid witness file) 0 --- inspect .79 .48 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     error (invalid witness file) 0 --- inspect .0019 .0021 .40 0     0      - --- inspect
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   800   2300 9800 .64 0     error (invalid witness file) 0 --- inspect .75 .47 40 0   .0041 error (2) 0 --- inspect .027 .027 5.6 0    0     error (invalid witness file) 0 --- inspect .0063 .0081 .54 0     0      - --- inspect
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   820   2600 12000 .69 0     error (invalid witness file) 0 --- inspect .73 .43 40 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0     error (invalid witness file) 0 --- inspect .0053 .0063 .53 0     0      - --- inspect
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   800   2200 12000 .70 0     error (invalid witness file) 0 --- inspect .77 .46 41 0   0      error (2) 0 --- inspect .020 .022 5.6 0    0     error (invalid witness file) 0 --- inspect .0049 .0061 .41 0     0      - --- inspect
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   830   750 10000 .63 0     error (invalid witness file) 0 --- inspect .72 .46 40 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0     error (invalid witness file) 0 --- inspect .0048 .0060 .53 0     0      - --- inspect
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   830   2200 11000 .69 15     error (invalid witness file) 0 --- inspect .78 .48 41 0   0      error (2) 0 --- inspect .022 .023 5.6 0    0     error (invalid witness file) 0 --- inspect .0022 .0027 .52 0     0      - --- inspect
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   780   2000 10000 .63 0     error (invalid witness file) 0 --- inspect .60 .37 41 0   0      error (2) 0 --- inspect .029 .030 5.5 0    0     error (invalid witness file) 0 --- inspect .0040 .0052 .53 0     0      - --- inspect
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   810   2200 9800 .69 0     error (invalid witness file) 0 --- inspect .71 .44 41 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0     error (invalid witness file) 0 --- inspect .0043 .016  .53 0     0      - --- inspect
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   780   2400 9300 .69 0     error (invalid witness file) 0 --- inspect .63 .38 41 0   0      error (2) 0 --- inspect .023 .024 5.6 0    0     error (invalid witness file) 0 --- inspect .0049 .0066 .53 0     0      - --- inspect
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   810   790 11000 .64 0     error (invalid witness file) 0 --- inspect .59 .36 42 0   0      error (2) 0 --- inspect .022 .022 5.6 0    0     error (invalid witness file) 0 --- inspect .0049 .0060 .54 0     0      - --- inspect
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   850   2400 11000 .70 0     error (invalid witness file) 0 --- inspect .80 .49 41 0   0      error (2) 0 --- inspect .021 .022 5.7 0    0     error (invalid witness file) 0 --- inspect .0021 .0029 .53 0     0      - --- inspect
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i true -32 wit inspect 25   11   740 220 .66 0     error (1) 0 --- inspect .89 .54 47 0   0      true -32 --- inspect 28     18     550   .62 .012 error (1) 0 --- inspect .076  .076  12    0     0      - --- inspect
list-properties/list_false-unreach-call_false-valid-memcleanup.i false(valid-memtrack) 0 wit inspect 12   4.3 580 110 .66 0     timeout (exception) 0 wit inspect 93    62    3500 0   .0082 false(valid-memtrack) 0 --- inspect 8.7   4.9   310   .62 0     error (2) 0 --- inspect .69   .68   20    .078 .025  - --- inspect
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i false(valid-memtrack) 0 wit inspect 10   3.5 390 79 .66 0     false(valid-memcleanup) 1 wit inspect 4.9  2.6  250 0   0      false(valid-memtrack) 0 --- inspect 8.2   4.7   310   .66 0     error (2) 0 --- inspect .66   .66   20    .078 0      - --- inspect
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i true -32 wit inspect 480   450   870 6200 .62 0     error (1) 0 --- inspect .71 .42 46 0   0      timeout 0 --- inspect 96     80     650   1.2  .037 error (1) 0 --- inspect .069  .069  12    0     0      - --- inspect
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   840   850 10000 .63 0     error (invalid witness file) 0 --- inspect .62 .38 42 0   0      error (2) 0 --- inspect .023 .024 5.7 0    0     error (invalid witness file) 0 --- inspect .0016 .0021 .53 0     0      - --- inspect
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(valid-memtrack) 0 wit inspect 13   4.5 510 100 .66 0     timeout 0 wit inspect 93    64    3400 0   0      false(valid-memtrack) 0 --- inspect 11     6.3   310   .66 0     true -32 --- inspect .65   .65   20    .078 0      - --- inspect
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(valid-memtrack) 0 wit inspect 9.8 3.2 390 73 .66 0     false(valid-memcleanup) 1 wit inspect 5.5  3.0  260 0   0      false(valid-memtrack) 0 --- inspect 9.1   5.3   310   .62 0     true -32 --- inspect .65   .65   20    .082 0      - --- inspect
list-ext3-properties/dll_nullified_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   830   2300 11000 .70 0     error (invalid witness file) 0 --- inspect .59 .36 40 0   0      error (2) 0 --- inspect .021 .022 5.7 0    0     error (invalid witness file) 0 --- inspect .0034 .0055 .54 0     0      - --- inspect
list-ext3-properties/sll_length_check_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   830   2200 12000 .69 0     error (invalid witness file) 0 --- inspect .77 .47 42 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0     error (invalid witness file) 0 --- inspect .0017 .0025 .53 0     0      - --- inspect
list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   850   1300 11000 .64 0     error (invalid witness file) 0 --- inspect .58 .35 41 0   0      error (2) 0 --- inspect .023 .025 5.6 0    0     error (invalid witness file) 0 --- inspect .0049 .0061 .53 0     0      - --- inspect
list-ext3-properties/sll_of_sll_nondet_append_false-unreach-call_false-valid-memcleanup.i timeout 0 --- inspect 900   880   970 11000 .63 0     error (invalid witness file) 0 --- inspect .67 .41 42 0   .0041 error (2) 0 --- inspect .021 .022 5.6 0    0     error (invalid witness file) 0 --- inspect .0067 .0086 .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 -128 22000 20000 45000 270000 21   15   32 2 220 140   8500 0   .020 32 -96 210 150 3900 5.6 .049 32 -64 3.0 3.1 140 .32 .029 0
    correct results 0 2 2 10 5.6 510 0   0     0 0 0
        correct true 0 0 0 0 0
        correct false 0 2 2 10 5.6 510 0   0     0 0 0
    incorrect results 4 -128 550 470 2700 6800 2.6 0   0 3 -96 79 49 1800 1.9 .012 2 -64 1.3 1.3 41 .16 0     0
        incorrect true 4 -128 550 470 2700 6800 2.6 0   0 3 -96 79 49 1800 1.9 .012 2 -64 1.3 1.3 41 .16 0     0
        incorrect false 0 0 0 0 0
score (32 tasks, max score: 32) -128 2 -96 -64 0
Run set uautomizer.sv-comp19_prop-memsafety.MemSafety-MemCleanup cpa-seq-validate-violation-witnesses-uautomizer.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-violation-witnesses-uautomizer.sv-comp19_prop-memsafety.MemSafety-MemCleanup fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-correctness-witnesses-uautomizer.sv-comp19_prop-memsafety.MemSafety-MemCleanup