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 ---