Tool ESBMC version 6.0.0 64-bit x86_64 linux 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* [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-08 09:00:44 CET 2018-12-12 20:28:15 CET 2018-12-08 05:09:23 CET
Run set esbmc-kind.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-LinkedLists
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 -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true -witness ../../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 (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 timeout 0 --- inspect 900    900    6500 7200   1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .029 5.5 0    0   
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i out of memory 0 --- inspect 22    21    15000 270   1.1  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .026 5.6 0    0   
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900    900    1800 9500   1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0   
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900    900    820 11000   1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .022 5.8 0    0   
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .36 .36 29 4.3 1.0  0   false(valid-deref) 1 wit inspect 5.6 3.0 260 0   0   error (7) 0 --- inspect 18   10   310 .71 0   timeout 0 --- inspect 98   68   3900 0     0   false(valid-deref) 1 --- inspect .66 .66 20 .094 0     - --- inspect
heap-manipulation/tree_false-valid-deref.i false(valid-deref) 1 wit inspect .11 .11 27 1.3 1.0  0   false(valid-deref) 1 wit inspect 5.2 2.8 270 0   0   error (7) 0 --- inspect 21   12   320 .71 0   timeout 0 --- inspect 93   69   3200 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 .25 .25 27 3.1 1.0  0   error (recursion) 0 wit inspect 5.3 2.9 250 0   0   true -32 --- inspect 9.4 5.6 320 .62 0   timeout 0 --- inspect 98   68   4100 .082 0   true -32 --- inspect .66 .66 20 .090 0     - --- inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .59 .60 32 8.9 .85 0   timeout 0 wit inspect 95   68   2700 0   0   error (7) 0 --- inspect 20   11   310 .68 0   timeout 0 --- inspect 98   69   3700 .95  0   true -32 --- inspect .68 .68 20 .094 0     - --- inspect
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .47 .47 29 5.8 1.0  0   timeout 0 wit inspect 95   69   2600 0   0   error (7) 0 --- inspect 17   9.9 310 .68 0   timeout (exception) 0 --- inspect 92   69   3200 0     0   false(valid-deref) -16 --- inspect .68 .68 20 .086 0     - --- inspect
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .47 .47 29 6.0 1.0  0   timeout 0 --- inspect 97   82   2200 0   0   error (7) 0 --- inspect 16   9.1 310 .68 0   timeout 0 --- inspect 96   72   3300 0     0   false(valid-deref) -16 --- inspect .67 .67 20 .086 0     - --- inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900    900    450 12000   1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.7 0    0   
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .11 .11 26 1.4 .85 0   timeout 0 wit inspect 94   67   2800 0   0   true -32 --- inspect 8.6 5.2 310 .62 0   timeout (exception) 0 --- inspect 92   68   3500 0     0   false(valid-deref) -16 --- inspect .67 .67 20 .078 0     - --- inspect
list-properties/list_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .13 .13 26 2.4 .85 0   timeout 0 wit inspect 93   65   2500 0   0   true -32 --- inspect 8.2 4.6 310 .62 0   timeout (exception) 0 --- inspect 93   69   3100 0     0   false(valid-deref) -16 --- inspect .66 .65 20 .078 0     - --- inspect
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .15 .15 26 1.6 1.0  0   timeout 0 wit inspect 93   65   2900 0   0   true -32 --- inspect 10   5.7 310 .62 0   timeout 0 --- inspect 92   67   3200 0     0   true -32 --- inspect .65 .65 20 .074 0     - --- inspect
list-properties/simple_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .20 .20 26 2.7 1.0  0   timeout 0 wit inspect 95   65   2800 0   0   true -32 --- inspect 9.0 4.9 310 .66 0   timeout 0 --- inspect 93   68   3400 0     0   true -32 --- inspect .65 .65 20 .078 0     - --- inspect
list-properties/splice_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .10 .10 27 1.1 1.0  0   timeout 0 wit inspect 95   62   3000 0   0   true -32 --- inspect 8.5 4.7 300 .62 0   timeout 0 --- inspect 92   66   3300 0     0   true -32 --- inspect .70 .71 20 .082 0     - --- inspect
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i true 2 wit inspect .20 .20 39 3.1 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (7) 0 --- inspect 31     17     520   .75 0   
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i true 2 wit inspect .21 .21 39 2.0 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect error (7) 0 --- inspect 39     21     530   .75 0   
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i true 2 wit inspect .21 .21 39 2.2 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (7) 0 --- inspect 36     20     520   .75 0   
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 3.1  3.1  130 38   1.0  0   true -32 wit inspect 9.7 5.1 380 0   0   error (7) 0 --- inspect 33   19   520 .71 0   unknown 0 --- inspect 6.7 3.6 280 0     0   true -32 --- inspect 1.2  1.2  21 .73  0     - --- inspect
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 3.1  3.1  130 47   1.0  0   true -32 wit inspect 8.8 4.6 380 0   0   error (7) 0 --- inspect 33   19   540 .68 0   unknown 0 --- inspect 6.7 3.6 280 0     0   true -32 --- inspect 1.2  1.2  22 .73  .13  - --- inspect
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 3.1  3.1  130 40   .85 0   true -32 wit inspect 9.4 4.9 380 0   0   error (7) 0 --- inspect 34   19   520 .68 0   unknown 0 --- inspect 7.0 3.7 290 0     0   true -32 --- inspect 1.2  1.2  22 .73  0     - --- inspect
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 3.1  3.1  130 45   .85 0   true -32 wit inspect 9.9 5.2 380 0   0   error (7) 0 --- inspect 33   19   530 .68 0   unknown 0 --- inspect 6.5 3.5 280 0     0   true -32 --- inspect 1.2  1.2  22 .73  .13  - --- inspect
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 3.9  3.9  130 55   .85 0   true -32 wit inspect 9.8 5.2 380 0   0   error (7) 0 --- inspect 35   20   530 .68 0   unknown 0 --- inspect 6.7 3.6 280 0     0   true -32 --- inspect 1.2  1.2  22 .73  0     - --- inspect
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 3.1  3.1  130 42   1.0  0   true -32 wit inspect 8.4 4.4 380 0   0   error (7) 0 --- inspect 36   20   530 .47 0   unknown 0 --- inspect 6.3 3.4 280 0     0   true -32 --- inspect 1.2  1.2  22 .73  0     - --- inspect
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 3.0  3.0  130 40   1.0  0   true -32 wit inspect 11   5.6 380 0   0   error (7) 0 --- inspect 34   19   540 .68 0   unknown 0 --- inspect 7.1 3.8 300 0     0   true -32 --- inspect 1.2  1.2  22 .73  .086 - --- inspect
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 3.0  3.0  130 38   1.0  0   true -32 wit inspect 9.6 5.1 380 0   0   error (7) 0 --- inspect 34   19   550 .68 0   unknown 0 --- inspect 7.3 3.9 290 0     0   true -32 --- inspect 1.2  1.2  22 .73  0     - --- inspect
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 3.1  3.1  130 43   .85 0   true -32 wit inspect 10   5.3 380 0   0   error (7) 0 --- inspect 32   18   520 .71 0   unknown 0 --- inspect 6.6 3.5 290 0     0   true -32 --- inspect 1.2  1.2  22 .73  0     - --- inspect
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect 3.0  3.0  130 38   .85 0   true -32 wit inspect 9.3 4.9 380 0   0   error (7) 0 --- inspect 32   18   520 .68 0   unknown 0 --- inspect 6.9 3.7 280 0     0   true -32 --- inspect 1.2  1.2  22 .72  0     - --- inspect
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900    900    360 10000   .86 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0   
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900    900    2500 11000   .86 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0   
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900    900    420 11000   .86 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.6 0    0   
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900    900    520 12000   .86 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0    0   
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900    900    440 9700   1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .030 5.7 0    0   
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900    900    490 11000   1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .026 5.6 0    0   
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900    900    990 13000   .86 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .032 .033 5.7 0    0   
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900    900    710 12000   .86 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0   
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900    900    590 12000   1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0   
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900    900    360 11000   1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .026 5.6 0    0   
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900    900    200 12000   1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0   
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900    900    2400 12000   1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0    0   
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900    900    410 11000   .86 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0    0   
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900    900    450 12000   1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .025 5.7 0    0   
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900    900    410 11000   .86 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .030 5.7 0    0   
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900    900    400 12000   1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .029 5.6 0    0   
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900    900    870 9900   1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0   
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900    900    710 11000   1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .023 5.6 0    0   
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900    900    460 11000   .86 0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .026 5.5 0    0   
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .43 .43 30 5.1 .85 0   false(valid-deref) 1 wit inspect 4.9 2.7 250 0   0   error (7) 0 --- inspect 20   11   310 .71 0   timeout 0 --- inspect 98   76   3200 .93  0   true -32 --- inspect .69 .69 20 .086 0     - --- inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .17 .17 27 2.2 .85 0   false(valid-deref) 1 wit inspect 4.8 2.6 260 0   0   error (7) 0 --- inspect 18   10   310 .68 0   timeout (exception) 0 --- inspect 92   65   3700 0     0   error (2) 0 --- inspect .64 .64 20 .057 0     - --- inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .42 .42 30 5.5 1.0  0   false(valid-deref) 1 wit inspect 4.7 2.6 250 0   0   error (7) 0 --- inspect 17   9.6 310 .68 0   timeout 0 --- inspect 98   76   3200 .97  0   true -32 --- inspect .66 .66 20 .086 0     - --- inspect
list-simple/dll2c_append_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .22 .22 27 2.7 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     940   .64 0   
list-simple/dll2c_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .25 .25 27 3.5 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     980   .63 0   
list-simple/dll2c_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .22 .22 27 2.6 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     900   .64 0   
list-simple/dll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .25 .25 27 2.6 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     860   .65 0   
list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .22 .22 27 2.5 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     860   .71 0   
list-simple/dll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .25 .25 27 2.6 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     900   .63 0   
list-simple/dll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .17 .17 27 1.9 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     1100   .64 0   
list-simple/dll2c_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .17 .17 27 2.1 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     900     840   .68 0   
list-simple/dll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .20 .20 27 2.0 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 350     310     1000   .62 0   
list-simple/dll2c_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .17 .17 27 2.1 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 400     360     1000   .62 0   
list-simple/dll2n_append_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .42 .42 27 5.1 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout (error (7)) 0 --- inspect 940     900     2300   .68 0   
list-simple/dll2n_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .41 .41 28 4.9 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1300   .74 0   
list-simple/dll2n_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .40 .40 28 5.0 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     940     1200   .70 0   
list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .43 .43 28 6.0 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1600   1.5  0   
list-simple/dll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .37 .37 27 5.1 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1000   .69 0   
list-simple/dll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .38 .38 27 5.1 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     930   .72 0   
list-simple/dll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .15 .15 26 2.1 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     1200   .70 0   
list-simple/dll2n_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .16 .16 27 1.5 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 180     150     850   .62 0   
list-simple/dll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .17 .17 27 1.6 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     900     1500   .69 0   
list-simple/dll2n_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .16 .16 27 1.7 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     1400   .64 0   
list-simple/sll2c_append_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .22 .22 27 2.5 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1400   .63 0   
list-simple/sll2c_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .22 .22 27 3.6 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1400   .73 0   
list-simple/sll2c_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .21 .22 27 2.8 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1200   .63 0   
list-simple/sll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .25 .25 27 2.6 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1100   .65 0   
list-simple/sll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .22 .22 27 2.7 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     1300   1.7  0   
list-simple/sll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .24 .24 27 2.2 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1300   1.3  0   
list-simple/sll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .18 .18 27 2.4 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     890     760   .73 0   
list-simple/sll2c_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .17 .17 27 2.2 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 410     370     700   .62 0   
list-simple/sll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .17 .17 27 2.3 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     940   .71 0   
list-simple/sll2c_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .17 .17 27 2.0 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     900     900   .69 0   
list-simple/sll2n_append_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .38 .38 27 5.0 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     2200   .78 0   
list-simple/sll2n_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .40 .40 27 5.4 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     2000   2.1  0   
list-simple/sll2n_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .37 .37 27 5.2 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     930   .72 0   
list-simple/sll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .40 .40 27 5.9 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     940     1000   .74 0   
list-simple/sll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .36 .36 27 4.9 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     940     890   .80 .40
list-simple/sll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .39 .39 27 4.1 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     780   .74 0   
list-simple/sll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .15 .15 26 1.8 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     1000   .69 0   
list-simple/sll2n_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .15 .15 27 1.7 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 390     370     760   .62 0   
list-simple/sll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .14 .14 27 2.0 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 490     460     1100   .62 0   
list-simple/sll2n_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .14 .14 27 1.6 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 590     560     980   .62 0   
list-ext3-properties/dll_circular_traversal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .59 .59 27 7.2 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     2800   .65 0   
list-ext3-properties/dll_nondet_free_order_true-valid-memsafety.i true 2 wit inspect .24 .24 27 2.5 1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1900   .63 0   
list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .71 .71 27 11   1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     890     2100   .69 0   
list-ext3-properties/sll_circular_traversal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .61 .61 27 8.1 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     1300   1.4  0   
list-ext3-properties/sll_length_check_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 340    340    260 3800   1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     890     2300   .70 0   
list-ext3-properties/sll_nondet_insert_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 100    100    250 1300   1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     1100   1.3  0   
list-ext3-properties/sll_of_sll_nondet_append_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900    900    1300 9400   1.0  0   - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.6 0    0   
list-ext3-properties/sll_shallow_copy_true-valid-memsafety.i true 2 wit inspect .12 .13 26 1.3 .85 0   - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 18     11     530   .62 0   
list-ext3-properties/dll_circular_traversal_false-valid-deref.i false(valid-deref) 1 wit inspect .72 .72 27 11   .85 0   true -32 wit inspect 5.5 3.0 260 0   0   true -32 --- inspect 9.5 5.2 300 .62 0   unknown 0 --- inspect 4.4 2.5 260 0     0   false(valid-deref) 1 --- inspect .66 .65 20 .082 0     - --- inspect
list-ext3-properties/sll_circular_traversal_false-valid-deref.i false(valid-deref) 1 wit inspect .69 .69 27 9.4 1.0  0   true -32 wit inspect 5.0 2.7 250 0   0   true -32 --- inspect 8.9 5.3 310 .66 0   unknown 0 --- inspect 4.5 2.5 260 0     0   false(valid-deref) 1 --- inspect .65 .65 21 .082 0     - --- inspect
list-ext3-properties/dll_nondet_free_order_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .20 .20 27 2.0 1.0  0   true -32 wit inspect 4.9 2.7 260 0   0   true -32 --- inspect 8.3 5.2 310 .66 0   unknown 0 --- inspect 4.4 2.5 250 0     0   false(valid-deref) -16 --- inspect .66 .67 20 .086 0     - --- inspect
list-ext3-properties/sll_shallow_copy_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .10 .10 26 1.2 1.0  0   true -32 wit inspect 5.1 2.8 250 0   0   true -32 --- inspect 8.8 5.2 310 .62 0   unknown 0 --- inspect 4.1 2.4 250 0     0   true -32 --- inspect .64 .64 20 .070 .025 - --- 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 107 22000   22000   43000 270000 98   0   28 -443 900 620 28000 0   0   28 -320 570 320 11000 19   0   28 0 1400 1000 52000 2.9 0   28 -652 24   24   580 8.8  .37 75 16 40000 39000 59000 39   .40
    correct results 57 107 460   460   2000 5400 54   0   5 5 25 14 1300 0   0   0 0 4 4 2.6 2.6 82 .35 0    8 16 2800 2600 6900 5.0 0   
        correct true 50 100 450   450   1800 5400 47   0   0 0 0 0 8 16 2800 2600 6900 5.0 0   
        correct false 7 7 2.9 2.9 200 39 6.6 0   5 5 25 14 1300 0   0   0 0 4 4 2.6 2.6 82 .35 0    0
    correct-unconfimed results 21 0 34   34   1600 460 20   0   0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0
        correct-unconfirmed false 21 0 34   34   1600 460 20   0   0 0 0 0 0
    incorrect results 0 14 -448 120 61 4800 0   0   10 -320 89 52 3100 6.3 0   0 23 -656 21   21   480 8.4  .37 0
        incorrect true 0 14 -448 120 61 4800 0   0   10 -320 89 52 3100 6.3 0   0 18 -576 17   17   380 7.9  .37 0
        incorrect false 0 0 0 0 5 -80 3.3 3.4 100 .41 0    0
score (103 tasks, max score: 178) 107 -443 -320 0 -652 16
Run set esbmc-kind.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp19_prop-memsafety.MemSafety-LinkedLists