Tool VeriAbs 1.3.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-10 16:50:17 CET 2018-12-10 20:34:10 CET 2018-12-10 21:22:10 CET 2018-12-10 21:27:56 CET 2018-12-12 21:52:30 CET 2018-12-10 19:33:41 CET 2018-12-10 20:40:20 CET
Run set veriabs.sv-comp19_prop-reachsafety.ReachSafety-Heap cpa-seq-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Heap uautomizer-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Heap uautomizer-validate-correctness-witnesses-veriabs.sv-comp19_prop-reachsafety.ReachSafety-Heap
Options -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/veriabs.2018-12-10_1650.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/veriabs.2018-12-10_1650.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/veriabs.2018-12-10_1650.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/veriabs.2018-12-10_1650.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/veriabs.2018-12-10_1650.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/veriabs.2018-12-10_1650.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 330   320   10000 3200 .95 0      true -32 wit inspect 6.4  3.5  260 0   0      error (7) 0 --- inspect 19     11     340   .71 0      unknown 0 --- inspect 5.1  2.8  270 0     0      false(unreach-call) 1 --- inspect .68   .68   21    .11  0      - --- inspect - --- inspect
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 340   320   1300 3700 2.1  0      true -32 wit inspect 6.2  3.3  270 0   0      error (7) 0 --- inspect 20     12     330   .75 0      unknown 0 --- inspect 5.0  2.8  260 0     0      true -32 --- inspect .72   .72   22    .094 0      - --- inspect - --- inspect
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 340   320   550 4100 .88 0      false(unreach-call) 1 wit inspect 4.7  2.6  260 0   0      error (7) 0 --- inspect 17     9.7   330   .75 0      unknown 0 --- inspect 4.2  2.4  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 230   220   3200 2300 .82 .32   true -32 wit inspect 5.7  3.1  260 0   0      error (7) 0 --- inspect 21     12     310   .75 0      unknown 0 --- inspect 5.2  2.9  260 0     0      false(unreach-call) 1 --- inspect .67   .66   21    .082 0      - --- inspect - --- inspect
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 110   92   760 1400 .51 .0041 unknown 0 wit inspect 4.6  2.6  270 0   0      error (7) 0 --- inspect 16     9.0   310   .68 0      unknown 0 --- inspect 4.6  2.6  250 0     0      false(unreach-call) 1 --- inspect .63   .63   21    .074 .025  - --- inspect - --- inspect
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 110   93   760 1200 .52 0      unknown 0 wit inspect 4.8  2.6  260 0   0      error (7) 0 --- inspect 19     11     300   .75 0      unknown 0 --- inspect 5.0  2.9  260 0     0      false(unreach-call) 1 --- inspect .63   .65   21    .074 0      - --- inspect - --- inspect
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i unknown 0 --- inspect 660   640   10000 6600 1.2  .0041 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .57 .35 40 0   0      error (2) 0 --- inspect .025 .025 5.6 0    0     
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i timeout 0 --- inspect 900   890   2700 9300 .66 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .58 .35 40 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0     
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i unknown 0 --- inspect 540   520   1300 6300 1.8  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .79 .48 42 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0     
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i unknown 0 --- inspect 560   540   3300 6600 1.1  0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .63 .38 40 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0     
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i unknown 0 --- inspect 730   720   4000 4500 .99 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .37 41 0   0      error (2) 0 --- inspect .020 .021 5.7 0    0     
heap-manipulation/tree_true-unreach-call.i timeout 0 --- inspect 900   890   1600 9600 .71 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .61 .39 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 24   8.6 280 200 .50 .0041 false(unreach-call) 1 wit inspect 5.6  3.0  260 0   0      false(unreach-call) 1 --- inspect 9.8   5.6   310   .66 0      unknown 0 --- inspect 4.3  2.5  260 0     0      false(unreach-call) 1 --- inspect .62   .62   20    .066 0      - --- inspect - --- inspect
list-properties/list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 150   140   600 2100 .58 .29   true -32 wit inspect 6.4  3.5  280 0   0      out of memory 0 --- inspect 56     36     7000   .70 0      unknown 0 --- inspect 6.4  3.5  280 0     0      false(unreach-call) 1 --- inspect .71   .71   22    .066 0      - --- inspect - --- inspect
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 22   7.9 290 170 .46 .0041 false(unreach-call) 1 wit inspect 5.4  3.0  260 0   0      false(unreach-call) 1 --- inspect 8.8   4.8   310   .66 0      unknown 0 --- inspect 4.3  2.4  250 0     0      false(unreach-call) 1 --- inspect .62   .62   21    .066 0      - --- inspect - --- inspect
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 18   6.6 280 150 .46 0      true -32 wit inspect 6.1  3.3  260 0   0      true -32 --- inspect 9.8   5.9   340   .66 0      unknown 0 --- inspect 5.2  2.9  250 0     .47   false(unreach-call) 1 --- inspect .61   .61   21    .070 0      - --- inspect - --- inspect
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 22   8.2 280 160 .45 0      false(unreach-call) 1 wit inspect 4.5  2.4  260 0   .025  false(unreach-call) 1 --- inspect 11     6.0   310   .66 0      unknown 0 --- inspect 4.1  2.4  250 0     0      false(unreach-call) 1 --- inspect .63   .63   20    .066 0      - --- inspect - --- inspect
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 31   16   290 310 .49 0      false(unreach-call) 1 wit inspect 5.3  2.9  270 0   0      false(unreach-call) 1 --- inspect 8.5   4.7   320   .62 0      unknown 0 --- inspect 4.2  2.4  250 0     0      false(unreach-call) 1 --- inspect .62   .62   21    .070 0      - --- inspect - --- inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout 0 --- inspect 900   890   5200 8000 .72 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .65 .43 40 0   0      error (2) 0 --- inspect .020 .021 5.7 0    0     
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i timeout 0 --- inspect 900   890   3300 8100 .70 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .70 .43 42 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0     
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i true 2 wit inspect 77   40   1100 650 140    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 26    16    620 0   0      true 2 --- inspect 110     96     780   .62 0     
list-properties/list_true-unreach-call_false-valid-memtrack.i timeout 0 --- inspect 900   890   13000 8800 .63 .0082 - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .72 .45 40 0   0      error (2) 0 --- inspect .021 .021 5.6 0    0     
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i unknown 0 --- inspect 830   810   5900 8100 .95 .025  - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .76 .46 40 0   0      error (2) 0 --- inspect .024 .024 5.6 0    0     
list-properties/simple_true-unreach-call_false-valid-memtrack.i timeout 0 --- inspect 900   890   6100 10000 .64 .27   - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .59 .36 40 0   0      error (2) 0 --- inspect .020 .021 5.6 0    0     
list-properties/splice_true-unreach-call_false-valid-memtrack.i timeout 0 --- inspect 900   880   5000 9000 .65 0      - --- inspect - --- inspect - --- inspect - --- inspect error (invalid witness file) 0 --- inspect .73 .45 41 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0     
ldv-regression/1_3_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 8.9 3.5 270 85 .12 0      false(unreach-call) 1 wit inspect 4.0  2.2  250 0   0      false(unreach-call) 1 --- inspect 8.6   5.1   310   .66 0      false(unreach-call) 1 --- inspect 4.6  2.6  250 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 22   7.6 280 170 .53 0      false(unreach-call) 1 wit inspect 5.4  2.9  250 0   0      false(unreach-call) 1 --- inspect 9.6   5.4   330   .66 0      unknown 0 --- inspect 4.2  2.4  250 0     0      false(unreach-call) 1 --- inspect .68   .68   20    .086 0      - --- inspect - --- inspect
ldv-regression/callfpointer_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 8.7 3.4 270 70 .11 .0041 false(unreach-call) 1 wit inspect 3.7  2.0  250 0   0      false(unreach-call) 1 --- inspect 6.5   3.8   300   .66 0      false(unreach-call) 1 --- inspect 4.1  2.4  240 0     0      false(unreach-call) 1 --- inspect .59   .59   20    .045 0      - --- inspect - --- inspect
ldv-regression/fo_test_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 22   7.4 280 160 .50 0      true -32 wit inspect 4.4  2.4  250 0   0      unknown 0 --- inspect 16     9.1   320   .75 0      unknown 0 --- inspect 4.4  2.5  250 0     0      false(unreach-call) 1 --- inspect .67   .67   20    .074 0      - --- inspect - --- inspect
ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 8.6 3.5 270 73 .11 0      false(unreach-call) 1 wit inspect 3.6  2.0  250 0   0      false(unreach-call) 1 --- inspect 8.4   4.6   300   .66 0      false(unreach-call) 1 --- inspect 4.6  2.6  250 0     0      false(unreach-call) 1 --- inspect .60   .60   20    .049 0      - --- inspect - --- inspect
ldv-regression/mutex_lock_struct_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 8.7 3.5 270 68 .11 .0041 false(unreach-call) 1 wit inspect 3.7  2.1  250 0   0      false(unreach-call) 1 --- inspect 7.5   4.2   310   .66 0      false(unreach-call) 1 --- inspect 3.8  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 9.0 3.6 270 75 .12 .0041 false(unreach-call) 1 wit inspect 3.8  2.2  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    .049 0      - --- inspect - --- inspect
ldv-regression/rule57_ebda_blast_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 9.8 3.8 280 81 .12 0      false(unreach-call) 1 wit inspect 4.2  2.3  260 0   0      false(unreach-call) 1 --- inspect 10     6.1   320   .66 .0041 unknown 0 --- inspect 3.9  2.2  250 0     0      false(unreach-call) 1 --- inspect .59   .60   20    .061 0      - --- inspect - --- inspect
ldv-regression/rule60_list2_true-termination.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect 21   7.1 290 170 .46 0      false(unreach-call) 1 wit inspect 4.8  2.6  260 0   0      false(unreach-call) 1 --- inspect 13     7.2   480   .66 0      exception 0 --- inspect 4.2  2.4  250 0     .020  false(unreach-call) 1 --- inspect .63   .63   21    .078 0      - --- inspect - --- inspect
ldv-regression/stateful_check_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect 16   6.1 280 130 .38 .16   false(unreach-call) 1 wit inspect 4.4  2.4  260 0   0      false(unreach-call) 1 --- inspect 8.3   4.6   310   .66 0      false(unreach-call) 1 --- inspect 4.1  2.3  250 0     0      false(unreach-call) 1 --- inspect .58   .58   21    .057 0      - --- inspect - --- inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 14   5.0 270 110 .32 .020  false(unreach-call) 1 wit inspect 4.4  2.4  250 0   .0041 false(unreach-call) 1 --- inspect 7.5   4.2   300   .66 0      false(unreach-call) 1 --- inspect 3.9  2.2  250 0     0      false(unreach-call) 1 --- inspect .59   .58   20    .045 0      - --- inspect - --- inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect 13   4.8 280 89 .23 .0041 false(unreach-call) 1 wit inspect 4.1  2.3  250 0   0      false(unreach-call) 1 --- inspect 6.8   4.3   300   .66 0      false(unreach-call) 1 --- inspect 3.5  2.0  240 0     .0041 false(unreach-call) 1 --- inspect .57   .58   20    .045 .0041 - --- inspect - --- inspect
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call.i true 2 wit inspect 14   6.5 460 110 150    .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  1.9  250 0   0      true 2 --- inspect 7.7   4.8   310   .66 0     
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i true 2 wit inspect 13   6.4 470 120 140    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.6  2.6  250 0   0      true 2 --- inspect 8.1   4.5   310   .66 0     
ldv-regression/alias_of_return_true-termination.c_true-unreach-call.i true 2 wit inspect 14   6.5 450 110 150    .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.0  250 0   0      true 2 --- inspect 7.6   4.3   310   .66 0     
ldv-regression/alias_of_return_true-termination.c_true-unreach-call_1.i true 2 wit inspect 13   6.4 450 120 140    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  250 0   0      true 2 --- inspect 8.1   4.8   310   .66 0     
ldv-regression/ex3_forlist_true-termination.c_true-unreach-call.i true 2 wit inspect 43   19   930 380 140    .11   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 15    8.9  480 0   0      true 2 --- inspect 97     78     810   .62 0     
ldv-regression/just_assert_true-termination.c_true-unreach-call.i true 2 wit inspect 12   6.3 440 110 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.2  2.3  240 0   0      true 2 --- inspect 7.9   4.7   290   .66 0     
ldv-regression/mutex_lock_int_true-termination.c_true-unreach-call_1.i true 2 wit inspect 14   6.6 470 110 140    .27   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.3  2.4  250 0   .0041 true 2 --- inspect 8.0   5.0   310   .62 0     
ldv-regression/mutex_lock_struct_true-termination.c_true-unreach-call_1.i true 2 wit inspect 14   6.6 460 120 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.3  2.4  250 0   0      true 2 --- inspect 7.7   4.7   310   .62 0     
ldv-regression/nested_structure_noptr_true-termination.c_true-unreach-call.i true 2 wit inspect 12   6.3 440 110 140    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.3  1.9  250 0   0      true 2 --- inspect 8.4   5.0   310   .62 0     
ldv-regression/nested_structure_noptr_true-unreach-call_true-termination.i true 2 wit inspect 14   6.5 480 130 140    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.1  250 0   0      true 2 --- inspect 7.9   4.5   310   .62 0     
ldv-regression/nested_structure_ptr_true-termination.c_true-unreach-call.i true 2 wit inspect 16   7.7 580 130 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.9  2.7  250 0   0      true 2 --- inspect 7.1   4.0   300   .66 0     
ldv-regression/nested_structure_ptr_true-unreach-call_true-termination.i true 2 wit inspect 16   7.6 500 140 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.1  2.3  250 0   0      true 2 --- inspect 7.8   4.9   310   .66 0     
ldv-regression/nested_structure_true-termination.c_true-unreach-call.i true 2 wit inspect 15   6.7 470 120 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.1  250 0   0      true 2 --- inspect 8.7   5.1   310   .66 0     
ldv-regression/nested_structure_true-unreach-call_true-termination.i true 2 wit inspect 14   6.8 450 110 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  250 0   0      true 2 --- inspect 7.1   4.5   310   .66 0     
ldv-regression/oomInt_true-termination.c_true-unreach-call.i true 2 wit inspect 13   6.5 450 120 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.5  250 0   0      true 2 --- inspect 7.8   4.8   310   .66 0     
ldv-regression/oomInt_true-termination.c_true-unreach-call_1.i true 2 wit inspect 13   6.6 460 110 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.9  2.7  250 0   .0041 true 2 --- inspect 7.1   4.5   310   .66 0     
ldv-regression/rule57_ebda_blast_true-termination.c_true-unreach-call_1.i true 2 wit inspect 16   7.4 450 150 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.0  2.8  260 0   0      true 2 --- inspect 10     6.1   330   .66 .0041
ldv-regression/rule60_list2_true-termination.c_true-unreach-call.i true 2 wit inspect 36   15   840 340 140    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.1  2.8  260 0   0      true 2 --- inspect 20     13     650   .62 0     
ldv-regression/rule60_list_true-termination.c_true-unreach-call.i true 2 wit inspect 24   10   520 220 140    .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.3  2.4  260 0   .016  true 2 --- inspect 12     7.0   400   .62 0     
ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i true 2 wit inspect 24   10   440 180 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.1  2.8  250 0   0      true 2 --- inspect 9.3   5.4   310   .62 0     
ldv-regression/structure_assignment_true-termination.c_true-unreach-call.i true 2 wit inspect 12   6.3 440 100 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.9  2.2  250 0   0      true 2 --- inspect 8.0   4.5   310   .66 0     
ldv-regression/test_address_true-termination.c_true-unreach-call.i true 2 wit inspect 17   7.7 450 150 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.2  2.3  250 0   0      true 2 --- inspect 9.1   5.4   310   .66 0     
ldv-regression/test_cut_trace_true-termination.c_true-unreach-call.i true 2 wit inspect 13   6.3 460 130 140    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  250 0   0      true 2 --- inspect 8.2   4.9   310   .66 0     
ldv-regression/test_malloc-1_true-unreach-call_true-termination.i true 2 wit inspect 23   9.9 450 180 140    .43   - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.9  2.2  260 0   0      true 2 --- inspect 8.1   4.6   310   .62 0     
ldv-regression/test_malloc-2_true-unreach-call_true-termination.i true 2 wit inspect 23   9.8 450 200 140    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  260 0   0      true 2 --- inspect 8.4   5.1   320   .66 0     
ldv-regression/test_overflow_true-termination.c_true-unreach-call.i true 2 wit inspect 19   8.4 450 150 140    .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 5.2  2.9  260 0   .033  true 2 --- inspect 8.7   4.8   320   .66 0     
ldv-regression/test_union_cast-1_true-unreach-call_true-termination.i true 2 wit inspect 12   6.3 470 110 140    .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.5  250 0   0      true 2 --- inspect 7.0   4.5   310   .66 0     
ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i true 2 wit inspect 13   6.5 470 120 140    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.6  2.6  250 0   0      true 2 --- inspect 7.2   4.6   310   .66 0     
ldv-regression/test_union_cast_true-termination.c_true-unreach-call.i true 2 wit inspect 13   6.3 450 100 150    .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.2  2.4  250 0   0      true 2 --- inspect 6.9   4.0   310   .66 0     
ldv-regression/test_union_cast_true-termination.c_true-unreach-call_1.i true 2 wit inspect 13   6.4 470 110 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  2.0  250 0   0      true 2 --- inspect 7.2   4.5   310   .66 0     
ldv-regression/test_union_true-termination.c_true-unreach-call.i true 2 wit inspect 13   6.3 470 100 150    .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.2  2.4  250 0   0      true 2 --- inspect 7.1   4.0   290   .66 0     
ldv-regression/test_union_true-termination.c_true-unreach-call_1.i true 2 wit inspect 13   6.5 470 110 140    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.0  250 0   0      true 2 --- inspect 6.8   3.9   300   .62 0     
ldv-regression/volatile_alias_true-termination.c_true-unreach-call.i true 2 wit inspect 13   6.6 470 99 140    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.5  250 0   0      true 2 --- inspect 6.6   3.8   310   .66 0     
ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i true 2 wit inspect 13   6.4 460 120 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  1.9  250 0   0      true 2 --- inspect 7.7   4.6   310   .66 0     
ldv-regression/test02_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.8 3.6 270 77 .11 .016  false(unreach-call) 1 wit inspect 3.7  2.0  250 0   0      false(unreach-call) 1 --- inspect 6.9   3.9   310   .66 0      false(unreach-call) 1 --- inspect 3.8  2.2  260 0     .0041 false(unreach-call) 1 --- inspect .57   .57   20    .045 0      - --- inspect - --- inspect
ldv-regression/test06_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.4 3.4 270 72 .11 .0041 true -32 wit inspect 3.9  2.2  250 0   0      false(unreach-call) 1 --- inspect 8.4   4.7   310   .66 0      false(unreach-call) 1 --- inspect 3.8  2.1  250 0     0      false(unreach-call) 1 --- inspect .62   .64   20    .057 0      - --- inspect - --- inspect
ldv-regression/test08_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.9 3.5 270 69 .11 0      false(unreach-call) 1 wit inspect 4.5  2.5  250 0   0      false(unreach-call) 1 --- inspect 8.0   4.5   310   .66 0      false(unreach-call) 1 --- inspect 3.5  2.0  250 0     .0041 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 8.8 3.5 270 84 .11 .0082 false(unreach-call) 1 wit inspect 3.9  2.2  250 0   0      false(unreach-call) 1 --- inspect 6.7   3.9   310   .62 .0041 false(unreach-call) 1 --- inspect 3.4  2.0  250 0     0      false(unreach-call) 1 --- inspect .58   .58   20    .045 0      - --- inspect - --- inspect
ldv-regression/test21_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 9.4 3.6 280 82 .11 .0041 false(unreach-call) 1 wit inspect 4.5  2.5  250 0   0      false(unreach-call) 1 --- inspect 7.0   4.0   310   .66 0      unknown 0 --- inspect 4.2  2.5  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 13   4.8 280 100 .29 .016  false(unreach-call) 1 wit inspect 4.4  2.4  260 0   0      false(unreach-call) 1 --- inspect 11     6.2   400   .66 0      unknown 0 --- inspect 3.6  2.1  240 0     0      true -32 --- inspect .59   .59   21    .057 0      - --- inspect - --- inspect
ldv-regression/test23_false-unreach-call.c false(unreach-call) 1 wit inspect 24   13   300 270 .34 .012  false(unreach-call) 1 wit inspect 4.6  2.6  270 0   0      timeout 0 --- inspect 98     62     7000   1.5  0      unknown 0 --- inspect 5.0  2.9  250 0     .0041 true -32 --- inspect .60   .59   21    .057 0      - --- inspect - --- inspect
ldv-regression/test24_false-unreach-call.c false(unreach-call) 1 wit inspect 22   8.7 330 190 .36 0      false(unreach-call) 1 wit inspect 5.9  3.4  270 0   .0041 out of memory 0 --- inspect 83     52     7000   .68 0      unknown 0 --- inspect 3.9  2.2  250 0     0      true -32 --- inspect .61   .61   21    .057 0      - --- inspect - --- inspect
ldv-regression/test25_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 27   14   310 240 .36 .0041 false(unreach-call) 1 wit inspect 6.1  3.4  280 0   0      timeout 0 --- inspect 97     74     3300   .63 0      unknown 0 --- inspect 4.2  2.4  270 0     0      true -32 --- inspect .62   .61   21    .057 .0041 - --- inspect - --- inspect
ldv-regression/test26_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.9 3.3 270 70 .11 0      false(unreach-call) 1 wit inspect 4.0  2.2  250 0   0      false(unreach-call) 1 --- inspect 7.9   4.4   310   .66 0      false(unreach-call) 1 --- inspect 3.7  2.2  250 0     0      false(unreach-call) 1 --- inspect .57   .56   20    .045 0      - --- inspect - --- inspect
ldv-regression/test27_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 22   9.0 300 180 .37 .0041 false(unreach-call) 1 wit inspect 5.4  3.0  270 0   0      out of memory 0 --- inspect 87     55     7000   .68 0      unknown 0 --- inspect 3.9  2.3  250 0     0      error (2) 0 --- inspect .58   .58   21    .057 0      - --- inspect - --- inspect
ldv-regression/test28_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.7 3.5 280 75 .11 0      false(unreach-call) 1 wit inspect 3.7  2.1  250 0   0      false(unreach-call) 1 --- inspect 7.6   4.3   310   .66 0      true -32 --- inspect 3.4  2.0  250 0     0      false(unreach-call) 1 --- inspect .59   .59   20    .049 .0041 - --- inspect - --- inspect
ldv-regression/test29_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.6 3.1 270 74 .11 .0041 false(unreach-call) 1 wit inspect 4.9  2.7  250 0   0      false(unreach-call) 1 --- inspect 9.7   5.6   310   .66 0      false(unreach-call) 1 --- inspect 3.5  2.1  250 0     0      false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
ldv-regression/test30_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.7 3.5 270 76 .11 0      false(unreach-call) 1 wit inspect 4.4  2.5  260 0   0      false(unreach-call) 1 --- inspect 7.3   4.2   310   .66 0      false(unreach-call) 1 --- inspect 4.6  2.6  250 0     0      false(unreach-call) 1 --- inspect .57   .57   20    .049 0      - --- inspect - --- inspect
ldv-regression/test01_true-unreach-call_true-termination.c true 2 wit inspect 13   6.6 460 110 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.5  1.9  250 0   0      true 2 --- inspect 7.1   4.1   310   .66 0     
ldv-regression/test03_true-unreach-call_true-termination.c true 2 wit inspect 13   6.7 470 110 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.2  2.4  250 0   0      true 2 --- inspect 9.2   5.5   310   .66 0     
ldv-regression/test04_true-unreach-call_true-termination.c true 2 wit inspect 14   6.5 480 130 170    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.8  2.1  250 0   0      true 2 --- inspect 7.6   4.3   310   .66 0     
ldv-regression/test05_true-unreach-call_true-termination.c true 2 wit inspect 18   8.1 680 140 140    .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.1  2.2  250 0   0      true 2 --- inspect 12     6.7   330   .66 0     
ldv-regression/test07_true-unreach-call_true-termination.c true 2 wit inspect 15   7.3 520 130 140    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.2  2.4  250 0   0      true 2 --- inspect 9.4   5.8   320   .66 0     
ldv-regression/test09_true-unreach-call_true-termination.c true 2 wit inspect 15   7.2 500 140 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.0  260 0   0      true 2 --- inspect 10     5.5   320   .66 0     
ldv-regression/test10_true-unreach-call_true-termination.c true 2 wit inspect 20   9.0 650 200 140    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.7  2.1  260 0   0      true 2 --- inspect 11     6.5   440   .66 0     
ldv-regression/test11_true-unreach-call_true-termination.c true 2 wit inspect 14   6.8 460 130 140    .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.2  2.4  260 0   0      true 2 --- inspect 8.5   5.2   310   .66 0     
ldv-regression/test13_true-unreach-call_true-termination.c true 2 wit inspect 14   6.6 460 110 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.1  2.3  250 0   0      true 2 --- inspect 7.9   4.5   320   .66 0     
ldv-regression/test14_true-unreach-call_true-termination.c true 2 wit inspect 14   6.7 460 110 170    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.0  250 0   0      true 2 --- inspect 8.0   4.5   310   .66 0     
ldv-regression/test15_true-unreach-call_true-termination.c true 2 wit inspect 14   6.8 460 120 140    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.8  2.1  250 0   .0041 true 2 --- inspect 8.4   4.7   310   .66 0     
ldv-regression/test16_true-unreach-call_true-termination.c true 2 wit inspect 14   6.7 480 140 140    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.4  1.9  250 0   0      true 2 --- inspect 8.4   4.9   310   .66 0     
ldv-regression/test17_true-unreach-call_true-termination.c true 2 wit inspect 13   6.4 450 120 150    .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.3  2.5  250 0   0      true 2 --- inspect 7.2   4.6   310   .66 0     
ldv-regression/test18_true-unreach-call_true-termination.c true 2 wit inspect 15   7.1 460 120 140    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 3.6  2.0  250 0   0      true 2 --- inspect 8.0   4.5   310   .66 0     
ldv-regression/test19_true-unreach-call_true-termination.c true 2 wit inspect 16   7.3 510 160 140    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.7  2.7  250 0   0      true 2 --- inspect 8.7   4.9   310   .66 0     
ldv-regression/test20_true-unreach-call_true-termination.c true 2 wit inspect 14   6.8 470 120 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.6  2.6  250 0   0      true 2 --- inspect 7.7   4.3   300   .66 0     
ldv-regression/test21_true-unreach-call_true-termination.c true 2 wit inspect 15   7.0 490 130 140    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.7  2.6  250 0   0      true 2 --- inspect 9.2   5.6   310   .66 0     
ldv-regression/test22_true-unreach-call.c true 2 wit inspect 28   14   820 290 140    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 8.2  4.7  320 0   0      true 2 --- inspect 22     14     660   .62 0     
ldv-regression/test23_true-unreach-call.c true 2 wit inspect 66   38   740 650 140    6.3    - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 9.7  5.8  330 0   0      true 2 --- inspect 67     59     610   .62 0     
ldv-regression/test24_true-unreach-call_true-termination.c true 2 wit inspect 21   8.9 580 170 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 8.3  4.6  310 0   0      true 2 --- inspect 27     22     470   .62 0     
ldv-regression/test25_true-unreach-call.c true 2 wit inspect 47   28   690 490 140    .13   - --- inspect - --- inspect - --- inspect - --- inspect assertion 0 --- inspect 4.8  2.7  260 0   0      error (7) 0 --- inspect 10     6.0   280   .74 0     
ldv-regression/test26_true-unreach-call_true-termination.c true 2 wit inspect 15   6.9 480 120 140    .0041 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.2  2.4  250 0   0      true 2 --- inspect 8.5   4.8   310   .66 0     
ldv-regression/test27_true-unreach-call_true-termination.c true 2 wit inspect 75   50   780 780 150    .057  - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 29    22    550 0   0      true 2 --- inspect 86     70     840   .62 0     
ldv-regression/test28_true-unreach-call_true-termination.c true 2 wit inspect 14   6.8 470 140 140    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.4  2.5  250 0   0      true 2 --- inspect 8.7   5.0   310   .66 0     
ldv-regression/test29_true-unreach-call_true-termination.c true 2 wit inspect 12   6.5 440 120 140    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.5  2.5  250 0   0      true 2 --- inspect 8.7   5.4   320   .62 0     
ldv-regression/test30_true-unreach-call_true-termination.c true 2 wit inspect 17   8.3 620 160 170    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 4.8  2.7  260 0   0      true 2 --- inspect 10     6.2   340   .66 0     
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i error 0 --- inspect 14   4.9 240 120 .17 0      error (invalid witness file) 0 --- inspect .66 .41 41 0   0      error (2) 0 --- inspect .024 .025 5.6 0    0      error (invalid witness file) 0 --- inspect 1.2  .78 48 0     0      error (invalid witness file) 0 --- inspect .0048 .0058 .54 0     0      - --- inspect - --- inspect
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i error 0 --- inspect 15   4.9 250 130 .14 0      error (invalid witness file) 0 --- inspect .72 .46 40 0   0      error (2) 0 --- inspect .021 .022 5.6 0    0      error (invalid witness file) 0 --- inspect 1.2  .75 47 0     0      error (invalid witness file) 0 --- inspect .0020 .0026 .53 0     0      - --- inspect - --- inspect
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i error 0 --- inspect 15   5.0 240 130 .17 0      error (invalid witness file) 0 --- inspect .58 .35 41 0   0      error (2) 0 --- inspect .024 .025 5.7 0    0      error (invalid witness file) 0 --- inspect .90 .59 47 0     0      error (invalid witness file) 0 --- inspect .0019 .0036 .54 0     0      - --- inspect - --- inspect
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 34   12   630 300 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 7.6  4.0  290 0   0      error (7) 0 --- inspect 27     15     530   .75 0     
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 34   12   650 270 140    .0082 - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 8.4  4.4  300 0   0      error (7) 0 --- inspect 27     15     530   .75 0     
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 33   12   640 270 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 9.2  4.9  290 0   0      error (7) 0 --- inspect 27     15     520   .71 0     
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 33   12   620 260 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 9.1  4.8  310 0   0      error (7) 0 --- inspect 27     15     540   .75 0     
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 35   12   650 260 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 8.4  4.4  300 0   .086  error (7) 0 --- inspect 30     17     530   .75 0     
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 34   12   610 280 150    0      - --- inspect - --- inspect - --- inspect - --- inspect true 2 wit inspect 12    6.0  310 0   0      error (7) 0