Tool CBMC 5.8 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:26:01 CET 2017-12-01 07:56:00 CET 2017-12-01 08:08:00 CET 2017-12-01 08:15:34 CET 2017-12-01 04:22:29 CET 2017-12-01 07:31:28 CET
Run set cbmc.sv-comp18.ReachSafety-Heap cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-Heap uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.ReachSafety-Heap uautomizer-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.ReachSafety-Heap
Options --graphml-witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.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/cbmc.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.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/cbmc.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cbmc.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cbmc.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
heap-manipulation/bubble_sort_linux_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .73 45 7.0 false(unreach-call) 1 wit inspect 4.4 270 false(unreach-call) 1 wit inspect 10   340 unknown 0 wit inspect 4.5 250 false(unreach-call) 1 wit inspect .68 19 - wit inspect - wit inspect
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .73 42 7.5 true -32 wit inspect 4.9 250 true -32 wit inspect 6.4 290 unknown 0 wit inspect 5.6 270 true -32 wit inspect .74 19 - wit inspect - wit inspect
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .92 54 11   false(unreach-call) 1 wit inspect 4.4 260 false(unreach-call) 1 wit inspect 7.5 320 unknown 0 wit inspect 3.7 250 false(unreach-call) 1 wit inspect .69 19 - wit inspect - wit inspect
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .66 42 7.2 false(unreach-call) 1 wit inspect 4.5 270 false(unreach-call) 1 wit inspect 9.1 310 unknown 0 wit inspect 4.1 250 false(unreach-call) 1 wit inspect .65 19 - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .64 41 7.1 false(unreach-call) 1 wit inspect 4.0 260 false(unreach-call) 1 wit inspect 8.6 290 unknown 0 wit inspect 3.6 250 true -32 wit inspect .70 19 - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .67 42 6.4 false(unreach-call) 1 wit inspect 4.2 260 false(unreach-call) 1 wit inspect 7.6 300 unknown 0 wit inspect 3.7 250 false(unreach-call) 1 wit inspect .68 19 - wit inspect - wit inspect
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 870    4600 5500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 44 error (2) 0 wit inspect .019 4.8
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i error (42) 0 wit inspect 870    980 12000   - 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
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 870    1900 8200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .039 5.0
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i error (134) 0 wit inspect 370    13000 4500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .018 4.9
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 870    7400 5400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .024 4.8
heap-manipulation/tree_true-unreach-call.i error (42) 0 wit inspect 870    5100 7800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.8
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .46 37 4.5 true -32 wit inspect 3.7 250 false(unreach-call) 1 wit inspect 6.2 260 unknown 0 wit inspect 3.9 250 false(unreach-call) 1 wit inspect .76 18 - wit inspect - wit inspect
list-properties/list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .49 36 4.9 false(unreach-call) 1 wit inspect 4.0 260 false(unreach-call) 1 wit inspect 6.4 270 unknown 0 wit inspect 4.1 250 false(unreach-call) 1 wit inspect .83 18 - wit inspect - wit inspect
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .49 36 4.3 false(unreach-call) 1 wit inspect 3.6 260 false(unreach-call) 1 wit inspect 5.4 270 unknown 0 wit inspect 3.3 250 false(unreach-call) 1 wit inspect .83 18 - wit inspect - wit inspect
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 1.3  36 12   unknown 0 wit inspect 4.0 280 false(unreach-call) 1 wit inspect 27   690 unknown 0 wit inspect 3.4 220 false(unreach-call) 1 wit inspect .64 18 - wit inspect - wit inspect
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .47 36 4.6 false(unreach-call) 1 wit inspect 3.8 250 false(unreach-call) 1 wit inspect 5.7 260 unknown 0 wit inspect 3.4 250 false(unreach-call) 1 wit inspect .67 18 - wit inspect - wit inspect
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .44 37 4.7 true -32 wit inspect 2.7 250 false(unreach-call) 1 wit inspect 6.9 270 unknown 0 wit inspect 4.2 250 error (1) 0 wit inspect .70 19 - wit inspect - wit inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 870    3600 7100   - 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
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i error (42) 0 wit inspect 870    3500 4100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .020 4.9
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i true 2 wit inspect 1.7  37 18   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 6.2  280 true 2 wit inspect 67     950  
list-properties/list_true-unreach-call_false-valid-memtrack.i error (42) 0 wit inspect 870    6500 6700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .017 5.0
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i error (42) 0 wit inspect 870    4900 8500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .019 4.9
list-properties/simple_true-unreach-call_false-valid-memtrack.i error (42) 0 wit inspect 880    13000 6700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 44 error (2) 0 wit inspect .018 4.9
list-properties/splice_true-unreach-call_false-valid-memtrack.i error (134) 0 wit inspect 830    13000 7700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .022 4.9
ldv-regression/1_3_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .40 36 4.0 false(unreach-call) 1 wit inspect 3.2 260 false(unreach-call) 1 wit inspect 8.8 320 unknown 0 wit inspect 2.8 210 false(unreach-call) 1 wit inspect .79 18 - wit inspect - wit inspect
ldv-regression/alt_test_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .49 37 4.2 false(unreach-call) 1 wit inspect 4.3 280 false(unreach-call) 1 wit inspect 6.9 260 unknown 0 wit inspect 3.5 220 false(unreach-call) 1 wit inspect .68 18 - wit inspect - wit inspect
ldv-regression/callfpointer_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .25 33 2.1 false(unreach-call) 1 wit inspect 3.0 260 false(unreach-call) 1 wit inspect 4.7 230 unknown 0 wit inspect 2.9 180 false(unreach-call) 1 wit inspect .73 18 - wit inspect - wit inspect
ldv-regression/fo_test_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .51 36 4.3 false(unreach-call) 1 wit inspect 3.7 260 unknown 0 wit inspect 11   290 unknown 0 wit inspect 3.5 220 false(unreach-call) 1 wit inspect .67 18 - wit inspect - wit inspect
ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .21 33 1.9 true -32 wit inspect 3.3 270 false(unreach-call) 1 wit inspect 5.5 250 unknown 0 wit inspect 2.9 180 false(unreach-call) 1 wit inspect .62 18 - wit inspect - wit inspect
ldv-regression/mutex_lock_struct_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .23 33 2.3 true -32 wit inspect 2.8 250 false(unreach-call) 1 wit inspect 4.9 250 unknown 0 wit inspect 3.8 210 false(unreach-call) 1 wit inspect .62 18 - wit inspect - wit inspect
ldv-regression/recursive_list_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .44 34 3.8 false(unreach-call) 1 wit inspect 4.1 260 false(unreach-call) 1 wit inspect 5.5 260 unknown 0 wit inspect 3.0 180 error (2) 0 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 .25 33 2.6 false(unreach-call) 1 wit inspect 3.6 270 false(unreach-call) 1 wit inspect 5.6 260 unknown 0 wit inspect 4.0 210 error (2) 0 wit inspect .71 18 - wit inspect - wit inspect
ldv-regression/rule60_list2_true-termination.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect .27 35 3.2 true -32 wit inspect 5.1 270 false(unreach-call) 1 wit inspect 7.9 320 unknown 0 wit inspect 4.1 280 error (2) 0 wit inspect .65 19 - wit inspect - wit inspect
ldv-regression/stateful_check_false-unreach-call_false-termination.i false(unreach-call) 0 wit inspect .67 33 7.1 true -32 wit inspect 3.6 260 out of memory 0 wit inspect 84   7000 unknown 0 wit inspect 3.6 220 true -32 wit inspect .61 19 - wit inspect - wit inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .57 33 6.5 true -32 wit inspect 3.3 250 false(unreach-call) 1 wit inspect 4.9 240 unknown 0 wit inspect 3.0 180 false(unreach-call) 1 wit inspect .59 18 - wit inspect - wit inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect .62 33 5.6 false(unreach-call) 1 wit inspect 3.0 260 false(unreach-call) 1 wit inspect 5.9 260 unknown 0 wit inspect 2.8 180 false(unreach-call) 1 wit inspect .59 18 - wit inspect - wit inspect
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call.i true 2 wit inspect .39 33 3.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 6.1   270  
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i true 2 wit inspect .40 33 4.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.2   260  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call.i true 2 wit inspect .40 33 4.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  270 true 2 wit inspect 6.4   260  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call_1.i true 2 wit inspect .39 33 4.0 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 5.0   260  
ldv-regression/ex3_forlist_true-termination.c_true-unreach-call.i true 2 wit inspect .79 33 6.7 - wit inspect - wit inspect - wit inspect - wit inspect assertion 0 wit inspect 4.4  250 true 2 wit inspect 29     710  
ldv-regression/just_assert_true-termination.c_true-unreach-call.i true 2 wit inspect .38 33 4.1 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 4.7   220  
ldv-regression/mutex_lock_int_true-termination.c_true-unreach-call_1.i true 2 wit inspect .40 33 3.3 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  260 true 2 wit inspect 6.1   270  
ldv-regression/mutex_lock_struct_true-termination.c_true-unreach-call_1.i true 2 wit inspect .41 33 3.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 6.4   270  
ldv-regression/nested_structure_noptr_true-termination.c_true-unreach-call.i true 2 wit inspect .42 33 4.0 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 5.2   250  
ldv-regression/nested_structure_noptr_true-unreach-call_true-termination.i true 2 wit inspect .37 33 4.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  240 true 2 wit inspect 5.9   260  
ldv-regression/nested_structure_ptr_true-termination.c_true-unreach-call.i true 2 wit inspect .40 35 4.1 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 8.8   480  
ldv-regression/nested_structure_ptr_true-unreach-call_true-termination.i true 2 wit inspect .42 33 3.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 10     410  
ldv-regression/nested_structure_true-termination.c_true-unreach-call.i true 2 wit inspect .42 33 3.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  270 true 2 wit inspect 7.6   270  
ldv-regression/nested_structure_true-unreach-call_true-termination.i true 2 wit inspect .41 33 3.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 9.2   280  
ldv-regression/oomInt_true-termination.c_true-unreach-call.i true 2 wit inspect .42 33 3.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 6.7   270  
ldv-regression/oomInt_true-termination.c_true-unreach-call_1.i true 2 wit inspect .40 33 3.2 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 6.3   260  
ldv-regression/rule57_ebda_blast_true-termination.c_true-unreach-call_1.i true 2 wit inspect .43 33 4.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 6.3   260  
ldv-regression/rule60_list2_true-termination.c_true-unreach-call.i true 2 wit inspect .47 35 4.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  260 true 2 wit inspect 23     650  
ldv-regression/rule60_list_true-termination.c_true-unreach-call.i true 2 wit inspect .85 36 7.3 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  260 true 2 wit inspect 9.4   380  
ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i true 2 wit inspect .47 34 3.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  250 true 2 wit inspect 4.8   260  
ldv-regression/structure_assignment_true-termination.c_true-unreach-call.i true 2 wit inspect .42 33 3.9 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 5.2   260  
ldv-regression/test_address_true-termination.c_true-unreach-call.i true 2 wit inspect .47 34 4.1 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  260 true 2 wit inspect 5.9   260  
ldv-regression/test_cut_trace_true-termination.c_true-unreach-call.i true 2 wit inspect .42 33 3.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 3.7   260  
ldv-regression/test_malloc-1_true-unreach-call_true-termination.i true 2 wit inspect .83 36 6.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 5.8   260  
ldv-regression/test_malloc-2_true-unreach-call_true-termination.i true 2 wit inspect .46 35 4.3 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  260 true 2 wit inspect 5.7   260  
ldv-regression/test_overflow_true-termination.c_true-unreach-call.i true 2 wit inspect .50 36 5.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 5.2   260  
ldv-regression/test_union_cast-1_true-unreach-call_true-termination.i true 2 wit inspect .40 33 3.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 5.1   260  
ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i true 2 wit inspect .40 33 3.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  250 true 2 wit inspect 5.9   260  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call.i true 2 wit inspect .41 33 3.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.1   260  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call_1.i true 2 wit inspect .42 33 3.2 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  260 true 2 wit inspect 5.4   270  
ldv-regression/test_union_true-termination.c_true-unreach-call.i true 2 wit inspect .39 33 3.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 5.0   250  
ldv-regression/test_union_true-termination.c_true-unreach-call_1.i true 2 wit inspect .40 33 5.2 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 5.4   270  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call.i true 2 wit inspect .41 33 4.1 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 6.0   260  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i true 2 wit inspect .41 33 3.9 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 6.0   260  
ldv-regression/test02_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .24 33 2.1 false(unreach-call) 1 wit inspect 2.9 260 false(unreach-call) 1 wit inspect 5.3 220 unknown 0 wit inspect 2.9 210 false(unreach-call) 1 wit inspect .58 18 - wit inspect - wit inspect
ldv-regression/test06_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .25 33 1.9 true -32 wit inspect 3.1 260 false(unreach-call) 1 wit inspect 7.7 270 unknown 0 wit inspect 3.3 180 error (2) 0 wit inspect .62 18 - wit inspect - wit inspect
ldv-regression/test08_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .24 33 2.2 false(unreach-call) 1 wit inspect 3.1 260 false(unreach-call) 1 wit inspect 7.1 260 unknown 0 wit inspect 2.8 180 false(unreach-call) 1 wit inspect .67 18 - wit inspect - wit inspect
ldv-regression/test12_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .24 33 2.0 true -32 wit inspect 3.1 260 false(unreach-call) 1 wit inspect 5.1 230 unknown 0 wit inspect 3.5 180 false(unreach-call) 1 wit inspect .67 18 - wit inspect - wit inspect
ldv-regression/test21_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .28 33 2.0 false(unreach-call) 1 wit inspect 2.5 270 false(unreach-call) 1 wit inspect 5.7 260 unknown 0 wit inspect 3.7 210 true -32 wit inspect .60 18 - wit inspect - wit inspect
ldv-regression/test22_false-unreach-call.c false(unreach-call) 1 wit inspect .26 33 2.2 false(unreach-call) 1 wit inspect 4.3 260 false(unreach-call) 1 wit inspect 9.7 440 unknown 0 wit inspect 3.2 220 false(unreach-call) 1 wit inspect .78 18 - wit inspect - wit inspect
ldv-regression/test23_false-unreach-call.c false(unreach-call) 1 wit inspect 1.4  36 15   true -32 wit inspect 4.8 260 out of memory 0 wit inspect 88   7000 unknown 0 wit inspect 3.2 210 false(unreach-call) 1 wit inspect .79 19 - wit inspect - wit inspect
ldv-regression/test24_false-unreach-call.c false(unreach-call) 0 wit inspect 2.0  38 21   true -32 wit inspect 3.9 260 out of memory 0 wit inspect 66   7000 unknown 0 wit inspect 4.9 220 error (2) 0 wit inspect .83 19 - wit inspect - wit inspect
ldv-regression/test25_false-unreach-call_true-termination.c false(unreach-call) 0 wit inspect 1.1  36 12   true -32 wit inspect 4.5 260 out of memory 0 wit inspect 62   7000 unknown 0 wit inspect 3.7 220 error (2) 0 wit inspect .62 19 - wit inspect - wit inspect
ldv-regression/test26_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .26 33 2.0 false(unreach-call) 1 wit inspect 2.9 250 false(unreach-call) 1 wit inspect 5.0 260 unknown 0 wit inspect 2.9 190 false(unreach-call) 1 wit inspect .58 18 - wit inspect - wit inspect
ldv-regression/test27_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 1.2  36 12   false(unreach-call) 1 wit inspect 4.6 280 out of memory 0 wit inspect 73   7000 unknown 0 wit inspect 3.6 210 error (2) 0 wit inspect .62 19 - wit inspect - wit inspect
ldv-regression/test28_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .24 33 2.1 false(unreach-call) 1 wit inspect 3.3 260 false(unreach-call) 1 wit inspect 6.9 250 unknown 0 wit inspect 3.3 210 false(unreach-call) 1 wit inspect .59 18 - wit inspect - wit inspect
ldv-regression/test29_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .26 33 2.1 false(unreach-call) 1 wit inspect 3.4 260 false(unreach-call) 1 wit inspect 6.1 260 unknown 0 wit inspect 3.0 210 false(unreach-call) 1 wit inspect .60 18 - wit inspect - wit inspect
ldv-regression/test30_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .27 33 2.1 true -32 wit inspect 3.3 260 false(unreach-call) 1 wit inspect 5.7 280 unknown 0 wit inspect 3.1 210 false(unreach-call) 1 wit inspect .61 18 - wit inspect - wit inspect
ldv-regression/test01_true-unreach-call_true-termination.c true 2 wit inspect .43 33 2.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 5.2   250  
ldv-regression/test03_true-unreach-call_true-termination.c true 2 wit inspect .41 33 3.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 6.8   280  
ldv-regression/test04_true-unreach-call_true-termination.c true 2 wit inspect .40 33 3.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  240 true 2 wit inspect 6.5   280  
ldv-regression/test05_true-unreach-call_true-termination.c true 2 wit inspect .43 33 3.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 11     490  
ldv-regression/test07_true-unreach-call_true-termination.c true 2 wit inspect .45 33 4.0 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 8.9   350  
ldv-regression/test09_true-unreach-call_true-termination.c true 2 wit inspect .41 33 3.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 8.4   340  
ldv-regression/test10_true-unreach-call_true-termination.c true 2 wit inspect .42 33 3.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  250 true 2 wit inspect 12     480  
ldv-regression/test11_true-unreach-call_true-termination.c true 2 wit inspect .41 33 4.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  260 true 2 wit inspect 7.2   270  
ldv-regression/test13_true-unreach-call_true-termination.c true 2 wit inspect .43 33 3.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 6.3   260  
ldv-regression/test14_true-unreach-call_true-termination.c true 2 wit inspect .41 33 4.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  250 true 2 wit inspect 6.8   270  
ldv-regression/test15_true-unreach-call_true-termination.c true 2 wit inspect .40 33 4.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 8.1   280  
ldv-regression/test16_true-unreach-call_true-termination.c true 2 wit inspect .40 33 4.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 7.4   300  
ldv-regression/test17_true-unreach-call_true-termination.c true 2 wit inspect .42 33 3.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 4.8   260  
ldv-regression/test18_true-unreach-call_true-termination.c true 2 wit inspect .42 33 3.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 7.8   300  
ldv-regression/test19_true-unreach-call_true-termination.c true 2 wit inspect .43 33 4.0 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 9.1   370  
ldv-regression/test20_true-unreach-call_true-termination.c true 2 wit inspect .42 33 3.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 5.6   270  
ldv-regression/test21_true-unreach-call_true-termination.c true 2 wit inspect .41 33 4.2 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 7.7   300  
ldv-regression/test22_true-unreach-call.c true 2 wit inspect 2.0  35 21   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.5  290 true 2 wit inspect 20     630  
ldv-regression/test23_true-unreach-call.c true 2 wit inspect 1.6  36 18   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 4.9  280 true 2 wit inspect 250     770  
ldv-regression/test24_true-unreach-call_true-termination.c true 2 wit inspect 1.4  36 16   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 4.4  270 true 2 wit inspect 9.9   430  
ldv-regression/test25_true-unreach-call.c true 2 wit inspect 2.8  36 40   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 310    990 true 2 wit inspect 26     550  
ldv-regression/test26_true-unreach-call_true-termination.c true 2 wit inspect .40 33 4.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  260 true 2 wit inspect 8.1   300  
ldv-regression/test27_true-unreach-call_true-termination.c true 2 wit inspect 1.4  36 14   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1300 true 2 wit inspect 170     790  
ldv-regression/test28_true-unreach-call_true-termination.c true 2 wit inspect .41 33 5.0 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 6.8   270  
ldv-regression/test29_true-unreach-call_true-termination.c true 2 wit inspect .40 33 4.9 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 7.3   280  
ldv-regression/test30_true-unreach-call_true-termination.c true 2 wit inspect .45 33 3.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 9.3   450  
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 32    640 380   true -32 wit inspect 6.4 280 unknown 0 wit inspect 40   610 unknown 0 wit inspect 6.1 290 false(unreach-call) 1 wit inspect 1.1  19 - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 28    630 250   true -32 wit inspect 6.4 280 unknown 0 wit inspect 38   730 unknown 0 wit inspect 7.1 280 false(unreach-call) 1 wit inspect 1.2  19 - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 31    640 380   true -32 wit inspect 6.5 280 unknown 0 wit inspect 42   610 unknown 0 wit inspect 5.5 270 false(unreach-call) 1 wit inspect 1.2  19 - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i error (42) 0 wit inspect 870    1100 7800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .024 4.9
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i error (42) 0 wit inspect 870    1100 7800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .047 4.9
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i error (42) 0 wit inspect 870    1100 7200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .018 4.8
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i error (42) 0 wit inspect 870    1100 7900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .020 4.9
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i error (42) 0 wit inspect 870    1100 6300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .020 4.9
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i error (42) 0 wit inspect 870    1100 6500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 42 error (2) 0 wit inspect .019 4.9
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i error (42) 0 wit inspect 870    1100 8000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .019 4.9
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i error (42) 0 wit inspect 870    1100 7900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 46 error (2) 0 wit inspect .019 4.9
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i error (42) 0 wit inspect 870    1100 6500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .022 4.8
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i error (42) 0 wit inspect 870    1100 7100   - 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-01_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .49 37 4.6 false(unreach-call) 1 wit inspect 4.7 260 false(unreach-call) 1 wit inspect 21   620 unknown 0 wit inspect 3.9 250 true -32 wit inspect .67 19 - wit inspect - wit inspect
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .53 36 4.6 false(unreach-call) 1 wit inspect 4.5 260 false(unreach-call) 1 wit inspect 12   370 unknown 0 wit inspect 3.6 250 false(unreach-call) 1 wit inspect .72 18 - wit inspect - wit inspect
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .47 37 5.4 false(unreach-call) 1 wit inspect 3.8 260 false(unreach-call) 1 wit inspect 6.8 280 unknown 0 wit inspect 3.5 250 false(unreach-call) 1 wit inspect .65 18 - wit inspect - wit inspect
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 1.3  37 15   true -32 wit inspect 3.8 250 false(unreach-call) 1 wit inspect 9.2 350 unknown 0 wit inspect 4.6 260 false(unreach-call) 1 wit inspect .66 19 - wit inspect - wit inspect
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .58 39 5.7 false(unreach-call) 1 wit inspect 4.1 260 false(unreach-call) 1 wit inspect 6.8 290 unknown 0 wit inspect 4.2 270 error (2) 0 wit inspect .84 19 - wit inspect - wit inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(unreach-call) 1 wit inspect .65 43 5.6 false(unreach-call) 1 wit inspect 4.6 270 false(unreach-call) 1 wit inspect 8.3 310 unknown 0 wit inspect 3.6 260 false(unreach-call) 1 wit inspect .66 19 - wit inspect - wit inspect
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .52 36 6.0 false(unreach-call) 1 wit inspect 4.0 260 false(unreach-call) 1 wit inspect 7.9 280 unknown 0 wit inspect 3.5 250 false(unreach-call) 1 wit inspect .81 19 - wit inspect - wit inspect
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .50 36 5.7 false(unreach-call) 1 wit inspect 4.0 260 false(unreach-call) 1 wit inspect 9.9 290 unknown 0 wit inspect 3.5 250 false(unreach-call) 1 wit inspect .66 18 - wit inspect - wit inspect
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .50 36 5.2 false(unreach-call) 1 wit inspect 4.4 250 false(unreach-call) 1 wit inspect 6.6 280 unknown 0 wit inspect 4.2 250 false(unreach-call) 1 wit inspect .71 18 - wit inspect - wit inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .51 36 4.5 false(unreach-call) 1 wit inspect 3.2 270 false(unreach-call) 1 wit inspect 18   580 unknown 0 wit inspect 4.9 250 true -32 wit inspect .71 19 - wit inspect - wit inspect
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .56 36 4.9 false(unreach-call) 1 wit inspect 4.0 260 false(unreach-call) 1 wit inspect 8.6 300 unknown 0 wit inspect 3.6 250 false(unreach-call) 1 wit inspect .82 19 - wit inspect - wit inspect
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .48 36 4.8 false(unreach-call) 1 wit inspect 3.8 260 false(unreach-call) 1 wit inspect 9.7 360 unknown 0 wit inspect 3.4 250 false(unreach-call) 1 wit inspect .65 18 - wit inspect - wit inspect
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .48 36 4.5 false(unreach-call) 1 wit inspect 3.8 260 false(unreach-call) 1 wit inspect 6.9 290 unknown 0 wit inspect 3.6 250 false(unreach-call) 1 wit inspect .87 18 - wit inspect - wit inspect
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 1.3  37 12   true -32 wit inspect 4.2 250 false(unreach-call) 1 wit inspect 7.9 340 unknown 0 wit inspect 2.8 250 false(unreach-call) 1 wit inspect .80 19 - wit inspect - wit inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .53 37 5.0 false(unreach-call) 1 wit inspect 4.1 260 false(unreach-call) 1 wit inspect 6.8 290 unknown 0 wit inspect 3.5 250 error (2) 0 wit inspect .84 18 - wit inspect - wit inspect
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .52 36 5.4 false(unreach-call) 1 wit inspect 5.1 260 false(unreach-call) 1 wit inspect 7.3 290 unknown 0 wit inspect 4.1 250 false(unreach-call) 1 wit inspect .73 19 - wit inspect - wit inspect
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .52 36 4.5 false(unreach-call) 1 wit inspect 4.0 250 false(unreach-call) 1 wit inspect 5.5 280 unknown 0 wit inspect 4.3 250 false(unreach-call) 1 wit inspect .66 18 - wit inspect - wit inspect
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .49 36 4.9 false(unreach-call) 1 wit inspect 5.8 260 false(unreach-call) 1 wit inspect 13   410 unknown 0 wit inspect 3.7 250 false(unreach-call) 1 wit inspect .68 19 - wit inspect - wit inspect
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .49 37 5.2 false(unreach-call) 1 wit inspect 3.9 260 false(unreach-call) 1 wit inspect 6.2 280 unknown 0 wit inspect 3.5 210 false(unreach-call) 1 wit inspect .80 18 - wit inspect - wit inspect
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 870    2100 8600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .020 4.9
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 390    15000 4500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 44 error (2) 0 wit inspect .050 4.9
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 870    2600 4400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 46 error (2) 0 wit inspect .020 4.8
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 870    1500 4000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.9
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 870    2900 5700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .035 4.8
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 870    3200 5500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 44 error (2) 0 wit inspect .023 4.9
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 880    5300 6700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .019 4.8
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i error (42) 0 wit inspect 880    9900 7000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .027 4.9
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 870    920 9100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .019 4.8
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 870    970 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .020 4.9
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 880    8500 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .019 4.9
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 870    520 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .018 4.9
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 380    15000 4100   - 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
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 880    2200 4200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .018 5.0
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 870    1100 3600   - 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
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 870    2100 5400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .018 5.0
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 870    2100 5500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .019 5.0
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 870    2200 6900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .048 4.8
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i error (42) 0 wit inspect 880    6000 5700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .019 5.0
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 870    7500 6100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .047 4.8
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i error (42) 0 wit inspect 870    970 9900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .73 41 error (2) 0 wit inspect .047 4.8
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .50 38 5.7 timeout 0 wit inspect 92   2000 false(unreach-call) 1 wit inspect 6.8 290 unknown 0 wit inspect 3.5 250 false(unreach-call) 1 wit inspect .73 19 - wit inspect - wit inspect
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i false(valid-free) 0 wit inspect .48 36 5.4 timeout 0 wit inspect 92   2100 true -32 wit inspect 6.4 240 unknown 0 wit inspect 3.5 250 true -32 wit inspect .66 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 .46 36 4.0 false(unreach-call) 1 wit inspect 5.4 260 false(unreach-call) 1 wit inspect 5.7 260 unknown 0 wit inspect 3.8 210 false(unreach-call) 1 wit inspect .65 18 - wit inspect - wit inspect
list-ext2-properties/list_and_tree_cnstr_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect .75 47 8.4 true -32 wit inspect 6.3 260 false(unreach-call) 1 wit inspect 12   320 unknown 0 wit inspect 3.8 250 error (2) 0 wit inspect .66 19 - wit inspect - wit inspect
list-ext2-properties/list_and_tree_cnstr_true-unreach-call_false-termination.i error (42) 0 wit inspect 870    2000 5100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .044 4.9
list-ext2-properties/simple_and_skiplist_2lvl_false-unreach-call.i false(unreach-call) 1 wit inspect .50 36 5.0 false(unreach-call) 1 wit inspect 4.3 260 false(unreach-call) 1 wit inspect 7.0 300 unknown 0 wit inspect 3.6 250 false(unreach-call) 1 wit inspect .65 18 - wit inspect - wit inspect
list-ext2-properties/simple_and_skiplist_2lvl_true-unreach-call.i error (42) 0 wit inspect 870    350 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 44 error (2) 0 wit inspect .019 4.9
list-ext2-properties/simple_search_value_false-unreach-call.i false(unreach-call) 1 wit inspect 2.2  36 21   false(unreach-call) 1 wit inspect 8.1 290 out of memory 0 wit inspect 49   7000 unknown 0 wit inspect 4.1 260 error (1) 0 wit inspect .63 19 - wit inspect - wit inspect
list-ext2-properties/simple_search_value_true-unreach-call.i error (42) 0 wit inspect 880    12000 9600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .020 4.9
ldv-sets/test_add_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .50 36 4.2 false(unreach-call) 1 wit inspect 4.3 260 false(unreach-call) 1 wit inspect 7.6 280 unknown 0 wit inspect 4.5 230 error (1) 0 wit inspect .60 18 - wit inspect - wit inspect
ldv-sets/test_mutex_double_lock_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .55 37 4.9 false(unreach-call) 1 wit inspect 5.2 270 false(unreach-call) 1 wit inspect 9.9 310 unknown 0 wit inspect 4.2 250 error (1) 0 wit inspect .74 19 - wit inspect - wit inspect
ldv-sets/test_mutex_double_unlock_false-unreach-call.i false(unreach-call) 1 wit inspect 1.8  48 17   true -32 wit inspect 20   590 false(unreach-call) 1 wit inspect 9.2 460 unknown 0 wit inspect 4.8 260 error (1) 0 wit inspect .59 19 - wit inspect - wit inspect
ldv-sets/test_mutex_unbounded_false-unreach-call.i false(unreach-call) 1 wit inspect .78 47 7.7 true -32 wit inspect 9.6 310 false(unreach-call) 1 wit inspect 9.0 420 unknown 0 wit inspect 3.1 260 error (1) 0 wit inspect .72 19 - wit inspect - wit inspect
ldv-sets/test_mutex_unlock_at_exit_false-unreach-call.i false(unreach-call) 1 wit inspect 1.6  40 18   true -32 wit inspect 10   460 false(unreach-call) 1 wit inspect 11   500 unknown 0 wit inspect 5.9 260 error (1) 0 wit inspect .62 18 - wit inspect - wit inspect
ldv-sets/test_add_true-unreach-call_true-termination.i true 2 wit inspect .90 36 7.6 - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 6.5  320 error (7) 0 wit inspect 360     850  
ldv-sets/test_mutex_true-unreach-call.i true 2 wit inspect 2.2  46 26   - wit inspect - wit inspect - wit inspect - wit inspect exception 0 wit inspect 9.0  290 timeout 0 wit inspect 960     1600  
ldv-sets/test_mutex_unbounded_true-unreach-call.i error (42) 0 wit inspect 870    12000 6000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .021 4.8
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 192 40000   210000 330000 71 -691 500 23000 71 -5 1000 63000 71 0 270 17000 71 -177 50   1300 110 110 1500 20000 110 122 2300 24000
    correct results 129 192 170   6400 1800 45 45 180 12000 59 59 480 19000 0 47 47 34   870 55 110 200 14000 61 122 950 21000
        correct true 63 126 38   2100 390 0 0 0 0 55 110 200 14000 61 122 950 21000
        correct false 66 66 130   4200 1400 45 45 180 12000 59 59 480 19000 0 47 47 34   870 0 0
    correct-unconfimed results 4 0 4.5 150 48 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 4 0 4.5 150 48 0 0 0 0 0 0
    incorrect results 0 23 -736 130 6600 2 -64 13 530 0 7 -224 4.7 130 0 0
        incorrect true 0 23 -736 130 6600 2 -64 13 530 0 7 -224 4.7 130 0 0
        incorrect false 0 0 0 0 0 0 0
score (181 tasks, max score: 291) 192 -691 -5 0 -177 110 122
Run set cbmc.sv-comp18.ReachSafety-Heap cpa-seq-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-Heap uautomizer-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-cbmc.sv-comp18-violation-witness.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.ReachSafety-Heap uautomizer-validate-correctness-witnesses-cbmc.sv-comp18-correctness-witness.ReachSafety-Heap