Tool symbiotic 6.0.3-77d4af47 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* [apollon013; apollon098] 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-07 21:42:05 CET 2018-12-08 23:40:56 CET 2018-12-09 00:46:04 CET 2018-12-12 21:10:03 CET 2018-12-08 23:47:25 CET
Run set symbiotic.sv-comp19_prop-memsafety.MemSafety-MemCleanup cpa-seq-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-MemCleanup fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-correctness-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-MemCleanup
Options --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/symbiotic.2018-12-07_2142.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/symbiotic.2018-12-07_2142.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/symbiotic.2018-12-07_2142.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/symbiotic.2018-12-07_2142.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 .25 .24 18 2.8 0   0     false(valid-memcleanup) 1 wit inspect 5.3 2.9 250 0   0      true -32 --- inspect 9.8 5.5 320 .62 0   true -32 --- inspect .65 .65 20 .078 0      - --- inspect
heap-manipulation/bubble_sort_linux_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .25 .25 18 2.8 0   0     false(valid-memcleanup) 1 wit inspect 5.9 3.2 260 0   .037  error (7) 0 --- inspect 21   12   360 .68 0   error (2) 0 --- inspect .70 .70 20 .13  0      - --- inspect
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 0 wit inspect .35 .36 22 3.1 0   5.0   error (recursion) 0 wit inspect 5.0 2.7 260 0   .0082 error (7) 0 --- inspect 21   13   340 .68 0   error (2) 0 --- inspect .68 .68 20 .12  0      - --- inspect
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .25 .25 17 3.3 0   0     false(valid-memcleanup) 1 wit inspect 4.8 2.6 250 0   0      error (7) 0 --- inspect 21   12   320 .68 0   true -32 --- inspect .67 .67 20 .11  0      - --- inspect
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .27 .26 18 3.4 0   0     false(valid-memcleanup) 1 wit inspect 6.1 3.2 260 0   0      error (7) 0 --- inspect 20   12   330 .68 0   error (2) 0 --- inspect .68 .68 20 .11  0      - --- inspect
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .26 .26 17 2.8 0   0     false(valid-memcleanup) 1 wit inspect 6.6 3.6 250 0   .025  error (7) 0 --- inspect 17   9.7 310 .68 0   true -32 --- inspect .67 .67 20 .094 .025  - --- inspect
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .25 .24 17 3.0 0   0     false(valid-memcleanup) 1 wit inspect 4.9 2.6 260 0   0      error (7) 0 --- inspect 19   12   330 .68 0   error (2) 0 --- inspect .67 .67 20 .094 .025  - --- inspect
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .24 .23 19 3.5 0   0     false(valid-memcleanup) 1 wit inspect 4.9 2.7 250 0   0      error (7) 0 --- inspect 16   9.0 310 .68 0   timeout 0 --- inspect 96    96    20 .098 0      - --- inspect
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .24 .23 18 2.8 0   0     false(valid-memcleanup) 1 wit inspect 5.6 3.1 250 0   .58   error (7) 0 --- inspect 17   9.9 310 .68 0   error (2) 0 --- inspect .66 .66 20 .090 .025  - --- inspect
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .26 .25 18 2.4 0   0     false(valid-memcleanup) 1 wit inspect 5.7 3.0 260 0   .0082 error (7) 0 --- inspect 17   10   310 .68 0   true -32 --- inspect .66 .66 20 .094 0      - --- inspect
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .25 .24 18 3.2 0   0     false(valid-memcleanup) 1 wit inspect 5.5 3.0 250 0   0      error (7) 0 --- inspect 17   9.5 310 .68 0   error (2) 0 --- inspect .67 .69 20 .086 0      - --- inspect
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .24 .24 18 2.9 0   0     false(valid-memcleanup) 1 wit inspect 5.1 2.8 250 0   0      error (7) 0 --- inspect 18   10   310 .68 0   error (2) 0 --- inspect .66 .66 20 .094 0      - --- inspect
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .23 .23 17 3.0 0   0     false(valid-memcleanup) 1 wit inspect 4.4 2.5 250 0   0      error (7) 0 --- inspect 17   9.6 310 .68 0   true -32 --- inspect .65 .65 20 .086 0      - --- inspect
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .27 .26 17 4.1 0   .025 false(valid-memcleanup) 1 wit inspect 5.2 2.8 270 0   0      error (7) 0 --- inspect 16   10   310 .68 0   true -32 --- inspect .65 .66 20 .090 0      - --- inspect
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .23 .22 17 3.0 0   0     false(valid-memcleanup) 1 wit inspect 5.1 2.8 250 0   .63   error (7) 0 --- inspect 16   8.9 310 .71 0   timeout 0 --- inspect 96    96    20 .098 .0041 - --- inspect
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .23 .22 18 2.6 0   0     false(valid-memcleanup) 1 wit inspect 4.8 2.6 250 0   0      error (7) 0 --- inspect 17   9.8 310 .68 0   error (2) 0 --- inspect .66 .66 20 .090 0      - --- inspect
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .26 .26 18 3.2 0   0     false(valid-memcleanup) 1 wit inspect 5.0 2.7 250 0   0      error (7) 0 --- inspect 17   9.8 310 .68 0   true -32 --- inspect .65 .65 20 .090 0      - --- inspect
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .30 .29 17 2.5 0   0     false(valid-memcleanup) 1 wit inspect 5.4 2.9 280 0   0      error (7) 0 --- inspect 17   10   310 .68 0   true -32 --- inspect .64 .64 20 .086 0      - --- inspect
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .26 .25 18 3.2 0   0     false(valid-memcleanup) 1 wit inspect 4.5 2.4 250 0   0      error (7) 0 --- inspect 16   9.2 310 .68 0   error (2) 0 --- inspect .66 .66 20 .086 .029  - --- inspect
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .26 .26 18 3.5 0   0     false(valid-memcleanup) 1 wit inspect 13   6.7 440 0   0      error (7) 0 --- inspect 17   9.8 310 .71 0   error (2) 0 --- inspect .66 .66 20 .090 0      - --- inspect
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .22 .22 18 2.4 0   0     false(valid-memcleanup) 1 wit inspect 5.1 2.7 260 0   0      error (7) 0 --- inspect 16   9.3 310 .68 0   true -32 --- inspect .67 .68 20 .086 0      - --- inspect
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .26 .25 18 3.3 0   0     false(valid-memcleanup) 1 wit inspect 5.3 2.9 250 0   .029  true -32 --- inspect 9.0 5.5 320 .62 0   true -32 --- inspect .67 .67 20 .078 0      - --- inspect
list-properties/list_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .26 .25 18 3.6 0   0     false(valid-memcleanup) 1 wit inspect 5.6 3.0 270 0   0      true -32 --- inspect 9.2 5.6 320 .62 0   error (2) 0 --- inspect .68 .68 20 .078 0      - --- inspect
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .26 .25 18 3.2 0   0     false(valid-memcleanup) 1 wit inspect 4.1 2.2 250 0   .0082 true -32 --- inspect 9.6 5.4 320 .62 0   error (2) 0 --- inspect .69 .69 20 .078 0      - --- inspect
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .19 .19 16 2.1 0   0     false(valid-memcleanup) 1 wit inspect 5.5 3.0 270 0   .029  true -32 --- inspect 9.2 5.5 330 .62 0   true -32 --- inspect .65 .66 20 .078 0      - --- inspect
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .20 .19 16 2.2 0   0     false(valid-memcleanup) 1 wit inspect 5.1 2.8 250 0   0      true -32 --- inspect 9.6 5.7 340 .62 0   true -32 --- inspect .67 .67 20 .098 0      - --- inspect
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .25 .24 19 2.8 0   0     false(valid-memcleanup) 1 wit inspect 4.6 2.5 250 0   0      true -32 --- inspect 9.6 5.4 320 .62 0   true -32 --- inspect .63 .63 20 .078 0      - --- inspect
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .25 .24 18 2.8 0   0     false(valid-memcleanup) 1 wit inspect 5.4 2.9 270 0   0      true -32 --- inspect 9.4 5.3 320 .62 0   true -32 --- inspect .65 .64 20 .082 0      - --- inspect
list-ext3-properties/dll_nullified_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .27 .26 17 2.7 0   0     false(valid-memcleanup) 1 wit inspect 8.7 4.6 380 0   0      true -32 --- inspect 9.2 5.6 320 .62 0   error (2) 0 --- inspect .66 .66 20 .086 0      - --- inspect
list-ext3-properties/sll_length_check_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .30 .29 18 4.1 0   0     false(valid-memcleanup) 1 wit inspect 5.4 2.9 250 0   0      true -32 --- inspect 8.3 5.1 310 .62 0   true -32 --- inspect .64 .66 20 .078 0      - --- inspect
list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .31 .30 18 3.5 0   0     false(valid-memcleanup) 1 wit inspect 5.3 2.9 260 0   0      true -32 --- inspect 8.6 4.8 310 .62 0   error (2) 0 --- inspect .66 .66 20 .098 0      - --- inspect
list-ext3-properties/sll_of_sll_nondet_append_false-unreach-call_false-valid-memcleanup.i false(valid-memcleanup) 1 wit inspect .32 .31 18 3.5 0   0     false(valid-memcleanup) 1 wit inspect 9.1 4.8 400 0   0      true -32 --- inspect 8.7 5.4 310 .62 0   error (2) 0 --- inspect .66 .66 20 .10  .0041 - --- 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 31 8.2  8.0  570 97   0   5.0   32 31 180 98 8700 0   1.4 32 -384 460 270 10000 21   0   32 -480 210   210   650 2.9 .11  0
    correct results 31 31 7.9  7.7  550 94   0   .025 31 31 180 95 8400 0   1.4 0 0 0
        correct true 0 0 0 0 0
        correct false 31 31 7.9  7.7  550 94   0   .025 31 31 180 95 8400 0   1.4 0 0 0
    correct-unconfimed results 1 0 .35 .36 22 3.1 0   5.0   0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 1 0 .35 .36 22 3.1 0   5.0   0 0 0 0
    incorrect results 0 0 12 -384 110 65 3800 7.5 0   15 -480 9.8 9.9 300 1.3 .025 0
        incorrect true 0 0 12 -384 110 65 3800 7.5 0   15 -480 9.8 9.9 300 1.3 .025 0
        incorrect false 0 0 0 0 0
score (32 tasks, max score: 32) 31 31 -384 -480 0
Run set symbiotic.sv-comp19_prop-memsafety.MemSafety-MemCleanup cpa-seq-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-MemCleanup fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-MemCleanup uautomizer-validate-correctness-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-MemCleanup