Tool ULTIMATE Taipan 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 17:23:13 CET 2017-12-03 07:22:17 CET 2017-12-03 07:45:29 CET 2017-12-03 07:47:53 CET 2017-12-03 07:50:34 CET 2017-12-03 06:47:45 CET 2017-12-03 07:25:40 CET
Run set utaipan.sv-comp18.ReachSafety-Heap cpa-seq-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-Heap uautomizer-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-utaipan.sv-comp18-violation-witness.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.ReachSafety-Heap uautomizer-validate-correctness-witnesses-utaipan.sv-comp18-correctness-witness.ReachSafety-Heap
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-02_1723.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/utaipan.2017-12-02_1723.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-02_1723.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/utaipan.2017-12-02_1723.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/utaipan.2017-12-02_1723.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/utaipan.2017-12-02_1723.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 error (7) 0 wit inspect 51   900 540 error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .049 4.9 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   1500 8700 error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0029 .29 - wit inspect - wit inspect
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 11   480 91 true -32 wit inspect 3.9  260 false(unreach-call) 1 wit inspect 7.8   320   unknown 0 wit inspect 3.4  220 true -32 wit inspect .67   19    - wit inspect - wit inspect
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i error (7) 0 wit inspect 180   890 2300 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .049 4.9 error (invalid witness file) 0 wit inspect .82 47 error (invalid witness file) 0 wit inspect .0020 .35 - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-deref.i error (7) 0 wit inspect 740   820 8900 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .047 4.9 error (invalid witness file) 0 wit inspect .82 49 error (invalid witness file) 0 wit inspect .0017 .31 - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i error (7) 0 wit inspect 84   890 830 error (invalid witness file) 0 wit inspect .50 41 error (2) 0 wit inspect .047 4.8 error (invalid witness file) 0 wit inspect .90 50 error (invalid witness file) 0 wit inspect .0041 .30 - wit inspect - wit inspect
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i error (7) 0 wit inspect 50   890 500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .025 4.9
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i error (7) 0 wit inspect 500   790 6400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .023 4.8
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   1300 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .019 4.8
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   1300 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 44 error (2) 0 wit inspect .049 4.9
heap-manipulation/sll_to_dll_rev_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 .59 41 error (2) 0 wit inspect .018 4.9
heap-manipulation/tree_true-unreach-call.i error (7) 0 wit inspect 420   980 6000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 42 error (2) 0 wit inspect .018 4.9
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 6.2 290 56 true -32 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 5.3   270   unknown 0 wit inspect 3.2  210 true -32 wit inspect .64   19    - wit inspect - wit inspect
list-properties/list_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   1300 12000 error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .80 50 error (invalid witness file) 0 wit inspect .0017 .31 - wit inspect - wit inspect
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 7.0 310 62 true -32 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 5.2   260   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .66   18    - wit inspect - wit inspect
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 240   1200 2800 true -32 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 22     690   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .63   19    - wit inspect - wit inspect
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 8.8 540 84 true -32 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 5.3   260   unknown 0 wit inspect 3.1  210 true -32 wit inspect .65   19    - wit inspect - wit inspect
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 7.3 320 57 true -32 wit inspect 3.8  260 false(unreach-call) 1 wit inspect 5.9   280   unknown 0 wit inspect 3.3  220 true -32 wit inspect .63   19    - wit inspect - wit inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   940 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .051 4.9
list-properties/list_flag_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 .50 41 error (2) 0 wit inspect .019 4.9
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 910   13000 3900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .018 4.8
list-properties/list_true-unreach-call_false-valid-memtrack.i error (7) 0 wit inspect 690   1100 8300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .019 4.9
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i error (7) 0 wit inspect 470   920 5500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .019 4.8
list-properties/simple_true-unreach-call_false-valid-memtrack.i error (7) 0 wit inspect 200   930 2500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .049 4.9
list-properties/splice_true-unreach-call_false-valid-memtrack.i error (7) 0 wit inspect 190   1600 2000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .018 4.8
ldv-regression/1_3_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 5.5 290 50 true -32 wit inspect 3.1  250 false(unreach-call) 1 wit inspect 4.9   260   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .58   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 3.5  260 false(unreach-call) 1 wit inspect 6.4   280   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .66   18    - wit inspect - wit inspect
ldv-regression/callfpointer_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 4.1 240 34 true -32 wit inspect 2.9  260 false(unreach-call) 1 wit inspect 4.6   240   unknown 0 wit inspect 2.6  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/fo_test_true-termination.c_false-unreach-call.i unknown 0 wit inspect 10   300 87 error (invalid witness file) 0 wit inspect .56 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 .0029 .26 - wit inspect - wit inspect
ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 5.1 290 36 true -32 wit inspect 2.8  260 false(unreach-call) 1 wit inspect 4.6   250   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/mutex_lock_struct_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 4.8 290 40 true -32 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 5.8   320   unknown 0 wit inspect 2.6  180 false(unreach-call) 1 wit inspect .59   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 41 true -32 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 5.0   270   unknown 0 wit inspect 2.7  190 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/rule57_ebda_blast_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 5.8 290 54 true -32 wit inspect 3.2  250 false(unreach-call) 1 wit inspect 6.0   270   unknown 0 wit inspect 2.9  210 error (2) 0 wit inspect .61   19    - wit inspect - wit inspect
ldv-regression/rule60_list2_true-termination.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect 80   1400 740 true -32 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 5.4   270   unknown 0 wit inspect 3.1  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 15   600 150 true -32 wit inspect 4.9  260 false(unreach-call) 1 wit inspect 5.6   290   unknown 0 wit inspect 3.4  210 true -32 wit inspect .60   19    - wit inspect - wit inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 6.2 310 51 true -32 wit inspect 2.9  250 false(unreach-call) 1 wit inspect 4.5   250   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .59   19    - wit inspect - wit inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect 5.3 290 47 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 4.3   240   unknown 0 wit inspect 2.6  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call.i true 2 wit inspect 5.1 290 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 6.1   280  
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i true 2 wit inspect 4.7 290 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 5.8   260  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call.i true 2 wit inspect 5.0 290 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  260 true 2 wit inspect 5.5   270  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call_1.i true 2 wit inspect 4.6 280 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 5.4   260  
ldv-regression/ex3_forlist_true-termination.c_true-unreach-call.i true 2 wit inspect 40   960 330 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 16    410 true 2 wit inspect 28     680  
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 2.8  240 true 2 wit inspect 3.2   220  
ldv-regression/mutex_lock_int_true-termination.c_true-unreach-call_1.i true 2 wit inspect 5.4 290 44 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 6.0   260  
ldv-regression/mutex_lock_struct_true-termination.c_true-unreach-call_1.i true 2 wit inspect 5.1 290 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 6.0   260  
ldv-regression/nested_structure_noptr_true-termination.c_true-unreach-call.i true 2 wit inspect 4.4 280 34 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.8  240 true 2 wit inspect 5.1   240  
ldv-regression/nested_structure_noptr_true-unreach-call_true-termination.i true 2 wit inspect 4.8 280 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 5.4   260  
ldv-regression/nested_structure_ptr_true-termination.c_true-unreach-call.i true 2 wit inspect 5.6 320 49 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 9.1   480  
ldv-regression/nested_structure_ptr_true-unreach-call_true-termination.i true 2 wit inspect 5.7 320 41 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 8.6   410  
ldv-regression/nested_structure_true-termination.c_true-unreach-call.i true 2 wit inspect 5.2 290 41 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 8.3   300  
ldv-regression/nested_structure_true-unreach-call_true-termination.i true 2 wit inspect 5.1 290 49 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  260 true 2 wit inspect 7.7   290  
ldv-regression/oomInt_true-termination.c_true-unreach-call.i true 2 wit inspect 5.1 290 41 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  260 true 2 wit inspect 5.4   260  
ldv-regression/oomInt_true-termination.c_true-unreach-call_1.i true 2 wit inspect 4.7 290 34 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 4.5   250  
ldv-regression/rule57_ebda_blast_true-termination.c_true-unreach-call_1.i true 2 wit inspect 6.3 300 52 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 6.3   260  
ldv-regression/rule60_list2_true-termination.c_true-unreach-call.i true 2 wit inspect 86   1400 780 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  260 true 2 wit inspect 22     670  
ldv-regression/rule60_list_true-termination.c_true-unreach-call.i true 2 wit inspect 7.4 360 67 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3  250 true 2 wit inspect 8.6   380  
ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i true 2 wit inspect 4.7 270 42 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  250 true 2 wit inspect 4.9   260  
ldv-regression/structure_assignment_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 2.9  250 true 2 wit inspect 4.9   260  
ldv-regression/test_address_true-termination.c_true-unreach-call.i true 2 wit inspect 5.0 280 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  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 290 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 4.8   260  
ldv-regression/test_malloc-1_true-unreach-call_true-termination.i true 2 wit inspect 5.1 290 43 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  250 true 2 wit inspect 5.7   270  
ldv-regression/test_malloc-2_true-unreach-call_true-termination.i true 2 wit inspect 4.8 290 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  250 true 2 wit inspect 6.1   260  
ldv-regression/test_overflow_true-termination.c_true-unreach-call.i true 2 wit inspect 5.0 280 41 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  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.7 290 38 - 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-2_true-unreach-call_true-termination.i true 2 wit inspect 4.9 290 42 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 5.5   260  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call.i true 2 wit inspect 5.0 280 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 4.9   260  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call_1.i true 2 wit inspect 4.6 280 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.1   270  
ldv-regression/test_union_true-termination.c_true-unreach-call.i true 2 wit inspect 4.4 270 39 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 4.6   260  
ldv-regression/test_union_true-termination.c_true-unreach-call_1.i true 2 wit inspect 4.7 280 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  240 true 2 wit inspect 4.6   260  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call.i true 2 wit inspect 4.5 280 34 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 6.2   280  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i true 2 wit inspect 4.7 280 39 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.6   260  
ldv-regression/test02_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.4 250 38 true -32 wit inspect 2.7  260 false(unreach-call) 1 wit inspect 4.6   220   unknown 0 wit inspect 2.6  180 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 6.0 300 50 true -32 wit inspect 2.8  260 false(unreach-call) 1 wit inspect 5.1   280   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/test08_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.6 280 39 true -32 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 4.9   260   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
ldv-regression/test12_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.3 250 34 true -32 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 4.4   230   unknown 0 wit inspect 2.6  180 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
ldv-regression/test21_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.7 280 41 true -32 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 5.3   260   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/test22_false-unreach-call.c false(unreach-call) 1 wit inspect 10   570 77 true -32 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 9.8   440   unknown 0 wit inspect 2.7  210 true -32 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/test23_false-unreach-call.c false(unreach-call) 0 wit inspect 260   3300 2700 true -32 wit inspect 3.1  260 timeout 0 wit inspect 98     6600   unknown 0 wit inspect 2.9  210 true -32 wit inspect .62   19    - wit inspect - wit inspect
ldv-regression/test24_false-unreach-call.c false(unreach-call) 0 wit inspect 120   830 1600 true -32 wit inspect 3.4  260 out of memory 0 wit inspect 56     7000   unknown 0 wit inspect 3.0  190 true -32 wit inspect .61   19    - wit inspect - wit inspect
ldv-regression/test25_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 36   790 330 true -32 wit inspect 3.1  250 out of memory 0 wit inspect 45     7000   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .60   19    - wit inspect - wit inspect
ldv-regression/test26_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.4 260 36 true -32 wit inspect 2.8  250 false(unreach-call) 1 wit inspect 4.8   250   unknown 0 wit inspect 2.6  180 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
ldv-regression/test27_false-unreach-call_true-termination.c false(unreach-call) 0 wit inspect 200   770 2200 true -32 wit inspect 3.2  260 out of memory 0 wit inspect 51     7000   unknown 0 wit inspect 2.8  210 error (2) 0 wit inspect .60   19    - wit inspect - wit inspect
ldv-regression/test28_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.4 360 55 true -32 wit inspect 3.0  250 false(unreach-call) 1 wit inspect 5.5   260   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/test29_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 5.3 290 42 true -32 wit inspect 2.8  250 false(unreach-call) 1 wit inspect 5.4   260   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
ldv-regression/test30_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 5.1 290 46 true -32 wit inspect 2.7  250 false(unreach-call) 1 wit inspect 5.2   260   unknown 0 wit inspect 2.6  190 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/test01_true-unreach-call_true-termination.c true 2 wit inspect 4.5 270 33 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 4.8   260  
ldv-regression/test03_true-unreach-call_true-termination.c true 2 wit inspect 5.3 300 43 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 6.7   270  
ldv-regression/test04_true-unreach-call_true-termination.c true 2 wit inspect 5.3 290 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 6.3   270  
ldv-regression/test05_true-unreach-call_true-termination.c true 2 wit inspect 7.4 390 58 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 9.6   490  
ldv-regression/test07_true-unreach-call_true-termination.c true 2 wit inspect 8.5 370 66 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 8.4   350  
ldv-regression/test09_true-unreach-call_true-termination.c true 2 wit inspect 6.4 300 53 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 7.8   340  
ldv-regression/test10_true-unreach-call_true-termination.c true 2 wit inspect 9.4 430 76 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 11     490  
ldv-regression/test11_true-unreach-call_true-termination.c true 2 wit inspect 5.7 290 47 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  270 true 2 wit inspect 7.2   280  
ldv-regression/test13_true-unreach-call_true-termination.c true 2 wit inspect 5.0 290 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 5.4   270  
ldv-regression/test14_true-unreach-call_true-termination.c true 2 wit inspect 5.4 290 45 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  260 true 2 wit inspect 6.7   270  
ldv-regression/test15_true-unreach-call_true-termination.c true 2 wit inspect 4.8 290 42 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 7.5   280  
ldv-regression/test16_true-unreach-call_true-termination.c true 2 wit inspect 5.4 300 46 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 7.5   280  
ldv-regression/test17_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.8  250 true 2 wit inspect 5.1   260  
ldv-regression/test18_true-unreach-call_true-termination.c true 2 wit inspect 6.2 320 49 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 7.3   310  
ldv-regression/test19_true-unreach-call_true-termination.c true 2 wit inspect 6.3 320 47 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 8.2   360  
ldv-regression/test20_true-unreach-call_true-termination.c true 2 wit inspect 4.8 290 42 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 5.4   260  
ldv-regression/test21_true-unreach-call_true-termination.c true 2 wit inspect 6.4 340 59 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 7.8   290  
ldv-regression/test22_true-unreach-call.c true 2 wit inspect 20   750 160 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.0  300 true 2 wit inspect 20     630  
ldv-regression/test23_true-unreach-call.c true 2 wit inspect 97   2900 1100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.5  320 true 2 wit inspect 230     780  
ldv-regression/test24_true-unreach-call_true-termination.c true 2 wit inspect 34   560 370 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5  280 true 2 wit inspect 9.4   420  
ldv-regression/test25_true-unreach-call.c true 2 wit inspect 34   730 360 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 18    360 error (7) 0 wit inspect 7.8   210  
ldv-regression/test26_true-unreach-call_true-termination.c true 2 wit inspect 5.9 320 49 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 7.3   300  
ldv-regression/test27_true-unreach-call_true-termination.c timeout 0 wit inspect 900   1100 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.8
ldv-regression/test28_true-unreach-call_true-termination.c true 2 wit inspect 5.8 290 50 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 7.1   270  
ldv-regression/test29_true-unreach-call_true-termination.c true 2 wit inspect 5.8 290 46 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 6.4   260  
ldv-regression/test30_true-unreach-call_true-termination.c true 2 wit inspect 7.3 370 62 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  260 true 2 wit inspect 9.1   450  
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 590   2500 5800 true -32 wit inspect 6.1  270 unknown 0 wit inspect 38     750   unknown 0 wit inspect 5.0  270 false(unreach-call) 1 wit inspect 1.1    19    - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 590   2600 5300 true -32 wit inspect 6.1  270 unknown 0 wit inspect 37     720   unknown 0 wit inspect 5.1  260 false(unreach-call) 1 wit inspect 1.1    19    - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 590   2500 4500 true -32 wit inspect 5.9  270 unknown 0 wit inspect 36     740   unknown 0 wit inspect 4.9  270 false(unreach-call) 1 wit inspect 1.1    19    - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 15   920 120 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.7  290 true 2 wit inspect 12     450  
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 15   900 130 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.3  290 true 2 wit inspect 13     450  
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 15   920 120 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.0  280 true 2 wit inspect 12     450  
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 15   950 120 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.8  290 true 2 wit inspect 12     440  
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 16   920 130 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.5  280 true 2 wit inspect 13     460  
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 15   930 110 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.5  280 true 2 wit inspect 12     450  
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 15   930 110 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.3  290 true 2 wit inspect 12     450  
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 15   930 120 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.0  280 true 2 wit inspect 11     460  
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 16   920 110 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.8  290 true 2 wit inspect 13     450  
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 16   920 130 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.1  280 true 2 wit inspect 11     440  
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 11   540 88 true -32 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 9.5   360   unknown 0 wit inspect 3.3  220 false(unreach-call) 1 wit inspect .67   18    - wit inspect - wit inspect
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 7.8 380 61 true -32 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 9.7   350   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 6.4 300 51 true -32 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 5.8   280   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   1200 12000 error (invalid witness file) 0 wit inspect .51 42 error (2) 0 wit inspect .051 4.9 error (invalid witness file) 0 wit inspect .85 50 error (invalid witness file) 0 wit inspect .0049 .28 - wit inspect - wit inspect
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 13   710 110 true -32 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 6.0   280   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   1700 9900 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .043 4.8 error (invalid witness file) 0 wit inspect .83 50 error (invalid witness file) 0 wit inspect .0040 .31 - wit inspect - wit inspect
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 6.0 290 51 true -32 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 5.8   290   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 7.0 310 55 true -32 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 8.2   290   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .68   18    - wit inspect - wit inspect
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 8.1 370 57 true -32 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 6.1   280   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .65   19    - wit inspect - wit inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 23   910 210 true -32 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 9.2   340   unknown 0 wit inspect 3.2  210 error (2) 0 wit inspect .67   18    - wit inspect - wit inspect
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i true -32 wit inspect 40   900 390 unknown 0 wit inspect 13    390 false(unreach-call) 1 wit inspect 12     500   unknown 0 wit inspect .97 51 error (1) 0 wit inspect .073  9.1  - wit inspect - wit inspect
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 7.7 380 67 true -32 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 9.1   360   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 5.9 300 49 true -32 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 5.6   280   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .66   18    - wit inspect - wit inspect
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i error (7) 0 wit inspect 140   1300 1600 error (invalid witness file) 0 wit inspect .39 43 error (2) 0 wit inspect .051 4.8 error (invalid witness file) 0 wit inspect .83 47 error (invalid witness file) 0 wit inspect .0043 .26 - wit inspect - wit inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 15   640 97 true -32 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 5.8   280   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .66   18    - wit inspect - wit inspect
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   3200 7300 error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .047 4.8 error (invalid witness file) 0 wit inspect .87 50 error (invalid witness file) 0