Tool ULTIMATE Kojak 0.1.23-3204b741 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-02 02:33:02 CET 2017-12-03 03:22:18 CET 2017-12-03 03:55:21 CET 2017-12-03 04:22:06 CET 2017-12-03 04:36:43 CET 2017-12-03 00:36:56 CET 2017-12-03 03:32:10 CET
Run set ukojak.sv-comp18.ReachSafety-Heap cpa-seq-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-Heap uautomizer-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.ReachSafety-Heap uautomizer-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.ReachSafety-Heap
Options --full-output -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-02_0233.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/ukojak.2017-12-02_0233.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-02_0233.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/ukojak.2017-12-02_0233.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/ukojak.2017-12-02_0233.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/ukojak.2017-12-02_0233.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 timeout 0 wit inspect 900   1800 13000 error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .95 49 error (invalid witness file) 0 wit inspect .0017 .29 - wit inspect - wit inspect
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   2100 10000 error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .049 5.0 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0015 .34 - wit inspect - wit inspect
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 13   540 110 true -32 wit inspect 3.9  260 false(unreach-call) 1 wit inspect 7.5   320   unknown 0 wit inspect 4.5  220 true -32 wit inspect .88   18    - wit inspect - wit inspect
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   2200 11000 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .022 4.9 error (invalid witness file) 0 wit inspect .65 51 error (invalid witness file) 0 wit inspect .0015 .26 - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 18   690 180 false(unreach-call) 1 wit inspect 4.0  280 false(unreach-call) 1 wit inspect 11     340   unknown 0 wit inspect 3.5  210 true -32 wit inspect .70   18    - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 21   730 190 false(unreach-call) 1 wit inspect 4.0  270 false(unreach-call) 1 wit inspect 4.9   310   unknown 0 wit inspect 4.1  220 true -32 wit inspect .86   19    - wit inspect - wit inspect
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   1900 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .019 4.9
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   1700 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .019 4.8
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   1900 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 41 error (2) 0 wit inspect .018 4.9
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   1600 12000 - 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
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   2200 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .022 4.8
heap-manipulation/tree_true-unreach-call.i timeout 0 wit inspect 900   2700 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .020 5.0
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 6.8 350 49 true -32 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 6.0   270   unknown 0 wit inspect 4.2  220 true -32 wit inspect .63   18    - wit inspect - wit inspect
list-properties/list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 18   690 170 false(unreach-call) 1 wit inspect 4.4  270 false(unreach-call) 1 wit inspect 6.1   280   unknown 0 wit inspect 3.8  210 true -32 wit inspect .65   19    - wit inspect - wit inspect
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 6.6 350 59 true -32 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 5.5   260   unknown 0 wit inspect 3.9  230 false(unreach-call) 1 wit inspect .73   18    - wit inspect - wit inspect
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   1800 9700 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0014 .27 - wit inspect - wit inspect
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 6.1 310 49 true -32 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 5.3   260   unknown 0 wit inspect 3.2  210 true -32 wit inspect .77   19    - wit inspect - wit inspect
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 7.3 360 52 false(unreach-call) 1 wit inspect 4.4  270 false(unreach-call) 1 wit inspect 6.7   270   unknown 0 wit inspect 3.3  220 true -32 wit inspect .77   19    - wit inspect - wit inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   3400 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 46 error (2) 0 wit inspect .019 4.8
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   1800 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 4.9
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   1600 9300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .019 4.8
list-properties/list_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   1800 11000 - 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
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   10000 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .018 4.8
list-properties/simple_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   2600 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 45 error (2) 0 wit inspect .019 4.8
list-properties/splice_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   1500 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 41 error (2) 0 wit inspect .019 5.0
ldv-regression/1_3_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 5.5 300 46 true -32 wit inspect 3.1  250 false(unreach-call) 1 wit inspect 5.9   260   unknown 0 wit inspect 3.0  190 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
ldv-regression/alt_test_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 6.5 320 58 false(unreach-call) 1 wit inspect 4.0  270 false(unreach-call) 1 wit inspect 6.8   280   unknown 0 wit inspect 4.6  220 false(unreach-call) 1 wit inspect .68   18    - wit inspect - wit inspect
ldv-regression/callfpointer_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 4.2 250 37 true -32 wit inspect 3.0  250 false(unreach-call) 1 wit inspect 5.4   230   unknown 0 wit inspect 3.4  180 false(unreach-call) 1 wit inspect .76   18    - wit inspect - wit inspect
ldv-regression/fo_test_true-termination.c_false-unreach-call.i unknown 0 wit inspect 10   270 81 error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0015 .34 - wit inspect - wit inspect
ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 5.3 290 37 true -32 wit inspect 3.2  250 false(unreach-call) 1 wit inspect 5.3   270   unknown 0 wit inspect 3.0  190 false(unreach-call) 1 wit inspect .62   18    - wit inspect - wit inspect
ldv-regression/mutex_lock_struct_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 5.2 290 39 true -32 wit inspect 2.9  260 false(unreach-call) 1 wit inspect 5.0   250   unknown 0 wit inspect 2.8  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) 1 wit inspect 5.5 290 48 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 6.9   270   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .72   19    - wit inspect - wit inspect
ldv-regression/rule57_ebda_blast_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 6.0 310 42 true -32 wit inspect 3.9  260 false(unreach-call) 1 wit inspect 6.3   280   unknown 0 wit inspect 2.8  180 error (2) 0 wit inspect .66   19    - wit inspect - wit inspect
ldv-regression/rule60_list2_true-termination.c_false-unreach-call_1.i timeout 0 wit inspect 900   1500 11000 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .91 50 error (invalid witness file) 0 wit inspect .0013 .28 - wit inspect - wit inspect
ldv-regression/stateful_check_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect 8.9 490 63 false(unreach-call) 1 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 7.1   290   unknown 0 wit inspect 3.6  220 true -32 wit inspect .69   19    - wit inspect - wit inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 5.2 290 48 false(unreach-call) 1 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 6.2   240   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .79   18    - wit inspect - wit inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect 4.8 260 41 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 5.9   240   unknown 0 wit inspect 3.4  180 false(unreach-call) 1 wit inspect .62   18    - wit inspect - wit inspect
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call.i true 2 wit inspect 4.7 260 44 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 6.3   290  
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i true 2 wit inspect 4.4 260 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 5.3   270  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call.i true 2 wit inspect 4.5 250 42 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 5.8   270  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call_1.i true 2 wit inspect 4.4 250 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  240 true 2 wit inspect 5.7   260  
ldv-regression/ex3_forlist_true-termination.c_true-unreach-call.i timeout 0 wit inspect 900   1700 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 4.9
ldv-regression/just_assert_true-termination.c_true-unreach-call.i true 2 wit inspect 4.1 250 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.8  240 true 2 wit inspect 4.2   220  
ldv-regression/mutex_lock_int_true-termination.c_true-unreach-call_1.i true 2 wit inspect 4.9 260 42 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 6.6   260  
ldv-regression/mutex_lock_struct_true-termination.c_true-unreach-call_1.i true 2 wit inspect 5.1 270 42 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 7.3   280  
ldv-regression/nested_structure_noptr_true-termination.c_true-unreach-call.i true 2 wit inspect 4.4 250 34 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 4.6   240  
ldv-regression/nested_structure_noptr_true-unreach-call_true-termination.i true 2 wit inspect 4.2 250 33 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 5.6   260  
ldv-regression/nested_structure_ptr_true-termination.c_true-unreach-call.i true 2 wit inspect 6.2 330 53 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 9.9   480  
ldv-regression/nested_structure_ptr_true-unreach-call_true-termination.i true 2 wit inspect 6.1 320 47 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 11     420  
ldv-regression/nested_structure_true-termination.c_true-unreach-call.i true 2 wit inspect 5.5 280 42 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 8.9   290  
ldv-regression/nested_structure_true-unreach-call_true-termination.i true 2 wit inspect 5.2 280 46 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 7.5   280  
ldv-regression/oomInt_true-termination.c_true-unreach-call.i true 2 wit inspect 4.2 250 34 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 5.9   260  
ldv-regression/oomInt_true-termination.c_true-unreach-call_1.i true 2 wit inspect 4.2 240 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 5.2   260  
ldv-regression/rule57_ebda_blast_true-termination.c_true-unreach-call_1.i timeout 0 wit inspect 900   1300 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .020 4.8
ldv-regression/rule60_list2_true-termination.c_true-unreach-call.i timeout 0 wit inspect 900   1600 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .019 5.0
ldv-regression/rule60_list_true-termination.c_true-unreach-call.i true 2 wit inspect 7.6 430 60 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  260 true 2 wit inspect 9.6   380  
ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i true 2 wit inspect 4.5 260 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  250 true 2 wit inspect 3.7   270  
ldv-regression/structure_assignment_true-termination.c_true-unreach-call.i true 2 wit inspect 4.3 250 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 5.7   250  
ldv-regression/test_address_true-termination.c_true-unreach-call.i true 2 wit inspect 4.7 280 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 5.5   260  
ldv-regression/test_cut_trace_true-termination.c_true-unreach-call.i true 2 wit inspect 4.4 260 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 6.0   260  
ldv-regression/test_malloc-1_true-unreach-call_true-termination.i true 2 wit inspect 4.8 280 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 6.3   270  
ldv-regression/test_malloc-2_true-unreach-call_true-termination.i true 2 wit inspect 4.8 290 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  260 true 2 wit inspect 5.9   270  
ldv-regression/test_overflow_true-termination.c_true-unreach-call.i true 2 wit inspect 5.1 280 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  250 true 2 wit inspect 5.0   260  
ldv-regression/test_union_cast-1_true-unreach-call_true-termination.i true 2 wit inspect 4.6 250 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 5.1   260  
ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i true 2 wit inspect 4.5 260 41 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.3  260 true 2 wit inspect 5.2   260  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call.i true 2 wit inspect 4.7 260 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.2  250 true 2 wit inspect 4.8   260  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call_1.i true 2 wit inspect 4.3 250 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 4.9   260  
ldv-regression/test_union_true-termination.c_true-unreach-call.i true 2 wit inspect 4.6 260 35 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 4.8   260  
ldv-regression/test_union_true-termination.c_true-unreach-call_1.i true 2 wit inspect 4.4 250 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 5.4   260  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call.i true 2 wit inspect 4.4 250 41 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.9   270  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i true 2 wit inspect 4.5 250 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 6.3   270  
ldv-regression/test02_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.6 250 32 true -32 wit inspect 3.2  270 false(unreach-call) 1 wit inspect 4.9   230   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) 1 wit inspect 6.6 320 58 false(unreach-call) 1 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 5.4   280   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
ldv-regression/test08_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 5.0 260 36 false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 3.6   270   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/test12_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.3 260 36 false(unreach-call) 1 wit inspect 3.3  280 false(unreach-call) 1 wit inspect 6.3   240   unknown 0 wit inspect 3.2  180 false(unreach-call) 1 wit inspect .64   18    - wit inspect - wit inspect
ldv-regression/test21_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 5.6 290 48 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 6.0   270   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .78   18    - wit inspect - wit inspect
ldv-regression/test22_false-unreach-call.c false(unreach-call) 1 wit inspect 6.1 320 44 false(unreach-call) 1 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 7.3   450   unknown 0 wit inspect 3.8  210 true -32 wit inspect .78   18    - wit inspect - wit inspect
ldv-regression/test23_false-unreach-call.c false(unreach-call) 1 wit inspect 54   1300 610 false(unreach-call) 1 wit inspect 3.8  270 timeout 0 wit inspect 97     5400   unknown 0 wit inspect 3.6  210 true -32 wit inspect .72   19    - wit inspect - wit inspect
ldv-regression/test24_false-unreach-call.c false(unreach-call) 0 wit inspect 24   570 220 true -32 wit inspect 3.3  260 out of memory 0 wit inspect 66     7000   unknown 0 wit inspect 3.8  180 true -32 wit inspect .75   19    - wit inspect - wit inspect
ldv-regression/test25_false-unreach-call_true-termination.c error (7) 0 wit inspect 140   1400 1600 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .022 5.0 error (invalid witness file) 0 wit inspect .97 49 error (invalid witness file) 0 wit inspect .0017 .29 - wit inspect - wit inspect
ldv-regression/test26_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 4.6 260 44 true -32 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 6.6   280   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .68   18    - wit inspect - wit inspect
ldv-regression/test27_false-unreach-call_true-termination.c error (7) 0 wit inspect 45   680 430 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect 1.1  47 error (invalid witness file) 0 wit inspect .0020 .26 - wit inspect - wit inspect
ldv-regression/test28_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 5.0 270 43 false(unreach-call) 1 wit inspect 2.1  260 false(unreach-call) 1 wit inspect 5.2   270   unknown 0 wit inspect 3.2  180 false(unreach-call) 1 wit inspect .76   18    - wit inspect - wit inspect
ldv-regression/test29_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 5.2 270 40 false(unreach-call) 1 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 7.2   260   unknown 0 wit inspect 2.0  180 false(unreach-call) 1 wit inspect .74   18    - wit inspect - wit inspect
ldv-regression/test30_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 5.5 280 46 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 6.8   270   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
ldv-regression/test01_true-unreach-call_true-termination.c true 2 wit inspect 4.6 250 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 5.6   270  
ldv-regression/test03_true-unreach-call_true-termination.c true 2 wit inspect 4.6 260 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 6.6   290  
ldv-regression/test04_true-unreach-call_true-termination.c true 2 wit inspect 4.8 260 42 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 6.9   270  
ldv-regression/test05_true-unreach-call_true-termination.c true 2 wit inspect 7.0 380 55 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 9.8   450  
ldv-regression/test07_true-unreach-call_true-termination.c true 2 wit inspect 5.0 280 47 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 8.7   350  
ldv-regression/test09_true-unreach-call_true-termination.c true 2 wit inspect 5.3 290 42 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 8.5   340  
ldv-regression/test10_true-unreach-call_true-termination.c true 2 wit inspect 8.6 400 71 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 12     480  
ldv-regression/test11_true-unreach-call_true-termination.c true 2 wit inspect 5.7 330 51 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  260 true 2 wit inspect 7.9   280  
ldv-regression/test13_true-unreach-call_true-termination.c true 2 wit inspect 5.0 260 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 5.1   260  
ldv-regression/test14_true-unreach-call_true-termination.c true 2 wit inspect 5.5 290 44 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 6.9   260  
ldv-regression/test15_true-unreach-call_true-termination.c true 2 wit inspect 7.1 350 54 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.2  250 true 2 wit inspect 7.6   290  
ldv-regression/test16_true-unreach-call_true-termination.c true 2 wit inspect 4.9 260 45 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 7.6   290  
ldv-regression/test17_true-unreach-call_true-termination.c true 2 wit inspect 4.3 260 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 4.9   250  
ldv-regression/test18_true-unreach-call_true-termination.c true 2 wit inspect 6.2 320 49 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 8.3   300  
ldv-regression/test19_true-unreach-call_true-termination.c true 2 wit inspect 6.0 320 47 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 9.7   340  
ldv-regression/test20_true-unreach-call_true-termination.c true 2 wit inspect 4.4 260 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 5.4   260  
ldv-regression/test21_true-unreach-call_true-termination.c true 2 wit inspect 5.1 290 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 5.8   310  
ldv-regression/test22_true-unreach-call.c true 2 wit inspect 25   800 280 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.1  290 true 2 wit inspect 21     510  
ldv-regression/test23_true-unreach-call.c true 2 wit inspect 49   2100 490 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.9  300 true 2 wit inspect 220     750  
ldv-regression/test24_true-unreach-call_true-termination.c true 2 wit inspect 22   740 230 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.6  280 true 2 wit inspect 10     420  
ldv-regression/test25_true-unreach-call.c true 2 wit inspect 160   2000 2100 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 15    470 true 2 wit inspect 29     490  
ldv-regression/test26_true-unreach-call_true-termination.c true 2 wit inspect 4.9 280 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 7.3   300  
ldv-regression/test27_true-unreach-call_true-termination.c true 2 wit inspect 170   2800 1700 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 31    410 true 2 wit inspect 170     800  
ldv-regression/test28_true-unreach-call_true-termination.c true 2 wit inspect 5.2 260 42 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 7.1   270  
ldv-regression/test29_true-unreach-call_true-termination.c true 2 wit inspect 4.9 260 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 7.0   260  
ldv-regression/test30_true-unreach-call_true-termination.c true 2 wit inspect 5.7 300 47 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 9.8   460  
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i error (7) 0 wit inspect 610   1800 6300 error (invalid witness file) 0 wit inspect .52 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0017 .29 - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i error (7) 0 wit inspect 650   1700 6800 error (invalid witness file) 0 wit inspect .40 45 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0016 .27 - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i error (7) 0 wit inspect 670   1700 7300 error (invalid witness file) 0 wit inspect .52 42 error (2) 0 wit inspect .021 5.0 error (invalid witness file) 0 wit inspect 1.2  49 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 150   820 1700 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.1  280 true 2 wit inspect 13     460  
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 130   870 1400 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.4  290 true 2 wit inspect 13     450  
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 140   840 1600 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  290 true 2 wit inspect 12     430  
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 140   880 1500 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.9  280 true 2 wit inspect 13     440  
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 130   850 1300 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.7  280 true 2 wit inspect 12     450  
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 140   850 1600 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.0  290 true 2 wit inspect 13     450  
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 150   880 1600 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.8  280 true 2 wit inspect 12     450  
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 150   840 1700 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.1  290 true 2 wit inspect 12     460  
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 140   790 1700 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.7  280 true 2 wit inspect 13     450  
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 120   860 1200 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.8  290 true 2 wit inspect 12     430  
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 13   600 110 false(unreach-call) 1 wit inspect 4.1  270 false(unreach-call) 1 wit inspect 9.8   350   unknown 0 wit inspect 4.2  210 false(unreach-call) 1 wit inspect .77   18    - wit inspect - wit inspect
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 7.8 330 55 false(unreach-call) 1 wit inspect 4.0  270 false(unreach-call) 1 wit inspect 12     360   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .77   18    - wit inspect - wit inspect
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 8.4 400 63 false(unreach-call) 1 wit inspect 3.8  260 false(unreach-call) 1 wit inspect 6.1   280   unknown 0 wit inspect 3.6  210 false(unreach-call) 1 wit inspect .69   19    - wit inspect - wit inspect
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   1300 12000 error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0015 .30 - wit inspect - wit inspect
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 14   680 130 false(unreach-call) 1 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 6.4   290   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .77   18    - wit inspect - wit inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(unreach-call) 1 wit inspect 48   850 490 false(unreach-call) 1 wit inspect 4.8  270 false(unreach-call) 1 wit inspect 6.8   300   unknown 0 wit inspect 3.4  210 true -32 wit inspect .67   19    - wit inspect - wit inspect
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 6.7 340 57 true -32 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 6.2   280   unknown 0 wit inspect 4.0  210 false(unreach-call) 1 wit inspect .82   18    - wit inspect - wit inspect
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 8.3 400 68 false(unreach-call) 1 wit inspect 4.2  270 false(unreach-call) 1 wit inspect 10     300   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .85   18    - wit inspect - wit inspect
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 9.4 420 68 false(unreach-call) 1 wit inspect 3.8  260 false(unreach-call) 1 wit inspect 7.7   280   unknown 0 wit inspect 4.2  210 false(unreach-call) 1 wit inspect .71   18    - wit inspect - wit inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 24   780 250 false(unreach-call) 1 wit inspect 3.8  260 false(unreach-call) 1 wit inspect 11     350   unknown 0 wit inspect 4.5  210 error (2) 0 wit inspect .88   19    - wit inspect - wit inspect
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 22   740 240 false(unreach-call) 1 wit inspect 3.7  270 false(unreach-call) 1 wit inspect 7.8   290   unknown 0 wit inspect 3.8  210 true -32 wit inspect .65   19    - wit inspect - wit inspect
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 7.1 360 65 false(unreach-call) 1 wit inspect 3.9  270 false(unreach-call) 1 wit inspect 12     380   unknown 0 wit inspect 4.0  210 false(unreach-call) 1 wit inspect .75   19    - wit inspect - wit inspect
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 7.6 370 69 false(unreach-call) 1 wit inspect 4.5  260 false(unreach-call) 1 wit inspect 6.0   280   unknown 0 wit inspect 3.8  210 false(unreach-call) 1 wit inspect .83   18    - wit inspect - wit inspect
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 64   1400 760 false(unreach-call) 1 wit inspect 4.2  270 false(unreach-call) 1 wit inspect 9.0   340   unknown 0 wit inspect 3.5  210 true -32 wit inspect .68   19    - wit inspect - wit inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 11   500 90 false(unreach-call) 1 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 6.6   290   unknown 0 wit inspect 3.9  210 false(unreach-call) 1 wit inspect .86   18    - wit inspect - wit inspect
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 28   820 270 false(unreach-call) 1 wit inspect 3.9  270 false(unreach-call) 1 wit inspect 8.1   290   unknown 0 wit inspect 4.0  210 true -32 wit inspect .86   19    - wit inspect - wit inspect
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 6.3 320 49 true -32 wit inspect 3.9  260 false(unreach-call) 1 wit inspect 8.0   280   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .77   18    - wit inspect - wit inspect
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 510   1500 7000 unknown 0 wit inspect 4.3  280 false(unreach-call) 1 wit inspect 14     520   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .75   19    - wit inspect - wit inspect
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 6.4 340 49 false(unreach-call) 1 wit inspect 3.8  260 false(unreach-call) 1 wit inspect 6.3   280   unknown 0 wit inspect 4.4  210 false(unreach-call) 1 wit inspect .84   18    - wit inspect - wit inspect
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   11000 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 4.8
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   1400 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .019 5.0
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   12000 8200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 41 error (2) 0 wit inspect .018 4.8
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   1400 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .019 4.9
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   3700 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .019 4.9
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   2600 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .021 5.0
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   1200 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 43 error (2) 0 wit inspect .019 4.8
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   1400 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .024 4.8
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   1500 9000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 45 error (2) 0 wit inspect .020 5.0
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   1800 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 4.9
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   5800 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 44 error (2) 0 wit inspect .020 4.9
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i error (7) 0 wit inspect 260   1100 3200 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 45 error (2) 0 wit inspect .017 4.9
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   1200 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 46 error (2) 0 wit inspect .018 4.8
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   13000 7900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .41 46 error (2) 0 wit inspect .019 4.8
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   1900 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .77 43 error (2) 0 wit inspect .018 4.8
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i error (7) 0 wit inspect 580   2000 6800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 43 error (2) 0 wit inspect .018 4.8
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   980 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .71 44 error (2) 0 wit inspect .021 4.9
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   2100 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 44 error (2) 0 wit inspect .028 4.9
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   1500 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 46 error (2) 0 wit inspect .019 4.9
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   2000 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .018 4.8
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   2300 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 41 error (2) 0 wit inspect .019 4.8
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 5.9 320 53 false(unreach-call) 1 wit inspect 4.6  270 false(unreach-call) 1 wit inspect 7.1   270   unknown 0 wit inspect 4.3  210 false(unreach-call) 1 wit inspect .77   18    - wit inspect - wit inspect
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i timeout 0 wit inspect 900   1700 13000 error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect 1.1  47 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup_true-termination.i false(unreach-call) 1 wit inspect 5.6 290 47 timeout 0 wit inspect 91    2000 false(unreach-call) 1 wit inspect 5.4   260   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .71   18    - wit inspect - wit inspect
list-ext2-properties/list_and_tree_cnstr_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect 25   760 230 unknown 0 wit inspect 4.1  270 false(unreach-call) 1 wit inspect 7.4   300   unknown 0 wit inspect 4.3  220 false(unreach-call) 1 wit inspect .82   19    - wit inspect - wit inspect
list-ext2-properties/list_and_tree_cnstr_true-unreach-call_false-termination.i timeout 0 wit inspect 900   1500 14000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 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 7.9 390 66 true -32 wit inspect 4.1  260 false(unreach-call) 1 wit inspect 7.6   280   unknown 0 wit inspect 4.2  210 true -32 wit inspect .78   18    - wit inspect - wit inspect
list-ext2-properties/simple_and_skiplist_2lvl_true-unreach-call.i timeout 0 wit inspect 900   2400 13000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .020 4.9
list-ext2-properties/simple_search_value_false-unreach-call.i timeout 0 wit inspect 900   13000 10000 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .82 47 error (invalid witness file) 0 wit inspect .0018 .26 - wit inspect - wit inspect
list-ext2-properties/simple_search_value_true-unreach-call.i timeout 0 wit inspect 900   4700 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 42 error (2) 0 wit inspect .041 4.9
ldv-sets/test_add_false-unreach-call_true-termination.i timeout 0 wit inspect 900   1600 11000 error (invalid witness file) 0 wit inspect .54 45 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .89 49 error (invalid witness file) 0 wit inspect .0013 .34 - wit inspect - wit inspect
ldv-sets/test_mutex_double_lock_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 12   540 110 true -32 wit inspect 4.4  260 false(unreach-call) 1 wit inspect 7.6   310   unknown 0 wit inspect 4.6  220 error (1) 0 wit inspect .73   19    - wit inspect - wit inspect
ldv-sets/test_mutex_double_unlock_false-unreach-call.i timeout 0 wit inspect 900   2000 12000 error (invalid witness file) 0 wit inspect .50 43 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect 1.1  50 error (invalid witness file) 0 wit inspect .0016 .32 - wit inspect - wit inspect
ldv-sets/test_mutex_unbounded_false-unreach-call.i timeout 0 wit inspect 900   1500 10000 error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .025 4.8 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0011 .29 - wit inspect - wit inspect
ldv-sets/test_mutex_unlock_at_exit_false-unreach-call.i timeout 0 wit inspect 900   2000 14000 error (invalid witness file) 0 wit inspect .39 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
ldv-sets/test_add_true-unreach-call_true-termination.i timeout 0 wit inspect 900   1700 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .019 4.8
ldv-sets/test_mutex_true-unreach-call.i timeout 0 wit inspect 900   2400 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 41 error (2) 0 wit inspect .018 5.0
ldv-sets/test_mutex_unbounded_true-unreach-call.i timeout 0 wit inspect 900   1600 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .72 45 error (2) 0 wit inspect .018 4.8
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
total 181 186 54000 220000 690000 71 -478 290 16000 71 51 530 27000 71 0 210 12000 71 -478 39 980 110 134 360 19000 110 134 920 23000
    correct results 119 186 3200 56000 35000 34 34 130 9000 51 51 360 15000 0 34 34 25 620 67 134 330 18000 67 134 920 23000
        correct true 67 134 2100 31000 22000 0 0 0 0 67 134 330 18000 67 134 920 23000
        correct false 52 52 1100 25000 13000 34 34 130 9000 51 51 360 15000 0 34 34 25 620 0 0
    correct-unconfimed results 1 0 24 570 220 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 1 0 24 570 220 0 0 0 0 0 0
    incorrect results 0 16 -512 57 4100 0 0 16 -512 12 300 0 0
        incorrect true 0 16 -512 57 4100 0 0 16 -512 12 300 0 0
        incorrect false 0 0 0 0 0 0 0
score (181 tasks, max score: 291) 186 -478 51 0 -478 134 134
Run set ukojak.sv-comp18.ReachSafety-Heap cpa-seq-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-Heap uautomizer-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-ukojak.sv-comp18-violation-witness.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.ReachSafety-Heap uautomizer-validate-correctness-witnesses-ukojak.sv-comp18-correctness-witness.ReachSafety-Heap