Tool ESBMC ESBMC version 4.6.0 64-bit x86_64 linux 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* [apollon073; apollon077; apollon078; apollon119; apollon130] apollon* [apollon077; apollon078; apollon091; apollon114] apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 33553 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-01 12:59:33 CET 2017-12-02 09:20:19 CET 2017-12-02 10:53:45 CET 2017-12-02 11:06:16 CET 2017-12-02 11:21:21 CET 2017-12-02 06:57:43 CET 2017-12-02 09:56:59 CET
Run set esbmc-kind.sv-comp18.ReachSafety-Heap cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-Heap uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.ReachSafety-Heap uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.ReachSafety-Heap
Options -s kinduction -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-01_1259.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/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-01_1259.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/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/esbmc-kind.2017-12-01_1259.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) 0 wit inspect 3.5   89 40    error (invalid witness file) 0 wit inspect 3.7  210 true -32 wit inspect 6.4   260   error (invalid witness file) 0 wit inspect 2.2  210 error (1) 0 wit inspect .62   18    - wit inspect - wit inspect
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900     12000 5700    error (invalid witness file) 0 wit inspect .50 41 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .40  29 3.1  false(unreach-call) 1 wit inspect 4.5  270 true -32 wit inspect 7.5   300   unknown 0 wit inspect 2.4  210 true -32 wit inspect .64   18    - wit inspect - wit inspect
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 1.1   30 9.6  unknown 0 wit inspect 6.1  280 true -32 wit inspect 6.0   260   unknown 0 wit inspect 2.5  220 true -32 wit inspect .64   18    - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(unreach-call) 0 wit inspect .69  29 5.8  error (invalid witness file) 0 wit inspect 1.8  180 true -32 wit inspect 7.0   280   error (invalid witness file) 0 wit inspect 2.9  190 error (1) 0 wit inspect .59   18    - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .73  29 5.2  error (invalid witness file) 0 wit inspect 2.8  180 true -32 wit inspect 8.2   290   error (invalid witness file) 0 wit inspect 2.9  190 error (1) 0 wit inspect .58   18    - wit inspect - wit inspect
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     11000 8200    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .025 4.8
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900     3200 7000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 42 error (2) 0 wit inspect .019 4.9
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     12000 6600    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .019 4.8
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     4500 9800    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .026 5.0
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     3000 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.9
heap-manipulation/tree_true-unreach-call.i timeout 0 wit inspect 900     4200 8600    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .024 4.9
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .34  29 3.2  false(unreach-call) 1 wit inspect 3.9  270 true -32 wit inspect 3.4   230   unknown 0 wit inspect 2.2  210 true -32 wit inspect .66   18    - wit inspect - wit inspect
list-properties/list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .57  30 6.1  false(unreach-call) 1 wit inspect 4.7  270 false(unreach-call) 1 wit inspect 6.0   260   unknown 0 wit inspect 2.3  210 true -32 wit inspect .67   18    - wit inspect - wit inspect
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .36  29 2.9  false(unreach-call) 1 wit inspect 3.9  270 false(unreach-call) 1 wit inspect 4.1   270   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .93  29 8.1  false(unreach-call) 1 wit inspect 4.1  270 true -32 wit inspect 6.4   280   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .37  29 4.0  false(unreach-call) 1 wit inspect 2.6  270 false(unreach-call) 1 wit inspect 6.1   270   unknown 0 wit inspect 2.3  210 true -32 wit inspect .65   18    - wit inspect - wit inspect
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .39  29 3.5  false(unreach-call) 1 wit inspect 4.9  270 true -32 wit inspect 5.4   250   unknown 0 wit inspect 3.2  210 true -32 wit inspect .63   18    - wit inspect - wit inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900     5400 8600    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 44 error (2) 0 wit inspect .019 5.0
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900     3400 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .020 4.8
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i true 2 wit inspect .30  27 3.0  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 26    520 true 2 wit inspect 85     1100  
list-properties/list_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900     1600 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .74 44 error (2) 0 wit inspect .024 4.9
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900     2900 9100    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .019 4.9
list-properties/simple_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900     3400 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .021 4.8
list-properties/splice_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900     3400 9500    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 44 error (2) 0 wit inspect .018 4.8
ldv-regression/1_3_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .21  28 2.0  false(unreach-call) 1 wit inspect 3.0  270 false(unreach-call) 1 wit inspect 5.4   260   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/alt_test_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .12  29 1.1  false(unreach-call) 1 wit inspect 3.9  270 true -32 wit inspect 4.8   230   unknown 0 wit inspect 2.4  210 false(unreach-call) 1 wit inspect .67   19    - wit inspect - wit inspect
ldv-regression/callfpointer_true-termination.c_false-unreach-call.i unknown 0 wit inspect .074 26 .79 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .86 50 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
ldv-regression/fo_test_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .18  28 1.1  false(unreach-call) 1 wit inspect 4.1  260 true -32 wit inspect 4.8   230   unknown 0 wit inspect 2.3  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 .10  28 .84 false(unreach-call) 1 wit inspect 3.1  260 true -32 wit inspect 5.5   270   unknown 0 wit inspect 1.9  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 .20  28 1.6  false(unreach-call) 1 wit inspect 3.2  250 false(unreach-call) 1 wit inspect 4.9   240   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
ldv-regression/recursive_list_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .19  28 1.8  false(unreach-call) 1 wit inspect 3.3  260 true -32 wit inspect 5.4   230   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .57   19    - wit inspect - wit inspect
ldv-regression/rule57_ebda_blast_true-termination.c_false-unreach-call.i false(unreach-call) 0 wit inspect .34  29 3.4  true -32 wit inspect 4.4  260 true -32 wit inspect 5.2   230   unknown 0 wit inspect 2.8  210 error (2) 0 wit inspect .56   18    - wit inspect - wit inspect
ldv-regression/rule60_list2_true-termination.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect .25  29 2.8  false(unreach-call) 1 wit inspect 3.9  270 true -32 wit inspect 5.1   240   unknown 0 wit inspect 3.3  210 true -32 wit inspect .63   18    - wit inspect - wit inspect
ldv-regression/stateful_check_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect .24  28 2.2  false(unreach-call) 1 wit inspect 2.4  260 true -32 wit inspect 5.4   220   unknown 0 wit inspect 2.1  210 true -32 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .12  28 .85 false(unreach-call) 1 wit inspect 2.2  260 true -32 wit inspect 5.8   260   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect .11  28 .74 false(unreach-call) 1 wit inspect 2.3  260 true -32 wit inspect 5.1   250   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call.i true 2 wit inspect .073 26 .77 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 8.5   270  
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i true 2 wit inspect .072 26 .78 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 6.0   260  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call.i true 2 wit inspect .10  26 .67 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 6.2   270  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call_1.i true 2 wit inspect .072 26 .82 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 5.3   260  
ldv-regression/ex3_forlist_true-termination.c_true-unreach-call.i true 2 wit inspect .20  27 1.7  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 21    490 true 2 wit inspect 34     730  
ldv-regression/just_assert_true-termination.c_true-unreach-call.i true 2 wit inspect .10  26 .74 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  240 true 2 wit inspect 4.9   220  
ldv-regression/mutex_lock_int_true-termination.c_true-unreach-call_1.i true 2 wit inspect .10  26 .84 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 6.6   260  
ldv-regression/mutex_lock_struct_true-termination.c_true-unreach-call_1.i true 2 wit inspect .072 26 .70 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 4.6   260  
ldv-regression/nested_structure_noptr_true-termination.c_true-unreach-call.i true 2 wit inspect .084 26 .89 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 5.9   240  
ldv-regression/nested_structure_noptr_true-unreach-call_true-termination.i true 2 wit inspect .097 26 .71 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 5.9   260  
ldv-regression/nested_structure_ptr_true-termination.c_true-unreach-call.i true 2 wit inspect .083 26 .77 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 13     470  
ldv-regression/nested_structure_ptr_true-unreach-call_true-termination.i true 2 wit inspect .095 27 .78 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 6.6   360  
ldv-regression/nested_structure_true-termination.c_true-unreach-call.i true 2 wit inspect .079 26 .69 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 7.8   280  
ldv-regression/nested_structure_true-unreach-call_true-termination.i true 2 wit inspect .082 26 .74 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 9.3   290  
ldv-regression/oomInt_true-termination.c_true-unreach-call.i true 2 wit inspect .094 26 .74 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 3.8   260  
ldv-regression/oomInt_true-termination.c_true-unreach-call_1.i true 2 wit inspect .11  26 .70 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 4.9   250  
ldv-regression/rule57_ebda_blast_true-termination.c_true-unreach-call_1.i true 2 wit inspect .085 27 1.1  - 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 .14  27 1.2  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  250 true 2 wit inspect 16     650  
ldv-regression/rule60_list_true-termination.c_true-unreach-call.i true 2 wit inspect .11  27 .73 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  260 true 2 wit inspect 6.4   380  
ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i true 2 wit inspect .11  27 .75 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  260 true 2 wit inspect 5.4   260  
ldv-regression/structure_assignment_true-termination.c_true-unreach-call.i true 2 wit inspect .11  26 .68 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 5.1   250  
ldv-regression/test_address_true-termination.c_true-unreach-call.i true 2 wit inspect .079 27 .76 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 6.0   260  
ldv-regression/test_cut_trace_true-termination.c_true-unreach-call.i true 2 wit inspect .088 26 .65 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.5  250 true 2 wit inspect 5.0   260  
ldv-regression/test_malloc-1_true-unreach-call_true-termination.i true 2 wit inspect .10  27 .86 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  250 true 2 wit inspect 6.9   260  
ldv-regression/test_malloc-2_true-unreach-call_true-termination.i true 2 wit inspect .077 26 .92 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 7.7   260  
ldv-regression/test_overflow_true-termination.c_true-unreach-call.i true 2 wit inspect .11  27 .78 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1  250 true 2 wit inspect 4.7   260  
ldv-regression/test_union_cast-1_true-unreach-call_true-termination.i true 2 wit inspect .17  29 1.8  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 5.5   260  
ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i true 2 wit inspect .16  27 1.6  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 4.0   280  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call.i true 2 wit inspect .13  27 1.5  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 5.5   260  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call_1.i true 2 wit inspect .18  29 1.5  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 5.4   260  
ldv-regression/test_union_true-termination.c_true-unreach-call.i true 2 wit inspect .076 26 .76 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 3.3   260  
ldv-regression/test_union_true-termination.c_true-unreach-call_1.i true 2 wit inspect .099 26 .79 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 5.4   260  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call.i true 2 wit inspect .097 26 .76 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 6.5   270  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i true 2 wit inspect .086 26 .77 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 6.1   270  
ldv-regression/test02_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .12  28 .79 false(unreach-call) 1 wit inspect 2.1  260 false(unreach-call) 1 wit inspect 4.6   220   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
ldv-regression/test06_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .082 28 .76 false(unreach-call) 1 wit inspect 3.1  260 true -32 wit inspect 3.6   230   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
ldv-regression/test08_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .12  28 .88 false(unreach-call) 1 wit inspect 3.3  260 true -32 wit inspect 4.7   230   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
ldv-regression/test12_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .10  28 1.1  false(unreach-call) 1 wit inspect 3.9  260 false(unreach-call) 1 wit inspect 4.9   230   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
ldv-regression/test21_false-unreach-call_true-termination.c false(unreach-call) 0 wit inspect .37  28 3.1  error (invalid witness file) 0 wit inspect 2.9  160 false(unreach-call) 1 wit inspect 5.4   260   error (invalid witness file) 0 wit inspect 2.7  170 error (1) 0 wit inspect .54   18    - wit inspect - wit inspect
ldv-regression/test22_false-unreach-call.c false(unreach-call) 0 wit inspect .54  28 4.7  error (invalid witness file) 0 wit inspect 2.0  170 true -32 wit inspect 5.5   260   error (invalid witness file) 0 wit inspect 2.6  180 error (1) 0 wit inspect .52   18    - wit inspect - wit inspect
ldv-regression/test23_false-unreach-call.c false(unreach-call) 0 wit inspect 2.8   31 39    error (invalid witness file) 0 wit inspect 2.7  170 true -32 wit inspect 6.6   270   error (invalid witness file) 0 wit inspect 2.7  180 error (1) 0 wit inspect .53   18    - wit inspect - wit inspect
ldv-regression/test24_false-unreach-call.c unknown 0 wit inspect 2.4   51 33    error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0017 .26 - wit inspect - wit inspect
ldv-regression/test25_false-unreach-call_true-termination.c unknown 0 wit inspect .93  40 11    error (invalid witness file) 0 wit inspect .39 44 error (2) 0 wit inspect .021 5.0 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
ldv-regression/test26_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .079 28 .82 false(unreach-call) 1 wit inspect 3.0  260 true -32 wit inspect 3.3   230   unknown 0 wit inspect 2.0  180 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
ldv-regression/test27_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .88  28 8.0  false(unreach-call) 1 wit inspect 3.8  280 true -32 wit inspect 4.7   240   unknown 0 wit inspect 3.0  210 error (2) 0 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/test28_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .23  28 2.7  false(unreach-call) 1 wit inspect 2.4  260 false(unreach-call) 1 wit inspect 5.8   260   unknown 0 wit inspect 2.0  210 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 .40  28 3.6  true -32 wit inspect 3.9  260 false(unreach-call) 1 wit inspect 6.4   260   unknown 0 wit inspect 2.0  210 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 .084 28 .84 false(unreach-call) 1 wit inspect 2.2  260 true -32 wit inspect 5.3   230   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
ldv-regression/test01_true-unreach-call_true-termination.c true 2 wit inspect .095 26 .79 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 6.4   260  
ldv-regression/test03_true-unreach-call_true-termination.c true 2 wit inspect .077 26 .66 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 8.2   270  
ldv-regression/test04_true-unreach-call_true-termination.c true 2 wit inspect .095 26 .86 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 6.3   300  
ldv-regression/test05_true-unreach-call_true-termination.c true 2 wit inspect .079 26 .80 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 10     490  
ldv-regression/test07_true-unreach-call_true-termination.c true 2 wit inspect .098 26 .71 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.4  250 true 2 wit inspect 8.9   350  
ldv-regression/test09_true-unreach-call_true-termination.c true 2 wit inspect .086 26 .84 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 8.5   340  
ldv-regression/test10_true-unreach-call_true-termination.c true 2 wit inspect .076 26 .78 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  260 true 2 wit inspect 15     490  
ldv-regression/test11_true-unreach-call_true-termination.c true 2 wit inspect .073 26 .78 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 8.1   280  
ldv-regression/test13_true-unreach-call_true-termination.c true 2 wit inspect .071 26 .92 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 3.7   260  
ldv-regression/test14_true-unreach-call_true-termination.c true 2 wit inspect .10  26 .94 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 7.2   280  
ldv-regression/test15_true-unreach-call_true-termination.c true 2 wit inspect .11  26 .63 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 8.0   270  
ldv-regression/test16_true-unreach-call_true-termination.c true 2 wit inspect .077 26 .77 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 8.0   280  
ldv-regression/test17_true-unreach-call_true-termination.c true 2 wit inspect .11  26 .71 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 5.8   260  
ldv-regression/test18_true-unreach-call_true-termination.c true 2 wit inspect .11  26 .70 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 7.9   300  
ldv-regression/test19_true-unreach-call_true-termination.c true 2 wit inspect .11  26 .65 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 11     340  
ldv-regression/test20_true-unreach-call_true-termination.c true 2 wit inspect .11  26 .76 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 6.1   270  
ldv-regression/test21_true-unreach-call_true-termination.c true 2 wit inspect .11  26 1.1  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 9.1   320  
ldv-regression/test22_true-unreach-call.c true 2 wit inspect .98  27 13    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.2  290 true 2 wit inspect 24     640  
ldv-regression/test23_true-unreach-call.c true 2 wit inspect 2.3   30 26    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.2  290 true 2 wit inspect 240     750  
ldv-regression/test24_true-unreach-call_true-termination.c true 2 wit inspect 4.2   32 57    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.8  280 true 2 wit inspect 10     430  
ldv-regression/test25_true-unreach-call.c true 2 wit inspect 2.6   39 37    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 16    440 true 2 wit inspect 31     550  
ldv-regression/test26_true-unreach-call_true-termination.c true 2 wit inspect .10  26 .68 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 9.4   290  
ldv-regression/test27_true-unreach-call_true-termination.c true 2 wit inspect .20  27 2.0  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 33    490 true 2 wit inspect 150     820  
ldv-regression/test28_true-unreach-call_true-termination.c true 2 wit inspect .082 26 .90 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 8.6   270  
ldv-regression/test29_true-unreach-call_true-termination.c true 2 wit inspect .11  26 .73 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 7.5   260  
ldv-regression/test30_true-unreach-call_true-termination.c true 2 wit inspect .10  26 .60 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 9.9   440  
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect .24  42 2.5  false(unreach-call) 1 wit inspect 8.4  350 true -32 wit inspect 13     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_inw_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect .21  42 2.8  false(unreach-call) 1 wit inspect 5.5  350 true -32 wit inspect 9.5   460   unknown 0 wit inspect 3.3  270 false(unreach-call) 1 wit inspect 1.1    18    - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect .24  42 2.4  false(unreach-call) 1 wit inspect 9.6  350 true -32 wit inspect 14     470   unknown 0 wit inspect 3.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 .40  56 4.9  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.5  280 true 2 wit inspect 14     430  
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .39  56 4.4  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.9  290 true 2 wit inspect 13     440  
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .38  56 5.4  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7  280 true 2 wit inspect 12     430  
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .37  57 5.0  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.2  280 true 2 wit inspect 12     430  
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .42  56 3.8  - 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_outb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .44  56 4.3  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.5  300 true 2 wit inspect 13     430  
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .41  56 4.6  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.7  280 true 2 wit inspect 13     440  
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .39  56 4.6  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.9  280 true 2 wit inspect 15     430  
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .38  56 5.0  - 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_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .39  57 4.3  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.8  280 true 2 wit inspect 12     430  
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .88  31 7.6  false(unreach-call) 1 wit inspect 3.2  280 false(unreach-call) 1 wit inspect 17     590   unknown 0 wit inspect 3.3  210 error (2) 0 wit inspect .62   18    - wit inspect - wit inspect
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .51  29 5.2  false(unreach-call) 1 wit inspect 4.9  270 false(unreach-call) 1 wit inspect 6.3   280   unknown 0 wit inspect 2.3  210 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 .35  29 3.4  false(unreach-call) 1 wit inspect 2.5  270 false(unreach-call) 1 wit inspect 6.9   280   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .68   18    - wit inspect - wit inspect
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 1.1   30 10    false(unreach-call) 1 wit inspect 2.9  270 true -32 wit inspect 6.0   260   unknown 0 wit inspect 2.4  210 true -32 wit inspect .63   18    - wit inspect - wit inspect
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .57  29 4.9  false(unreach-call) 1 wit inspect 2.9  270 true -32 wit inspect 5.9   270   unknown 0 wit inspect 2.3  210 false(unreach-call) 1 wit inspect .63   19    - wit inspect - wit inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(unreach-call) 1 wit inspect 1.1   30 8.9  false(unreach-call) 1 wit inspect 5.5  270 true -32 wit inspect 5.8   250   unknown 0 wit inspect 2.4  210 true -32 wit inspect .66   18    - wit inspect - wit inspect
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .73  29 6.2  false(unreach-call) 1 wit inspect 2.6  270 false(unreach-call) 1 wit inspect 6.9   290   unknown 0 wit inspect 2.3  210 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .52  29 4.3  false(unreach-call) 1 wit inspect 3.8  270 true -32 wit inspect 6.5   280   unknown 0 wit inspect 2.4  210 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .44  29 6.7  error (invalid witness file) 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect 6.5   290   error (invalid witness file) 0 wit inspect 2.1  180 error (1) 0 wit inspect .61   18    - wit inspect - wit inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .83  30 7.4  false(unreach-call) 1 wit inspect 4.5  270 true -32 wit inspect 6.6   300   unknown 0 wit inspect 2.4  210 error (2) 0 wit inspect .62   18    - wit inspect - wit inspect
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .73  29 6.6  false(unreach-call) 1 wit inspect 2.8  270 true -32 wit inspect 3.9   250   unknown 0 wit inspect 2.4  210 true -32 wit inspect .63   18    - wit inspect - wit inspect
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .49  29 4.2  false(unreach-call) 1 wit inspect 3.9  270 false(unreach-call) 1 wit inspect 6.2   280   unknown 0 wit inspect 2.3  210 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .29  29 3.0  false(unreach-call) 1 wit inspect 4.0  260 false(unreach-call) 1 wit inspect 6.3   270   unknown 0 wit inspect 2.3  210 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .91  30 10    false(unreach-call) 1 wit inspect 5.1  270 true -32 wit inspect 5.9   260   unknown 0 wit inspect 3.4  210 true -32 wit inspect .63   18    - wit inspect - wit inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .44  29 2.9  false(unreach-call) 1 wit inspect 2.8  260 true -32 wit inspect 5.9   270   unknown 0 wit inspect 3.2  210