Tool ULTIMATE Automizer 0.1.23-635dfa2a 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-08 07:42:40 CET 2018-12-09 20:30:54 CET 2018-12-09 21:05:03 CET 2018-12-09 21:08:07 CET 2018-12-12 21:10:19 CET 2018-12-09 20:42:29 CET
Run set uautomizer.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-uautomizer.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-uautomizer.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-witness2test-validate-violation-witnesses-uautomizer.sv-comp19_prop-memsafety.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-uautomizer.sv-comp19_prop-memsafety.MemSafety-LinkedLists
Options --full-output -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/uautomizer.2018-12-08_0742.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/uautomizer.2018-12-08_0742.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/uautomizer.2018-12-08_0742.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/uautomizer.2018-12-08_0742.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/uautomizer.2018-12-08_0742.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   850   1200 11000 .63 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   860   1200 11000 .84 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 error (7) 0 --- inspect 850   750   2300 11000 .68 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .029 5.6 0    0  
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   870   1900 10000 .63 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .025 5.6 0    0  
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 350   310   1300 4500 .62 0     false(valid-deref) 1 wit inspect 4.8  2.6  260 0   0   error (7) 0 --- inspect 17     9.7   310   .71 .025 unknown 0 --- inspect 5.0  3.0  260 0   0   true -32 --- inspect .68   .67   21    .094 0     - --- inspect
heap-manipulation/tree_false-valid-deref.i false(valid-deref) 1 wit inspect 8.8 3.1 340 70 .66 .012 false(valid-deref) 1 wit inspect 4.3  2.4  250 0   0   error (7) 0 --- inspect 18     9.9   310   .68 0     unknown 0 --- inspect 4.9  3.0  250 0   3.3 false(valid-deref) 1 --- inspect .71   .71   20    .094 .025 - --- inspect
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i timeout 0 --- inspect 900   820   1600 11000 .70 0     error (invalid witness file) 0 --- inspect .59 .38 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0     error (invalid witness file) 0 --- inspect 1.1  .71 47 0   0   error (invalid witness file) 0 --- inspect .0017 .0022 .53 0     0     - --- inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i unknown 0 --- inspect 67   37   790 680 .75 .066 error (invalid witness file) 0 --- inspect .75 .46 40 0   0   error (2) 0 --- inspect .022 .024 5.6 0    0     error (invalid witness file) 0 --- inspect 1.1  .71 47 0   0   error (invalid witness file) 0 --- inspect .0044 .0053 .53 0     0     - --- inspect
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i timeout 0 --- inspect 900   850   2000 9200 .72 0     error (invalid witness file) 0 --- inspect .70 .43 40 0   0   error (2) 0 --- inspect .022 .024 5.6 0    0     error (invalid witness file) 0 --- inspect .93 .61 47 0   0   error (invalid witness file) 0 --- inspect .0057 .0079 .53 0     0     - --- inspect
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i timeout 0 --- inspect 900   850   1200 12000 .74 0     error (invalid witness file) 0 --- inspect .76 .47 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0     error (invalid witness file) 0 --- inspect .95 .63 47 0   0   error (invalid witness file) 0 --- inspect .0046 .0056 .41 0     0     - --- inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   800   1100 8700 .64 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.6 0    0  
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i unknown 0 --- inspect 19   6.4 390 150 .75 0     error (invalid witness file) 0 --- inspect .79 .49 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0     error (invalid witness file) 0 --- inspect 1.0  .66 48 0   0   error (invalid witness file) 0 --- inspect .0039 .0049 .53 0     0     - --- inspect
list-properties/list_true-unreach-call_false-valid-memtrack.i unknown 0 --- inspect 26   10   590 250 .75 0     error (invalid witness file) 0 --- inspect .65 .41 40 0   0   error (2) 0 --- inspect .022 .025 5.6 0    0     error (invalid witness file) 0 --- inspect .95 .61 47 0   0   error (invalid witness file) 0 --- inspect .0017 .0021 .53 0     0     - --- inspect
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i unknown 0 --- inspect 19   6.8 400 150 .75 0     error (invalid witness file) 0 --- inspect .91 .56 42 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0     error (invalid witness file) 0 --- inspect 1.1  .69 47 0   0   error (invalid witness file) 0 --- inspect .0059 .0093 .53 0     0     - --- inspect
list-properties/simple_true-unreach-call_false-valid-memtrack.i unknown 0 --- inspect 23   8.7 530 210 .75 0     error (invalid witness file) 0 --- inspect .90 .55 42 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0     error (invalid witness file) 0 --- inspect .92 .58 47 0   0   error (invalid witness file) 0 --- inspect .0014 .0018 .53 0     0     - --- inspect
list-properties/splice_true-unreach-call_false-valid-memtrack.i unknown 0 --- inspect 20   7.4 400 150 .75 0     error (invalid witness file) 0 --- inspect .60 .37 42 0   0   error (2) 0 --- inspect .052 .053 5.5 0    0     error (invalid witness file) 0 --- inspect .97 .65 47 0   0   error (invalid witness file) 0 --- inspect .0016 .0021 .53 0     0     - --- inspect
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i error (7) 0 --- inspect 31   9.6 600 290 .75 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 (7) 0 --- inspect 34   10   590 260 .75 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .026 5.6 0    0  
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i error (7) 0 --- inspect 32   10   590 240 .75 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 (7) 0 --- inspect 34   10   590 250 .75 0     error (invalid witness file) 0 --- inspect .61 .39 40 0   0   error (2) 0 --- inspect .021 .023 5.6 0    0     error (invalid witness file) 0 --- inspect .96 .63 47 0   0   error (invalid witness file) 0 --- inspect .0049 .0059 .39 0     0     - --- inspect
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i error (7) 0 --- inspect 32   9.3 590 240 .75 0     error (invalid witness file) 0 --- inspect .63 .39 42 0   0   error (2) 0 --- inspect .032 .033 5.5 0    0     error (invalid witness file) 0 --- inspect 1.1  .74 47 0   0   error (invalid witness file) 0 --- inspect .0021 .0029 .53 0     0     - --- inspect
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i error (7) 0 --- inspect 32   9.9 570 250 .75 0     error (invalid witness file) 0 --- inspect .76 .47 40 0   0   error (2) 0 --- inspect .024 .024 5.6 0    0     error (invalid witness file) 0 --- inspect .96 .61 48 0   0   error (invalid witness file) 0 --- inspect .0045 .0074 .53 0     0     - --- inspect
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i error (7) 0 --- inspect 31   9.3 570 290 .75 .098 error (invalid witness file) 0 --- inspect .78 .48 41 0   0   error (2) 0 --- inspect .022 .024 5.7 0    0     error (invalid witness file) 0 --- inspect 1.0  .65 49 0   0   error (invalid witness file) 0 --- inspect .0039 .0053 .53 0     0     - --- inspect
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i error (7) 0 --- inspect 32   9.9 590 270 .75 0     error (invalid witness file) 0 --- inspect .74 .46 42 0   0   error (2) 0 --- inspect .022 .024 5.7 0    0     error (invalid witness file) 0 --- inspect .96 .62 47 0   0   error (invalid witness file) 0 --- inspect .0045 .0058 .52 0     0     - --- inspect
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i error (7) 0 --- inspect 31   9.9 590 240 .75 0     error (invalid witness file) 0 --- inspect .61 .37 42 0   0   error (2) 0 --- inspect .021 .029 5.7 0    0     error (invalid witness file) 0 --- inspect 1.0  .67 46 0   0   error (invalid witness file) 0 --- inspect .0016 .0019 .40 0     0     - --- inspect
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i error (7) 0 --- inspect 31   9.5 560 260 .75 0     error (invalid witness file) 0 --- inspect .74 .46 41 0   0   error (2) 0 --- inspect .024 .025 5.6 0    0     error (invalid witness file) 0 --- inspect .98 .62 48 0   0   error (invalid witness file) 0 --- inspect .0054 .0069 .53 0     0     - --- inspect
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i error (7) 0 --- inspect 32   9.3 590 240 .75 0     error (invalid witness file) 0 --- inspect .69 .42 40 0   0   error (2) 0 --- inspect .022 .024 5.6 0    0     error (invalid witness file) 0 --- inspect .92 .61 47 0   0   error (invalid witness file) 0 --- inspect .0055 .0072 .41 0     0     - --- inspect
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i error (7) 0 --- inspect 33   10   570 260 .75 0     error (invalid witness file) 0 --- inspect .69 .43 40 0   0   error (2) 0 --- inspect .038 .041 5.5 0    0     error (invalid witness file) 0 --- inspect 1.0  .64 48 0   0   error (invalid witness file) 0 --- inspect .0051 .0065 .54 0     0     - --- inspect
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i error (7) 0 --- inspect 32   9.5 590 260 .75 0     error (invalid witness file) 0 --- inspect .63 .39 42 0   0   error (2) 0 --- inspect .054 .056 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .76 47 0   0   error (invalid witness file) 0 --- inspect .0063 .0088 .53 0     0     - --- inspect
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   820   1700 11000 .63 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0    0  
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   830   1300 12000 .64 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   800   2300 10000 .69 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.7 0    0  
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   810   970 10000 .63 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   790   2100 12000 .70 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0  
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   800   2400 9800 .69 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .022 5.8 0    0  
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   750   960 7600 .65 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0    0  
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   790   2100 7300 .70 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .021 5.7 0    0  
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   850   1400 12000 .64 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 0 --- inspect 900   830   1800 11000 .64 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0  
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   820   2200 9700 .63 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .026 5.8 0    0  
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   780   890 11000 .63 .037 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   800   2300 9900 .70 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   800   1100 10000 .63 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .029 5.6 0    0  
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   790   1100 11000 .63 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0  
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   810   2200 9600 .70 .020 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.6 0    0  
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   780   2200 9400 .70 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 0 --- inspect 900   760   2400 8700 .70 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   820   2300 13000 .70 .070 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 80   48   780 660 .62 0     false(valid-deref) 1 wit inspect 6.8  3.8  250 0   0   error (7) 0 --- inspect 17     10     310   .68 0     unknown 0 --- inspect 5.3  3.1  280 0   0   true -32 --- inspect .68   .68   20    .086 0     - --- inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 30   12   810 280 .66 0     false(valid-deref) 1 wit inspect 5.6  3.0  260 0   0   error (7) 0 --- inspect 18     11     310   .71 0     timeout 0 --- inspect 92    58    3300 0   0   false(valid-deref) 1 --- inspect .68   .68   21    .094 .025 - --- inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 54   29   920 500 .66 0     false(valid-deref) 1 wit inspect 5.6  3.0  260 0   0   error (7) 0 --- inspect 16     10     310   .68 .025 unknown 0 --- inspect 5.1  2.9  280 0   0   true -32 --- inspect .68   .68   21    .086 0     - --- inspect
list-simple/dll2c_append_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   860   960 14000 .64 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
list-simple/dll2c_append_unequal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   860   1100 11000 .63 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.6 0    0  
list-simple/dll2c_insert_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   870   1100 12000 .64 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0    0  
list-simple/dll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   870   870 13000 .64 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.7 0    0  
list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   850   930 13000 .69 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
list-simple/dll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   870   960 10000 .63 .012 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .029 5.7 0    0  
list-simple/dll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   860   1300 11000 .64 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0    0  
list-simple/dll2c_remove_all_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   830   1300 13000 .69 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
list-simple/dll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 300   260   1200 3600 .62 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 310     280     1100   .62 0  
list-simple/dll2c_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 320   280   1100 4400 .62 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 360     320     940   .62 0  
list-simple/dll2n_append_equal_true-unreach-call_true-valid-memsafety.i error (7) 0 --- inspect 720   690   2300 9300 .68 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0  
list-simple/dll2n_append_unequal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   870   1100 12000 .69 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0  
list-simple/dll2n_insert_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   880   1200 10000 .64 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   870   2400 10000 .63 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.6 0    0  
list-simple/dll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   870   1300 13000 .71 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .022 5.7 0    0  
list-simple/dll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   870   860 13000 .69 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
list-simple/dll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   860   1100 13000 .69 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
list-simple/dll2n_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 150   120   890 1900 .62 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 160     130     840   .62 0  
list-simple/dll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   850   2400 13000 .63 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .024 5.6 0    0  
list-simple/dll2n_update_all_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   850   1600 11000 .63 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .032 .034 5.5 0    0  
list-simple/sll2c_append_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   870   1200 13000 .64 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
list-simple/sll2c_append_unequal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   870   1900 12000 .64 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.8 0    0  
list-simple/sll2c_insert_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   860   1300 13000 .64 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .028 .029 5.5 0    0  
list-simple/sll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   860   1300 13000 .64 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.7 0    0  
list-simple/sll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   860   1800 12000 .64 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
list-simple/sll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   870   1700 9100 .64 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .023 5.6 0    0  
list-simple/sll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   830   750 11000 .70 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .026 5.6 0    0  
list-simple/sll2c_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 380   330   820 4000 .62 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 390     350     700   .62 0  
list-simple/sll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   850   910 11000 .70 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
list-simple/sll2c_update_all_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   840   990 12000 .70 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.7 0    0  
list-simple/sll2n_append_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   870   2200 11000 .72 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .023 .024 5.6 0    0  
list-simple/sll2n_append_unequal_true-unreach-call_true-valid-memsafety.i error (7) 0 --- inspect 840   810   2200 11000 .71 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .045 .046 5.6 0    0  
list-simple/sll2n_insert_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   880   920 11000 .72 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .024 .025 5.6 0    0  
list-simple/sll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   870   1100 10000 .73 .72  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .020 5.6 0    0  
list-simple/sll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   870   1200 11000 .72 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .024 5.6 0    0  
list-simple/sll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   870   1200 11000 .73 .41  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0  
list-simple/sll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   850   1100 10000 .70 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .020 .022 5.6 0    0  
list-simple/sll2n_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 320   290   800 4000 .62 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 350     320     910   .62 0  
list-simple/sll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 470   430   1100 5400 .62 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 500     470     1100   .62 0  
list-simple/sll2n_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 590   550   920 8200 .62 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 640     600     1000   .62 0  
list-ext3-properties/dll_circular_traversal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   850   2400 9200 .63 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .022 .023 5.6 0    0  
list-ext3-properties/dll_nondet_free_order_true-valid-memsafety.i timeout 0 --- inspect 900   870   1900 6300 .63 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   820   2000 13000 .69 .41  - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .023 5.6 0    0  
list-ext3-properties/sll_circular_traversal_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   860   1100 12000 .64 .025 - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .027 .028 5.6 0    0  
list-ext3-properties/sll_length_check_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   820   2500 9700 .70 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .026 .027 5.6 0    0  
list-ext3-properties/sll_nondet_insert_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   850   1300 13000 .64 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .022 5.6 0    0  
list-ext3-properties/sll_of_sll_nondet_append_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   870   800 12000 .63 0     - --- inspect - --- inspect - --- inspect - --- inspect error (2) 0 --- inspect .021 .021 5.6 0    0  
list-ext3-properties/sll_shallow_copy_true-valid-memsafety.i true 2 wit inspect 15   6.4 560 130 .66 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 --- inspect 19     12     500   .66 0  
list-ext3-properties/dll_circular_traversal_false-valid-deref.i timeout 0 --- inspect 900   820   2400 10000 .63 0     error (invalid witness file) 0 --- inspect .60 .37 40 0   0   error (2) 0 --- inspect .020 .029 5.6 0    0     error (invalid witness file) 0 --- inspect .96 .61 47 0   0   error (invalid witness file) 0 --- inspect .0058 .0068 .53 0     0     - --- inspect
list-ext3-properties/sll_circular_traversal_false-valid-deref.i timeout 0 --- inspect 900   860   850 12000 .63 0     error (invalid witness file) 0 --- inspect .79 .48 40 0   0   error (2) 0 --- inspect .020 .020 5.6 0    0     error (invalid witness file) 0 --- inspect 1.2  .76 47 0   0   error (invalid witness file) 0 --- inspect .0060 .0076 .52 0     0     - --- inspect
list-ext3-properties/dll_nondet_free_order_false-valid-memtrack.i unknown 0 --- inspect 260   220   990 2900 .68 15     error (invalid witness file) 0 --- inspect .64 .40 41 0   0   error (2) 0 --- inspect .020 .021 5.6 0    0     error (invalid witness file) 0 --- inspect 1.0  .68 47 0   0   error (invalid witness file) 0 --- inspect .0014 .0017 .40 0     0     - --- inspect
list-ext3-properties/sll_shallow_copy_false-valid-memtrack.i unknown 0 --- inspect 35   21   510 370 .75 0     error (invalid witness file) 0 --- inspect .60 .37 41 0   0   error (2) 0 --- inspect .024 .025 5.6 0    0     error (invalid witness file) 0 --- inspect .97 .63 48 0   0   error (invalid witness file) 0 --- inspect .0025 .0038 .52 0     0     - --- inspect
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (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 21 66000 61000 130000 800000 70   17     28 5 43 25 2200 0   0   28 0 87 51 1700 3.5 .049 28 0 140 85 5500 0   3.3 28 -94 3.5 3.5 110 .45 .049 75 16 2700 2500 7500 5.0 0  
    correct results 13 21 3100 2700 12000 37000 8.2 .012 5 5 27 15 1300 0   0   0 0 2 2 1.4 1.4 41 .19 .049 8 16 2700 2500 7100 5.0 0  
        correct true 8 16 2500 2300 7400 32000 5.0 0     0 0 0 0 8 16 2700 2500 7100 5.0 0  
        correct false 5 5 520 410 4100 6000 3.2 .012 5 5 27 15 1300 0   0   0 0 2 2 1.4 1.4 41 .19 .049 0
    incorrect results 0 0 0 0 3 -96 2.0 2.0 62 .27 0     0
        incorrect true 0 0 0 0 3 -96 2.0 2.0 62 .27 0     0
        incorrect false 0 0 0 0 0 0
score (103 tasks, max score: 178) 21 5 0 0 -94 16
Run set uautomizer.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-seq-validate-violation-witnesses-uautomizer.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-violation-witnesses-uautomizer.sv-comp19_prop-memsafety.MemSafety-LinkedLists cpa-witness2test-validate-violation-witnesses-uautomizer.sv-comp19_prop-memsafety.MemSafety-LinkedLists fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp19_prop-memsafety.MemSafety-LinkedLists uautomizer-validate-correctness-witnesses-uautomizer.sv-comp19_prop-memsafety.MemSafety-LinkedLists