Tool CBMC CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 CPAchecker 1.7-svn 29852 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-04 22:48:40 CET 2018-12-06 08:59:15 CET 2018-12-06 10:10:50 CET 2018-12-06 10:22:39 CET 2018-12-12 19:29:48 CET 2018-12-06 07:35:27 CET 2018-12-06 09:23:57 CET
Run set cbmc.sv-comp19_prop-reachsafety.ReachSafety-Heap cpa-seq-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Heap uautomizer-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Heap uautomizer-validate-correctness-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Heap
Options --graphml-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/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc.2018-12-04_2248.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/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc.2018-12-04_2248.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) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
heap-manipulation/bubble_sort_linux_false-unreach-call_false-valid-memcleanup.i 1 .21  .20  16   2.3  .012  0     1 6.2 3.4 270 0   0     0 20   12   340 .75 0   0 5.9 3.4 260 0   4.5   1 .68 .67 21 .11  0      - -
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i 0 .23  .22  13   3.1  .012  0     -32 7.0 3.8 270 0   0     0 22   13   330 .71 0   0 7.0 3.9 290 0   0     -32 .66 .66 21 .094 0      - -
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i 1 .25  .24  20   3.5  .012  0     1 6.2 3.4 260 0   0     0 17   9.5 310 .75 0   0 4.5 2.6 250 0   0     1 .63 .63 20 .082 0      - -
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i 1 .19  .18  13   2.3  .012  0     1 7.5 4.4 280 0   0     0 17   9.5 310 .75 0   0 4.9 2.8 260 0   0     1 .64 .64 21 .082 0      - -
heap-manipulation/tree_false-unreach-call_false-valid-deref.i 1 .17  .16  12   1.9  .012  0     1 6.2 3.4 260 0   0     0 16   9.9 310 .75 0   0 4.4 2.6 250 0   0     1 .63 .63 21 .074 0      - -
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i 1 .17  .16  12   2.3  .012  0     1 5.1 2.8 260 0   0     0 15   8.8 320 .75 0   0 4.5 2.5 250 0   .20  1 .63 .63 21 .074 0      - -
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i 0 880     880     3500   7600    .73   0     - - - - 0 .62 .38 41 0   0     0 .021 .021 5.6 0    0  
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i 0 880     880     490   9300    1.5    0     - - - - 0 .60 .37 40 0   0     0 .022 .024 5.6 0    0  
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i 0 880     880     1300   6700    .95   0     - - - - 0 .74 .46 41 0   0     0 .022 .023 5.6 0    0  
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i 0 180     180     13000   2100    3.9    0     - - - - 0 .74 .45 40 0   0     0 .028 .029 5.6 0    0  
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i 0 880     880     4300   14000    1.1    0     - - - - 0 .75 .45 41 0   0     0 .021 .022 5.6 0    0  
heap-manipulation/tree_true-unreach-call.i 0 880     880     1400   10000    6.8    0     - - - - 0 .67 .42 40 0   0     0 .024 .025 5.6 0    0  
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i 1 .097 .088 9.4 .89 .012  0     1 5.4 3.0 250 0   0     1 8.3 4.7 310 .62 0   0 4.4 2.5 270 0   0     1 .65 .65 20 .066 0      - -
list-properties/list_false-unreach-call_false-valid-memcleanup.i 1 .17  .16  9.5 1.0  .012  0     1 4.9 2.7 260 0   0     1 11   6.3 320 .66 0   0 4.4 2.5 250 0   .20  1 .64 .64 20 .066 0      - -
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i 1 .083 .073 9.9 .96 .012  0     1 4.5 2.4 260 0   0     1 8.4 4.9 310 .66 0   0 4.1 2.4 250 0   0     1 .62 .62 20 .066 0      - -
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i 1 .20  .19  9.9 1.5  .053  0     1 5.3 2.9 260 0   0     0 93   83   560 .62 0   0 4.5 2.6 250 0   0     1 .62 .62 21 .070 0      - -
list-properties/simple_false-unreach-call_false-valid-memcleanup.i 1 .083 .076 9.9 .82 .012  0     1 5.3 2.9 270 0   0     1 9.7 5.3 310 .66 0   0 4.1 2.4 250 0   0     1 .62 .62 20 .066 0      - -
list-properties/splice_false-unreach-call_false-valid-memcleanup.i 1 .099 .089 9.7 .88 .012  0     1 5.6 3.1 260 0   0     1 8.7 5.2 310 .66 0   0 4.2 2.5 250 0   0     0 .62 .62 21 .049 0      - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i 0 880     880     4000   8900    12      0     - - - - 0 .62 .38 40 0   0     0 .025 .025 5.6 0    0  
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i 0 830     830     13000   10000    10      0     - - - - 0 .75 .46 41 0   0     0 .020 .021 5.7 0    0  
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i 2 .17  .16  7.7 2.1  .070  0     - - - - 2 21    12    630 0   0     2 560     520     1400   .68 0  
list-properties/list_true-unreach-call_false-valid-memtrack.i 0 880     880     6400   13000    .95   0     - - - - 0 .69 .41 41 0   0     0 .027 .028 5.6 0    0  
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i 0 880     880     3900   9600    55      0     - - - - 0 .73 .45 41 0   0     0 .023 .023 5.6 0    0  
list-properties/simple_true-unreach-call_false-valid-memtrack.i 0 880     880     3300   11000    5.7    0     - - - - 0 .74 .45 41 0   0     0 .026 .027 5.6 0    0  
list-properties/splice_true-unreach-call_false-valid-memtrack.i 0 880     880     1700   14000    1.4    0     - - - - 0 .61 .38 41 0   0     0 .028 .029 5.6 0    0  
ldv-regression/1_3_true-termination.c_false-unreach-call.i 1 .076 .067 9.8 .56 .012  0     1 5.0 2.7 250 0   0     1 8.6 4.8 310 .12 0   1 3.6 2.1 250 0   .033 1 .58 .58 20 .057 0      - -
ldv-regression/alt_test_true-termination.c_false-unreach-call.i 1 .090 .082 9.2 .86 .012  0     1 4.7 2.6 260 0   0     1 11   6.2 340 .66 0   0 4.4 2.5 260 0   .11  1 .64 .64 20 .086 0      - -
ldv-regression/callfpointer_true-termination.c_false-unreach-call.i 1 .057 .048 9.3 .48 .0082 0     1 4.7 2.6 250 0   0     1 7.3 4.0 310 .66 0   1 3.6 2.0 250 0   0     1 .56 .56 20 .045 0      - -
ldv-regression/fo_test_true-termination.c_false-unreach-call.i 1 .13  .12  9.6 .91 .012  0     0 4.5 2.5 260 0   0     0 16   9.5 330 .71 0   0 4.1 2.4 250 0   .094 1 .66 .66 20 .074 0      - -
ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i 1 .10  .090 9.5 .35 .0082 0     -32 3.8 2.1 250 0   0     1 7.4 4.2 320 .66 0   1 3.7 2.2 250 0   0     1 .58 .58 20 .049 0      - -
ldv-regression/mutex_lock_struct_true-termination.c_false-unreach-call.i 1 .059 .049 9.8 .50 .0082 0     1 4.8 2.7 250 0   0     1 7.0 4.0 310 .62 0   1 3.7 2.2 250 0   0     1 .56 .56 20 .045 0      - -
ldv-regression/recursive_list_true-termination.c_false-unreach-call.i 1 .086 .074 9.5 .56 .012  0     1 5.0 2.7 260 0   0     1 7.7 4.6 310 .66 0   1 4.0 2.3 240 0   0     0 .58 .58 20 .037 0      - -
ldv-regression/rule57_ebda_blast_true-termination.c_false-unreach-call.i 1 .078 .070 9.8 .65 .012  0     1 4.2 2.3 250 0   0     1 8.3 5.2 310 .62 0   0 4.1 2.4 250 0   .23  1 .60 .61 20 .070 0      - -
ldv-regression/rule60_list2_true-termination.c_false-unreach-call_1.i 1 .079 .068 8.5 .63 .0082 0     -32 8.2 4.4 270 0   0     1 15   9.2 470 .62 0   0 4.4 2.5 250 0   .13  0 .64 .64 20 .049 0      - -
ldv-regression/stateful_check_false-unreach-call_false-termination.i 1 .15  .14  9.4 1.1  .037  0     1 8.2 4.4 280 0   0     1 8.6 4.7 310 .66 0   0 4.7 2.7 250 0   0     1 .59 .59 20 .057 0      - -
ldv-regression/test_while_int_true-termination.c_false-unreach-call.i 1 .086 .074 9.5 .58 .020  0     1 3.7 2.1 250 0   0     1 6.2 3.6 290 .66 0   1 3.9 2.2 250 0   0     1 .59 .59 20 .045 .012  - -
ldv-regression/test_while_int_true-termination.c_false-unreach-call_1.i 1 .074 .064 10   .51 .016  0     1 4.7 2.6 250 0   0     1 9.0 5.1 310 .66 0   1 3.5 2.1 250 0   0     1 .57 .57 20 .045 0      - -
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call.i 2 .053 .050 6.9 .34 .0082 0     - - - - 2 3.5  2.0  250 0   0     2 9.2   5.1   310   .66 0  
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i 2 .049 .045 7.5 .29 .0082 0     - - - - 2 3.6  2.0  250 0   0     2 8.7   5.1   310   .62 0  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call.i 2 .043 .041 6.6 .38 .0082 0     - - - - 2 3.8  2.1  250 0   0     2 8.6   5.2   300   .62 0  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call_1.i 2 .065 .061 6.0 .35 .0082 0     - - - - 2 4.5  2.5  250 0   0     2 9.3   5.2   300   .66 0  
ldv-regression/ex3_forlist_true-termination.c_true-unreach-call.i 2 .11  .11  6.2 .50 .033  0     - - - - 0 3.9  2.2  250 0   0     2 100     83     840   .62 0  
ldv-regression/just_assert_true-termination.c_true-unreach-call.i 2 .052 .050 7.1 .29 .0082 0     - - - - 2 4.0  2.3  250 0   0     2 7.8   4.3   300   .66 0  
ldv-regression/mutex_lock_int_true-termination.c_true-unreach-call_1.i 2 .078 .073 6.2 .26 .0082 0     - - - - 2 3.4  2.0  250 0   0     2 11     6.1   310   .66 0  
ldv-regression/mutex_lock_struct_true-termination.c_true-unreach-call_1.i 2 .049 .045 6.4 .37 .0082 0     - - - - 2 3.9  2.1  250 0   0     2 8.3   5.2   310   .66 0  
ldv-regression/nested_structure_noptr_true-termination.c_true-unreach-call.i 2 .047 .044 6.5 .36 .0082 0     - - - - 2 4.4  2.4  250 0   0     2 8.4   5.0   310   .66 0  
ldv-regression/nested_structure_noptr_true-unreach-call_true-termination.i 2 .044 .041 6.6 .31 .0082 0     - - - - 2 3.8  2.1  250 0   0     2 8.6   4.9   310   .66 0  
ldv-regression/nested_structure_ptr_true-termination.c_true-unreach-call.i 2 .076 .069 6.7 .25 .0082 0     - - - - 2 4.1  2.3  250 0   0     2 8.1   4.5   300   .62 0  
ldv-regression/nested_structure_ptr_true-unreach-call_true-termination.i 2 .043 .041 7.7 .37 .0082 0     - - - - 2 4.3  2.5  250 0   0     2 9.5   5.7   310   .66 0  
ldv-regression/nested_structure_true-termination.c_true-unreach-call.i 2 .049 .047 6.3 .67 .0082 0     - - - - 2 4.0  2.2  250 0   0     2 7.2   4.1   310   .66 0  
ldv-regression/nested_structure_true-unreach-call_true-termination.i 2 .048 .046 7.0 .32 .0082 0     - - - - 2 4.2  2.3  250 0   0     2 9.2   5.2   310   .66 0  
ldv-regression/oomInt_true-termination.c_true-unreach-call.i 2 .040 .037 7.3 .16 .0082 0     - - - - 2 4.4  2.4  250 0   0     2 7.7   4.4   310   .66 0  
ldv-regression/oomInt_true-termination.c_true-unreach-call_1.i 2 .043 .040 6.6 .40 .0082 0     - - - - 2 4.3  2.4  250 0   0     2 8.5   4.8   310   .66 0  
ldv-regression/rule57_ebda_blast_true-termination.c_true-unreach-call_1.i 2 .074 .071 7.5 .61 .016  0     - - - - 2 4.4  2.4  260 0   0     2 11     6.2   330   .66 0  
ldv-regression/rule60_list2_true-termination.c_true-unreach-call.i 2 .056 .054 6.4 .50 .0082 0     - - - - 2 4.3  2.4  260 0   0     2 27     17     680   .66 0  
ldv-regression/rule60_list_true-termination.c_true-unreach-call.i 2 .11  .10  7.0 .62 .016  0     - - - - 2 4.7  2.6  260 0   0     2 15     8.6   390   .66 0  
ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i 2 .053 .051 6.9 .57 .0082 0     - - - - 2 4.0  2.2  250 0   0     2 9.5   5.3   310   .66 0  
ldv-regression/structure_assignment_true-termination.c_true-unreach-call.i 2 .044 .042 6.4 .39 .0082 0     - - - - 2 3.9  2.2  250 0   0     2 8.6   5.1   310   .62 0  
ldv-regression/test_address_true-termination.c_true-unreach-call.i 2 .069 .065 6.4 .31 .0082 0     - - - - 2 5.1  2.8  250 0   0     2 10     5.9   320   .66 0  
ldv-regression/test_cut_trace_true-termination.c_true-unreach-call.i 2 .051 .048 7.2 .32 .0082 0     - - - - 2 4.1  2.3  250 0   0     2 8.1   4.8   300   .66 0  
ldv-regression/test_malloc-1_true-unreach-call_true-termination.i 2 .12  .11  6.7 .42 .016  0     - - - - 2 4.2  2.3  250 0   0     2 10     6.0   310   .66 0  
ldv-regression/test_malloc-2_true-unreach-call_true-termination.i 2 .075 .069 6.5 .34 .0082 0     - - - - 2 4.0  2.2  250 0   0     2 11     6.1   310   .66 0  
ldv-regression/test_overflow_true-termination.c_true-unreach-call.i 2 .058 .055 7.6 .56 .0082 0     - - - - 2 5.4  3.0  260 0   0     2 12     6.7   330   .66 0  
ldv-regression/test_union_cast-1_true-unreach-call_true-termination.i 2 .046 .043 6.3 .28 .0082 0     - - - - 2 3.4  1.9  250 0   0     2 7.5   4.3   310   .66 0  
ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i 2 .050 .047 6.5 .27 .0082 0     - - - - 2 3.5  1.9  250 0   0     2 8.1   4.9   300   .66 0  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call.i 2 .044 .041 7.1 .34 .0082 0     - - - - 2 3.7  2.1  240 0   0     2 8.8   5.2   310   .66 0  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call_1.i 2 .048 .045 6.7 .34 .0082 0     - - - - 2 3.8  2.1  250 0   0     2 8.4   5.0   300   .66 0  
ldv-regression/test_union_true-termination.c_true-unreach-call.i 2 .052 .048 6.6 .30 .0082 0     - - - - 2 4.2  2.3  250 0   0     2 8.6   5.1   300   .66 0  
ldv-regression/test_union_true-termination.c_true-unreach-call_1.i 2 .048 .045 7.8 .29 .0082 0     - - - - 2 3.5  2.0  250 0   0     2 6.8   4.3   300   .66 0  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call.i 2 .047 .044 6.8 .33 .0082 0     - - - - 2 4.0  2.2  250 0   0     2 8.7   4.8   300   .66 0  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i 2 .050 .048 6.9 .27 .0082 0     - - - - 2 4.4  2.4  250 0   0     2 9.2   5.4   310   .66 0  
ldv-regression/test02_false-unreach-call_true-termination.c 1 .061 .053 9.2 .55 .0082 0     1 4.3 2.4 250 0   0     1 7.0 4.4 300 .66 0   1 3.7 2.1 250 0   0     1 .59 .58 20 .045 0      - -
ldv-regression/test06_false-unreach-call_true-termination.c 1 .069 .059 9.9 .53 .0082 0     -32 4.6 2.6 250 0   0     1 7.2 4.1 310 .62 0   1 3.7 2.2 250 0   .012 0 .57 .57 20 .037 .0041 - -
ldv-regression/test08_false-unreach-call_true-termination.c 1 .14  .12  8.6 .43 .0082 0     1 3.8 2.1 260 0   0     1 7.4 4.6 310 .66 0   1 3.6 2.1 250 0   0     1 .60 .60 20 .045 0      - -
ldv-regression/test12_false-unreach-call_true-termination.c 1 .072 .062 9.6 .41 .0082 0     1 4.7 2.6 250 0   0     1 7.4 4.1 310 .66 0   1 3.6 2.1 250 0   0     1 .57 .57 20 .045 0      - -
ldv-regression/test21_false-unreach-call_true-termination.c 1 .12  .11  10   .37 .0082 0     1 4.7 2.6 250 0   0     1 8.2 4.6 300 .66 0   0 3.9 2.3 250 0   0     1 .58 .58 20 .057 .0041 - -
ldv-regression/test22_false-unreach-call.c 1 .077 .067 9.8 .59 .0082 0     1 4.6 2.6 260 0   0     1 11   6.5 400 .66 0   0 3.8 2.2 250 0   .21  -32 .61 .60 20 .057 0      - -
ldv-regression/test23_false-unreach-call.c 1 .41  .40  12   5.2  .053  0     1 5.6 3.1 260 0   0     0 97   61   5400 .76 0   0 4.1 2.4 250 0   0     -32 .62 .62 20 .057 0      - -
ldv-regression/test24_false-unreach-call.c 1 .37  .36  16   4.7  .16   0     1 5.0 2.8 270 0   0     0 71   45   7000 .66 0   0 4.3 2.5 250 0   .20  0 .59 .59 21 .037 .0041 - -
ldv-regression/test25_false-unreach-call_true-termination.c 1 .17  .16  10   1.9  .074  0     1 5.7 3.2 280 0   0     1 35   20   600 .62 0   0 4.4 2.5 250 0   0     0 .59 .59 21 .037 0      - -
ldv-regression/test26_false-unreach-call_true-termination.c 1 .063 .054 9.5 .59 .0082 0     1 4.8 2.6 250 0   0     1 7.2 4.4 310 .66 0   1 3.6 2.1 250 0   0     1 .56 .56 20 .045 0      - -
ldv-regression/test27_false-unreach-call_true-termination.c 1 .23  .22  11   2.4  .078  0     1 5.6 3.2 270 0   0     1 12   6.7 520 .66 0   0 4.3 2.5 250 0   0     0 .60 .60 20 .037 0      - -
ldv-regression/test28_false-unreach-call_true-termination.c 1 .059 .050 9.5 .59 .0082 0     1 5.1 2.8 250 0   0     1 8.6 4.8 320 .66 0   -32 3.6 2.1 250 0   0     1 .59 .59 20 .049 0      - -
ldv-regression/test29_false-unreach-call_true-termination.c 1 .075 .065 10   .48 .0082 0     1 5.1 2.8 250 0   0     1 8.9 5.3 320 .66 0   0 3.8 2.2 250 0   0     1 .59 .60 20 .049 0      - -
ldv-regression/test30_false-unreach-call_true-termination.c 1 .058 .049 10   .47 .0082 0     -32 4.0 2.2 260 0   0     1 7.0 4.0 310 .62 0   1 3.7 2.1 240 0   0     1 .59 .59 20 .049 0      - -
ldv-regression/test01_true-unreach-call_true-termination.c 2 .048 .045 6.8 .36 .0082 0     - - - - 2 3.4  1.9  250 0   0     2 7.9   4.5   310   .62 0  
ldv-regression/test03_true-unreach-call_true-termination.c 2 .11  .099 6.4 .25 .0082 0     - - - - 2 4.5  2.5  250 0   0     2 9.7   5.7   310   .66 0  
ldv-regression/test04_true-unreach-call_true-termination.c 2 .050 .047 7.5 .32 .0082 0     - - - - 2 3.5  2.0  260 0   0     2 10     5.9   310   .66 0  
ldv-regression/test05_true-unreach-call_true-termination.c 2 .047 .047 7.1 .48 .0082 0     - - - - 2 3.7  2.1  250 0   0     2 12     7.2   330   .66 0  
ldv-regression/test07_true-unreach-call_true-termination.c 2 .052 .049 6.6 .36 .0082 0     - - - - 2 3.4  1.9  250 0   0     2 11     6.7   320   .66 0  
ldv-regression/test09_true-unreach-call_true-termination.c 2 .050 .047 6.7 .44 .0082 0     - - - - 2 4.7  2.6  260 0   0     2 9.5   5.8   310   .62 0  
ldv-regression/test10_true-unreach-call_true-termination.c 2 .12  .11  6.1 .27 .0082 0     - - - - 2 3.5  2.0  260 0   0     2 14     8.4   440   .62 0  
ldv-regression/test11_true-unreach-call_true-termination.c 2 .056 .054 6.5 .39 .0082 0     - - - - 2 4.4  2.4  260 0   0     2 10     6.1   310   .66 0  
ldv-regression/test13_true-unreach-call_true-termination.c 2 .055 .053 6.9 .39 .0082 0     - - - - 2 3.6  2.1  250 0   0     2 9.7   5.6   310   .66 0  
ldv-regression/test14_true-unreach-call_true-termination.c 2 .057 .055 6.5 .38 .0082 0     - - - - 2 4.5  2.5  260 0   0     2 9.4   5.2   310   .62 0  
ldv-regression/test15_true-unreach-call_true-termination.c 2 .058 .055 7.9 .32 .0082 0     - - - - 2 4.1  2.3  250 0   0     2 7.5   4.3   310   .66 0  
ldv-regression/test16_true-unreach-call_true-termination.c 2 .049 .046 7.2 .37 .0082 0     - - - - 2 3.7  2.1  250 0   0     2 7.6   4.4   300   .62 0  
ldv-regression/test17_true-unreach-call_true-termination.c 2 .053 .050 7.4 .30 .0082 0     - - - - 2 3.4  1.9  250 0   0     2 7.3   4.2   300   .62 0  
ldv-regression/test18_true-unreach-call_true-termination.c 2 .11  .10  6.2 .26 .0082 0     - - - - 2 3.7  2.0  250 0   0     2 9.8   5.9   310   .66 0  
ldv-regression/test19_true-unreach-call_true-termination.c 2 .047 .044 7.8 .43 .0082 0     - - - - 2 4.4  2.5  250 0   0     2 9.9   5.5   310   .66 0  
ldv-regression/test20_true-unreach-call_true-termination.c 2 .049 .046 7.7 .36 .0082 0     - - - - 2 3.8  2.2  250 0   0     2 8.0   4.5   320   .66 0  
ldv-regression/test21_true-unreach-call_true-termination.c 2 .10  .094 6.5 .28 .0082 0     - - - - 2 4.8  2.6  250 0   0     2 9.8   5.5   310   .62 0  
ldv-regression/test22_true-unreach-call.c 2 .79  .79  7.6 9.8  .045  0     - - - - 0 6.7  3.7  290 0   0     2 26     16     670   .66 0  
ldv-regression/test23_true-unreach-call.c 2 .43  .42  12   5.3  .045  0     - - - - 0 5.7  3.2  300 0   0     2 60     46     670   .62 0  
ldv-regression/test24_true-unreach-call_true-termination.c 2 .33  .33  10   4.1  .041  0     - - - - 0 5.5  3.0  280 0   0     2 27     21     490   .62 0  
ldv-regression/test25_true-unreach-call.c 2 1.9   1.9   13   24    .057  0     - - - - 0 12    7.6  440 0   0     2 31     22     500   .66 0  
ldv-regression/test26_true-unreach-call_true-termination.c 2 .049 .047 7.4 .32 .0082 0     - - - - 2 4.3  2.4  250 0   0     2 10     5.6   310   .66 0  
ldv-regression/test27_true-unreach-call_true-termination.c 2 .23  .22  11   2.7  .070  0     - - - - 0 17    13    510 0   0     2 83     69     690   .62 0  
ldv-regression/test28_true-unreach-call_true-termination.c 2 .050 .047 7.4 .39 .0082 0     - - - - 2 4.5  2.5  250 0   0     2 9.0   5.1   320   .66 0  
ldv-regression/test29_true-unreach-call_true-termination.c 2 .061 .058 6.7 .41 .0082 0     - - - - 2 3.5  2.0  250 0   0     2 10     6.1   310   .62 0  
ldv-regression/test30_true-unreach-call_true-termination.c 2 .057 .055 7.0 .34 .0082 0     - - - - 2 3.4  1.9  250 0   0     2 12     6.7   340   .66 0  
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i 1 55     55     1400   590    1.4    0     0 8.6 4.6 340 0   0     0 28   16   530 .68 0   0 6.3 3.6 280 0   .43  1 1.1  1.1  21 .50  0      - -
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i 1 46     46     1400   570    1.1    0     0 8.5 4.5 340 0   0     0 28   16   510 .71 0   0 7.5 4.0 300 0   0     1 1.1  1.1  23 .39  0      - -
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i 1 51     51     1400   610    1.3    0     0 8.6 4.5 340 0   0     0 32   17   520 .75 0   0 6.4 3.6 280 0   .30  1 1.1  1.1  21 .50  0      - -
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i 0 880     880     2400   7100    22      0     - - - - 0 .62 .37 41 0   0     0 .021 .022 5.8 0    0  
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i 0 880     880     2400   9400    22      0     - - - - 0 .75 .47 41 0   0     0 .025 .026 5.6 0    0  
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i 0 880     880     2400   7500    16      0     - - - - 0 .72 .44 42 0   0     0 .033 .034 5.6 0    0  
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i 0 880     880     2400   7400    16      0     - - - - 0 .59 .37 41 0   0     0 .021 .022 5.6 0    0  
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i 0 880     880     2400   7600    20      0     - - - - 0 .81 .49 41 0   0     0 .024 .025 5.6 0    0  
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i 0 880     880     2400   7100    16      0     - - - - 0 .77 .47 40 0   0     0 .024 .024 5.6 0    0  
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i 0 880     880     2400   7200    16      0     - - - - 0 .77 .48 40 0   0     0 .021 .022 5.6 0    0  
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i 0 880     880     2400   8000    23      0     - - - - 0 .60 .37 41 0   0     0 .021 .022 5.6 0    0  
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i 0 880     880     2400   9900    17      0     - - - - 0 .58 .35 40 0   0     0 .021 .022 5.8 0    0  
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i 0 880     880     2400   9400    23      0     - - - - 0 .62 .39 40 0   0     0 .030 .032 5.7 0    0  
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i 1 .15  .14  9.8 .87 .012  0     1 6.5 3.6 270 0   .057 0 19   11   310 .71 0   0 4.3 2.5 250 0   0     0 .58 .58 20 .020 0      - -
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i 1 .10  .094 9.7 .92 .012  0     1 5.6 3.1 260 0   0     0 16   9.1 310 .75 0   0 4.4 2.5 250 0   0     1 .62 .62 20 .070 0      - -
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i 1 .14  .13  9.5 .73 .012  0     1 5.8 3.2 260 0   0     0 16   9.7 310 .71 0   0 4.5 2.6 250 0   .20  1 .63 .64 20 .070 0      - -
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i 1 .17  .16  9.4 2.2  .057  0     1 5.3 3.0 260 0   0     0 16   9.4 310 .75 0   0 4.8 2.7 250 0   .012 1 .63 .63 21 .074 0      - -
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i 1 .15  .14  11   1.3  .012  0     1 5.4 3.0 250 0   0     0 18   11   300 .71 0   0 4.1 2.4 250 0   .20  0 .59 .59 20 .020 0      - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i 1 .17  .17  13   2.0  .012  0     1 6.6 3.7 260 0   0     0 16   9.5 320 .75 0   0 5.5 3.1 250 0   0     1 .64 .64 21 .074 0      - -
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i 1 .13  .12  9.8 2.1  .012  0     1 5.0 2.7 260 0   0     0 18   11   310 .75 0   0 4.3 2.4 250 0   0     1 .63 .63 20 .070 0      - -
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i 1 .13  .12  9.7 1.2  .012  0     1 5.8 3.2 260 0   0     0 16   9.4 310 .75 0   0 4.5 2.6 260 0   0     1 .63 .63 20 .074 0      - -
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i 1 .12  .11  9.4 1.1  .012  0     1 5.8 3.2 260 0   0     0 17   9.7 310 .75 0   0 4.3 2.5 250 0   0     1 .66 .66 20 .070 0      - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i 1 .10  .096 9.7 1.1  .012  0     1 7.9 4.3 280 0   0     0 15   9.2 310 .75 0   0 4.5 2.5 260 0   0     0 .58 .58 20 .020 0      - -
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i 1 .13  .12  9.7 1.2  .012  0     1 5.8 3.2 260 0   0     0 21   13   310 .68 0   0 5.3 3.0 260 0   .29  0 .57 .57 21 .020 .025  - -
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i 1 .10  .093 9.6 1.2  .012  0     1 4.8 2.6 270 0   0     0 14   8.4 310 .75 0   0 4.2 2.4 250 0   .29  1 .62 .62 20 .070 0      - -
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i 1 .10  .092 9.4 1.0  .012  0     1 5.4 3.0 260 0   0     0 19   11   310 .75 0   0 4.3 2.4 250 0   0     1 .66 .66 20 .070 0      - -
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i 1 .19  .18  9.5 1.9  .053  0     1 5.5 3.1 260 0   0     0 17   9.6 310 .75 0   0 4.4 2.5 260 0   0     1 .63 .63 21 .074 0      - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i 1 .16  .15  9.5 1.0  .012  0     1 5.6 3.0 260 0   0     0 14   8.8 310 .75 0   0 4.3 2.5 250 0   0     0 .57 .57 20 .020 0      - -
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i 1 .14  .13  9.4 1.4  .012  0     1 5.2 2.9 260 0   0     0 15   9.3 310 .75 0   0 4.3 2.5 250 0   0     1 .62 .62 21 .074 0      - -
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i 1 .14  .13  9.9 1.2  .012  0     1 5.8 3.2 260 0   0     0 17   10   310 .75 0   0 4.2 2.5 260 0   0     1 .63 .63 20 .070 0      - -
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i 1 .18  .17  9.6 .99 .012  0     1 5.1 2.8 270 0   .057 0 16   9.4 310 .68 0   0 4.6 2.6 260 0   0     1 .63 .64 21 .074 .025  - -
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i 1 .15  .14  9.8 1.0  .012  0     1 6.1 3.3 250 0   0     0 16   9.4 320 .75 0   0 4.2 2.4 250 0   0     1 .63 .63 20 .070 0      - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i 0 880     880     2000   12000    14      0     - - - - 0 .75 .47 42 0   0     0 .021 .022 5.8 0    0  
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i 0 220     220     15000   2600    1.2    0     - - - - 0 .75 .47 40 0   0     0 .021 .023 5.6 0    0  
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i 0 720     720     4300   6500    11      0     - - - - 0 .63 .38 41 0   0     0 .021 .022 5.6 0    0  
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i 0 880     880     4300   9900    7.2    0     - - - - 0 .76 .45 40 0   0     0 .020 .021 5.6 0    0  
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i 0 880     880     2500   11000    3.3    0     - - - - 0 .63 .39 41 0   0     0 .027 .028 5.6 0    0  
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i 0 880     880     2700   9400    1.0    0     - - - - 0 .78 .48 41 0   0     0 .026 .028 5.7 0    0  
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i 0 880     880     5200   11000    4.1    0     - - - - 0 .60 .36 41 0   0     0 .021 .022 5.7 0    0  
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i 0 880     880     12000   10000    1.5    0     - - - - 0 .62 .38 42 0   0     0 .021 .022 5.6 0    0  
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i 0 880     880     810   8200    2.9    0     - - - - 0 .73 .45 41 0   0     0 .024 .024 5.6 0    0  
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i 0 870     880     520   8400    1.6    0     - - - - 0 .60 .37 41 0   0     0 .028 .029 5.6 0    0  
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i 0 880     880     1200   12000    10      0     - - - - 0 .67 .42 40 0   0     0 .022 .022 5.6 0    0  
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i 0 880     880     610   7700    .36   0     - - - - 0 .66 .41 40 0   0     0 .022 .023 5.6 0    0  
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i 0 210     210     15000   2600    1.2    0     - - - - 0 .67 .41 41 0   0     0 .020 .021 5.6 0    0  
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i 0 840     840     4100   7800    14      0     - - - - 0 .60 .36 40 0   0     0 .025 .026 5.6 0    0  
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i 0 880     880     4200   13000    6.8    0     - - - - 0 .72 .43 40 0   0     0 .022 .024 5.6 0    0  
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i 0 880     880     1900   12000    1.1    0     - - - - 0 .64 .38 42 0   0     0 .021 .024 5.6 0    0  
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i 0 880     880     2000   11000    1.1    0     - - - - 0 .80 .49 41 0   0     0 .024 .025 5.8 0    0  
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i 0 880     880     2200   12000    17      0     - - - - 0 .71 .43 40 0   0     0 .023 .025 5.7 0    0  
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i 0 880     880     6400   11000    1.4    0     - - - - 0 .73 .44 40 0   0     0 .023 .025 5.7 0    0  
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i 0 880     880     8100   9700    2.3    0     - - - - 0 .71 .44 41 0   0     0 .027 .028 5.6 0    0  
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i 0 880     880     490   10000    1.3    0     - - - - 0 .71 .43 41 0   0     0 .026 .027 5.7 0    0  
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i 1 .13  .12  9.7 1.2  .012  0     1 6.5 3.5 260 0   0     1 8.5 4.7 310 .62 0   0 4.3 2.5 250 0   0     1 .66 .66 20 .070 0      - -
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i 0 .11  .099 9.2 .90 .012  0     0 96   77   2000 0   0     -32 8.6 5.0 310 .66 0   0 4.0 2.3 250 0   0     -32 .63 .62 21 .070 .025  - -
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup_true-termination.i 1 .10  .095 9.7 .92 .012  0     1 4.9 2.7 260 0   0     1 8.3 4.7 310 .62 0   0 4.0 2.4 240 0   .30  1 .62 .63 20 .066 0      - -
list-ext2-properties/list_and_tree_cnstr_false-unreach-call_false-termination.i 1 .27  .26  20   3.0  .012  0     -32 7.3 3.9 270 0   0     1 19   11   490 .66 0   0 5.0 2.9 260 0   0     0 .66 .68 21 .049 0      - -
list-ext2-properties/list_and_tree_cnstr_true-unreach-call_false-termination.i 0 880     880     1500   8000    .50   0     - - - - 0 .75 .45 42 0   0     0 .020 .021 5.6 0    0  
list-ext2-properties/simple_and_skiplist_2lvl_false-unreach-call.i 1 .15  .14  9.5 1.4  .012  0     1 5.6 3.1 250 0   0     1 11   6.1 320 .66 0   0 4.1 2.4 250 0   0     1 .64 .63 20 .078 0      - -
list-ext2-properties/simple_and_skiplist_2lvl_true-unreach-call.i 0 880     880     680   7500    .28   0     - - - - 0 .76 .46 40 0   0     0 .023 .024 5.6 0    0  
list-ext2-properties/simple_search_value_false-unreach-call.i 1 .24  .23  10   1.9  .14   0     1 11   7.1 300 0   0     0 75   48   7000 .72 0   0 4.7 2.7 260 0   0     1 .64 .64 21 .066 0      - -
list-ext2-properties/simple_search_value_true-unreach-call.i 0 880     880     7200   12000    18      0     - - - - 0 .62 .38 41 0   0     0 .027 .028 5.7 0    0  
ldv-sets/test_add_false-unreach-call_true-termination.i 1 .10  .089 9.1 .91 .012  0     1 5.5 3.0 260 0   0     1 9.3 5.2 320 .66 0   0 4.5 2.6 260 0   .11  0 .58 .58 20 .020 0      - -
ldv-sets/test_mutex_double_lock_false-unreach-call_true-termination.i 1 .14  .13  9.8 2.0  .012  0     1 5.1 2.8 260 0   0     1 12   6.8 360 .62 0   0 4.7 2.7 250 0   .070 0 .58 .57 20 .020 0      - -
ldv-sets/test_mutex_double_unlock_false-unreach-call.i 1 .49  .48  21   5.6  .086  0     -32 12   6.2 440 0   0     1 13   6.8 510 .62 0   0 5.1 2.9 270 0   .18  0 .58 .58 21 .020 0      - -
ldv-sets/test_mutex_unbounded_false-unreach-call.i 1 .22  .21  15   2.2  .012  0     -32 8.2 4.5 270 0   0     1 11   6.5 420 .62 0   0 5.2 2.9 260 0   .11  0 .57 .57 21 .020 0      - -
ldv-sets/test_mutex_unlock_at_exit_false-unreach-call.i 1 .32  .31  14   4.3  .082  0     -32 9.2 4.8 370 0   0     1 12   6.9 460 .66 0   0 5.6 3.2 270 0   0     0 .57 .57 21 .020 0      - -
ldv-sets/test_add_true-unreach-call_true-termination.i 2 .088 .082 7.4 1.0  .016  0     - - - - 0 6.2  3.4  290 0   0     0 960     940     890   .62 0  
ldv-sets/test_mutex_true-unreach-call.i 2 .51  .50  22   6.3  .15   0     - - - - 2 160    140    2000 0   0     0 960     930     1100   .68 0  
ldv-sets/test_mutex_unbounded_true-unreach-call.i 0 880     880     4900   8100    15      0     - - - - 0 .68 .41 40 0   0     0 .022 .023 5.6 0    0  
list-simple/dll2c_append_equal_true-unreach-call_true-valid-memsafety.i 2 .22  .21  7.1 2.1  .074  0     - - - - 0 15    11    550 0   .057 0 960     940     690   .68 0  
list-simple/dll2c_append_unequal_true-unreach-call_true-valid-memsafety.i 2 .19  .19  7.1 2.0  .074  0     - - - - 0 16    11    570 0   0     0 960     930     760   .70 0  
list-simple/dll2c_insert_equal_true-unreach-call_true-valid-memsafety.i 2 .19  .19  7.2 2.3  .074  0     - - - - 0 20    15    730 0   0     0 960     930     910   .63 0  
list-simple/dll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i 2 .21  .20  7.3 2.6  .078  0     - - - - 0 34    27    870 0   0     0 960     930     690   .69 0  
list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i 2 .18  .18  6.9 2.0  .074  0     - - - - 0 18    13    560 0   0     0 960     940     650   .72 0  
list-simple/dll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i 2 .19  .18  7.7 2.7  .074  0     - - - - 0 18    13    560 0   0     0 960     930     800   .69 0  
list-simple/dll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i 2 .16  .15  7.3 2.3  .053  0     - - - - 2 37    30    900 0   0     2 270     260     800   .62 0  
list-simple/dll2c_remove_all_true-unreach-call_true-valid-memsafety.i 2 .19  .18  7.2 2.0  .053  0     - - - - 0 14    9.4  520 0   0     0 960     950     530   1.2  0  
list-simple/dll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i 2 .16  .16  7.0 2.7  .070  0     - - - - 0 28    22    890 0   0     0 960     920     1500   .63 0  
list-simple/dll2c_update_all_true-unreach-call_true-valid-memsafety.i 2 .17  .17  7.5 2.1  .070  0     - - - - 0 24    19    790 0   0     2 75     56     880   .62 0  
list-simple/dll2n_append_equal_true-unreach-call_true-valid-memsafety.i 2 .23  .23  8.1 1.9  .078  0     - - - - 0 10    5.4  340 0   0     0 960     940     1300   1.3  0  
list-simple/dll2n_append_unequal_true-unreach-call_true-valid-memsafety.i 2 .18  .18  7.5 2.2  .082  0     - - - - 0 9.0  4.9  350 0   0     0 960     940     1000   1.3  0  
list-simple/dll2n_insert_equal_true-unreach-call_true-valid-memsafety.i 2 .20  .20  7.8 2.0  .074  0     - - - - 0 8.4  4.6  330 0   0     0 960     920     940   1.3  0  
list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i 2 .19  .18  7.5 1.9  .074  0     - - - - 0 9.8  5.2  360 0   0     0 960     930     1400   .63 0  
list-simple/dll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i 2 .17  .17  7.7 1.8  .070  0     - - - - 0 7.2  4.0  310 0   0     0 690     660     900   .68 0  
list-simple/dll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i 2 .22  .21  7.6 1.9  .070  0     - - - - 0 6.8  3.7  300 0   0     0 960     920     1600   1.0  0  
list-simple/dll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i 2 .15  .15  7.8 2.0  .066  0     - - - - 0 7.1  3.9  310 0   0     2 53     40     580   .62 0  
list-simple/dll2n_remove_all_true-unreach-call_true-valid-memsafety.i 2 .14  .13  7.7 2.1  .049  0     - - - - 0 6.2  3.3  290 0   0     2 24     15     520   .62 0  
list-simple/dll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i 2 .17  .16  7.7 1.4  .061  0     - - - - 0 8.7  4.7  350 0   0     2 9.3   5.2   320   .66 0  
list-simple/dll2n_update_all_true-unreach-call_true-valid-memsafety.i 2 .17  .17  7.4 2.5  .066  0     - - - - 0 7.7  4.1  330 0   0     2 62     45     750   .62 0  
list-simple/sll2c_append_equal_true-unreach-call_true-valid-memsafety.i 2 .19  .18  7.0 2.4  .078  .049 - - - - 0 20    14    680 0   0     0 960     940     850   .63 0  
list-simple/sll2c_append_unequal_true-unreach-call_true-valid-memsafety.i 2 .20  .20  7.6 2.1  .082  0     - - - - 0 40    32    1100 0   0     0 960     950     790   .63 0  
list-simple/sll2c_insert_equal_true-unreach-call_true-valid-memsafety.i 2 .21  .21  7.0 2.0  .070  0     - - - - 0 21    15    660 0   0     0 960     900     730   .68 0  
list-simple/sll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i 2 .20  .19  7.2 2.1  .074  0     - - - - 0 28    22    850 0   0     0 960     930     930   .68 0  
list-simple/sll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i 2 .18  .18  7.7 2.4  .078  0     - - - - 0 21    15    670 0   0     0 960     940     850   .63 0  
list-simple/sll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i 2 .19  .19  7.8 2.4  .078  0     - - - - 0 24    17    720 0   0     0 960     940     710   .62 0  
list-simple/sll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i 2 .18  .18  7.1 1.8  .074  0     - - - - 2 160    150    2000 0   0     2 40     26     640   .66 0  
list-simple/sll2c_remove_all_true-unreach-call_true-valid-memsafety.i 2 .18  .17  6.9 1.7  .061  0     - - - - 0 15    10    550 0   0     0 960     950     680   .63 0  
list-simple/sll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i 2 .17  .17  7.3 1.8  .066  0     - - - - 0 26    21    890 0   0     2 55     39     580   .62 0  
list-simple/sll2c_update_all_true-unreach-call_true-valid-memsafety.i 2 .16  .16  7.1 1.8  .066  0     - - - - 0 24    18    670 0   0     2 51     36     740   .62 0  
list-simple/sll2n_append_equal_true-unreach-call_true-valid-memsafety.i 2 .18  .17  7.9 2.3  .078  0     - - - - 0 23    17    680 0   0     0 960     940     1800   1.3  3.3
list-simple/sll2n_append_unequal_true-unreach-call_true-valid-memsafety.i 2 .17  .17  7.7 1.9  .078  0     - - - - 0 26    19    820 0   .057 0 960     940     950   .68 0  
list-simple/sll2n_insert_equal_true-unreach-call_true-valid-memsafety.i 2 .18  .17  8.0 1.9  .070  0     - - - - 0 28    20    730 0   0     0 960     930     870   .74 0  
list-simple/sll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i 2 .21  .20  7.5 1.8  .074  0     - - - - 0 35    28    1000 0   0     0 960     920     750   .69 0  
list-simple/sll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i 2 .20  .20  7.4 1.8  .070  0     - - - - 0 16    11    550 0   0     0 960     930     720   .68 0  
list-simple/sll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i 2 .16  .16  8.0 1.8  .070  0     - - - - 0 17    12    560 0   0     0 960     920     890   1.3  0  
list-simple/sll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i 2 .17  .16  7.0 1.7  .066  0     - - - - 2 28    21    700 0   0     2 95     77     890   .62 0  
list-simple/sll2n_remove_all_true-unreach-call_true-valid-memsafety.i 2 .14  .13  7.7 1.7  .049  0     - - - - 2 14    9.4  540 0   0     2 33     25     770   .62 0  
list-simple/sll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i 2 .16  .15  7.4 1.5  .066  0     - - - - 0 37    27    960 0   0     2 41     29     690   .66 0  
list-simple/sll2n_update_all_true-unreach-call_true-valid-memsafety.i 2 .17  .17  7.1 1.5  .066  0     - - - - 0 22    17    700 0   0     2 62     46     760   .62 0  
heap-data/calendar_true-unreach-call.i 0 880     880     2600   7900    .76   0     - - - - 0 .57 .35 40 0   0     0 .029 .030 5.7 0    0  
heap-data/cart_true-unreach-call.i 0 880     880     950   9300    .29   0     - - - - 0 .59 .37 41 0   0     0 .025 .026 5.6 0    0  
heap-data/hash_fun_true-unreach-call.i 0 880     880     64   13000    .14   0     - - - - 0 .61 .38 41 0   0     0 .022 .023 5.6 0    0  
heap-data/min_max_true-unreach-call.i 0 880     880     190   13000    .14   0     - - - - 0 .61 .37 40 0   0     0 .026 .026 5.6 0    0  
heap-data/packet_filter_true-unreach-call.i 0 880     880     730   9300    1.1    0     - - - - 0 .71 .43 40 0   0     0 .027 .027 5.6 0    0  
heap-data/process_queue_true-unreach-call.i 0 880     880     6400   9200    5.7    0     - - - - 0 .74 .45 42 0   0     0 .022 .024 5.6 0    0  
heap-data/quick_sort_split_true-unreach-call.i 0 880     880     2100   12000    1.3    0     - - - - 0 .64 .39 41 0   0     0 .021 .022 5.6 0    0  
heap-data/running_example_true-unreach-call.i 0 880     880     2200   5200    .28   0     - - - - 0 .79 .48 41 0   0     0 .027 .028 5.6 0    0  
heap-data/shared_mem1_true-unreach-call.i 0 880     880     1800   12000    12      0     - - - - 0 .79 .49 41 0   0     0 .026 .027 5.8 0    0  
heap-data/shared_mem2_true-unreach-call.i 0 880     880     6700   9000    8.2    0     - - - - 0 .74 .46 40 0   0     0 .026 .027 5.6 0    0  
list-ext3-properties/dll_nullified_false-unreach-call_false-valid-memcleanup.i 1 .18  .17  10   2.1  .070  0     1 6.2 3.4 270 0   0     1 17   10   530 .62 0   0 4.6 2.6 260 0   0     1 .64 .64 21 .074 0      - -
list-ext3-properties/sll_length_check_false-unreach-call_false-valid-memcleanup.i 1 .21  .19  9.9 1.8  .066  0     0 98   85   1900 0   0     0 91   82   960 .62 0   0 4.6 2.7 260 0   0     1 .63 .63 21 .070 0      - -
list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i 1 .48  .47  35   5.7  .078  0     1 7.2 3.8 280 0   0     1 89   81   1100 .62 0   0 4.6 2.7 260 0   0     -32 .64 .64 21 .078 .025  - -
list-ext3-properties/sll_of_sll_nondet_append_false-unreach-call_false-valid-memcleanup.i 0 5.4   5.4   230   65    .42   0     0 97   76   1700 0   0     0 94   60   7000 .67 0   0 12   6.3 470 0   0     0 .69 .69 23 .053 0      - -
list-ext3-properties/dll_circular_traversal_true-unreach-call_true-valid-memsafety.i 2 .19  .19  8.0 2.1  .082  0     - - - - 0 8.2  4.4  330 0   0     0 960     910     3300   .63 0  
list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i 2 .20  .20  8.2 2.4  .082  0     - - - - 0 7.0  3.8  330 0   0     0 960     900     1600   1.2  0  
list-ext3-properties/sll_circular_traversal_true-unreach-call_true-valid-memsafety.i 2 .18  .18  7.5 2.0  .078  0     - - - - 0 7.0  3.7  310 0   0     0 960     940     970   .63 0  
list-ext3-properties/sll_length_check_true-unreach-call_true-valid-memsafety.i 2 2.5   2.4   44   29    .91   0     - - - - 0 910    910    910 0   0     0 960     920     1200   .63 0  
list-ext3-properties/sll_nondet_insert_true-unreach-call_true-valid-memsafety.i 2 8.8   8.8   160   140    1.0    0     - - - - 0 910    900    1600 0   0     0 960     900     2300   1.2  0  
list-ext3-properties/sll_of_sll_nondet_append_true-unreach-call_true-valid-memsafety.i 0 880     880     2000   5900    23      0     - - - - 0 .71 .43 41 0   0     0 .022 .024 5.6 0    0  
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) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
total 241 288 49000   49000   220000 540000 490    .049 75 -229 710 470 25000 0   .11 75 7 1500   1000   52000 50    0   75 -19 340   200   19000 0   8.5   75 -109 47   47   1500 5.5  .12  166 120 3300 2900 51000 0   .11 166 148 35000 33000 69000 75 3.3
    correct results 180 288 190   190   5900 2200 11    .049 59 59 330 180 15000 0   .11 39 39 480   310   15000 25    0   13 13 48   28   3200 0   .045 51 51 33   33   1000 4.5  .041 60 120 640 480 20000 0   0    74 148 2300 1800 31000 48 0  
        correct true 108 216 27   26   1000 330 5.9  .049 0 0 0 0 60 120 640 480 20000 0   0    74 148 2300 1800 31000 48 0  
        correct false 72 72 160   160   4900 1900 5.5  0     59 59 330 180 15000 0   .11 39 39 480   310   15000 25    0   13 13 48   28   3200 0   .045 51 51 33   33   1000 4.5  .041 0 0
    correct-unconfimed results 2 0 5.7 5.7 240 68 .43 0     0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 2 0 5.7 5.7 240 68 .43 0     0 0 0 0 0 0
    incorrect results 0 9 -288 64 34 2700 0   0    1 -32 8.6 5.0 310 .66 0   1 -32 3.6 2.1 250 0   0     5 -160 3.2 3.1 100 .36 .049 0 0
        incorrect true 0 9 -288 64 34 2700 0   0    1 -32 8.6 5.0 310 .66 0   1 -32 3.6 2.1 250 0   0     5 -160 3.2 3.1 100 .36 .049 0 0
        incorrect false 0 0 0 0 0 0 0
score (241 tasks, max score: 407) 288 -229 7 -19 -109 120 148
Run set cbmc.sv-comp19_prop-reachsafety.ReachSafety-Heap cpa-seq-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Heap uautomizer-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Heap uautomizer-validate-correctness-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Heap