Tool ESBMC version 6.0.0 64-bit x86_64 linux 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* [apollon004; apollon069; apollon137; apollon154] 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-06 11:03:31 CET 2018-12-08 04:49:09 CET 2018-12-08 07:45:10 CET 2018-12-12 20:28:15 CET 2018-12-08 05:09:23 CET
Run set esbmc-kind.sv-comp19_prop-memsafety.MemSafety-MemCleanup cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-MemCleanup fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-MemCleanup
Options -s kinduction -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/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/esbmc-kind.2018-12-06_1103.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/esbmc-kind.2018-12-06_1103.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 error (1) 0 --- inspect .020 .021 5.5 .050 0   0   error (invalid witness file) 0 --- inspect .72 .43 40 0   0   error (2) 0 --- inspect .026 .027 5.6 0   0   error (invalid witness file) 0 --- inspect .0049 .0060 .53 0   0   - --- inspect
heap-manipulation/bubble_sort_linux_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .037 .038 5.3 .083 0   0   error (invalid witness file) 0 --- inspect .64 .40 41 0   0   error (2) 0 --- inspect .024 .025 5.7 0   0   error (invalid witness file) 0 --- inspect .0052 .0097 .52 0   0   - --- inspect
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .049 .051 5.5 .078 0   0   error (invalid witness file) 0 --- inspect .65 .40 41 0   0   error (2) 0 --- inspect .021 .022 5.7 0   0   error (invalid witness file) 0 --- inspect .0052 .0064 .52 0   0   - --- inspect
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .028 .030 5.5 .17  0   0   error (invalid witness file) 0 --- inspect .62 .39 41 0   0   error (2) 0 --- inspect .022 .024 5.6 0   0   error (invalid witness file) 0 --- inspect .0036 .0046 .49 0   0   - --- inspect
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .021 .022 5.4 .091 0   0   error (invalid witness file) 0 --- inspect .61 .37 40 0   0   error (2) 0 --- inspect .024 .024 5.6 0   0   error (invalid witness file) 0 --- inspect .0041 .0070 .41 0   0   - --- inspect
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .034 .035 5.5 .067 0   0   error (invalid witness file) 0 --- inspect .60 .36 41 0   0   error (2) 0 --- inspect .021 .023 5.7 0   0   error (invalid witness file) 0 --- inspect .0036 .0077 .52 0   0   - --- inspect
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .023 .025 5.5 .14  0   0   error (invalid witness file) 0 --- inspect .61 .37 40 0   0   error (2) 0 --- inspect .031 .036 5.6 0   0   error (invalid witness file) 0 --- inspect .0021 .0027 .52 0   0   - --- inspect
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .024 .025 5.4 .054 0   0   error (invalid witness file) 0 --- inspect .58 .35 41 0   0   error (2) 0 --- inspect .020 .021 5.7 0   0   error (invalid witness file) 0 --- inspect .0028 .0035 .53 0   0   - --- inspect
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .020 .021 5.5 .093 0   0   error (invalid witness file) 0 --- inspect .60 .37 41 0   0   error (2) 0 --- inspect .021 .022 5.8 0   0   error (invalid witness file) 0 --- inspect .0051 .0065 .53 0   0   - --- inspect
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .044 .045 5.4 .10  0   0   error (invalid witness file) 0 --- inspect .64 .39 40 0   0   error (2) 0 --- inspect .026 .027 5.7 0   0   error (invalid witness file) 0 --- inspect .0025 .0042 .53 0   0   - --- inspect
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .026 .027 5.5 .18  0   0   error (invalid witness file) 0 --- inspect .61 .38 41 0   0   error (2) 0 --- inspect .024 .026 5.6 0   0   error (invalid witness file) 0 --- inspect .0053 .0069 .53 0   0   - --- inspect
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .047 .050 5.3 .14  0   0   error (invalid witness file) 0 --- inspect .76 .46 43 0   0   error (2) 0 --- inspect .022 .023 5.6 0   0   error (invalid witness file) 0 --- inspect .0063 .0080 .41 0   0   - --- inspect
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .021 .021 5.4 .12  0   0   error (invalid witness file) 0 --- inspect .62 .38 41 0   0   error (2) 0 --- inspect .023 .024 5.6 0   0   error (invalid witness file) 0 --- inspect .0052 .0071 .53 0   0   - --- inspect
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .043 .045 5.3 .13  0   0   error (invalid witness file) 0 --- inspect .68 .43 40 0   0   error (2) 0 --- inspect .024 .024 5.6 0   0   error (invalid witness file) 0 --- inspect .0015 .0018 .41 0   0   - --- inspect
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .028 .030 5.3 .17  0   0   error (invalid witness file) 0 --- inspect .75 .46 41 0   0   error (2) 0 --- inspect .022 .024 5.7 0   0   error (invalid witness file) 0 --- inspect .0036 .0053 .53 0   0   - --- inspect
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .021 .022 5.4 .083 0   0   error (invalid witness file) 0 --- inspect .76 .47 41 0   0   error (2) 0 --- inspect .022 .023 5.7 0   0   error (invalid witness file) 0 --- inspect .0043 .0054 .40 0   0   - --- inspect
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .024 .025 5.4 .090 0   0   error (invalid witness file) 0 --- inspect .62 .39 40 0   0   error (2) 0 --- inspect .022 .024 5.6 0   0   error (invalid witness file) 0 --- inspect .0023 .0028 .53 0   0   - --- inspect
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .027 .028 5.3 .085 0   0   error (invalid witness file) 0 --- inspect .71 .44 41 0   0   error (2) 0 --- inspect .022 .023 5.6 0   0   error (invalid witness file) 0 --- inspect .0053 .0067 .52 0   0   - --- inspect
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .020 .021 5.4 .16  0   0   error (invalid witness file) 0 --- inspect .72 .44 41 0   0   error (2) 0 --- inspect .025 .027 5.6 0   0   error (invalid witness file) 0 --- inspect .0062 .0077 .53 0   0   - --- inspect
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .021 .022 5.5 .093 0   0   error (invalid witness file) 0 --- inspect .77 .48 41 0   0   error (2) 0 --- inspect .027 .027 5.6 0   0   error (invalid witness file) 0 --- inspect .0017 .0022 .53 0   0   - --- inspect
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .020 .021 5.3 .12  0   0   error (invalid witness file) 0 --- inspect .69 .43 40 0   0   error (2) 0 --- inspect .022 .023 5.6 0   0   error (invalid witness file) 0 --- inspect .0059 .0097 .53 0   0   - --- inspect
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .034 .035 5.5 .11  0   0   error (invalid witness file) 0 --- inspect .70 .42 41 0   0   error (2) 0 --- inspect .024 .026 5.7 0   0   error (invalid witness file) 0 --- inspect .0048 .0064 .53 0   0   - --- inspect
list-properties/list_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .027 .029 5.4 .15  0   0   error (invalid witness file) 0 --- inspect .75 .46 40 0   0   error (2) 0 --- inspect .022 .023 5.7 0   0   error (invalid witness file) 0 --- inspect .0055 .0065 .52 0   0   - --- inspect
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .020 .020 5.5 .11  0   0   error (invalid witness file) 0 --- inspect .60 .36 41 0   0   error (2) 0 --- inspect .021 .021 5.6 0   0   error (invalid witness file) 0 --- inspect .0019 .0025 .53 0   0   - --- inspect
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .020 .021 5.4 .063 0   0   error (invalid witness file) 0 --- inspect .58 .36 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0   0   error (invalid witness file) 0 --- inspect .0022 .0029 .53 0   0   - --- inspect
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .022 .022 5.4 .050 0   0   error (invalid witness file) 0 --- inspect .68 .42 40 0   0   error (2) 0 --- inspect .030 .031 5.6 0   0   error (invalid witness file) 0 --- inspect .0021 .0036 .53 0   0   - --- inspect
list-properties/simple_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .022 .024 5.5 .097 0   0   error (invalid witness file) 0 --- inspect .66 .40 40 0   0   error (2) 0 --- inspect .027 .027 5.6 0   0   error (invalid witness file) 0 --- inspect .0018 .0021 .39 0   0   - --- inspect
list-properties/splice_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .024 .025 5.4 .093 0   0   error (invalid witness file) 0 --- inspect .60 .38 40 0   0   error (2) 0 --- inspect .023 .024 5.6 0   0   error (invalid witness file) 0 --- inspect .0051 .0058 .40 0   0   - --- inspect
list-ext3-properties/dll_nullified_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .035 .036 5.5 .087 0   0   error (invalid witness file) 0 --- inspect .67 .42 40 0   0   error (2) 0 --- inspect .021 .023 5.7 0   0   error (invalid witness file) 0 --- inspect .0055 .0070 .54 0   0   - --- inspect
list-ext3-properties/sll_length_check_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .049 .053 5.4 .13  0   0   error (invalid witness file) 0 --- inspect .69 .42 40 0   0   error (2) 0 --- inspect .025 .026 5.6 0   0   error (invalid witness file) 0 --- inspect .0049 .0064 .52 0   0   - --- inspect
list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .038 .039 5.3 .086 0   0   error (invalid witness file) 0 --- inspect .75 .47 40 0   0   error (2) 0 --- inspect .024 .025 5.6 0   0   error (invalid witness file) 0 --- inspect .0050 .0062 .53 0   0   - --- inspect
list-ext3-properties/sll_of_sll_nondet_append_false-unreach-call_false-valid-memcleanup.i error (1) 0 --- inspect .047 .048 5.4 .090 0   0   error (invalid witness file) 0 --- inspect .60 .36 41 0   0   error (2) 0 --- inspect .024 .026 5.6 0   0   error (invalid witness file) 0 --- inspect .0050 .0066 .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 0 .94 .98 170 3.4 0   0   32 0 21 13 1300 0   0   32 0 .75 .79 180 0   0   32 0 .13 .18 16 0   0   0
    correct results 0 0 0 0 0
        correct true 0 0 0 0 0
        correct false 0 0 0 0 0
    incorrect results 0 0 0 0 0
        incorrect true 0 0 0 0 0
        incorrect false 0 0 0 0 0
score (32 tasks, max score: 32) 0 0 0 0 0
Run set esbmc-kind.sv-comp19_prop-memsafety.MemSafety-MemCleanup cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-MemCleanup fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-MemCleanup