Tool 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-11-30 11:20:26 CET 2017-12-01 07:29:20 CET 2017-12-01 08:07:14 CET 2017-12-01 08:15:38 CET 2017-12-01 08:19:10 CET 2017-12-01 04:11:27 CET 2017-12-01 07:35:08 CET
Run set cpa-seq.sv-comp18.ReachSafety-Heap cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Heap uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.ReachSafety-Heap uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.ReachSafety-Heap
Options -svcomp18 -heap 10000M -benchmark -timelimit 900s -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.2017-11-30_1120.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/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.2017-11-30_1120.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/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cpa-seq.2017-11-30_1120.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 950   7800 6600 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .80 47 error (invalid witness file) 0 wit inspect .0016 .28 - wit inspect - wit inspect
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 640   2500 7000 true -32 wit inspect 4.1  250 true -32 wit inspect 6.2   270   unknown 0 wit inspect 3.7  250 true -32 wit inspect .65   19    - wit inspect - wit inspect
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 5.7 310 51 false(unreach-call) 1 wit inspect 4.2  260 false(unreach-call) 1 wit inspect 11     320   unknown 0 wit inspect 3.8  260 false(unreach-call) 1 wit inspect .71   19    - wit inspect - wit inspect
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 160   3200 1800 true -32 wit inspect 4.2  270 timeout 0 wit inspect 96     720   unknown 0 wit inspect 4.3  220 true -32 wit inspect .73   19    - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 18   1100 180 false(unreach-call) 1 wit inspect 4.0  260 false(unreach-call) 1 wit inspect 8.6   290   unknown 0 wit inspect 3.7  250 false(unreach-call) 1 wit inspect .81   19    - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 18   1200 150 false(unreach-call) 1 wit inspect 4.3  260 false(unreach-call) 1 wit inspect 7.7   290   unknown 0 wit inspect 4.1  250 false(unreach-call) 1 wit inspect .65   19    - wit inspect - wit inspect
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   7600 8100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 41 error (2) 0 wit inspect .023 4.9
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   4100 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 44 error (2) 0 wit inspect .022 4.8
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 630   3000 6600 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5  250 true 2 wit inspect 6.4   280  
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   2500 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .021 4.9
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   4800 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 44 error (2) 0 wit inspect .022 4.9
heap-manipulation/tree_true-unreach-call.i timeout 0 wit inspect 900   3900 5900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .021 4.9
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.7 280 42 false(unreach-call) 1 wit inspect 2.7  260 false(unreach-call) 1 wit inspect 6.9   270   unknown 0 wit inspect 3.8  250 false(unreach-call) 1 wit inspect .83   18    - wit inspect - wit inspect
list-properties/list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 12   620 92 unknown 0 wit inspect 4.1  260 true -32 wit inspect 12     480   unknown 0 wit inspect 4.6  210 true -32 wit inspect .64   19    - wit inspect - wit inspect
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.4 280 34 false(unreach-call) 1 wit inspect 4.1  260 false(unreach-call) 1 wit inspect 6.9   280   unknown 0 wit inspect 3.4  240 false(unreach-call) 1 wit inspect .65   19    - wit inspect - wit inspect
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 8.5 460 71 false(unreach-call) 1 wit inspect 4.3  270 false(unreach-call) 1 wit inspect 35     710   unknown 0 wit inspect 4.4  210 false(unreach-call) 1 wit inspect .80   18    - wit inspect - wit inspect
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.0 280 33 false(unreach-call) 1 wit inspect 4.0  260 false(unreach-call) 1 wit inspect 7.3   270   unknown 0 wit inspect 3.5  250 false(unreach-call) 1 wit inspect .65   19    - wit inspect - wit inspect
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 5.4 300 42 false(unreach-call) 1 wit inspect 4.0  260 false(unreach-call) 1 wit inspect 6.4   290   unknown 0 wit inspect 4.7  250 false(unreach-call) 1 wit inspect .64   19    - wit inspect - wit inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   3000 6000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .020 4.9
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   2400 6900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .020 4.8
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i true 2 wit inspect 24   1500 240 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 27    520 true 2 wit inspect 68     1100  
list-properties/list_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   3100 6900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 44 error (2) 0 wit inspect .021 4.9
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   2300 6400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .021 4.9
list-properties/simple_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   2100 5800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .020 4.9
list-properties/splice_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   3700 5600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 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 3.4 270 31 false(unreach-call) 1 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 5.4   270   unknown 0 wit inspect 3.0  180 false(unreach-call) 1 wit inspect .69   18    - wit inspect - wit inspect
ldv-regression/alt_test_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 5.1 300 46 false(unreach-call) 1 wit inspect 3.8  260 false(unreach-call) 1 wit inspect 8.7   270   unknown 0 wit inspect 4.1  220 false(unreach-call) 1 wit inspect .73   18    - wit inspect - wit inspect
ldv-regression/callfpointer_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 2.6 250 23 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 5.5   230   unknown 0 wit inspect 2.6  210 false(unreach-call) 1 wit inspect .71   18    - wit inspect - wit inspect
ldv-regression/fo_test_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.5 270 30 false(unreach-call) 1 wit inspect 4.4  260 unknown 0 wit inspect 11     290   unknown 0 wit inspect 4.1  210 false(unreach-call) 1 wit inspect .64   18    - wit inspect - wit inspect
ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.2 270 27 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 4.8   250   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .70   18    - wit inspect - wit inspect
ldv-regression/mutex_lock_struct_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.1 270 28 false(unreach-call) 1 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 4.8   250   unknown 0 wit inspect 3.1  190 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 2.7 260 24 false(unreach-call) 1 wit inspect 2.3  260 false(unreach-call) 1 wit inspect 6.0   270   unknown 0 wit inspect 3.0  190 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
ldv-regression/rule57_ebda_blast_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 2.8 260 23 false(unreach-call) 1 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 8.0   270   unknown 0 wit inspect 2.9  190 error (2) 0 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/rule60_list2_true-termination.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect 4.0 280 32 false(unreach-call) 1 wit inspect 3.8  270 false(unreach-call) 1 wit inspect 14     500   unknown 0 wit inspect 4.0  210 true -32 wit inspect .64   19    - wit inspect - wit inspect
ldv-regression/stateful_check_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect 3.3 270 33 false(unreach-call) 1 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 7.0   280   unknown 0 wit inspect 3.2  210 true -32 wit inspect .74   19    - wit inspect - wit inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 2.7 260 28 false(unreach-call) 1 wit inspect 4.2  260 false(unreach-call) 1 wit inspect 4.9   250   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .73   19    - wit inspect - wit inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect 2.6 250 26 false(unreach-call) 1 wit inspect 2.3  260 false(unreach-call) 1 wit inspect 5.0   240   unknown 0 wit inspect 3.3  190 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call.i true 2 wit inspect 3.2 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 6.6   280  
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.9 260 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.3   260  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call.i true 2 wit inspect 3.2 260 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 6.1   270  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.9 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 5.5   260  
ldv-regression/ex3_forlist_true-termination.c_true-unreach-call.i true 2 wit inspect 2.6 250 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 25    450 true 2 wit inspect 23     660  
ldv-regression/just_assert_true-termination.c_true-unreach-call.i true 2 wit inspect 2.5 260 19 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.8  250 true 2 wit inspect 4.3   220  
ldv-regression/mutex_lock_int_true-termination.c_true-unreach-call_1.i true 2 wit inspect 3.1 270 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 6.9   260  
ldv-regression/mutex_lock_struct_true-termination.c_true-unreach-call_1.i true 2 wit inspect 3.2 270 31 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 7.9   270  
ldv-regression/nested_structure_noptr_true-termination.c_true-unreach-call.i true 2 wit inspect 2.3 240 21 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  260 true 2 wit inspect 5.4   250  
ldv-regression/nested_structure_noptr_true-unreach-call_true-termination.i true 2 wit inspect 2.3 240 20 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.4   260  
ldv-regression/nested_structure_ptr_true-termination.c_true-unreach-call.i true 2 wit inspect 3.2 260 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 9.3   470  
ldv-regression/nested_structure_ptr_true-unreach-call_true-termination.i true 2 wit inspect 3.0 260 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 9.6   390  
ldv-regression/nested_structure_true-termination.c_true-unreach-call.i true 2 wit inspect 3.3 270 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  260 true 2 wit inspect 8.2   280  
ldv-regression/nested_structure_true-unreach-call_true-termination.i true 2 wit inspect 3.0 260 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 8.5   290  
ldv-regression/oomInt_true-termination.c_true-unreach-call.i true 2 wit inspect 2.8 260 22 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  240 true 2 wit inspect 6.4   260  
ldv-regression/oomInt_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.3 250 20 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  250 true 2 wit inspect 5.2   270  
ldv-regression/rule57_ebda_blast_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.5 240 21 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 6.5   270  
ldv-regression/rule60_list2_true-termination.c_true-unreach-call.i true 2 wit inspect 2.9 250 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  260 true 2 wit inspect 23     660  
ldv-regression/rule60_list_true-termination.c_true-unreach-call.i true 2 wit inspect 3.9 280 39 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  260 true 2 wit inspect 11     400  
ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i true 2 wit inspect 2.7 250 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  250 true 2 wit inspect 5.7   260  
ldv-regression/structure_assignment_true-termination.c_true-unreach-call.i true 2 wit inspect 3.0 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.7   250  
ldv-regression/test_address_true-termination.c_true-unreach-call.i true 2 wit inspect 3.9 280 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  250 true 2 wit inspect 5.8   260  
ldv-regression/test_cut_trace_true-termination.c_true-unreach-call.i true 2 wit inspect 2.4 250 20 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.1   260  
ldv-regression/test_malloc-1_true-unreach-call_true-termination.i true 2 wit inspect 4.1 280 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  260 true 2 wit inspect 6.6   270  
ldv-regression/test_malloc-2_true-unreach-call_true-termination.i true 2 wit inspect 4.2 280 34 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  250 true 2 wit inspect 5.9   260  
ldv-regression/test_overflow_true-termination.c_true-unreach-call.i true 2 wit inspect 2.9 250 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  260 true 2 wit inspect 6.3   250  
ldv-regression/test_union_cast-1_true-unreach-call_true-termination.i true 2 wit inspect 2.5 250 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 6.1   260  
ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i true 2 wit inspect 3.1 260 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 5.4   280  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call.i true 2 wit inspect 3.3 270 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 5.3   260  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.4 250 20 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 6.4   270  
ldv-regression/test_union_true-termination.c_true-unreach-call.i true 2 wit inspect 2.3 250 20 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 5.0   260  
ldv-regression/test_union_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.4 250 20 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 5.5   260  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call.i true 2 wit inspect 3.0 260 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 5.7   270  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i true 2 wit inspect 3.0 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.8   270  
ldv-regression/test02_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.5 260 23 false(unreach-call) 1 wit inspect 2.1  260 false(unreach-call) 1 wit inspect 4.6   220   unknown 0 wit inspect 3.2  210 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 2.7 250 21 false(unreach-call) 1 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 7.5   280   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/test08_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.6 260 23 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 5.5   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 2.7 250 23 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 4.7   260   unknown 0 wit inspect 3.0  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
ldv-regression/test21_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.8 250 23 false(unreach-call) 1 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 5.8   270   unknown 0 wit inspect 3.0  180 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
ldv-regression/test22_false-unreach-call.c false(unreach-call) 1 wit inspect 3.8 280 31 false(unreach-call) 1 wit inspect 3.5  270 false(unreach-call) 1 wit inspect 11     440   unknown 0 wit inspect 4.0  210 true -32 wit inspect .62   19    - wit inspect - wit inspect
ldv-regression/test23_false-unreach-call.c false(unreach-call) 1 wit inspect 11   290 120 false(unreach-call) 1 wit inspect 3.8  260 timeout 0 wit inspect 94     7000   unknown 0 wit inspect 4.2  210 true -32 wit inspect .60   19    - wit inspect - wit inspect
ldv-regression/test24_false-unreach-call.c false(unreach-call) 1 wit inspect 3.4 270 29 false(unreach-call) 1 wit inspect 4.5  280 out of memory 0 wit inspect 89     7000   unknown 0 wit inspect 3.2  210 true -32 wit inspect .59   19    - wit inspect - wit inspect
ldv-regression/test25_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 12   310 130 false(unreach-call) 1 wit inspect 4.2  280 out of memory 0 wit inspect 70     7000   unknown 0 wit inspect 3.3  210 true -32 wit inspect .61   19    - wit inspect - wit inspect
ldv-regression/test26_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.6 250 22 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 4.8   260   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
ldv-regression/test27_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.2 270 28 false(unreach-call) 1 wit inspect 3.9  270 false(unreach-call) 1 wit inspect 66     920   unknown 0 wit inspect 3.0  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 3.2 270 30 false(unreach-call) 1 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 7.2   270   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
ldv-regression/test29_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.4 270 28 false(unreach-call) 1 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 7.5   260   unknown 0 wit inspect 3.4  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/test30_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.6 250 21 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 5.7   270   unknown 0 wit inspect 2.9  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/test01_true-unreach-call_true-termination.c true 2 wit inspect 2.9 260 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 5.3   260  
ldv-regression/test03_true-unreach-call_true-termination.c true 2 wit inspect 3.1 270 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 6.4   270  
ldv-regression/test04_true-unreach-call_true-termination.c true 2 wit inspect 3.4 280 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 7.1   270  
ldv-regression/test05_true-unreach-call_true-termination.c true 2 wit inspect 3.6 270 33 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 9.9   480  
ldv-regression/test07_true-unreach-call_true-termination.c true 2 wit inspect 3.5 290 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 9.1   340  
ldv-regression/test09_true-unreach-call_true-termination.c true 2 wit inspect 3.1 260 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 8.2   340  
ldv-regression/test10_true-unreach-call_true-termination.c true 2 wit inspect 3.2 270 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 12     490  
ldv-regression/test11_true-unreach-call_true-termination.c true 2 wit inspect 3.4 280 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 7.9   270  
ldv-regression/test13_true-unreach-call_true-termination.c true 2 wit inspect 3.0 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 6.5   260  
ldv-regression/test14_true-unreach-call_true-termination.c true 2 wit inspect 3.2 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  260 true 2 wit inspect 7.2   260  
ldv-regression/test15_true-unreach-call_true-termination.c true 2 wit inspect 3.5 290 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 7.3   280  
ldv-regression/test16_true-unreach-call_true-termination.c true 2 wit inspect 3.1 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 9.9   290  
ldv-regression/test17_true-unreach-call_true-termination.c true 2 wit inspect 2.9 260 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.2   260  
ldv-regression/test18_true-unreach-call_true-termination.c true 2 wit inspect 3.1 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 8.7   310  
ldv-regression/test19_true-unreach-call_true-termination.c true 2 wit inspect 3.1 260 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 9.0   360  
ldv-regression/test20_true-unreach-call_true-termination.c true 2 wit inspect 3.0 270 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 5.7   280  
ldv-regression/test21_true-unreach-call_true-termination.c true 2 wit inspect 3.4 270 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 11     310  
ldv-regression/test22_true-unreach-call.c true 2 wit inspect 5.9 290 55 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.9  290 true 2 wit inspect 21     620  
ldv-regression/test23_true-unreach-call.c true 2 wit inspect 11   330 130 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1  300 true 2 wit inspect 240     740  
ldv-regression/test24_true-unreach-call_true-termination.c true 2 wit inspect 11   300 110 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  280 true 2 wit inspect 11     410  
ldv-regression/test25_true-unreach-call.c true 2 wit inspect 210   1200 2100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 18    480 true 2 wit inspect 31     550  
ldv-regression/test26_true-unreach-call_true-termination.c true 2 wit inspect 3.0 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 9.1   290  
ldv-regression/test27_true-unreach-call_true-termination.c true 2 wit inspect 40   640 400 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 30    420 true 2 wit inspect 180     830  
ldv-regression/test28_true-unreach-call_true-termination.c true 2 wit inspect 3.2 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 7.8   280  
ldv-regression/test29_true-unreach-call_true-termination.c true 2 wit inspect 3.3 270 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 7.0   260  
ldv-regression/test30_true-unreach-call_true-termination.c true 2 wit inspect 3.2 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  270 true 2 wit inspect 10     440  
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 9.2 420 76 false(unreach-call) 1 wit inspect 8.5  350 unknown 0 wit inspect 45     780   unknown 0 wit inspect 6.2  270 false(unreach-call) 1 wit inspect 1.4    19    - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 9.2 420 77 false(unreach-call) 1 wit inspect 10    350 unknown 0 wit inspect 42     720   unknown 0 wit inspect 5.2  270 false(unreach-call) 1 wit inspect 1.2    19    - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 9.1 420 77 false(unreach-call) 1 wit inspect 8.8  350 unknown 0 wit inspect 41     790   unknown 0 wit inspect 5.2  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 97   2600 1200 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.1  310 true 2 wit inspect 12     440  
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 97   3100 1100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.2  280 true 2 wit inspect 14     450  
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 97   3000 1000 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.6  320 true 2 wit inspect 12     430  
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 98   2900 1000 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.3  310 true 2 wit inspect 12     430  
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 98   2800 1000 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.1  280 true 2 wit inspect 14     490  
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 98   3100 1200 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.8  290 true 2 wit inspect 12     430  
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 97   2800 1100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.3  320 true 2 wit inspect 15     450  
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 98   3000 1100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.6  300 true 2 wit inspect 13     450  
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 97   2700 950 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.6  320 true 2 wit inspect 14     440  
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 98   2800 1100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.1  310 true 2 wit inspect 15     450  
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 210   720 2900 false(unreach-call) 1 wit inspect 4.5  260 false(unreach-call) 1 wit inspect 11     360   unknown 0 wit inspect 4.0  250 false(unreach-call) 1 wit inspect .65   19    - wit inspect - wit inspect
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.6 280 38 false(unreach-call) 1 wit inspect 3.8  260 false(unreach-call) 1 wit inspect 9.9   360   unknown 0 wit inspect 3.5  250 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 3.4 270 28 false(unreach-call) 1 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 6.2   290   unknown 0 wit inspect 3.9  210 false(unreach-call) 1 wit inspect .83   18    - wit inspect - wit inspect
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 17   640 130 unknown 0 wit inspect 4.2  270 true -32 wit inspect 34     910   unknown 0 wit inspect 2.5  210 true -32 wit inspect .94   19    - wit inspect - wit inspect
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 3.4 260 30 false(unreach-call) 1 wit inspect 3.6  270 false(unreach-call) 1 wit inspect 8.0   280   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .73   18    - wit inspect - wit inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(unreach-call) 1 wit inspect 15   640 140 false(unreach-call) 1 wit inspect 4.3  270 false(unreach-call) 1 wit inspect 7.2   310   unknown 0 wit inspect 3.6  260 false(unreach-call) 1 wit inspect .65   19    - wit inspect - wit inspect
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 3.3 270 33 false(unreach-call) 1 wit inspect 3.8  270 false(unreach-call) 1 wit inspect 7.4   280   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .66   18    - wit inspect - wit inspect
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.9 290 41 false(unreach-call) 1 wit inspect 4.0  260 false(unreach-call) 1 wit inspect 9.4   300   unknown 0 wit inspect 3.9  250 false(unreach-call) 1 wit inspect .65   19    - wit inspect - wit inspect
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.5 280 44 false(unreach-call) 1 wit inspect 5.0  260 false(unreach-call) 1 wit inspect 7.0   280   unknown 0 wit inspect 3.9  250 false(unreach-call) 1 wit inspect .83   18    - wit inspect - wit inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 240   1700 3100 false(unreach-call) 1 wit inspect 4.6  260 false(unreach-call) 1 wit inspect 23     570   unknown 0 wit inspect 3.7  250 error (2) 0 wit inspect .68   19    - wit inspect - wit inspect
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 270   2300 3600 unknown 0 wit inspect 3.6  260 true -32 wit inspect 7.1   250   unknown 0 wit inspect 4.4  210 true -32 wit inspect .64   18    - wit inspect - wit inspect
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.4 280 34 false(unreach-call) 1 wit inspect 3.8  250 false(unreach-call) 1 wit inspect 9.5   370   unknown 0 wit inspect 4.3  250 false(unreach-call) 1 wit inspect .68   18    - wit inspect - wit inspect
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 3.4 260 31 false(unreach-call) 1 wit inspect 4.6  270 false(unreach-call) 1 wit inspect 7.1   300   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .68   18    - wit inspect - wit inspect
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 17   680 130 unknown 0 wit inspect 4.3  270 true -32 wit inspect 23     750   unknown 0 wit inspect 4.0  210 true -32 wit inspect .64   19    - wit inspect - wit inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 5.8 310 44 false(unreach-call) 1 wit inspect 4.4  260 false(unreach-call) 1 wit inspect 6.0   280   unknown 0 wit inspect 4.6  270 false(unreach-call) 1 wit inspect .64   18    - wit inspect - wit inspect
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1