Tool DIVINE CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 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-06 11:06:04 CET 2018-12-08 03:24:14 CET 2018-12-08 05:17:35 CET 2018-12-08 06:43:53 CET 2018-12-12 20:24:22 CET 2018-12-08 04:38:54 CET
Run set divine-smt.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-divine-smt.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-divine-smt.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-witness2test-validate-violation-witnesses-divine-smt.sv-comp19_prop-memsafety.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-divine-smt.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-divine-smt.sv-comp19_prop-memsafety.MemSafety-LinkedLists
Options -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/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true -witness ../../results-verified/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/divine-smt.2018-12-06_1106.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/divine-smt.2018-12-06_1106.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 (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)
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i false(valid-memtrack) -16 wit inspect 8.4 8.4 450 100 0      0   - --- inspect - --- inspect - --- inspect - --- inspect error (7) 0 --- inspect 20     12     360   .75 0   
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   230   410 8000 .0041 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0   
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i false(valid-memtrack) -16 wit inspect 8.7 8.8 450 100 0      0   - --- inspect - --- inspect - --- inspect - --- inspect error (7) 0 --- inspect 22     13     330   .75 0   
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   230   440 8100 .0041 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0   
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(valid-memtrack) -16 wit inspect 8.7 8.7 450 110 0      0   false(valid-deref) 1 wit inspect 6.5  3.5  250 0   0     error (7) 0 --- inspect 20     12     310   .75 0   timeout (exception) 0 --- inspect 92    66    3400 0     0    true -32 --- inspect .66   .66   20    .094 0     - --- inspect
heap-manipulation/tree_false-valid-deref.i false(valid-deref) 1 wit inspect 9.4 8.8 450 110 0      0   false(valid-deref) 1 wit inspect 5.7  3.0  250 0   0     error (7) 0 --- inspect 21     12     310   .75 0   timeout 0 --- inspect 92    71    2800 0     0    false(valid-deref) 1 --- inspect .66   .66   20    .094 0     - --- inspect
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 9.5 8.9 450 99 0      0   error (recursion) 0 wit inspect 5.2  2.8  270 0   0     true -32 --- inspect 16     9.3   450   .66 0   timeout (exception) 0 --- inspect 92    64    3400 0     0    true -32 --- inspect .66   .66   20    .090 0     - --- inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i unknown 0 --- inspect 8.5 8.5 450 97 0      0   error (invalid witness file) 0 --- inspect .68 .41 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .77 47 0     0    error (invalid witness file) 0 --- inspect .0043 .0059 .53 0     0     - --- inspect
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 8.5 8.5 450 100 0      0   false(valid-memtrack) 1 wit inspect 5.3  2.9  260 0   0     error (7) 0 --- inspect 17     10     310   .75 0   timeout 0 --- inspect 92    65    3500 0     0    false(valid-deref) -16 --- inspect .67   .69   20    .086 .025 - --- inspect
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 8.5 8.6 450 100 0      0   false(valid-memtrack) 1 wit inspect 6.7  3.6  260 0   0     error (7) 0 --- inspect 18     10     310   .75 0   timeout (exception) 0 --- inspect 93    65    3500 0     0    false(valid-deref) -16 --- inspect .66   .66   20    .086 0     - --- inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   230   400 8000 .0041 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0   
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 9.7 9.0 450 120 0      0   timeout 0 wit inspect 95    75    2200 0   .037 true -32 --- inspect 11     6.6   340   .66 0   timeout (exception) 0 --- inspect 92    63    3400 0     0    false(valid-deref) -16 --- inspect .68   .67   20    .078 0     - --- inspect
list-properties/list_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 8.5 8.5 440 110 0      0   false(valid-memtrack) 1 wit inspect 5.5  3.0  250 0   0     true -32 --- inspect 9.9   5.5   320   .66 0   timeout 0 --- inspect 97    66    3800 0     0    false(valid-deref) -16 --- inspect .66   .66   20    .078 0     - --- inspect
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 8.6 8.6 450 100 0      0   timeout 0 wit inspect 96    65    2700 0   0     true -32 --- inspect 11     6.1   320   .66 0   timeout (exception) 0 --- inspect 92    62    3100 0     0    true -32 --- inspect .65   .67   20    .074 0     - --- inspect
list-properties/simple_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 8.4 8.4 450 100 0      0   false(valid-memtrack) 1 wit inspect 5.9  3.2  260 0   0     true -32 --- inspect 9.9   5.5   320   .66 0   timeout (exception) 0 --- inspect 92    64    3100 0     0    true -32 --- inspect .65   .65   20    .078 .13  - --- inspect
list-properties/splice_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 8.5 8.6 450 97 0      0   false(valid-memtrack) 1 wit inspect 5.8  3.2  250 0   0     unknown 0 --- inspect 24     13     330   .75 0   timeout 0 --- inspect 96    66    3600 .033 0    true -32 --- inspect .65   .65   20    .082 .13  - --- inspect
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 21 0      0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.6 0    0   
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 22 0      0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0   
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 19 0      0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0   
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 23 0      0   error (invalid witness file) 0 --- inspect .76 .47 40 0   0     error (2) 0 --- inspect .022 .023 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .66 48 0     0    error (invalid witness file) 0 --- inspect .0019 .0030 .53 0     0     - --- inspect
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 21 0      0   error (invalid witness file) 0 --- inspect .73 .46 42 0   0     error (2) 0 --- inspect .023 .024 5.6 0    0   error (invalid witness file) 0 --- inspect 1.3  .80 47 0     0    error (invalid witness file) 0 --- inspect .0021 .0026 .53 0     0     - --- inspect
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 21 0      0   error (invalid witness file) 0 --- inspect .63 .38 40 0   0     error (2) 0 --- inspect .027 .027 5.5 0    0   error (invalid witness file) 0 --- inspect .95 .62 47 0     0    error (invalid witness file) 0 --- inspect .0026 .0033 .53 0     0     - --- inspect
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 20 0      0   error (invalid witness file) 0 --- inspect .61 .37 41 0   0     error (2) 0 --- inspect .022 .023 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .76 47 0     0    error (invalid witness file) 0 --- inspect .0060 .0077 .53 0     0     - --- inspect
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i error - divine failed with signal 11 0 --- inspect 1.6 1.7 200 21 0      0   error (invalid witness file) 0 --- inspect .72 .43 40 0   0     error (2) 0 --- inspect .028 .028 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .76 49 0     0    error (invalid witness file) 0 --- inspect .0055 .0073 .53 0     0     - --- inspect
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 20 0      0   error (invalid witness file) 0 --- inspect .57 .37 40 0   0     error (2) 0 --- inspect .028 .029 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .73 46 0     0    error (invalid witness file) 0 --- inspect .0053 .0075 .52 0     0     - --- inspect
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 22 0      0   error (invalid witness file) 0 --- inspect .67 .40 41 0   0     error (2) 0 --- inspect .026 .027 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .60 47 0     0    error (invalid witness file) 0 --- inspect .0050 .0062 .53 0     0     - --- inspect
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 20 0      0   error (invalid witness file) 0 --- inspect .67 .40 40 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .63 49 0     0    error (invalid witness file) 0 --- inspect .0018 .0023 .41 0     0     - --- inspect
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i error - divine failed with signal 11 0 --- inspect 1.6 1.7 200 21 0      0   error (invalid witness file) 0 --- inspect .61 .38 42 0   0     error (2) 0 --- inspect .027 .027 5.6 0    0   error (invalid witness file) 0 --- inspect 1.2  .76 47 0     0    error (invalid witness file) 0 --- inspect .0042 .0047 .40 0     0     - --- inspect
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i error - divine failed with signal 11 0 --- inspect 1.6 1.6 200 22 0      0   error (invalid witness file) 0 --- inspect .62 .38 41 0   0     error (2) 0 --- inspect .027 .029 5.7 0    0   error (invalid witness file) 0 --- inspect 1.2  .79 47 0     0    error (invalid witness file) 0 --- inspect .0016 .0018 .40 0     0     - --- inspect
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   230   670 8100 .0041 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0   
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   230   440 8000 .0041 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0   
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   230   1600 7900 .012  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0   
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   230   430 7600 .0041 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0   
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   230   440 8300 .0041 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0    0   
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   230   450 8200 .0041 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0   
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   230   510 7800 .0041 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0   
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   230   790 8000 .0041 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0   
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   230   400 8700 .0041 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .020 5.6 0    0   
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   230   500 8900 .0041 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .029 5.6 0    0   
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   240   970 9100 .0041 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .026 5.6 0    0   
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   230   430 9000 .0041 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0    0   
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   230   1000 8200 .0041 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0   
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   230   420 7500 .0041 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .025 5.6 0    0   
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   230   430 8200 .0041 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .025 5.7 0    0   
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   230   430 7800 .0041 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0   
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   230   460 8500 .0041 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0    0   
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   230   640 8200 .012  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .027 5.6 0    0   
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   230   400 7700 .012  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0   
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i unknown 0 --- inspect 8.5 8.5 440 97 0      0   error (invalid witness file) 0 --- inspect .76 .48 41 0   0     error (2) 0 --- inspect .028 .028 5.6 0    0   error (invalid witness file) 0 --- inspect 1.3  .84 47 0     0    error (invalid witness file) 0 --- inspect .0020 .0026 .53 0     0     - --- inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 8.6 8.5 450 120 0      0   false(valid-deref) 1 wit inspect 6.4  3.5  260 0   0     error (7) 0 --- inspect 24     14     310   .75 0   timeout 0 --- inspect 92    68    3400 0     0    false(valid-deref) 1 --- inspect .69   .69   20    .094 0     - --- inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i unknown 0 --- inspect 8.5 8.5 450 100 0      0   error (invalid witness file) 0 --- inspect .71 .44 41 0   0     error (2) 0 --- inspect .021 .022 5.7 0    0   error (invalid witness file) 0 --- inspect .97 .63 48 0     0    error (invalid witness file) 0 --- inspect .0053 .0064 .53 0     0     - --- inspect
list-simple/dll2c_append_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.4 8.4 390 110 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     940   1.7  0   
list-simple/dll2c_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.4 8.4 380 110 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     950   1.6  0   
list-simple/dll2c_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.3 8.3 390 98 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1000   .74 0   
list-simple/dll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.3 8.3 390 110 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     700   .68 0   
list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.3 8.3 390 98 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     840   1.6  0   
list-simple/dll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.5 8.5 380 100 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1000   .64 0   
list-simple/dll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.6 8.6 390 110 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     1300   1.7  0   
list-simple/dll2c_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.5 8.5 380 120 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     900     920   .70 0   
list-simple/dll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.3 8.3 390 110 0      0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 330     300     1000   .62 0   
list-simple/dll2c_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.5 8.5 390 100 0      0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 350     320     950   .62 0   
list-simple/dll2n_append_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.3 8.3 390 110 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     1400   .70 0   
list-simple/dll2n_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.3 8.3 390 120 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     1800   1.6  0   
list-simple/dll2n_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.3 8.3 390 100 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1100   1.6  0   
list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.1 8.1 390 93 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1800   1.6  0   
list-simple/dll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.3 8.3 390 100 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     800   .70 0   
list-simple/dll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.3 8.3 390 110 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     900   1.8  0   
list-simple/dll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.3 8.3 380 130 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     1200   1.6  0   
list-simple/dll2n_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.6 8.6 380 120 0      0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 170     140     960   .62 .76
list-simple/dll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.4 8.4 380 110 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     1800   .64 0   
list-simple/dll2n_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.3 8.3 380 120 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     1300   .64 0   
list-simple/sll2c_append_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.3 8.3 390 120 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1300   .64 0   
list-simple/sll2c_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.4 8.4 380 100 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1300   .63 0   
list-simple/sll2c_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.3 8.3 390 110 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1100   .64 0   
list-simple/sll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.3 8.3 390 100 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1100   1.5  0   
list-simple/sll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.2 8.2 380 120 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1400   1.6  0   
list-simple/sll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.5 8.5 390 94 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1400   1.3  0   
list-simple/sll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.2 8.3 390 98 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     890     780   1.8  0   
list-simple/sll2c_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.4 8.4 390 110 0      0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 370     330     710   .62 0   
list-simple/sll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.3 8.3 390 100 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     900     940   1.8  0   
list-simple/sll2c_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.3 8.3 390 120 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     900     900   1.6  0   
list-simple/sll2n_append_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.3 8.3 390 120 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     2200   .77 0   
list-simple/sll2n_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.3 8.3 390 120 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     2200   .72 0   
list-simple/sll2n_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.3 8.3 390 120 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     920   1.8  0   
list-simple/sll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.5 8.5 390 97 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1200   1.9  0   
list-simple/sll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.2 8.2 390 110 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     900   .73 0   
list-simple/sll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.3 8.3 390 110 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     800   1.8  0   
list-simple/sll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.3 8.3 380 110 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     900     880   .71 0   
list-simple/sll2n_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.2 8.2 380 110 0      0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 360     340     890   .62 0   
list-simple/sll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.2 8.2 390 99 0      0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 520     480     900   .62 0   
list-simple/sll2n_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.3 8.3 390 110 0      0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 670     630     920   .62 0   
list-ext3-properties/dll_circular_traversal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.2 8.2 390 120 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     3500   .69 0   
list-ext3-properties/dll_nondet_free_order_true-valid-memsafety.i true 2 wit inspect 8.4 8.4 390 98 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1900   .65 .12
list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.4 8.5 390 110 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     880     2100   .96 0   
list-ext3-properties/sll_circular_traversal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.2 8.2 390 97 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1300   1.7  0   
list-ext3-properties/sll_length_check_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.9 8.6 390 100 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     890     2600   .69 0   
list-ext3-properties/sll_nondet_insert_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 9.2 8.6 390 100 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     1100   .64 0   
list-ext3-properties/sll_of_sll_nondet_append_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 240   66   510 2100 0      0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     940     650   .64 0   
list-ext3-properties/sll_shallow_copy_true-valid-memsafety.i false(valid-deref) -16 wit inspect 8.3 8.3 450 100 0      0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 9.4   5.7   310   .66 0   
list-ext3-properties/dll_circular_traversal_false-valid-deref.i false(valid-deref) 1 wit inspect 8.4 8.4 450 100 0      0   false(valid-deref) 1 wit inspect 5.7  3.1  250 0   0     true -32 --- inspect 8.7   4.9   310   .62 0   unknown 0 --- inspect 6.2  3.5  260 0     1.5  false(valid-deref) 1 --- inspect .65   .65   20    .082 0     - --- inspect
list-ext3-properties/sll_circular_traversal_false-valid-deref.i false(valid-deref) 1 wit inspect 8.4 8.5 450 100 0      0   false(valid-deref) 1 wit inspect 6.4  3.4  260 0   0     true -32 --- inspect 9.2   5.3   320   .66 0   unknown 0 --- inspect 6.5  3.7  260 0     .14 false(valid-deref) 1 --- inspect .67   .68   20    .082 0     - --- inspect
list-ext3-properties/dll_nondet_free_order_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 8.6 8.7 450 130 0      0   false(valid-memtrack) 1 wit inspect 6.3  3.4  260 0   0     true -32 --- inspect 12     6.6   350   .66 0   unknown 0 --- inspect 6.6  3.8  280 0     0    false(valid-deref) -16 --- inspect .69   .68   20    .086 0     - --- inspect
list-ext3-properties/sll_shallow_copy_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 8.5 8.5 440 110 0      0   false(valid-memtrack) 1 wit inspect 5.4  2.9  270 0   0     true -32 --- inspect 9.0   5.2   310   .66 0   unknown 0 --- inspect 5.7  3.2  250 0     .18 true -32 --- inspect .70   .70   20    .070 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 (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)
total 103 41 21000 5800 43000 190000 .11 0   28 12 280 190 8800 0   .037 28 -288 220 130 5000 10   0   28 0 1100 740 39000 .033 1.9 28 -268 10   10   310 1.3  .29  75 16 41000 39000 60000 53   .88
    correct results 58 105 720 540 23000 8300 0    0   12 12 71 39 3100 0   0     0 0 4 4 2.7 2.7 81 .35 0     8 16 2800 2500 6600 5.0 .76
        correct true 47 94 620 450 18000 7100 0    0   0 0 0 0 8 16 2800 2500 6600 5.0 .76
        correct false 11 11 94 94 4900 1200 0    0   12 12 71 39 3100 0   0     0 0 4 4 2.7 2.7 81 .35 0     0
    correct-unconfimed results 3 0 28 27 1300 330 0    0   0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0
        correct-unconfirmed false 3 0 28 27 1300 330 0    0   0 0 0 0 0
    incorrect results 4 -64 34 34 1800 420 0    0   0 9 -288 96 55 3000 5.9 0   0 11 -272 7.3 7.4 220 .90 .29  0
        incorrect true 0 0 9 -288 96 55 3000 5.9 0   0 6 -192 4.0 4.0 120 .49 .26  0
        incorrect false 4 -64 34 34 1800 420 0    0   0 0 0 5 -80 3.4 3.4 100 .41 .025 0
score (103 tasks, max score: 178) 41 12 -288 0 -268 16
Run set divine-smt.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-divine-smt.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-divine-smt.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-witness2test-validate-violation-witnesses-divine-smt.sv-comp19_prop-memsafety.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-divine-smt.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-divine-smt.sv-comp19_prop-memsafety.MemSafety-LinkedLists