Tool CPAchecker 1.6.1-svn 26758M 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-11-30 11:20:26 CET 2017-12-01 07:36:48 CET 2017-12-01 08:27:40 CET 2017-12-01 08:32:13 CET 2017-12-01 08:39:14 CET 2017-12-01 04:24:39 CET 2017-12-01 07:43:13 CET
Run set cpa-bam-slicing.sv-comp18.ReachSafety-Heap cpa-seq-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Heap uautomizer-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-cpa-bam-slicing.sv-comp18-correctness-witness.ReachSafety-Heap uautomizer-validate-correctness-witnesses-cpa-bam-slicing.sv-comp18-correctness-witness.ReachSafety-Heap
Options -ldv-bam-svcomp -disable-java-assertions -heap 10000m -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.2017-11-30_1120.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/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.2017-11-30_1120.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/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-slicing.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cpa-bam-slicing.2017-11-30_1120.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 7.6 430 60 true -32 wit inspect 4.7  260 true -32 wit inspect 6.1   270   unknown 0 wit inspect 3.7  210 false(unreach-call) 1 wit inspect .69   19    - wit inspect - wit inspect
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 4.7 310 42 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .88 50 error (invalid witness file) 0 wit inspect .0019 .26 - wit inspect - wit inspect
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 3.9 290 33 true -32 wit inspect 4.1  260 true -32 wit inspect 6.2   270   unknown 0 wit inspect 2.5  210 true -32 wit inspect .67   19    - wit inspect - wit inspect
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i true -32 wit inspect 32   1200 270 unknown 0 wit inspect 6.0  310 false(unreach-call) 1 wit inspect 6.6   290   unknown 0 wit inspect .90 51 error (1) 0 wit inspect .069  9.0  - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(unreach-call) 0 wit inspect 4.5 300 47 true -32 wit inspect 4.6  260 true -32 wit inspect 5.8   240   unknown 0 wit inspect 3.5  210 true -32 wit inspect .67   19    - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 4.7 300 38 true -32 wit inspect 4.1  260 true -32 wit inspect 5.7   260   unknown 0 wit inspect 3.4  210 true -32 wit inspect .66   19    - wit inspect - wit inspect
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 9.4 500 88 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .029 4.8
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 9.1 460 74 - wit inspect - wit inspect - wit inspect - wit inspect error (recursion) 0 wit inspect 4.1  250 true 2 wit inspect 330     1100  
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 4.6 300 42 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 43 error (2) 0 wit inspect .018 4.9
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.6 280 43 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5100 timeout 0 wit inspect 960     3800  
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 45   2000 450 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3900 false(unreach-call) -16 wit inspect 7.6   290  
heap-manipulation/tree_true-unreach-call.i true 2 wit inspect 8.6 450 67 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3500 timeout 0 wit inspect 960     1000  
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 3.9 300 33 true -32 wit inspect 4.9  260 true -32 wit inspect 5.4   240   unknown 0 wit inspect 3.4  220 true -32 wit inspect .64   19    - wit inspect - wit inspect
list-properties/list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 6.0 330 49 true -32 wit inspect 3.7  260 true -32 wit inspect 5.4   250   unknown 0 wit inspect 3.2  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 3.6 290 33 true -32 wit inspect 3.7  260 true -32 wit inspect 4.7   240   unknown 0 wit inspect 3.6  230 false(unreach-call) 1 wit inspect .66   19    - wit inspect - wit inspect
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i true -32 wit inspect 3.9 280 36 unknown 0 wit inspect 8.4  300 false(unreach-call) 1 wit inspect 47     850   unknown 0 wit inspect .88 51 error (1) 0 wit inspect .071  9.1  - wit inspect - wit inspect
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 3.6 290 29 true -32 wit inspect 3.4  260 true -32 wit inspect 5.3   240   unknown 0 wit inspect 3.1  210 true -32 wit inspect .95   19    - wit inspect - wit inspect
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 4.0 290 35 true -32 wit inspect 3.9  260 true -32 wit inspect 6.6   310   unknown 0 wit inspect 3.4  210 true -32 wit inspect .66   19    - wit inspect - wit inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.7 300 45 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3200 timeout 0 wit inspect 960     1100  
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 5.3 300 43 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2100 false(unreach-call) -16 wit inspect 6.0   260  
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i true 2 wit inspect 4.9 300 39 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 26    510 true 2 wit inspect 70     1100  
list-properties/list_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 6.8 390 54 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3100 timeout 0 wit inspect 960     1500  
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 3.4 280 32 - wit inspect - wit inspect - wit inspect - wit inspect out of java memory 0 wit inspect 160    5200 timeout 0 wit inspect 960     1100  
list-properties/simple_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 4.5 290 44 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1800 timeout 0 wit inspect 960     1000  
list-properties/splice_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 5.7 310 45 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4100 timeout 0 wit inspect 960     1200  
ldv-regression/1_3_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.3 280 29 true -32 wit inspect 3.2  260 true -32 wit inspect 6.9   300   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/alt_test_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.9 290 34 true -32 wit inspect 3.7  260 true -32 wit inspect 4.8   230   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .71   18    - wit inspect - wit inspect
ldv-regression/callfpointer_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.1 270 27 true -32 wit inspect 2.9  260 false(unreach-call) 1 wit inspect 4.5   230   unknown 0 wit inspect 2.7  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 3.4 280 29 true -32 wit inspect 3.5  260 true -32 wit inspect 5.0   230   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .68   19    - wit inspect - wit inspect
ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.1 280 30 true -32 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 4.8   250   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
ldv-regression/mutex_lock_struct_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.2 280 30 true -32 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 6.2   320   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 true -32 wit inspect 3.2 270 28 false(unreach-call) 1 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 5.6   250   unknown 0 wit inspect .95 51 error (1) 0 wit inspect .072  9.1  - wit inspect - wit inspect
ldv-regression/rule57_ebda_blast_true-termination.c_false-unreach-call.i false(unreach-call) 0 wit inspect 3.7 290 37 true -32 wit inspect 3.7  260 true -32 wit inspect 4.8   230   unknown 0 wit inspect 2.9  210 error (2) 0 wit inspect .60   19    - wit inspect - wit inspect
ldv-regression/rule60_list2_true-termination.c_false-unreach-call_1.i false(unreach-call) 0 wit inspect 4.7 300 40 true -32 wit inspect 3.7  260 true -32 wit inspect 3.6   240   unknown 0 wit inspect 2.4  210 true -32 wit inspect .65   18    - wit inspect - wit inspect
ldv-regression/stateful_check_false-unreach-call_false-termination.i false(unreach-call) 0 wit inspect 4.0 290 38 true -32 wit inspect 3.3  260 true -32 wit inspect 4.7   240   unknown 0 wit inspect 3.0  210 true -32 wit inspect .66   19    - wit inspect - wit inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.4 300 30 true -32 wit inspect 2.9  250 false(unreach-call) 1 wit inspect 5.3   250   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .61   18    - wit inspect - wit inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect 3.2 280 27 true -32 wit inspect 3.1  250 false(unreach-call) 1 wit inspect 4.7   240   unknown 0 wit inspect 2.0  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call.i true 2 wit inspect 3.1 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 5.9   270  
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.7 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 5.6   260  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call.i true 2 wit inspect 2.8 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 5.7   280  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.8 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  260 true 2 wit inspect 5.3   250  
ldv-regression/ex3_forlist_true-termination.c_true-unreach-call.i unknown 0 wit inspect 6.2 350 53 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 41 error (2) 0 wit inspect .024 4.8
ldv-regression/just_assert_true-termination.c_true-unreach-call.i true 2 wit inspect 2.7 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 5.0   220  
ldv-regression/mutex_lock_int_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.9 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 7.7   270  
ldv-regression/mutex_lock_struct_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.8 270 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 7.8   270  
ldv-regression/nested_structure_noptr_true-termination.c_true-unreach-call.i true 2 wit inspect 2.7 270 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 4.6   240  
ldv-regression/nested_structure_noptr_true-unreach-call_true-termination.i true 2 wit inspect 2.7 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  250 true 2 wit inspect 4.9   260  
ldv-regression/nested_structure_ptr_true-termination.c_true-unreach-call.i true 2 wit inspect 2.7 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 10     440  
ldv-regression/nested_structure_ptr_true-unreach-call_true-termination.i true 2 wit inspect 2.8 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 9.0   390  
ldv-regression/nested_structure_true-termination.c_true-unreach-call.i true 2 wit inspect 2.7 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 7.8   270  
ldv-regression/nested_structure_true-unreach-call_true-termination.i true 2 wit inspect 2.9 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 8.1   290  
ldv-regression/oomInt_true-termination.c_true-unreach-call.i true 2 wit inspect 2.9 270 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 5.9   260  
ldv-regression/oomInt_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.8 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 5.3   260  
ldv-regression/rule57_ebda_blast_true-termination.c_true-unreach-call_1.i true 2 wit inspect 3.5 280 36 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  250 true 2 wit inspect 6.8   260  
ldv-regression/rule60_list2_true-termination.c_true-unreach-call.i true 2 wit inspect 3.8 280 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3  260 true 2 wit inspect 23     700  
ldv-regression/rule60_list_true-termination.c_true-unreach-call.i true 2 wit inspect 3.3 270 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  260 true 2 wit inspect 9.7   370  
ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i true 2 wit inspect 3.3 280 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  250 true 2 wit inspect 5.0   270  
ldv-regression/structure_assignment_true-termination.c_true-unreach-call.i true 2 wit inspect 2.9 260 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 5.2   260  
ldv-regression/test_address_true-termination.c_true-unreach-call.i true 2 wit inspect 2.9 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  250 true 2 wit inspect 6.1   260  
ldv-regression/test_cut_trace_true-termination.c_true-unreach-call.i true 2 wit inspect 2.8 270 22 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 5.5   260  
ldv-regression/test_malloc-1_true-unreach-call_true-termination.i true 2 wit inspect 2.8 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 7.6   260  
ldv-regression/test_malloc-2_true-unreach-call_true-termination.i true 2 wit inspect 2.8 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  260 true 2 wit inspect 7.2   260  
ldv-regression/test_overflow_true-termination.c_true-unreach-call.i true 2 wit inspect 2.8 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2  280 true 2 wit inspect 6.6   260  
ldv-regression/test_union_cast-1_true-unreach-call_true-termination.i true 2 wit inspect 2.9 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 5.8   260  
ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i true 2 wit inspect 2.9 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 5.4   260  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call.i true 2 wit inspect 2.6 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 6.1   260  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.7 260 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.8   260  
ldv-regression/test_union_true-termination.c_true-unreach-call.i true 2 wit inspect 2.7 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.2  250 true 2 wit inspect 5.6   270  
ldv-regression/test_union_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.8 280 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  240 true 2 wit inspect 6.3   260  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call.i true 2 wit inspect 2.9 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 6.0   270  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.7 270 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 7.8   280  
ldv-regression/test02_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.1 280 26 true -32 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 4.8   220   unknown 0 wit inspect 2.6  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/test06_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.4 290 30 true -32 wit inspect 3.1  260 true -32 wit inspect 4.8   240   unknown 0 wit inspect 2.9  190 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 3.2 280 30 true -32 wit inspect 3.3  250 true -32 wit inspect 5.0   220   unknown 0 wit inspect 2.8  210 false(unreach-call) 1 wit inspect .60   18    - wit inspect - wit inspect
ldv-regression/test12_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.2 270 25 true -32 wit inspect 2.9  260 true -32 wit inspect 5.9   290   unknown 0 wit inspect 2.6  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/test21_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.5 280 33 true -32 wit inspect 3.5  260 true -32 wit inspect 5.0   230   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .59   19    - wit inspect - wit inspect
ldv-regression/test22_false-unreach-call.c false(unreach-call) 0 wit inspect 3.5 290 32 true -32 wit inspect 3.4  250 true -32 wit inspect 5.4   250   unknown 0 wit inspect 3.0  190 true -32 wit inspect .63   19    - wit inspect - wit inspect
ldv-regression/test23_false-unreach-call.c false(unreach-call) 0 wit inspect 27   1700 230 true -32 wit inspect 3.6  260 true -32 wit inspect 5.4   250   unknown 0 wit inspect 3.0  210 true -32 wit inspect .68   19    - wit inspect - wit inspect
ldv-regression/test24_false-unreach-call.c false(unreach-call) 0 wit inspect 5.5 440 49 true -32 wit inspect 3.5  260 out of memory 0 wit inspect 56     7000   unknown 0 wit inspect 3.2  210 true -32 wit inspect .61   19    - wit inspect - wit inspect
ldv-regression/test25_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 7.2 410 63 true -32 wit inspect 3.6  260 out of memory 0 wit inspect 55     7000   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .62   19    - wit inspect - wit inspect
ldv-regression/test26_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.3 280 30 true -32 wit inspect 3.1  250 false(unreach-call) 1 wit inspect 5.6   260   unknown 0 wit inspect 2.8  190 false(unreach-call) 1 wit inspect .62   18    - wit inspect - wit inspect
ldv-regression/test27_false-unreach-call_true-termination.c false(unreach-call) 0 wit inspect 4.8 310 44 true -32 wit inspect 3.3  260 out of memory 0 wit inspect 56     7000   unknown 0 wit inspect 2.9  210 error (2) 0 wit inspect .61   19    - wit inspect - wit inspect
ldv-regression/test28_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.3 280 30 true -32 wit inspect 3.4  260 true -32 wit inspect 5.1   240   unknown 0 wit inspect 2.8  190 false(unreach-call) 1 wit inspect .73   19    - wit inspect - wit inspect
ldv-regression/test29_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.2 290 29 true -32 wit inspect 3.7  260 true -32 wit inspect 5.1   240   unknown 0 wit inspect 2.9  190 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 3.3 280 29 true -32 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 5.6   260   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
ldv-regression/test01_true-unreach-call_true-termination.c true 2 wit inspect 2.7 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 5.5   260  
ldv-regression/test03_true-unreach-call_true-termination.c true 2 wit inspect 2.8 270 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 7.6   270  
ldv-regression/test04_true-unreach-call_true-termination.c true 2 wit inspect 2.9 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  260 true 2 wit inspect 6.9   280  
ldv-regression/test05_true-unreach-call_true-termination.c true 2 wit inspect 3.1 270 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 11     480  
ldv-regression/test07_true-unreach-call_true-termination.c true 2 wit inspect 3.2 280 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 9.6   360  
ldv-regression/test09_true-unreach-call_true-termination.c true 2 wit inspect 2.9 270 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 10     340  
ldv-regression/test10_true-unreach-call_true-termination.c true 2 wit inspect 3.1 270 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 13     510  
ldv-regression/test11_true-unreach-call_true-termination.c true 2 wit inspect 3.0 270 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  260 true 2 wit inspect 7.2   260  
ldv-regression/test13_true-unreach-call_true-termination.c true 2 wit inspect 2.7 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 6.1   260  
ldv-regression/test14_true-unreach-call_true-termination.c true 2 wit inspect 2.9 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 6.7   260  
ldv-regression/test15_true-unreach-call_true-termination.c true 2 wit inspect 2.8 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 8.1   290  
ldv-regression/test16_true-unreach-call_true-termination.c true 2 wit inspect 2.8 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 8.0   290  
ldv-regression/test17_true-unreach-call_true-termination.c true 2 wit inspect 2.9 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 5.6   260  
ldv-regression/test18_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.0 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  260 true 2 wit inspect 5.6   230  
ldv-regression/test19_true-unreach-call_true-termination.c true 2 wit inspect 2.9 270 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 12     360  
ldv-regression/test20_true-unreach-call_true-termination.c true 2 wit inspect 2.8 270 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 6.0   260  
ldv-regression/test21_true-unreach-call_true-termination.c true 2 wit inspect 3.0 270 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 9.2   310  
ldv-regression/test22_true-unreach-call.c true 2 wit inspect 6.0 370 49 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.1  290 true 2 wit inspect 22     650  
ldv-regression/test23_true-unreach-call.c true 2 wit inspect 29   1700 250 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.8  300 true 2 wit inspect 230     770  
ldv-regression/test24_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 3.3 290 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 9.3   420  
ldv-regression/test25_true-unreach-call.c true 2 wit inspect 5.6 310 46 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 18    440 true 2 wit inspect 29     560  
ldv-regression/test26_true-unreach-call_true-termination.c true 2 wit inspect 2.9 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 8.0   290  
ldv-regression/test27_true-unreach-call_true-termination.c false(unreach-call) -16 wit inspect 4.9 320 47 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  260 out of memory 0 wit inspect 56     7000  
ldv-regression/test28_true-unreach-call_true-termination.c true 2 wit inspect 2.9 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 7.2   270  
ldv-regression/test29_true-unreach-call_true-termination.c true 2 wit inspect 2.8 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 8.1   320  
ldv-regression/test30_true-unreach-call_true-termination.c true 2 wit inspect 3.0 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 11     450  
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 5.0 310 47 true -32 wit inspect 8.0  270 true -32 wit inspect 12     470   unknown 0 wit inspect 5.0  270 false(unreach-call) 1 wit inspect 1.1    19    - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 5.0 310 44 true -32 wit inspect 6.6  290 true -32 wit inspect 12     470   unknown 0 wit inspect 5.2  270 false(unreach-call) 1 wit inspect 1.1    19    - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 5.6 310 45 true -32 wit inspect 7.2  270 true -32 wit inspect 14     470   unknown 0 wit inspect 5.1  290 false(unreach-call) 1 wit inspect 1.1    19    - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 2.9 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.9  270 true 2 wit inspect 12     430  
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 3.1 270 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.2  280 true 2 wit inspect 12     430  
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 2.9 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.3  280 true 2 wit inspect 12     430  
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 2.9 270 30 - 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 3.0 270 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.7  280 true 2 wit inspect 12     420  
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 2.9 270 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.2  280 true 2 wit inspect 13     430  
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 3.0 260 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.5  280 true 2 wit inspect 15     430  
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 3.0 260 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.9  280 true 2 wit inspect 13     440  
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 2.9 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.2  280 true 2 wit inspect 13     430  
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 2.9 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.8  280 true 2 wit inspect 11     430  
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 20   710 170 true -32 wit inspect 3.9  260 true -32 wit inspect 5.8   260   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .67   19    - wit inspect - wit inspect
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.5 300 43 true -32 wit inspect 4.5  260 false(unreach-call) 1 wit inspect 9.4   350   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .67   18    - wit inspect - wit inspect
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 3.7 290 38 true -32 wit inspect 3.7  260 true -32 wit inspect 5.2   250   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .66   19    - wit inspect - wit inspect
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 4.6 300 42 error (invalid witness file) 0 wit inspect .54 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 .0014 .26 - wit inspect - wit inspect
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 3.9 300 34 true -32 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 6.3   290   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i witness invalid (false(unreach-call)) 0 wit inspect 4.3 310 40 true -32 wit inspect 3.2  260 true -32 wit inspect 5.5   250   unknown 0 wit inspect 3.1  210 error (invalid witness file) 0 wit inspect .61   18    - wit inspect - wit inspect
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 3.5 290 30 true -32 wit inspect 3.6  260 true -32 wit inspect 6.3   300   unknown 0 wit inspect 2.3  210 false(unreach-call) 1 wit inspect .68   19    - wit inspect - wit inspect
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 3.7 290 31 true -32 wit inspect 3.9  260 true -32 wit inspect 5.7   250   unknown 0 wit inspect 3.3  210 false(unreach-call) 1 wit inspect .65   19    - wit inspect - wit inspect
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 3.5 290 29 true -32 wit inspect 3.9  260 true -32 wit inspect 5.4   240   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .67   18    - wit inspect - wit inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(unreach-call) 0 wit inspect 30   1200 240 true -32 wit inspect 4.0  260 true -32 wit inspect 5.6   260   unknown 0 wit inspect 3.3  210 error (2) 0 wit inspect .68   19    - wit inspect - wit inspect
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 9.4 470 72 true -32 wit inspect 4.6  280 true -32 wit inspect 5.6   250   unknown 0 wit inspect 3.5  210 true -32 wit inspect .66   19    - wit inspect - wit inspect
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.5 310 39 true -32 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 9.8   380   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .66   19    - wit inspect - wit inspect
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 3.7 290 32 true -32 wit inspect 3.6  260 true -32 wit inspect 5.9   240   unknown 0 wit inspect 2.3  210 false(unreach-call) 1 wit inspect .66   19    - wit inspect - wit inspect
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 4.4 300 40 error (invalid witness file) 0 wit inspect .58 43 error (2) 0 wit inspect .020 5.0 error (invalid witness file) 0 wit inspect .85 47 error (invalid witness file) 0 wit inspect .0013 .27 - wit inspect - wit inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 3.8 290 36 true -32 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 7.2   290   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .70   18    - wit inspect - wit inspect
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 6.0 340 52 true -32 wit inspect 3.8  260 true -32 wit inspect 5.5   240   unknown 0 wit inspect 3.3  210 true -32 wit inspect .67   19    - wit inspect - wit inspect
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 3.6 290 29 true -32 wit inspect 4.4  260 true -32 wit inspect 5.2   240   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .65   19    - wit inspect - wit inspect
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 5.2 310 48 true -32 wit inspect 3.8  260 true -32 wit inspect 5.7   250   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .66   19    - wit inspect - wit inspect
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 3.4 280 32 true -32 wit inspect 3.5  260 true -32 wit inspect 5.3   240   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .66   18    - wit inspect - wit inspect
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 71   2100 730 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1600 timeout 0 wit inspect 960     1100  
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 7.3 400 64 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1600 timeout 0 wit inspect 960     1100  
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 12   490 95 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1000 timeout 0 wit inspect 960     960  
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 4.5 300 39 - 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
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 8.8 460 71 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1100 timeout 0 wit inspect 960     1200  
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 4.3 310 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  260 true 2 wit inspect 6.4   250  
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 29   1200 300 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3000 timeout 0 wit inspect 960     1100  
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 6.9 450 55 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3300 timeout 0 wit inspect 960     760  
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 5.9 310 47 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4100 timeout 0 wit inspect 960     1200  
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.4 280 35 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2300 timeout 0 wit inspect 960     720  
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 37   1300 290 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2300 timeout 0 wit inspect 960     1500  
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   5900 9800 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 43 error (2) 0 wit inspect .019 4.8
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 6.5 370 59 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1900 timeout 0 wit inspect 960     1800  
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 11   470 89 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    1200 timeout 0 wit inspect 960     920  
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 4.7 310 39 - 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-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 7.8 460 61 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2000 timeout 0 wit inspect 960     1100  
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 6.8 420 56 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .018 4.9
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 29   1200 230 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    3700 timeout 0 wit inspect 960     1100  
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 8.5 450 64 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4400 timeout 0 wit inspect 960     940  
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 6.0 330 50 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    4900 timeout 0 wit inspect 960     1300  
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 4.8 290 39 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2900 timeout 0 wit inspect 960     740  
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 14   490 100 timeout 0 wit inspect 91    1900 true -32 wit inspect 5.1   240   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .63   19    - wit inspect - wit inspect
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i unknown 0 wit inspect 35   980 300 error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect .88 49 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup_true-termination.i false(unreach-call) 1 wit inspect 4.3 290 39 timeout 0 wit inspect 92    1700 true -32 wit inspect 7.0   320   unknown 0 wit inspect 2.2  210 false(unreach-call) 1 wit inspect .67   18    - wit inspect - wit inspect
list-ext2-properties/list_and_tree_cnstr_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect 5.8 320 55 true -32 wit inspect 4.5  260 true -32 wit inspect 7.1   310   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .68   19    - wit inspect - wit inspect
list-ext2-properties/list_and_tree_cnstr_true-unreach-call_false-termination.i true 2 wit inspect 6.6 390 51 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5000 timeout 0 wit inspect 960     1400  
list-ext2-properties/simple_and_skiplist_2lvl_false-unreach-call.i false(unreach-call) 0 wit inspect 3.7 290 30 true -32 wit inspect 3.6  260 true -32 wit inspect 5.9   250   unknown 0 wit inspect 3.3  210 true -32 wit inspect .64   18    - wit inspect - wit inspect
list-ext2-properties/simple_and_skiplist_2lvl_true-unreach-call.i true 2 wit inspect 4.5 290 45 - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6000 timeout 0 wit inspect 960     1100  
list-ext2-properties/simple_search_value_false-unreach-call.i unknown 0 wit inspect 12   400 99 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .024 5.0 error (invalid witness file) 0 wit inspect .89 50 error (invalid witness file) 0 wit inspect .0014 .27 - wit inspect - wit inspect
list-ext2-properties/simple_search_value_true-unreach-call.i unknown 0 wit inspect 11   400 91 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .024 4.8
ldv-sets/test_add_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 4.2 300 38 true -32 wit inspect 4.1  260 true -32 wit inspect 5.2   240   unknown 0 wit inspect 3.6  210 error (1) 0 wit inspect .61   19    - wit inspect - wit inspect
ldv-sets/test_mutex_double_lock_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 4.7 300 39 true -32 wit inspect 4.3  260 true -32 wit inspect 5.9   250   unknown 0 wit inspect 3.9  210 error (1) 0 wit inspect .62   19    - wit inspect - wit inspect
ldv-sets/test_mutex_double_unlock_false-unreach-call.i unknown 0 wit inspect 4.6 300 35 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0014 .31 - wit inspect - wit inspect
ldv-sets/test_mutex_unbounded_false-unreach-call.i false(unreach-call) 0 wit inspect 8.6 430 71 timeout 0 wit inspect 93    2300 true -32 wit inspect 6.5   270   unknown 0 wit inspect 3.6  220 error (1) 0 wit inspect .61   19    - wit inspect - wit inspect
ldv-sets/test_mutex_unlock_at_exit_false-unreach-call.i unknown 0 wit inspect 4.6 300 38 error (invalid witness file) 0 wit inspect .70 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0016 .30 - wit inspect - wit inspect
ldv-sets/test_add_true-unreach-call_true-termination.i true 2 wit inspect 4.4 290 39 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.6  290 error (7) 0 wit inspect 360     830  
ldv-sets/test_mutex_true-unreach-call.i unknown 0 wit inspect 4.6 310 41 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .54 43 error (2) 0 wit inspect .020 4.9
ldv-sets/test_mutex_unbounded_true-unreach-call.i unknown 0 wit inspect 33   1400 320 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .019 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 71 2000 74000 20000 71 -1855 520   22000 71 -1457 580 38000 71 0 200 13000 71 -441 41 1200 110 144 24000 100000 110 110 26000 65000
    correct results 135 231 780 48000 7000 1 1 3.7 260 15 15 130 4700 0 39 39 26 720 72 144 340 19000 71 142 1200 25000
        correct true 96 192 600 36000 5400 0 0 0 0 72 144 340 19000 71 142 1200 25000
        correct false 39 39 180 12000 1600 1 1 3.7 260 15 15 130 4700 0 39 39 26 720 0 0
    correct-unconfimed results 21 0 150 9000 1300 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 21 0 150 9000 1300 0 0 0 0 0 0
    incorrect results 7 -160 54 3000 480 58 -1856 220   15000 46 -1472 280 12000 0 15 -480 10 280 0 2 -32 14 560
        incorrect true 3 -96 39 1800 340 58 -1856 220   15000 46 -1472 280 12000 0 15 -480 10 280 0 0
        incorrect false 4 -64 16 1200 140 0 0 0 0 0 2 -32 14 560
score (181 tasks, max score: 291) 71 -1855 -1457 0 -441 144 110
Run set cpa-bam-slicing.sv-comp18.ReachSafety-Heap cpa-seq-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Heap uautomizer-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-cpa-bam-slicing.sv-comp18-violation-witness.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-cpa-bam-slicing.sv-comp18-correctness-witness.ReachSafety-Heap uautomizer-validate-correctness-witnesses-cpa-bam-slicing.sv-comp18-correctness-witness.ReachSafety-Heap