Tool Map2Check Map2Check 7.1 : Wed Nov 22 22:30:11 -04 2017 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-01 19:46:39 CET 2017-12-01 22:34:51 CET 2017-12-01 23:03:48 CET 2017-12-01 23:06:19 CET 2017-12-01 23:09:14 CET 2017-12-01 22:04:37 CET 2017-12-01 22:38:34 CET
Run set map2check.sv-comp18.ReachSafety-Heap cpa-seq-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Heap uautomizer-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-map2check.sv-comp18-correctness-witness.ReachSafety-Heap uautomizer-validate-correctness-witnesses-map2check.sv-comp18-correctness-witness.ReachSafety-Heap
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/map2check.2017-12-01_1946.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/map2check.2017-12-01_1946.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/map2check.2017-12-01_1946.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/map2check.2017-12-01_1946.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/map2check.2017-12-01_1946.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/map2check.2017-12-01_1946.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 .48  12 5.5  unknown 0 wit inspect 6.4  260 true -32 wit inspect 6.4   270   unknown 0 wit inspect 4.9  250 false(unreach-call) 1 wit inspect .92   19    - wit inspect - wit inspect
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .56  12 7.1  true -32 wit inspect 3.1  260 true -32 wit inspect 6.3   270   unknown 0 wit inspect 4.9  250 true -32 wit inspect .75   19    - wit inspect - wit inspect
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .49  12 5.9  false(unreach-call) 1 wit inspect 5.1  260 true -32 wit inspect 7.9   300   unknown 0 wit inspect 4.4  250 false(unreach-call) 1 wit inspect .79   19    - wit inspect - wit inspect
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .49  12 5.1  unknown 0 wit inspect 4.6  260 true -32 wit inspect 6.7   270   unknown 0 wit inspect 4.8  250 false(unreach-call) 1 wit inspect .67   18    - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .49  12 5.6  unknown 0 wit inspect 4.9  260 true -32 wit inspect 3.9   250   unknown 0 wit inspect 4.4  250 false(unreach-call) 1 wit inspect .75   18    - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .51  12 6.0  unknown 0 wit inspect 5.1  260 true -32 wit inspect 6.7   250   unknown 0 wit inspect 2.5  260 false(unreach-call) 1 wit inspect .66   18    - wit inspect - wit inspect
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900     230 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.8
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .29  11 3.2  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .021 4.8
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900     1600 9200    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .026 4.9
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900     250 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .027 4.9
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900     440 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .023 4.8
heap-manipulation/tree_true-unreach-call.i unknown 0 wit inspect 900     2100 9600    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .023 4.9
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .44  12 4.9  false(unreach-call) 1 wit inspect 3.7  250 false(unreach-call) 1 wit inspect 7.2   260   unknown 0 wit inspect 4.0  250 false(unreach-call) 1 wit inspect .72   18    - wit inspect - wit inspect
list-properties/list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .93  13 11    unknown 0 wit inspect 5.0  260 true -32 wit inspect 4.2   280   unknown 0 wit inspect 3.8  260 false(unreach-call) 1 wit inspect .69   19    - wit inspect - wit inspect
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .58  12 7.4  false(unreach-call) 1 wit inspect 4.8  260 false(unreach-call) 1 wit inspect 6.6   260   unknown 0 wit inspect 3.5  250 false(unreach-call) 1 wit inspect .82   18    - wit inspect - wit inspect
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .34  11 4.2  true -32 wit inspect 4.9  260 true -32 wit inspect 7.3   290   unknown 0 wit inspect 4.1  210 false(unreach-call) 1 wit inspect .68   18    - wit inspect - wit inspect
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .46  12 5.0  false(unreach-call) 1 wit inspect 4.2  260 false(unreach-call) 1 wit inspect 7.5   260   unknown 0 wit inspect 4.1  250 false(unreach-call) 1 wit inspect .82   18    - wit inspect - wit inspect
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .50  12 6.3  false(unreach-call) 1 wit inspect 4.9  260 true -32 wit inspect 5.6   260   unknown 0 wit inspect 2.5  250 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900     420 8300    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.8
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 890     40 13000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .026 4.8
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i true 2 wit inspect .41  12 4.0  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 20    520 true 2 wit inspect 83     1100  
list-properties/list_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900     110 13000    - 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
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 890     60 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .025 4.9
list-properties/simple_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 890     59 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .020 5.0
list-properties/splice_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 890     85 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 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 .32  11 3.6  true -32 wit inspect 3.8  260 false(unreach-call) 1 wit inspect 5.5   260   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/alt_test_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .36  11 4.4  true -32 wit inspect 4.8  260 false(unreach-call) 1 wit inspect 6.7   270   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .74   18    - wit inspect - wit inspect
ldv-regression/callfpointer_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .30  12 3.6  true -32 wit inspect 3.7  250 false(unreach-call) 1 wit inspect 4.6   220   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .71   18    - wit inspect - wit inspect
ldv-regression/fo_test_true-termination.c_false-unreach-call.i true -32 wit inspect .38  12 4.6  false(unreach-call) 1 wit inspect 5.9  270 unknown 0 wit inspect 12     290   unknown 0 wit inspect 1.2  51 error (1) 0 wit inspect .091  9.0  - wit inspect - wit inspect
ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .33  11 3.6  true -32 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 4.9   250   unknown 0 wit inspect 3.0  180 false(unreach-call) 1 wit inspect .64   18    - wit inspect - wit inspect
ldv-regression/mutex_lock_struct_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .31  11 4.6  true -32 wit inspect 2.4  260 false(unreach-call) 1 wit inspect 5.4   250   unknown 0 wit inspect 2.9  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/recursive_list_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .31  11 3.9  true -32 wit inspect 4.2  260 false(unreach-call) 1 wit inspect 5.6   270   unknown 0 wit inspect 3.3  180 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
ldv-regression/rule57_ebda_blast_true-termination.c_false-unreach-call.i unknown 0 wit inspect .073 11 .41 error (invalid witness file) 0 wit inspect .76 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
ldv-regression/rule60_list2_true-termination.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect 1.1   12 14    false(unreach-call) 1 wit inspect 4.6  260 true -32 wit inspect 3.4   240   unknown 0 wit inspect 4.1  210 false(unreach-call) 1 wit inspect .64   18    - wit inspect - wit inspect
ldv-regression/stateful_check_false-unreach-call_false-termination.i unknown 0 wit inspect 34     74 400    error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0015 .27 - wit inspect - wit inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .30  11 4.4  true -32 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 7.3   260   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .76   18    - wit inspect - wit inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect .30  11 3.7  false(unreach-call) 1 wit inspect 4.2  260 false(unreach-call) 1 wit inspect 5.8   260   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .69   18    - wit inspect - wit inspect
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call.i true 2 wit inspect .36  11 4.7  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 6.7   270  
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i true 2 wit inspect .30  11 3.6  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 6.4   260  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call.i true 2 wit inspect .30  11 3.5  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  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 .31  11 2.7  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.8  240 true 2 wit inspect 5.5   260  
ldv-regression/ex3_forlist_true-termination.c_true-unreach-call.i true 2 wit inspect .36  11 4.3  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 17    470 true 2 wit inspect 38     700  
ldv-regression/just_assert_true-termination.c_true-unreach-call.i true 2 wit inspect .31  11 3.6  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 5.2   220  
ldv-regression/mutex_lock_int_true-termination.c_true-unreach-call_1.i true 2 wit inspect .32  11 4.8  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  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 .31  11 3.8  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 9.1   270  
ldv-regression/nested_structure_noptr_true-termination.c_true-unreach-call.i true 2 wit inspect .29  11 3.8  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 6.0   240  
ldv-regression/nested_structure_noptr_true-unreach-call_true-termination.i true 2 wit inspect .31  11 3.9  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 7.0   250  
ldv-regression/nested_structure_ptr_true-termination.c_true-unreach-call.i true 2 wit inspect .31  11 3.6  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 10     450  
ldv-regression/nested_structure_ptr_true-unreach-call_true-termination.i true 2 wit inspect .31  12 3.6  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  260 true 2 wit inspect 13     420  
ldv-regression/nested_structure_true-termination.c_true-unreach-call.i true 2 wit inspect .32  11 4.3  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 9.1   280  
ldv-regression/nested_structure_true-unreach-call_true-termination.i true 2 wit inspect .30  11 3.3  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 9.5   290  
ldv-regression/oomInt_true-termination.c_true-unreach-call.i true 2 wit inspect .32  11 3.4  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 5.4   270  
ldv-regression/oomInt_true-termination.c_true-unreach-call_1.i true 2 wit inspect .30  11 4.4  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 5.0   260  
ldv-regression/rule57_ebda_blast_true-termination.c_true-unreach-call_1.i unknown 0 wit inspect .081 11 .36 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 45 error (2) 0 wit inspect .024 4.8
ldv-regression/rule60_list2_true-termination.c_true-unreach-call.i true 2 wit inspect 1.4   12 16    - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  260 true 2 wit inspect 26     520  
ldv-regression/rule60_list_true-termination.c_true-unreach-call.i true 2 wit inspect .35  12 4.0  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  260 true 2 wit inspect 11     380  
ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i false(unreach-call) -16 wit inspect .34  11 3.6  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  260 true 2 wit inspect 5.6   260  
ldv-regression/structure_assignment_true-termination.c_true-unreach-call.i true 2 wit inspect .30  11 3.5  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 5.8   250  
ldv-regression/test_address_true-termination.c_true-unreach-call.i true 2 wit inspect .32  11 3.7  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 6.7   260  
ldv-regression/test_cut_trace_true-termination.c_true-unreach-call.i true 2 wit inspect .29  11 3.6  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 5.3   260  
ldv-regression/test_malloc-1_true-unreach-call_true-termination.i unknown 0 wit inspect .050 11 .37 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .027 4.8
ldv-regression/test_malloc-2_true-unreach-call_true-termination.i unknown 0 wit inspect .040 11 .31 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 44 error (2) 0 wit inspect .025 4.8
ldv-regression/test_overflow_true-termination.c_true-unreach-call.i true 2 wit inspect .35  12 3.6  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  260 true 2 wit inspect 6.3   260  
ldv-regression/test_union_cast-1_true-unreach-call_true-termination.i true 2 wit inspect .30  11 4.1  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 5.3   260  
ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i true 2 wit inspect .32  11 3.6  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 7.1   260  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call.i true 2 wit inspect .33  12 3.8  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 5.8   260  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call_1.i true 2 wit inspect .29  11 4.2  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.3   260  
ldv-regression/test_union_true-termination.c_true-unreach-call.i true 2 wit inspect .29  11 3.6  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 5.2   260  
ldv-regression/test_union_true-termination.c_true-unreach-call_1.i true 2 wit inspect .32  11 3.5  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 6.7   270  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call.i true 2 wit inspect .32  11 3.3  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 6.8   270  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i true 2 wit inspect .33  11 4.0  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 5.8   290  
ldv-regression/test02_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .32  11 3.5  true -32 wit inspect 2.2  260 false(unreach-call) 1 wit inspect 5.1   230   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
ldv-regression/test06_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .36  11 3.5  true -32 wit inspect 2.4  260 false(unreach-call) 1 wit inspect 6.0   270   unknown 0 wit inspect 3.5  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 .33  11 3.7  true -32 wit inspect 4.0  250 false(unreach-call) 1 wit inspect 5.1   260   unknown 0 wit inspect 3.0  180 false(unreach-call) 1 wit inspect .64   18    - wit inspect - wit inspect
ldv-regression/test12_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .29  11 3.3  true -32 wit inspect 4.4  260 false(unreach-call) 1 wit inspect 3.5   240   unknown 0 wit inspect 2.9  180 false(unreach-call) 1 wit inspect .62   18    - wit inspect - wit inspect
ldv-regression/test21_false-unreach-call_true-termination.c unknown 0 wit inspect .28  11 3.5  error (invalid witness file) 0 wit inspect .70 41 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0019 .29 - wit inspect - wit inspect
ldv-regression/test22_false-unreach-call.c unknown 0 wit inspect .30  11 3.1  error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
ldv-regression/test23_false-unreach-call.c unknown 0 wit inspect .31  11 4.0  error (invalid witness file) 0 wit inspect .73 42 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0018 .29 - wit inspect - wit inspect
ldv-regression/test24_false-unreach-call.c false(unreach-call) 1 wit inspect .80  19 12    false(unreach-call) 1 wit inspect 4.1  280 true -32 wit inspect 5.4   250   unknown 0 wit inspect 3.6  210 false(unreach-call) 1 wit inspect .69   18    - wit inspect - wit inspect
ldv-regression/test25_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .73  17 8.4  false(unreach-call) 1 wit inspect 18    310 true -32 wit inspect 4.9   240   unknown 0 wit inspect 3.7  210 false(unreach-call) 1 wit inspect .62   19    - wit inspect - wit inspect
ldv-regression/test26_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .30  11 3.6  true -32 wit inspect 3.9  250 false(unreach-call) 1 wit inspect 5.2   260   unknown 0 wit inspect 3.6  210 false(unreach-call) 1 wit inspect .66   18    - wit inspect - wit inspect
ldv-regression/test27_false-unreach-call_true-termination.c unknown 0 wit inspect .074 11 .46 error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .89 47 error (invalid witness file) 0 wit inspect .0015 .28 - wit inspect - wit inspect
ldv-regression/test28_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .33  11 3.9  false(unreach-call) 1 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 7.4   260   unknown 0 wit inspect 3.0  220 false(unreach-call) 1 wit inspect .68   18    - wit inspect - wit inspect
ldv-regression/test29_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .34  12 5.2  false(unreach-call) 1 wit inspect 4.2  260 false(unreach-call) 1 wit inspect 4.8   280   unknown 0 wit inspect 3.7  210 false(unreach-call) 1 wit inspect .66   18    - wit inspect - wit inspect
ldv-regression/test30_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .34  11 3.5  true -32 wit inspect 3.9  260 false(unreach-call) 1 wit inspect 5.7   270   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .67   18    - wit inspect - wit inspect
ldv-regression/test01_true-unreach-call_true-termination.c unknown 0 wit inspect .27  11 3.1  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 42 error (2) 0 wit inspect .021 4.9
ldv-regression/test03_true-unreach-call_true-termination.c unknown 0 wit inspect .30  11 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.8
ldv-regression/test04_true-unreach-call_true-termination.c unknown 0 wit inspect .27  11 3.0  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .021 4.8
ldv-regression/test05_true-unreach-call_true-termination.c unknown 0 wit inspect .31  11 2.9  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .025 4.9
ldv-regression/test07_true-unreach-call_true-termination.c unknown 0 wit inspect .30  11 3.4  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .021 4.8
ldv-regression/test09_true-unreach-call_true-termination.c unknown 0 wit inspect .31  11 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
ldv-regression/test10_true-unreach-call_true-termination.c unknown 0 wit inspect .32  11 3.1  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .026 4.8
ldv-regression/test11_true-unreach-call_true-termination.c unknown 0 wit inspect .27  11 3.3  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 44 error (2) 0 wit inspect .025 5.0
ldv-regression/test13_true-unreach-call_true-termination.c true 2 wit inspect .29  11 3.4  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 6.4   260  
ldv-regression/test14_true-unreach-call_true-termination.c unknown 0 wit inspect .26  11 2.8  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .019 5.0
ldv-regression/test15_true-unreach-call_true-termination.c unknown 0 wit inspect .29  11 3.0  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .025 4.8
ldv-regression/test16_true-unreach-call_true-termination.c true 2 wit inspect .30  11 3.5  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 10     290  
ldv-regression/test17_true-unreach-call_true-termination.c true 2 wit inspect .29  11 3.5  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 6.3   260  
ldv-regression/test18_true-unreach-call_true-termination.c unknown 0 wit inspect .29  11 3.4  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 44 error (2) 0 wit inspect .019 4.9
ldv-regression/test19_true-unreach-call_true-termination.c unknown 0 wit inspect .27  11 2.9  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 42 error (2) 0 wit inspect .019 4.9
ldv-regression/test20_true-unreach-call_true-termination.c true 2 wit inspect .32  11 3.0  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 5.7   270  
ldv-regression/test21_true-unreach-call_true-termination.c unknown 0 wit inspect .26  11 3.5  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .026 4.9
ldv-regression/test22_true-unreach-call.c unknown 0 wit inspect .31  11 3.2  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .027 4.9
ldv-regression/test23_true-unreach-call.c unknown 0 wit inspect .30  11 3.0  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 45 error (2) 0 wit inspect .027 4.8
ldv-regression/test24_true-unreach-call_true-termination.c unknown 0 wit inspect .32  11 3.5  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 41 error (2) 0 wit inspect .018 4.8
ldv-regression/test25_true-unreach-call.c unknown 0 wit inspect .36  15 4.7  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .021 4.9
ldv-regression/test26_true-unreach-call_true-termination.c unknown 0 wit inspect .28  11 3.7  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .025 4.8
ldv-regression/test27_true-unreach-call_true-termination.c unknown 0 wit inspect .065 11 .40 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 42 error (2) 0 wit inspect .018 4.9
ldv-regression/test28_true-unreach-call_true-termination.c unknown 0 wit inspect .33  12 3.3  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .025 4.8
ldv-regression/test29_true-unreach-call_true-termination.c unknown 0 wit inspect .32  11 3.2  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .024 4.9
ldv-regression/test30_true-unreach-call_true-termination.c unknown 0 wit inspect .36  44 3.2  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .019 4.9
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 25     15000 330    error (invalid witness file) 0 wit inspect .73 44 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 25     15000 330    error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 25     15000 360    error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0014 .27 - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900     3600 5900    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .029 4.8
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900     3700 5700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .018 4.8
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900     3500 6000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .019 4.9
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900     3500 5700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .019 4.8
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900     3700 7300    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .021 4.8
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900     3600 5600    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .021 4.8
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900     3700 4900    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 43 error (2) 0 wit inspect .019 4.8
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900     3500 5700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .019 4.9
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900     3600 5700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .022 4.9
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900     3600 7100    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .026 4.8
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i out of memory 0 wit inspect 82     15000 1000    error (invalid witness file) 0 wit inspect .73 43 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0015 .29 - wit inspect - wit inspect
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .36  12 5.1  false(unreach-call) 1 wit inspect 2.9  280 true -32 wit inspect 7.4   280   unknown 0 wit inspect 3.3  250 false(unreach-call) 1 wit inspect .73   18    - wit inspect - wit inspect
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .39  12 4.5  false(unreach-call) 1 wit inspect 5.8  250 false(unreach-call) 1 wit inspect 6.3   270   unknown 0 wit inspect 3.9  250 false(unreach-call) 1 wit inspect .71   18    - wit inspect - wit inspect
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect .26  12 2.6  error (invalid witness file) 0 wit inspect .72 43 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .89 48 error (invalid witness file) 0 wit inspect .0015 .27 - wit inspect - wit inspect
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .40  12 4.9  false(unreach-call) 1 wit inspect 4.9  260 true -32 wit inspect 5.9   270   unknown 0 wit inspect 4.0  250 false(unreach-call) 1 wit inspect .83   18    - wit inspect - wit inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(unreach-call) 1 wit inspect .61  12 5.4  unknown 0 wit inspect 4.7  260 true -32 wit inspect 5.8   250   unknown 0 wit inspect 4.5  250 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .44  12 4.9  false(unreach-call) 1 wit inspect 2.7  260 true -32 wit inspect 6.0   240   unknown 0 wit inspect 3.5  250 false(unreach-call) 1 wit inspect .85   18    - wit inspect - wit inspect
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .50  12 6.1  false(unreach-call) 1 wit inspect 3.0  260 true -32 wit inspect 6.8   290   unknown 0 wit inspect 4.2  250 false(unreach-call) 1 wit inspect .71   18    - wit inspect - wit inspect
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .40  12 4.5  false(unreach-call) 1 wit inspect 4.4  270 true -32 wit inspect 5.3   240   unknown 0 wit inspect 3.7  250 false(unreach-call) 1 wit inspect .64   18    - wit inspect - wit inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i unknown 0 wit inspect 900     3800 5000    error (invalid witness file) 0 wit inspect .69 44 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .67 50 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .52  12 5.5  unknown 0 wit inspect 2.9  260 true -32 wit inspect 6.2   250   unknown 0 wit inspect 3.4  250 false(unreach-call) 1 wit inspect .73   18    - wit inspect - wit inspect
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .38  12 4.2  false(unreach-call) 1 wit inspect 5.2  280 true -32 wit inspect 7.6   270   unknown 0 wit inspect 3.6  260 false(unreach-call) 1 wit inspect .72   18    - wit inspect - wit inspect
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .42  12 4.9  false(unreach-call) 1 wit inspect 4.9  260 false(unreach-call) 1 wit inspect 6.1   280   unknown 0 wit inspect 4.4  230 false(unreach-call) 1 wit inspect .73   18    - wit inspect - wit inspect
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect .26  11 2.5  error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .40  12 4.4  false(unreach-call) 1 wit inspect 4.9  270 true -32 wit inspect 7.3   270   unknown 0 wit inspect 4.0  250 false(unreach-call) 1 wit inspect .64   18    - wit inspect - wit inspect
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .50  12 6.6  unknown 0 wit inspect 5.1  260 true -32 wit inspect 5.4   240   unknown 0 wit inspect 4.2  220 false(unreach-call) 1 wit inspect .78   18    - wit inspect - wit inspect
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .44  12 5.1  false(unreach-call) 1 wit inspect 4.5  260 true -32 wit inspect 3.7   240   unknown 0 wit inspect 2.4  250 false(unreach-call) 1 wit inspect .86   19    - wit inspect - wit inspect
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .52  12 6.7  unknown 0 wit inspect 4.6  260 true -32 wit inspect 6.2   280   unknown 0 wit inspect 4.1  250 false(unreach-call) 1 wit inspect .75   18    - wit inspect - wit inspect
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .38  12 4.8  false(unreach-call) 1 wit inspect 4.5  260 true -32 wit inspect 6.5   270   unknown 0 wit inspect 3.4  250 false(unreach-call) 1 wit inspect .72   18    - wit inspect - wit inspect
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900     3400 9100    - 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
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900     370 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .025 4.9
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900     2300 13000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 42 error (2) 0 wit inspect .024 4.9
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .22  12 2.8  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .018 5.0
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900     1400 9200    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 45 error (2) 0 wit inspect .023 4.8
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900     1400 9700    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 44 error (2) 0 wit inspect .025 4.9
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900     420 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .024 4.9
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900     160 10000    - 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/dll-sorted_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900     2000 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 45 error (2) 0 wit inspect .023 4.8
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890     80 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .024 4.8
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900     3700 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .018 4.8
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900     810 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 45 error (2) 0 wit inspect .026 4.8
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900     410 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 5.0
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900     2300 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .023 5.0
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .23  11 2.9  - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .023 4.8
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900     2200 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .024 4.9
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900     2400 13000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .018 4.8
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900     400 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 45 error (2) 0 wit inspect .027 4.8
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 890     160 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .024 4.8
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900     1700 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 45 error (2) 0 wit inspect .021 4.9
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890     81 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .024 4.8
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .41  12 5.3  false(unreach-call) 1 wit inspect 4.8  270 true -32 wit inspect 4.0   270   unknown 0 wit inspect 4.7  250 false(unreach-call) 1 wit inspect .74   18    - wit inspect - wit inspect
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 39     380 410    timeout 0 wit inspect 92    1900 true -32 wit inspect 6.2   300   unknown 0 wit inspect 4.5  250 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup_true-termination.i false(unreach-call) 1 wit inspect .38  12 4.8  false(unreach-call) 1 wit inspect 2.7  250 false(unreach-call) 1 wit inspect 5.6   270   unknown 0 wit inspect 4.4  240 false(unreach-call) 1 wit inspect .64   18    - wit inspect - wit inspect
list-ext2-properties/list_and_tree_cnstr_false-unreach-call_false-termination.i true -32 wit inspect 1.2   14 15    unknown 0 wit inspect 23    1100 false(unreach-call) 1 wit inspect 46     800   unknown 0 wit inspect 1.1  52 error (1) 0 wit inspect .079  9.1  - wit inspect - wit inspect
list-ext2-properties/list_and_tree_cnstr_true-unreach-call_false-termination.i unknown 0 wit inspect 900     590 12000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .023 4.8
list-ext2-properties/simple_and_skiplist_2lvl_false-unreach-call.i false(unreach-call) 1 wit inspect .41  12 4.9  false(unreach-call) 1 wit inspect 5.0  260 false(unreach-call) 1 wit inspect 5.3   290   unknown 0 wit inspect 3.5  250 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
list-ext2-properties/simple_and_skiplist_2lvl_true-unreach-call.i unknown 0 wit inspect 900     1200 11000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 41 error (2) 0 wit inspect .024 4.9
list-ext2-properties/simple_search_value_false-unreach-call.i false(unreach-call) 1 wit inspect .51  85 6.8  unknown 0 wit inspect 4.9  280 true -32 wit inspect 4.7   270   unknown 0 wit inspect 3.8  250 false(unreach-call) 1 wit inspect .77   19    - wit inspect - wit inspect
list-ext2-properties/simple_search_value_true-unreach-call.i unknown 0 wit inspect 890     82 10000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .019 5.0
ldv-sets/test_add_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .40  12 5.2  false(unreach-call) 1 wit inspect 4.6  260 true -32 wit inspect 3.5   230   unknown 0 wit inspect 4.7  250 error (1) 0 wit inspect .73   18    - wit inspect - wit inspect
ldv-sets/test_mutex_double_lock_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .40  12 5.4  true -32 wit inspect 5.5  280 false(unreach-call) 1 wit inspect 7.2   300   unknown 0 wit inspect 3.5  210 error (1) 0 wit inspect .79   18    - wit inspect - wit inspect
ldv-sets/test_mutex_double_unlock_false-unreach-call.i false(unreach-call) 0 wit inspect .47  12 6.0  true -32 wit inspect 5.5  260 true -32 wit inspect 6.4   260   unknown 0 wit inspect 4.4  210 error (1) 0 wit inspect .60   19    - wit inspect - wit inspect
ldv-sets/test_mutex_unbounded_false-unreach-call.i false(unreach-call) 0 wit inspect .56  12 7.3  unknown 0 wit inspect 5.6  270 true -32 wit inspect 4.1   260   unknown 0 wit inspect 3.9  250 error (1) 0 wit inspect .67   18    - wit inspect - wit inspect
ldv-sets/test_mutex_unlock_at_exit_false-unreach-call.i out of memory 0 wit inspect 93     15000 1100    error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .91 47 error (invalid witness file) 0 wit inspect .0016 .28 - wit inspect - wit inspect
ldv-sets/test_add_true-unreach-call_true-termination.i true 2 wit inspect .43  12 4.8  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.6  290 error (7) 0 wit inspect 370     840  
ldv-sets/test_mutex_true-unreach-call.i true 2 wit inspect .48  12 5.9  - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 270    3600 timeout 0 wit inspect 960     1300  
ldv-sets/test_mutex_unbounded_true-unreach-call.i unknown 0 wit inspect 890     130 13000    - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .023 5.0
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 46 41000    150000 440000   71 -517 380 18000 71 -967 380 16000 71 0 220 13000 71 18 39    1000 110 76 470 17000 110 72 1700 14000
    correct results 89 126 75    1500 830   27 27 130 7100 25 25 190 7100 0 50 50 35    920 38 76 430 13000 36 72 380 11000
        correct true 37 74 13    420 150   0 0 0 0 38 76 430 13000 36 72 380 11000
        correct false 52 52 62    1100 680   27 27 130 7100 25 25 190 7100 0 50 50 35    920 0 0
    correct-unconfimed results 3 0 1.6  36 20   0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 3 0 1.6  36 20   0 0 0 0 0 0
    incorrect results 3 -80 1.9  37 24   17 -544 65 4400 31 -992 180 8100 0 1 -32 .75 19 0 0
        incorrect true 2 -64 1.6  26 20   17 -544 65 4400 31 -992 180 8100 0 1 -32 .75 19 0 0
        incorrect false 1 -16 .34 11 3.6 0 0 0 0 0 0
score (181 tasks, max score: 291) 46 -517 -967 0 18 76 72
Run set map2check.sv-comp18.ReachSafety-Heap cpa-seq-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Heap uautomizer-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-map2check.sv-comp18-violation-witness.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-map2check.sv-comp18-correctness-witness.ReachSafety-Heap uautomizer-validate-correctness-witnesses-map2check.sv-comp18-correctness-witness.ReachSafety-Heap