Tool 2LS 0.6.0 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-11-30 11:20:26 CET 2017-12-01 07:32:03 CET 2017-12-01 08:01:50 CET 2017-12-01 08:11:41 CET 2017-12-01 08:15:34 CET 2017-12-01 04:23:32 CET 2017-12-01 07:36:49 CET
Run set 2ls.sv-comp18.ReachSafety-Heap cpa-seq-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-Heap uautomizer-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.ReachSafety-Heap uautomizer-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.ReachSafety-Heap
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.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/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.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/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/2ls.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/2ls.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 error (134) 0 wit inspect .22  28 1.8  error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .97 48 error (invalid witness file) 0 wit inspect .0012 .29 - wit inspect - wit inspect
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i error (5) 0 wit inspect .20  27 1.7  error (invalid witness file) 0 wit inspect .53 45 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i error (5) 0 wit inspect .32  32 3.4  error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .71  48 8.9  unknown 0 wit inspect 4.7  290 true -32 wit inspect 7.6   270   unknown 0 wit inspect 3.4  220 error (1) 0 wit inspect .73   18    - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-deref.i error (5) 0 wit inspect .33  30 3.1  error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0012 .32 - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i error (5) 0 wit inspect .37  31 3.4  error (invalid witness file) 0 wit inspect .50 41 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .90 50 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i error (134) 0 wit inspect .21  29 1.6  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .022 4.8
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i error (5) 0 wit inspect .19  26 1.4  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 46 error (2) 0 wit inspect .018 5.0
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .22  27 1.9  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .018 4.8
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .31  32 3.8  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .023 4.8
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 91     15000 1100    - 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
heap-manipulation/tree_true-unreach-call.i error (5) 0 wit inspect .29  31 3.4  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .43 43 error (2) 0 wit inspect .019 4.9
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i error (5) 0 wit inspect .31  29 3.0  error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0016 .27 - wit inspect - wit inspect
list-properties/list_false-unreach-call_false-valid-memcleanup.i error (5) 0 wit inspect .36  31 2.6  error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .95 49 error (invalid witness file) 0 wit inspect .0036 .34 - wit inspect - wit inspect
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i error (5) 0 wit inspect .28  28 2.6  error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .90 49 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .26  29 2.5  unknown 0 wit inspect 4.3  270 true -32 wit inspect 19     660   unknown 0 wit inspect 4.0  210 error (1) 0 wit inspect .59   19    - wit inspect - wit inspect
list-properties/simple_false-unreach-call_false-valid-memcleanup.i error (5) 0 wit inspect .22  27 2.0  error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .73 49 error (invalid witness file) 0 wit inspect .0044 .26 - wit inspect - wit inspect
list-properties/splice_false-unreach-call_false-valid-memcleanup.i error (5) 0 wit inspect .33  30 4.0  error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0016 .29 - wit inspect - wit inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .28  29 2.5  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .018 4.9
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i error (5) 0 wit inspect .28  28 3.0  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 41 error (2) 0 wit inspect .019 4.9
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i true 2 wit inspect .23  30 2.0  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 25    540 true 2 wit inspect 65     1100  
list-properties/list_true-unreach-call_false-valid-memtrack.i error (5) 0 wit inspect .38  32 3.7  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.9
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i error (5) 0 wit inspect .23  26 1.6  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .018 4.9
list-properties/simple_true-unreach-call_false-valid-memtrack.i error (5) 0 wit inspect .27  28 2.6  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .74 42 error (2) 0 wit inspect .018 4.9
list-properties/splice_true-unreach-call_false-valid-memtrack.i error (5) 0 wit inspect .35  30 4.1  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 42 error (2) 0 wit inspect .019 4.9
ldv-regression/1_3_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .19  24 1.3  false(unreach-call) 1 wit inspect 3.2  260 true -32 wit inspect 4.7   230   unknown 0 wit inspect 2.8  210 error (1) 0 wit inspect .53   18    - wit inspect - wit inspect
ldv-regression/alt_test_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .19  27 2.0  false(unreach-call) 1 wit inspect 3.8  260 false(unreach-call) 1 wit inspect 7.2   270   unknown 0 wit inspect 3.3  210 error (1) 0 wit inspect .84   18    - wit inspect - wit inspect
ldv-regression/callfpointer_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .11  22 .76 false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 5.7   240   unknown 0 wit inspect 3.4  180 false(unreach-call) 1 wit inspect .76   18    - wit inspect - wit inspect
ldv-regression/fo_test_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .21  27 1.6  false(unreach-call) 1 wit inspect 3.9  260 unknown 0 wit inspect 12     290   unknown 0 wit inspect 3.4  210 error (1) 0 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .11  22 .86 true -32 wit inspect 2.9  250 false(unreach-call) 1 wit inspect 5.8   250   unknown 0 wit inspect 3.8  210 false(unreach-call) 1 wit inspect .59   19    - wit inspect - wit inspect
ldv-regression/mutex_lock_struct_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .12  22 .69 false(unreach-call) 1 wit inspect 3.2  270 false(unreach-call) 1 wit inspect 6.9   260   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .73   18    - wit inspect - wit inspect
ldv-regression/recursive_list_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .20  24 1.4  false(unreach-call) 1 wit inspect 3.3  260 true -32 wit inspect 5.0   230   unknown 0 wit inspect 3.4  190 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/rule57_ebda_blast_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .14  23 .87 true -32 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 6.2   270   unknown 0 wit inspect 3.0  210 error (2) 0 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/rule60_list2_true-termination.c_false-unreach-call_1.i error (134) 0 wit inspect .12  25 .56 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0018 .29 - wit inspect - wit inspect
ldv-regression/stateful_check_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect .65  37 7.9  true -32 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 6.3   270   unknown 0 wit inspect 3.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 .16  24 1.6  false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 4.5   240   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect .17  24 1.5  false(unreach-call) 1 wit inspect 3.0  250 false(unreach-call) 1 wit inspect 5.0   240   unknown 0 wit inspect 3.0  210 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 .097 22 .87 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 5.8   270  
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i true 2 wit inspect .10  22 .66 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 5.6   260  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call.i true 2 wit inspect .087 22 .71 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 6.3   270  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call_1.i true 2 wit inspect .11  22 .51 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 5.4   260  
ldv-regression/ex3_forlist_true-termination.c_true-unreach-call.i false(unreach-call) -16 wit inspect .42  33 5.4  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  260 true 2 wit inspect 22     650  
ldv-regression/just_assert_true-termination.c_true-unreach-call.i true 2 wit inspect .12  22 .76 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  240 true 2 wit inspect 4.2   220  
ldv-regression/mutex_lock_int_true-termination.c_true-unreach-call_1.i true 2 wit inspect .098 22 .69 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 6.1   260  
ldv-regression/mutex_lock_struct_true-termination.c_true-unreach-call_1.i true 2 wit inspect .10  22 .87 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 6.9   280  
ldv-regression/nested_structure_noptr_true-termination.c_true-unreach-call.i true 2 wit inspect .080 22 .75 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 4.5   230  
ldv-regression/nested_structure_noptr_true-unreach-call_true-termination.i true 2 wit inspect .10  22 .95 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  260 true 2 wit inspect 5.0   260  
ldv-regression/nested_structure_ptr_true-termination.c_true-unreach-call.i true 2 wit inspect .12  22 .72 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 11     480  
ldv-regression/nested_structure_ptr_true-unreach-call_true-termination.i true 2 wit inspect .099 22 .73 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 8.8   410  
ldv-regression/nested_structure_true-termination.c_true-unreach-call.i true 2 wit inspect .11  22 .65 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 7.9   280  
ldv-regression/nested_structure_true-unreach-call_true-termination.i true 2 wit inspect .12  22 .64 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 7.6   300  
ldv-regression/oomInt_true-termination.c_true-unreach-call.i true 2 wit inspect .11  22 .65 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 5.8   260  
ldv-regression/oomInt_true-termination.c_true-unreach-call_1.i true 2 wit inspect .11  22 .71 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 5.7   270  
ldv-regression/rule57_ebda_blast_true-termination.c_true-unreach-call_1.i true 2 wit inspect .11  23 .84 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  250 true 2 wit inspect 6.0   270  
ldv-regression/rule60_list2_true-termination.c_true-unreach-call.i error (134) 0 wit inspect .11  25 .72 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .020 4.8
ldv-regression/rule60_list_true-termination.c_true-unreach-call.i true 2 wit inspect .18  26 1.2  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  260 true 2 wit inspect 8.9   380  
ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i true 2 wit inspect .12  24 .83 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 5.2   260  
ldv-regression/structure_assignment_true-termination.c_true-unreach-call.i true 2 wit inspect .11  22 .65 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 5.9   250  
ldv-regression/test_address_true-termination.c_true-unreach-call.i true 2 wit inspect .12  24 .79 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 5.6   260  
ldv-regression/test_cut_trace_true-termination.c_true-unreach-call.i true 2 wit inspect .11  22 .63 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  240 true 2 wit inspect 5.4   260  
ldv-regression/test_malloc-1_true-unreach-call_true-termination.i true 2 wit inspect .20  26 1.7  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  270 true 2 wit inspect 7.0   270  
ldv-regression/test_malloc-2_true-unreach-call_true-termination.i true 2 wit inspect .11  25 .82 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 5.9   260  
ldv-regression/test_overflow_true-termination.c_true-unreach-call.i true 2 wit inspect .096 26 .79 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  250 true 2 wit inspect 5.2   260  
ldv-regression/test_union_cast-1_true-unreach-call_true-termination.i true 2 wit inspect .12  22 .63 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 5.1   270  
ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i true 2 wit inspect .11  22 .77 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 7.0   250  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call.i true 2 wit inspect .080 22 .84 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 5.1   260  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call_1.i true 2 wit inspect .098 22 .65 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  240 true 2 wit inspect 6.4   250  
ldv-regression/test_union_true-termination.c_true-unreach-call.i true 2 wit inspect .082 22 .76 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  240 true 2 wit inspect 5.3   270  
ldv-regression/test_union_true-termination.c_true-unreach-call_1.i true 2 wit inspect .086 22 .68 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  240 true 2 wit inspect 5.1   270  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call.i true 2 wit inspect .097 22 .67 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 6.2   270  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i true 2 wit inspect .099 22 .74 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 5.5   280  
ldv-regression/test02_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .10  22 .83 true -32 wit inspect 2.8  260 true -32 wit inspect 4.3   220   unknown 0 wit inspect 2.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 .096 22 .97 true -32 wit inspect 3.2  260 true -32 wit inspect 5.1   230   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .62   18    - wit inspect - wit inspect
ldv-regression/test08_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .14  22 .85 true -32 wit inspect 3.3  260 true -32 wit inspect 5.1   230   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/test12_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .13  22 .84 true -32 wit inspect 3.1  260 true -32 wit inspect 4.7   230   unknown 0 wit inspect 3.1  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 .11  22 .80 false(unreach-call) 1 wit inspect 3.5  260 true -32 wit inspect 4.7   230   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .73   18    - wit inspect - wit inspect
ldv-regression/test22_false-unreach-call.c false(unreach-call) 1 wit inspect .14  25 .87 false(unreach-call) 1 wit inspect 3.4  270 true -32 wit inspect 6.2   230   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/test23_false-unreach-call.c error (134) 0 wit inspect .097 22 .89 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .017 4.9 error (invalid witness file) 0 wit inspect .97 47 error (invalid witness file) 0 wit inspect .0012 .32 - wit inspect - wit inspect
ldv-regression/test24_false-unreach-call.c error (134) 0 wit inspect .10  22 .71 error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .86 51 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
ldv-regression/test25_false-unreach-call_true-termination.c error (134) 0 wit inspect .084 22 .92 error (invalid witness file) 0 wit inspect .52 44 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0013 .31 - wit inspect - wit inspect
ldv-regression/test26_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .12  22 .94 true -32 wit inspect 2.8  260 true -32 wit inspect 4.8   220   unknown 0 wit inspect 2.9  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/test27_false-unreach-call_true-termination.c error (134) 0 wit inspect .12  22 .71 error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0017 .27 - wit inspect - wit inspect
ldv-regression/test28_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .14  22 .81 true -32 wit inspect 3.0  250 true -32 wit inspect 6.0   230   unknown 0 wit inspect 2.9  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) 0 wit inspect .12  22 .92 true -32 wit inspect 3.2  270 true -32 wit inspect 5.0   250   unknown 0 wit inspect 2.9  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 .10  22 .86 true -32 wit inspect 3.1  250 true -32 wit inspect 4.7   240   unknown 0 wit inspect 2.6  190 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 .12  22 .62 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 5.0   260  
ldv-regression/test03_true-unreach-call_true-termination.c true 2 wit inspect .090 22 .87 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 6.6   270  
ldv-regression/test04_true-unreach-call_true-termination.c true 2 wit inspect .10  22 .89 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 6.5   270  
ldv-regression/test05_true-unreach-call_true-termination.c true 2 wit inspect .13  22 .76 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 9.6   480  
ldv-regression/test07_true-unreach-call_true-termination.c true 2 wit inspect .13  22 .71 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 8.3   350  
ldv-regression/test09_true-unreach-call_true-termination.c true 2 wit inspect .12  22 .72 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 8.1   340  
ldv-regression/test10_true-unreach-call_true-termination.c true 2 wit inspect .11  22 .95 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  250 true 2 wit inspect 12     490  
ldv-regression/test11_true-unreach-call_true-termination.c true 2 wit inspect .11  22 .93 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 7.0   270  
ldv-regression/test13_true-unreach-call_true-termination.c true 2 wit inspect .11  22 .74 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 6.3   260  
ldv-regression/test14_true-unreach-call_true-termination.c true 2 wit inspect .098 22 .81 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 6.4   270  
ldv-regression/test15_true-unreach-call_true-termination.c true 2 wit inspect .12  22 .83 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 7.8   290  
ldv-regression/test16_true-unreach-call_true-termination.c true 2 wit inspect .12  22 .79 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 7.3   280  
ldv-regression/test17_true-unreach-call_true-termination.c true 2 wit inspect .10  22 .76 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 5.0   260  
ldv-regression/test18_true-unreach-call_true-termination.c true 2 wit inspect .10  22 .70 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 7.0   300  
ldv-regression/test19_true-unreach-call_true-termination.c true 2 wit inspect .11  22 .72 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 9.1   350  
ldv-regression/test20_true-unreach-call_true-termination.c true 2 wit inspect .10  22 .74 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.0   260  
ldv-regression/test21_true-unreach-call_true-termination.c true 2 wit inspect .11  22 .95 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  270 true 2 wit inspect 7.5   300  
ldv-regression/test22_true-unreach-call.c true 2 wit inspect .21  25 2.5  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7  290 true 2 wit inspect 23     640  
ldv-regression/test23_true-unreach-call.c error (134) 0 wit inspect .11  22 .65 - 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
ldv-regression/test24_true-unreach-call_true-termination.c error (134) 0 wit inspect .11  22 .65 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 42 error (2) 0 wit inspect .019 4.9
ldv-regression/test25_true-unreach-call.c error (134) 0 wit inspect .12  22 .67 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 42 error (2) 0 wit inspect .018 4.9
ldv-regression/test26_true-unreach-call_true-termination.c true 2 wit inspect .11  22 .64 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 7.9   290  
ldv-regression/test27_true-unreach-call_true-termination.c error (134) 0 wit inspect .11  22 .63 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .024 4.8
ldv-regression/test28_true-unreach-call_true-termination.c true 2 wit inspect .11  22 1.1  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  260 true 2 wit inspect 7.5   270  
ldv-regression/test29_true-unreach-call_true-termination.c true 2 wit inspect .12  22 .84 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 7.4   260  
ldv-regression/test30_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect .13  22 1.0  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  260 true 2 wit inspect 4.6   230  
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i error (134) 0 wit inspect .48  40 3.8  error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0015 .27 - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i error (134) 0 wit inspect .38  40 3.4  error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0017 .26 - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i error (134) 0 wit inspect .45  40 3.2  error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i error (134) 0 wit inspect .37  40 3.5  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 4.9
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i error (134) 0 wit inspect .38  40 2.8  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .024 4.9
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i error (134) 0 wit inspect .38  40 3.1  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .019 4.9
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i error (134) 0 wit inspect .40  40 2.9  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .022 4.8
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i error (134) 0 wit inspect .40  40 3.0  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .019 4.9
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i error (134) 0 wit inspect .38  40 2.5  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 42 error (2) 0 wit inspect .020 4.9
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i error (134) 0 wit inspect .40  40 3.0  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 41 error (2) 0 wit inspect .019 4.9
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i error (134) 0 wit inspect .41  40 3.1  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .020 4.9
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i error (134) 0 wit inspect .41  40 2.9  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .018 5.0
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i error (134) 0 wit inspect .43  40 3.3  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .019 4.9
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .37  30 3.3  unknown 0 wit inspect 4.1  270 false(unreach-call) 1 wit inspect 12     500   unknown 0 wit inspect 4.2  210 error (1) 0 wit inspect .60   18    - wit inspect - wit inspect
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i out of memory 0 wit inspect 92     15000 1200    error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .025 4.8 error (invalid witness file) 0 wit inspect 1.1  50 error (invalid witness file) 0 wit inspect .0013 .27 - wit inspect - wit inspect
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .29  29 3.0  false(unreach-call) 1 wit inspect 3.8  270 false(unreach-call) 1 wit inspect 7.6   270   unknown 0 wit inspect 3.4  210 error (1) 0 wit inspect .80   18    - wit inspect - wit inspect
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i error (5) 0 wit inspect .28  29 2.9  error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .93 49 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect - wit inspect
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .25  30 2.2  false(unreach-call) 1 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 6.3   280   unknown 0 wit inspect 3.4  210 error (1) 0 wit inspect .60   19    - wit inspect - wit inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 98     15000 1500    error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0014 .28 - wit inspect - wit inspect
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .24  27 1.9  true -32 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 7.6   270   unknown 0 wit inspect 3.7  210 error (1) 0 wit inspect .59   18    - wit inspect - wit inspect
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i error (5) 0 wit inspect .38  31 3.5  error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .81 47 error (invalid witness file) 0 wit inspect .0015 .27 - wit inspect - wit inspect
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .25  29 1.9  false(unreach-call) 1 wit inspect 3.9  270 false(unreach-call) 1 wit inspect 8.5   280   unknown 0 wit inspect 3.4  210 error (1) 0 wit inspect .62   18    - wit inspect - wit inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i error (5) 0 wit inspect .32  29 2.8  error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0018 .29 - wit inspect - wit inspect
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i error (5) 0 wit inspect .34  29 2.4  error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect 1.0  48 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .32  29 3.2  false(unreach-call) 1 wit inspect 3.9  270 false(unreach-call) 1 wit inspect 11     360   unknown 0 wit inspect 3.3  210 error (1) 0 wit inspect .59   18    - wit inspect - wit inspect
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .31  28 2.6  false(unreach-call) 1 wit inspect 3.7  270 false(unreach-call) 1 wit inspect 7.3   280   unknown 0 wit inspect 3.8  230 error (1) 0 wit inspect .63   18    - wit inspect - wit inspect
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i error (5) 0 wit inspect .30  30 3.1  error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .89 51 error (invalid witness file) 0 wit inspect .0021 .27 - wit inspect - wit inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .25  27 2.7  false(unreach-call) 1 wit inspect 3.8  260 false(unreach-call) 1 wit inspect 6.1   270   unknown 0 wit inspect 3.2  210 error (1) 0 wit inspect .70   18    - wit inspect - wit inspect
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i error (5) 0 wit inspect .37  33 3.9  error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0016 .27 - wit inspect - wit inspect
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .25  27 1.9  true -32 wit inspect 3.8  260 false(unreach-call) 1 wit inspect 5.4   260   unknown 0 wit inspect 3.5  210 error (1) 0 wit inspect .62   18    - wit inspect - wit inspect
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i error (5) 0 wit inspect .31  30 2.9  error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .85 49 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .23  27 2.0  false(unreach-call) 1 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 5.9   280   unknown 0 wit inspect 3.3  210 error (1) 0 wit inspect .66   19    - wit inspect - wit inspect
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .33  29 3.4  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .018 4.8
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .31  30 3.6  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .017 4.9
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .32  30 3.0  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .018 4.9
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .25  29 2.5  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 41 error (2) 0 wit inspect .018 4.8
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 71     15000 890    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .018 4.8
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 98     15000 1400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .019 4.9
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 100     15000 1400    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 46 error (2) 0 wit inspect .018 4.9
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i error (8) 0 wit inspect .33  30 3.5  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 42 error (2) 0 wit inspect .019 5.0
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .40  30 4.1  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .74 43 error (2) 0 wit inspect .018 4.9
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i error (8) 0 wit inspect .33  30 3.6  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .019 4.9
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .30  29 3.3  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .019 4.9
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .31  29 3.5  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .022 4.9
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .31  30 3.1  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 42 error (2) 0 wit inspect .023 4.8
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .34  29 2.4  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .020 4.8
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .32  30 2.5  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .019 4.9
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .23  28 2.0  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 46 error (2) 0 wit inspect .019 5.0
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .36  33 3.4  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.9
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .34  30 3.4  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 4.9
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i error (8) 0 wit inspect .27  29 2.4  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .019 4.9
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .39  32 4.0  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .024 4.8
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i error (8) 0 wit inspect .34  30 3.4  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 4.9
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .73  37 9.0  false(unreach-call) 1 wit inspect 4.3  270 false(unreach-call) 1 wit inspect 6.0   280   unknown 0 wit inspect 3.7  210 error (1) 0 wit inspect .69   18    - wit inspect - wit inspect
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i error (5) 0 wit inspect .35  32 3.1  error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect 1.1  47 error (invalid witness file) 0 wit inspect .0013 .27 - wit inspect - wit inspect
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup_true-termination.i false(unreach-call) 1 wit inspect .32  29 2.9  false(unreach-call) 1 wit inspect 4.3  270 false(unreach-call) 1 wit inspect 5.6   260   unknown 0 wit inspect 3.2  210 error (1) 0 wit inspect .69   18    - wit inspect - wit inspect
list-ext2-properties/list_and_tree_cnstr_false-unreach-call_false-termination.i error (5) 0 wit inspect .60  35 7.0  error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .88 51 error (invalid witness file) 0 wit inspect .0015 .29 - wit inspect - wit inspect
list-ext2-properties/list_and_tree_cnstr_true-unreach-call_false-termination.i error (5) 0 wit inspect .61  35 6.3  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.9
list-ext2-properties/simple_and_skiplist_2lvl_false-unreach-call.i error (5) 0 wit inspect .57  34 6.3  error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .026 4.8 error (invalid witness file) 0 wit inspect .91 49 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
list-ext2-properties/simple_and_skiplist_2lvl_true-unreach-call.i error (5) 0 wit inspect .50  33 5.8  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .019 4.8
list-ext2-properties/simple_search_value_false-unreach-call.i error (5) 0 wit inspect .37  30 4.0  error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
list-ext2-properties/simple_search_value_true-unreach-call.i error (5) 0 wit inspect .33  30 3.0  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 4.8
ldv-sets/test_add_false-unreach-call_true-termination.i error (134) 0 wit inspect .16  26 1.6  error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .86 48 error (invalid witness file) 0 wit inspect .0012 .33 - wit inspect - wit inspect
ldv-sets/test_mutex_double_lock_false-unreach-call_true-termination.i error (134) 0 wit inspect .20  26 2.1  error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .87 50 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect - wit inspect
ldv-sets/test_mutex_double_unlock_false-unreach-call.i error (134) 0 wit inspect .20  27 2.4  error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
ldv-sets/test_mutex_unbounded_false-unreach-call.i error (134) 0 wit inspect .20  27 1.8  error (invalid witness file) 0 wit inspect .52 45 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .82 47 error (invalid witness file) 0 wit inspect .0016 .30 - wit inspect - wit inspect
ldv-sets/test_mutex_unlock_at_exit_false-unreach-call.i error (134) 0 wit inspect .20  27 2.1  error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .024 4.9 error (invalid witness file) 0 wit inspect .83 50 error (invalid witness file) 0 wit inspect .0012 .30 - wit inspect - wit inspect
ldv-sets/test_add_true-unreach-call_true-termination.i error (134) 0 wit inspect .19  27 1.4  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .019 4.9
ldv-sets/test_mutex_true-unreach-call.i error (134) 0 wit inspect .20  27 2.1  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .048 4.8
ldv-sets/test_mutex_unbounded_true-unreach-call.i error (134) 0 wit inspect .17  27 1.8  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 44 error (2) 0 wit inspect .019 4.9
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
total 181 108 590    95000 7800   71 -397 140 11000 71 -428 240 9800 71 0 150 9000 71 -49 22   650 110 112 250 17000 110 112 460 18000
    correct results 86 140 13    2100 110   19 19 69 5000 20 20 140 5600 0 15 15 9.2 280 56 112 220 14000 56 112 460 18000
        correct true 54 108 6.2  1200 45   0 0 0 0 56 112 220 14000 56 112 460 18000
        correct false 32 32 7.1  830 65   19 19 69 5000 20 20 140 5600 0 15 15 9.2 280 0 0
    correct-unconfimed results 3 0 1.1  99 12   0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 3 0 1.1  99 12   0 0 0 0 0 0
    incorrect results 2 -32 .55 55 6.4 13 -416 42 3400 14 -448 87 3700 0 2 -64 1.2 37 0 0
        incorrect true 0 13 -416 42 3400 14 -448 87 3700 0 2 -64 1.2 37 0 0
        incorrect false 2 -32 .55 55 6.4 0 0 0 0 0 0
score (181 tasks, max score: 291) 108 -397 -428 0 -49 112 112
Run set 2ls.sv-comp18.ReachSafety-Heap cpa-seq-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-Heap uautomizer-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-2ls.sv-comp18-violation-witness.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.ReachSafety-Heap uautomizer-validate-correctness-witnesses-2ls.sv-comp18-correctness-witness.ReachSafety-Heap