Tool CBMC CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a CPA-witness2test 1.7-svn 29852 CProver witness2test 0.1 CPAchecker 1.7-svn 29852 ULTIMATE Automizer 0.1.23-635dfa2a
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-04 22:48:40 CET 2018-12-06 08:59:15 CET 2018-12-06 10:10:50 CET 2018-12-06 10:22:39 CET 2018-12-12 19:29:48 CET 2018-12-06 07:35:27 CET 2018-12-06 09:23:57 CET
Run set cbmc.sv-comp19_prop-reachsafety.ReachSafety-Heap cpa-seq-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Heap uautomizer-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Heap uautomizer-validate-correctness-witnesses-cbmc.sv-comp19_prop-reachsafety.ReachSafety-Heap
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const -witness ../../results-verified/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true -witness ../../results-verified/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/cbmc.2018-12-04_2248.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) wall (s) mem (MB) energy (J) blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB) status score witness inspect witness cpu (s) wall (s) mem (MB) energy blkio-w (MB) blkio-r (MB)
heap-manipulation/bubble_sort_linux_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .21  .20  16   2.3  .012  0     false(unreach-call) 1 wit inspect 6.2 3.4 270 0   0     error (7) 0 --- inspect 20   12   340 .75 0   unknown 0 --- inspect 5.9 3.4 260 0   4.5   false(unreach-call) 1 --- inspect .68 .67 21 .11  0      - --- inspect - --- inspect
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .23  .22  13   3.1  .012  0     true -32 wit inspect 7.0 3.8 270 0   0     error (7) 0 --- inspect 22   13   330 .71 0   unknown 0 --- inspect 7.0 3.9 290 0   0     true -32 --- inspect .66 .66 21 .094 0      - --- inspect - --- inspect
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .25  .24  20   3.5  .012  0     false(unreach-call) 1 wit inspect 6.2 3.4 260 0   0     error (7) 0 --- inspect 17   9.5 310 .75 0   unknown 0 --- inspect 4.5 2.6 250 0   0     false(unreach-call) 1 --- inspect .63 .63 20 .082 0      - --- inspect - --- inspect
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .19  .18  13   2.3  .012  0     false(unreach-call) 1 wit inspect 7.5 4.4 280 0   0     error (7) 0 --- inspect 17   9.5 310 .75 0   unknown 0 --- inspect 4.9 2.8 260 0   0     false(unreach-call) 1 --- inspect .64 .64 21 .082 0      - --- inspect - --- inspect
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .17  .16  12   1.9  .012  0     false(unreach-call) 1 wit inspect 6.2 3.4 260 0   0     error (7) 0 --- inspect 16   9.9 310 .75 0   unknown 0 --- inspect 4.4 2.6 250 0   0     false(unreach-call) 1 --- inspect .63 .63 21 .074 0      - --- inspect - --- inspect
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .17  .16  12   2.3  .012  0     false(unreach-call) 1 wit inspect 5.1 2.8 260 0   0     error (7) 0 --- inspect 15   8.8 320 .75 0   unknown 0 --- inspect 4.5 2.5 250 0   .20  false(unreach-call) 1 --- inspect .63 .63 21 .074 0      - --- inspect - --- inspect
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     3500   7600    .73   0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 41 0   0     error (2) 0 --- inspect .021 .021 5.6 0    0  
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i error (42) 0 --- inspect 880     880     490   9300    1.5    0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .60 .37 40 0   0     error (2) 0 --- inspect .022 .024 5.6 0    0  
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     1300   6700    .95   0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .46 41 0   0     error (2) 0 --- inspect .022 .023 5.6 0    0  
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i out of memory 0 --- inspect 180     180     13000   2100    3.9    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/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     4300   14000    1.1    0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .45 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0  
heap-manipulation/tree_true-unreach-call.i error (42) 0 --- inspect 880     880     1400   10000    6.8    0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .67 .42 40 0   0     error (2) 0 --- inspect .024 .025 5.6 0    0  
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .097 .088 9.4 .89 .012  0     false(unreach-call) 1 wit inspect 5.4 3.0 250 0   0     false(unreach-call) 1 --- inspect 8.3 4.7 310 .62 0   unknown 0 --- inspect 4.4 2.5 270 0   0     false(unreach-call) 1 --- inspect .65 .65 20 .066 0      - --- inspect - --- inspect
list-properties/list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .17  .16  9.5 1.0  .012  0     false(unreach-call) 1 wit inspect 4.9 2.7 260 0   0     false(unreach-call) 1 --- inspect 11   6.3 320 .66 0   unknown 0 --- inspect 4.4 2.5 250 0   .20  false(unreach-call) 1 --- inspect .64 .64 20 .066 0      - --- inspect - --- inspect
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .083 .073 9.9 .96 .012  0     false(unreach-call) 1 wit inspect 4.5 2.4 260 0   0     false(unreach-call) 1 --- inspect 8.4 4.9 310 .66 0   unknown 0 --- inspect 4.1 2.4 250 0   0     false(unreach-call) 1 --- inspect .62 .62 20 .066 0      - --- inspect - --- inspect
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .20  .19  9.9 1.5  .053  0     false(unreach-call) 1 wit inspect 5.3 2.9 260 0   0     timeout (false(unreach-call)) 0 --- inspect 93   83   560 .62 0   unknown 0 --- inspect 4.5 2.6 250 0   0     false(unreach-call) 1 --- inspect .62 .62 21 .070 0      - --- inspect - --- inspect
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .083 .076 9.9 .82 .012  0     false(unreach-call) 1 wit inspect 5.3 2.9 270 0   0     false(unreach-call) 1 --- inspect 9.7 5.3 310 .66 0   unknown 0 --- inspect 4.1 2.4 250 0   0     false(unreach-call) 1 --- inspect .62 .62 20 .066 0      - --- inspect - --- inspect
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .099 .089 9.7 .88 .012  0     false(unreach-call) 1 wit inspect 5.6 3.1 260 0   0     false(unreach-call) 1 --- inspect 8.7 5.2 310 .66 0   unknown 0 --- inspect 4.2 2.5 250 0   0     error (2) 0 --- inspect .62 .62 21 .049 0      - --- inspect - --- inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i error (42) 0 --- inspect 880     880     4000   8900    12      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .38 40 0   0     error (2) 0 --- inspect .025 .025 5.6 0    0  
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i error (6) 0 --- inspect 830     830     13000   10000    10      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .46 41 0   0     error (2) 0 --- inspect .020 .021 5.7 0    0  
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i true 2 wit inspect .17  .16  7.7 2.1  .070  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 21    12    630 0   0     true 2 --- inspect 560     520     1400   .68 0  
list-properties/list_true-unreach-call_false-valid-memtrack.i error (42) 0 --- inspect 880     880     6400   13000    .95   0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .69 .41 41 0   0     error (2) 0 --- inspect .027 .028 5.6 0    0  
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i error (42) 0 --- inspect 880     880     3900   9600    55      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 41 0   0     error (2) 0 --- inspect .023 .023 5.6 0    0  
list-properties/simple_true-unreach-call_false-valid-memtrack.i error (42) 0 --- inspect 880     880     3300   11000    5.7    0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .74 .45 41 0   0     error (2) 0 --- inspect .026 .027 5.6 0    0  
list-properties/splice_true-unreach-call_false-valid-memtrack.i error (42) 0 --- inspect 880     880     1700   14000    1.4    0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .38 41 0   0     error (2) 0 --- inspect .028 .029 5.6 0    0  
ldv-regression/1_3_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .076 .067 9.8 .56 .012  0     false(unreach-call) 1 wit inspect 5.0 2.7 250 0   0     false(unreach-call) 1 --- inspect 8.6 4.8 310 .12 0   false(unreach-call) 1 --- inspect 3.6 2.1 250 0   .033 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 .090 .082 9.2 .86 .012  0     false(unreach-call) 1 wit inspect 4.7 2.6 260 0   0     false(unreach-call) 1 --- inspect 11   6.2 340 .66 0   unknown 0 --- inspect 4.4 2.5 260 0   .11  false(unreach-call) 1 --- inspect .64 .64 20 .086 0      - --- inspect - --- inspect
ldv-regression/callfpointer_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .057 .048 9.3 .48 .0082 0     false(unreach-call) 1 wit inspect 4.7 2.6 250 0   0     false(unreach-call) 1 --- inspect 7.3 4.0 310 .66 0   false(unreach-call) 1 --- inspect 3.6 2.0 250 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 false(unreach-call) 1 wit inspect .13  .12  9.6 .91 .012  0     unknown 0 wit inspect 4.5 2.5 260 0   0     unknown 0 --- inspect 16   9.5 330 .71 0   unknown 0 --- inspect 4.1 2.4 250 0   .094 false(unreach-call) 1 --- inspect .66 .66 20 .074 0      - --- inspect - --- inspect
ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .10  .090 9.5 .35 .0082 0     true -32 wit inspect 3.8 2.1 250 0   0     false(unreach-call) 1 --- inspect 7.4 4.2 320 .66 0   false(unreach-call) 1 --- inspect 3.7 2.2 250 0   0     false(unreach-call) 1 --- inspect .58 .58 20 .049 0      - --- inspect - --- inspect
ldv-regression/mutex_lock_struct_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .059 .049 9.8 .50 .0082 0     false(unreach-call) 1 wit inspect 4.8 2.7 250 0   0     false(unreach-call) 1 --- inspect 7.0 4.0 310 .62 0   false(unreach-call) 1 --- inspect 3.7 2.2 250 0   0     false(unreach-call) 1 --- inspect .56 .56 20 .045 0      - --- inspect - --- inspect
ldv-regression/recursive_list_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .086 .074 9.5 .56 .012  0     false(unreach-call) 1 wit inspect 5.0 2.7 260 0   0     false(unreach-call) 1 --- inspect 7.7 4.6 310 .66 0   false(unreach-call) 1 --- inspect 4.0 2.3 240 0   0     error (2) 0 --- inspect .58 .58 20 .037 0      - --- inspect - --- inspect
ldv-regression/rule57_ebda_blast_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .078 .070 9.8 .65 .012  0     false(unreach-call) 1 wit inspect 4.2 2.3 250 0   0     false(unreach-call) 1 --- inspect 8.3 5.2 310 .62 0   unknown 0 --- inspect 4.1 2.4 250 0   .23  false(unreach-call) 1 --- inspect .60 .61 20 .070 0      - --- inspect - --- inspect
ldv-regression/rule60_list2_true-termination.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect .079 .068 8.5 .63 .0082 0     true -32 wit inspect 8.2 4.4 270 0   0     false(unreach-call) 1 --- inspect 15   9.2 470 .62 0   exception 0 --- inspect 4.4 2.5 250 0   .13  error (2) 0 --- inspect .64 .64 20 .049 0      - --- inspect - --- inspect
ldv-regression/stateful_check_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect .15  .14  9.4 1.1  .037  0     false(unreach-call) 1 wit inspect 8.2 4.4 280 0   0     false(unreach-call) 1 --- inspect 8.6 4.7 310 .66 0   unknown 0 --- inspect 4.7 2.7 250 0   0     false(unreach-call) 1 --- inspect .59 .59 20 .057 0      - --- inspect - --- inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .086 .074 9.5 .58 .020  0     false(unreach-call) 1 wit inspect 3.7 2.1 250 0   0     false(unreach-call) 1 --- inspect 6.2 3.6 290 .66 0   false(unreach-call) 1 --- inspect 3.9 2.2 250 0   0     false(unreach-call) 1 --- inspect .59 .59 20 .045 .012  - --- inspect - --- inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect .074 .064 10   .51 .016  0     false(unreach-call) 1 wit inspect 4.7 2.6 250 0   0     false(unreach-call) 1 --- inspect 9.0 5.1 310 .66 0   false(unreach-call) 1 --- inspect 3.5 2.1 250 0   0     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 .053 .050 6.9 .34 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  250 0   0     true 2 --- inspect 9.2   5.1   310   .66 0  
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i true 2 wit inspect .049 .045 7.5 .29 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.0  250 0   0     true 2 --- inspect 8.7   5.1   310   .62 0  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call.i true 2 wit inspect .043 .041 6.6 .38 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.8  2.1  250 0   0     true 2 --- inspect 8.6   5.2   300   .62 0  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call_1.i true 2 wit inspect .065 .061 6.0 .35 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  250 0   0     true 2 --- inspect 9.3   5.2   300   .66 0  
ldv-regression/ex3_forlist_true-termination.c_true-unreach-call.i true 2 wit inspect .11  .11  6.2 .50 .033  0     - --- inspect - --- inspect - --- inspect - --- inspect assertion 0 --- inspect 3.9  2.2  250 0   0     true 2 --- inspect 100     83     840   .62 0  
ldv-regression/just_assert_true-termination.c_true-unreach-call.i true 2 wit inspect .052 .050 7.1 .29 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.0  2.3  250 0   0     true 2 --- inspect 7.8   4.3   300   .66 0  
ldv-regression/mutex_lock_int_true-termination.c_true-unreach-call_1.i true 2 wit inspect .078 .073 6.2 .26 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  2.0  250 0   0     true 2 --- inspect 11     6.1   310   .66 0  
ldv-regression/mutex_lock_struct_true-termination.c_true-unreach-call_1.i true 2 wit inspect .049 .045 6.4 .37 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.9  2.1  250 0   0     true 2 --- inspect 8.3   5.2   310   .66 0  
ldv-regression/nested_structure_noptr_true-termination.c_true-unreach-call.i true 2 wit inspect .047 .044 6.5 .36 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.4  250 0   0     true 2 --- inspect 8.4   5.0   310   .66 0  
ldv-regression/nested_structure_noptr_true-unreach-call_true-termination.i true 2 wit inspect .044 .041 6.6 .31 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.8  2.1  250 0   0     true 2 --- inspect 8.6   4.9   310   .66 0  
ldv-regression/nested_structure_ptr_true-termination.c_true-unreach-call.i true 2 wit inspect .076 .069 6.7 .25 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.1  2.3  250 0   0     true 2 --- inspect 8.1   4.5   300   .62 0  
ldv-regression/nested_structure_ptr_true-unreach-call_true-termination.i true 2 wit inspect .043 .041 7.7 .37 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.3  2.5  250 0   0     true 2 --- inspect 9.5   5.7   310   .66 0  
ldv-regression/nested_structure_true-termination.c_true-unreach-call.i true 2 wit inspect .049 .047 6.3 .67 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.0  2.2  250 0   0     true 2 --- inspect 7.2   4.1   310   .66 0  
ldv-regression/nested_structure_true-unreach-call_true-termination.i true 2 wit inspect .048 .046 7.0 .32 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.2  2.3  250 0   0     true 2 --- inspect 9.2   5.2   310   .66 0  
ldv-regression/oomInt_true-termination.c_true-unreach-call.i true 2 wit inspect .040 .037 7.3 .16 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.4  250 0   0     true 2 --- inspect 7.7   4.4   310   .66 0  
ldv-regression/oomInt_true-termination.c_true-unreach-call_1.i true 2 wit inspect .043 .040 6.6 .40 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.3  2.4  250 0   0     true 2 --- inspect 8.5   4.8   310   .66 0  
ldv-regression/rule57_ebda_blast_true-termination.c_true-unreach-call_1.i true 2 wit inspect .074 .071 7.5 .61 .016  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.4  260 0   0     true 2 --- inspect 11     6.2   330   .66 0  
ldv-regression/rule60_list2_true-termination.c_true-unreach-call.i true 2 wit inspect .056 .054 6.4 .50 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.3  2.4  260 0   0     true 2 --- inspect 27     17     680   .66 0  
ldv-regression/rule60_list_true-termination.c_true-unreach-call.i true 2 wit inspect .11  .10  7.0 .62 .016  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.7  2.6  260 0   0     true 2 --- inspect 15     8.6   390   .66 0  
ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i true 2 wit inspect .053 .051 6.9 .57 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.0  2.2  250 0   0     true 2 --- inspect 9.5   5.3   310   .66 0  
ldv-regression/structure_assignment_true-termination.c_true-unreach-call.i true 2 wit inspect .044 .042 6.4 .39 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.9  2.2  250 0   0     true 2 --- inspect 8.6   5.1   310   .62 0  
ldv-regression/test_address_true-termination.c_true-unreach-call.i true 2 wit inspect .069 .065 6.4 .31 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.1  2.8  250 0   0     true 2 --- inspect 10     5.9   320   .66 0  
ldv-regression/test_cut_trace_true-termination.c_true-unreach-call.i true 2 wit inspect .051 .048 7.2 .32 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.1  2.3  250 0   0     true 2 --- inspect 8.1   4.8   300   .66 0  
ldv-regression/test_malloc-1_true-unreach-call_true-termination.i true 2 wit inspect .12  .11  6.7 .42 .016  0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.2  2.3  250 0   0     true 2 --- inspect 10     6.0   310   .66 0  
ldv-regression/test_malloc-2_true-unreach-call_true-termination.i true 2 wit inspect .075 .069 6.5 .34 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.0  2.2  250 0   0     true 2 --- inspect 11     6.1   310   .66 0  
ldv-regression/test_overflow_true-termination.c_true-unreach-call.i true 2 wit inspect .058 .055 7.6 .56 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.4  3.0  260 0   0     true 2 --- inspect 12     6.7   330   .66 0  
ldv-regression/test_union_cast-1_true-unreach-call_true-termination.i true 2 wit inspect .046 .043 6.3 .28 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  1.9  250 0   0     true 2 --- inspect 7.5   4.3   310   .66 0  
ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i true 2 wit inspect .050 .047 6.5 .27 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  1.9  250 0   0     true 2 --- inspect 8.1   4.9   300   .66 0  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call.i true 2 wit inspect .044 .041 7.1 .34 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.1  240 0   0     true 2 --- inspect 8.8   5.2   310   .66 0  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call_1.i true 2 wit inspect .048 .045 6.7 .34 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.8  2.1  250 0   0     true 2 --- inspect 8.4   5.0   300   .66 0  
ldv-regression/test_union_true-termination.c_true-unreach-call.i true 2 wit inspect .052 .048 6.6 .30 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.2  2.3  250 0   0     true 2 --- inspect 8.6   5.1   300   .66 0  
ldv-regression/test_union_true-termination.c_true-unreach-call_1.i true 2 wit inspect .048 .045 7.8 .29 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  250 0   0     true 2 --- inspect 6.8   4.3   300   .66 0  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call.i true 2 wit inspect .047 .044 6.8 .33 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.0  2.2  250 0   0     true 2 --- inspect 8.7   4.8   300   .66 0  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i true 2 wit inspect .050 .048 6.9 .27 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.4  250 0   0     true 2 --- inspect 9.2   5.4   310   .66 0  
ldv-regression/test02_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .061 .053 9.2 .55 .0082 0     false(unreach-call) 1 wit inspect 4.3 2.4 250 0   0     false(unreach-call) 1 --- inspect 7.0 4.4 300 .66 0   false(unreach-call) 1 --- inspect 3.7 2.1 250 0   0     false(unreach-call) 1 --- inspect .59 .58 20 .045 0      - --- inspect - --- inspect
ldv-regression/test06_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .069 .059 9.9 .53 .0082 0     true -32 wit inspect 4.6 2.6 250 0   0     false(unreach-call) 1 --- inspect 7.2 4.1 310 .62 0   false(unreach-call) 1 --- inspect 3.7 2.2 250 0   .012 error (2) 0 --- inspect .57 .57 20 .037 .0041 - --- inspect - --- inspect
ldv-regression/test08_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .14  .12  8.6 .43 .0082 0     false(unreach-call) 1 wit inspect 3.8 2.1 260 0   0     false(unreach-call) 1 --- inspect 7.4 4.6 310 .66 0   false(unreach-call) 1 --- inspect 3.6 2.1 250 0   0     false(unreach-call) 1 --- inspect .60 .60 20 .045 0      - --- inspect - --- inspect
ldv-regression/test12_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .072 .062 9.6 .41 .0082 0     false(unreach-call) 1 wit inspect 4.7 2.6 250 0   0     false(unreach-call) 1 --- inspect 7.4 4.1 310 .66 0   false(unreach-call) 1 --- inspect 3.6 2.1 250 0   0     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 .12  .11  10   .37 .0082 0     false(unreach-call) 1 wit inspect 4.7 2.6 250 0   0     false(unreach-call) 1 --- inspect 8.2 4.6 300 .66 0   unknown 0 --- inspect 3.9 2.3 250 0   0     false(unreach-call) 1 --- inspect .58 .58 20 .057 .0041 - --- inspect - --- inspect
ldv-regression/test22_false-unreach-call.c false(unreach-call) 1 wit inspect .077 .067 9.8 .59 .0082 0     false(unreach-call) 1 wit inspect 4.6 2.6 260 0   0     false(unreach-call) 1 --- inspect 11   6.5 400 .66 0   unknown 0 --- inspect 3.8 2.2 250 0   .21  true -32 --- inspect .61 .60 20 .057 0      - --- inspect - --- inspect
ldv-regression/test23_false-unreach-call.c false(unreach-call) 1 wit inspect .41  .40  12   5.2  .053  0     false(unreach-call) 1 wit inspect 5.6 3.1 260 0   0     timeout 0 --- inspect 97   61   5400 .76 0   unknown 0 --- inspect 4.1 2.4 250 0   0     true -32 --- inspect .62 .62 20 .057 0      - --- inspect - --- inspect
ldv-regression/test24_false-unreach-call.c false(unreach-call) 1 wit inspect .37  .36  16   4.7  .16   0     false(unreach-call) 1 wit inspect 5.0 2.8 270 0   0     out of memory 0 --- inspect 71   45   7000 .66 0   unknown 0 --- inspect 4.3 2.5 250 0   .20  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 .17  .16  10   1.9  .074  0     false(unreach-call) 1 wit inspect 5.7 3.2 280 0   0     false(unreach-call) 1 --- inspect 35   20   600 .62 0   unknown 0 --- inspect 4.4 2.5 250 0   0     error (2) 0 --- inspect .59 .59 21 .037 0      - --- inspect - --- inspect
ldv-regression/test26_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .063 .054 9.5 .59 .0082 0     false(unreach-call) 1 wit inspect 4.8 2.6 250 0   0     false(unreach-call) 1 --- inspect 7.2 4.4 310 .66 0   false(unreach-call) 1 --- inspect 3.6 2.1 250 0   0     false(unreach-call) 1 --- inspect .56 .56 20 .045 0      - --- inspect - --- inspect
ldv-regression/test27_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .23  .22  11   2.4  .078  0     false(unreach-call) 1 wit inspect 5.6 3.2 270 0   0     false(unreach-call) 1 --- inspect 12   6.7 520 .66 0   unknown 0 --- inspect 4.3 2.5 250 0   0     error (2) 0 --- inspect .60 .60 20 .037 0      - --- inspect - --- inspect
ldv-regression/test28_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .059 .050 9.5 .59 .0082 0     false(unreach-call) 1 wit inspect 5.1 2.8 250 0   0     false(unreach-call) 1 --- inspect 8.6 4.8 320 .66 0   true -32 --- inspect 3.6 2.1 250 0   0     false(unreach-call) 1 --- inspect .59 .59 20 .049 0      - --- inspect - --- inspect
ldv-regression/test29_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .075 .065 10   .48 .0082 0     false(unreach-call) 1 wit inspect 5.1 2.8 250 0   0     false(unreach-call) 1 --- inspect 8.9 5.3 320 .66 0   unknown 0 --- inspect 3.8 2.2 250 0   0     false(unreach-call) 1 --- inspect .59 .60 20 .049 0      - --- inspect - --- inspect
ldv-regression/test30_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .058 .049 10   .47 .0082 0     true -32 wit inspect 4.0 2.2 260 0   0     false(unreach-call) 1 --- inspect 7.0 4.0 310 .62 0   false(unreach-call) 1 --- inspect 3.7 2.1 240 0   0     false(unreach-call) 1 --- inspect .59 .59 20 .049 0      - --- inspect - --- inspect
ldv-regression/test01_true-unreach-call_true-termination.c true 2 wit inspect .048 .045 6.8 .36 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  1.9  250 0   0     true 2 --- inspect 7.9   4.5   310   .62 0  
ldv-regression/test03_true-unreach-call_true-termination.c true 2 wit inspect .11  .099 6.4 .25 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  250 0   0     true 2 --- inspect 9.7   5.7   310   .66 0  
ldv-regression/test04_true-unreach-call_true-termination.c true 2 wit inspect .050 .047 7.5 .32 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  260 0   0     true 2 --- inspect 10     5.9   310   .66 0  
ldv-regression/test05_true-unreach-call_true-termination.c true 2 wit inspect .047 .047 7.1 .48 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.1  250 0   0     true 2 --- inspect 12     7.2   330   .66 0  
ldv-regression/test07_true-unreach-call_true-termination.c true 2 wit inspect .052 .049 6.6 .36 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  1.9  250 0   0     true 2 --- inspect 11     6.7   320   .66 0  
ldv-regression/test09_true-unreach-call_true-termination.c true 2 wit inspect .050 .047 6.7 .44 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.7  2.6  260 0   0     true 2 --- inspect 9.5   5.8   310   .62 0  
ldv-regression/test10_true-unreach-call_true-termination.c true 2 wit inspect .12  .11  6.1 .27 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  260 0   0     true 2 --- inspect 14     8.4   440   .62 0  
ldv-regression/test11_true-unreach-call_true-termination.c true 2 wit inspect .056 .054 6.5 .39 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.4  260 0   0     true 2 --- inspect 10     6.1   310   .66 0  
ldv-regression/test13_true-unreach-call_true-termination.c true 2 wit inspect .055 .053 6.9 .39 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.1  250 0   0     true 2 --- inspect 9.7   5.6   310   .66 0  
ldv-regression/test14_true-unreach-call_true-termination.c true 2 wit inspect .057 .055 6.5 .38 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  260 0   0     true 2 --- inspect 9.4   5.2   310   .62 0  
ldv-regression/test15_true-unreach-call_true-termination.c true 2 wit inspect .058 .055 7.9 .32 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.1  2.3  250 0   0     true 2 --- inspect 7.5   4.3   310   .66 0  
ldv-regression/test16_true-unreach-call_true-termination.c true 2 wit inspect .049 .046 7.2 .37 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.1  250 0   0     true 2 --- inspect 7.6   4.4   300   .62 0  
ldv-regression/test17_true-unreach-call_true-termination.c true 2 wit inspect .053 .050 7.4 .30 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  1.9  250 0   0     true 2 --- inspect 7.3   4.2   300   .62 0  
ldv-regression/test18_true-unreach-call_true-termination.c true 2 wit inspect .11  .10  6.2 .26 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.0  250 0   0     true 2 --- inspect 9.8   5.9   310   .66 0  
ldv-regression/test19_true-unreach-call_true-termination.c true 2 wit inspect .047 .044 7.8 .43 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.5  250 0   0     true 2 --- inspect 9.9   5.5   310   .66 0  
ldv-regression/test20_true-unreach-call_true-termination.c true 2 wit inspect .049 .046 7.7 .36 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.8  2.2  250 0   0     true 2 --- inspect 8.0   4.5   320   .66 0  
ldv-regression/test21_true-unreach-call_true-termination.c true 2 wit inspect .10  .094 6.5 .28 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.8  2.6  250 0   0     true 2 --- inspect 9.8   5.5   310   .62 0  
ldv-regression/test22_true-unreach-call.c true 2 wit inspect .79  .79  7.6 9.8  .045  0     - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 6.7  3.7  290 0   0     true 2 --- inspect 26     16     670   .66 0  
ldv-regression/test23_true-unreach-call.c true 2 wit inspect .43  .42  12   5.3  .045  0     - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 5.7  3.2  300 0   0     true 2 --- inspect 60     46     670   .62 0  
ldv-regression/test24_true-unreach-call_true-termination.c true 2 wit inspect .33  .33  10   4.1  .041  0     - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 5.5  3.0  280 0   0     true 2 --- inspect 27     21     490   .62 0  
ldv-regression/test25_true-unreach-call.c true 2 wit inspect 1.9   1.9   13   24    .057  0     - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 12    7.6  440 0   0     true 2 --- inspect 31     22     500   .66 0  
ldv-regression/test26_true-unreach-call_true-termination.c true 2 wit inspect .049 .047 7.4 .32 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.3  2.4  250 0   0     true 2 --- inspect 10     5.6   310   .66 0  
ldv-regression/test27_true-unreach-call_true-termination.c true 2 wit inspect .23  .22  11   2.7  .070  0     - --- inspect - --- inspect - --- inspect - --- inspect unknown 0 wit inspect 17    13    510 0   0     true 2 --- inspect 83     69     690   .62 0  
ldv-regression/test28_true-unreach-call_true-termination.c true 2 wit inspect .050 .047 7.4 .39 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  250 0   0     true 2 --- inspect 9.0   5.1   320   .66 0  
ldv-regression/test29_true-unreach-call_true-termination.c true 2 wit inspect .061 .058 6.7 .41 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  250 0   0     true 2 --- inspect 10     6.1   310   .62 0  
ldv-regression/test30_true-unreach-call_true-termination.c true 2 wit inspect .057 .055 7.0 .34 .0082 0     - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  1.9  250 0   0     true 2 --- inspect 12     6.7   340   .66 0  
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 55     55     1400   590    1.4    0     unknown 0 wit inspect 8.6 4.6 340 0   0     error (7) 0 --- inspect 28   16   530 .68 0   unknown 0 --- inspect 6.3 3.6 280 0   .43  false(unreach-call) 1 --- inspect 1.1  1.1  21 .50  0      - --- inspect - --- inspect
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 46     46     1400   570    1.1    0     unknown 0 wit inspect 8.5 4.5 340 0   0     error (7) 0 --- inspect 28   16   510 .71 0   unknown 0 --- inspect 7.5 4.0 300 0   0     false(unreach-call) 1 --- inspect 1.1  1.1  23 .39  0      - --- inspect - --- inspect
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 51     51     1400   610    1.3    0     unknown 0 wit inspect 8.6 4.5 340 0   0     error (7) 0 --- inspect 32   17   520 .75 0   unknown 0 --- inspect 6.4 3.6 280 0   .30  false(unreach-call) 1 --- inspect 1.1  1.1  21 .50  0      - --- inspect - --- inspect
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i error (42) 0 --- inspect 880     880     2400   7100    22      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .62 .37 41 0   0     error (2) 0 --- inspect .021 .022 5.8 0    0  
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i error (42) 0 --- inspect 880     880     2400   9400    22      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .75 .47 41 0   0     error (2) 0 --- inspect .025 .026 5.6 0    0  
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i error (42) 0 --- inspect 880     880     2400   7500    16      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .44 42 0   0     error (2) 0 --- inspect .033 .034 5.6 0    0  
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i error (42) 0 --- inspect 880     880     2400   7400    16      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0  
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i error (42) 0 --- inspect 880     880     2400   7600    20      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .81 .49 41 0   0     error (2) 0 --- inspect .024 .025 5.6 0    0  
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i error (42) 0 --- inspect 880     880     2400   7100    16      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .47 40 0   0     error (2) 0 --- inspect .024 .024 5.6 0    0  
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i error (42) 0 --- inspect 880     880     2400   7200    16      0     - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .77 .48 40 0   0     error (2) 0 --- inspect .021 .022 5.6 0    0  
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i error (42) 0 --- inspect 880     880     2400   8000    23      0     - --- inspect - --- inspect