Tool symbiotic 5.0.0-KLEE:1faddfe0-dg:12c34aac-symbiotic:5e14b94d-minisat:3db58943-llvm-instrumentation:cd767593-stp:17249213 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* [apollon005; apollon043; apollon077; apollon078; apollon087; apollon118] [apollon061; apollon077; apollon078; apollon086; apollon134] [apollon038; apollon077; apollon078; apollon083] [apollon077; apollon078; apollon161] 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: [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]
Date of execution 2017-12-01 22:41:19 CET 2017-12-02 21:10:50 CET 2017-12-02 22:39:24 CET 2017-12-02 22:51:52 CET 2017-12-02 23:01:21 CET 2017-12-02 19:44:15 CET 2017-12-02 21:36:25 CET
Run set symbiotic.sv-comp18.ReachSafety-Heap cpa-seq-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Heap uautomizer-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.ReachSafety-Heap uautomizer-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.ReachSafety-Heap
Options --witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-01_2241.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/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-01_2241.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/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/symbiotic.2017-12-01_2241.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 .21 11 2.9 unknown 0 wit inspect 6.3  280 true -32 wit inspect 6.3   260   unknown 0 wit inspect 2.7  220 false(unreach-call) 1 wit inspect .67   19    - wit inspect - wit inspect
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .23 11 3.0 unknown 0 wit inspect 3.8  280 true -32 wit inspect 6.3   270   unknown 0 wit inspect 2.5  210 true -32 wit inspect .67   18    - wit inspect - wit inspect
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .23 11 2.7 false(unreach-call) 1 wit inspect 4.1  270 true -32 wit inspect 6.3   270   unknown 0 wit inspect 2.5  220 true -32 wit inspect .64   18    - wit inspect - wit inspect
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .21 11 2.5 unknown 0 wit inspect 5.2  270 true -32 wit inspect 4.1   260   unknown 0 wit inspect 3.8  230 true -32 wit inspect .63   18    - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(unreach-call) 0 wit inspect .20 11 2.2 unknown 0 wit inspect 4.6  270 true -32 wit inspect 5.8   250   unknown 0 wit inspect 2.4  210 true -32 wit inspect .68   18    - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .20 11 2.2 unknown 0 wit inspect 5.2  270 true -32 wit inspect 5.6   240   unknown 0 wit inspect 2.4  210 true -32 wit inspect .63   18    - wit inspect - wit inspect
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    520 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .021 5.0
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i timeout (timeout) 0 wit inspect 900    370 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .024 4.8
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    6400 4600   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .019 4.9
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    600 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .76 43 error (2) 0 wit inspect .019 4.9
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    4500 9100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .42 44 error (2) 0 wit inspect .024 5.0
heap-manipulation/tree_true-unreach-call.i timeout (timeout) 0 wit inspect 900    2200 8100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 42 error (2) 0 wit inspect .018 4.9
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .21 11 1.9 false(unreach-call) 1 wit inspect 4.3  260 true -32 wit inspect 3.5   230   unknown 0 wit inspect 2.4  210 true -32 wit inspect .62   18    - wit inspect - wit inspect
list-properties/list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .18 11 2.4 unknown 0 wit inspect 4.8  270 true -32 wit inspect 3.7   240   unknown 0 wit inspect 2.3  210 true -32 wit inspect .62   18    - wit inspect - wit inspect
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .19 11 2.2 false(unreach-call) 1 wit inspect 4.6  270 true -32 wit inspect 3.5   250   unknown 0 wit inspect 2.4  210 false(unreach-call) 1 wit inspect .62   18    - wit inspect - wit inspect
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .18 11 1.7 unknown 0 wit inspect 6.1  270 true -32 wit inspect 6.8   230   unknown 0 wit inspect 2.4  210 false(unreach-call) 1 wit inspect .62   18    - wit inspect - wit inspect
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .20 11 2.0 false(unreach-call) 1 wit inspect 5.0  270 true -32 wit inspect 6.5   230   unknown 0 wit inspect 3.5  210 true -32 wit inspect .63   18    - wit inspect - wit inspect
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .21 11 2.0 false(unreach-call) 1 wit inspect 4.3  270 true -32 wit inspect 5.1   240   unknown 0 wit inspect 2.4  220 true -32 wit inspect .64   18    - wit inspect - wit inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    1600 7400   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .019 5.0
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i timeout (timeout) 0 wit inspect 900    260 13000   - 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_search_true-unreach-call_false-valid-memcleanup.i true 2 wit inspect .17 11 1.9 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 25    530 true 2 wit inspect 73     1100  
list-properties/list_true-unreach-call_false-valid-memtrack.i timeout (timeout) 0 wit inspect 900    1300 10000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .020 4.9
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i timeout (timeout) 0 wit inspect 900    1500 9900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 44 error (2) 0 wit inspect .019 4.9
list-properties/simple_true-unreach-call_false-valid-memtrack.i timeout (timeout) 0 wit inspect 900    1300 7200   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .021 4.9
list-properties/splice_true-unreach-call_false-valid-memtrack.i timeout (timeout) 0 wit inspect 900    1400 8800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 42 error (2) 0 wit inspect .024 5.0
ldv-regression/1_3_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .16 11 1.8 false(unreach-call) 1 wit inspect 3.4  260 true -32 wit inspect 4.4   230   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
ldv-regression/alt_test_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .18 11 1.6 false(unreach-call) 1 wit inspect 5.4  280 true -32 wit inspect 5.0   240   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .66   18    - wit inspect - wit inspect
ldv-regression/callfpointer_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .15 11 1.7 false(unreach-call) 1 wit inspect 3.2  250 false(unreach-call) 1 wit inspect 4.6   230   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
ldv-regression/fo_test_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .20 11 2.0 false(unreach-call) 1 wit inspect 5.4  260 true -32 wit inspect 3.2   230   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .16 11 1.8 false(unreach-call) 1 wit inspect 3.2  260 true -32 wit inspect 5.6   260   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/mutex_lock_struct_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .16 11 1.6 false(unreach-call) 1 wit inspect 3.0  260 true -32 wit inspect 5.3   260   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/recursive_list_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .17 11 1.5 false(unreach-call) 1 wit inspect 3.6  260 true -32 wit inspect 3.2   230   unknown 0 wit inspect 2.1  210 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 .20 11 2.4 false(unreach-call) 1 wit inspect 3.0  270 true -32 wit inspect 4.8   230   unknown 0 wit inspect 2.9  210 error (2) 0 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/rule60_list2_true-termination.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect .19 11 2.3 false(unreach-call) 1 wit inspect 3.0  270 true -32 wit inspect 3.9   260   unknown 0 wit inspect 2.3  210 true -32 wit inspect .66   18    - wit inspect - wit inspect
ldv-regression/stateful_check_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect .22 11 2.6 false(unreach-call) 1 wit inspect 4.6  270 true -32 wit inspect 4.7   230   unknown 0 wit inspect 2.0  210 true -32 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect .17 11 1.6 false(unreach-call) 1 wit inspect 4.0  250 true -32 wit inspect 5.3   260   unknown 0 wit inspect 1.9  200 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect .15 11 1.9 false(unreach-call) 1 wit inspect 3.0  260 true -32 wit inspect 5.1   250   unknown 0 wit inspect 1.9  190 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call.i true 2 wit inspect .12 11 1.3 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  250 true 2 wit inspect 7.4   270  
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i true 2 wit inspect .12 11 1.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 5.9   260  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call.i true 2 wit inspect .15 11 1.3 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.0  250 true 2 wit inspect 6.8   270  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call_1.i true 2 wit inspect .14 11 1.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 5.2   260  
ldv-regression/ex3_forlist_true-termination.c_true-unreach-call.i true 2 wit inspect .18 11 1.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 18    460 true 2 wit inspect 30     690  
ldv-regression/just_assert_true-termination.c_true-unreach-call.i true 2 wit inspect .12 11 1.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  240 true 2 wit inspect 3.4   220  
ldv-regression/mutex_lock_int_true-termination.c_true-unreach-call_1.i true 2 wit inspect .14 11 1.2 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 6.9   260  
ldv-regression/mutex_lock_struct_true-termination.c_true-unreach-call_1.i true 2 wit inspect .15 11 1.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 6.4   260  
ldv-regression/nested_structure_noptr_true-termination.c_true-unreach-call.i true 2 wit inspect .15 11 1.3 - 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 .17 11 1.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 5.6   260  
ldv-regression/nested_structure_ptr_true-termination.c_true-unreach-call.i true 2 wit inspect .15 11 1.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 9.1   470  
ldv-regression/nested_structure_ptr_true-unreach-call_true-termination.i true 2 wit inspect .16 11 1.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 13     400  
ldv-regression/nested_structure_true-termination.c_true-unreach-call.i true 2 wit inspect .15 11 1.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 8.3   290  
ldv-regression/nested_structure_true-unreach-call_true-termination.i true 2 wit inspect .14 11 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 8.6   290  
ldv-regression/oomInt_true-termination.c_true-unreach-call.i true 2 wit inspect .14 11 1.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 5.9   270  
ldv-regression/oomInt_true-termination.c_true-unreach-call_1.i true 2 wit inspect .12 11 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 3.7   280  
ldv-regression/rule57_ebda_blast_true-termination.c_true-unreach-call_1.i true 2 wit inspect .22 11 2.2 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 6.5   270  
ldv-regression/rule60_list2_true-termination.c_true-unreach-call.i true 2 wit inspect .20 11 2.0 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1  270 true 2 wit inspect 15     670  
ldv-regression/rule60_list_true-termination.c_true-unreach-call.i true 2 wit inspect .15 11 1.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  260 true 2 wit inspect 11     370  
ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i true 2 wit inspect .15 11 1.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7  260 true 2 wit inspect 4.8   260  
ldv-regression/structure_assignment_true-termination.c_true-unreach-call.i true 2 wit inspect .15 11 1.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 4.7   250  
ldv-regression/test_address_true-termination.c_true-unreach-call.i true 2 wit inspect .15 11 1.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  250 true 2 wit inspect 6.3   260  
ldv-regression/test_cut_trace_true-termination.c_true-unreach-call.i true 2 wit inspect .12 11 1.3 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.1   260  
ldv-regression/test_malloc-1_true-unreach-call_true-termination.i true 2 wit inspect .14 11 2.0 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 6.4   260  
ldv-regression/test_malloc-2_true-unreach-call_true-termination.i true 2 wit inspect .16 11 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 6.1   260  
ldv-regression/test_overflow_true-termination.c_true-unreach-call.i true 2 wit inspect .14 11 1.9 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  250 true 2 wit inspect 5.3   260  
ldv-regression/test_union_cast-1_true-unreach-call_true-termination.i true 2 wit inspect .14 11 1.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 5.7   260  
ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i true 2 wit inspect .14 11 1.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 5.6   260  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call.i true 2 wit inspect .15 11 1.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 6.2   260  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call_1.i true 2 wit inspect .14 11 1.2 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.7   260  
ldv-regression/test_union_true-termination.c_true-unreach-call.i true 2 wit inspect .14 11 1.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 5.0   270  
ldv-regression/test_union_true-termination.c_true-unreach-call_1.i true 2 wit inspect .15 11 1.3 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 3.6   260  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call.i true 2 wit inspect .15 11 1.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 6.6   280  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i true 2 wit inspect .12 11 1.1 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 6.3   270  
ldv-regression/test02_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .16 11 1.4 false(unreach-call) 1 wit inspect 2.2  260 false(unreach-call) 1 wit inspect 4.8   220   unknown 0 wit inspect 2.0  190 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 .14 11 1.5 false(unreach-call) 1 wit inspect 2.3  260 true -32 wit inspect 3.3   230   unknown 0 wit inspect 2.0  210 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 .16 11 1.9 false(unreach-call) 1 wit inspect 4.0  260 true -32 wit inspect 4.6   230   unknown 0 wit inspect 1.9  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 .15 11 1.6 false(unreach-call) 1 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 3.3   230   unknown 0 wit inspect 1.9  180 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/test21_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .20 12 2.4 false(unreach-call) 1 wit inspect 2.3  270 true -32 wit inspect 3.9   250   unknown 0 wit inspect 1.9  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/test22_false-unreach-call.c false(unreach-call) 1 wit inspect .26 12 2.6 false(unreach-call) 1 wit inspect 2.6  280 true -32 wit inspect 3.4   230   unknown 0 wit inspect 2.8  210 true -32 wit inspect .57   18    - wit inspect - wit inspect
ldv-regression/test23_false-unreach-call.c false(unreach-call) 1 wit inspect .28 13 3.4 false(unreach-call) 1 wit inspect 14    290 true -32 wit inspect 4.9   240   unknown 0 wit inspect 2.8  210 true -32 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/test24_false-unreach-call.c false(unreach-call) 1 wit inspect .20 14 2.4 false(unreach-call) 1 wit inspect 4.6  290 true -32 wit inspect 3.4   220   unknown 0 wit inspect 2.0  210 true -32 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/test25_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .20 14 2.3 false(unreach-call) 1 wit inspect 14    300 true -32 wit inspect 3.4   240   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/test26_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .15 11 1.8 false(unreach-call) 1 wit inspect 3.2  260 true -32 wit inspect 3.3   220   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
ldv-regression/test27_false-unreach-call_true-termination.c unknown 0 wit inspect .52 13 7.1 error (invalid witness file) 0 wit inspect .64 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 .28 - wit inspect - wit inspect
ldv-regression/test28_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .17 11 1.9 false(unreach-call) 1 wit inspect 3.0  260 true -32 wit inspect 4.5   230   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .61   19    - wit inspect - wit inspect
ldv-regression/test29_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .16 11 1.7 false(unreach-call) 1 wit inspect 3.1  260 true -32 wit inspect 3.3   240   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
ldv-regression/test30_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .15 11 1.5 false(unreach-call) 1 wit inspect 2.3  270 true -32 wit inspect 4.7   230   unknown 0 wit inspect 2.1  200 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
ldv-regression/test01_true-unreach-call_true-termination.c true 2 wit inspect .12 11 1.3 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 6.7   270  
ldv-regression/test03_true-unreach-call_true-termination.c true 2 wit inspect .12 11 1.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 6.8   270  
ldv-regression/test04_true-unreach-call_true-termination.c true 2 wit inspect .13 11 1.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 8.0   270  
ldv-regression/test05_true-unreach-call_true-termination.c true 2 wit inspect .15 11 1.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 13     490  
ldv-regression/test07_true-unreach-call_true-termination.c true 2 wit inspect .12 11 1.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 8.6   340  
ldv-regression/test09_true-unreach-call_true-termination.c true 2 wit inspect .15 11 1.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 9.8   350  
ldv-regression/test10_true-unreach-call_true-termination.c true 2 wit inspect .14 11 1.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  260 true 2 wit inspect 12     490  
ldv-regression/test11_true-unreach-call_true-termination.c true 2 wit inspect .12 11 1.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 7.8   270  
ldv-regression/test13_true-unreach-call_true-termination.c true 2 wit inspect .15 11 1.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 5.3   260  
ldv-regression/test14_true-unreach-call_true-termination.c true 2 wit inspect .13 11 1.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  260 true 2 wit inspect 4.9   260  
ldv-regression/test15_true-unreach-call_true-termination.c true 2 wit inspect .14 11 1.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 7.3   280  
ldv-regression/test16_true-unreach-call_true-termination.c true 2 wit inspect .13 11 1.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.2  250 true 2 wit inspect 8.5   300  
ldv-regression/test17_true-unreach-call_true-termination.c true 2 wit inspect .14 11 1.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.8  250 true 2 wit inspect 6.3   250  
ldv-regression/test18_true-unreach-call_true-termination.c true 2 wit inspect .15 11 1.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 8.6   300  
ldv-regression/test19_true-unreach-call_true-termination.c true 2 wit inspect .15 11 1.2 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 11     360  
ldv-regression/test20_true-unreach-call_true-termination.c true 2 wit inspect .15 11 1.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 5.7   260  
ldv-regression/test21_true-unreach-call_true-termination.c true 2 wit inspect .14 11 1.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 8.0   310  
ldv-regression/test22_true-unreach-call.c true 2 wit inspect .15 11 1.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.3  290 true 2 wit inspect 25     640  
ldv-regression/test23_true-unreach-call.c true 2 wit inspect .13 11 1.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.9  310 true 2 wit inspect 260     760  
ldv-regression/test24_true-unreach-call_true-termination.c true 2 wit inspect .15 11 1.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.9  290 true 2 wit inspect 11     410  
ldv-regression/test25_true-unreach-call.c true 2 wit inspect .15 11 1.4 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 15    430 true 2 wit inspect 26     550  
ldv-regression/test26_true-unreach-call_true-termination.c true 2 wit inspect .15 11 1.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 9.3   290  
ldv-regression/test27_true-unreach-call_true-termination.c true 2 wit inspect .15 11 1.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 31    480 true 2 wit inspect 180     780  
ldv-regression/test28_true-unreach-call_true-termination.c true 2 wit inspect .18 11 1.7 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 7.5   270  
ldv-regression/test29_true-unreach-call_true-termination.c true 2 wit inspect .19 11 1.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 4.8   270  
ldv-regression/test30_true-unreach-call_true-termination.c true 2 wit inspect .15 11 1.6 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  250 true 2 wit inspect 7.0   450  
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect .47 17 5.3 false(unreach-call) 1 wit inspect 8.3  360 true -32 wit inspect 8.4   460   unknown 0 wit inspect 3.6  280 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 .47 15 4.9 false(unreach-call) 1 wit inspect 6.1  370 true -32 wit inspect 8.7   470   unknown 0 wit inspect 3.6  280 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 .45 16 5.2 false(unreach-call) 1 wit inspect 11    360 true -32 wit inspect 8.6   440   unknown 0 wit inspect 5.2  270 false(unreach-call) 1 wit inspect 1.1    18    - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .32 14 3.9 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.2  280 true 2 wit inspect 18     430  
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .32 14 4.3 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  300 true 2 wit inspect 8.6   430  
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .35 14 3.9 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.9  280 true 2 wit inspect 12     430  
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .32 14 4.0 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.9  280 true 2 wit inspect 12     430  
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .34 14 4.2 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.9  280 true 2 wit inspect 14     430  
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .32 14 4.0 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.8  280 true 2 wit inspect 14     440  
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .34 14 3.5 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.7  280 true 2 wit inspect 12     430  
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .34 14 4.1 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1  280 true 2 wit inspect 14     430  
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .32 14 4.0 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.5  270 true 2 wit inspect 11     420  
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .31 14 4.8 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1  280 true 2 wit inspect 12     430  
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .19 11 2.2 unknown 0 wit inspect 5.4  280 true -32 wit inspect 6.6   280   unknown 0 wit inspect 2.4  210 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .17 11 1.8 unknown 0 wit inspect 4.1  260 true -32 wit inspect 3.7   250   unknown 0 wit inspect 2.4  220 false(unreach-call) 1 wit inspect .66   18    - wit inspect - wit inspect
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .18 11 2.5 false(unreach-call) 1 wit inspect 4.2  270 true -32 wit inspect 5.4   250   unknown 0 wit inspect 2.3  210 false(unreach-call) 1 wit inspect .62   18    - wit inspect - wit inspect
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .22 11 2.2 unknown 0 wit inspect 4.0  260 true -32 wit inspect 4.0   260   unknown 0 wit inspect 3.6  220 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 .17 11 2.0 unknown 0 wit inspect 4.7  270 true -32 wit inspect 3.9   250   unknown 0 wit inspect 2.4  210 false(unreach-call) 1 wit inspect .64   19    - wit inspect - wit inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(unreach-call) 0 wit inspect .20 11 1.9 unknown 0 wit inspect 4.2  270 true -32 wit inspect 3.9   250   unknown 0 wit inspect 3.3  210 true -32 wit inspect .63   18    - wit inspect - wit inspect
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .18 11 2.1 false(unreach-call) 1 wit inspect 4.6  260 true -32 wit inspect 5.6   240   unknown 0 wit inspect 2.4  220 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .21 11 2.4 false(unreach-call) 1 wit inspect 5.2  270 true -32 wit inspect 5.5   250   unknown 0 wit inspect 2.3  210 false(unreach-call) 1 wit inspect .64   18    - wit inspect - wit inspect
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .20 11 2.1 unknown 0 wit inspect 3.3  270 true -32 wit inspect 5.2   240   unknown 0 wit inspect 2.3  210 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i timeout (timeout) 0 wit inspect 900    2200 7200   error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0011 .26 - wit inspect - wit inspect
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .22 15 2.0 unknown 0 wit inspect 5.4  280 true -32 wit inspect 3.9   250   unknown 0 wit inspect 2.4  210 true -32 wit inspect .63   18    - wit inspect - wit inspect
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .17 11 1.8 false(unreach-call) 1 wit inspect 3.2  270 true -32 wit inspect 3.6   240   unknown 0 wit inspect 3.5  220 false(unreach-call) 1 wit inspect .64   18    - wit inspect - wit inspect
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .21 11 2.0 false(unreach-call) 1 wit inspect 5.5  270 true -32 wit inspect 5.5   250   unknown 0 wit inspect 2.4  210 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect .19 11 2.5 unknown 0 wit inspect 4.8  270 true -32 wit inspect 5.8   260   unknown 0 wit inspect 3.4  210 true -32 wit inspect .63   18    - wit inspect - wit inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .17 11 1.6 unknown 0 wit inspect 4.5  270 true -32 wit inspect 3.3   250   unknown 0 wit inspect 2.3  210 false(unreach-call) 1 wit inspect .62   18    - wit inspect - wit