Tool CPAchecker 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-05 07:52:24 CET 2017-12-05 13:10:09 CET 2017-12-05 13:34:02 CET 2017-12-05 13:37:41 CET 2017-12-05 13:41:35 CET 2017-12-05 12:37:13 CET 2017-12-05 13:13:01 CET
Run set interpchecker.sv-comp18.ReachSafety-Heap cpa-seq-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-Heap uautomizer-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-interpchecker.sv-comp18-violation-witness.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-interpchecker.sv-comp18-correctness-witness.ReachSafety-Heap uautomizer-validate-correctness-witnesses-interpchecker.sv-comp18-correctness-witness.ReachSafety-Heap
Options -sv-comp18-interpcpachecker -heap 10000M -disable-java-assertions -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/interpchecker.2017-12-05_0752.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/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/interpchecker.2017-12-05_0752.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/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/interpchecker.2017-12-05_0752.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/interpchecker.2017-12-05_0752.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 10   470 83 true -32 wit inspect 4.5  260 false(unreach-call) 1 wit inspect 7.1   320   unknown 0 wit inspect 3.7  260 false(unreach-call) 1 wit inspect .72   19    - wit inspect - wit inspect
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 200   3400 2600 true -32 wit inspect 4.4  260 true -32 wit inspect 6.2   280   unknown 0 wit inspect 3.8  250 true -32 wit inspect .67   18    - wit inspect - wit inspect
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 5.2 300 44 true -32 wit inspect 4.0  250 false(unreach-call) 1 wit inspect 7.1   320   unknown 0 wit inspect 3.8  250 false(unreach-call) 1 wit inspect .67   19    - wit inspect - wit inspect
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 12   500 96 true -32 wit inspect 4.2  270 false(unreach-call) 1 wit inspect 8.0   310   unknown 0 wit inspect 3.7  250 error (2) 0 wit inspect .67   19    - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(unreach-call) 0 wit inspect 86   3100 990 true -32 wit inspect 3.8  250 true -32 wit inspect 5.4   250   unknown 0 wit inspect 3.4  250 true -32 wit inspect .66   19    - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 92   3300 940 true -32 wit inspect 4.0  270 true -32 wit inspect 5.7   260   unknown 0 wit inspect 3.8  270 true -32 wit inspect .63   19    - wit inspect - wit inspect
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   3900 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .025 4.8
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i false(unreach-call) -16 wit inspect 140   4000 1500 - wit inspect - wit inspect - wit inspect - wit inspect false(unreach-call) -16 wit inspect 22    500 true 2 wit inspect 5.8   260  
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 220   3700 2600 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.0  250 true 2 wit inspect 6.1   270  
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   4500 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 45 error (2) 0 wit inspect .025 4.9
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   4100 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .74 44 error (2) 0 wit inspect .048 4.9
heap-manipulation/tree_true-unreach-call.i timeout 0 wit inspect 900   4000 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .048 5.0
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 8.5 470 61 true -32 wit inspect 3.9  250 false(unreach-call) 1 wit inspect 6.1   270   unknown 0 wit inspect 3.5  250 error (255) 0 wit inspect .60   18    - wit inspect - wit inspect
list-properties/list_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   4200 13000 error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .044 4.8 error (invalid witness file) 0 wit inspect .81 49 error (invalid witness file) 0 wit inspect .0047 .26 - wit inspect - wit inspect
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.7 290 41 true -32 wit inspect 3.5  250 false(unreach-call) 1 wit inspect 5.4   270   unknown 0 wit inspect 3.3  250 error (255) 0 wit inspect .59   19    - wit inspect - wit inspect
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 11   470 85 true -32 wit inspect 3.9  260 false(unreach-call) 1 wit inspect 24     700   unknown 0 wit inspect 3.6  220 error (255) 0 wit inspect .63   19    - wit inspect - wit inspect
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 6.4 330 53 true -32 wit inspect 3.5  250 false(unreach-call) 1 wit inspect 5.5   270   unknown 0 wit inspect 3.3  250 false(unreach-call) 1 wit inspect .66   19    - wit inspect - wit inspect
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 95   3700 1000 true -32 wit inspect 4.0  250 false(unreach-call) 1 wit inspect 5.5   270   unknown 0 wit inspect 3.6  250 error (255) 0 wit inspect .59   19    - wit inspect - wit inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   4100 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 5.0
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   4500 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .77 41 error (2) 0 wit inspect .018 4.9
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i true 2 wit inspect 22   1100 160 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 27    490 true 2 wit inspect 61     1100  
list-properties/list_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   4300 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .018 5.0
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   4100 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .050 4.8
list-properties/simple_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   4200 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .018 4.8
list-properties/splice_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   4300 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .018 5.0
ldv-regression/1_3_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.2 270 32 true -32 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 5.2   250   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/alt_test_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 4.5 290 40 true -32 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 6.2   270   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .69   18    - wit inspect - wit inspect
ldv-regression/callfpointer_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 2.7 270 27 false(unreach-call) 1 wit inspect 2.9  260 false(unreach-call) 1 wit inspect 4.8   240   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
ldv-regression/fo_test_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.6 280 32 true -32 wit inspect 3.4  250 unknown 0 wit inspect 11     290   unknown 0 wit inspect 3.3  220 false(unreach-call) 1 wit inspect .66   18    - wit inspect - wit inspect
ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 2.8 280 25 false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 5.5   250   unknown 0 wit inspect 2.7  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/mutex_lock_struct_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 2.9 280 27 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 4.7   250   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
ldv-regression/recursive_list_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.1 270 30 true -32 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 5.3   280   unknown 0 wit inspect 2.9  210 error (2) 0 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.5 300 45 false(unreach-call) 1 wit inspect 4.4  270 false(unreach-call) 1 wit inspect 6.5   270   unknown 0 wit inspect 2.2  220 error (1) 0 wit inspect .57   18    - wit inspect - wit inspect
ldv-regression/rule60_list2_true-termination.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect 7.1 380 55 true -32 wit inspect 3.9  250 false(unreach-call) 1 wit inspect 6.5   280   unknown 0 wit inspect 3.4  220 false(unreach-call) 1 wit inspect .64   19    - wit inspect - wit inspect
ldv-regression/stateful_check_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect 5.3 300 43 true -32 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 5.4   290   unknown 0 wit inspect 3.1  210 true -32 wit inspect .62   19    - wit inspect - wit inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.2 270 31 true -32 wit inspect 2.9  260 false(unreach-call) 1 wit inspect 4.5   240   unknown 0 wit inspect 2.7  210 false(unreach-call) 1 wit inspect .59   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 29 false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 5.9   260   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call.i true 2 wit inspect 2.9 280 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 6.0   270  
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.7 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  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.0 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 5.7   270  
ldv-regression/alias_of_return_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 4.0  250 true 2 wit inspect 5.3   260  
ldv-regression/ex3_forlist_true-termination.c_true-unreach-call.i true 2 wit inspect 15   610 120 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 16    480 true 2 wit inspect 28     700  
ldv-regression/just_assert_true-termination.c_true-unreach-call.i true 2 wit inspect 2.5 270 21 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.1   220  
ldv-regression/mutex_lock_int_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.0  250 true 2 wit inspect 6.3   280  
ldv-regression/mutex_lock_struct_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.9 280 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 5.8   260  
ldv-regression/nested_structure_noptr_true-termination.c_true-unreach-call.i true 2 wit inspect 2.8 260 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 4.4   250  
ldv-regression/nested_structure_noptr_true-unreach-call_true-termination.i true 2 wit inspect 2.8 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  260 true 2 wit inspect 4.9   260  
ldv-regression/nested_structure_ptr_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 3.8  260 true 2 wit inspect 9.9   480  
ldv-regression/nested_structure_ptr_true-unreach-call_true-termination.i true 2 wit inspect 3.0 270 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 6.3   400  
ldv-regression/nested_structure_true-termination.c_true-unreach-call.i true 2 wit inspect 2.9 280 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 7.0   280  
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.0  260 true 2 wit inspect 7.9   290  
ldv-regression/oomInt_true-termination.c_true-unreach-call.i true 2 wit inspect 3.0 280 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 5.3   260  
ldv-regression/oomInt_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.8 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 6.4   260  
ldv-regression/rule57_ebda_blast_true-termination.c_true-unreach-call_1.i false(unreach-call) -16 wit inspect 5.4 300 43 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9  270 true 2 wit inspect 5.9   270  
ldv-regression/rule60_list2_true-termination.c_true-unreach-call.i true 2 wit inspect 17   630 130 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3  260 true 2 wit inspect 21     660  
ldv-regression/rule60_list_true-termination.c_true-unreach-call.i true 2 wit inspect 4.7 290 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 9.3   380  
ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i true 2 wit inspect 3.3 280 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 5.1   250  
ldv-regression/structure_assignment_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 4.0  250 true 2 wit inspect 5.0   260  
ldv-regression/test_address_true-termination.c_true-unreach-call.i true 2 wit inspect 3.3 280 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  250 true 2 wit inspect 5.7   260  
ldv-regression/test_cut_trace_true-termination.c_true-unreach-call.i true 2 wit inspect 2.9 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 4.7   250  
ldv-regression/test_malloc-1_true-unreach-call_true-termination.i true 2 wit inspect 3.2 280 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 5.8   260  
ldv-regression/test_malloc-2_true-unreach-call_true-termination.i true 2 wit inspect 3.3 280 30 - 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_overflow_true-termination.c_true-unreach-call.i true 2 wit inspect 3.6 280 31 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  250 true 2 wit inspect 5.3   260  
ldv-regression/test_union_cast-1_true-unreach-call_true-termination.i true 2 wit inspect 2.7 260 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.8  250 true 2 wit inspect 5.4   260  
ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i true 2 wit inspect 2.9 280 26 - 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_union_cast_true-termination.c_true-unreach-call.i true 2 wit inspect 2.8 260 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 4.8   250  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.9 280 22 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.8  250 true 2 wit inspect 4.9   260  
ldv-regression/test_union_true-termination.c_true-unreach-call.i true 2 wit inspect 2.8 270 27 - 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_union_true-termination.c_true-unreach-call_1.i false(unreach-call) -16 wit inspect 2.7 260 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 5.8   260  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call.i true 2 wit inspect 2.9 280 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 5.6   280  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.8 280 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 5.6   270  
ldv-regression/test02_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.7 270 25 false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 4.0   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.2 270 25 true -32 wit inspect 3.0  260 true -32 wit inspect 4.6   230   unknown 0 wit inspect 2.8  180 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 3.0 280 25 true -32 wit inspect 2.8  250 false(unreach-call) 1 wit inspect 5.1   260   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .61   21    - wit inspect - wit inspect
ldv-regression/test12_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.8 280 28 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 .56   18    - wit inspect - wit inspect
ldv-regression/test21_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.8 270 27 true -32 wit inspect 2.9  260 false(unreach-call) 1 wit inspect 5.0   260   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/test22_false-unreach-call.c false(unreach-call) 1 wit inspect 9.4 460 76 true -32 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 9.6   440   unknown 0 wit inspect 3.3  230 true -32 wit inspect .82   18    - wit inspect - wit inspect
ldv-regression/test23_false-unreach-call.c false(unreach-call) 0 wit inspect 19   850 150 true -32 wit inspect 3.4  250 timeout 0 wit inspect 97     6500   unknown 0 wit inspect 3.2  210 true -32 wit inspect .62   19    - wit inspect - wit inspect
ldv-regression/test24_false-unreach-call.c false(unreach-call) 0 wit inspect 13   610 120 true -32 wit inspect 3.6  260 out of memory 0 wit inspect 71     7000   unknown 0 wit inspect 3.0  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 27   1200 250 true -32 wit inspect 3.4  260 out of memory 0 wit inspect 72     7000   unknown 0 wit inspect 3.2  220 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 2.7 270 25 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 4.8   260   unknown 0 wit inspect 2.6  190 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/test27_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.4 470 61 true -32 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 43     970   unknown 0 wit inspect 3.1  210 error (2) 0 wit inspect .62   19    - wit inspect - wit inspect
ldv-regression/test28_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.2 280 29 true -32 wit inspect 2.9  260 false(unreach-call) 1 wit inspect 7.9   270   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/test29_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.3 280 33 true -32 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 6.2   260   unknown 0 wit inspect 2.6  180 true -32 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/test30_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 2.8 270 29 true -32 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 5.2   260   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/test01_true-unreach-call_true-termination.c true 2 wit inspect 2.7 260 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 5.3   270  
ldv-regression/test03_true-unreach-call_true-termination.c true 2 wit inspect 2.9 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 7.1   280  
ldv-regression/test04_true-unreach-call_true-termination.c true 2 wit inspect 2.9 280 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 6.2   270  
ldv-regression/test05_true-unreach-call_true-termination.c true 2 wit inspect 3.6 280 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 9.9   500  
ldv-regression/test07_true-unreach-call_true-termination.c true 2 wit inspect 3.5 260 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 8.5   350  
ldv-regression/test09_true-unreach-call_true-termination.c true 2 wit inspect 3.1 280 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.8  250 true 2 wit inspect 7.8   340  
ldv-regression/test10_true-unreach-call_true-termination.c true 2 wit inspect 3.1 280 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 14     500  
ldv-regression/test11_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.6  250 true 2 wit inspect 7.2   270  
ldv-regression/test13_true-unreach-call_true-termination.c true 2 wit inspect 2.9 280 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  270 true 2 wit inspect 5.0   260  
ldv-regression/test14_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.8  250 true 2 wit inspect 6.4   260  
ldv-regression/test15_true-unreach-call_true-termination.c true 2 wit inspect 3.0 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.8  250 true 2 wit inspect 7.3   280  
ldv-regression/test16_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.6  250 true 2 wit inspect 7.1   280  
ldv-regression/test17_true-unreach-call_true-termination.c true 2 wit inspect 2.7 280 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 6.1   250  
ldv-regression/test18_true-unreach-call_true-termination.c true 2 wit inspect 3.0 280 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 6.9   300  
ldv-regression/test19_true-unreach-call_true-termination.c true 2 wit inspect 3.0 280 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 8.8   350  
ldv-regression/test20_true-unreach-call_true-termination.c true 2 wit inspect 2.9 280 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.1   260  
ldv-regression/test21_true-unreach-call_true-termination.c true 2 wit inspect 3.3 280 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 8.8   330  
ldv-regression/test22_true-unreach-call.c true 2 wit inspect 11   460 88 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6  290 true 2 wit inspect 21     630  
ldv-regression/test23_true-unreach-call.c true 2 wit inspect 46   2200 390 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.8  290 true 2 wit inspect 250     770  
ldv-regression/test24_true-unreach-call_true-termination.c true 2 wit inspect 9.1 460 72 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.3  290 true 2 wit inspect 8.8   420  
ldv-regression/test25_true-unreach-call.c true 2 wit inspect 16   620 130 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 16    370 true 2 wit inspect 26     570  
ldv-regression/test26_true-unreach-call_true-termination.c true 2 wit inspect 3.0 260 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.8  250 true 2 wit inspect 7.7   300  
ldv-regression/test27_true-unreach-call_true-termination.c true 2 wit inspect 36   1900 320 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 27    480 true 2 wit inspect 160     810  
ldv-regression/test28_true-unreach-call_true-termination.c timeout 0 wit inspect 900   5600 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 43 error (2) 0 wit inspect .025 4.8
ldv-regression/test29_true-unreach-call_true-termination.c true 2 wit inspect 3.6 290 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 8.2   260  
ldv-regression/test30_true-unreach-call_true-termination.c true 2 wit inspect 3.1 260 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  270 true 2 wit inspect 11     430  
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 13   500 110 true -32 wit inspect 6.5  270 timeout 0 wit inspect 96     1200   unknown 0 wit inspect 5.2  270 false(unreach-call) 1 wit inspect 1.2    19    - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 13   500 110 true -32 wit inspect 6.3  270 timeout 0 wit inspect 96     1100   unknown 0 wit inspect 5.3  290 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 13   480 94 true -32 wit inspect 6.3  270 timeout 0 wit inspect 97     1200   unknown 0 wit inspect 5.3  270 false(unreach-call) 1 wit inspect 1.2    19    - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 4.6 290 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.7  280 true 2 wit inspect 11     430  
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 4.6 290 39 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.9  280 true 2 wit inspect 11     430  
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 4.8 290 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.4  280 true 2 wit inspect 12     430  
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 4.8 290 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.0  280 true 2 wit inspect 11     430  
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 4.7 290 42 - 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_outb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 4.7 290 39 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.8  290 true 2 wit inspect 14     470  
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 4.6 300 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.7  300 true 2 wit inspect 11     430  
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 4.8 290 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1  290 true 2 wit inspect 12     430  
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 4.8 300 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.7  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 4.9 290 42 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.3  280 true 2 wit inspect 12     430  
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   4400 11000 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .025 4.9 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0042 .26 - wit inspect - wit inspect
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 9.0 460 72 true -32 wit inspect 4.0  270 false(unreach-call) 1 wit inspect 26     730   unknown 0 wit inspect 3.6  220 false(unreach-call) 1 wit inspect .64   19    - wit inspect - wit inspect
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 3.9 280 37 true -32 wit inspect 3.7  250 false(unreach-call) 1 wit inspect 6.1   280   unknown 0 wit inspect 3.3  250 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 38   1400 280 true -32 wit inspect 4.4  260 false(unreach-call) 1 wit inspect 7.4   350   unknown 0 wit inspect 3.8  250 false(unreach-call) 1 wit inspect .66   19    - wit inspect - wit inspect
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 4.6 290 44 true -32 wit inspect 3.9  250 false(unreach-call) 1 wit inspect 5.8   280   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .66   18    - wit inspect - wit inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   4300 12000 error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .025 4.9 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0019 .34 - wit inspect - wit inspect
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 3.8 280 31 true -32 wit inspect 3.7  250 false(unreach-call) 1 wit inspect 5.6   270   unknown 0 wit inspect 3.5  250 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 7.1 380 55 true -32 wit inspect 4.0  250 false(unreach-call) 1 wit inspect 7.8   300   unknown 0 wit inspect 3.6  250 false(unreach-call) 1 wit inspect .64   19    - wit inspect - wit inspect
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.4 290 40 true -32 wit inspect 3.7  250 false(unreach-call) 1 wit inspect 6.1   280   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .64   18    - wit inspect - wit inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i timeout 0 wit inspect 900   4200 11000 error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0041 .35 - wit inspect - wit inspect
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 13   490 95 true -32 wit inspect 4.2  260 true -32 wit inspect 5.4   250   unknown 0 wit inspect 3.9  240 false(unreach-call) 1 wit inspect .68   19    - wit inspect - wit inspect
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 8.8 460 61 true -32 wit inspect 4.0  250 false(unreach-call) 1 wit inspect 73     850   unknown 0 wit inspect 3.5  250 false(unreach-call) 1 wit inspect .68   19    - wit inspect - wit inspect
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 3.9 280 33 true -32 wit inspect 4.0  270 false(unreach-call) 1 wit inspect 5.8   280   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .66   18    - wit inspect - wit inspect
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 38   1700 300 true -32 wit inspect 4.3  260 false(unreach-call) 1 wit inspect 7.3   340   unknown 0 wit inspect 3.8  260 false(unreach-call) 1 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 4.5 290 35 true -32 wit inspect 3.7  250 false(unreach-call) 1 wit inspect 5.8   280   unknown 0 wit