Tool ULTIMATE Automizer 0.1.23-3204b741 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
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.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-02 01:06:24 CET 2017-12-03 03:07:09 CET 2017-12-03 03:49:57 CET 2017-12-03 03:57:59 CET 2017-12-03 04:29:07 CET 2017-12-02 23:12:02 CET 2017-12-03 03:11:19 CET
Run set uautomizer.sv-comp18.ReachSafety-Heap cpa-seq-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-Heap uautomizer-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-uautomizer.sv-comp18-violation-witness.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.ReachSafety-Heap uautomizer-validate-correctness-witnesses-uautomizer.sv-comp18-correctness-witness.ReachSafety-Heap
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/uautomizer.2017-12-02_0106.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -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 --full-output --validate ../../results-verified/uautomizer.2017-12-02_0106.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/uautomizer.2017-12-02_0106.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true --graphml-witness ../../results-verified/uautomizer.2017-12-02_0106.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/uautomizer.2017-12-02_0106.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/uautomizer.2017-12-02_0106.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
heap-manipulation/bubble_sort_linux_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   1100 13000 error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .80 49 error (invalid witness file) 0 wit inspect .0026 .28 - wit inspect - wit inspect
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   5300 9200 error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect 1.1  51 error (invalid witness file) 0 wit inspect .0013 .35 - wit inspect - wit inspect
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 9.9 520 86 false(unreach-call) 1 wit inspect 4.3  270 false(unreach-call) 1 wit inspect 7.4   310   unknown 0 wit inspect 4.5  210 true -32 wit inspect .72   19    - wit inspect - wit inspect
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 130   1100 1600 true -32 wit inspect 4.5  260 false(unreach-call) 1 wit inspect 5.6   320   unknown 0 wit inspect 4.3  220 true -32 wit inspect .81   19    - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 74   680 850 false(unreach-call) 1 wit inspect 3.8  260 false(unreach-call) 1 wit inspect 4.7   300   unknown 0 wit inspect 3.4  210 true -32 wit inspect .85   19    - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 71   670 950 false(unreach-call) 1 wit inspect 4.9  260 false(unreach-call) 1 wit inspect 6.8   290   unknown 0 wit inspect 3.6  210 true -32 wit inspect .85   19    - wit inspect - wit inspect
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   1300 9600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 42 error (2) 0 wit inspect .018 4.8
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   950 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 41 error (2) 0 wit inspect .019 4.9
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   5900 9900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .019 5.0
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   1200 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .024 4.8
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   930 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .017 4.8
heap-manipulation/tree_true-unreach-call.i timeout 0 wit inspect 900   1100 9200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .018 5.0
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 6.1 290 51 false(unreach-call) 1 wit inspect 2.7  260 false(unreach-call) 1 wit inspect 5.6   270   unknown 0 wit inspect 4.2  210 true -32 wit inspect .80   18    - wit inspect - wit inspect
list-properties/list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 28   810 260 false(unreach-call) 1 wit inspect 4.8  260 false(unreach-call) 1 wit inspect 5.9   270   unknown 0 wit inspect 4.3  210 true -32 wit inspect .76   18    - wit inspect - wit inspect
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 6.8 320 59 false(unreach-call) 1 wit inspect 3.9  270 false(unreach-call) 1 wit inspect 5.5   270   unknown 0 wit inspect 4.2  210 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 42   990 450 unknown 0 wit inspect 4.2  270 false(unreach-call) 1 wit inspect 24     670   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .84   19    - wit inspect - wit inspect
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 7.0 350 59 false(unreach-call) 1 wit inspect 3.7  270 false(unreach-call) 1 wit inspect 5.3   260   unknown 0 wit inspect 3.1  210 true -32 wit inspect .64   18    - wit inspect - wit inspect
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 6.9 300 54 false(unreach-call) 1 wit inspect 4.3  270 false(unreach-call) 1 wit inspect 7.6   270   unknown 0 wit inspect 4.4  210 true -32 wit inspect .64   19    - wit inspect - wit inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   1100 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .019 4.9
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   1300 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .020 4.9
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i true 2 wit inspect 56   1200 580 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 26    500 true 2 wit inspect 55     1100  
list-properties/list_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   1100 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .020 4.8
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   1000 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .019 4.9
list-properties/simple_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   1100 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .019 4.9
list-properties/splice_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   1300 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .019 4.9
ldv-regression/1_3_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 5.7 300 47 true -32 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 5.1   260   unknown 0 wit inspect 3.1  190 false(unreach-call) 1 wit inspect .62   18    - wit inspect - wit inspect
ldv-regression/alt_test_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 6.0 290 50 false(unreach-call) 1 wit inspect 5.0  270 false(unreach-call) 1 wit inspect 6.9   270   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .71   18    - wit inspect - wit inspect
ldv-regression/callfpointer_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 4.1 240 37 true -32 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 3.2   230   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
ldv-regression/fo_test_true-termination.c_false-unreach-call.i unknown 0 wit inspect 11   300 84 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect 1.1  47 error (invalid witness file) 0 wit inspect .0017 .29 - wit inspect - wit inspect
ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 4.9 280 38 true -32 wit inspect 2.1  250 false(unreach-call) 1 wit inspect 4.9   260   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .68   18    - wit inspect - wit inspect
ldv-regression/mutex_lock_struct_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 5.0 290 36 true -32 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 4.9   250   unknown 0 wit inspect 3.2  190 false(unreach-call) 1 wit inspect .78   18    - wit inspect - wit inspect
ldv-regression/recursive_list_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 4.8 260 38 false(unreach-call) 1 wit inspect 4.2  260 false(unreach-call) 1 wit inspect 6.3   260   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .77   19    - wit inspect - wit inspect
ldv-regression/rule57_ebda_blast_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 5.5 290 42 true -32 wit inspect 3.8  260 false(unreach-call) 1 wit inspect 4.3   280   unknown 0 wit inspect 3.0  190 error (2) 0 wit inspect .77   19    - wit inspect - wit inspect
ldv-regression/rule60_list2_true-termination.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect 18   740 150 true -32 wit inspect 4.9  260 false(unreach-call) 1 wit inspect 7.1   280   unknown 0 wit inspect 3.7  210 true -32 wit inspect .63   19    - wit inspect - wit inspect
ldv-regression/stateful_check_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect 6.9 320 56 true -32 wit inspect 5.8  270 false(unreach-call) 1 wit inspect 4.3   290   unknown 0 wit inspect 3.6  210 true -32 wit inspect .68   19    - wit inspect - wit inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 5.8 310 44 true -32 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 5.6   230   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .78   18    - wit inspect - wit inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect 4.7 290 41 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 5.5   240   unknown 0 wit inspect 3.7  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call.i true 2 wit inspect 5.3 300 43 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 8.0   280  
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i true 2 wit inspect 4.8 290 44 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  240 true 2 wit inspect 5.6   260  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call.i true 2 wit inspect 4.9 290 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 6.0   280  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call_1.i true 2 wit inspect 4.8 290 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 5.3   260  
ldv-regression/ex3_forlist_true-termination.c_true-unreach-call.i true 2 wit inspect 27   780 280 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 17    470 true 2 wit inspect 29     700  
ldv-regression/just_assert_true-termination.c_true-unreach-call.i true 2 wit inspect 4.3 270 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 5.2   210  
ldv-regression/mutex_lock_int_true-termination.c_true-unreach-call_1.i true 2 wit inspect 5.6 300 45 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 7.2   270  
ldv-regression/mutex_lock_struct_true-termination.c_true-unreach-call_1.i true 2 wit inspect 5.7 300 42 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 6.3   260  
ldv-regression/nested_structure_noptr_true-termination.c_true-unreach-call.i true 2 wit inspect 4.3 280 34 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 4.7   240  
ldv-regression/nested_structure_noptr_true-unreach-call_true-termination.i true 2 wit inspect 4.4 280 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 4.9   260  
ldv-regression/nested_structure_ptr_true-termination.c_true-unreach-call.i true 2 wit inspect 10   530 96 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  270 true 2 wit inspect 10     470  
ldv-regression/nested_structure_ptr_true-unreach-call_true-termination.i true 2 wit inspect 7.4 460 64 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 12     420  
ldv-regression/nested_structure_true-termination.c_true-unreach-call.i true 2 wit inspect 6.3 340 53 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 7.7   280  
ldv-regression/nested_structure_true-unreach-call_true-termination.i true 2 wit inspect 6.4 360 49 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 8.0   290  
ldv-regression/oomInt_true-termination.c_true-unreach-call.i true 2 wit inspect 4.9 290 41 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 5.9   260  
ldv-regression/oomInt_true-termination.c_true-unreach-call_1.i true 2 wit inspect 4.9 290 39 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 6.0   270  
ldv-regression/rule57_ebda_blast_true-termination.c_true-unreach-call_1.i true 2 wit inspect 6.0 300 49 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.4  260 true 2 wit inspect 6.6   270  
ldv-regression/rule60_list2_true-termination.c_true-unreach-call.i true 2 wit inspect 17   690 140 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1  260 true 2 wit inspect 21     660  
ldv-regression/rule60_list_true-termination.c_true-unreach-call.i true 2 wit inspect 8.0 420 62 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 12     390  
ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i true 2 wit inspect 4.9 280 41 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  250 true 2 wit inspect 4.6   260  
ldv-regression/structure_assignment_true-termination.c_true-unreach-call.i true 2 wit inspect 4.5 280 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 5.4   260  
ldv-regression/test_address_true-termination.c_true-unreach-call.i true 2 wit inspect 4.9 290 42 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 5.5   260  
ldv-regression/test_cut_trace_true-termination.c_true-unreach-call.i true 2 wit inspect 4.7 280 41 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  240 true 2 wit inspect 5.3   250  
ldv-regression/test_malloc-1_true-unreach-call_true-termination.i true 2 wit inspect 5.3 300 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  260 true 2 wit inspect 7.3   270  
ldv-regression/test_malloc-2_true-unreach-call_true-termination.i true 2 wit inspect 5.3 290 41 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  260 true 2 wit inspect 5.8   270  
ldv-regression/test_overflow_true-termination.c_true-unreach-call.i true 2 wit inspect 4.7 280 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  250 true 2 wit inspect 5.6   260  
ldv-regression/test_union_cast-1_true-unreach-call_true-termination.i true 2 wit inspect 4.8 280 41 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 5.3   260  
ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i true 2 wit inspect 4.9 280 44 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.9   250  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call.i true 2 wit inspect 4.7 280 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 5.1   260  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call_1.i true 2 wit inspect 6.7 350 44 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 5.3   260  
ldv-regression/test_union_true-termination.c_true-unreach-call.i true 2 wit inspect 4.6 290 41 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 5.0   260  
ldv-regression/test_union_true-termination.c_true-unreach-call_1.i true 2 wit inspect 4.7 280 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 4.9   260  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call.i true 2 wit inspect 5.2 290 43 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 5.9   270  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i true 2 wit inspect 5.2 290 39 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 5.9   270  
ldv-regression/test02_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.2 240 37 false(unreach-call) 1 wit inspect 4.0  260 false(unreach-call) 1 wit inspect 3.2   220   unknown 0 wit inspect 3.6  180 false(unreach-call) 1 wit inspect .70   18    - wit inspect - wit inspect
ldv-regression/test06_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 6.5 320 52 true -32 wit inspect 3.1  250 false(unreach-call) 1 wit inspect 5.8   280   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
ldv-regression/test08_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.5 250 35 false(unreach-call) 1 wit inspect 5.2  280 false(unreach-call) 1 wit inspect 6.1   270   unknown 0 wit inspect 3.8  190 false(unreach-call) 1 wit inspect .64   18    - wit inspect - wit inspect
ldv-regression/test12_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.2 250 36 false(unreach-call) 1 wit inspect 3.9  260 false(unreach-call) 1 wit inspect 4.5   220   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .67   18    - wit inspect - wit inspect
ldv-regression/test21_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.7 260 42 true -32 wit inspect 4.3  260 false(unreach-call) 1 wit inspect 6.8   260   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .75   18    - wit inspect - wit inspect
ldv-regression/test22_false-unreach-call.c false(unreach-call) 1 wit inspect 8.9 470 76 true -32 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 7.1   450   unknown 0 wit inspect 3.1  210 true -32 wit inspect .69   18    - wit inspect - wit inspect
ldv-regression/test23_false-unreach-call.c false(unreach-call) 0 wit inspect 130   1200 1500 true -32 wit inspect 4.0  260 out of memory 0 wit inspect 76     7000   unknown 0 wit inspect 2.8  180 true -32 wit inspect .78   19    - wit inspect - wit inspect
ldv-regression/test24_false-unreach-call.c false(unreach-call) 1 wit inspect 37   740 370 false(unreach-call) 1 wit inspect 4.0  280 out of memory 0 wit inspect 56     7000   unknown 0 wit inspect 3.5  210 true -32 wit inspect .60   19    - wit inspect - wit inspect
ldv-regression/test25_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 89   870 920 false(unreach-call) 1 wit inspect 5.1  280 out of memory 0 wit inspect 49     7000   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .69   19    - wit inspect - wit inspect
ldv-regression/test26_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.4 250 34 false(unreach-call) 1 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 4.8   260   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/test27_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 49   580 530 false(unreach-call) 1 wit inspect 3.8  270 out of memory 0 wit inspect 75     7000   unknown 0 wit inspect 3.3  180 error (2) 0 wit inspect .65   19    - wit inspect - wit inspect
ldv-regression/test28_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 5.8 310 50 false(unreach-call) 1 wit inspect 4.3  260 false(unreach-call) 1 wit inspect 4.4   280   unknown 0 wit inspect 2.9  180 false(unreach-call) 1 wit inspect .76   18    - wit inspect - wit inspect
ldv-regression/test29_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 5.3 280 42 false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 6.6   260   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .69   18    - wit inspect - wit inspect
ldv-regression/test30_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.6 260 35 true -32 wit inspect 3.0  250 false(unreach-call) 1 wit inspect 5.7   280   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .77   18    - wit inspect - wit inspect
ldv-regression/test01_true-unreach-call_true-termination.c true 2 wit inspect 4.8 290 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 5.5   260  
ldv-regression/test03_true-unreach-call_true-termination.c true 2 wit inspect 5.7 320 51 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 6.6   270  
ldv-regression/test04_true-unreach-call_true-termination.c true 2 wit inspect 5.7 320 44 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  240 true 2 wit inspect 7.1   270  
ldv-regression/test05_true-unreach-call_true-termination.c true 2 wit inspect 8.3 520 63 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 13     510  
ldv-regression/test07_true-unreach-call_true-termination.c true 2 wit inspect 9.0 410 84 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 9.2   360  
ldv-regression/test09_true-unreach-call_true-termination.c true 2 wit inspect 7.2 370 62 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  270 true 2 wit inspect 9.0   330  
ldv-regression/test10_true-unreach-call_true-termination.c true 2 wit inspect 11   700 96 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 12     490  
ldv-regression/test11_true-unreach-call_true-termination.c true 2 wit inspect 6.1 300 55 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  250 true 2 wit inspect 7.6   270  
ldv-regression/test13_true-unreach-call_true-termination.c true 2 wit inspect 5.1 280 46 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 5.5   260  
ldv-regression/test14_true-unreach-call_true-termination.c true 2 wit inspect 5.9 290 48 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 7.4   270  
ldv-regression/test15_true-unreach-call_true-termination.c true 2 wit inspect 6.2 330 58 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 8.3   280  
ldv-regression/test16_true-unreach-call_true-termination.c true 2 wit inspect 6.5 340 57 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 7.6   280  
ldv-regression/test17_true-unreach-call_true-termination.c true 2 wit inspect 4.6 280 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 6.5   240  
ldv-regression/test18_true-unreach-call_true-termination.c true 2 wit inspect 6.4 350 53 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 8.1   300  
ldv-regression/test19_true-unreach-call_true-termination.c true 2 wit inspect 7.6 490 63 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 9.9   370  
ldv-regression/test20_true-unreach-call_true-termination.c true 2 wit inspect 4.9 280 43 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.5   270  
ldv-regression/test21_true-unreach-call_true-termination.c true 2 wit inspect 6.6 370 54 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 7.5   310  
ldv-regression/test22_true-unreach-call.c true 2 wit inspect 17   700 170 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.4  300 true 2 wit inspect 23     640  
ldv-regression/test23_true-unreach-call.c true 2 wit inspect 250   830 3300 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.1  320 error (7) 0 wit inspect 7.1   210  
ldv-regression/test24_true-unreach-call_true-termination.c true 2 wit inspect 8.3 460 71 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.9  280 true 2 wit inspect 9.2   410  
ldv-regression/test25_true-unreach-call.c true 2 wit inspect 22   610 240 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 16    460 error (7) 0 wit inspect 8.5   210  
ldv-regression/test26_true-unreach-call_true-termination.c true 2 wit inspect 6.2 340 48 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 9.3   270  
ldv-regression/test27_true-unreach-call_true-termination.c true 2 wit inspect 130   850 1400 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 29    500 true 2 wit inspect 170     790  
ldv-regression/test28_true-unreach-call_true-termination.c true 2 wit inspect 5.9 300 51 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 7.7   270  
ldv-regression/test29_true-unreach-call_true-termination.c true 2 wit inspect 5.5 280 44 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 8.3   260  
ldv-regression/test30_true-unreach-call_true-termination.c true 2 wit inspect 8.7 470 74 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 9.4   460  
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 320   1200 1700 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0015 .29 - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 320   1200 1600 error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0012 .35 - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 320   1200 2600 error (invalid witness file) 0 wit inspect .63 45 error (2) 0 wit inspect .049 4.8 error (invalid witness file) 0 wit inspect .93 49 error (invalid witness file) 0 wit inspect .0016 .27 - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 9.6 510 74 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.8  280 true 2 wit inspect 13     480  
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 9.2 500 76 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.0  300 true 2 wit inspect 12     450  
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 9.8 510 72 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.4  290 true 2 wit inspect 12     440  
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 10   520 85 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.4  290 true 2 wit inspect 14     460  
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 10   520 81 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.6  280 true 2 wit inspect 12     440  
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 9.9 520 83 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.7  280 true 2 wit inspect 14     440  
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 9.7 520 70 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.1  280 true 2 wit inspect 12     440  
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 10   520 78 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.7  290 true 2 wit inspect 12     470  
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 10   530 76 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.3  280 true 2 wit inspect 12     440  
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 10   510 87 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.8  280 true 2 wit inspect 15     450  
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 14   560 110 false(unreach-call) 1 wit inspect 3.8  270 false(unreach-call) 1 wit inspect 9.6   350   unknown 0 wit inspect 4.2  210 false(unreach-call) 1 wit inspect .77   18    - wit inspect - wit inspect
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 8.9 500 76 false(unreach-call) 1 wit inspect 4.4  290 false(unreach-call) 1 wit inspect 9.0   350   unknown 0 wit inspect 3.7  210 false(unreach-call) 1 wit inspect .71   18    - wit inspect - wit inspect
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 5.8 280 46 false(unreach-call) 1 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 4.3   290   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .82   18    - wit inspect - wit inspect
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 77   1100 880 false(unreach-call) 1 wit inspect 4.3  270 false(unreach-call) 1 wit inspect 7.7   340   unknown 0 wit inspect 3.7  220 true -32 wit inspect .67   19    - wit inspect - wit inspect
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 7.2 300 57 false(unreach-call) 1 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 6.6   280   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .66   18    - wit inspect - wit inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(unreach-call) 1 wit inspect 50   1000 470 false(unreach-call) 1 wit inspect 4.6  270 false(unreach-call) 1 wit inspect 8.6   300   unknown 0 wit inspect 3.5  210 true -32 wit inspect .82   19    - wit inspect - wit inspect
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 5.4 290 46 true -32 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 6.3   280   unknown 0 wit inspect 4.1  210 false(unreach-call) 1 wit inspect .64   18    - wit inspect - wit inspect
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 7.6 350 62 false(unreach-call) 1 wit inspect 5.3  270 false(unreach-call) 1 wit inspect 8.2   300   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .86   18    - wit inspect - wit inspect
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 23   540 220 false(unreach-call) 1 wit inspect 4.3  270 false(unreach-call) 1 wit inspect 6.4   280   unknown 0 wit inspect 3.6  210 false(unreach-call) 1 wit inspect .74   18    - wit inspect - wit inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 21   720 170 false(unreach-call) 1 wit inspect 4.0  270 false(unreach-call) 1 wit inspect 10     330   unknown 0 wit inspect 3.9  210 error (2) 0 wit inspect .71   19    - wit inspect - wit inspect
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 55   920 630 false(unreach-call) 1 wit inspect 4.5  290 false(unreach-call) 1 wit inspect 6.1   310   unknown 0 wit inspect 3.5  220 true -32 wit inspect .88   19    - wit inspect - wit inspect
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 9.2 470 66 false(unreach-call) 1 wit inspect 5.1  270 false(unreach-call) 1 wit inspect 10     360   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .66   18    - wit inspect - wit inspect
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 5.4 280 41 false(unreach-call) 1 wit inspect 4.7  280 false(unreach-call) 1 wit inspect 6.3   280   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .74   18    - wit inspect - wit inspect
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i error (7) 0 wit inspect 150   800 2000 error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .023 5.0 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0021 .30 - wit inspect - wit inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 6.5 290 53 false(unreach-call) 1 wit inspect 4.0  260 false(unreach-call) 1 wit inspect 4.2   290   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .67   18    - wit inspect - wit inspect
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i