Tool VeriAbs 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* [apollon020; apollon077; apollon078; apollon084; apollon149; apollon164] apollon* [apollon037; apollon065; apollon077; apollon078; apollon155; apollon159] apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-02 18:04:04 CET 2017-12-03 04:46:33 CET 2017-12-03 06:08:30 CET 2017-12-03 06:21:09 CET 2017-12-03 06:27:12 CET 2017-12-03 03:55:53 CET 2017-12-03 04:55:47 CET
Run set veriabs.sv-comp18.ReachSafety-Heap cpa-seq-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Heap uautomizer-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-veriabs.sv-comp18-correctness-witness.ReachSafety-Heap uautomizer-validate-correctness-witnesses-veriabs.sv-comp18-correctness-witness.ReachSafety-Heap
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/veriabs.2017-12-02_1804.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/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/veriabs.2017-12-02_1804.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/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/veriabs.2017-12-02_1804.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 unknown 0 wit inspect 180   1500 2100 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .67 51 error (invalid witness file) 0 wit inspect .0030 .26 - wit inspect - wit inspect
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 750   880 8800 error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0015 .31 - wit inspect - wit inspect
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 340   550 4000 error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .69 49 error (invalid witness file) 0 wit inspect .0046 .32 - wit inspect - wit inspect
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 800   870 8600 error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .69 49 error (invalid witness file) 0 wit inspect .0011 .30 - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-deref.i unknown 0 wit inspect 750   570 8000 error (invalid witness file) 0 wit inspect .44 42 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 640   570 7700 error (invalid witness file) 0 wit inspect .43 40 error (2) 0 wit inspect .017 4.9 error (invalid witness file) 0 wit inspect .66 50 error (invalid witness file) 0 wit inspect .0012 .26 - wit inspect - wit inspect
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 180   1500 2000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 45 error (2) 0 wit inspect .018 4.8
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   2700 12000 - 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
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 730   880 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .024 4.8
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 340   540 4300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 42 error (2) 0 wit inspect .024 4.8
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 790   850 9000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .76 43 error (2) 0 wit inspect .022 4.8
heap-manipulation/tree_true-unreach-call.i unknown 0 wit inspect 700   570 8400 - 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
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   3600 10000 error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .86 50 error (invalid witness file) 0 wit inspect .0034 .26 - wit inspect - wit inspect
list-properties/list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 450   2800 5500 true -32 wit inspect 4.4  260 false(unreach-call) 1 wit inspect 8.6   510   unknown 0 wit inspect 3.1  260 false(unreach-call) 1 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 22   300 210 true -32 wit inspect 3.6  250 false(unreach-call) 1 wit inspect 5.5   270   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .64   19    - wit inspect - wit inspect
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 740   3700 5600 error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .021 4.8 error (invalid witness file) 0 wit inspect .85 50 error (invalid witness file) 0 wit inspect .0017 .29 - wit inspect - wit inspect
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 23   290 200 true -32 wit inspect 4.0  250 false(unreach-call) 1 wit inspect 6.2   260   unknown 0 wit inspect 3.5  250 false(unreach-call) 1 wit inspect .69   19    - wit inspect - wit inspect
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 43   300 380 true -32 wit inspect 2.8  250 false(unreach-call) 1 wit inspect 4.0   280   unknown 0 wit inspect 2.6  250 false(unreach-call) 1 wit inspect .65   19    - wit inspect - wit inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   4000 9300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .62 43 error (2) 0 wit inspect .019 4.9
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   2600 8500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .022 4.9
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i true 2 wit inspect 42   660 320 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 25    620 true 2 wit inspect 70     1100  
list-properties/list_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 630   270 7100 - 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
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   4500 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 43 error (2) 0 wit inspect .019 4.9
list-properties/simple_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   4200 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .018 4.8
list-properties/splice_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   1600 9300 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .018 4.8
ldv-regression/1_3_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 10   280 82 false(unreach-call) 1 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 5.2   250   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/alt_test_true-termination.c_false-unreach-call.i unknown 0 wit inspect 22   250 170 error (invalid witness file) 0 wit inspect .56 42 error (2) 0 wit inspect .021 5.0 error (invalid witness file) 0 wit inspect .86 49 error (invalid witness file) 0 wit inspect .0012 .29 - wit inspect - wit inspect
ldv-regression/callfpointer_true-termination.c_false-unreach-call.i true -32 wit inspect 6.3 290 46 false(unreach-call) 1 wit inspect 4.2  260 false(unreach-call) 1 wit inspect 4.5   220   unknown 0 wit inspect .94 52 error (1) 0 wit inspect .091  9.0  - wit inspect - wit inspect
ldv-regression/fo_test_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 22   280 170 true -32 wit inspect 4.2  250 unknown 0 wit inspect 11     280   unknown 0 wit inspect 2.5  250 false(unreach-call) 1 wit inspect .64   18    - wit inspect - wit inspect
ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 9.0 280 85 false(unreach-call) 1 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 4.6   250   unknown 0 wit inspect 2.0  210 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 9.1 280 74 false(unreach-call) 1 wit inspect 2.3  260 false(unreach-call) 1 wit inspect 7.4   260   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
ldv-regression/recursive_list_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 10   280 85 false(unreach-call) 1 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 5.4   260   unknown 0 wit inspect 2.7  190 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/rule57_ebda_blast_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 11   280 88 false(unreach-call) 1 wit inspect 2.4  260 false(unreach-call) 1 wit inspect 6.4   270   unknown 0 wit inspect 2.1  210 error (2) 0 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/rule60_list2_true-termination.c_false-unreach-call_1.i unknown 0 wit inspect 23   250 150 error (invalid witness file) 0 wit inspect .51 42 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .65 50 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
ldv-regression/stateful_check_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect 19   290 150 true -32 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 6.3   300   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .63   19    - wit inspect - wit inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 15   280 110 false(unreach-call) 1 wit inspect 2.3  260 false(unreach-call) 1 wit inspect 5.4   250   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .68   19    - wit inspect - wit inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect 14   280 130 false(unreach-call) 1 wit inspect 2.2  260 false(unreach-call) 1 wit inspect 4.8   240   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .72   18    - wit inspect - wit inspect
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call.i true 2 wit inspect 9.2 280 90 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 6.1   280  
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i true 2 wit inspect 8.1 270 73 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 3.7   260  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call.i true 2 wit inspect 9.1 260 71 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  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 7.8 270 68 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 5.4   260  
ldv-regression/ex3_forlist_true-termination.c_true-unreach-call.i true 2 wit inspect 31   600 260 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 28    510 true 2 wit inspect 42     740  
ldv-regression/just_assert_true-termination.c_true-unreach-call.i true 2 wit inspect 7.8 280 68 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 4.5   220  
ldv-regression/mutex_lock_int_true-termination.c_true-unreach-call_1.i true 2 wit inspect 9.6 270 76 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 6.4   260  
ldv-regression/mutex_lock_struct_true-termination.c_true-unreach-call_1.i true 2 wit inspect 9.8 280 82 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 7.3   260  
ldv-regression/nested_structure_noptr_true-termination.c_true-unreach-call.i true 2 wit inspect 7.9 270 79 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 4.6   240  
ldv-regression/nested_structure_noptr_true-unreach-call_true-termination.i true 2 wit inspect 7.8 270 74 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  260 true 2 wit inspect 5.2   260  
ldv-regression/nested_structure_ptr_true-termination.c_true-unreach-call.i true 2 wit inspect 10   280 74 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 11     460  
ldv-regression/nested_structure_ptr_true-unreach-call_true-termination.i true 2 wit inspect 9.5 260 79 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 11     400  
ldv-regression/nested_structure_true-termination.c_true-unreach-call.i true 2 wit inspect 9.7 260 91 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 5.2   280  
ldv-regression/nested_structure_true-unreach-call_true-termination.i true 2 wit inspect 9.8 260 78 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 8.6   290  
ldv-regression/oomInt_true-termination.c_true-unreach-call.i true 2 wit inspect 8.5 270 77 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 5.5   260  
ldv-regression/oomInt_true-termination.c_true-unreach-call_1.i true 2 wit inspect 9.0 270 71 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 5.2   260  
ldv-regression/rule57_ebda_blast_true-termination.c_true-unreach-call_1.i true 2 wit inspect 12   280 94 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  260 true 2 wit inspect 7.9   270  
ldv-regression/rule60_list2_true-termination.c_true-unreach-call.i unknown 0 wit inspect 22   250 160 - 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/rule60_list_true-termination.c_true-unreach-call.i true 2 wit inspect 20   290 160 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  250 true 2 wit inspect 9.6   380  
ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i true 2 wit inspect 20   270 150 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.5  250 true 2 wit inspect 5.3   260  
ldv-regression/structure_assignment_true-termination.c_true-unreach-call.i true 2 wit inspect 7.9 270 68 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 5.0   260  
ldv-regression/test_address_true-termination.c_true-unreach-call.i true 2 wit inspect 19   270 150 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 5.6   270  
ldv-regression/test_cut_trace_true-termination.c_true-unreach-call.i true 2 wit inspect 7.9 260 67 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 5.3   260  
ldv-regression/test_malloc-1_true-unreach-call_true-termination.i true 2 wit inspect 20   280 170 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 4.4   280  
ldv-regression/test_malloc-2_true-unreach-call_true-termination.i true 2 wit inspect 19   280 150 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 5.8   260  
ldv-regression/test_overflow_true-termination.c_true-unreach-call.i true 2 wit inspect 18   280 130 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  260 true 2 wit inspect 5.5   270  
ldv-regression/test_union_cast-1_true-unreach-call_true-termination.i true 2 wit inspect 7.8 280 65 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 6.8   260  
ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i true 2 wit inspect 9.6 270 81 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 3.9   260  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call.i true 2 wit inspect 9.2 270 82 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.3   260  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call_1.i true 2 wit inspect 7.7 270 72 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 5.9   260  
ldv-regression/test_union_true-termination.c_true-unreach-call.i true 2 wit inspect 7.6 270 70 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.8  250 true 2 wit inspect 5.5   260  
ldv-regression/test_union_true-termination.c_true-unreach-call_1.i true 2 wit inspect 7.6 270 75 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 5.4   270  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call.i true 2 wit inspect 9.5 270 74 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 6.3   280  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i true 2 wit inspect 9.7 270 82 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 5.7   270  
ldv-regression/test02_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.3 270 66 false(unreach-call) 1 wit inspect 3.4  250 false(unreach-call) 1 wit inspect 4.6   220   unknown 0 wit inspect 2.7  210 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 10   280 78 true -32 wit inspect 4.5  260 false(unreach-call) 1 wit inspect 5.7   270   unknown 0 wit inspect 2.1  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/test08_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 9.5 310 71 false(unreach-call) 1 wit inspect 2.3  260 false(unreach-call) 1 wit inspect 3.9   270   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
ldv-regression/test12_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 8.4 270 69 false(unreach-call) 1 wit inspect 3.3  270 false(unreach-call) 1 wit inspect 5.5   230   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
ldv-regression/test21_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 10   280 71 false(unreach-call) 1 wit inspect 2.4  270 false(unreach-call) 1 wit inspect 5.3   270   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
ldv-regression/test22_false-unreach-call.c false(unreach-call) 1 wit inspect 15   280 100 false(unreach-call) 1 wit inspect 2.4  270 false(unreach-call) 1 wit inspect 13     450   unknown 0 wit inspect 2.4  230 true -32 wit inspect .73   18    - wit inspect - wit inspect
ldv-regression/test23_false-unreach-call.c unknown 0 wit inspect 19   220 150 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .017 4.9 error (invalid witness file) 0 wit inspect .70 50 error (invalid witness file) 0 wit inspect .0037 .26 - wit inspect - wit inspect
ldv-regression/test24_false-unreach-call.c unknown 0 wit inspect 400   740 3100 error (invalid witness file) 0 wit inspect .59 41 error (2) 0 wit inspect .026 5.0 error (invalid witness file) 0 wit inspect .84 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 61   220 610 error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .68 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
ldv-regression/test26_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 10   280 73 false(unreach-call) 1 wit inspect 2.2  260 false(unreach-call) 1 wit inspect 4.8   260   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/test27_false-unreach-call_true-termination.c false(unreach-call) 0 wit inspect 34   410 280 true -32 wit inspect 3.7  260 out of memory 0 wit inspect 59     7000   unknown 0 wit inspect 3.3  210 error (2) 0 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/test28_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.6 280 71 false(unreach-call) 1 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 4.3   270   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/test29_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.8 280 70 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 9.3   260   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/test30_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 10   280 76 false(unreach-call) 1 wit inspect 3.8  260 false(unreach-call) 1 wit inspect 5.3   260   unknown 0 wit inspect 2.1  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/test01_true-unreach-call_true-termination.c true 2 wit inspect 8.1 270 69 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 5.5   260  
ldv-regression/test03_true-unreach-call_true-termination.c true 2 wit inspect 9.8 270 77 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 4.6   290  
ldv-regression/test04_true-unreach-call_true-termination.c true 2 wit inspect 11   270 88 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 5.8   280  
ldv-regression/test05_true-unreach-call_true-termination.c true 2 wit inspect 11   270 87 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 11     490  
ldv-regression/test07_true-unreach-call_true-termination.c true 2 wit inspect 9.8 270 84 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 9.2   350  
ldv-regression/test09_true-unreach-call_true-termination.c true 2 wit inspect 10   280 79 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.5  250 true 2 wit inspect 9.8   340  
ldv-regression/test10_true-unreach-call_true-termination.c true 2 wit inspect 9.9 270 90 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 16     510  
ldv-regression/test11_true-unreach-call_true-termination.c true 2 wit inspect 10   270 84 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  280 true 2 wit inspect 7.9   270  
ldv-regression/test13_true-unreach-call_true-termination.c true 2 wit inspect 9.7 270 73 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 5.5   270  
ldv-regression/test14_true-unreach-call_true-termination.c true 2 wit inspect 10   270 78 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 9.0   260  
ldv-regression/test15_true-unreach-call_true-termination.c true 2 wit inspect 9.8 270 92 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 7.0   280  
ldv-regression/test16_true-unreach-call_true-termination.c true 2 wit inspect 10   270 89 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 7.9   280  
ldv-regression/test17_true-unreach-call_true-termination.c true 2 wit inspect 8.7 270 86 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 5.4   260  
ldv-regression/test18_true-unreach-call_true-termination.c true 2 wit inspect 9.7 270 69 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 7.6   300  
ldv-regression/test19_true-unreach-call_true-termination.c true 2 wit inspect 10   280 93 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 9.1   340  
ldv-regression/test20_true-unreach-call_true-termination.c true 2 wit inspect 9.2 270 82 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.5   260  
ldv-regression/test21_true-unreach-call_true-termination.c true 2 wit inspect 12   290 92 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 7.9   310  
ldv-regression/test22_true-unreach-call.c true 2 wit inspect 17   450 120 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.5  300 true 2 wit inspect 21     630  
ldv-regression/test23_true-unreach-call.c true 2 wit inspect 18   300 140 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.5  310 true 2 wit inspect 160     690  
ldv-regression/test24_true-unreach-call_true-termination.c true 2 wit inspect 17   290 130 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8  290 true 2 wit inspect 11     450  
ldv-regression/test25_true-unreach-call.c unknown 0 wit inspect 56   220 570 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .018 4.9
ldv-regression/test26_true-unreach-call_true-termination.c true 2 wit inspect 10   270 76 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.1  250 true 2 wit inspect 5.1   290  
ldv-regression/test27_true-unreach-call_true-termination.c true 2 wit inspect 40   500 390 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 150    990 true 2 wit inspect 170     810  
ldv-regression/test28_true-unreach-call_true-termination.c true 2 wit inspect 8.1 270 85 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  270 true 2 wit inspect 7.3   260  
ldv-regression/test29_true-unreach-call_true-termination.c true 2 wit inspect 8.0 270 76 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 7.7   260  
ldv-regression/test30_true-unreach-call_true-termination.c true 2 wit inspect 11   270 83 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 10     440  
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i error 0 wit inspect 20   280 150 error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .83 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 0 wit inspect 20   280 160 error (invalid witness file) 0 wit inspect .57 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0012 .29 - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i error 0 wit inspect 20   280 150 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .86 50 error (invalid witness file) 0 wit inspect .0012 .29 - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 24   340 180 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.3  290 true 2 wit inspect 13     450  
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 24   350 190 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.7  290 true 2 wit inspect 13     440  
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 23   340 190 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.1  290 true 2 wit inspect 13     430  
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 24   340 190 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.1  290 true 2 wit inspect 12     450  
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 23   330 170 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.9  280 true 2 wit inspect 14     440  
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 24   340 170 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.5  300 true 2 wit inspect 12     440  
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 24   330 160 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.7  290 true 2 wit inspect 13     440  
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 23   320 180 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.9  300 true 2 wit inspect 12     440  
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 24   340 170 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.1  280 true 2 wit inspect 12     430  
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 23   350 160 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.0  280 true 2 wit inspect 13     420  
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   2000 6700 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0018 .28 - wit inspect - wit inspect
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   1000 11000 error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .022 4.8 error (invalid witness file) 0 wit inspect .64 49 error (invalid witness file) 0 wit inspect .0013 .27 - wit inspect - wit inspect
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   3900 8700 error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .64 49 error (invalid witness file) 0 wit inspect .0010 .31 - wit inspect - wit inspect
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   4100 7700 error (invalid witness file) 0 wit inspect .41 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .80 47 error (invalid witness file) 0 wit inspect .0016 .30 - wit inspect - wit inspect
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i unknown 0 wit inspect 630   340 8500 error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .67 49 error (invalid witness file) 0 wit inspect .0010 .26 - wit inspect - wit inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 660   410 7500 error (invalid witness file) 0 wit inspect .58 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .84 49 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   3000 10000 error (invalid witness file) 0 wit inspect .40 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .70 49 error (invalid witness file) 0 wit inspect .0017 .26 - wit inspect - wit inspect
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   820 11000 error (invalid witness file) 0 wit inspect .40 44 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .69 49 error (invalid witness file) 0 wit inspect .0029 .26 - wit inspect - wit inspect
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   2400 11000 error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0030 .29 - wit inspect - wit inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i timeout 0 wit inspect 900   1900 6200 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .020 4.9 error (invalid witness file) 0 wit inspect .65 49 error (invalid witness file) 0 wit inspect .0033 .29 - wit inspect - wit inspect
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 65   610 660 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .83 47 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   940 9000 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .87 47 error (invalid witness file) 0 wit inspect .0033 .26 - wit inspect - wit inspect
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   4100 7800 error (invalid witness file) 0 wit inspect .42 44 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .83 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   3900 7500 error (invalid witness file) 0 wit inspect .53 41 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0014 .30 - wit inspect - wit inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i unknown 0 wit inspect 710   290 9000 error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .69 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 620   350 7000 error (invalid witness file) 0 wit inspect .53 42 error (2) 0 wit inspect .018 4.8 error (invalid witness file) 0 wit inspect .64 49 error (invalid witness file) 0 wit inspect .0013 .35 - wit inspect - wit inspect
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   2800 12000