Tool symbiotic 6.0.3-77d4af47 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* [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-09 01:29:54 CET 2018-12-12 21:10:03 CET 2018-12-08 23:47:25 CET
Run set symbiotic.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-witness2test-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-LinkedLists
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 -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true -witness ../../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 (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 (verification) 0 --- inspect 900    900    1100 13000   .025 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.6 0    0     
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i timeout (verification) 0 --- inspect 900    900    5600 5800   .033 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0     
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i timeout (verification) 0 --- inspect 900    900    1800 12000   .025 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0    0     
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i timeout (verification) 0 --- inspect 900    900    4400 10000   .029 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .026 5.6 0    0     
heap-manipulation/tree_false-unreach-call_false-valid-deref.i error(unknown, verification-finished) 0 --- inspect .36 .36 18 4.5 0     0      error (invalid witness file) 0 --- inspect .61 .37 41 0   0     error (2) 0 --- inspect .023 .024 5.7 0    0   error (invalid witness file) 0 --- inspect .94 .62 48 0    0      error (invalid witness file) 0 --- inspect .0014 .0016 .39 0     0     - --- inspect
heap-manipulation/tree_false-valid-deref.i false(valid-deref) 1 wit inspect .26 .26 19 3.5 0     0      false(valid-deref) 1 wit inspect 5.7  3.1  250 0   0     error (7) 0 --- inspect 18     10     320   .68 0   timeout 0 --- inspect 92    69    3100 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 .29 .28 18 4.0 0     0      error (recursion) 0 wit inspect 6.6  3.6  250 0   0     true -32 --- inspect 9.9   5.6   320   .62 0   timeout 0 --- inspect 98    69    3700 1.0  0      true -32 --- inspect .67   .66   20    .090 0     - --- inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .27 .27 18 3.1 0     0      false(valid-memtrack) 1 wit inspect 5.1  2.8  260 0   0     error (7) 0 --- inspect 17     9.9   310   .68 0   timeout (exception) 0 --- inspect 92    65    3300 0    .029  true -32 --- inspect .67   .70   20    .094 0     - --- inspect
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .29 .28 19 3.7 0     0      false(valid-memtrack) 1 wit inspect 5.2  2.8  250 0   0     error (7) 0 --- inspect 17     10     310   .68 0   timeout 0 --- inspect 92    69    3300 0    0      false(valid-deref) -16 --- inspect .69   .69   20    .086 0     - --- inspect
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .36 .35 17 3.5 0     0      false(valid-memtrack) 1 wit inspect 5.1  2.8  260 0   0     error (7) 0 --- inspect 16     9.2   310   .68 0   timeout (exception) 0 --- inspect 92    69    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 (verification) 0 --- inspect 900    900    1800 10000   .029 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0    0     
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .26 .25 20 3.2 0     0      timeout 0 wit inspect 93    65    2800 0   0     true -32 --- inspect 9.1   5.6   330   .62 0   timeout 0 --- inspect 91    66    3400 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) 1 wit inspect .26 .26 18 3.1 0     0      false(valid-memtrack) 1 wit inspect 5.1  2.7  270 0   0     true -32 --- inspect 9.4   5.3   320   .62 0   timeout 0 --- inspect 92    68    3300 0    0      false(valid-deref) -16 --- inspect .66   .67   20    .078 0     - --- inspect
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 0 wit inspect .25 .24 18 2.9 0     0      timeout 0 wit inspect 93    65    2800 0   0     true -32 --- inspect 9.2   5.2   330   .62 0   timeout 0 --- inspect 95    70    3200 0    0      true -32 --- inspect .64   .64   20    .074 0     - --- inspect
list-properties/simple_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .26 .25 18 3.0 0     0      false(valid-memtrack) 1 wit inspect 5.1  2.7  260 0   0     true -32 --- inspect 8.8   5.3   320   .62 0   timeout 0 --- inspect 92    68    3100 0    0      true -32 --- inspect .80   .80   20    .078 0     - --- inspect
list-properties/splice_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .26 .25 18 2.7 0     0      false(valid-memtrack) 1 wit inspect 6.1  3.3  250 0   0     true -32 --- inspect 8.9   5.1   330   .62 0   timeout (exception) 0 --- inspect 92    68    3300 0    0      true -32 --- inspect .68   .68   20    .082 0     - --- inspect
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i true 2 wit inspect .70 .69 35 9.6 0     0      - --- inspect - --- inspect - --- inspect - --- inspect error (7) 0 --- inspect 32     18     520   .75 0     
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i true 2 wit inspect .72 .71 34 7.8 0     0      - --- inspect - --- inspect - --- inspect - --- inspect error (7) 0 --- inspect 37     20     530   .71 0     
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i true 2 wit inspect .77 .76 35 9.1 0     0      - --- inspect - --- inspect - --- inspect - --- inspect error (7) 0 --- inspect 30     18     520   .68 0     
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .91 .90 33 7.8 0     0      false(valid-memtrack) 1 wit inspect 8.8  4.6  390 0   0     error (7) 0 --- inspect 30     17     530   .68 0   unknown 0 --- inspect 8.0  4.4  350 0    0      true -32 --- inspect 1.2    1.2    22    .73  0     - --- inspect
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .92 .91 33 9.2 0     0      false(valid-memtrack) 1 wit inspect 10    5.4  410 0   .53  error (7) 0 --- inspect 31     17     520   .68 0   unknown 0 --- inspect 7.8  4.4  340 0    3.1    true -32 --- inspect 1.2    1.2    22    .73  0     - --- inspect
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .93 .91 33 9.3 0     0      false(valid-memtrack) 1 wit inspect 8.7  4.6  400 0   .13  error (7) 0 --- inspect 31     18     520   .68 0   unknown 0 --- inspect 7.7  4.3  340 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) 1 wit inspect .92 .91 33 9.8 0     0      false(valid-memtrack) 1 wit inspect 11    5.6  400 0   0     error (7) 0 --- inspect 31     18     520   .68 0   unknown 0 --- inspect 7.7  4.3  340 0    .0041 true -32 --- inspect 1.2    1.2    22    .73  0     - --- inspect
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .91 .90 33 9.6 0     0      false(valid-memtrack) 1 wit inspect 8.9  4.7  400 0   0     error (7) 0 --- inspect 31     18     520   .68 0   unknown 0 --- inspect 8.6  4.8  340 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) 1 wit inspect .86 .84 33 9.7 0     0      false(valid-memtrack) 1 wit inspect 11    5.6  390 0   0     error (7) 0 --- inspect 32     18     530   .68 0   unknown 0 --- inspect 7.8  4.4  350 0    .086  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) 1 wit inspect .86 .84 33 11   0     0      false(valid-memtrack) 1 wit inspect 8.2  4.3  390 0   0     error (7) 0 --- inspect 30     17     520   .68 0   unknown 0 --- inspect 7.7  4.3  340 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) 1 wit inspect .91 .89 33 9.8 0     0      false(valid-memtrack) 1 wit inspect 8.1  4.2  400 0   0     error (7) 0 --- inspect 32     18     520   .68 0   unknown 0 --- inspect 7.7  4.3  340 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) 1 wit inspect .87 .85 33 11   0     0      false(valid-memtrack) 1 wit inspect 9.8  5.1  400 0   0     error (7) 0 --- inspect 31     18     530   .68 0   unknown 0 --- inspect 7.8  4.3  340 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) 1 wit inspect .88 .87 33 9.8 0     0      false(valid-memtrack) 1 wit inspect 9.8  5.1  400 0   0     error (7) 0 --- inspect 32     18     520   .68 0   unknown 0 --- inspect 7.7  4.4  340 0    .11   true -32 --- inspect 1.2    1.2    22    .72  .086 - --- inspect
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i timeout (verification) 0 --- inspect 900    900    4400 6100   .029 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .023 5.6 0    0     
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i timeout (verification) 0 --- inspect 900    900    6200 9200   .033 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.7 0    0     
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i timeout (verification) 0 --- inspect 900    900    4800 8100   .033 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0     
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i error(unknown, verification-finished) 0 --- inspect 460    460    3200 3200   0     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 error(unknown, verification-finished) 0 --- inspect 550    550    4000 4000   0     0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.8 0    0     
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i error(unknown, verification-finished) 0 --- inspect 570    570    3900 3800   0     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 (verification) 0 --- inspect 900    900    4000 11000   .029 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0    0     
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i timeout (verification) 0 --- inspect 900    900    4800 5300   .033 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .024 5.5 0    0     
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i timeout (verification) 0 --- inspect 900    900    1400 9000   .029 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0     
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i timeout (verification) 0 --- inspect 900    900    4400 5800   .033 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.6 0    0     
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i timeout (verification) 0 --- inspect 900    900    3800 4900   .029 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0     
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i timeout (verification) 0 --- inspect 900    900    6100 7100   .033 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .024 5.6 0    0     
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i timeout (verification) 0 --- inspect 900    900    4600 5500   .029 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .029 5.6 0    0     
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i error(unknown, verification-finished) 0 --- inspect 480    480    3200 4000   0     0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.7 0    0     
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout (verification) 0 --- inspect 900    900    5000 6400   .033 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.6 0    0     
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout (verification) 0 --- inspect 900    900    4900 5600   .033 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .025 .026 5.6 0    0     
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i timeout (verification) 0 --- inspect 900    900    4200 10000   .029 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0     
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i timeout (verification) 0 --- inspect 900    900    4800 5400   .029 0      - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0     
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i timeout (verification) 0 --- inspect 900    900    1700 10000   .033 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 false(valid-deref) 1 wit inspect .28 .27 19 3.2 0     0      false(valid-deref) 1 wit inspect 6.4  3.4  280 0   0     error (7) 0 --- inspect 17     10     310   .68 0   timeout 0 --- inspect 93    71    3100 0    0      true -32 --- inspect .69   .68   20    .086 0     - --- inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .29 .30 22 3.8 0     5.2    false(valid-deref) 1 wit inspect 5.8  3.1  260 0   0     error (7) 0 --- inspect 18     11     310   .68 0   timeout (exception) 0 --- inspect 92    65    3600 0    .025  false(valid-deref) 1 --- inspect .67   .67   20    .094 0     - --- inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .31 .30 18 3.5 0     0      false(valid-deref) 1 wit inspect 7.1  3.8  270 0   .025 error (7) 0 --- inspect 16     9.5   310   .68 0   timeout 0 --- inspect 98    77    3200 .93 0      true -32 --- inspect .70   .70   20    .086 0     - --- inspect
list-simple/dll2c_append_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .22 .22 16 2.9 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     1000   .82 0     
list-simple/dll2c_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .21 .20 16 2.2 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     970   1.2  0     
list-simple/dll2c_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .22 .21 16 2.6 0     .0041 - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     920   .63 0     
list-simple/dll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .27 .26 17 2.3 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     740   1.4  0     
list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .21 .21 16 2.8 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     920   1.6  0     
list-simple/dll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .22 .22 17 2.5 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     970   1.4  0     
list-simple/dll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .23 .22 16 2.3 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1400   1.6  0     
list-simple/dll2c_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .20 .19 17 2.5 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     890     830   1.5  0     
list-simple/dll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .24 .23 15 2.9 0     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 330     300     1200   .62 0     
list-simple/dll2c_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .21 .20 16 2.3 0     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 340     310     900   .62 0     
list-simple/dll2n_append_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .22 .21 16 2.6 0     0      - --- inspect - --- inspect - --- inspect - --- inspect error (7) 0 --- inspect 820     780     2200   .68 0     
list-simple/dll2n_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .21 .20 16 2.5 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     1300   1.1  0     
list-simple/dll2n_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .21 .20 16 2.5 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1200   1.5  0     
list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .22 .22 16 3.1 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1300   .67 0     
list-simple/dll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .24 .23 16 2.6 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     910   .68 0     
list-simple/dll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .21 .20 16 2.5 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     840   .69 0     
list-simple/dll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .21 .20 17 2.2 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     1200   .70 16     
list-simple/dll2n_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .20 .20 17 2.4 0     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 190     160     990   .62 0     
list-simple/dll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .21 .20 16 2.7 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     900     1400   .72 0     
list-simple/dll2n_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .21 .21 17 2.4 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     1300   .66 0     
list-simple/sll2c_append_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .21 .21 16 2.5 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1400   1.7  0     
list-simple/sll2c_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .23 .22 16 2.8 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1400   .64 0     
list-simple/sll2c_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .21 .20 16 2.5 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1300   .66 0     
list-simple/sll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .22 .21 16 2.3 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     920     1100   .64 0     
list-simple/sll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .21 .21 16 2.6 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1600   .63 0     
list-simple/sll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .21 .20 16 2.7 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1300   .63 0     
list-simple/sll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .20 .19 16 2.4 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     890     740   .69 0     
list-simple/sll2c_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .20 .19 16 2.4 0     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 400     360     750   .52 0     
list-simple/sll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .21 .21 17 2.4 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     880   .82 0     
list-simple/sll2c_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .21 .21 17 2.7 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     910   .71 .045 
list-simple/sll2n_append_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .20 .20 17 2.4 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     2300   .73 0     
list-simple/sll2n_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .21 .20 16 2.5 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     940     1800   .74 0     
list-simple/sll2n_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .21 .21 17 2.5 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     980   .72 0     
list-simple/sll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .21 .21 16 2.6 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     980   .71 0     
list-simple/sll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .23 .22 16 2.0 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     860   .80 0     
list-simple/sll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .20 .20 16 2.4 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     940     830   .79 0     
list-simple/sll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .21 .21 16 2.2 0     .28   - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     920   1.6  .057 
list-simple/sll2n_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .20 .19 17 2.3 0     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 380     350     900   .62 0     
list-simple/sll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .23 .22 16 2.6 0     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 520     490     910   .62 0     
list-simple/sll2n_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .21 .20 16 2.4 0     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 640     600     940   .62 0     
list-ext3-properties/dll_circular_traversal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .20 .19 16 2.6 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1100   .63 0     
list-ext3-properties/dll_nondet_free_order_true-valid-memsafety.i true 2 wit inspect .25 .25 18 2.9 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     940     1900   .63 0     
list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .25 .24 16 2.3 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     890     2100   .70 .39  
list-ext3-properties/sll_circular_traversal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .20 .19 16 2.3 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     930     1300   1.5  0     
list-ext3-properties/sll_length_check_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .47 .46 18 5.7 0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     880     2500   .71 .045 
list-ext3-properties/sll_nondet_insert_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 1.8  1.7  44 23   0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     910     1000   .74 0     
list-ext3-properties/sll_of_sll_nondet_append_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 6.3  6.3  100 81   0     0      - --- inspect - --- inspect - --- inspect - --- inspect timeout 0 --- inspect 960     940     770   .71 .0082
list-ext3-properties/sll_shallow_copy_true-valid-memsafety.i true 2 wit inspect .18 .17 15 2.0 0     0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 19     12     520   .66 0     
list-ext3-properties/dll_circular_traversal_false-valid-deref.i false(valid-deref) 1 wit inspect .22 .22 17 2.7 0     0      false(valid-deref) 1 wit inspect 6.9  3.7  250 0   0     true -32 --- inspect 9.9   5.9   320   .62 0   unknown 0 --- inspect 6.0  3.3  270 0    .12   false(valid-deref) 1 --- inspect .65   .66   20    .082 0     - --- inspect
list-ext3-properties/sll_circular_traversal_false-valid-deref.i false(valid-deref) 1 wit inspect .23 .22 16 2.9 0     0      false(valid-deref) 1 wit inspect 5.6  3.0  250 0   0     true -32 --- inspect 9.3   5.2   320   .62 0   unknown 0 --- inspect 5.4  3.0  260 0    0      false(valid-deref) 1 --- inspect .67   .67   20    .082 0     - --- inspect
list-ext3-properties/dll_nondet_free_order_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .30 .29 17 3.0 0     0      false(valid-memtrack) 1 wit inspect 6.2  3.3  250 0   0     true -32 --- inspect 9.1   5.2   320   .62 0   unknown 0 --- inspect 5.3  3.0  260 0    0      false(valid-deref) -16 --- inspect .69   .69   20    .086 0     - --- inspect
list-ext3-properties/sll_shallow_copy_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .26 .25 16 2.3 0     0      false(valid-memtrack) 1 wit inspect 4.8  2.6  250 0   0     true -32 --- inspect 8.2   5.0   310   .62 0   unknown 0 --- inspect 4.9  2.8  270 0    0      true -32 --- inspect .64   .64   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 126 20000    20000    96000 180000 .60 5.5  28 24 370 230 13000 0   .68 28 -320 520 300 11000 18   0   28 0 1300 950 47000 1.9 3.4 28 -652 24   24   560 8.7  .17 75 16 41000 39000 58000 43   16  
    correct results 75 126 33    33    1600 390 0    5.5  24 24 170 92 7600 0   .68 0 0 4 4 2.6 2.7 81 .35 0    8 16 2800 2600 7100 4.9 0  
        correct true 51 102 20    20    1000 250 0    .28 0 0 0 0 8 16 2800 2600 7100 4.9 0  
        correct false 24 24 13    13    580 140 0    5.2  24 24 170 92 7600 0   .68 0 0 4 4 2.6 2.7 81 .35 0    0
    correct-unconfimed results 3 0 .80 .78 55 10 0    0    0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0
        correct-unconfirmed false 3 0 .80 .78 55 10 0    0    0 0 0 0 0
    incorrect results 0 0 10 -320 92 53 3200 6.2 0   0 23 -656 21   21   480 8.4  .17 0
        incorrect true 0 0 10 -320 92 53 3200 6.2 0   0 18 -576 18   18   380 7.9  .17 0
        incorrect false 0 0 0 0 5 -80 3.4 3.4 100 .41 0    0
score (103 tasks, max score: 178) 126 24 -320 0 -652 16
Run set symbiotic.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-witness2test-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-symbiotic.sv-comp19_prop-memsafety.MemSafety-LinkedLists