Tool 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:29:20 CET 2017-12-01 08:07:14 CET 2017-12-01 08:15:38 CET 2017-12-01 08:19:10 CET 2017-12-01 04:11:27 CET 2017-12-01 07:35:08 CET
Run set cpa-seq.sv-comp18.ReachSafety-Heap cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Heap uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.ReachSafety-Heap uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.ReachSafety-Heap
Options -svcomp18 -heap 10000M -benchmark -timelimit 900s -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.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-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.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-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/cpa-seq.2017-11-30_1120.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/cpa-seq.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 0 950   7800 6600 0 .54 41 0 .019 4.8 0 .80 47 0 .0016 .28 - -
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i 0 640   2500 7000 -32 4.1  250 -32 6.2   270   0 3.7  250 -32 .65   19    - -
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i 1 5.7 310 51 1 4.2  260 1 11     320   0 3.8  260 1 .71   19    - -
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i 0 160   3200 1800 -32 4.2  270 0 96     720   0 4.3  220 -32 .73   19    - -
heap-manipulation/tree_false-unreach-call_false-valid-deref.i 1 18   1100 180 1 4.0  260 1 8.6   290   0 3.7  250 1 .81   19    - -
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i 1 18   1200 150 1 4.3  260 1 7.7   290   0 4.1  250 1 .65   19    - -
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i 0 900   7600 8100 - - - - 0 .59 41 0 .023 4.9
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i 0 900   4100 11000 - - - - 0 .61 44 0 .022 4.8
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i -16 630   3000 6600 - - - - 2 5.5  250 2 6.4   280  
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i 0 900   2500 11000 - - - - 0 .55 43 0 .021 4.9
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i 0 900   4800 11000 - - - - 0 .72 44 0 .022 4.9
heap-manipulation/tree_true-unreach-call.i 0 900   3900 5900 - - - - 0 .53 41 0 .021 4.9
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i 1 4.7 280 42 1 2.7  260 1 6.9   270   0 3.8  250 1 .83   18    - -
list-properties/list_false-unreach-call_false-valid-memcleanup.i 0 12   620 92 0 4.1  260 -32 12     480   0 4.6  210 -32 .64   19    - -
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i 1 4.4 280 34 1 4.1  260 1 6.9   280   0 3.4  240 1 .65   19    - -
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i 1 8.5 460 71 1 4.3  270 1 35     710   0 4.4  210 1 .80   18    - -
list-properties/simple_false-unreach-call_false-valid-memcleanup.i 1 4.0 280 33 1 4.0  260 1 7.3   270   0 3.5  250 1 .65   19    - -
list-properties/splice_false-unreach-call_false-valid-memcleanup.i 1 5.4 300 42 1 4.0  260 1 6.4   290   0 4.7  250 1 .64   19    - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i 0 900   3000 6000 - - - - 0 .63 43 0 .020 4.9
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i 0 900   2400 6900 - - - - 0 .52 41 0 .020 4.8
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i 2 24   1500 240 - - - - 2 27    520 2 68     1100  
list-properties/list_true-unreach-call_false-valid-memtrack.i 0 900   3100 6900 - - - - 0 .72 44 0 .021 4.9
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i 0 900   2300 6400 - - - - 0 .54 42 0 .021 4.9
list-properties/simple_true-unreach-call_false-valid-memtrack.i 0 900   2100 5800 - - - - 0 .63 43 0 .020 4.9
list-properties/splice_true-unreach-call_false-valid-memtrack.i 0 900   3700 5600 - - - - 0 .66 43 0 .019 4.9
ldv-regression/1_3_true-termination.c_false-unreach-call.i 1 3.4 270 31 1 3.5  260 1 5.4   270   0 3.0  180 1 .69   18    - -
ldv-regression/alt_test_true-termination.c_false-unreach-call.i 1 5.1 300 46 1 3.8  260 1 8.7   270   0 4.1  220 1 .73   18    - -
ldv-regression/callfpointer_true-termination.c_false-unreach-call.i 1 2.6 250 23 1 3.1  260 1 5.5   230   0 2.6  210 1 .71   18    - -
ldv-regression/fo_test_true-termination.c_false-unreach-call.i 1 3.5 270 30 1 4.4  260 0 11     290   0 4.1  210 1 .64   18    - -
ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i 1 3.2 270 27 1 3.2  260 1 4.8   250   0 3.0  210 1 .70   18    - -
ldv-regression/mutex_lock_struct_true-termination.c_false-unreach-call.i 1 3.1 270 28 1 3.4  260 1 4.8   250   0 3.1  190 1 .59   18    - -
ldv-regression/recursive_list_true-termination.c_false-unreach-call.i 1 2.7 260 24 1 2.3  260 1 6.0   270   0 3.0  190 1 .63   18    - -
ldv-regression/rule57_ebda_blast_true-termination.c_false-unreach-call.i 1 2.8 260 23 1 3.5  260 1 8.0   270   0 2.9  190 0 .60   18    - -
ldv-regression/rule60_list2_true-termination.c_false-unreach-call_1.i 1 4.0 280 32 1 3.8  270 1 14     500   0 4.0  210 -32 .64   19    - -
ldv-regression/stateful_check_false-unreach-call_false-termination.i 1 3.3 270 33 1 3.6  260 1 7.0   280   0 3.2  210 -32 .74   19    - -
ldv-regression/test_while_int_true-termination.c_false-unreach-call.i 1 2.7 260 28 1 4.2  260 1 4.9   250   0 3.1  210 1 .73   19    - -
ldv-regression/test_while_int_true-termination.c_false-unreach-call_1.i 1 2.6 250 26 1 2.3  260 1 5.0   240   0 3.3  190 1 .58   18    - -
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call.i 2 3.2 270 24 - - - - 2 3.3  250 2 6.6   280  
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i 2 2.9 260 27 - - - - 2 3.0  250 2 5.3   260  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call.i 2 3.2 260 26 - - - - 2 2.9  250 2 6.1   270  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call_1.i 2 2.9 270 25 - - - - 2 3.2  250 2 5.5   260  
ldv-regression/ex3_forlist_true-termination.c_true-unreach-call.i 2 2.6 250 24 - - - - 2 25    450 2 23     660  
ldv-regression/just_assert_true-termination.c_true-unreach-call.i 2 2.5 260 19 - - - - 2 2.8  250 2 4.3   220  
ldv-regression/mutex_lock_int_true-termination.c_true-unreach-call_1.i 2 3.1 270 29 - - - - 2 3.1  250 2 6.9   260  
ldv-regression/mutex_lock_struct_true-termination.c_true-unreach-call_1.i 2 3.2 270 31 - - - - 2 3.3  250 2 7.9   270  
ldv-regression/nested_structure_noptr_true-termination.c_true-unreach-call.i 2 2.3 240 21 - - - - 2 3.2  260 2 5.4   250  
ldv-regression/nested_structure_noptr_true-unreach-call_true-termination.i 2 2.3 240 20 - - - - 2 3.0  250 2 5.4   260  
ldv-regression/nested_structure_ptr_true-termination.c_true-unreach-call.i 2 3.2 260 30 - - - - 2 3.3  250 2 9.3   470  
ldv-regression/nested_structure_ptr_true-unreach-call_true-termination.i 2 3.0 260 25 - - - - 2 3.3  250 2 9.6   390  
ldv-regression/nested_structure_true-termination.c_true-unreach-call.i 2 3.3 270 29 - - - - 2 4.0  260 2 8.2   280  
ldv-regression/nested_structure_true-unreach-call_true-termination.i 2 3.0 260 28 - - - - 2 3.5  250 2 8.5   290  
ldv-regression/oomInt_true-termination.c_true-unreach-call.i 2 2.8 260 22 - - - - 2 3.7  240 2 6.4   260  
ldv-regression/oomInt_true-termination.c_true-unreach-call_1.i 2 2.3 250 20 - - - - 2 4.2  250 2 5.2   270  
ldv-regression/rule57_ebda_blast_true-termination.c_true-unreach-call_1.i 2 2.5 240 21 - - - - 2 3.5  250 2 6.5   270  
ldv-regression/rule60_list2_true-termination.c_true-unreach-call.i 2 2.9 250 25 - - - - 2 5.0  260 2 23     660  
ldv-regression/rule60_list_true-termination.c_true-unreach-call.i 2 3.9 280 39 - - - - 2 4.1  260 2 11     400  
ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i 2 2.7 250 23 - - - - 2 4.3  250 2 5.7   260  
ldv-regression/structure_assignment_true-termination.c_true-unreach-call.i 2 3.0 270 26 - - - - 2 3.0  250 2 5.7   250  
ldv-regression/test_address_true-termination.c_true-unreach-call.i 2 3.9 280 32 - - - - 2 4.5  250 2 5.8   260  
ldv-regression/test_cut_trace_true-termination.c_true-unreach-call.i 2 2.4 250 20 - - - - 2 3.0  250 2 5.1   260  
ldv-regression/test_malloc-1_true-unreach-call_true-termination.i 2 4.1 280 32 - - - - 2 3.7  260 2 6.6   270  
ldv-regression/test_malloc-2_true-unreach-call_true-termination.i 2 4.2 280 34 - - - - 2 4.2  250 2 5.9   260  
ldv-regression/test_overflow_true-termination.c_true-unreach-call.i 2 2.9 250 24 - - - - 2 4.1  260 2 6.3   250  
ldv-regression/test_union_cast-1_true-unreach-call_true-termination.i 2 2.5 250 25 - - - - 2 3.5  250 2 6.1   260  
ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i 2 3.1 260 26 - - - - 2 3.2  250 2 5.4   280  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call.i 2 3.3 270 29 - - - - 2 3.7  250 2 5.3   260  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call_1.i 2 2.4 250 20 - - - - 2 3.1  250 2 6.4   270  
ldv-regression/test_union_true-termination.c_true-unreach-call.i 2 2.3 250 20 - - - - 2 3.3  250 2 5.0   260  
ldv-regression/test_union_true-termination.c_true-unreach-call_1.i 2 2.4 250 20 - - - - 2 2.9  250 2 5.5   260  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call.i 2 3.0 260 28 - - - - 2 3.3  250 2 5.7   270  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i 2 3.0 270 24 - - - - 2 3.0  250 2 5.8   270  
ldv-regression/test02_false-unreach-call_true-termination.c 1 2.5 260 23 1 2.1  260 1 4.6   220   0 3.2  210 1 .56   18    - -
ldv-regression/test06_false-unreach-call_true-termination.c 1 2.7 250 21 1 3.7  260 1 7.5   280   0 3.0  210 1 .58   18    - -
ldv-regression/test08_false-unreach-call_true-termination.c 1 2.6 260 23 1 3.2  260 1 5.5   260   0 2.8  180 1 .57   18    - -
ldv-regression/test12_false-unreach-call_true-termination.c 1 2.7 250 23 1 3.1  260 1 4.7   260   0 3.0  180 1 .57   18    - -
ldv-regression/test21_false-unreach-call_true-termination.c 1 2.8 250 23 1 3.3  260 1 5.8   270   0 3.0  180 1 .61   18    - -
ldv-regression/test22_false-unreach-call.c 1 3.8 280 31 1 3.5  270 1 11     440   0 4.0  210 -32 .62   19    - -
ldv-regression/test23_false-unreach-call.c 1 11   290 120 1 3.8  260 0 94     7000   0 4.2  210 -32 .60   19    - -
ldv-regression/test24_false-unreach-call.c 1 3.4 270 29 1 4.5  280 0 89     7000   0 3.2  210 -32 .59   19    - -
ldv-regression/test25_false-unreach-call_true-termination.c 1 12   310 130 1 4.2  280 0 70     7000   0 3.3  210 -32 .61   19    - -
ldv-regression/test26_false-unreach-call_true-termination.c 1 2.6 250 22 1 3.1  260 1 4.8   260   0 2.9  210 1 .63   18    - -
ldv-regression/test27_false-unreach-call_true-termination.c 1 3.2 270 28 1 3.9  270 1 66     920   0 3.0  210 0 .60   19    - -
ldv-regression/test28_false-unreach-call_true-termination.c 1 3.2 270 30 1 3.3  260 1 7.2   270   0 2.8  210 1 .57   18    - -
ldv-regression/test29_false-unreach-call_true-termination.c 1 3.4 270 28 1 3.5  260 1 7.5   260   0 3.4  180 1 .60   18    - -
ldv-regression/test30_false-unreach-call_true-termination.c 1 2.6 250 21 1 3.2  260 1 5.7   270   0 2.9  180 1 .59   18    - -
ldv-regression/test01_true-unreach-call_true-termination.c 2 2.9 260 27 - - - - 2 3.1  250 2 5.3   260  
ldv-regression/test03_true-unreach-call_true-termination.c 2 3.1 270 30 - - - - 2 3.1  250 2 6.4   270  
ldv-regression/test04_true-unreach-call_true-termination.c 2 3.4 280 26 - - - - 2 3.1  250 2 7.1   270  
ldv-regression/test05_true-unreach-call_true-termination.c 2 3.6 270 33 - - - - 2 3.7  250 2 9.9   480  
ldv-regression/test07_true-unreach-call_true-termination.c 2 3.5 290 29 - - - - 2 4.0  250 2 9.1   340  
ldv-regression/test09_true-unreach-call_true-termination.c 2 3.1 260 30 - - - - 2 3.0  250 2 8.2   340  
ldv-regression/test10_true-unreach-call_true-termination.c 2 3.2 270 29 - - - - 2 3.3  250 2 12     490  
ldv-regression/test11_true-unreach-call_true-termination.c 2 3.4 280 30 - - - - 2 3.6  250 2 7.9   270  
ldv-regression/test13_true-unreach-call_true-termination.c 2 3.0 270 27 - - - - 2 3.0  250 2 6.5   260  
ldv-regression/test14_true-unreach-call_true-termination.c 2 3.2 270 28 - - - - 2 3.6  260 2 7.2   260  
ldv-regression/test15_true-unreach-call_true-termination.c 2 3.5 290 26 - - - - 2 3.0  250 2 7.3   280  
ldv-regression/test16_true-unreach-call_true-termination.c 2 3.1 270 27 - - - - 2 3.8  250 2 9.9   290  
ldv-regression/test17_true-unreach-call_true-termination.c 2 2.9 260 29 - - - - 2 3.0  250 2 5.2   260  
ldv-regression/test18_true-unreach-call_true-termination.c 2 3.1 270 25 - - - - 2 3.7  250 2 8.7   310  
ldv-regression/test19_true-unreach-call_true-termination.c 2 3.1 260 28 - - - - 2 3.1  250 2 9.0   360  
ldv-regression/test20_true-unreach-call_true-termination.c 2 3.0 270 29 - - - - 2 3.1  250 2 5.7   280  
ldv-regression/test21_true-unreach-call_true-termination.c 2 3.4 270 29 - - - - 2 3.2  250 2 11     310  
ldv-regression/test22_true-unreach-call.c 2 5.9 290 55 - - - - 2 6.9  290 2 21     620  
ldv-regression/test23_true-unreach-call.c 2 11   330 130 - - - - 2 6.1  300 2 240     740  
ldv-regression/test24_true-unreach-call_true-termination.c 2 11   300 110 - - - - 2 5.0  280 2 11     410  
ldv-regression/test25_true-unreach-call.c 2 210   1200 2100 - - - - 2 18    480 2 31     550  
ldv-regression/test26_true-unreach-call_true-termination.c 2 3.0 270 27 - - - - 2 3.8  250 2 9.1   290  
ldv-regression/test27_true-unreach-call_true-termination.c 2 40   640 400 - - - - 2 30    420 2 180     830  
ldv-regression/test28_true-unreach-call_true-termination.c 2 3.2 270 25 - - - - 2 3.4  250 2 7.8   280  
ldv-regression/test29_true-unreach-call_true-termination.c 2 3.3 270 29 - - - - 2 3.6  250 2 7.0   260  
ldv-regression/test30_true-unreach-call_true-termination.c 2 3.2 270 28 - - - - 2 3.5  270 2 10     440  
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i 1 9.2 420 76 1 8.5  350 0 45     780   0 6.2  270 1 1.4    19    - -
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i 1 9.2 420 77 1 10    350 0 42     720   0 5.2  270 1 1.2    19    - -
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i 1 9.1 420 77 1 8.8  350 0 41     790   0 5.2  270 1 1.1    19    - -
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i 2 97   2600 1200 - - - - 2 7.1  310 2 12     440  
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i 2 97   3100 1100 - - - - 2 7.2  280 2 14     450  
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i 2 97   3000 1000 - - - - 2 7.6  320 2 12     430  
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i 2 98   2900 1000 - - - - 2 7.3  310 2 12     430  
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i 2 98   2800 1000 - - - - 2 9.1  280 2 14     490  
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i 2 98   3100 1200 - - - - 2 8.8  290 2 12     430  
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i 2 97   2800 1100 - - - - 2 7.3  320 2 15     450  
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i 2 98   3000 1100 - - - - 2 7.6  300 2 13     450  
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i 2 97   2700 950 - - - - 2 8.6  320 2 14     440  
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i 2 98   2800 1100 - - - - 2 8.1  310 2 15     450  
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i 1 210   720 2900 1 4.5  260 1 11     360   0 4.0  250 1 .65   19    - -
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i 1 4.6 280 38 1 3.8  260 1 9.9   360   0 3.5  250 1 .63   18    - -
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i 1 3.4 270 28 1 3.7  260 1 6.2   290   0 3.9  210 1 .83   18    - -
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i 0 17   640 130 0 4.2  270 -32 34     910   0 2.5  210 -32 .94   19    - -
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i 1 3.4 260 30 1 3.6  270 1 8.0   280   0 3.5  210 1 .73   18    - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i 1 15   640 140 1 4.3  270 1 7.2   310   0 3.6  260 1 .65   19    - -
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i 1 3.3 270 33 1 3.8  270 1 7.4   280   0 3.3  210 1 .66   18    - -
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i 1 4.9 290 41 1 4.0  260 1 9.4   300   0 3.9  250 1 .65   19    - -
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i 1 4.5 280 44 1 5.0  260 1 7.0   280   0 3.9  250 1 .83   18    - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i 1 240   1700 3100 1 4.6  260 1 23     570   0 3.7  250 0 .68   19    - -
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i 0 270   2300 3600 0 3.6  260 -32 7.1   250   0 4.4  210 -32 .64   18    - -
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i 1 4.4 280 34 1 3.8  250 1 9.5   370   0 4.3  250 1 .68   18    - -
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i 1 3.4 260 31 1 4.6  270 1 7.1   300   0 3.1  210 1 .68   18    - -
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i 0 17   680 130 0 4.3  270 -32 23     750   0 4.0  210 -32 .64   19    - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i 1 5.8 310 44 1 4.4  260 1 6.0   280   0 4.6  270 1 .64   18    - -
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i 1 9.0 490 68 1 4.4  260 1 8.4   300   0 3.5  250 1 .65   19    - -
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i 1 3.4 270 31 1 3.8  280 1 6.3   270   0 3.5  210 1 .64   18    - -
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i 1 35   1600 340 1 4.5  270 1 13     410   0 4.5  250 1 .64   18    - -
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i 1 4.1 280 36 1 3.7  260 1 6.3   280   0 3.7  250 1 .63   19    - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i 0 900   2400 7200 - - - - 0 .52 43 0 .020 4.9
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i 0 900   2300 5500 - - - - 0 .66 43 0 .019 4.9
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i 0 900   2000 7000 - - - - 0 .68 44 0 .020 4.9
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i 0 900   2900 8100 - - - - 0 .52 41 0 .019 5.0
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i 0 900   2700 6000 - - - - 0 .60 41 0 .020 4.9
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i 0 900   2300 8300 - - - - 0 .52 41 0 .019 5.0
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i 0 900   4000 6600 - - - - 0 .63 43 0 .021 4.9
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i 0 900   6100 7200 - - - - 0 .69 45 0 .020 4.9
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i 0 910   6200 8500 - - - - 0 .52 43 0 .020 4.8
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i 0 900   3200 5100 - - - - 0 .70 43 0 .021 4.9
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i 0 900   2300 7300 - - - - 0 .53 41 0 .020 5.0
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i 0 900   5500 10000 - - - - 0 .56 42 0 .023 4.9
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i 0 900   2400 6400 - - - - 0 .67 43 0 .024 4.9
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i 0 900   1900 6000 - - - - 0 .68 43 0 .019 4.9
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i 0 900   2900 8100 - - - - 0 .55 42 0 .022 4.8
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i 0 900   2100 5800 - - - - 0 .52 44 0 .021 4.8
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i 0 900   2000 8400 - - - - 0 .56 43 0 .022 4.9
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i 0 900   4100 6900 - - - - 0 .72 43 0 .020 4.9
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i 0 900   5900 6600 - - - - 0 .55 41 0 .019 4.9
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i 0 900   6700 8200 - - - - 0 .70 43 0 .019 4.9
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i 0 900   3500 5500 - - - - 0 .68 43 0 .019 4.9
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i 1 4.7 290 40 1 4.0  260 1 6.3   270   0 3.5  250 1 .67   19    - -
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i 0 900   3900 7200 0 .58 44 0 .018 5.0 0 .84 49 0 .0016 .28 - -
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup_true-termination.i 1 3.3 260 32 1 3.8  260 1 5.8   270   0 3.6  210 1 .68   18    - -
list-ext2-properties/list_and_tree_cnstr_false-unreach-call_false-termination.i 1 600   1900 7500 0 4.9  260 -32 17     510   0 3.8  210 1 .70   19    - -
list-ext2-properties/list_and_tree_cnstr_true-unreach-call_false-termination.i 0 900   1500 12000 - - - - 0 .61 41 0 .024 4.9
list-ext2-properties/simple_and_skiplist_2lvl_false-unreach-call.i 1 5.3 280 45 1 3.8  260 1 6.0   280   0 4.3  250 1 .72   19    - -
list-ext2-properties/simple_and_skiplist_2lvl_true-unreach-call.i 0 900   8200 8600 - - - - 0 .72 43 0 .021 4.8
list-ext2-properties/simple_search_value_false-unreach-call.i 1 56   2000 490 -32 4.7  270 0 97     1600   0 3.7  210 1 .68   19    - -
list-ext2-properties/simple_search_value_true-unreach-call.i 0 900   3200 7200 - - - - 0 .58 41 0 .019 4.9
ldv-sets/test_add_false-unreach-call_true-termination.i 1 4.7 290 40 1 2.9  270 1 7.1   290   0 3.5  210 0 .58   19    - -
ldv-sets/test_mutex_double_lock_false-unreach-call_true-termination.i 1 5.1 300 44 1 4.1  270 1 8.2   310   0 4.3  210 0 .62   19    - -
ldv-sets/test_mutex_double_unlock_false-unreach-call.i 1 750   7900 6600 1 5.2  280 1 11     470   0 4.9  250 0 .66   20    - -
ldv-sets/test_mutex_unbounded_false-unreach-call.i 1 88   3900 770 1 4.5  260 1 11     430   0 3.5  210 0 .59   19    - -
ldv-sets/test_mutex_unlock_at_exit_false-unreach-call.i 1 120   1500 1200 1 5.7  270 1 12     500   0 3.8  260 0 .63   19    - -
ldv-sets/test_add_true-unreach-call_true-termination.i 2 5.3 310 48 - - - - 2 6.3  290 0 380     850  
ldv-sets/test_mutex_true-unreach-call.i 2 350   3500 3700 - - - - 2 310    3600 0 960     1300  
ldv-sets/test_mutex_unbounded_true-unreach-call.i 0 900   5900 7200 - - - - 0 .56 43 0 .021 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 193 40000 250000 350000 71 -35 280 19000 71 -138 1200 47000 71 0 260 16000 71 -335 47   1300 110 148 730 25000 110 144 2500 28000
    correct results 136 209 4200 91000 45000 61 61 250 16000 54 54 510 18000 0 49 49 34   910 74 148 700 24000 72 144 1100 26000
        correct true 73 146 1800 51000 19000 0 0 0 0 74 148 700 24000 72 144 1100 26000
        correct false 63 63 2400 39000 25000 61 61 250 16000 54 54 510 18000 0 49 49 34   910 0 0
    correct-unconfimed results 6 0 1100 9800 13000 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 6 0 1100 9800 13000 0 0 0 0 0 0
    incorrect results 1 -16 630 3000 6600 3 -96 13 790 6 -192 99 3200 0 12 -384 8.0 230 0 0
        incorrect true 0 3 -96 13 790 6 -192 99 3200 0 12 -384 8.0 230 0 0
        incorrect false 1 -16 630 3000 6600 0 0 0 0 0 0
score (181 tasks, max score: 291) 193 -35 -138 0 -335 148 144
Run set cpa-seq.sv-comp18.ReachSafety-Heap cpa-seq-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Heap uautomizer-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-cpa-seq.sv-comp18-violation-witness.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.ReachSafety-Heap uautomizer-validate-correctness-witnesses-cpa-seq.sv-comp18-correctness-witness.ReachSafety-Heap