Tool DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 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]
Date of execution 2017-11-30 16:01:31 CET 2017-12-01 08:31:47 CET 2017-12-01 08:56:50 CET 2017-12-01 08:59:39 CET 2017-12-01 09:01:39 CET 2017-12-01 08:10:33 CET 2017-12-01 08:38:18 CET
Run set depthk.sv-comp18.ReachSafety-Heap cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Heap uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.ReachSafety-Heap uautomizer-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.ReachSafety-Heap
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-11-30_1601.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/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-11-30_1601.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/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/depthk.2017-11-30_1601.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 8.4  500 92   true -32 wit inspect 4.4  260 true -32 wit inspect 6.3   270   unknown 0 wit inspect 4.0  230 false(unreach-call) 1 wit inspect .71   18    - wit inspect - wit inspect
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 6.9  480 83   true -32 wit inspect 4.2  260 true -32 wit inspect 6.6   280   unknown 0 wit inspect 3.8  220 true -32 wit inspect .66   18    - wit inspect - wit inspect
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 1.9  240 29   true -32 wit inspect 4.0  280 true -32 wit inspect 4.4   280   unknown 0 wit inspect 3.4  210 true -32 wit inspect .65   18    - wit inspect - wit inspect
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 1.4  410 17   true -32 wit inspect 4.1  260 true -32 wit inspect 6.1   260   unknown 0 wit inspect 3.5  220 true -32 wit inspect .68   18    - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(unreach-call) 0 wit inspect 1.4  190 18   true -32 wit inspect 3.7  260 true -32 wit inspect 5.8   250   unknown 0 wit inspect 3.5  210 true -32 wit inspect .65   19    - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 1.4  190 17   true -32 wit inspect 3.9  280 true -32 wit inspect 5.7   250   unknown 0 wit inspect 3.5  210 true -32 wit inspect .65   18    - wit inspect - wit inspect
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    930 9300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 41 error (2) 0 wit inspect .019 4.9
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900    190 9000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .50 43 error (2) 0 wit inspect .018 4.8
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    680 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 5.0
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    800 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 45 error (2) 0 wit inspect .019 4.9
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    430 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .019 4.9
heap-manipulation/tree_true-unreach-call.i unknown 0 wit inspect 890    200 10000   - 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/alternating_list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 1.5  180 22   true -32 wit inspect 3.7  260 true -32 wit inspect 5.1   240   unknown 0 wit inspect 3.4  220 true -32 wit inspect .63   18    - wit inspect - wit inspect
list-properties/list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 1.4  240 15   unknown 0 wit inspect 4.3  260 true -32 wit inspect 3.3   230   unknown 0 wit inspect 2.4  210 true -32 wit inspect .64   18    - wit inspect - wit inspect
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 1.2  180 16   true -32 wit inspect 3.6  260 true -32 wit inspect 3.5   230   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 2.7  100 33   true -32 wit inspect 3.6  260 true -32 wit inspect 5.1   240   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .67   18    - wit inspect - wit inspect
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 1.2  160 15   false(unreach-call) 1 wit inspect 4.3  260 true -32 wit inspect 5.1   230   unknown 0 wit inspect 2.4  210 true -32 wit inspect .64   18    - wit inspect - wit inspect
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 1.5  210 17   true -32 wit inspect 2.6  260 true -32 wit inspect 6.9   300   unknown 0 wit inspect 3.6  210 error (255) 0 wit inspect .59   18    - wit inspect - wit inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900    510 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .023 4.9
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900    340 11000   - 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
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i true 2 wit inspect 34    480 230   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 22    510 true 2 wit inspect 64     970  
list-properties/list_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 890    250 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .047 4.8
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900    220 13000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .019 4.9
list-properties/simple_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900    420 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .020 4.9
list-properties/splice_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900    210 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .019 4.8
ldv-regression/1_3_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .48 49 6.2 true -32 wit inspect 3.1  260 true -32 wit inspect 4.5   230   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/alt_test_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 4.5  450 32   exception 0 wit inspect 3.5  260 true -32 wit inspect 3.4   230   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .71   18    - wit inspect - wit inspect
ldv-regression/callfpointer_true-termination.c_false-unreach-call.i unknown 0 wit inspect 16    28 210   error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
ldv-regression/fo_test_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .51 29 5.6 exception 0 wit inspect 3.4  260 true -32 wit inspect 4.8   240   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .66   18    - wit inspect - wit inspect
ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .39 48 4.3 true -32 wit inspect 3.0  260 true -32 wit inspect 4.6   230   unknown 0 wit inspect 3.2  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
ldv-regression/mutex_lock_struct_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .38 49 4.7 true -32 wit inspect 2.9  260 true -32 wit inspect 4.6   230   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/recursive_list_true-termination.c_false-unreach-call.i false(unreach-call) 0 wit inspect .58 49 6.1 true -32 wit inspect 3.2  250 true -32 wit inspect 4.5   230   unknown 0 wit inspect 2.8  210 error (2) 0 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/rule57_ebda_blast_true-termination.c_false-unreach-call.i false(unreach-call) 0 wit inspect .41 50 4.4 true -32 wit inspect 3.5  260 true -32 wit inspect 5.4   240   unknown 0 wit inspect 3.0  210 error (2) 0 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/rule60_list2_true-termination.c_false-unreach-call_1.i false(unreach-call) 0 wit inspect 5.0  440 44   error (invalid witness file) 0 wit inspect 2.7  170 true -32 wit inspect 3.8   250   error (invalid witness file) 0 wit inspect 3.0  170 error (2) 0 wit inspect .62   18    - wit inspect - wit inspect
ldv-regression/stateful_check_false-unreach-call_false-termination.i false(unreach-call) 0 wit inspect 2.1  77 26   true -32 wit inspect 2.4  260 true -32 wit inspect 5.2   230   unknown 0 wit inspect 3.0  210 true -32 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 1.5  75 19   true -32 wit inspect 2.1  260 true -32 wit inspect 4.7   220   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect 1.5  75 23   true -32 wit inspect 3.1  250 true -32 wit inspect 4.5   220   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call.i true 2 wit inspect 3.8  270 36   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 5.8   270  
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i true 2 wit inspect 3.5  270 35   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.5   260  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call.i true 2 wit inspect 3.5  270 33   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 5.6   280  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call_1.i true 2 wit inspect 3.6  260 34   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  240 true 2 wit inspect 5.0   260  
ldv-regression/ex3_forlist_true-termination.c_true-unreach-call.i true 2 wit inspect 4.0  260 40   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 17    470 true 2 wit inspect 29     700  
ldv-regression/just_assert_true-termination.c_true-unreach-call.i true 2 wit inspect 2.9  220 29   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 4.3   220  
ldv-regression/mutex_lock_int_true-termination.c_true-unreach-call_1.i true 2 wit inspect 3.5  260 34   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 6.0   260  
ldv-regression/mutex_lock_struct_true-termination.c_true-unreach-call_1.i true 2 wit inspect 3.9  270 35   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 6.6   270  
ldv-regression/nested_structure_noptr_true-termination.c_true-unreach-call.i true 2 wit inspect 3.1  260 31   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 4.3   240  
ldv-regression/nested_structure_noptr_true-unreach-call_true-termination.i true 2 wit inspect 3.1  250 35   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.0   260  
ldv-regression/nested_structure_ptr_true-termination.c_true-unreach-call.i true 2 wit inspect 3.8  270 36   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 11     450  
ldv-regression/nested_structure_ptr_true-unreach-call_true-termination.i true 2 wit inspect 3.7  270 40   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  270 true 2 wit inspect 9.3   400  
ldv-regression/nested_structure_true-termination.c_true-unreach-call.i true 2 wit inspect 3.9  280 36   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  240 true 2 wit inspect 7.4   280  
ldv-regression/nested_structure_true-unreach-call_true-termination.i true 2 wit inspect 3.7  270 31   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 8.5   300  
ldv-regression/oomInt_true-termination.c_true-unreach-call.i true 2 wit inspect 3.3  260 29   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 5.5   270  
ldv-regression/oomInt_true-termination.c_true-unreach-call_1.i true 2 wit inspect 3.1  260 32   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.1   260  
ldv-regression/rule57_ebda_blast_true-termination.c_true-unreach-call_1.i true 2 wit inspect 3.4  270 31   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 6.7   280  
ldv-regression/rule60_list2_true-termination.c_true-unreach-call.i true 2 wit inspect 9.3  410 96   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  260 true 2 wit inspect 22     650  
ldv-regression/rule60_list_true-termination.c_true-unreach-call.i true 2 wit inspect 5.2  280 50   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  260 true 2 wit inspect 10     370  
ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i true 2 wit inspect 3.6  270 37   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 4.8   260  
ldv-regression/structure_assignment_true-termination.c_true-unreach-call.i true 2 wit inspect 3.5  270 32   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 4.9   260  
ldv-regression/test_address_true-termination.c_true-unreach-call.i true 2 wit inspect 5.3  290 52   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  260 true 2 wit inspect 5.3   260  
ldv-regression/test_cut_trace_true-termination.c_true-unreach-call.i true 2 wit inspect 3.0  260 29   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 5.1   250  
ldv-regression/test_malloc-1_true-unreach-call_true-termination.i true 2 wit inspect 5.0  280 52   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  270 true 2 wit inspect 5.9   280  
ldv-regression/test_malloc-2_true-unreach-call_true-termination.i true 2 wit inspect 5.3  280 52   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  260 true 2 wit inspect 7.3   330  
ldv-regression/test_overflow_true-termination.c_true-unreach-call.i true 2 wit inspect .99 48 12   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 5.0   260  
ldv-regression/test_union_cast-1_true-unreach-call_true-termination.i true 2 wit inspect 3.2  260 33   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 5.2   260  
ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i true 2 wit inspect 4.0  270 39   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 5.7   270  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call.i true 2 wit inspect 3.9  280 34   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 5.1   260  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call_1.i true 2 wit inspect 3.2  270 30   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 3.7   270  
ldv-regression/test_union_true-termination.c_true-unreach-call.i true 2 wit inspect 3.2  260 29   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 5.8   280  
ldv-regression/test_union_true-termination.c_true-unreach-call_1.i true 2 wit inspect 3.1  260 30   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 5.7   260  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call.i true 2 wit inspect 3.6  270 33   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 5.6   270  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i true 2 wit inspect 3.6  270 30   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.8  250 true 2 wit inspect 5.5   260  
ldv-regression/test02_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .38 48 4.7 true -32 wit inspect 2.9  250 true -32 wit inspect 4.5   210   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/test06_false-unreach-call_true-termination.c false(unreach-call) 0 wit inspect .40 48 4.2 true -32 wit inspect 3.2  250 true -32 wit inspect 6.3   300   unknown 0 wit inspect 2.9  210 error (2) 0 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/test08_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .39 48 4.4 true -32 wit inspect 3.3  260 true -32 wit inspect 5.0   230   unknown 0 wit inspect 2.9  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/test12_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .37 27 4.2 true -32 wit inspect 3.0  250 true -32 wit inspect 5.1   220   unknown 0 wit inspect 2.9  190 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/test21_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .37 39 4.6 true -32 wit inspect 2.9  260 true -32 wit inspect 4.6   220   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/test22_false-unreach-call.c false(unreach-call) 0 wit inspect .37 66 4.4 true -32 wit inspect 3.3  260 true -32 wit inspect 4.9   230   unknown 0 wit inspect 3.1  210 true -32 wit inspect .62   18    - wit inspect - wit inspect
ldv-regression/test23_false-unreach-call.c false(unreach-call) 0 wit inspect 16    66 200   true -32 wit inspect 3.4  260 true -32 wit inspect 5.2   240   unknown 0 wit inspect 3.2  210 true -32 wit inspect .62   18    - wit inspect - wit inspect
ldv-regression/test24_false-unreach-call.c false(unreach-call) 0 wit inspect 1.3  100 15   true -32 wit inspect 3.6  260 true -32 wit inspect 5.1   250   unknown 0 wit inspect 2.2  210 error (2) 0 wit inspect .61   19    - wit inspect - wit inspect
ldv-regression/test25_false-unreach-call_true-termination.c false(unreach-call) 0 wit inspect 6.9  100 94   true -32 wit inspect 3.4  260 true -32 wit inspect 5.2   250   unknown 0 wit inspect 3.0  210 error (2) 0 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/test26_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .38 48 4.3 true -32 wit inspect 2.9  250 true -32 wit inspect 4.6   220   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/test27_false-unreach-call_true-termination.c false(unreach-call) 0 wit inspect 6.4  110 92   true -32 wit inspect 3.4  260 true -32 wit inspect 5.0   240   unknown 0 wit inspect 3.3  210 error (2) 0 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/test28_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .40 49 4.5 true -32 wit inspect 2.2  260 true -32 wit inspect 4.4   230   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/test29_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .37 48 4.8 true -32 wit inspect 3.0  260 true -32 wit inspect 4.7   230   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/test30_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .37 48 4.6 true -32 wit inspect 2.3  260 true -32 wit inspect 4.7   240   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/test01_true-unreach-call_true-termination.c true 2 wit inspect 3.5  260 35   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 5.7   270  
ldv-regression/test03_true-unreach-call_true-termination.c true 2 wit inspect 3.9  280 33   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 6.6   280  
ldv-regression/test04_true-unreach-call_true-termination.c true 2 wit inspect 3.6  270 33   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 6.8   270  
ldv-regression/test05_true-unreach-call_true-termination.c true 2 wit inspect 4.0  280 38   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 10     480  
ldv-regression/test07_true-unreach-call_true-termination.c true 2 wit inspect 4.0  270 40   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 8.2   350  
ldv-regression/test09_true-unreach-call_true-termination.c true 2 wit inspect 3.8  280 38   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 8.8   340  
ldv-regression/test10_true-unreach-call_true-termination.c true 2 wit inspect 3.9  270 37   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 12     490  
ldv-regression/test11_true-unreach-call_true-termination.c true 2 wit inspect 4.0  280 34   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 7.3   270  
ldv-regression/test13_true-unreach-call_true-termination.c true 2 wit inspect 3.5  260 34   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 5.4   270  
ldv-regression/test14_true-unreach-call_true-termination.c true 2 wit inspect 3.9  270 40   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  260 true 2 wit inspect 7.3   260  
ldv-regression/test15_true-unreach-call_true-termination.c true 2 wit inspect 3.7  270 37   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 6.9   280  
ldv-regression/test16_true-unreach-call_true-termination.c true 2 wit inspect 3.6  270 39   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 7.6   280  
ldv-regression/test17_true-unreach-call_true-termination.c true 2 wit inspect 3.6  270 35   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.0   260  
ldv-regression/test18_true-unreach-call_true-termination.c true 2 wit inspect 4.0  270 36   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 8.0   310  
ldv-regression/test19_true-unreach-call_true-termination.c true 2 wit inspect 3.6  270 33   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 8.5   350  
ldv-regression/test20_true-unreach-call_true-termination.c true 2 wit inspect 3.6  260 32   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 5.6   260  
ldv-regression/test21_true-unreach-call_true-termination.c true 2 wit inspect 4.2  280 42   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 7.8   310  
ldv-regression/test22_true-unreach-call.c true 2 wit inspect 6.9  280 57   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.3  290 true 2 wit inspect 20     630  
ldv-regression/test23_true-unreach-call.c true 2 wit inspect 21    400 220   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.3  300 true 2 wit inspect 210     800  
ldv-regression/test24_true-unreach-call_true-termination.c true 2 wit inspect 44    500 590   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1  280 true 2 wit inspect 10     420  
ldv-regression/test25_true-unreach-call.c true 2 wit inspect 220    1200 2400   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 49    760 true 2 wit inspect 27     550  
ldv-regression/test26_true-unreach-call_true-termination.c true 2 wit inspect 3.8  270 36   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 7.3   290  
ldv-regression/test27_true-unreach-call_true-termination.c true 2 wit inspect 22    660 280   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 120    880 true 2 wit inspect 170     820  
ldv-regression/test28_true-unreach-call_true-termination.c true 2 wit inspect 4.0  270 37   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  260 true 2 wit inspect 7.3   270  
ldv-regression/test29_true-unreach-call_true-termination.c true 2 wit inspect 3.9  270 33   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 6.9   260  
ldv-regression/test30_true-unreach-call_true-termination.c true 2 wit inspect 3.8  270 35   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 9.3   430  
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    1200 9500   error (invalid witness file) 0 wit inspect .51 42 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0014 .27 - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    910 12000   error (invalid witness file) 0 wit inspect .45 45 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .88 47 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    1200 11000   error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900    1200 7600   - 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_inb_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900    1200 7300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .020 4.8
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900    1200 7700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .049 4.9
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900    1200 7200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .020 4.9
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900    1200 7500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .039 4.8
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900    1200 7000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 42 error (2) 0 wit inspect .019 4.9
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900    1300 7900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .021 4.9
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900    1300 8600   - 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
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900    1200 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .020 4.9
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 900    1200 7800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .018 4.8
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 1.2  160 15   unknown 0 wit inspect 4.3  270 true -32 wit inspect 6.0   260   unknown 0 wit inspect 3.6  210 false(unreach-call) 1 wit inspect .71   19    - wit inspect - wit inspect
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .83 130 9.9 unknown 0 wit inspect 3.7  260 true -32 wit inspect 5.1   240   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .69 130 8.0 false(unreach-call) 1 wit inspect 4.1  270 true -32 wit inspect 5.6   250   unknown 0 wit inspect 2.5  210 false(unreach-call) 1 wit inspect .64   18    - wit inspect - wit inspect
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 3.6  140 42   unknown 0 wit inspect 4.4  270 true -32 wit inspect 5.8   250   unknown 0 wit inspect 3.6  220 true -32 wit inspect .64   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 130 7.3 false(unreach-call) 1 wit inspect 3.9  270 true -32 wit inspect 5.5   240   unknown 0 wit inspect 2.3  210 false(unreach-call) 1 wit inspect .66   18    - wit inspect - wit inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(unreach-call) 0 wit inspect 1.8  130 24   unknown 0 wit inspect 4.0  270 true -32 wit inspect 5.6   250   unknown 0 wit inspect 2.3  210 true -32 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 .72 190 8.4 false(unreach-call) 1 wit inspect 4.1  270 true -32 wit inspect 5.2   230   unknown 0 wit inspect 3.7  220 false(unreach-call) 1 wit inspect .65   19    - wit inspect - wit inspect
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 1.8  210 23   unknown 0 wit inspect 3.0  270 true -32 wit inspect 6.2   260   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .72 130 9.8 unknown 0 wit inspect 4.0  260 true -32 wit inspect 5.2   240   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .63   19    - wit inspect - wit inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 2.1  160 28   false(unreach-call) 1 wit inspect 4.2  270 true -32 wit inspect 6.0   260   unknown 0 wit inspect 3.4  210 error (2) 0 wit inspect .66   18    - wit inspect - wit inspect
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 1.7  190 21   unknown 0 wit inspect 4.0  290 true -32 wit inspect 6.8   260   unknown 0 wit inspect 3.4  210 true -32 wit inspect .65   18    - wit inspect - wit inspect
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .82 130 10   false(unreach-call) 1 wit inspect 4.1  270 true -32 wit inspect 5.5   240   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .64   18    - wit inspect - wit inspect
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .67 130 8.3 false(unreach-call) 1 wit inspect 4.2  280 true -32 wit inspect 5.9   250   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .74   18    - wit inspect - wit inspect
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 3.4  140 43   unknown 0 wit inspect 4.3  270 true -32 wit inspect 5.9   250   unknown 0 wit inspect 3.4  220 true -32 wit inspect .65   18    - wit inspect - wit inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .57 130 6.4 false(unreach-call) 1 wit inspect 4.2  270 true -32 wit inspect 5.5   250   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 1.5  130 19   unknown 0 wit inspect 4.1  270 true -32 wit inspect 5.4   240   unknown 0 wit inspect 3.4  220 true -32 wit inspect .64   18    - wit inspect - wit inspect
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .68 190 8.0 false(unreach-call) 1 wit inspect 2.8  270 true -32 wit inspect 5.4   240   unknown 0 wit inspect 3.4  220 false(unreach-call) 1 wit inspect .65   19    - wit inspect - wit inspect
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 1.8  210 26   true -32 wit inspect 4.3  260 true -32 wit inspect 5.5   250   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .67   18    - wit inspect - wit inspect
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .68 130 9.0 false(unreach-call) 1 wit inspect 4.1  260 true -32 wit inspect 5.2   240   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .64   18    - wit inspect - wit inspect
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    540 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .020 4.9
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    210 9500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .019 5.0
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900    480 10000   - 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/dll-queue_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900    920 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 43 error (2) 0 wit inspect .018 4.8
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    270 9900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .018 4.9
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    380 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .018 4.9
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    190 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .042 4.9
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 890    190 9700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .019 4.8
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    210 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 4.9
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    280 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .019 4.9
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900    620 8500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .020 4.9
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    190 9500   - 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-circular_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    190 12000   - 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
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900    520 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 46 error (2) 0 wit inspect .018 4.8
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 900    940 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .022 4.8
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    190 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 42 error (2) 0 wit inspect .018 4.8
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    200 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.8
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    190 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .028 4.8
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 890    190 9600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 41 error (2) 0 wit inspect .019 4.9
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    210 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .020 4.9
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 890    340 9400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .020 4.9
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .93 270 12   timeout 0 wit inspect 91    2000 true -32 wit inspect 5.4   230   unknown 0 wit inspect 2.3  210 false(unreach-call) 1 wit inspect .64   18    - wit inspect - wit inspect
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i false(unreach-call) 0 wit inspect 15    190 230   timeout 0 wit inspect 91    1900 true -32 wit inspect 5.2   240   unknown 0 wit inspect 3.6  210 true -32 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 .79 180 12   false(unreach-call) 1 wit inspect 4.3  260 true -32 wit inspect 5.1   220   unknown 0 wit inspect 3.2  210 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 false(unreach-call) 0 wit inspect 1.9  350 24   unknown 0 wit inspect 3.9  270 true -32 wit inspect 5.9   250   unknown 0 wit inspect 3.7  210 error (2) 0 wit inspect .63   18    - wit inspect - wit inspect
list-ext2-properties/list_and_tree_cnstr_true-unreach-call_false-termination.i unknown 0 wit inspect 890    370 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .020 4.9
list-ext2-properties/simple_and_skiplist_2lvl_false-unreach-call.i false(unreach-call) 1 wit inspect 1.5  270 19   false(unreach-call) 1 wit inspect 3.2  270 true -32 wit inspect 6.5   260   unknown 0 wit inspect 3.5  210 true -32 wit inspect .64   19    - wit inspect - wit inspect
list-ext2-properties/simple_and_skiplist_2lvl_true-unreach-call.i unknown 0 wit inspect 890    270 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .020 4.8
list-ext2-properties/simple_search_value_false-unreach-call.i false(unreach-call) 1 wit inspect 9.1  160 130   unknown 0 wit inspect 3.3  270 true -32 wit inspect 3.5   240   unknown 0 wit inspect 2.4  210 false(unreach-call) 1 wit inspect .64   18    - wit inspect - wit inspect
list-ext2-properties/simple_search_value_true-unreach-call.i unknown 0 wit inspect 900    550 9000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 43 error (2) 0 wit inspect .019 4.9
ldv-sets/test_add_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect .57 100 6.5 true -32 wit inspect 3.7  260 true -32 wit inspect 5.2   240   unknown 0 wit inspect 3.3  220 error (1) 0 wit inspect .59   18    - wit inspect - wit inspect
ldv-sets/test_mutex_double_lock_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 3.4  270 43   true -32 wit inspect 4.4  260 true -32 wit inspect 7.3   330   unknown 0 wit inspect 3.6  210 error (1) 0 wit inspect .60   18    - wit inspect - wit inspect
ldv-sets/test_mutex_double_unlock_false-unreach-call.i false(unreach-call) 0 wit inspect 140    310 1300   true -32 wit inspect 4.2  260 true -32 wit inspect 5.8   250   unknown 0 wit inspect 3.8  220 error (1) 0 wit inspect .59   19    - wit inspect - wit inspect
ldv-sets/test_mutex_unbounded_false-unreach-call.i false(unreach-call) 0 wit inspect 25    240 250   timeout 0 wit inspect 92    2300 true -32 wit inspect 6.0   250   unknown 0 wit inspect 3.8  220 error (1) 0 wit inspect .67   19    - wit inspect - wit inspect
ldv-sets/test_mutex_unlock_at_exit_false-unreach-call.i false(unreach-call) 0 wit inspect 83    220 790   true -32 wit inspect 4.5  270 true -32 wit inspect 5.7   250   unknown 0 wit inspect 3.8  220 error (1) 0 wit inspect .59   19    - wit inspect - wit inspect
ldv-sets/test_add_true-unreach-call_true-termination.i true 2 wit inspect 1.4  100 23   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.0  290 error (7) 0 wit inspect 360     860  
ldv-sets/test_mutex_true-unreach-call.i true 2 wit inspect 440    1500 4600   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 300    3600 timeout 0 wit inspect 960     1400  
ldv-sets/test_mutex_unbounded_true-unreach-call.i unknown 0 wit inspect 890    1200 7600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .021 4.9
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
total 181 163 46000 61000 510000 71 -1172 510 23000 71 -2144 350 16000 71 0 220 14000 71 -542 42 1200 110 126 740 23000 110 122 2200 24000
    correct results 100 163 1000 25000 11000 12 12 47 3200 0 0 34 34 21 630 63 126 710 21000 61 122 900 21000
        correct true 63 126 990 20000 10000 0 0 0 0 63 126 710 21000 61 122 900 21000
        correct false 37 37 52 5100 640 12 12 47 3200 0 0 34 34 21 630 0 0
    correct-unconfimed results 30 0 340 5700 3500 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 30 0 340 5700 3500 0 0 0 0 0 0
    incorrect results 0 37 -1184 120 9600 67 -2144 350 16000 0 18 -576 12 330 0 0
        incorrect true 0 37 -1184 120 9600 67 -2144 350 16000 0 18 -576 12 330 0 0
        incorrect false 0 0 0 0 0 0 0
score (181 tasks, max score: 291) 163 -1172 -2144 0 -542 126 122
Run set depthk.sv-comp18.ReachSafety-Heap cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Heap uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.ReachSafety-Heap uautomizer-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.ReachSafety-Heap