Tool Predator-HP 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* [apollon077; apollon078; apollon109] 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: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 33553 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-01 20:24:12 CET 2017-12-01 21:20:39 CET 2017-12-01 21:42:31 CET 2017-12-01 21:44:16 CET 2017-12-01 21:44:33 CET 2017-12-01 21:03:47 CET 2017-12-01 21:22:11 CET
Run set predatorhp.sv-comp18 cpa-seq-validate-violation-witnesses-predatorhp.sv-comp18-violation-witness uautomizer-validate-violation-witnesses-predatorhp.sv-comp18-violation-witness cpa-witness2test-validate-violation-witnesses-predatorhp.sv-comp18-violation-witness fshell-witness2test-validate-violation-witnesses-predatorhp.sv-comp18-violation-witness cpa-seq-validate-correctness-witnesses-predatorhp.sv-comp18-correctness-witness uautomizer-validate-correctness-witnesses-predatorhp.sv-comp18-correctness-witness
Options --witness error-witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/predatorhp.2017-12-01_2024.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/predatorhp.2017-12-01_2024.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/predatorhp.2017-12-01_2024.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/predatorhp.2017-12-01_2024.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/predatorhp.2017-12-01_2024.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/predatorhp.2017-12-01_2024.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 1.1  51 14   false(unreach-call) 1 wit inspect 3.0  270 false(unreach-call) 1 wit inspect 8.6   330   unknown 0 wit inspect 3.6  210 false(unreach-call) 1 wit inspect .72   18    - wit inspect - wit inspect
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 2.3  53 24   true -32 wit inspect 4.7  260 true -32 wit inspect 7.2   280   unknown 0 wit inspect 6.0  280 true -32 wit inspect .66   18    - wit inspect - wit inspect
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .17 26 2.0 false(unreach-call) 1 wit inspect 2.8  270 false(unreach-call) 1 wit inspect 8.5   310   unknown 0 wit inspect 3.7  210 true -32 wit inspect .66   18    - wit inspect - wit inspect
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 2.4  69 21   false(unreach-call) 1 wit inspect 4.0  270 true -32 wit inspect 6.5   260   unknown 0 wit inspect 3.7  240 true -32 wit inspect .66   18    - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-deref.i timeout 0 wit inspect 900    120 13000   error (invalid witness file) 0 wit inspect .40 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0012 .30 - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 2.1  26 22   false(unreach-call) 1 wit inspect 4.0  290 true -32 wit inspect 6.3   250   unknown 0 wit inspect 3.4  210 true -32 wit inspect .64   18    - wit inspect - wit inspect
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 1.5  49 20   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5200 timeout 0 wit inspect 960     1000  
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .29 26 3.2 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 3.8  250 true 2 wit inspect 710     860  
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.5  58 28   - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 140    1600 timeout 0 wit inspect 960     5300  
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 1.6  68 20   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5200 timeout 0 wit inspect 960     1400  
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.2  73 22   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4000 timeout 0 wit inspect 960     860  
heap-manipulation/tree_true-unreach-call.i timeout 0 wit inspect 900    860 5500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .049 4.9
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .18 25 1.9 false(unreach-call) 1 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 6.5   270   unknown 0 wit inspect 3.6  230 true -32 wit inspect .67   18    - wit inspect - wit inspect
list-properties/list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 1.1  26 11   unknown 0 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 13     490   unknown 0 wit inspect 3.5  210 true -32 wit inspect .66   18    - wit inspect - wit inspect
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .22 24 2.1 false(unreach-call) 1 wit inspect 2.6  260 false(unreach-call) 1 wit inspect 5.7   270   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .17 24 1.8 unknown 0 wit inspect 3.1  280 true -32 wit inspect 17     640   unknown 0 wit inspect 3.6  210 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .15 24 2.0 false(unreach-call) 1 wit inspect 2.5  260 false(unreach-call) 1 wit inspect 5.3   260   unknown 0 wit inspect 3.6  210 true -32 wit inspect .64   18    - wit inspect - wit inspect
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .19 23 2.3 false(unreach-call) 1 wit inspect 3.7  270 false(unreach-call) 1 wit inspect 7.2   270   unknown 0 wit inspect 3.9  230 true -32 wit inspect .66   18    - wit inspect - wit inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    2000 7700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .047 4.8
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 2.4  24 22   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2000 timeout 0 wit inspect 960     1000  
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i true 2 wit inspect .25 25 2.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 19    510 true 2 wit inspect 72     1100  
list-properties/list_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 2.7  24 26   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2900 timeout 0 wit inspect 960     1200  
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 2.7  24 29   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2000 timeout 0 wit inspect 960     1200  
list-properties/simple_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 2.7  24 27   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2000 timeout 0 wit inspect 960     1000  
list-properties/splice_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900    1400 9200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .050 4.9
ldv-regression/1_3_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .13 22 1.9 false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 5.4   260   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/alt_test_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .12 25 2.1 false(unreach-call) 1 wit inspect 2.7  270 false(unreach-call) 1 wit inspect 6.7   270   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .67   18    - wit inspect - wit inspect
ldv-regression/callfpointer_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .15 22 1.8 false(unreach-call) 1 wit inspect 2.9  250 false(unreach-call) 1 wit inspect 4.7   230   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .64   18    - wit inspect - wit inspect
ldv-regression/fo_test_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .13 24 1.9 false(unreach-call) 1 wit inspect 2.6  270 unknown 0 wit inspect 13     290   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 .12 23 1.8 false(unreach-call) 1 wit inspect 2.2  260 false(unreach-call) 1 wit inspect 6.3   250   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/mutex_lock_struct_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .12 23 1.8 false(unreach-call) 1 wit inspect 2.2  260 false(unreach-call) 1 wit inspect 5.2   250   unknown 0 wit inspect 3.1  190 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) 1 wit inspect .15 22 2.1 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 6.5   260   unknown 0 wit inspect 2.9  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/rule57_ebda_blast_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .19 24 2.1 false(unreach-call) 1 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 6.4   280   unknown 0 wit inspect 3.2  210 error (2) 0 wit inspect .61   18    - wit inspect - wit inspect
ldv-regression/rule60_list2_true-termination.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect .15 25 5.1 false(unreach-call) 1 wit inspect 2.6  270 false(unreach-call) 1 wit inspect 13     500   unknown 0 wit inspect 3.4  210 true -32 wit inspect .65   18    - wit inspect - wit inspect
ldv-regression/stateful_check_false-unreach-call_false-termination.i false(unreach-call) 0 wit inspect .16 24 1.9 true -32 wit inspect 3.6  260 true -32 wit inspect 5.9   260   unknown 0 wit inspect 3.3  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 .13 23 1.7 false(unreach-call) 1 wit inspect 2.1  260 false(unreach-call) 1 wit inspect 4.7   240   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect .13 22 1.8 false(unreach-call) 1 wit inspect 2.9  260 false(unreach-call) 1 wit inspect 5.2   260   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call.i true 2 wit inspect .12 21 1.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 5.7   270  
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i true 2 wit inspect .14 23 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 5.5   260  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call.i true 2 wit inspect .14 21 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 6.4   270  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call_1.i true 2 wit inspect .14 22 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 5.0   260  
ldv-regression/ex3_forlist_true-termination.c_true-unreach-call.i true 2 wit inspect .14 23 2.3 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 19    480 true 2 wit inspect 30     690  
ldv-regression/just_assert_true-termination.c_true-unreach-call.i true 2 wit inspect .14 20 1.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 4.4   210  
ldv-regression/mutex_lock_int_true-termination.c_true-unreach-call_1.i true 2 wit inspect .15 21 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 6.2   280  
ldv-regression/mutex_lock_struct_true-termination.c_true-unreach-call_1.i true 2 wit inspect .15 27 1.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 6.3   260  
ldv-regression/nested_structure_noptr_true-termination.c_true-unreach-call.i true 2 wit inspect .14 22 1.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 4.8   240  
ldv-regression/nested_structure_noptr_true-unreach-call_true-termination.i true 2 wit inspect .12 22 1.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 4.6   260  
ldv-regression/nested_structure_ptr_true-termination.c_true-unreach-call.i true 2 wit inspect .13 21 2.1 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 10     480  
ldv-regression/nested_structure_ptr_true-unreach-call_true-termination.i true 2 wit inspect .12 22 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  260 true 2 wit inspect 10     390  
ldv-regression/nested_structure_true-termination.c_true-unreach-call.i true 2 wit inspect .11 21 1.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 9.5   280  
ldv-regression/nested_structure_true-unreach-call_true-termination.i true 2 wit inspect .14 22 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 7.9   280  
ldv-regression/oomInt_true-termination.c_true-unreach-call.i true 2 wit inspect .15 22 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 5.9   260  
ldv-regression/oomInt_true-termination.c_true-unreach-call_1.i true 2 wit inspect .12 21 1.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.6   270  
ldv-regression/rule57_ebda_blast_true-termination.c_true-unreach-call_1.i true 2 wit inspect .31 23 3.0 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 6.5   270  
ldv-regression/rule60_list2_true-termination.c_true-unreach-call.i true 2 wit inspect .16 29 2.0 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  270 true 2 wit inspect 22     650  
ldv-regression/rule60_list_true-termination.c_true-unreach-call.i true 2 wit inspect .19 22 2.1 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  250 true 2 wit inspect 10     370  
ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i true 2 wit inspect .15 22 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 5.2   260  
ldv-regression/structure_assignment_true-termination.c_true-unreach-call.i true 2 wit inspect .15 21 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 5.3   260  
ldv-regression/test_address_true-termination.c_true-unreach-call.i true 2 wit inspect .12 22 1.9 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  250 true 2 wit inspect 5.9   260  
ldv-regression/test_cut_trace_true-termination.c_true-unreach-call.i true 2 wit inspect .15 21 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.2   260  
ldv-regression/test_malloc-1_true-unreach-call_true-termination.i true 2 wit inspect .17 22 1.9 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 6.6   260  
ldv-regression/test_malloc-2_true-unreach-call_true-termination.i true 2 wit inspect .14 23 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  270 true 2 wit inspect 6.2   260  
ldv-regression/test_overflow_true-termination.c_true-unreach-call.i unknown 0 wit inspect .16 24 1.8 - 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
ldv-regression/test_union_cast-1_true-unreach-call_true-termination.i true 2 wit inspect .15 22 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 5.1   260  
ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i true 2 wit inspect .12 21 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 6.2   270  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call.i true 2 wit inspect .14 21 1.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.6   250  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call_1.i true 2 wit inspect .12 21 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 5.3   260  
ldv-regression/test_union_true-termination.c_true-unreach-call.i true 2 wit inspect .15 21 1.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.7   270  
ldv-regression/test_union_true-termination.c_true-unreach-call_1.i true 2 wit inspect .14 21 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 6.7   270  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call.i true 2 wit inspect .15 21 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 6.3   280  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i true 2 wit inspect .11 20 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.8  250 true 2 wit inspect 6.1   270  
ldv-regression/test02_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .12 22 1.8 false(unreach-call) 1 wit inspect 2.1  250 false(unreach-call) 1 wit inspect 4.7   230   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/test06_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .12 22 2.1 false(unreach-call) 1 wit inspect 2.4  270 true -32 wit inspect 5.5   230   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/test08_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .12 23 1.9 false(unreach-call) 1 wit inspect 2.2  260 false(unreach-call) 1 wit inspect 5.3   260   unknown 0 wit inspect 2.8  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 .14 23 1.8 false(unreach-call) 1 wit inspect 2.2  270 false(unreach-call) 1 wit inspect 5.1   230   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/test21_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .17 29 1.8 false(unreach-call) 1 wit inspect 2.2  260 true -32 wit inspect 5.0   230   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/test22_false-unreach-call.c false(unreach-call) 1 wit inspect .18 23 1.9 false(unreach-call) 1 wit inspect 2.4  260 true -32 wit inspect 4.9   230   unknown 0 wit inspect 3.0  180 true -32 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/test23_false-unreach-call.c unknown 0 wit inspect .14 23 1.8 error (invalid witness file) 0 wit inspect .42 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .89 49 error (invalid witness file) 0 wit inspect .0015 .29 - wit inspect - wit inspect
ldv-regression/test24_false-unreach-call.c unknown 0 wit inspect .26 24 3.1 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .023 4.9 error (invalid witness file) 0 wit inspect .66 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
ldv-regression/test25_false-unreach-call_true-termination.c unknown 0 wit inspect .19 23 2.2 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .98 51 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
ldv-regression/test26_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .15 23 1.7 false(unreach-call) 1 wit inspect 2.9  260 false(unreach-call) 1 wit inspect 5.9   260   unknown 0 wit inspect 2.9  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/test27_false-unreach-call_true-termination.c unknown 0 wit inspect .16 23 1.9 error (invalid witness file) 0 wit inspect .44 44 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .95 50 error (invalid witness file) 0 wit inspect .0012 .27 - wit inspect - wit inspect
ldv-regression/test28_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .12 21 1.9 false(unreach-call) 1 wit inspect 2.3  260 false(unreach-call) 1 wit inspect 7.4   270   unknown 0 wit inspect 2.8  180 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 .14 23 1.7 false(unreach-call) 1 wit inspect 2.2  260 false(unreach-call) 1 wit inspect 6.8   260   unknown 0 wit inspect 1.9  190 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
ldv-regression/test30_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .12 23 1.9 false(unreach-call) 1 wit inspect 2.2  260 false(unreach-call) 1 wit inspect 5.8   260   unknown 0 wit inspect 2.9  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/test01_true-unreach-call_true-termination.c true 2 wit inspect .14 21 1.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 5.5   260  
ldv-regression/test03_true-unreach-call_true-termination.c true 2 wit inspect .11 23 1.9 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 7.8   280  
ldv-regression/test04_true-unreach-call_true-termination.c true 2 wit inspect .14 21 1.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 7.1   270  
ldv-regression/test05_true-unreach-call_true-termination.c true 2 wit inspect .15 22 1.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 10     490  
ldv-regression/test07_true-unreach-call_true-termination.c true 2 wit inspect .11 22 1.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  270 true 2 wit inspect 8.4   350  
ldv-regression/test09_true-unreach-call_true-termination.c true 2 wit inspect .14 22 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 8.9   330  
ldv-regression/test10_true-unreach-call_true-termination.c true 2 wit inspect .15 22 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 12     500  
ldv-regression/test11_true-unreach-call_true-termination.c true 2 wit inspect .12 22 1.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 7.6   270  
ldv-regression/test13_true-unreach-call_true-termination.c true 2 wit inspect .15 21 1.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.4   260  
ldv-regression/test14_true-unreach-call_true-termination.c true 2 wit inspect .15 21 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 6.4   260  
ldv-regression/test15_true-unreach-call_true-termination.c true 2 wit inspect .13 27 1.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 7.4   280  
ldv-regression/test16_true-unreach-call_true-termination.c true 2 wit inspect .15 21 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 9.4   290  
ldv-regression/test17_true-unreach-call_true-termination.c true 2 wit inspect .11 22 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 5.4   260  
ldv-regression/test18_true-unreach-call_true-termination.c true 2 wit inspect .15 22 1.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 7.2   300  
ldv-regression/test19_true-unreach-call_true-termination.c true 2 wit inspect .11 28 2.3 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 8.6   350  
ldv-regression/test20_true-unreach-call_true-termination.c true 2 wit inspect .14 24 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 5.6   270  
ldv-regression/test21_true-unreach-call_true-termination.c true 2 wit inspect .15 23 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 7.7   310  
ldv-regression/test22_true-unreach-call.c false(unreach-call) -16 wit inspect .18 24 1.9 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1600 true 2 wit inspect 4.7   230  
ldv-regression/test23_true-unreach-call.c unknown 0 wit inspect .14 22 1.7 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.8
ldv-regression/test24_true-unreach-call_true-termination.c unknown 0 wit inspect .11 22 1.8 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .018 5.0
ldv-regression/test25_true-unreach-call.c unknown 0 wit inspect .21 23 2.1 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .018 4.9
ldv-regression/test26_true-unreach-call_true-termination.c true 2 wit inspect .15 21 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 8.4   300  
ldv-regression/test27_true-unreach-call_true-termination.c unknown 0 wit inspect .17 23 1.9 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .019 4.9
ldv-regression/test28_true-unreach-call_true-termination.c true 2 wit inspect .13 21 1.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 7.4   260  
ldv-regression/test29_true-unreach-call_true-termination.c true 2 wit inspect .15 22 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 6.6   260  
ldv-regression/test30_true-unreach-call_true-termination.c true 2 wit inspect .14 22 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  270 true 2 wit inspect 9.6   460  
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect .54 53 4.6 false(unreach-call) 1 wit inspect 5.6  350 true -32 wit inspect 73     1000   unknown 0 wit inspect 5.0  270 false(unreach-call) 1 wit inspect 1.1    18    - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect .49 52 5.1 true -32 wit inspect 6.1  270 true -32 wit inspect 73     1000   unknown 0 wit inspect 5.1  270 false(unreach-call) 1 wit inspect 1.1    18    - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect .51 51 4.6 false(unreach-call) 1 wit inspect 7.4  350 true -32 wit inspect 66     970   unknown 0 wit inspect 5.4  280 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 unknown 0 wit inspect .64 52 5.6 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .50 41 error (2) 0 wit inspect .047 4.8
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .65 52 6.2 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .018 4.9
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .62 52 6.6 - 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_inl_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .67 52 6.4 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .020 4.8
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .64 53 6.4 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 44 error (2) 0 wit inspect .049 4.8
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .66 52 6.2 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .019 4.9
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .65 52 6.2 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .036 4.9
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .67 54 6.3 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .020 4.9
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .64 52 6.5 - 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
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .68 52 6.2 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .020 5.0
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .18 25 2.2 false(unreach-call) 1 wit inspect 2.8  270 true -32 wit inspect 7.2   300   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .67   18    - wit inspect - wit inspect
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .15 25 1.9 false(unreach-call) 1 wit inspect 2.7  270 false(unreach-call) 1 wit inspect 9.1   360   unknown 0 wit inspect 2.3  210 false(unreach-call) 1 wit inspect .64   19    - wit inspect - wit inspect
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .17 23 1.9 false(unreach-call) 1 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 7.5   280   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .67   18    - wit inspect - wit inspect
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .20 25 2.0 false(unreach-call) 1 wit inspect 3.9  270 false(unreach-call) 1 wit inspect 10     380   unknown 0 wit inspect 3.6  210 true -32 wit inspect .65   18    - wit inspect - wit inspect
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .14 24 1.8 false(unreach-call) 1 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 6.9   280   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .67   18    - wit inspect - wit inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(unreach-call) 1 wit inspect .19 24 2.2 false(unreach-call) 1 wit inspect 2.8  270 true -32 wit inspect 6.2   250   unknown 0 wit inspect 3.3  210 true -32 wit inspect .70   19    - wit inspect - wit inspect
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .16 25 1.9 false(unreach-call) 1 wit inspect 3.5  270 false(unreach-call) 1 wit inspect 7.0   280   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .85 31 11   false(unreach-call) 1 wit inspect 3.0  270 false(unreach-call) 1 wit inspect 9.8   300   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .13 29 2.1 false(unreach-call) 1 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 6.4   280   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .69   18    - wit inspect - wit inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i unknown 0 wit inspect .15 25 2.3 error (invalid witness file) 0 wit inspect .41 42 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0014 .26 - wit inspect - wit inspect
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .19 25 2.1 unknown 0 wit inspect 2.7  270 true -32 wit inspect 6.2   240   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 .13 21 1.9 false(unreach-call) 1 wit inspect 2.8  270 false(unreach-call) 1 wit inspect 9.7   360   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .66   18    - wit inspect - wit inspect
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .16 23 2.0 false(unreach-call) 1 wit inspect 2.7  270 false(unreach-call) 1 wit inspect 7.0   280   unknown 0 wit inspect 3.5  220 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .16 25 2.1 false(unreach-call) 1 wit inspect 2.8  260 false(unreach-call) 1 wit inspect 8.3   340   unknown 0 wit inspect 3.5  210 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 .16 23 1.8 false(unreach-call) 1 wit inspect 2.7  260 false(unreach-call) 1 wit inspect 5.9   270   unknown 0 wit inspect 3.6  210 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .21 24 2.3 false(unreach-call) 1 wit inspect 2.7  270 true -32 wit inspect 5.9   250   unknown 0 wit inspect 3.2  210 true -32 wit inspect .67   18    - wit inspect - wit inspect
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .12 24 2.1 false(unreach-call) 1 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 6.2   280   unknown 0 wit inspect 3.4  210 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 .97 25 11   unknown 0 wit inspect 2.6  270 false(unreach-call) 1 wit inspect 18     560   unknown 0 wit inspect 3.7  210 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .16 23 1.9 false(unreach-call) 1 wit inspect 2.5  270 false(unreach-call) 1 wit inspect 6.4   280   unknown 0 wit inspect 2.3  210 false(unreach-call) 1 wit inspect .66   18    - wit inspect - wit inspect
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    320 9200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .021 4.9
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.3  39 22   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1500 timeout 0 wit inspect 960     1800  
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    820 5300   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.8
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.1  25 20   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1800 timeout 0 wit inspect 960     1200  
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    3500 5500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 44 error (2) 0 wit inspect .018 4.9
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    3500 6500   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .020 4.8
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.2  32 26   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3000 timeout 0 wit inspect 960     1100  
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 3.5  30 26   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3400 timeout 0 wit inspect 960     780  
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.2  37 22   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3900 timeout 0 wit inspect 960     1200  
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 1.8  31 19   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2100 timeout 0 wit inspect 960     720  
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    280 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .018 4.8
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.3  39 26   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5600 timeout 0 wit inspect 960     1100  
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.3  38 24   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2000 timeout 0 wit inspect 960     1200  
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    690 6100   - 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/sll-queue_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.1  25 25   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2500 error (7) 0 wit inspect 160     740  
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    3600 6700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .018 4.9
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    3500 5900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .047 4.8
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.2  29 25   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3600 timeout 0 wit inspect 960     1200  
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 3.7  29 33   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4100 timeout 0 wit inspect 960     940  
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.2  37 24   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4900 timeout 0 wit inspect 960     1300  
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.1  32 23   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2800 timeout 0 wit inspect 960     740  
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .13 24 1.9 false(unreach-call) 1 wit inspect 3.2  270 false(unreach-call) 1 wit inspect 5.9   270   unknown 0 wit inspect 3.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 unknown 0 wit inspect .17 23 2.0 error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0015 .32 - wit inspect - wit inspect
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup_true-termination.i false(unreach-call) 1 wit inspect .13 24 1.8 false(unreach-call) 1 wit inspect 3.1  270 false(unreach-call) 1 wit inspect 5.6   260   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) 1 wit inspect 1.3  25 14   unknown 0 wit inspect 3.2  270 false(unreach-call) 1 wit inspect 14     500   unknown 0 wit inspect 3.6  220 false(unreach-call) 1 wit inspect .66   18    - wit inspect - wit inspect
list-ext2-properties/list_and_tree_cnstr_true-unreach-call_false-termination.i timeout 0 wit inspect 900    1300 5900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .018 5.0
list-ext2-properties/simple_and_skiplist_2lvl_false-unreach-call.i false(unreach-call) 1 wit inspect 2.2  63 25   false(unreach-call) 1 wit inspect 2.7  260 false(unreach-call) 1 wit inspect 6.6   280   unknown 0 wit inspect 3.3  210 true -32 wit inspect .66   18    - wit inspect - wit inspect
list-ext2-properties/simple_and_skiplist_2lvl_true-unreach-call.i timeout 0 wit inspect 900    1600 8400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 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 1.7  24 20   false(unreach-call) 1 wit inspect 5.6  300 timeout 0 wit inspect 96     1200   unknown 0 wit inspect 3.8  220 false(unreach-call) 1 wit inspect .64   19    - wit inspect - wit inspect
list-ext2-properties/simple_search_value_true-unreach-call.i timeout 0 wit inspect 900    1200 9600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .018 4.9
ldv-sets/test_add_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .19 26 1.8 false(unreach-call) 1 wit inspect 2.8  270 false(unreach-call) 1 wit inspect 7.5   270   unknown 0 wit inspect 3.9  210 error (1) 0 wit inspect .61   18    - wit inspect - wit inspect
ldv-sets/test_mutex_double_lock_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect .18 26 2.2 true -32 wit inspect 3.8  260 false(unreach-call) 1 wit inspect 7.9   300   unknown 0 wit inspect 3.4  220 error (1) 0 wit inspect .60   18    - wit inspect - wit inspect
ldv-sets/test_mutex_double_unlock_false-unreach-call.i false(unreach-call) 1 wit inspect .21 25 2.3 true -32 wit inspect 4.0  260 false(unreach-call) 1 wit inspect 9.7   500   unknown 0 wit inspect 3.5  220 error (1) 0 wit inspect .60   19    - wit inspect - wit inspect
ldv-sets/test_mutex_unbounded_false-unreach-call.i false(unreach-call) 1 wit inspect .18 27 2.2 timeout 0 wit inspect 92    2300 false(unreach-call) 1 wit inspect 8.7   420   unknown 0 wit inspect 3.5  210 error (1) 0 wit inspect .61   18    - wit inspect - wit inspect
ldv-sets/test_mutex_unlock_at_exit_false-unreach-call.i false(unreach-call) 1 wit inspect .26 26 2.8 true -32 wit inspect 2.7  260 false(unreach-call) 1 wit inspect 9.2   500   unknown 0 wit inspect 3.5  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 .20 27 2.2 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.4  290 error (7) 0 wit inspect 350     690  
ldv-sets/test_mutex_true-unreach-call.i true 2 wit inspect .32 25 3.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 380    3600 timeout 0 wit inspect 960     1200  
ldv-sets/test_mutex_unbounded_true-unreach-call.i timeout 0 wit inspect 900    4000 7900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .018 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 203 15000    33000 120000   71 -140 290 20000 71 -433 760 23000 71 0 220 14000 71 -503 42 1200 110 114 20000 87000 110 114 22000 48000
    correct results 140 219 81    3700 880   52 52 160 14000 47 47 350 15000 0 41 41 27 760 57 114 600 18000 57 114 1200 19000
        correct true 79 158 58    2100 620   0 0 0 0 57 114 600 18000 57 114 1200 19000
        correct false 61 61 23    1700 260   52 52 160 14000 47 47 350 15000 0 41 41 27 760 0 0
    correct-unconfimed results 3 0 2.7  100 28   0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 3 0 2.7  100 28   0 0 0 0 0 0
    incorrect results 1 -16 .18 24 1.9 6 -192 25 1600 15 -480 300 6400 0 17 -544 11 310 0 0
        incorrect true 0 6 -192 25 1600 15 -480 300 6400 0 17 -544 11 310 0 0
        incorrect false 1 -16 .18 24 1.9 0 0 0 0 0 0
score (181 tasks, max score: 291) 203 -140 -433 0 -503 114 114
Run set predatorhp.sv-comp18 cpa-seq-validate-violation-witnesses-predatorhp.sv-comp18-violation-witness uautomizer-validate-violation-witnesses-predatorhp.sv-comp18-violation-witness cpa-witness2test-validate-violation-witnesses-predatorhp.sv-comp18-violation-witness fshell-witness2test-validate-violation-witnesses-predatorhp.sv-comp18-violation-witness cpa-seq-validate-correctness-witnesses-predatorhp.sv-comp18-correctness-witness uautomizer-validate-correctness-witnesses-predatorhp.sv-comp18-correctness-witness