Tool CPAchecker 1.6.1-svn 26758M 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] 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:36:48 CET 2017-12-01 08:27:40 CET 2017-12-01 08:32:13 CET 2017-12-01 08:39:14 CET 2017-12-01 04:24:39 CET 2017-12-01 07:43:13 CET
Run set cpa-bam-slicing.sv-comp18.ReachSafety-Heap cpa-seq-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Heap uautomizer-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-cpa-bam-slicing.sv-comp18-correctness-witness.ReachSafety-Heap uautomizer-validate-correctness-witnesses-cpa-bam-slicing.sv-comp18-correctness-witness.ReachSafety-Heap
Options -ldv-bam-svcomp -disable-java-assertions -heap 10000m -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.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-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.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-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cpa-bam-slicing.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 false(unreach-call) 1 wit inspect 7.6 430 60 true -32 wit inspect 4.7  260 true -32 wit inspect 6.1   270   unknown 0 wit inspect 3.7  210 false(unreach-call) 1 wit inspect .69   19    - wit inspect - wit inspect
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 4.7 310 42 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .88 50 error (invalid witness file) 0 wit inspect .0019 .26 - wit inspect - wit inspect
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 3.9 290 33 true -32 wit inspect 4.1  260 true -32 wit inspect 6.2   270   unknown 0 wit inspect 2.5  210 true -32 wit inspect .67   19    - wit inspect - wit inspect
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i true -32 wit inspect 32   1200 270 unknown 0 wit inspect 6.0  310 false(unreach-call) 1 wit inspect 6.6   290   unknown 0 wit inspect .90 51 error (1) 0 wit inspect .069  9.0  - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(unreach-call) 0 wit inspect 4.5 300 47 true -32 wit inspect 4.6  260 true -32 wit inspect 5.8   240   unknown 0 wit inspect 3.5  210 true -32 wit inspect .67   19    - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 4.7 300 38 true -32 wit inspect 4.1  260 true -32 wit inspect 5.7   260   unknown 0 wit inspect 3.4  210 true -32 wit inspect .66   19    - wit inspect - wit inspect
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 9.4 500 88 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .029 4.8
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 9.1 460 74 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 4.1  250 true 2 wit inspect 330     1100  
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 4.6 300 42 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .018 4.9
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.6 280 43 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5100 timeout 0 wit inspect 960     3800  
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 45   2000 450 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3900 false(unreach-call) -16 wit inspect 7.6   290  
heap-manipulation/tree_true-unreach-call.i true 2 wit inspect 8.6 450 67 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3500 timeout 0 wit inspect 960     1000  
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 3.9 300 33 true -32 wit inspect 4.9  260 true -32 wit inspect 5.4   240   unknown 0 wit inspect 3.4  220 true -32 wit inspect .64   19    - wit inspect - wit inspect
list-properties/list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 6.0 330 49 true -32 wit inspect 3.7  260 true -32 wit inspect 5.4   250   unknown 0 wit inspect 3.2  210 true -32 wit inspect .65   19    - wit inspect - wit inspect
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 3.6 290 33 true -32 wit inspect 3.7  260 true -32 wit inspect 4.7   240   unknown 0 wit inspect 3.6  230 false(unreach-call) 1 wit inspect .66   19    - wit inspect - wit inspect
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i true -32 wit inspect 3.9 280 36 unknown 0 wit inspect 8.4  300 false(unreach-call) 1 wit inspect 47     850   unknown 0 wit inspect .88 51 error (1) 0 wit inspect .071  9.1  - wit inspect - wit inspect
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 3.6 290 29 true -32 wit inspect 3.4  260 true -32 wit inspect 5.3   240   unknown 0 wit inspect 3.1  210 true -32 wit inspect .95   19    - wit inspect - wit inspect
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 4.0 290 35 true -32 wit inspect 3.9  260 true -32 wit inspect 6.6   310   unknown 0 wit inspect 3.4  210 true -32 wit inspect .66   19    - wit inspect - wit inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.7 300 45 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3200 timeout 0 wit inspect 960     1100  
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 5.3 300 43 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2100 false(unreach-call) -16 wit inspect 6.0   260  
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i true 2 wit inspect 4.9 300 39 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 26    510 true 2 wit inspect 70     1100  
list-properties/list_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 6.8 390 54 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3100 timeout 0 wit inspect 960     1500  
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 3.4 280 32 - wit inspect - wit inspect - wit inspect - wit inspect out of java memory 0 wit inspect 160    5200 timeout 0 wit inspect 960     1100  
list-properties/simple_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 4.5 290 44 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1800 timeout 0 wit inspect 960     1000  
list-properties/splice_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 5.7 310 45 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4100 timeout 0 wit inspect 960     1200  
ldv-regression/1_3_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.3 280 29 true -32 wit inspect 3.2  260 true -32 wit inspect 6.9   300   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/alt_test_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.9 290 34 true -32 wit inspect 3.7  260 true -32 wit inspect 4.8   230   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .71   18    - wit inspect - wit inspect
ldv-regression/callfpointer_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.1 270 27 true -32 wit inspect 2.9  260 false(unreach-call) 1 wit inspect 4.5   230   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
ldv-regression/fo_test_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.4 280 29 true -32 wit inspect 3.5  260 true -32 wit inspect 5.0   230   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .68   19    - wit inspect - wit inspect
ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.1 280 30 true -32 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 4.8   250   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
ldv-regression/mutex_lock_struct_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.2 280 30 true -32 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 6.2   320   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/recursive_list_true-termination.c_false-unreach-call.i true -32 wit inspect 3.2 270 28 false(unreach-call) 1 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 5.6   250   unknown 0 wit inspect .95 51 error (1) 0 wit inspect .072  9.1  - wit inspect - wit inspect
ldv-regression/rule57_ebda_blast_true-termination.c_false-unreach-call.i false(unreach-call) 0 wit inspect 3.7 290 37 true -32 wit inspect 3.7  260 true -32 wit inspect 4.8   230   unknown 0 wit inspect 2.9  210 error (2) 0 wit inspect .60   19    - wit inspect - wit inspect
ldv-regression/rule60_list2_true-termination.c_false-unreach-call_1.i false(unreach-call) 0 wit inspect 4.7 300 40 true -32 wit inspect 3.7  260 true -32 wit inspect 3.6   240   unknown 0 wit inspect 2.4  210 true -32 wit inspect .65   18    - wit inspect - wit inspect
ldv-regression/stateful_check_false-unreach-call_false-termination.i false(unreach-call) 0 wit inspect 4.0 290 38 true -32 wit inspect 3.3  260 true -32 wit inspect 4.7   240   unknown 0 wit inspect 3.0  210 true -32 wit inspect .66   19    - wit inspect - wit inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.4 300 30 true -32 wit inspect 2.9  250 false(unreach-call) 1 wit inspect 5.3   250   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect 3.2 280 27 true -32 wit inspect 3.1  250 false(unreach-call) 1 wit inspect 4.7   240   unknown 0 wit inspect 2.0  210 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.1 270 26 - 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_2_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.7 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 5.6   260  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call.i true 2 wit inspect 2.8 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 5.7   280  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.8 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  260 true 2 wit inspect 5.3   250  
ldv-regression/ex3_forlist_true-termination.c_true-unreach-call.i unknown 0 wit inspect 6.2 350 53 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .024 4.8
ldv-regression/just_assert_true-termination.c_true-unreach-call.i true 2 wit inspect 2.7 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 5.0   220  
ldv-regression/mutex_lock_int_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.9 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 7.7   270  
ldv-regression/mutex_lock_struct_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.8 270 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 7.8   270  
ldv-regression/nested_structure_noptr_true-termination.c_true-unreach-call.i true 2 wit inspect 2.7 270 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 4.6   240  
ldv-regression/nested_structure_noptr_true-unreach-call_true-termination.i true 2 wit inspect 2.7 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  250 true 2 wit inspect 4.9   260  
ldv-regression/nested_structure_ptr_true-termination.c_true-unreach-call.i true 2 wit inspect 2.7 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 10     440  
ldv-regression/nested_structure_ptr_true-unreach-call_true-termination.i true 2 wit inspect 2.8 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 9.0   390  
ldv-regression/nested_structure_true-termination.c_true-unreach-call.i true 2 wit inspect 2.7 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 7.8   270  
ldv-regression/nested_structure_true-unreach-call_true-termination.i true 2 wit inspect 2.9 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 8.1   290  
ldv-regression/oomInt_true-termination.c_true-unreach-call.i true 2 wit inspect 2.9 270 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 5.9   260  
ldv-regression/oomInt_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.8 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 5.3   260  
ldv-regression/rule57_ebda_blast_true-termination.c_true-unreach-call_1.i true 2 wit inspect 3.5 280 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 6.8   260  
ldv-regression/rule60_list2_true-termination.c_true-unreach-call.i true 2 wit inspect 3.8 280 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3  260 true 2 wit inspect 23     700  
ldv-regression/rule60_list_true-termination.c_true-unreach-call.i true 2 wit inspect 3.3 270 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  260 true 2 wit inspect 9.7   370  
ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i true 2 wit inspect 3.3 280 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  250 true 2 wit inspect 5.0   270  
ldv-regression/structure_assignment_true-termination.c_true-unreach-call.i true 2 wit inspect 2.9 260 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 5.2   260  
ldv-regression/test_address_true-termination.c_true-unreach-call.i true 2 wit inspect 2.9 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  250 true 2 wit inspect 6.1   260  
ldv-regression/test_cut_trace_true-termination.c_true-unreach-call.i true 2 wit inspect 2.8 270 22 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 5.5   260  
ldv-regression/test_malloc-1_true-unreach-call_true-termination.i true 2 wit inspect 2.8 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 7.6   260  
ldv-regression/test_malloc-2_true-unreach-call_true-termination.i true 2 wit inspect 2.8 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  260 true 2 wit inspect 7.2   260  
ldv-regression/test_overflow_true-termination.c_true-unreach-call.i true 2 wit inspect 2.8 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  280 true 2 wit inspect 6.6   260  
ldv-regression/test_union_cast-1_true-unreach-call_true-termination.i true 2 wit inspect 2.9 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 5.8   260  
ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i true 2 wit inspect 2.9 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 5.4   260  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call.i true 2 wit inspect 2.6 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 6.1   260  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.7 260 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.8   260  
ldv-regression/test_union_true-termination.c_true-unreach-call.i true 2 wit inspect 2.7 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.2  250 true 2 wit inspect 5.6   270  
ldv-regression/test_union_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.8 280 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  240 true 2 wit inspect 6.3   260  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call.i true 2 wit inspect 2.9 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 6.0   270  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.7 270 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 7.8   280  
ldv-regression/test02_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.1 280 26 true -32 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 4.8   220   unknown 0 wit inspect 2.6  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/test06_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.4 290 30 true -32 wit inspect 3.1  260 true -32 wit inspect 4.8   240   unknown 0 wit inspect 2.9  190 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/test08_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.2 280 30 true -32 wit inspect 3.3  250 true -32 wit inspect 5.0   220   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/test12_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.2 270 25 true -32 wit inspect 2.9  260 true -32 wit inspect 5.9   290   unknown 0 wit inspect 2.6  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/test21_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.5 280 33 true -32 wit inspect 3.5  260 true -32 wit inspect 5.0   230   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .59   19    - wit inspect - wit inspect
ldv-regression/test22_false-unreach-call.c false(unreach-call) 0 wit inspect 3.5 290 32 true -32 wit inspect 3.4  250 true -32 wit inspect 5.4   250   unknown 0 wit inspect 3.0  190 true -32 wit inspect .63   19    - wit inspect - wit inspect
ldv-regression/test23_false-unreach-call.c false(unreach-call) 0 wit inspect 27   1700 230 true -32 wit inspect 3.6  260 true -32 wit inspect 5.4   250   unknown 0 wit inspect 3.0  210 true -32 wit inspect .68   19    - wit inspect - wit inspect
ldv-regression/test24_false-unreach-call.c false(unreach-call) 0 wit inspect 5.5 440 49 true -32 wit inspect 3.5  260 out of memory 0 wit inspect 56     7000   unknown 0 wit inspect 3.2  210 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 7.2 410 63 true -32 wit inspect 3.6  260 out of memory 0 wit inspect 55     7000   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .62   19    - wit inspect - wit inspect
ldv-regression/test26_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.3 280 30 true -32 wit inspect 3.1  250 false(unreach-call) 1 wit inspect 5.6   260   unknown 0 wit inspect 2.8  190 false(unreach-call) 1 wit inspect .62   18    - wit inspect - wit inspect
ldv-regression/test27_false-unreach-call_true-termination.c false(unreach-call) 0 wit inspect 4.8 310 44 true -32 wit inspect 3.3  260 out of memory 0 wit inspect 56     7000   unknown 0 wit inspect 2.9  210 error (2) 0 wit inspect .61   19    - wit inspect - wit inspect
ldv-regression/test28_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.3 280 30 true -32 wit inspect 3.4  260 true -32 wit inspect 5.1   240   unknown 0 wit inspect 2.8  190 false(unreach-call) 1 wit inspect .73   19    - wit inspect - wit inspect
ldv-regression/test29_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.2 290 29 true -32 wit inspect 3.7  260 true -32 wit inspect 5.1   240   unknown 0 wit inspect 2.9  190 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
ldv-regression/test30_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.3 280 29 true -32 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 5.6   260   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
ldv-regression/test01_true-unreach-call_true-termination.c true 2 wit inspect 2.7 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 5.5   260  
ldv-regression/test03_true-unreach-call_true-termination.c true 2 wit inspect 2.8 270 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 7.6   270  
ldv-regression/test04_true-unreach-call_true-termination.c true 2 wit inspect 2.9 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  260 true 2 wit inspect 6.9   280  
ldv-regression/test05_true-unreach-call_true-termination.c true 2 wit inspect 3.1 270 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 11     480  
ldv-regression/test07_true-unreach-call_true-termination.c true 2 wit inspect 3.2 280 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 9.6   360  
ldv-regression/test09_true-unreach-call_true-termination.c true 2 wit inspect 2.9 270 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 10     340  
ldv-regression/test10_true-unreach-call_true-termination.c true 2 wit inspect 3.1 270 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 13     510  
ldv-regression/test11_true-unreach-call_true-termination.c true 2 wit inspect 3.0 270 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  260 true 2 wit inspect 7.2   260  
ldv-regression/test13_true-unreach-call_true-termination.c true 2 wit inspect 2.7 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 6.1   260  
ldv-regression/test14_true-unreach-call_true-termination.c true 2 wit inspect 2.9 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 6.7   260  
ldv-regression/test15_true-unreach-call_true-termination.c true 2 wit inspect 2.8 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 8.1   290  
ldv-regression/test16_true-unreach-call_true-termination.c true 2 wit inspect 2.8 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 8.0   290  
ldv-regression/test17_true-unreach-call_true-termination.c true 2 wit inspect 2.9 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 5.6   260  
ldv-regression/test18_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.0 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  260 true 2 wit inspect 5.6   230  
ldv-regression/test19_true-unreach-call_true-termination.c true 2 wit inspect 2.9 270 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 12     360  
ldv-regression/test20_true-unreach-call_true-termination.c true 2 wit inspect 2.8 270 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 6.0   260  
ldv-regression/test21_true-unreach-call_true-termination.c true 2 wit inspect 3.0 270 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 9.2   310  
ldv-regression/test22_true-unreach-call.c true 2 wit inspect 6.0 370 49 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.1  290 true 2 wit inspect 22     650  
ldv-regression/test23_true-unreach-call.c true 2 wit inspect 29   1700 250 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.8  300 true 2 wit inspect 230     770  
ldv-regression/test24_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.3 290 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 9.3   420  
ldv-regression/test25_true-unreach-call.c true 2 wit inspect 5.6 310 46 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 18    440 true 2 wit inspect 29     560  
ldv-regression/test26_true-unreach-call_true-termination.c true 2 wit inspect 2.9 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 8.0   290  
ldv-regression/test27_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 4.9 320 47 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  260 out of memory 0 wit inspect 56     7000  
ldv-regression/test28_true-unreach-call_true-termination.c true 2 wit inspect 2.9 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 7.2   270  
ldv-regression/test29_true-unreach-call_true-termination.c true 2 wit inspect 2.8 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 8.1   320  
ldv-regression/test30_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.2  250 true 2 wit inspect 11     450  
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 5.0 310 47 true -32 wit inspect 8.0  270 true -32 wit inspect 12     470   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 5.0 310 44 true -32 wit inspect 6.6  290 true -32 wit inspect 12     470   unknown 0 wit inspect 5.2  270 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 5.6 310 45 true -32 wit inspect 7.2  270 true -32 wit inspect 14     470   unknown 0 wit inspect 5.1  290 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 2.9 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.9  270 true 2 wit inspect 12     430  
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 3.1 270 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.2  280 true 2 wit inspect 12     430  
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 2.9 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.3  280 true 2 wit inspect 12     430  
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 2.9 270 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.9  280 true 2 wit inspect 12     430  
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 3.0 270 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.7  280 true 2 wit inspect 12     420  
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 2.9 270 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.2  280 true 2 wit inspect 13     430  
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 3.0 260 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.5  280 true 2 wit inspect 15     430  
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 3.0 260 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.9  280 true 2 wit inspect 13     440  
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 2.9 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.2  280 true 2 wit inspect 13     430  
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 2.9 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.8  280 true 2 wit inspect 11     430  
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 20   710 170 true -32 wit inspect 3.9  260 true -32 wit inspect 5.8   260   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .67   19    - wit inspect - wit inspect
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.5 300 43 true -32 wit inspect 4.5  260 false(unreach-call) 1 wit inspect 9.4   350   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .67   18    - wit inspect - wit inspect
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 3.7 290 38 true -32 wit inspect 3.7  260 true -32 wit inspect 5.2   250   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .66   19    - wit inspect - wit inspect
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 4.6 300 42 error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 3.9 300 34 true -32 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 6.3   290   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 witness invalid (false(unreach-call)) 0 wit inspect 4.3 310 40 true -32 wit inspect 3.2  260 true -32 wit inspect 5.5   250   unknown 0 wit inspect 3.1  210 error (invalid witness file) 0 wit inspect .61   18    - wit inspect - wit inspect
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 3.5 290 30 true -32 wit inspect 3.6  260 true -32 wit inspect 6.3   300   unknown 0 wit inspect 2.3  210 false(unreach-call) 1 wit inspect .68   19    - wit inspect - wit inspect
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 3.7 290 31 true -32 wit inspect 3.9  260 true -32 wit inspect 5.7   250   unknown 0 wit inspect 3.3  210 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 3.5 290 29 true -32 wit inspect 3.9  260 true -32 wit inspect 5.4   240   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .67   18    - wit inspect - wit inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(unreach-call) 0 wit inspect 30   1200 240 true -32 wit inspect 4.0  260 true -32 wit inspect 5.6   260   unknown 0 wit inspect 3.3  210 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 9.4 470 72 true -32 wit inspect 4.6  280 true -32 wit inspect 5.6   250   unknown 0 wit inspect 3.5  210 true -32 wit inspect .66   19    - wit inspect - wit inspect
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.5 310 39 true -32 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 9.8   380   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .66   19    - wit inspect - wit inspect
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 3.7 290 32 true -32 wit inspect 3.6  260 true -32 wit inspect 5.9   240   unknown 0 wit inspect 2.3  210 false(unreach-call) 1 wit inspect .66   19    - wit inspect - wit inspect
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 4.4 300 40 error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0013 .27 - wit inspect - wit inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit