Tool skink 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* [apollon077; apollon078; apollon155] [apollon030; apollon077; apollon078] [apollon077; apollon078] 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] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 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] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 4, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33554 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-01 22:03:39 CET 2017-12-02 00:36:21 CET 2017-12-02 01:00:42 CET 2017-12-02 01:03:22 CET 2017-12-02 01:04:20 CET 2017-12-02 00:04:19 CET 2017-12-02 00:40:05 CET
Run set skink.sv-comp18.ReachSafety-Heap cpa-seq-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-Heap uautomizer-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-skink.sv-comp18-violation-witness.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-skink.sv-comp18-correctness-witness.ReachSafety-Heap uautomizer-validate-correctness-witnesses-skink.sv-comp18-correctness-witness.ReachSafety-Heap
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/skink.2017-12-01_2203.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/skink.2017-12-01_2203.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/skink.2017-12-01_2203.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/skink.2017-12-01_2203.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/skink.2017-12-01_2203.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/skink.2017-12-01_2203.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 unknown 0 wit inspect 8.2 470 64 error (invalid witness file) 0 wit inspect .61 44 error (2) 0 wit inspect .039 4.9 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect - wit inspect
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 12   680 89 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 8.4 410 77 error (invalid witness file) 0 wit inspect .72 42 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0020 .26 - wit inspect - wit inspect
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 8.4 470 73 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0013 .28 - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-deref.i unknown 0 wit inspect 7.4 370 68 error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0037 .30 - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 7.2 370 57 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .021 5.0 error (invalid witness file) 0 wit inspect .69 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 8.4 460 71 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .020 4.9
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 6.6 330 56 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 5.0
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 13   710 97 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .39 43 error (2) 0 wit inspect .027 4.8
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 7.0 390 60 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .44 43 error (2) 0 wit inspect .019 4.9
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 8.3 460 69 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .023 4.8
heap-manipulation/tree_true-unreach-call.i unknown 0 wit inspect 7.7 390 65 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.8
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 6.0 320 57 error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .023 5.0 error (invalid witness file) 0 wit inspect .87 47 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
list-properties/list_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 6.1 310 52 error (invalid witness file) 0 wit inspect .69 45 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .83 47 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 6.6 330 48 error (invalid witness file) 0 wit inspect .39 41 error (2) 0 wit inspect .023 5.0 error (invalid witness file) 0 wit inspect .82 47 error (invalid witness file) 0 wit inspect .0035 .32 - wit inspect - wit inspect
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 5.3 300 51 error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0010 .26 - wit inspect - wit inspect
list-properties/simple_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 5.8 310 58 error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0026 .26 - wit inspect - wit inspect
list-properties/splice_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 6.4 340 61 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .039 5.0 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 6.3 330 58 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .021 4.8
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 6.5 320 58 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .021 4.9
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 6.5 340 57 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .019 5.0
list-properties/list_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 6.7 320 52 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .025 4.8
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 5.4 310 52 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .019 4.9
list-properties/simple_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 5.7 320 50 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .47 43 error (2) 0 wit inspect .019 4.8
list-properties/splice_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 6.4 320 50 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .021 4.8
ldv-regression/1_3_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 5.0 300 48 false(unreach-call) 1 wit inspect 4.0  260 true -32 wit inspect 3.3   250   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
ldv-regression/alt_test_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 5.5 320 51 false(unreach-call) 1 wit inspect 4.4  270 true -32 wit inspect 5.0   230   unknown 0 wit inspect 2.5  210 false(unreach-call) 1 wit inspect .69   18    - wit inspect - wit inspect
ldv-regression/callfpointer_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 5.1 290 51 false(unreach-call) 1 wit inspect 2.2  260 false(unreach-call) 1 wit inspect 3.1   230   unknown 0 wit inspect 2.6  180 false(unreach-call) 1 wit inspect .55   18    - wit inspect - wit inspect
ldv-regression/fo_test_true-termination.c_false-unreach-call.i unknown 0 wit inspect 4.2 320 44 error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0036 .28 - wit inspect - wit inspect
ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 5.1 300 51 false(unreach-call) 1 wit inspect 4.0  250 true -32 wit inspect 3.8   260   unknown 0 wit inspect 2.6  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/mutex_lock_struct_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 5.2 320 52 false(unreach-call) 1 wit inspect 3.2  260 true -32 wit inspect 4.7   260   unknown 0 wit inspect 2.7  190 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
ldv-regression/recursive_list_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 5.3 310 45 false(unreach-call) 1 wit inspect 3.3  260 true -32 wit inspect 4.9   230   unknown 0 wit inspect 2.0  200 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
ldv-regression/rule57_ebda_blast_true-termination.c_false-unreach-call.i unknown 0 wit inspect 6.3 310 59 error (invalid witness file) 0 wit inspect .52 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .65 50 error (invalid witness file) 0 wit inspect .0038 .28 - wit inspect - wit inspect
ldv-regression/rule60_list2_true-termination.c_false-unreach-call_1.i unknown 0 wit inspect 5.4 300 50 error (invalid witness file) 0 wit inspect .65 42 error (2) 0 wit inspect .036 4.9 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
ldv-regression/stateful_check_false-unreach-call_false-termination.i unknown 0 wit inspect 39   700 370 error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0036 .29 - wit inspect - wit inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 5.1 310 42 false(unreach-call) 1 wit inspect 3.2  260 true -32 wit inspect 5.0   260   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .60   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 280 49 false(unreach-call) 1 wit inspect 3.0  260 true -32 wit inspect 3.3   270   unknown 0 wit inspect 2.6  190 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call.i true 2 wit inspect 3.9 260 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 7.6   280  
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i true 2 wit inspect 4.1 250 39 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 7.1   260  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call.i true 2 wit inspect 4.0 240 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 5.9   270  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call_1.i true 2 wit inspect 3.6 240 33 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 5.6   250  
ldv-regression/ex3_forlist_true-termination.c_true-unreach-call.i unknown 0 wit inspect 5.8 300 51 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .019 4.9
ldv-regression/just_assert_true-termination.c_true-unreach-call.i true 2 wit inspect 3.7 230 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 4.4   220  
ldv-regression/mutex_lock_int_true-termination.c_true-unreach-call_1.i true 2 wit inspect 3.8 260 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 6.5   260  
ldv-regression/mutex_lock_struct_true-termination.c_true-unreach-call_1.i true 2 wit inspect 4.4 270 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 6.2   270  
ldv-regression/nested_structure_noptr_true-termination.c_true-unreach-call.i true 2 wit inspect 4.0 240 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 5.0   250  
ldv-regression/nested_structure_noptr_true-unreach-call_true-termination.i true 2 wit inspect 3.9 240 39 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 5.9   260  
ldv-regression/nested_structure_ptr_true-termination.c_true-unreach-call.i true 2 wit inspect 4.0 240 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 9.6   470  
ldv-regression/nested_structure_ptr_true-unreach-call_true-termination.i true 2 wit inspect 3.7 240 31 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.5  250 true 2 wit inspect 9.8   410  
ldv-regression/nested_structure_true-termination.c_true-unreach-call.i true 2 wit inspect 3.9 250 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 7.4   280  
ldv-regression/nested_structure_true-unreach-call_true-termination.i true 2 wit inspect 4.0 240 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 8.3   280  
ldv-regression/oomInt_true-termination.c_true-unreach-call.i true 2 wit inspect 4.1 260 41 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 5.7   260  
ldv-regression/oomInt_true-termination.c_true-unreach-call_1.i true 2 wit inspect 3.9 260 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.2   260  
ldv-regression/rule57_ebda_blast_true-termination.c_true-unreach-call_1.i unknown 0 wit inspect 7.0 350 62 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .018 4.9
ldv-regression/rule60_list2_true-termination.c_true-unreach-call.i unknown 0 wit inspect 6.0 330 55 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 42 error (2) 0 wit inspect .020 4.8
ldv-regression/rule60_list_true-termination.c_true-unreach-call.i true 2 wit inspect 3.9 240 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  260 true 2 wit inspect 10     370  
ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i true 2 wit inspect 4.2 260 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 5.8   260  
ldv-regression/structure_assignment_true-termination.c_true-unreach-call.i true 2 wit inspect 4.0 240 34 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 5.7   260  
ldv-regression/test_address_true-termination.c_true-unreach-call.i true 2 wit inspect 4.3 250 39 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 5.5   260  
ldv-regression/test_cut_trace_true-termination.c_true-unreach-call.i true 2 wit inspect 3.9 240 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 5.4   260  
ldv-regression/test_malloc-1_true-unreach-call_true-termination.i true 2 wit inspect 4.0 240 39 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 5.7   260  
ldv-regression/test_malloc-2_true-unreach-call_true-termination.i true 2 wit inspect 3.9 240 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 6.4   260  
ldv-regression/test_overflow_true-termination.c_true-unreach-call.i true 2 wit inspect 5.4 310 44 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 5.0   260  
ldv-regression/test_union_cast-1_true-unreach-call_true-termination.i true 2 wit inspect 4.0 240 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.2   260  
ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i true 2 wit inspect 3.9 240 33 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 6.3   260  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call.i true 2 wit inspect 3.8 240 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 5.5   250  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call_1.i true 2 wit inspect 4.0 240 34 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 5.6   260  
ldv-regression/test_union_true-termination.c_true-unreach-call.i true 2 wit inspect 4.1 250 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  240 true 2 wit inspect 5.5   260  
ldv-regression/test_union_true-termination.c_true-unreach-call_1.i true 2 wit inspect 4.2 290 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.8   260  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call.i true 2 wit inspect 5.2 300 49 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 6.8   270  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i true 2 wit inspect 3.9 230 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.3  250 true 2 wit inspect 7.5   270  
ldv-regression/test02_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 5.2 290 45 false(unreach-call) 1 wit inspect 3.8  260 false(unreach-call) 1 wit inspect 4.8   220   unknown 0 wit inspect 2.8  190 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
ldv-regression/test06_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 5.1 310 53 false(unreach-call) 1 wit inspect 2.3  260 true -32 wit inspect 5.0   230   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/test08_false-unreach-call_true-termination.c unknown 0 wit inspect 4.7 290 45 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0021 .26 - wit inspect - wit inspect
ldv-regression/test12_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.9 300 44 false(unreach-call) 1 wit inspect 3.9  260 false(unreach-call) 1 wit inspect 3.9   230   unknown 0 wit inspect 2.6  180 false(unreach-call) 1 wit inspect .55   18    - wit inspect - wit inspect
ldv-regression/test21_false-unreach-call_true-termination.c unknown 0 wit inspect 5.5 320 50 error (invalid witness file) 0 wit inspect .66 42 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0038 .26 - wit inspect - wit inspect
ldv-regression/test22_false-unreach-call.c unknown 0 wit inspect 5.4 310 42 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .88 48 error (invalid witness file) 0 wit inspect .0032 .29 - wit inspect - wit inspect
ldv-regression/test23_false-unreach-call.c unknown 0 wit inspect 5.6 320 48 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .017 4.8 error (invalid witness file) 0 wit inspect .69 50 error (invalid witness file) 0 wit inspect .0011 .28 - wit inspect - wit inspect
ldv-regression/test24_false-unreach-call.c unknown 0 wit inspect 7.4 420 61 error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .81 47 error (invalid witness file) 0 wit inspect .0035 .26 - wit inspect - wit inspect
ldv-regression/test25_false-unreach-call_true-termination.c unknown 0 wit inspect 6.7 360 59 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .040 4.8 error (invalid witness file) 0 wit inspect .64 50 error (invalid witness file) 0 wit inspect .0018 .29 - wit inspect - wit inspect
ldv-regression/test26_false-unreach-call_true-termination.c unknown 0 wit inspect 4.8 290 41 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect - wit inspect
ldv-regression/test27_false-unreach-call_true-termination.c unknown 0 wit inspect 6.5 320 54 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .64 49 error (invalid witness file) 0 wit inspect .0011 .29 - wit inspect - wit inspect
ldv-regression/test28_false-unreach-call_true-termination.c unknown 0 wit inspect 5.3 310 43 error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect .82 47 error (invalid witness file) 0 wit inspect .0036 .26 - wit inspect - wit inspect
ldv-regression/test29_false-unreach-call_true-termination.c unknown 0 wit inspect 5.4 300 48 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .044 4.9 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0011 .29 - wit inspect - wit inspect
ldv-regression/test30_false-unreach-call_true-termination.c unknown 0 wit inspect 4.9 290 44 error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .86 48 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
ldv-regression/test01_true-unreach-call_true-termination.c true 2 wit inspect 3.8 230 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 5.5   250  
ldv-regression/test03_true-unreach-call_true-termination.c true 2 wit inspect 3.7 240 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 6.7   270  
ldv-regression/test04_true-unreach-call_true-termination.c true 2 wit inspect 3.7 240 33 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 6.8   300  
ldv-regression/test05_true-unreach-call_true-termination.c true 2 wit inspect 4.1 260 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 11     480  
ldv-regression/test07_true-unreach-call_true-termination.c true 2 wit inspect 4.1 270 43 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 8.6   350  
ldv-regression/test09_true-unreach-call_true-termination.c true 2 wit inspect 4.1 250 39 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 8.6   340  
ldv-regression/test10_true-unreach-call_true-termination.c unknown 0 wit inspect 5.1 290 44 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .49 43 error (2) 0 wit inspect .019 5.0
ldv-regression/test11_true-unreach-call_true-termination.c true 2 wit inspect 4.0 250 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  260 true 2 wit inspect 7.3   270  
ldv-regression/test13_true-unreach-call_true-termination.c unknown 0 wit inspect 4.9 290 39 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .024 5.0
ldv-regression/test14_true-unreach-call_true-termination.c true 2 wit inspect 4.0 250 41 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 8.2   280  
ldv-regression/test15_true-unreach-call_true-termination.c true 2 wit inspect 4.0 250 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 8.1   280  
ldv-regression/test16_true-unreach-call_true-termination.c true 2 wit inspect 4.2 260 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 8.8   300  
ldv-regression/test17_true-unreach-call_true-termination.c true 2 wit inspect 3.9 240 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.4  250 true 2 wit inspect 5.3   260  
ldv-regression/test18_true-unreach-call_true-termination.c true 2 wit inspect 3.8 240 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 8.7   300  
ldv-regression/test19_true-unreach-call_true-termination.c true 2 wit inspect 4.0 240 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 9.3   350  
ldv-regression/test20_true-unreach-call_true-termination.c true 2 wit inspect 3.6 240 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 5.8   260  
ldv-regression/test21_true-unreach-call_true-termination.c true 2 wit inspect 4.4 290 41 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 8.0   300  
ldv-regression/test22_true-unreach-call.c true 2 wit inspect 4.3 290 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.2  310 true 2 wit inspect 21     630  
ldv-regression/test23_true-unreach-call.c true 2 wit inspect 4.7 300 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.4  320 true 2 wit inspect 260     680  
ldv-regression/test24_true-unreach-call_true-termination.c true 2 wit inspect 4.1 350 42 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3  280 true 2 wit inspect 9.4   410  
ldv-regression/test25_true-unreach-call.c true 2 wit inspect 4.5 380 43 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 20    470 true 2 wit inspect 30     530  
ldv-regression/test26_true-unreach-call_true-termination.c true 2 wit inspect 4.0 250 41 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 8.5   290  
ldv-regression/test27_true-unreach-call_true-termination.c true 2 wit inspect 4.3 270 44 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 33    500 true 2 wit inspect 160     820  
ldv-regression/test28_true-unreach-call_true-termination.c unknown 0 wit inspect 5.5 310 53 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .42 43 error (2) 0 wit inspect .020 4.9
ldv-regression/test29_true-unreach-call_true-termination.c unknown 0 wit inspect 5.6 330 57 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 41 error (2) 0 wit inspect .026 4.8
ldv-regression/test30_true-unreach-call_true-termination.c unknown 0 wit inspect 5.5 310 49 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .46 44 error (2) 0 wit inspect .019 4.8
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 27   940 150 error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .66 50 error (invalid witness file) 0 wit inspect .0017 .26 - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 28   920 190 error (invalid witness file) 0 wit inspect .42 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0036 .26 - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 29   960 160 error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 24   890 130 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.4  280 true 2 wit inspect 13     430  
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 24   920 140 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.3  280 true 2 wit inspect 11     430  
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 25   920 150 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  290 true 2 wit inspect 13     420  
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 24   910 150 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1  280 true 2 wit inspect 14     440  
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 23   920 140 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.6  280 true 2 wit inspect 12     420  
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 24   890 150 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.4  280 true 2 wit inspect 13     430  
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 25   920 150 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  300 true 2 wit inspect 13     430  
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 25   920 160 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.4  290 true 2 wit inspect 13     420  
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 24   910 150 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1  280 true 2 wit inspect 16     430  
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 24   930 150 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.9  280 true 2 wit inspect 12     430  
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 6.9 360 54 error (invalid witness file) 0 wit inspect .40 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0011 .29 - wit inspect - wit inspect
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 6.6 320 60 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .82 47 error (invalid witness file) 0 wit inspect .0011 .29 - wit inspect - wit inspect
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 6.7 370 60 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0028 .34 - wit inspect - wit inspect
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 6.9 390 57 error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .046 5.0 error (invalid witness file) 0 wit inspect .68 52 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i unknown 0 wit inspect 6.9 330 57 error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .89 48 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 7.1 390 59 error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 6.8 350 58 error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .017 4.8 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0010 .26 - wit inspect - wit inspect
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 7.5 400 64 error (invalid witness file) 0 wit inspect .39 40 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0037 .29 - wit inspect - wit inspect
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 6.7 350 58 error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .70 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i unknown 0 wit inspect 6.6 330 55 error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .67 50 error (invalid witness file) 0 wit inspect .0013 .30 - wit inspect - wit inspect
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 7.3 380 64 error (invalid witness file) 0 wit inspect .63 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 6.1 320 54 error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .040 4.8 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0023 .26 - wit inspect - wit inspect
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 6.7 350 52 error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .033 4.8 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0014 .28 - wit inspect - wit inspect
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 7.0 380 63 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .86 47 error (invalid witness file) 0 wit inspect .0037 .26 - wit inspect - wit inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i unknown 0 wit inspect 6.0 310 55 error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 6.1 330 48 error (invalid witness file) 0 wit inspect .64 42 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .84 48 error (invalid witness file) 0 wit inspect .0036 .30 - wit inspect - wit inspect
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 6.7 330 57 error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .64 51 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 6.6 330 56 error (invalid witness file) 0 wit