Tool CPAchecker 1.6.1-svn 26725 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]
Date of execution 2017-11-30 11:20:26 CET 2017-12-01 07:36:53 CET 2017-12-01 08:24:12 CET 2017-12-01 08:27:09 CET 2017-12-01 08:31:26 CET 2017-12-01 04:24:37 CET 2017-12-01 07:42:15 CET
Run set cpa-bam-bnb.sv-comp18.ReachSafety-Heap cpa-seq-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Heap uautomizer-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-cpa-bam-bnb.sv-comp18-correctness-witness.ReachSafety-Heap uautomizer-validate-correctness-witnesses-cpa-bam-bnb.sv-comp18-correctness-witness.ReachSafety-Heap
Options -svcomp18-bam-bnb -disable-java-assertions -heap 10000m -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-bam-bnb.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-bnb.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-bnb.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-bnb.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-bnb.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cpa-bam-bnb.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 8.4 450 66 true -32 wit inspect 5.4  260 false(unreach-call) 1 wit inspect 9.7   330   unknown 0 wit inspect 4.6  250 false(unreach-call) 1 wit inspect .70   19    - wit inspect - wit inspect
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   7500 8600 error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .024 4.8 error (invalid witness file) 0 wit inspect .95 49 error (invalid witness file) 0 wit inspect .0014 .34 - wit inspect - wit inspect
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 5.6 320 50 false(unreach-call) 1 wit inspect 4.0  270 false(unreach-call) 1 wit inspect 8.2   330   unknown 0 wit inspect 4.0  210 true -32 wit inspect .64   19    - wit inspect - wit inspect
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 8.7 450 68 false(unreach-call) 1 wit inspect 4.3  270 false(unreach-call) 1 wit inspect 8.2   320   unknown 0 wit inspect 3.9  220 true -32 wit inspect .66   19    - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 7.6 440 68 false(unreach-call) 1 wit inspect 4.1  260 true -32 wit inspect 7.2   250   unknown 0 wit inspect 3.4  220 true -32 wit inspect .66   19    - wit inspect - wit inspect
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 7.4 430 60 false(unreach-call) 1 wit inspect 4.4  270 true -32 wit inspect 6.4   260   unknown 0 wit inspect 3.6  210 true -32 wit inspect .66   19    - wit inspect - wit inspect
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   6800 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .021 4.9
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   6300 9600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .019 4.8
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   7600 9700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 44 error (2) 0 wit inspect .018 4.8
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   5900 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 43 error (2) 0 wit inspect .019 4.8
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   6100 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 41 error (2) 0 wit inspect .021 4.8
heap-manipulation/tree_true-unreach-call.i timeout 0 wit inspect 900   5600 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 41 error (2) 0 wit inspect .019 4.8
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 5.5 320 50 false(unreach-call) 1 wit inspect 3.8  260 false(unreach-call) 1 wit inspect 7.0   280   unknown 0 wit inspect 3.9  210 true -32 wit inspect .65   18    - wit inspect - wit inspect
list-properties/list_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   4200 5700 error (invalid witness file) 0 wit inspect .54 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect 1.0  49 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect - wit inspect
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.8 310 47 false(unreach-call) 1 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 5.9   270   unknown 0 wit inspect 4.2  210 false(unreach-call) 1 wit inspect .64   18    - wit inspect - wit inspect
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 5.1 300 46 true -32 wit inspect 3.9  270 true -32 wit inspect 30     700   unknown 0 wit inspect 3.4  210 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.7 320 40 false(unreach-call) 1 wit inspect 3.9  270 false(unreach-call) 1 wit inspect 5.8   270   unknown 0 wit inspect 3.1  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 5.4 330 44 false(unreach-call) 1 wit inspect 3.8  270 false(unreach-call) 1 wit inspect 6.4   270   unknown 0 wit inspect 3.8  210 true -32 wit inspect .63   19    - wit inspect - wit inspect
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   4200 7900 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .019 4.8
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   7100 8600 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .020 4.8
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i false(unreach-call) -16 wit inspect 5.6 300 42 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  270 true 2 wit inspect 30     700  
list-properties/list_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   6400 9700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .019 4.8
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   8000 9700 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .025 5.0
list-properties/simple_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   6600 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 43 error (2) 0 wit inspect .023 4.8
list-properties/splice_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   4400 6100 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .020 4.9
ldv-regression/1_3_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.8 310 35 true -32 wit inspect 3.3  250 false(unreach-call) 1 wit inspect 5.3   260   unknown 0 wit inspect 3.1  190 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/alt_test_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 5.5 330 45 true -32 wit inspect 3.6  260 false(unreach-call) 1 wit inspect 7.1   270   unknown 0 wit inspect 4.0  210 false(unreach-call) 1 wit inspect .68   18    - wit inspect - wit inspect
ldv-regression/callfpointer_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.3 280 30 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 5.6   230   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/fo_test_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 4.8 320 40 true -32 wit inspect 3.6  260 unknown 0 wit inspect 12     280   unknown 0 wit inspect 4.1  220 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 3.2 280 31 true -32 wit inspect 3.4  260 false(unreach-call) 1 wit inspect 5.2   250   unknown 0 wit inspect 3.2  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
ldv-regression/mutex_lock_struct_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.3 280 33 true -32 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 5.9   260   unknown 0 wit inspect 3.0  180 false(unreach-call) 1 wit inspect .58   19    - wit inspect - wit inspect
ldv-regression/recursive_list_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.6 290 33 false(unreach-call) 1 wit inspect 3.5  260 false(unreach-call) 1 wit inspect 6.4   260   unknown 0 wit inspect 3.5  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/rule57_ebda_blast_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 4.2 290 39 true -32 wit inspect 3.7  270 false(unreach-call) 1 wit inspect 6.5   270   unknown 0 wit inspect 3.3  190 error (2) 0 wit inspect .61   18    - wit inspect - wit inspect
ldv-regression/rule60_list2_true-termination.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect 6.0 310 45 true -32 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 13     500   unknown 0 wit inspect 3.4  210 true -32 wit inspect .67   19    - wit inspect - wit inspect
ldv-regression/stateful_check_false-unreach-call_false-termination.i false(unreach-call) 1 wit inspect 4.2 290 38 true -32 wit inspect 4.3  260 false(unreach-call) 1 wit inspect 6.1   290   unknown 0 wit inspect 4.2  210 true -32 wit inspect .61   19    - wit inspect - wit inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.6 290 31 false(unreach-call) 1 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 5.2   250   unknown 0 wit inspect 3.1  190 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/test_while_int_true-termination.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect 3.5 290 28 false(unreach-call) 1 wit inspect 3.0  260 false(unreach-call) 1 wit inspect 4.0   270   unknown 0 wit inspect 3.1  210 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 2.8 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 7.6   270  
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.8 270 22 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 5.3   260  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call.i true 2 wit inspect 2.8 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 6.5   270  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.8 270 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 6.8   260  
ldv-regression/ex3_forlist_true-termination.c_true-unreach-call.i error 0 wit inspect 5.5 300 44 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .66 43 error (2) 0 wit inspect .022 4.9
ldv-regression/just_assert_true-termination.c_true-unreach-call.i true 2 wit inspect 2.6 270 22 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  240 true 2 wit inspect 4.5   230  
ldv-regression/mutex_lock_int_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.9 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 7.0   260  
ldv-regression/mutex_lock_struct_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.8 270 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 7.7   280  
ldv-regression/nested_structure_noptr_true-termination.c_true-unreach-call.i true 2 wit inspect 2.8 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 4.8   240  
ldv-regression/nested_structure_noptr_true-unreach-call_true-termination.i true 2 wit inspect 2.8 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.3   260  
ldv-regression/nested_structure_ptr_true-termination.c_true-unreach-call.i true 2 wit inspect 3.0 300 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 11     470  
ldv-regression/nested_structure_ptr_true-unreach-call_true-termination.i true 2 wit inspect 3.1 290 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 12     420  
ldv-regression/nested_structure_true-termination.c_true-unreach-call.i true 2 wit inspect 3.0 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 9.6   280  
ldv-regression/nested_structure_true-unreach-call_true-termination.i true 2 wit inspect 2.9 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  250 true 2 wit inspect 7.7   290  
ldv-regression/oomInt_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.7  250 true 2 wit inspect 7.2   320  
ldv-regression/oomInt_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.7 270 27 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 5.3   270  
ldv-regression/rule57_ebda_blast_true-termination.c_true-unreach-call_1.i true 2 wit inspect 3.5 300 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  260 true 2 wit inspect 6.7   260  
ldv-regression/rule60_list2_true-termination.c_true-unreach-call.i true 2 wit inspect 4.3 280 33 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  260 error (7) 0 wit inspect 7.5   200  
ldv-regression/rule60_list_true-termination.c_true-unreach-call.i true 2 wit inspect 4.1 300 39 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 11     380  
ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i true 2 wit inspect 3.1 270 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  250 true 2 wit inspect 5.5   260  
ldv-regression/structure_assignment_true-termination.c_true-unreach-call.i true 2 wit inspect 2.8 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  240 true 2 wit inspect 6.3   260  
ldv-regression/test_address_true-termination.c_true-unreach-call.i true 2 wit inspect 3.3 270 31 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4  250 true 2 wit inspect 5.5   260  
ldv-regression/test_cut_trace_true-termination.c_true-unreach-call.i true 2 wit inspect 2.7 270 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  240 true 2 wit inspect 5.6   260  
ldv-regression/test_malloc-1_true-unreach-call_true-termination.i true 2 wit inspect 3.3 270 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 6.9   270  
ldv-regression/test_malloc-2_true-unreach-call_true-termination.i true 2 wit inspect 3.6 300 32 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 6.2   260  
ldv-regression/test_overflow_true-termination.c_true-unreach-call.i true 2 wit inspect 3.8 300 34 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  250 true 2 wit inspect 6.5   260  
ldv-regression/test_union_cast-1_true-unreach-call_true-termination.i true 2 wit inspect 2.8 280 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 5.7   260  
ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i true 2 wit inspect 2.8 270 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 6.1   260  
ldv-regression/test_union_cast_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  240 true 2 wit inspect 5.6   260  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.7 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 5.4   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 3.8  250 true 2 wit inspect 5.1   260  
ldv-regression/test_union_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.3  250 true 2 wit inspect 5.3   260  
ldv-regression/volatile_alias_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 3.0  260 true 2 wit inspect 5.7   270  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i true 2 wit inspect 2.7 270 25 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.4  250 true 2 wit inspect 6.1   270  
ldv-regression/test02_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.3 280 27 false(unreach-call) 1 wit inspect 2.9  260 false(unreach-call) 1 wit inspect 6.0   230   unknown 0 wit inspect 3.3  180 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
ldv-regression/test06_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.7 280 33 false(unreach-call) 1 wit inspect 3.5  260 true -32 wit inspect 5.2   230   unknown 0 wit inspect 3.6  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.3 290 29 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 6.3   270   unknown 0 wit inspect 3.3  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/test12_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.2 280 28 false(unreach-call) 1 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 5.6   230   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
ldv-regression/test21_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.5 290 31 true -32 wit inspect 3.3  280 true -32 wit inspect 4.6   230   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
ldv-regression/test22_false-unreach-call.c false(unreach-call) 0 wit inspect 4.0 310 33 true -32 wit inspect 3.6  260 true -32 wit inspect 6.2   240   unknown 0 wit inspect 3.7  210 true -32 wit inspect .59   18    - wit inspect - wit inspect
ldv-regression/test23_false-unreach-call.c error 0 wit inspect 3.4 290 29 error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .021 5.0 error (invalid witness file) 0 wit inspect .97 49 error (invalid witness file) 0 wit inspect .0012 .33 - wit inspect - wit inspect
ldv-regression/test24_false-unreach-call.c false(unreach-call) 1 wit inspect 4.8 310 47 false(unreach-call) 1 wit inspect 4.3  280 out of memory 0 wit inspect 83     7000   unknown 0 wit inspect 3.9  220 true -32 wit inspect .58   19    - wit inspect - wit inspect
ldv-regression/test25_false-unreach-call_true-termination.c error 0 wit inspect 4.2 320 33 error (invalid witness file) 0 wit inspect .63 42 error (2) 0 wit inspect .018 4.9 error (invalid witness file) 0 wit inspect 1.0  50 error (invalid witness file) 0 wit inspect .0014 .30 - wit inspect - wit inspect
ldv-regression/test26_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.3 280 27 true -32 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 5.1   260   unknown 0 wit inspect 3.1  180 false(unreach-call) 1 wit inspect .56   18    - wit inspect - wit inspect
ldv-regression/test27_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 5.2 330 46 false(unreach-call) 1 wit inspect 3.7  270 false(unreach-call) 1 wit inspect 59     930   unknown 0 wit inspect 3.8  180 error (2) 0 wit inspect .59   19    - wit inspect - wit inspect
ldv-regression/test28_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.5 290 30 false(unreach-call) 1 wit inspect 3.3  260 false(unreach-call) 1 wit inspect 8.2   270   unknown 0 wit inspect 2.8  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
ldv-regression/test29_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.6 310 33 false(unreach-call) 1 wit inspect 3.2  260 false(unreach-call) 1 wit inspect 8.3   260   unknown 0 wit inspect 3.0  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
ldv-regression/test30_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 3.4 310 30 true -32 wit inspect 3.1  260 false(unreach-call) 1 wit inspect 6.3   260   unknown 0 wit inspect 2.8  180 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 2.7 270 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 5.3   260  
ldv-regression/test03_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.3  250 true 2 wit inspect 7.2   280  
ldv-regression/test04_true-unreach-call_true-termination.c true 2 wit inspect 3.0 270 22 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 8.0   280  
ldv-regression/test05_true-unreach-call_true-termination.c true 2 wit inspect 3.3 280 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5  250 true 2 wit inspect 10     480  
ldv-regression/test07_true-unreach-call_true-termination.c true 2 wit inspect 3.2 280 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 8.6   350  
ldv-regression/test09_true-unreach-call_true-termination.c true 2 wit inspect 3.0 270 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3  250 true 2 wit inspect 8.2   340  
ldv-regression/test10_true-unreach-call_true-termination.c true 2 wit inspect 3.0 270 29 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  250 true 2 wit inspect 14     470  
ldv-regression/test11_true-unreach-call_true-termination.c true 2 wit inspect 3.1 270 28 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.8  250 true 2 wit inspect 7.4   270  
ldv-regression/test13_true-unreach-call_true-termination.c true 2 wit inspect 2.8 280 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1  250 true 2 wit inspect 3.9   270  
ldv-regression/test14_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 6.8   270  
ldv-regression/test15_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.9  250 true 2 wit inspect 8.2   280  
ldv-regression/test16_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.2  250 true 2 wit inspect 7.9   280  
ldv-regression/test17_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 3.6  250 true 2 wit inspect 5.7   260  
ldv-regression/test18_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.0  250 true 2 wit inspect 8.1   300  
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 3.0  250 true 2 wit inspect 10     350  
ldv-regression/test20_true-unreach-call_true-termination.c true 2 wit inspect 2.9 280 26 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9  250 true 2 wit inspect 7.2   270  
ldv-regression/test21_true-unreach-call_true-termination.c true 2 wit inspect 3.1 270 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 8.9   310  
ldv-regression/test22_true-unreach-call.c true 2 wit inspect 6.5 380 53 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.1  290 true 2 wit inspect 25     660  
ldv-regression/test23_true-unreach-call.c error 0 wit inspect 3.7 300 32 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .019 4.8
ldv-regression/test24_true-unreach-call_true-termination.c error 0 wit inspect 3.5 310 29 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .67 44 error (2) 0 wit inspect .023 4.8
ldv-regression/test25_true-unreach-call.c error 0 wit inspect 4.3 320 36 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .51 43 error (2) 0 wit inspect .021 4.9
ldv-regression/test26_true-unreach-call_true-termination.c true 2 wit inspect 2.9 270 24 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  250 true 2 wit inspect 7.7   300  
ldv-regression/test27_true-unreach-call_true-termination.c error 0 wit inspect 6.2 340 54 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 44 error (2) 0 wit inspect .024 4.8
ldv-regression/test28_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.4  250 true 2 wit inspect 6.9   260  
ldv-regression/test29_true-unreach-call_true-termination.c true 2 wit inspect 3.1 300 23 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.2  250 true 2 wit inspect 7.0   260  
ldv-regression/test30_true-unreach-call_true-termination.c true 2 wit inspect 2.9 280 30 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 9.6   400  
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 9.0 490 70 true -32 wit inspect 6.3  270 timeout 0 wit inspect 96     1200   unknown 0 wit inspect 6.7  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 9.3 480 78 timeout 0 wit inspect 96    5200 timeout 0 wit inspect 96     1300   timeout 0 wit inspect 96    5200 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 8.9 490 73 true -32 wit inspect 6.7  270 timeout 0 wit inspect 96     1200   unknown 0 wit inspect 5.4  270 false(unreach-call) 1 wit inspect 1.2    19    - wit inspect - wit inspect
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 6.3 310 49 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.4  280 true 2 wit inspect 13     430  
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 6.3 300 50 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.2  280 true 2 wit inspect 15     450  
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 6.7 310 57 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.4  280 true 2 wit inspect 13     440  
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 6.8 310 57 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.0  280 true 2 wit inspect 12     430  
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 6.8 310 56 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.3  290 true 2 wit inspect 12     440  
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 7.0 320 53 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.4  280 true 2 wit inspect 12     430  
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 6.8 310 55 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.2  310 true 2 wit inspect 13     440  
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 6.8 310 59 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.1  280 true 2 wit inspect 13     430  
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 6.9 320 54 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.6  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 6.8 310 59 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.8  290 true 2 wit inspect 13     440  
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.6 320 37 true -32 wit inspect 4.6  260 true -32 wit inspect 12     310   unknown 0 wit inspect 3.6  210 false(unreach-call) 1 wit inspect .66   19    - wit inspect - wit inspect
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.9 330 47 unknown 0 wit inspect 3.7  260 true -32 wit inspect 70     460   unknown 0 wit inspect 2.3  210 false(unreach-call) 1 wit inspect .64   18    - wit inspect - wit inspect
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.8 320 40 false(unreach-call) 1 wit inspect 3.9  270 false(unreach-call) 1 wit inspect 7.0   280   unknown 0 wit inspect 3.9  210 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 4.7 320 39 true -32 wit inspect 4.6  260 true -32 wit inspect 9.5   300   unknown 0 wit inspect 3.4  210 true -32 wit inspect .67   18    - wit inspect - wit inspect
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 4.5 320 33 true -32 wit inspect 3.8  260 true -32 wit inspect 8.0   280   unknown 0 wit inspect 3.8  230 false(unreach-call) 1 wit inspect .63   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.5 320 41 error (invalid witness file) 0 wit inspect 2.5  170 unknown 0 wit inspect 3.1   190   error (invalid witness file) 0 wit inspect 3.5  170 error (invalid witness file) 0 wit inspect .60   18    - wit inspect - wit inspect
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 5.1 320 40 false(unreach-call) 1 wit inspect 4.3  260 false(unreach-call) 1 wit inspect 6.5   280   unknown 0 wit inspect 3.8  230 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 5.0 320 47 true -32 wit inspect 4.0  270 true -32 wit inspect 6.5   280   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .68   18    - wit inspect - wit inspect
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.6 320 43 unknown 0 wit inspect 3.7  260 true -32 wit inspect 8.1   280   unknown 0 wit inspect 3.7  210 false(unreach-call) 1 wit inspect .63   18    - wit inspect - wit inspect
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(unreach-call) 0 wit inspect 4.3 310 41 true -32 wit inspect 3.9  260 true -32 wit inspect 9.7   300   unknown 0 wit inspect 4.2  210 error (2) 0 wit inspect .69   18    - wit inspect - wit inspect
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 4.9 330 43 true -32 wit inspect 3.8  260 true -32 wit inspect 6.2   250   unknown 0 wit inspect 4.0  210 true -32 wit inspect .66   18    - wit inspect - wit inspect
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.6 320 39 true -32 wit inspect 3.6  260 true -32 wit inspect 12     380   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .69   18    - wit inspect - wit inspect
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.9 320 44 false(unreach-call) 1 wit inspect 4.1  270 false(unreach-call) 1 wit inspect 6.4   290   unknown 0 wit inspect 3.8  220 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 4.8 310 46 true -32 wit inspect 3.6  260 true -32 wit inspect 6.9   290   unknown 0 wit inspect 3.8  220 true -32 wit inspect .66   18    - wit inspect - wit inspect
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 4.5 320 42 true -32 wit inspect 3.6  260 true -32 wit inspect 7.5   290   unknown 0 wit inspect 3.5  210 false(unreach-call) 1 wit inspect .64   18    - wit inspect - wit inspect
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 0 wit inspect 4.6 310 40 true -32 wit inspect 3.8  260 true -32 wit inspect 9.4   290   unknown 0 wit inspect 3.8  210 true -32 wit inspect .65   18    - wit inspect - wit inspect
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.8 320 44 false(unreach-call) 1 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 6.4   280   unknown 0 wit inspect 4.2  210 false(unreach-call) 1 wit inspect .64   18    - wit inspect - wit inspect
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.9 320 40 true -32 wit inspect 3.8  260 true -32 wit inspect 7.0   280   unknown 0 wit inspect 3.8  210 false(unreach-call) 1 wit inspect .65   18    - wit inspect - wit inspect
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.9 320 42 true -32 wit inspect 3.8  260 true -32 wit inspect 6.6   280   unknown 0 wit inspect 3.2  210 false(unreach-call) 1 wit inspect .64   18    - wit inspect - wit inspect
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 4.3 310 39 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  280 true 2 wit inspect 9.4   300  
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 4.9 320 41 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 3.7  270 true 2 wit inspect 57     460  
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 5.6 330 48 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 5.4  270 timeout 0 wit inspect 960     1700  
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 4.7 320 37 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  260 true 2 wit inspect 10     310  
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 4.5 330 39 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 2.7  170 unknown 0 wit inspect 3.2   190  
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 4.5 320 42 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect 3.1  170 unknown 0 wit inspect 3.2   200  
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 5.1 320 43 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  260 true 2 wit inspect 11     380  
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(unreach-call) -16 wit inspect 6.2 330 49 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 3.6  260 error (7) 0 wit inspect 49     530  
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 5.0 320 46 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6  260 true 2 wit inspect 7.7   280  
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 4.6 320 41 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 4.4  260 true 2 wit inspect 8.2   280  
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 4.4 310 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  270 true 2 wit inspect 9.8   300  
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 5.0 330 41 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  260 true 2 wit inspect 6.2   250  
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 4.5 320 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  260 true 2 wit inspect 11     370  
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 5.4 330 45 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 4.9  260 true 2 wit inspect 530     1100  
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 4.9 320 40 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3  260 true 2 wit inspect 7.5   290  
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 4.6 320 41 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5  260 true 2 wit inspect 7.2   280  
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 4.7 320 38 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.0  260 true 2 wit inspect 9.6   290  
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 4.9 320 46 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.7  260 true 2 wit inspect 9.5   360  
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(unreach-call) -16 wit inspect 6.4 350 51 - wit inspect - wit inspect - wit inspect - wit inspect unknown 0 wit inspect 3.6  260 error (7) 0 wit inspect 750     820  
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 5.0 330 51 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1  270 true 2 wit inspect 6.9   290  
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 4.8 320 42 - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6  270 true 2 wit inspect 8.6   280  
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 4.8 320 44 false(unreach-call) 1 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 6.0   270   unknown 0 wit inspect 4.1  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 timeout 0 wit inspect 900   6100 10000 error (invalid witness file) 0 wit inspect .52 43 error (2) 0 wit inspect .025 4.9 error (invalid witness file) 0 wit inspect 1.0  47 error (invalid witness file) 0 wit inspect .0011 .30 - 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.5 290 37 false(unreach-call) 1 wit inspect 3.8  260 false(unreach-call) 1 wit inspect 6.9   270   unknown 0 wit inspect 3.6  210 false(unreach-call) 1 wit inspect .64   18    - wit inspect - wit inspect
list-ext2-properties/list_and_tree_cnstr_false-unreach-call_false-termination.i timeout 0 wit inspect 900   6500 12000 error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .021 4.9 error (invalid witness file) 0 wit inspect .84 47 error (invalid witness file) 0 wit inspect .0016 .26 - wit inspect - wit inspect
list-ext2-properties/list_and_tree_cnstr_true-unreach-call_false-termination.i timeout 0 wit inspect 900   5800 11000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .70 41 error (2) 0 wit inspect .022 5.0
list-ext2-properties/simple_and_skiplist_2lvl_false-unreach-call.i false(unreach-call) 1 wit inspect 4.8 310 47 false(unreach-call) 1 wit inspect 4.5  260 false(unreach-call) 1 wit inspect 7.9   280   unknown 0 wit inspect 3.3  210 true -32 wit inspect .65   18    - wit inspect - wit inspect
list-ext2-properties/simple_and_skiplist_2lvl_true-unreach-call.i timeout 0 wit inspect 910   7100 10000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 41 error (2) 0 wit inspect .020 4.8
list-ext2-properties/simple_search_value_false-unreach-call.i timeout 0 wit inspect 900   7100 12000 error (invalid witness file) 0 wit inspect .54 42 error (2) 0 wit inspect .027 4.8 error (invalid witness file) 0 wit inspect 1.1  49 error (invalid witness file) 0 wit inspect .0013 .30 - wit inspect - wit inspect
list-ext2-properties/simple_search_value_true-unreach-call.i timeout 0 wit inspect 900   7200 9500 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 44 error (2) 0 wit inspect .020 4.9
ldv-sets/test_add_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 5.4 320 46 true -32 wit inspect 3.7  260 false(unreach-call) 1 wit inspect 8.2   280   unknown 0 wit inspect 3.4  210 error (1) 0 wit inspect .58   18    - wit inspect - wit inspect
ldv-sets/test_mutex_double_lock_false-unreach-call_true-termination.i false(unreach-call) 1 wit inspect 5.8 310 51 true -32 wit inspect 4.4  260 false(unreach-call) 1 wit inspect 7.7   300   unknown 0 wit inspect 3.9  210 error (1) 0 wit inspect .59   19    - wit inspect - wit inspect
ldv-sets/test_mutex_double_unlock_false-unreach-call.i timeout 0 wit inspect 900   7700 12000 error (invalid witness file) 0 wit inspect .60 42 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .91 49 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
ldv-sets/test_mutex_unbounded_false-unreach-call.i timeout 0 wit inspect 900   7600 8600 error (invalid witness file) 0 wit inspect .58 41 error (2) 0 wit inspect .023 4.8 error (invalid witness file) 0 wit inspect .98 49 error (invalid witness file) 0 wit inspect .0012 .34 - wit inspect - wit inspect
ldv-sets/test_mutex_unlock_at_exit_false-unreach-call.i timeout 0 wit inspect 900   7900 9600 error (invalid witness file) 0 wit inspect .54 46 error (2) 0 wit inspect .024 5.0 error (invalid witness file) 0 wit inspect .85 50 error (invalid witness file) 0 wit inspect .0012 .30 - wit inspect - wit inspect
ldv-sets/test_add_true-unreach-call_true-termination.i timeout 0 wit inspect 900   7800 12000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .021 5.0
ldv-sets/test_mutex_true-unreach-call.i timeout 0 wit inspect 900   7100 9000 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .57 43 error (2) 0 wit inspect .020 4.8
ldv-sets/test_mutex_unbounded_true-unreach-call.i timeout 0 wit inspect 900   7700 9400 - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .68 41 error (2) 0 wit inspect .020 4.9
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
total 181 -168 24000 220000 260000 71 -933 330 21000 71 -605 920 28000 71 0 320 18000 71 -473 40 1100 110 158 380 23000 110 162 3000 31000
    correct results 119 184 500 36000 4400 27 27 100 7100 35 35 290 10000 0 39 39 26 720 79 158 330 20000 81 162 1300 27000
        correct true 65 130 230 18000 2100 0 0 0 0 79 158 330 20000 81 162 1300 27000
        correct false 54 54 270 18000 2300 27 27 100 7100 35 35 290 10000 0 39 39 26 720 0 0
    correct-unconfimed results 6 0 27 1900 240 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 6 0 27 1900 240 0 0 0 0 0 0
    incorrect results 22 -352 110 7100 940 30 -960 120 7900 20 -640 240 6200 0 16 -512 10 300 0 0
        incorrect true 0 30 -960 120 7900 20 -640 240 6200 0 16 -512 10 300 0 0
        incorrect false 22 -352 110 7100 940 0 0 0 0 0 0
score (181 tasks, max score: 291) -168 -933 -605 0 -473 158 162
Run set cpa-bam-bnb.sv-comp18.ReachSafety-Heap cpa-seq-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Heap uautomizer-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-cpa-bam-bnb.sv-comp18-violation-witness.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-cpa-bam-bnb.sv-comp18-correctness-witness.ReachSafety-Heap uautomizer-validate-correctness-witnesses-cpa-bam-bnb.sv-comp18-correctness-witness.ReachSafety-Heap