Tool CBMC Path 5.10 () 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:45:10 CET 2018-12-06 08:53:36 CET 2018-12-06 10:12:52 CET 2018-12-06 10:22:39 CET 2018-12-12 19:23:37 CET 2018-12-06 07:24:45 CET 2018-12-06 09:28:06 CET
Run set cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Heap cpa-seq-validate-violation-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Heap uautomizer-validate-violation-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Heap uautomizer-validate-correctness-witnesses-cbmc-path.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-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc-path.2018-12-04_2245.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-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cbmc-path.2018-12-04_2245.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-path.2018-12-04_2245.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc-path.2018-12-04_2245.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 false(unreach-call) 1 wit inspect .90  .89  66   9.7  3.0    0      false(unreach-call) 1 wit inspect 6.6  3.6  270 0   0   error (7) 0 --- inspect 19     11     340   .71 0   unknown 0 --- inspect 4.6  2.7  260 0   4.8  false(unreach-call) 1 --- inspect .67   .67   20    .11  0      - --- inspect - --- inspect
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .16  .16  20   1.7  .012  0      error (invalid witness file) 0 --- inspect .60 .36 40 0   0   error (2) 0 --- inspect .021 .023 5.8 0    0   error (invalid witness file) 0 --- inspect 1.1  .70 47 0   0    error (invalid witness file) 0 --- inspect .0042 .0053 .53 0     0      - --- inspect - --- inspect
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .071 .071 8.9 1.0  .012  0      error (invalid witness file) 0 --- inspect .58 .37 40 0   0   error (2) 0 --- inspect .021 .022 5.7 0    0   error (invalid witness file) 0 --- inspect .99 .63 48 0   0    error (invalid witness file) 0 --- inspect .0051 .0062 .39 0     0      - --- inspect - --- inspect
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .11  .11  13   1.1  .012  0      error (invalid witness file) 0 --- inspect .74 .46 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .95 .62 47 0   0    error (invalid witness file) 0 --- inspect .0050 .0061 .53 0     0      - --- inspect - --- inspect
heap-manipulation/tree_false-unreach-call_false-valid-deref.i error (134) 0 --- inspect .12  .12  9.3 .90 .012  0      error (invalid witness file) 0 --- inspect .67 .40 40 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0   error (invalid witness file) 0 --- inspect .93 .62 47 0   0    error (invalid witness file) 0 --- inspect .0052 .0065 .53 0     0      - --- inspect - --- inspect
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .087 .086 8.9 .80 .012  0      error (invalid witness file) 0 --- inspect .76 .45 41 0   0   error (2) 0 --- inspect .027 .027 5.6 0    0   error (invalid witness file) 0 --- inspect 1.0  .66 49 0   0    error (invalid witness file) 0 --- inspect .0065 .011  .53 0     0      - --- inspect - --- inspect
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i out of memory 0 --- inspect 170     170     15000   2400    360      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .47 41 0   0     error (2) 0 --- inspect .026 .027 5.6 0     0     
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i out of memory 0 --- inspect 240     240     15000   3100    530      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 40 0   0     error (2) 0 --- inspect .028 .029 5.6 0     0     
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .17  .17  20   1.9  .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .44 41 0   0     error (2) 0 --- inspect .022 .022 5.6 0     0     
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .073 .071 9.1 .71 .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0     error (2) 0 --- inspect .025 .026 5.6 0     0     
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i out of memory 0 --- inspect 130     130     15000   1700    290      .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .68 .41 41 0   0     error (2) 0 --- inspect .022 .022 5.6 0     0     
heap-manipulation/tree_true-unreach-call.i error (134) 0 --- inspect .16  .16  12   1.2  .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .45 41 0   0     error (2) 0 --- inspect .020 .021 5.6 0     0     
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i out of memory 0 --- inspect 220     220     15000   3000    650      0      error (invalid witness file) 0 --- inspect .62 .38 43 0   0   error (2) 0 --- inspect .022 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .95 .61 47 0   0    error (invalid witness file) 0 --- inspect .0016 .0027 .40 0     0      - --- inspect - --- inspect
list-properties/list_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .095 .095 13   1.1  .012  0      error (invalid witness file) 0 --- inspect .61 .39 40 0   0   error (2) 0 --- inspect .024 .025 5.6 0    0   error (invalid witness file) 0 --- inspect .99 .65 49 0   0    error (invalid witness file) 0 --- inspect .0017 .0019 .40 0     0      - --- inspect - --- inspect
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .091 .091 11   .94 .053  0      error (invalid witness file) 0 --- inspect .66 .41 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .90 .59 47 0   0    error (invalid witness file) 0 --- inspect .0025 .0032 .53 0     0      - --- inspect - --- inspect
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .83  .82  31   10    1.6    0      false(unreach-call) 1 wit inspect 5.1  2.8  260 0   0   timeout 0 --- inspect 97     86     680   1.0  0   unknown 0 --- inspect 4.3  2.4  260 0   .30 false(unreach-call) 1 --- inspect .62   .62   21    .070 0      - --- inspect - --- inspect
list-properties/simple_false-unreach-call_false-valid-memcleanup.i error (42) 0 --- inspect 880     880     12000   11000    1700      .0041 error (invalid witness file) 0 --- inspect .75 .47 40 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .95 .62 48 0   0    error (invalid witness file) 0 --- inspect .0055 .0075 .53 0     0      - --- inspect - --- inspect
list-properties/splice_false-unreach-call_false-valid-memcleanup.i error (42) 0 --- inspect 870     880     4300   9100    1900      0      error (invalid witness file) 0 --- inspect .76 .47 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .95 .61 47 0   0    error (invalid witness file) 0 --- inspect .0019 .0026 .53 0     0      - --- inspect - --- inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i out of memory 0 --- inspect 220     220     15000   3200    650      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .41 41 0   0     error (2) 0 --- inspect .027 .029 5.7 0     0     
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect .12  .12  11   .82 .053  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 40 0   0     error (2) 0 --- inspect .028 .030 5.6 0     0     
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i true 2 wit inspect 93     93     1500   1200    37      0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 28    15    630 0   0     true 2 --- inspect 560     530     1700   .68  0     
list-properties/list_true-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect .11  .11  13   1.1  .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 42 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0     
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect .082 .081 7.7 .44 .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0     error (2) 0 --- inspect .025 .027 5.6 0     0     
list-properties/simple_true-unreach-call_false-valid-memtrack.i error (42) 0 --- inspect 880     880     12000   9400    1700      .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .37 40 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0     
list-properties/splice_true-unreach-call_false-valid-memtrack.i error (42) 0 --- inspect 870     880     4500   9600    1900      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 40 0   0     error (2) 0 --- inspect .027 .027 5.6 0     0     
ldv-regression/1_3_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .078 .069 9.3 .65 .020  0      false(unreach-call) 1 wit inspect 4.4  2.5  250 0   0   false(unreach-call) 1 --- inspect 7.7   4.4   310   .66 0   false(unreach-call) 1 --- inspect 3.6  2.1  240 0   0    false(unreach-call) 1 --- inspect .58   .58   20    .057 0      - --- inspect - --- inspect
ldv-regression/alt_test_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .089 .081 9.4 .92 .012  0      false(unreach-call) 1 wit inspect 5.1  2.8  260 0   0   false(unreach-call) 1 --- inspect 11     6.4   350   .66 0   unknown 0 --- inspect 4.5  2.6  260 0   5.0  false(unreach-call) 1 --- inspect .65   .66   20    .086 0      - --- inspect - --- inspect
ldv-regression/callfpointer_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .066 .056 9.2 .36 .0082 0      false(unreach-call) 1 wit inspect 4.4  2.4  250 0   0   false(unreach-call) 1 --- inspect 6.9   4.0   320   .66 0   false(unreach-call) 1 --- inspect 3.4  2.0  240 0   0    false(unreach-call) 1 --- inspect .56   .56   20    .045 0      - --- inspect - --- inspect
ldv-regression/fo_test_true-termination.c_false-unreach-call.i error (134) 0 --- inspect .074 .074 8.0 .70 .012  0      error (invalid witness file) 0 --- inspect .76 .46 40 0   0   error (2) 0 --- inspect .026 .028 5.6 0    0   error (invalid witness file) 0 --- inspect .97 .62 47 0   0    error (invalid witness file) 0 --- inspect .0058 .0074 .53 0     0      - --- inspect - --- inspect
ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .14  .12  7.9 .25 .0082 0      true -32 wit inspect 3.6  2.0  250 0   0   false(unreach-call) 1 --- inspect 7.7   4.4   310   .66 0   false(unreach-call) 1 --- inspect 4.2  2.4  250 0   0    false(unreach-call) 1 --- inspect .60   .60   20    .049 .0041 - --- inspect - --- inspect
ldv-regression/mutex_lock_struct_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .064 .054 9.2 .44 .025  0      false(unreach-call) 1 wit inspect 3.8  2.1  250 0   0   false(unreach-call) 1 --- inspect 7.2   4.4   310   .66 0   false(unreach-call) 1 --- inspect 3.4  2.0  250 0   0    false(unreach-call) 1 --- inspect .61   .62   20    .045 0      - --- inspect - --- inspect
ldv-regression/recursive_list_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .082 .074 9.4 .51 .012  0      false(unreach-call) 1 wit inspect 4.1  2.3  250 0   0   false(unreach-call) 1 --- inspect 8.6   5.1   310   .66 0   false(unreach-call) 1 --- inspect 3.7  2.2  240 0   0    error (2) 0 --- inspect .59   .58   20    .037 0      - --- inspect - --- inspect
ldv-regression/rule57_ebda_blast_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .083 .075 8.9 .66 .012  0      true -32 wit inspect 4.4  2.4  250 0   0   false(unreach-call) 1 --- inspect 8.9   4.9   320   .66 0   unknown 0 --- inspect 4.0  2.3  250 0   .11 false(unreach-call) 1 --- inspect .61   .63   20    .070 .0041 - --- inspect - --- inspect
ldv-regression/rule60_list2_true-termination.c_false-unreach-call_1.i error (42) 0 --- inspect 6.7   6.7   45   93    24      0      error (invalid witness file) 0 --- inspect .61 .37 40 0   0   error (2) 0 --- inspect .026 .028 5.6 0    0   error (invalid witness file) 0 --- inspect .97 .63 48 0   0    error (invalid witness file) 0 --- inspect .0050 .0063 .53 0     0      - --- inspect - --- inspect
ldv-regression/stateful_check_false-unreach-call_false-termination.i out of memory 0 --- inspect 200     200     15000   2900    14      0      error (invalid witness file) 0 --- inspect .73 .44 42 0   0   error (2) 0 --- inspect .023 .025 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .62 47 0   0    error (invalid witness file) 0 --- inspect .0045 .0056 .53 0     0      - --- inspect - --- inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .16  .14  8.3 .35 .012  0      true -32 wit inspect 4.3  2.4  250 0   0   false(unreach-call) 1 --- inspect 7.2   4.1   300   .62 0   false(unreach-call) 1 --- inspect 3.9  2.2  250 0   0    false(unreach-call) 1 --- inspect .57   .57   20    .045 .0041 - --- inspect - --- inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect .069 .057 9.4 .59 .012  0      false(unreach-call) 1 wit inspect 4.6  2.5  250 0   0   false(unreach-call) 1 --- inspect 8.7   5.0   310   .66 0   false(unreach-call) 1 --- inspect 3.9  2.2  250 0   .29 false(unreach-call) 1 --- inspect .57   .57   20    .045 0      - --- inspect - --- inspect
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call.i true 2 wit inspect .036 .038 6.3 .34 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .82 .49 43 0   0     error (invalid witness file) 0 --- inspect 5.5   3.3   260   .61  0     
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i true 2 wit inspect .058 .054 5.1 .29 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .85 .51 42 0   0     error (invalid witness file) 0 --- inspect 5.4   2.9   270   .086 0     
ldv-regression/alias_of_return_true-termination.c_true-unreach-call.i true 2 wit inspect .042 .041 6.2 .24 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .82 .49 43 0   0     error (invalid witness file) 0 --- inspect 5.9   3.4   270   .65  0     
ldv-regression/alias_of_return_true-termination.c_true-unreach-call_1.i true 2 wit inspect .040 .039 6.2 .24 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .46 43 0   0     error (invalid witness file) 0 --- inspect 5.3   2.9   260   .65  0     
ldv-regression/ex3_forlist_true-termination.c_true-unreach-call.i true 2 wit inspect .084 .080 7.2 .69 .10   0      - --- inspect - --- inspect - --- inspect - --- inspect assertion 0 --- inspect 3.8  2.1  260 0   0     true 2 --- inspect 110     85     670   .62  0     
ldv-regression/just_assert_true-termination.c_true-unreach-call.i true 2 wit inspect .056 .055 5.7 .15 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .48 43 0   0     error (invalid witness file) 0 --- inspect 4.8   3.1   270   .61  0     
ldv-regression/mutex_lock_int_true-termination.c_true-unreach-call_1.i true 2 wit inspect .044 .042 6.1 .23 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .80 .47 43 0   0     error (invalid witness file) 0 --- inspect 6.2   3.7   270   .61  3.6   
ldv-regression/mutex_lock_struct_true-termination.c_true-unreach-call_1.i true 2 wit inspect .052 .049 6.6 .72 .025  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.1  250 0   0     true 2 --- inspect 9.3   5.6   310   .66  0     
ldv-regression/nested_structure_noptr_true-termination.c_true-unreach-call.i true 2 wit inspect .039 .038 5.9 .27 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .81 .49 43 0   0     error (invalid witness file) 0 --- inspect 5.1   2.8   270   .65  0     
ldv-regression/nested_structure_noptr_true-unreach-call_true-termination.i true 2 wit inspect .044 .043 5.7 .23 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .85 .51 43 0   0     error (invalid witness file) 0 --- inspect 5.4   2.9   250   .61  0     
ldv-regression/nested_structure_ptr_true-termination.c_true-unreach-call.i true 2 wit inspect .036 .035 6.1 .28 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .80 .48 42 0   0     error (invalid witness file) 0 --- inspect 6.4   3.7   260   .61  0     
ldv-regression/nested_structure_ptr_true-unreach-call_true-termination.i true 2 wit inspect .039 .040 6.3 .28 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .37 43 0   0     error (invalid witness file) 0 --- inspect 4.7   2.6   260   .61  0     
ldv-regression/nested_structure_true-termination.c_true-unreach-call.i true 2 wit inspect .042 .043 6.3 .25 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .85 .51 44 0   0     error (invalid witness file) 0 --- inspect 5.1   2.8   260   .65  0     
ldv-regression/nested_structure_true-unreach-call_true-termination.i true 2 wit inspect .044 .043 6.7 .24 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .83 .49 43 0   0     error (invalid witness file) 0 --- inspect 5.9   3.2   260   .61  0     
ldv-regression/oomInt_true-termination.c_true-unreach-call.i true 2 wit inspect .045 .044 5.8 .24 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .44 43 0   0     error (invalid witness file) 0 --- inspect 6.3   3.4   260   .61  0     
ldv-regression/oomInt_true-termination.c_true-unreach-call_1.i true 2 wit inspect .086 .082 5.5 .21 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .82 .49 43 0   0     error (invalid witness file) 0 --- inspect 6.7   3.9   270   .61  0     
ldv-regression/rule57_ebda_blast_true-termination.c_true-unreach-call_1.i true 2 wit inspect .096 .093 8.7 .42 .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .47 42 0   0     error (invalid witness file) 0 --- inspect 5.4   3.0   270   .65  0     
ldv-regression/rule60_list2_true-termination.c_true-unreach-call.i true 2 wit inspect .20  .20  15   2.4  .40   0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.6  3.1  260 0   0     true 2 --- inspect 24     15     690   .62  0     
ldv-regression/rule60_list_true-termination.c_true-unreach-call.i true 2 wit inspect .11  .11  7.3 .90 .066  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.8  3.1  280 0   0     true 2 --- inspect 14     8.3   390   .66  0     
ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i true 2 wit inspect .052 .049 7.0 .28 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .83 .50 44 0   0     error (invalid witness file) 0 --- inspect 6.2   3.6   270   .65  0     
ldv-regression/structure_assignment_true-termination.c_true-unreach-call.i true 2 wit inspect .041 .039 5.8 .23 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .47 43 0   0     error (invalid witness file) 0 --- inspect 5.1   2.8   270   .65  0     
ldv-regression/test_address_true-termination.c_true-unreach-call.i true 2 wit inspect .063 .060 6.2 .29 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 43 0   0     error (invalid witness file) 0 --- inspect 5.1   3.1   260   .61  3.6   
ldv-regression/test_cut_trace_true-termination.c_true-unreach-call.i true 2 wit inspect .052 .049 6.1 .25 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .38 44 0   0     error (invalid witness file) 0 --- inspect 6.0   3.3   270   .61  0     
ldv-regression/test_malloc-1_true-unreach-call_true-termination.i true 2 wit inspect .062 .061 7.7 .52 .016  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .46 42 0   0     error (invalid witness file) 0 --- inspect 6.7   3.8   260   .61  0     
ldv-regression/test_malloc-2_true-unreach-call_true-termination.i true 2 wit inspect .047 .048 7.4 .32 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .41 43 0   0     error (invalid witness file) 0 --- inspect 5.6   3.1   270   .61  0     
ldv-regression/test_overflow_true-termination.c_true-unreach-call.i true 2 wit inspect .052 .052 8.9 .41 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .88 .54 42 0   0     error (invalid witness file) 0 --- inspect 5.3   3.2   270   .61  3.6   
ldv-regression/test_union_cast-1_true-unreach-call_true-termination.i true 2 wit inspect .082 .082 5.6 .24 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 42 0   0     error (invalid witness file) 0 --- inspect 6.1   3.6   270   .65  0     
ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i true 2 wit inspect .083 .078 6.3 .31 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  250 0   0     true 2 --- inspect 9.1   5.4   310   .66  0     
ldv-regression/test_union_cast_true-termination.c_true-unreach-call.i true 2 wit inspect .042 .040 7.1 .39 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.0  250 0   0     true 2 --- inspect 8.5   4.7   310   .66  0     
ldv-regression/test_union_cast_true-termination.c_true-unreach-call_1.i true 2 wit inspect .040 .039 6.0 .25 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .42 42 0   0     error (invalid witness file) 0 --- inspect 6.7   4.0   270   .65  0     
ldv-regression/test_union_true-termination.c_true-unreach-call.i true 2 wit inspect .039 .039 6.8 .21 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .40 42 0   0     error (invalid witness file) 0 --- inspect 5.0   3.1   260   .61  0     
ldv-regression/test_union_true-termination.c_true-unreach-call_1.i true 2 wit inspect .087 .085 5.9 .18 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 42 0   0     error (invalid witness file) 0 --- inspect 5.1   3.2   260   .61  0     
ldv-regression/volatile_alias_true-termination.c_true-unreach-call.i true 2 wit inspect .034 .037 6.2 .52 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .47 43 0   0     error (invalid witness file) 0 --- inspect 5.3   2.9   270   .65  0     
ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i true 2 wit inspect .087 .082 5.7 .19 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 42 0   0     error (invalid witness file) 0 --- inspect 5.0   2.7   260   .61  0     
ldv-regression/test02_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .086 .074 8.6 .43 .0082 0      false(unreach-call) 1 wit inspect 3.7  2.1  250 0   0   false(unreach-call) 1 --- inspect 8.3   4.6   310   .66 0   false(unreach-call) 1 --- inspect 3.5  2.0  250 0   0    false(unreach-call) 1 --- inspect .57   .56   20    .045 .0041 - --- inspect - --- inspect
ldv-regression/test06_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .061 .054 9.4 .88 .0082 0      true -32 wit inspect 4.7  2.6  250 0   0   false(unreach-call) 1 --- inspect 7.9   4.4   310   .62 0   false(unreach-call) 1 --- inspect 3.6  2.1  250 0   4.6  error (2) 0 --- inspect .57   .57   20    .037 0      - --- inspect - --- inspect
ldv-regression/test08_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .065 .057 8.5 .51 .0082 0      true -32 wit inspect 3.7  2.0  250 0   0   false(unreach-call) 1 --- inspect 8.6   5.1   310   .66 0   false(unreach-call) 1 --- inspect 3.7  2.2  250 0   0    false(unreach-call) 1 --- inspect .57   .57   20    .045 0      - --- inspect - --- inspect
ldv-regression/test12_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .052 .045 9.2 .48 .0082 0      false(unreach-call) 1 wit inspect 3.7  2.0  250 0   0   false(unreach-call) 1 --- inspect 8.0   4.8   310   .62 0   false(unreach-call) 1 --- inspect 3.4  2.0  250 0   .37 false(unreach-call) 1 --- inspect .57   .57   20    .045 0      - --- inspect - --- inspect
ldv-regression/test21_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .065 .058 9.5 .60 .0082 0      false(unreach-call) 1 wit inspect 4.1  2.3  250 0   0   false(unreach-call) 1 --- inspect 7.8   4.8   310   .66 0   unknown 0 --- inspect 3.6  2.2  250 0   8.1  false(unreach-call) 1 --- inspect .60   .61   20    .057 0      - --- inspect - --- inspect
ldv-regression/test22_false-unreach-call.c false(unreach-call) 1 wit inspect .080 .070 9.5 .51 .0082 0      timeout 0 wit inspect 97    79    1300 0   0   false(unreach-call) 1 --- inspect 14     7.8   410   .66 0   unknown 0 --- inspect 4.0  2.3  250 0   .20 true -32 --- inspect .58   .58   20    .057 0      - --- inspect - --- inspect
ldv-regression/test23_false-unreach-call.c false(unreach-call) 0 wit inspect 1.3   1.3   14   17    .33   0      true -32 wit inspect 5.3  3.0  250 0   0   timeout 0 --- inspect 97     60     5900   1.7  0   unknown 0 --- inspect 3.8  2.2  240 0   .20 true -32 --- inspect .65   .65   21    .057 0      - --- inspect - --- inspect
ldv-regression/test24_false-unreach-call.c false(unreach-call) 0 wit inspect .97  .96  15   12    1.1    0      true -32 wit inspect 4.9  2.7  250 0   0   out of memory 0 --- inspect 66     43     7000   .65 0   unknown 0 --- inspect 4.3  2.5  250 0   4.4  error (2) 0 --- inspect .59   .59   21    .037 .0041 - --- inspect - --- inspect
ldv-regression/test25_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .66  .65  12   8.1  .44   0      true -32 wit inspect 5.6  3.1  250 0   0   false(unreach-call) 1 --- inspect 30     18     730   .62 0   unknown 0 --- inspect 4.0  2.3  250 0   0    error (2) 0 --- inspect .58   .58   21    .037 0      - --- inspect - --- inspect
ldv-regression/test26_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .056 .048 9.4 .56 .0082 0      false(unreach-call) 1 wit inspect 3.8  2.1  250 0   0   false(unreach-call) 1 --- inspect 8.2   4.5   320   .66 0   false(unreach-call) 1 --- inspect 3.5  2.0  250 0   0    false(unreach-call) 1 --- inspect .57   .57   20    .045 0      - --- inspect - --- inspect
ldv-regression/test27_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .31  .30  10   4.0  .21   0      true -32 wit inspect 4.2  2.4  250 0   0   false(unreach-call) 1 --- inspect 9.2   5.1   450   .66 0   unknown 0 --- inspect 4.2  2.4  260 0   .20 error (2) 0 --- inspect .62   .61   21    .061 .0041 - --- inspect - --- inspect
ldv-regression/test28_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .11  .088 7.5 .35 .0082 0      false(unreach-call) 1 wit inspect 4.0  2.2  250 0   0   false(unreach-call) 1 --- inspect 7.3   4.2   310   .62 0   true -32 --- inspect 3.6  2.1  250 0   .20 false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
ldv-regression/test29_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .073 .063 9.6 .41 .016  0      false(unreach-call) 1 wit inspect 4.5  2.5  250 0   0   false(unreach-call) 1 --- inspect 8.9   5.3   310   .66 0   unknown 0 --- inspect 3.6  2.1  250 0   0    false(unreach-call) 1 --- inspect .58   .58   20    .049 0      - --- inspect - --- inspect
ldv-regression/test30_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .069 .058 9.2 .66 .0082 0      true -32 wit inspect 4.2  2.3  260 0   0   false(unreach-call) 1 --- inspect 8.0   4.5   310   .66 0   false(unreach-call) 1 --- inspect 4.1  2.4  250 0   5.1  false(unreach-call) 1 --- inspect .56   .56   20    .049 0      - --- inspect - --- inspect
ldv-regression/test01_true-unreach-call_true-termination.c true 2 wit inspect .044 .042 6.6 .26 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .39 43 0   0     error (invalid witness file) 0 --- inspect 6.6   3.9   270   .65  0     
ldv-regression/test03_true-unreach-call_true-termination.c true 2 wit inspect .047 .045 6.3 .26 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 43 0   0     error (invalid witness file) 0 --- inspect 5.4   3.0   260   .61  0     
ldv-regression/test04_true-unreach-call_true-termination.c true 2 wit inspect .039 .040 6.9 .43 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .40 42 0   0     error (invalid witness file) 0 --- inspect 6.0   3.2   260   .61  0     
ldv-regression/test05_true-unreach-call_true-termination.c true 2 wit inspect .046 .044 6.9 .39 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .83 .51 44 0   0     error (invalid witness file) 0 --- inspect 5.2   2.8   260   .61  0     
ldv-regression/test07_true-unreach-call_true-termination.c true 2 wit inspect .041 .042 6.6 .31 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .40 44 0   0     error (invalid witness file) 0 --- inspect 6.4   3.7   270   .61  0     
ldv-regression/test09_true-unreach-call_true-termination.c true 2 wit inspect .074 .070 5.4 .29 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 43 0   0     error (invalid witness file) 0 --- inspect 5.4   2.9   270   .61  0     
ldv-regression/test10_true-unreach-call_true-termination.c true 2 wit inspect .045 .045 6.6 .32 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .49 42 0   0     error (invalid witness file) 0 --- inspect 7.1   4.1   270   .65  0     
ldv-regression/test11_true-unreach-call_true-termination.c true 2 wit inspect .072 .067 6.1 .31 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.4  260 0   0     true 2 --- inspect 8.0   5.0   310   .62  0     
ldv-regression/test13_true-unreach-call_true-termination.c true 2 wit inspect .038 .037 6.7 .32 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .48 42 0   0     error (invalid witness file) 0 --- inspect 6.2   3.7   260   .61  0     
ldv-regression/test14_true-unreach-call_true-termination.c true 2 wit inspect .044 .043 6.7 .34 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .83 .50 43 0   0     error (invalid witness file) 0 --- inspect 5.7   3.1   260   .61  0     
ldv-regression/test15_true-unreach-call_true-termination.c true 2 wit inspect .060 .057 6.7 .25 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.0  2.2  250 0   0     true 2 --- inspect 9.1   5.4   300   .62  0     
ldv-regression/test16_true-unreach-call_true-termination.c true 2 wit inspect .048 .048 6.2 .26 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 43 0   0     error (invalid witness file) 0 --- inspect 5.1   2.8   270   .61  0     
ldv-regression/test17_true-unreach-call_true-termination.c true 2 wit inspect .045 .044 6.6 .21 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 44 0   0     error (invalid witness file) 0 --- inspect 5.0   3.1   260   .61  0     
ldv-regression/test18_true-unreach-call_true-termination.c true 2 wit inspect .074 .071 6.3 .22 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .40 43 0   0     error (invalid witness file) 0 --- inspect 5.3   3.3   260   .65  0     
ldv-regression/test19_true-unreach-call_true-termination.c true 2 wit inspect .056 .053 6.2 .36 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.0  2.3  250 0   0     true 2 --- inspect 8.4   5.2   310   .62  0     
ldv-regression/test20_true-unreach-call_true-termination.c true 2 wit inspect .039 .038 6.4 .38 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 42 0   0     error (invalid witness file) 0 --- inspect 5.2   2.8   260   .61  0     
ldv-regression/test21_true-unreach-call_true-termination.c true 2 wit inspect .059 .056 6.7 .41 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.9  2.2  250 0   0     true 2 --- inspect 11     6.6   310   .62  0     
ldv-regression/test22_true-unreach-call.c true 2 wit inspect .58  .58  7.9 7.7  .31   0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 5.3  2.9  290 0   0     true 2 --- inspect 24     15     650   .66  0     
ldv-regression/test23_true-unreach-call.c true 2 wit inspect 1.3   1.3   13   21    .32   0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 6.4  3.6  290 0   0     true 2 --- inspect 42     30     670   .62  0     
ldv-regression/test24_true-unreach-call_true-termination.c true 2 wit inspect .96  .95  12   12    .27   0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 6.1  3.3  280 0   0     true 2 --- inspect 23     17     460   .66  0     
ldv-regression/test25_true-unreach-call.c true 2 wit inspect 1.6   1.6   12   20    .47   0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 14    8.0  440 0   .057 true 2 --- inspect 27     20     500   .62  0     
ldv-regression/test26_true-unreach-call_true-termination.c true 2 wit inspect .045 .044 6.2 .27 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .44 43 0   0     error (invalid witness file) 0 --- inspect 6.0   3.5   270   .65  0     
ldv-regression/test27_true-unreach-call_true-termination.c true 2 wit inspect .79  .79  13   11    .52   0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 19    13    510 0   0     true 2 --- inspect 90     76     820   .62  0     
ldv-regression/test28_true-unreach-call_true-termination.c true 2 wit inspect .062 .059 6.9 .37 .016  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.3  2.4  250 0   0     true 2 --- inspect 10     6.1   310   .62  0     
ldv-regression/test29_true-unreach-call_true-termination.c true 2 wit inspect .053 .051 6.5 .46 .016  0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.8  2.2  250 0   0     true 2 --- inspect 11     6.2   310   .66  .090 
ldv-regression/test30_true-unreach-call_true-termination.c true 2 wit inspect .040 .039 6.7 .29 .0082 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .42 42 0   0     error (invalid witness file) 0 --- inspect 5.2   3.3   270   .65  0     
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .27  .27  28   4.2  .012  0      error (invalid witness file) 0 --- inspect .76 .47 41 0   0   error (2) 0 --- inspect .021 .022 5.8 0    0   error (invalid witness file) 0 --- inspect .93 .62 47 0   0    error (invalid witness file) 0 --- inspect .0053 .0065 .40 0     0      - --- inspect - --- inspect
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .26  .26  28   3.2  .012  0      error (invalid witness file) 0 --- inspect .59 .36 41 0   0   error (2) 0 --- inspect .021 .022 5.7 0    0   error (invalid witness file) 0 --- inspect .95 .61 47 0   0    error (invalid witness file) 0 --- inspect .0047 .0054 .41 0     0      - --- inspect - --- inspect
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .26  .26  28   3.2  .012  0      error (invalid witness file) 0 --- inspect .76 .46 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect 1.1  .71 46 0   0    error (invalid witness file) 0 --- inspect .0058 .0070 .53 0     0      - --- inspect - --- inspect
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i out of memory 0 --- inspect 280     280     15000   3200    .037  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .47 40 0   0     error (2) 0 --- inspect .047 .049 5.5 0     0     
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i out of memory 0 --- inspect 280     280     15000   3400    .037  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .47 40 0   0     error (2) 0 --- inspect .021 .023 5.6 0     0     
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i out of memory 0 --- inspect 280     280     15000   3800    .037  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 40 0   0     error (2) 0 --- inspect .026 .027 5.6 0     0     
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i out of memory 0 --- inspect 280     280     15000   3300    .037  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .44 40 0   0     error (2) 0 --- inspect .022 .025 5.6 0     0     
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i out of memory 0 --- inspect 280     280     15000   3400    .037  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .41 41 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0     
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i out of memory 0 --- inspect 280     280     15000   3200    .037  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .46 41 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0     
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i out of memory 0 --- inspect 280     280     15000   4200    .037  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 41 0   0     error (2) 0 --- inspect .024 .025 5.6 0     0     
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i out of memory 0 --- inspect 280     280     15000   2800    .037  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .43 41 0   0     error (2) 0 --- inspect .025 .026 5.6 0     0     
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i out of memory 0 --- inspect 280     280     15000   3400    .037  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .40 40 0   0     error (2) 0 --- inspect .026 .027 5.5 0     0     
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i out of memory 0 --- inspect 280     280     15000   3100    .037  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .47 40 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0     
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .074 .074 7.8 .51 .020  0      error (invalid witness file) 0 --- inspect .59 .36 42 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .61 47 0   0    error (invalid witness file) 0 --- inspect .0063 .0079 .53 0     0      - --- inspect - --- inspect
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .064 .064 7.7 .89 .037  0      error (invalid witness file) 0 --- inspect .61 .38 40 0   0   error (2) 0 --- inspect .022 .022 5.5 0    0   error (invalid witness file) 0 --- inspect .93 .60 46 0   0    error (invalid witness file) 0 --- inspect .0056 .0068 .54 0     0      - --- inspect - --- inspect
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .087 .087 9.7 .78 .020  0      error (invalid witness file) 0 --- inspect .64 .38 40 0   0   error (2) 0 --- inspect .027 .029 5.7 0    0   error (invalid witness file) 0 --- inspect 1.2  .75 48 0   0    error (invalid witness file) 0 --- inspect .0058 .0074 .54 0     0      - --- inspect - --- inspect
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .077 .077 8.1 .78 .070  0      error (invalid witness file) 0 --- inspect .79 .49 41 0   0   error (2) 0 --- inspect .021 .022 5.7 0    0   error (invalid witness file) 0 --- inspect 1.0  .64 48 0   0    error (invalid witness file) 0 --- inspect .0048 .0059 .53 0     0      - --- inspect - --- inspect
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .085 .078 9.6 .90 .029  0      false(unreach-call) 1 wit inspect 4.8  2.6  250 0   0   error (7) 0 --- inspect 19     11     310   .75 0   unknown 0 --- inspect 4.1  2.4  250 0   0    error (1) 0 --- inspect .57   .57   20    .020 0      - --- inspect - --- inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect .066 .066 7.8 .50 .012  0      error (invalid witness file) 0 --- inspect .76 .46 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .61 46 0   0    error (invalid witness file) 0 --- inspect .0036 .0059 .54 0     0      - --- inspect - --- inspect
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .11  .11  14   1.3  .012  0      error (invalid witness file) 0 --- inspect .60 .36 41 0   0   error (2) 0 --- inspect .022 .026 5.6 0    0   error (invalid witness file) 0 --- inspect .95 .62 47 0   0    error (invalid witness file) 0 --- inspect .0042 .0054 .53 0     0      - --- inspect - --- inspect
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .12  .12  16   1.3  .012  0      error (invalid witness file) 0 --- inspect .78 .48 41 0   0   error (2) 0 --- inspect .026 .029 5.6 0    0   error (invalid witness file) 0 --- inspect .93 .61 46 0   0    error (invalid witness file) 0 --- inspect .0015 .0020 .53 0     0      - --- inspect - --- inspect
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .11  .10  9.4 .77 .061  0      false(unreach-call) 1 wit inspect 5.2  2.9  260 0   0   error (7) 0 --- inspect 15     8.7   310   .71 0   unknown 0 --- inspect 4.2  2.4  250 0   4.0  false(unreach-call) 1 --- inspect .62   .62   20    .070 0      - --- inspect - --- inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i error (134) 0 --- inspect .075 .076 8.3 .52 .020  0      error (invalid witness file) 0 --- inspect .66 .40 41 0   0   error (2) 0 --- inspect .020 .020 5.6 0    0   error (invalid witness file) 0 --- inspect .96 .62 49 0   0    error (invalid witness file) 0 --- inspect .0046 .019  .52 0     0      - --- inspect - --- inspect
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .074 .073 9.4 .79 .025  0      error (invalid witness file) 0 --- inspect .61 .36 42 0   0   error (2) 0 --- inspect .023 .024 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .61 48 0   0    error (invalid witness file) 0 --- inspect .0015 .0019 .54 0     0      - --- inspect - --- inspect
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .074 .074 7.4 .54 .029  0      error (invalid witness file) 0 --- inspect .59 .35 40 0   0   error (2) 0 --- inspect .021 .022 5.7 0    0   error (invalid witness file) 0 --- inspect 1.0  .65 48 0   0    error (invalid witness file) 0 --- inspect .0053 .0070 .53 0     0      - --- inspect - --- inspect
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .11  .11  9.5 .77 .020  0      error (invalid witness file) 0 --- inspect .70 .43 41 0   0   error (2) 0 --- inspect .023 .024 5.6 0    0   error (invalid witness file) 0 --- inspect .97 .66 48 0   0    error (invalid witness file) 0 --- inspect .0019 .0027 .53 0     0      - --- inspect - --- inspect
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .077 .076 8.1 .85 .066  0      error (invalid witness file) 0 --- inspect .79 .48 42 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .60 47 0   0    error (invalid witness file) 0 --- inspect .0061 .0078 .53 0     0      - --- inspect - --- inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .096 .087 9.2 .72 .029  0      false(unreach-call) 1 wit inspect 5.9  3.2  280 0   0   error (7) 0 --- inspect 15     8.6   310   .71 0   unknown 0 --- inspect 4.0  2.3  250 0   0    error (1) 0 --- inspect .59   .59   20    .020 0      - --- inspect - --- inspect
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .076 .076 7.9 .59 .025  0      error (invalid witness file) 0 --- inspect .78 .48 42 0   0   error (2) 0 --- inspect .022 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .91 .60 47 0   0    error (invalid witness file) 0 --- inspect .0050 .0066 .53 0     0      - --- inspect - --- inspect
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .14  .14  13   .89 .012  0      error (invalid witness file) 0 --- inspect .59 .38 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .61 48 0   0    error (invalid witness file) 0 --- inspect .0044 .0055 .54 0     0      - --- inspect - --- inspect
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .16  .16  16   1.4  .012  0      error (invalid witness file) 0 --- inspect .75 .46 42 0   0   error (2) 0 --- inspect .026 .027 5.6 0    0   error (invalid witness file) 0 --- inspect .95 .63 47 0   0    error (invalid witness file) 0 --- inspect .0058 .0068 .54 0     0      - --- inspect - --- inspect
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .092 .085 8.6 .81 .053  0      false(unreach-call) 1 wit inspect 4.5  2.5  250 0   0   error (7) 0 --- inspect 17     9.9   310   .75 0   unknown 0 --- inspect 4.3  2.5  250 0   0    false(unreach-call) 1 --- inspect .65   .65   20    .070 .025  - --- inspect - --- inspect
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .12  .12  8.0 .44 .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .48 40 0   0     error (2) 0 --- inspect .027 .028 5.5 0     0     
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .072 .071 7.9 .70 .037  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0     error (2) 0 --- inspect .026 .026 5.6 0     0     
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .094 .092 9.4 .88 .025  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .36 42 0   0     error (2) 0 --- inspect .021 .022 5.7 0     0     
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .081 .081 8.6 .98 .070  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 40 0   0     error (2) 0 --- inspect .029 .031 5.7 0     0     
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .072 .072 8.2 .74 .045  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .44 41 0   0     error (2) 0 --- inspect .021 .022 5.7 0     0     
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .081 .081 7.3 1.0  .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 40 0   0     error (2) 0 --- inspect .020 .021 5.6 0     0     
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .078 .077 9.5 .87 .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 41 0   0     error (2) 0 --- inspect .022 .022 5.6 0     0     
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect .14  .13  14   .84 .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0     
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .12  .12  17   1.4  .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 41 0   0     error (2) 0 --- inspect .022 .022 5.6 0     0     
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .081 .080 7.8 .71 .061  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 40 0   0     error (2) 0 --- inspect .025 .026 5.6 0     0     
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .064 .064 8.2 .70 .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .40 40 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0     
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .088 .087 8.8 .76 .025  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .42 40 0   0     error (2) 0 --- inspect .023 .024 5.8 0     0     
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .098 .096 7.7 .56 .029  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .49 41 0   0     error (2) 0 --- inspect .021 .021 5.6 0     0     
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .089 .088 9.6 .74 .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0     
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .082 .081 8.3 .91 .066  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0     error (2) 0 --- inspect .024 .025 5.6 0     0     
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .069 .068 7.8 .56 .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 41 0   0     error (2) 0 --- inspect .024 .025 5.6 0     0     
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .072 .072 7.7 .64 .025  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .66 .42 40 0   0     error (2) 0 --- inspect .020 .021 5.6 0     0     
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .090 .089 9.0 .71 .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0     error (2) 0 --- inspect .020 .021 5.6 0     0     
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i error (134) 0 --- inspect .10  .10  14   1.1  .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 40 0   0     error (2) 0 --- inspect .022 .023 5.6 0     0     
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .089 .089 11   .91 .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .36 42 0   0     error (2) 0 --- inspect .021 .021 5.6 0     0     
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .10  .10  7.3 .69 .057  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 41 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0     
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i error (134) 0 --- inspect .090 .088 10   .74 .012  0      error (invalid witness file) 0 --- inspect .64 .39 41 0   0   error (2) 0 --- inspect .021 .022 5.7 0    0   error (invalid witness file) 0 --- inspect .95 .62 47 0   0    error (invalid witness file) 0 --- inspect .0014 .0016 .40 0     0      - --- inspect - --- inspect
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i error (134) 0 --- inspect .080 .081 9.9 .90 .029  0      error (invalid witness file) 0 --- inspect .75 .45 40 0   0   error (2) 0 --- inspect .027 .027 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .63 47 0   0    error (invalid witness file) 0 --- inspect .0050 .0072 .52 0     0      - --- inspect - --- inspect
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup_true-termination.i false(unreach-call) 1 wit inspect .099 .089 9.3 .79 .012  0      false(unreach-call) 1 wit inspect 5.5  3.0  250 0   0   false(unreach-call) 1 --- inspect 8.3   5.0   310   .66 0   unknown 0 --- inspect 3.9  2.3  250 0   .39 false(unreach-call) 1 --- inspect .63   .62   20    .066 0      - --- inspect - --- inspect
list-ext2-properties/list_and_tree_cnstr_false-unreach-call_false-termination.i error (134) 0 --- inspect 1.8   1.7   280   22    .74   0      error (invalid witness file) 0 --- inspect .70 .43 40 0   0   error (2) 0 --- inspect .027 .028 5.6 0    0   error (invalid witness file) 0 --- inspect .97 .64 48 0   0    error (invalid witness file) 0 --- inspect .0056 .0068 .53 0     0      - --- inspect - --- inspect
list-ext2-properties/list_and_tree_cnstr_true-unreach-call_false-termination.i error (134) 0 --- inspect 1.7   1.7   280   25    .74   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 40 0   0     error (2) 0 --- inspect .023 .023 5.6 0     0     
list-ext2-properties/simple_and_skiplist_2lvl_false-unreach-call.i error (134) 0 --- inspect .18  .18  20   2.1  .14   0      error (invalid witness file) 0 --- inspect .68 .42 40 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .93 .60 47 0   0    error (invalid witness file) 0 --- inspect .0049 .0060 .53 0     0      - --- inspect - --- inspect
list-ext2-properties/simple_and_skiplist_2lvl_true-unreach-call.i error (134) 0 --- inspect .18  .18  19   2.1  .13   0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .48 40 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0     
list-ext2-properties/simple_search_value_false-unreach-call.i error (134) 0 --- inspect 19     19     1600   230    13      0      error (invalid witness file) 0 --- inspect .76 .46 41 0   0   error (2) 0 --- inspect .024 .025 5.7 0    0   error (invalid witness file) 0 --- inspect .96 .61 46 0   0    error (invalid witness file) 0 --- inspect .0048 .0053 .40 0     0      - --- inspect - --- inspect
list-ext2-properties/simple_search_value_true-unreach-call.i error (134) 0 --- inspect 19     19     1600   240    13      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .48 41 0   0     error (2) 0 --- inspect .027 .027 5.6 0     0     
ldv-sets/test_add_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .091 .082 9.3 .93 .012  0      false(unreach-call) 1 wit inspect 5.0  2.7  260 0   0   false(unreach-call) 1 --- inspect 9.3   5.2   320   .43 0   unknown 0 --- inspect 4.3  2.5  250 0   4.6  error (1) 0 --- inspect .59   .59   20    .020 0      - --- inspect - --- inspect
ldv-sets/test_mutex_double_lock_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .10  .095 9.4 1.2  .012  0      false(unreach-call) 1 wit inspect 5.4  3.0  260 0   0   false(unreach-call) 1 --- inspect 10     5.9   340   .66 0   unknown 0 --- inspect 4.6  2.6  260 0   .18 error (1) 0 --- inspect .56   .56   20    .020 0      - --- inspect - --- inspect
ldv-sets/test_mutex_double_unlock_false-unreach-call.i error (134) 0 --- inspect .092 .092 11   .92 .012  0      error (invalid witness file) 0 --- inspect .62 .39 42 0   0   error (2) 0 --- inspect .021 .021 5.6 0    0   error (invalid witness file) 0 --- inspect .94 .62 48 0   0    error (invalid witness file) 0 --- inspect .0017 .0024 .53 0     0      - --- inspect - --- inspect
ldv-sets/test_mutex_unbounded_false-unreach-call.i error (134) 0 --- inspect .097 .097 9.7 .98 .012  0      error (invalid witness file) 0 --- inspect .78 .48 41 0   0   error (2) 0 --- inspect .023 .023 5.6 0    0   error (invalid witness file) 0 --- inspect .96 .61 47 0   0    error (invalid witness file) 0 --- inspect .0042 .0074 .52 0     0      - --- inspect - --- inspect
ldv-sets/test_mutex_unlock_at_exit_false-unreach-call.i error (134) 0 --- inspect .11  .11  11   .85 .012  0      error (invalid witness file) 0 --- inspect .65 .40 41 0   0   error (2) 0 --- inspect .021 .022 5.6 0    0   error (invalid witness file) 0 --- inspect .95 .62 46 0   0    error (invalid witness file) 0 --- inspect .0054 .0064 .53 0     0      - --- inspect - --- inspect
ldv-sets/test_add_true-unreach-call_true-termination.i true 2 wit inspect .11  .10  8.6 .87 .045  0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 7.8  4.5  310 0   0     timeout 0 --- inspect 960     950     660   .68  0     
ldv-sets/test_mutex_true-unreach-call.i error (134) 0 --- inspect .13  .12  11   .84 .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .48 41 0   0     error (2) 0 --- inspect .020 .021 5.6 0     0     
ldv-sets/test_mutex_unbounded_true-unreach-call.i error (134) 0 --- inspect .092 .092 10   .95 .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .46 41 0   0     error (2) 0 --- inspect .023 .024 5.7 0     0     
list-simple/dll2c_append_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 600     600     11000   7100    1800      0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 18    13    550 0   0     timeout 0 --- inspect 960     940     730   1.6   0     
list-simple/dll2c_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 290     290     5400   3600    910      0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 16    11    570 0   0     timeout 0 --- inspect 960     940     760   1.6   0     
list-simple/dll2c_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 630     630     11000   7800    1900      0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 24    18    740 0   0     timeout 0 --- inspect 960     930     780   1.5   0     
list-simple/dll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 300     300     5500   4000    960      0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 27    21    860 0   0     timeout 0 --- inspect 960     930     680   1.6   0     
list-simple/dll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 600     600     11000   6600    1900      0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 17    12    550 0   0     timeout 0 --- inspect 960     950     630   1.6   3.5   
list-simple/dll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 290     290     5500   4000    940      0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 19    13    550 0   0     timeout 0 --- inspect 960     930     740   1.6   0     
list-simple/dll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .59  .59  14   7.3  1.9    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 35    29    880 0   0     true 2 --- inspect 250     230     720   .62  3.5   
list-simple/dll2c_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .55  .54  13   6.6  1.5    0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 14    9.9  560 0   0     timeout 0 --- inspect 960     950     530   1.5   0     
list-simple/dll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 250     250     4800   2900    920      .0041 - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 28    23    890 0   0     timeout 0 --- inspect 960     930     1700   1.5   0     
list-simple/dll2c_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 250     250     4800   3000    890      0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 28    21    760 0   0     true 2 --- inspect 76     55     690   .62  0     
list-simple/dll2n_append_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 580     580     12000   7400    860      0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 9.6  5.1  350 0   0     timeout 0 --- inspect 960     940     1300   .73  0     
list-simple/dll2n_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 600     600     13000   6400    870      0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 7.3  3.9  340 0   0     timeout 0 --- inspect 960     940     1000   .93  .0082
list-simple/dll2n_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 160     160     4700   1900    230      0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 9.0  4.9  310 0   .057 timeout 0 --- inspect 960     930     930   .79  0     
list-simple/dll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 160     160     4700   1800    240      0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 9.8  5.3  340 0   0     timeout 0 --- inspect 960     930     1300   1.6   .086 
list-simple/dll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 71     71     2200   890    110      0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 6.7  3.6  300 0   0     true 2 --- inspect 420     400     850   .62  0     
list-simple/dll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 70     70     2200   940    110      0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 7.6  4.1  290 0   0     timeout 0 --- inspect 960     930     750   1.7   0     
list-simple/dll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.0   8.0   76   120    47      0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 9.1  4.9  310 0   0     true 2 --- inspect 49     37     590   .62  0     
list-simple/dll2n_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .99  .98  22   14    3.9    0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 7.5  4.0  290 0   0     true 2 --- inspect 27     17     660   .62  .086 
list-simple/dll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 50     50     1600   620    100      0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 9.2  4.9  350 0   0     true 2 --- inspect 12     6.8   330   .66  0     
list-simple/dll2n_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 59     59     1900   670    110      0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 7.0  3.7  320 0   0     true 2 --- inspect 49     37     610   .62  0     
list-simple/sll2c_append_equal_true-unreach-call_true-valid-memsafety.i out of memory 0 --- inspect 270     270     15000   3800    920      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .35 41 0   0     error (2) 0 --- inspect .025 .026 5.6 0     0     
list-simple/sll2c_append_unequal_true-unreach-call_true-valid-memsafety.i out of memory 0 --- inspect 230     230     15000   3100    790      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .43 42 0   0     error (2) 0 --- inspect .027 .028 5.7 0     0     
list-simple/sll2c_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 560     560     11000   7900    1700      0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 20    14    670 0   0     timeout 0 --- inspect 960     910     910   1.5   0     
list-simple/sll2c_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 260     260     5300   3200    860      0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 25    20    910 0   0     timeout 0 --- inspect 960     920     710   .70  0     
list-simple/sll2c_prepend_equal_true-unreach-call_true-valid-memsafety.i out of memory 0 --- inspect 270     270     15000   3600    930      .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .39 40 0   0     error (2) 0 --- inspect .027 .027 5.6 0     0     
list-simple/sll2c_prepend_unequal_true-unreach-call_true-valid-memsafety.i out of memory 0 --- inspect 320     320     15000   4000    1100      0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .44 40 0   0     error (2) 0 --- inspect .021 .023 5.7 0     0     
list-simple/sll2c_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 340     340     2900   4100    1700      .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 130    120    2200 0   0     true 2 --- inspect 39     25     770   .62  0     
list-simple/sll2c_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.5   8.5   110   120    39      0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 16    11    570 0   0     timeout 0 --- inspect 960     950     560   1.5   0     
list-simple/sll2c_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 240     240     4700   3300    860      0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 28    22    1000 0   0     true 2 --- inspect 46     32     720   .62  .0082
list-simple/sll2c_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 230     230     4700   2700    860      0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 28    21    680 0   0     true 2 --- inspect 43     30     740   .62  0     
list-simple/sll2n_append_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 540     540     12000   6200    820      .0041 - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 20    13    660 0   0     timeout 0 --- inspect 960     930     1400   1.3   0     
list-simple/sll2n_append_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 570     570     12000   7200    820      0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 25    19    880 0   0     timeout 0 --- inspect 960     940     940   1.6   0     
list-simple/sll2n_insert_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 72     72     2300   860    120      0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 28    21    770 0   0     timeout 0 --- inspect 960     940     950   1.6   0     
list-simple/sll2n_insert_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 73     73     2300   840    120      0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 27    20    720 0   0     timeout 0 --- inspect 960     930     900   1.7   3.6   
list-simple/sll2n_prepend_equal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 68     68     2200   950    110      0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 22    15    570 0   0     timeout 0 --- inspect 960     930     710   .72  0     
list-simple/sll2n_prepend_unequal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 69     69     2200   710    110      0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 16    11    580 0   0     timeout 0 --- inspect 960     930     830   1.9   0     
list-simple/sll2n_remove_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 7.7   7.7   79   110    48      0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 14    9.3  540 0   0     true 2 --- inspect 98     82     970   .62  0     
list-simple/sll2n_remove_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .33  .32  11   4.0  .99   0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 7.4  4.1  290 0   0     true 2 --- inspect 32     25     680   .62  0     
list-simple/sll2n_update_all_reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 60     60     1900   740    120      0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 7.9  4.2  360 0   0     true 2 --- inspect 41     30     670   .62  3.7   
list-simple/sll2n_update_all_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 59     59     1900   670    120      0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 34    26    740 0   0     true 2 --- inspect 62     46     740   .62  0     
heap-data/calendar_true-unreach-call.i error (134) 0 --- inspect .075 .075 8.4 .74 .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .36 42 0   0     error (2) 0 --- inspect .030 .031 5.5 0     0     
heap-data/cart_true-unreach-call.i error (134) 0 --- inspect .061 .061 8.0 .63 .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0     
heap-data/hash_fun_true-unreach-call.i error (134) 0 --- inspect .069 .072 8.1 .62 .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 41 0   0     error (2) 0 --- inspect .027 .028 5.7 0     0     
heap-data/min_max_true-unreach-call.i error (134) 0 --- inspect .064 .063 7.8 .51 .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .71 .43 40 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0     
heap-data/packet_filter_true-unreach-call.i error (134) 0 --- inspect .070 .069 8.6 .64 .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .38 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0     0     
heap-data/process_queue_true-unreach-call.i out of memory 0 --- inspect 190     190     15000   2500    630      .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 41 0   0     error (2) 0 --- inspect .024 .026 5.8 0     0     
heap-data/quick_sort_split_true-unreach-call.i out of memory 0 --- inspect 790     790     15000   7900    1.5    0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .64 .39 42 0   0     error (2) 0 --- inspect .022 .022 5.6 0     0     
heap-data/running_example_true-unreach-call.i error (134) 0 --- inspect .075 .075 8.1 .57 .020  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .80 .49 41 0   0     error (2) 0 --- inspect .023 .023 5.6 0     0     
heap-data/shared_mem1_true-unreach-call.i error (134) 0 --- inspect .089 .088 9.3 1.4  .037  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .46 41 0   0     error (2) 0 --- inspect .021 .021 5.6 0     0     
heap-data/shared_mem2_true-unreach-call.i error (134) 0 --- inspect .074 .072 8.1 .63 .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .48 40 0   0     error (2) 0 --- inspect .027 .028 5.6 0     0     
list-ext3-properties/dll_nullified_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .64  .63  16   8.8  1.6    0      true -32 wit inspect 6.4  3.4  260 0   0   false(unreach-call) 1 --- inspect 16     9.1   520   .62 0   unknown 0 --- inspect 4.6  2.6  260 0   0    false(unreach-call) 1 --- inspect .66   .68   21    .074 0      - --- inspect - --- inspect
list-ext3-properties/sll_length_check_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .22  .21  9.6 2.9  .26   0      timeout 0 wit inspect 98    85    1600 0   0   false(unreach-call) 1 --- inspect 18     11     520   .66 0   unknown 0 --- inspect 4.8  2.7  260 0   4.8  false(unreach-call) 1 --- inspect .63   .63   21    .070 .016  - --- inspect - --- inspect
list-ext3-properties/sll_nondet_insert_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .83  .82  19   13    3.6    0      timeout 0 wit inspect 97    85    1800 0   0   false(unreach-call) 1 --- inspect 14     7.9   500   .62 0   unknown 0 --- inspect 4.9  2.8  260 0   0    false(unreach-call) 1 --- inspect .63   .63   21    .078 0      - --- inspect - --- inspect
list-ext3-properties/sll_of_sll_nondet_append_false-unreach-call_false-valid-memcleanup.i error (134) 0 --- inspect .14  .14  11   .98 .012  0      error (invalid witness file) 0 --- inspect .71 .46 41 0   0   error (2) 0 --- inspect .021 .022 5.7 0    0   error (invalid witness file) 0 --- inspect .96 .62 48 0   0    error (invalid witness file) 0 --- inspect .0049 .0065 .52 0     0      - --- inspect - --- inspect
list-ext3-properties/dll_circular_traversal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.3   4.3   130   56    10      0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 14    9.2  490 0   0     true 2 --- inspect 20     12     530   .62  0     
list-ext3-properties/dll_nullified_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     14000   11000    2000      .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 41 0   0     error (2) 0 --- inspect .027 .029 5.6 0     0     
list-ext3-properties/sll_circular_traversal_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 3.9   3.9   120   59    8.8    0      - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 7.9  4.3  320 0   0     timeout 0 --- inspect 960     930     920   1.6   0     
list-ext3-properties/sll_length_check_true-unreach-call_true-valid-memsafety.i out of memory 0 --- inspect 500     500     15000   7100    1100      .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 40 0   0     error (2) 0 --- inspect .037 .038 5.5 0     0     
list-ext3-properties/sll_nondet_insert_true-unreach-call_true-valid-memsafety.i out of memory 0 --- inspect 320     320     15000   3900    1300      .012  - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .80 .48 41 0   0     error (2) 0 --- inspect .021 .023 5.7 0     0     
list-ext3-properties/sll_of_sll_nondet_append_true-unreach-call_true-valid-memsafety.i error (134) 0 --- inspect .10  .10  12   1.1  .012  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .78 .48 41 0   0     error (2) 0 --- inspect .024 .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 233 20000   20000   580000 240000 40000   .057 75 -331 470 350 15000 0   0   75 27 620 400 25000 24 0   75 -19 180   110   11000 0   48    75 -40 21   21   730 1.8  .066 166 28 990 700 33000 0   .11 166 66 26000 24000 53000 80 26  
    correct results 133 233 8200   8200   170000 100000 21000   .012 21 21 98 54 5400 0   0   27 27 280 160 9700 17 0   13 13 48   28   3200 0   10    24 24 14   15   490 1.4  .057 14 28 240 190 6500 0   0    33 66 2200 1900 20000 21 7.4
        correct true 100 200 8200   8200   170000 100000 21000   .012 0 0 0 0 14 28 240 190 6500 0   0    33 66 2200 1900 20000 21 7.4
        correct false 33 33 6.6 6.3 400 73 11   0     21 21 98 54 5400 0   0   27 27 280 160 9700 17 0   13 13 48   28   3200 0   10    24 24 14   15   490 1.4  .057 0 0
    correct-unconfimed results 2 0 2.2 2.2 29 29 1.4 0     0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 2 0 2.2 2.2 29 29 1.4 0     0 0 0 0 0 0
    incorrect results 0 11 -352 51 28 2800 0   0   0 1 -32 3.6 2.1 250 0   .20 2 -64 1.2 1.2 41 .11 0     0 0
        incorrect true 0 11 -352 51 28 2800 0   0   0 1 -32 3.6 2.1 250 0   .20 2 -64 1.2 1.2 41 .11 0     0 0
        incorrect false 0 0 0 0 0 0 0
score (241 tasks, max score: 407) 233 -331 27 -19 -40 28 66
Run set cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Heap cpa-seq-validate-violation-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Heap uautomizer-validate-violation-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Heap uautomizer-validate-correctness-witnesses-cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Heap