Tool VeriAbs CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon* [apollon020; apollon077; apollon078; apollon084; apollon149; apollon164] apollon* [apollon037; apollon065; apollon077; apollon078; apollon155; apollon159] apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-02 18:04:04 CET 2017-12-03 04:46:33 CET 2017-12-03 06:08:30 CET 2017-12-03 06:21:09 CET 2017-12-03 06:27:12 CET 2017-12-03 03:55:53 CET 2017-12-03 04:55:47 CET
Run set veriabs.sv-comp18.ReachSafety-Heap cpa-seq-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Heap uautomizer-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-veriabs.sv-comp18-correctness-witness.ReachSafety-Heap uautomizer-validate-correctness-witnesses-veriabs.sv-comp18-correctness-witness.ReachSafety-Heap
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const --full-output --validate ../../results-verified/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true --graphml-witness ../../results-verified/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/veriabs.2017-12-02_1804.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
heap-manipulation/bubble_sort_linux_false-unreach-call_false-valid-memcleanup.i 0 180   1500 2100 0 .53 41 0 .020 4.8 0 .67 51 0 .0030 .26 - -
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i 0 750   880 8800 0 .65 41 0 .019 4.9 0 .65 49 0 .0015 .31 - -
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i 0 340   550 4000 0 .57 41 0 .020 4.9 0 .69 49 0 .0046 .32 - -
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i 0 800   870 8600 0 .56 41 0 .018 4.8 0 .69 49 0 .0011 .30 - -
heap-manipulation/tree_false-unreach-call_false-valid-deref.i 0 750   570 8000 0 .44 42 0 .019 4.9 0 .65 49 0 .0012 .26 - -
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i 0 640   570 7700 0 .43 40 0 .017 4.9 0 .66 50 0 .0012 .26 - -
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i 0 180   1500 2000 - - - - 0 .70 45 0 .018 4.8
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i 0 900   2700 12000 - - - - 0 .58 43 0 .020 4.9
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i 0 730   880 10000 - - - - 0 .53 41 0 .024 4.8
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i 0 340   540 4300 - - - - 0 .55 42 0 .024 4.8
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i 0 790   850 9000 - - - - 0 .76 43 0 .022 4.8
heap-manipulation/tree_true-unreach-call.i 0 700   570 8400 - - - - 0 .57 43 0 .019 4.9
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i 0 900   3600 10000 0 .56 41 0 .019 4.9 0 .86 50 0 .0034 .26 - -
list-properties/list_false-unreach-call_false-valid-memcleanup.i 1 450   2800 5500 -32 4.4  260 1 8.6   510   0 3.1  260 1 .65   19    - -
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i 1 22   300 210 -32 3.6  250 1 5.5   270   0 3.4  210 1 .64   19    - -
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i 0 740   3700 5600 0 .56 42 0 .021 4.8 0 .85 50 0 .0017 .29 - -
list-properties/simple_false-unreach-call_false-valid-memcleanup.i 1 23   290 200 -32 4.0  250 1 6.2   260   0 3.5  250 1 .69   19    - -
list-properties/splice_false-unreach-call_false-valid-memcleanup.i 1 43   300 380 -32 2.8  250 1 4.0   280   0 2.6  250 1 .65   19    - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i 0 900   4000 9300 - - - - 0 .62 43 0 .019 4.9
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i 0 900   2600 8500 - - - - 0 .70 43 0 .022 4.9
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i 2 42   660 320 - - - - 2 25    620 2 70     1100  
list-properties/list_true-unreach-call_false-valid-memtrack.i 0 630   270 7100 - - - - 0 .69 43 0 .022 4.8
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i 0 900   4500 11000 - - - - 0 .60 43 0 .019 4.9
list-properties/simple_true-unreach-call_false-valid-memtrack.i 0 900   4200 12000 - - - - 0 .68 43 0 .018 4.8
list-properties/splice_true-unreach-call_false-valid-memtrack.i 0 900   1600 9300 - - - - 0 .54 42 0 .018 4.8
ldv-regression/1_3_true-termination.c_false-unreach-call.i 1 10   280 82 1 3.5  260 1 5.2   250   0 2.9  210 1 .59   18    - -
ldv-regression/alt_test_true-termination.c_false-unreach-call.i 0 22   250 170 0 .56 42 0 .021 5.0 0 .86 49 0 .0012 .29 - -
ldv-regression/callfpointer_true-termination.c_false-unreach-call.i -32 6.3 290 46 1 4.2  260 1 4.5   220   0 .94 52 0 .091  9.0  - -
ldv-regression/fo_test_true-termination.c_false-unreach-call.i 1 22   280 170 -32 4.2  250 0 11     280   0 2.5  250 1 .64   18    - -
ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i 1 9.0 280 85 1 3.3  260 1 4.6   250   0 2.0  210 1 .58   18    - -
ldv-regression/mutex_lock_struct_true-termination.c_false-unreach-call.i 1 9.1 280 74 1 2.3  260 1 7.4   260   0 2.0  210 1 .57   18    - -
ldv-regression/recursive_list_true-termination.c_false-unreach-call.i 1 10   280 85 1 3.5  260 1 5.4   260   0 2.7  190 1 .60   18    - -
ldv-regression/rule57_ebda_blast_true-termination.c_false-unreach-call.i 1 11   280 88 1 2.4  260 1 6.4   270   0 2.1  210 0 .59   18    - -
ldv-regression/rule60_list2_true-termination.c_false-unreach-call_1.i 0 23   250 150 0 .51 42 0 .020 4.9 0 .65 50 0 .0011 .26 - -
ldv-regression/stateful_check_false-unreach-call_false-termination.i 1 19   290 150 -32 3.7  260 1 6.3   300   0 3.2  210 1 .63   19    - -
ldv-regression/test_while_int_true-termination.c_false-unreach-call.i 1 15   280 110 1 2.3  260 1 5.4   250   0 2.0  210 1 .68   19    - -
ldv-regression/test_while_int_true-termination.c_false-unreach-call_1.i 1 14   280 130 1 2.2  260 1 4.8   240   0 2.8  180 1 .72   18    - -
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call.i 2 9.2 280 90 - - - - 2 3.1  250 2 6.1   280  
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i 2 8.1 270 73 - - - - 2 3.1  250 2 3.7   260  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call.i 2 9.1 260 71 - - - - 2 3.4  250 2 5.8   270  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call_1.i 2 7.8 270 68 - - - - 2 4.0  250 2 5.4   260  
ldv-regression/ex3_forlist_true-termination.c_true-unreach-call.i 2 31   600 260 - - - - 2 28    510 2 42     740  
ldv-regression/just_assert_true-termination.c_true-unreach-call.i 2 7.8 280 68 - - - - 2 3.0  250 2 4.5   220  
ldv-regression/mutex_lock_int_true-termination.c_true-unreach-call_1.i 2 9.6 270 76 - - - - 2 3.1  250 2 6.4   260  
ldv-regression/mutex_lock_struct_true-termination.c_true-unreach-call_1.i 2 9.8 280 82 - - - - 2 2.9  250 2 7.3   260  
ldv-regression/nested_structure_noptr_true-termination.c_true-unreach-call.i 2 7.9 270 79 - - - - 2 3.8  250 2 4.6   240  
ldv-regression/nested_structure_noptr_true-unreach-call_true-termination.i 2 7.8 270 74 - - - - 2 4.1  260 2 5.2   260  
ldv-regression/nested_structure_ptr_true-termination.c_true-unreach-call.i 2 10   280 74 - - - - 2 3.3  250 2 11     460  
ldv-regression/nested_structure_ptr_true-unreach-call_true-termination.i 2 9.5 260 79 - - - - 2 4.1  250 2 11     400  
ldv-regression/nested_structure_true-termination.c_true-unreach-call.i 2 9.7 260 91 - - - - 2 3.5  250 2 5.2   280  
ldv-regression/nested_structure_true-unreach-call_true-termination.i 2 9.8 260 78 - - - - 2 3.4  250 2 8.6   290  
ldv-regression/oomInt_true-termination.c_true-unreach-call.i 2 8.5 270 77 - - - - 2 3.2  250 2 5.5   260  
ldv-regression/oomInt_true-termination.c_true-unreach-call_1.i 2 9.0 270 71 - - - - 2 3.9  250 2 5.2   260  
ldv-regression/rule57_ebda_blast_true-termination.c_true-unreach-call_1.i 2 12   280 94 - - - - 2 3.6  260 2 7.9   270  
ldv-regression/rule60_list2_true-termination.c_true-unreach-call.i 0 22   250 160 - - - - 0 .70 43 0 .018 4.9
ldv-regression/rule60_list_true-termination.c_true-unreach-call.i 2 20   290 160 - - - - 2 4.2  250 2 9.6   380  
ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i 2 20   270 150 - - - - 2 2.5  250 2 5.3   260  
ldv-regression/structure_assignment_true-termination.c_true-unreach-call.i 2 7.9 270 68 - - - - 2 3.6  250 2 5.0   260  
ldv-regression/test_address_true-termination.c_true-unreach-call.i 2 19   270 150 - - - - 2 3.6  250 2 5.6   270  
ldv-regression/test_cut_trace_true-termination.c_true-unreach-call.i 2 7.9 260 67 - - - - 2 3.1  250 2 5.3   260  
ldv-regression/test_malloc-1_true-unreach-call_true-termination.i 2 20   280 170 - - - - 2 3.8  250 2 4.4   280  
ldv-regression/test_malloc-2_true-unreach-call_true-termination.i 2 19   280 150 - - - - 2 3.7  250 2 5.8   260  
ldv-regression/test_overflow_true-termination.c_true-unreach-call.i 2 18   280 130 - - - - 2 4.5  260 2 5.5   270  
ldv-regression/test_union_cast-1_true-unreach-call_true-termination.i 2 7.8 280 65 - - - - 2 3.8  250 2 6.8   260  
ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i 2 9.6 270 81 - - - - 2 3.6  250 2 3.9   260  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call.i 2 9.2 270 82 - - - - 2 3.0  250 2 5.3   260  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call_1.i 2 7.7 270 72 - - - - 2 2.9  250 2 5.9   260  
ldv-regression/test_union_true-termination.c_true-unreach-call.i 2 7.6 270 70 - - - - 2 2.8  250 2 5.5   260  
ldv-regression/test_union_true-termination.c_true-unreach-call_1.i 2 7.6 270 75 - - - - 2 3.8  250 2 5.4   270  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call.i 2 9.5 270 74 - - - - 2 2.9  250 2 6.3   280  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i 2 9.7 270 82 - - - - 2 3.6  250 2 5.7   270  
ldv-regression/test02_false-unreach-call_true-termination.c 1 7.3 270 66 1 3.4  250 1 4.6   220   0 2.7  210 1 .60   18    - -
ldv-regression/test06_false-unreach-call_true-termination.c 1 10   280 78 -32 4.5  260 1 5.7   270   0 2.1  210 1 .59   18    - -
ldv-regression/test08_false-unreach-call_true-termination.c 1 9.5 310 71 1 2.3  260 1 3.9   270   0 2.0  210 1 .57   18    - -
ldv-regression/test12_false-unreach-call_true-termination.c 1 8.4 270 69 1 3.3  270 1 5.5   230   0 1.9  180 1 .57   18    - -
ldv-regression/test21_false-unreach-call_true-termination.c 1 10   280 71 1 2.4  270 1 5.3   270   0 3.0  210 1 .63   18    - -
ldv-regression/test22_false-unreach-call.c 1 15   280 100 1 2.4  270 1 13     450   0 2.4  230 -32 .73   18    - -
ldv-regression/test23_false-unreach-call.c 0 19   220 150 0 .54 41 0 .017 4.9 0 .70 50 0 .0037 .26 - -
ldv-regression/test24_false-unreach-call.c 0 400   740 3100 0 .59 41 0 .026 5.0 0 .84 49 0 .0013 .26 - -
ldv-regression/test25_false-unreach-call_true-termination.c 0 61   220 610 0 .57 41 0 .019 4.9 0 .68 49 0 .0011 .26 - -
ldv-regression/test26_false-unreach-call_true-termination.c 1 10   280 73 1 2.2  260 1 4.8   260   0 2.8  210 1 .59   18    - -
ldv-regression/test27_false-unreach-call_true-termination.c 0 34   410 280 -32 3.7  260 0 59     7000   0 3.3  210 0 .60   18    - -
ldv-regression/test28_false-unreach-call_true-termination.c 1 7.6 280 71 1 3.3  260 1 4.3   270   0 3.2  210 1 .60   18    - -
ldv-regression/test29_false-unreach-call_true-termination.c 1 7.8 280 70 1 3.2  260 1 9.3   260   0 2.0  210 1 .60   18    - -
ldv-regression/test30_false-unreach-call_true-termination.c 1 10   280 76 1 3.8  260 1 5.3   260   0 2.1  210 1 .60   18    - -
ldv-regression/test01_true-unreach-call_true-termination.c 2 8.1 270 69 - - - - 2 3.4  250 2 5.5   260  
ldv-regression/test03_true-unreach-call_true-termination.c 2 9.8 270 77 - - - - 2 3.2  250 2 4.6   290  
ldv-regression/test04_true-unreach-call_true-termination.c 2 11   270 88 - - - - 2 3.9  250 2 5.8   280  
ldv-regression/test05_true-unreach-call_true-termination.c 2 11   270 87 - - - - 2 3.3  250 2 11     490  
ldv-regression/test07_true-unreach-call_true-termination.c 2 9.8 270 84 - - - - 2 3.2  250 2 9.2   350  
ldv-regression/test09_true-unreach-call_true-termination.c 2 10   280 79 - - - - 2 2.5  250 2 9.8   340  
ldv-regression/test10_true-unreach-call_true-termination.c 2 9.9 270 90 - - - - 2 4.1  250 2 16     510  
ldv-regression/test11_true-unreach-call_true-termination.c 2 10   270 84 - - - - 2 3.6  280 2 7.9   270  
ldv-regression/test13_true-unreach-call_true-termination.c 2 9.7 270 73 - - - - 2 3.4  250 2 5.5   270  
ldv-regression/test14_true-unreach-call_true-termination.c 2 10   270 78 - - - - 2 3.1  250 2 9.0   260  
ldv-regression/test15_true-unreach-call_true-termination.c 2 9.8 270 92 - - - - 2 3.8  250 2 7.0   280  
ldv-regression/test16_true-unreach-call_true-termination.c 2 10   270 89 - - - - 2 3.0  250 2 7.9   280  
ldv-regression/test17_true-unreach-call_true-termination.c 2 8.7 270 86 - - - - 2 3.8  250 2 5.4   260  
ldv-regression/test18_true-unreach-call_true-termination.c 2 9.7 270 69 - - - - 2 3.0  250 2 7.6   300  
ldv-regression/test19_true-unreach-call_true-termination.c 2 10   280 93 - - - - 2 4.0  250 2 9.1   340  
ldv-regression/test20_true-unreach-call_true-termination.c 2 9.2 270 82 - - - - 2 3.0  250 2 5.5   260  
ldv-regression/test21_true-unreach-call_true-termination.c 2 12   290 92 - - - - 2 3.3  250 2 7.9   310  
ldv-regression/test22_true-unreach-call.c 2 17   450 120 - - - - 2 6.5  300 2 21     630  
ldv-regression/test23_true-unreach-call.c 2 18   300 140 - - - - 2 8.5  310 2 160     690  
ldv-regression/test24_true-unreach-call_true-termination.c 2 17   290 130 - - - - 2 4.8  290 2 11     450  
ldv-regression/test25_true-unreach-call.c 0 56   220 570 - - - - 0 .57 43 0 .018 4.9
ldv-regression/test26_true-unreach-call_true-termination.c 2 10   270 76 - - - - 2 2.1  250 2 5.1   290  
ldv-regression/test27_true-unreach-call_true-termination.c 2 40   500 390 - - - - 2 150    990 2 170     810  
ldv-regression/test28_true-unreach-call_true-termination.c 2 8.1 270 85 - - - - 2 4.0  270 2 7.3   260  
ldv-regression/test29_true-unreach-call_true-termination.c 2 8.0 270 76 - - - - 2 3.2  250 2 7.7   260  
ldv-regression/test30_true-unreach-call_true-termination.c 2 11   270 83 - - - - 2 3.1  250 2 10     440  
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i 0 20   280 150 0 .54 42 0 .019 4.9 0 .83 49 0 .0017 .29 - -
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i 0 20   280 160 0 .57 41 0 .019 4.8 0 .83 49 0 .0012 .29 - -
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i 0 20   280 150 0 .53 41 0 .019 4.8 0 .86 50 0 .0012 .29 - -
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i 2 24   340 180 - - - - 2 7.3  290 2 13     450  
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i 2 24   350 190 - - - - 2 8.7  290 2 13     440  
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i 2 23   340 190 - - - - 2 8.1  290 2 13     430  
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i 2 24   340 190 - - - - 2 7.1  290 2 12     450  
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i 2 23   330 170 - - - - 2 7.9  280 2 14     440  
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i 2 24   340 170 - - - - 2 9.5  300 2 12     440  
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i 2 24   330 160 - - - - 2 7.7  290 2 13     440  
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i 2 23   320 180 - - - - 2 8.9  300 2 12     440  
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i 2 24   340 170 - - - - 2 8.1  280 2 12     430  
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i 2 23   350 160 - - - - 2 8.0  280 2 13     420  
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i 0 900   2000 6700 0 .53 41 0 .021 4.9 0 .84 49 0 .0018 .28 - -
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i 0 900   1000 11000 0 .51 41 0 .022 4.8 0 .64 49 0 .0013 .27 - -
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i 0 900   3900 8700 0 .58 41 0 .018 4.9 0 .64 49 0 .0010 .31 - -
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i 0 900   4100 7700 0 .41 43 0 .019 4.9 0 .80 47 0 .0016 .30 - -
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i 0 630   340 8500 0 .51 41 0 .018 4.8 0 .67 49 0 .0010 .26 - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i 0 660   410 7500 0 .58 44 0 .018 4.8 0 .84 49 0 .0012 .34 - -
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i 0 900   3000 10000 0 .40 43 0 .019 4.8 0 .70 49 0 .0017 .26 - -
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i 0 900   820 11000 0 .40 44 0 .020 4.9 0 .69 49 0 .0029 .26 - -
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i 0 900   2400 11000 0 .58 41 0 .018 4.8 0 .83 49 0 .0030 .29 - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i 0 900   1900 6200 0 .54 41 0 .020 4.9 0 .65 49 0 .0033 .29 - -
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i 0 65   610 660 0 .55 41 0 .019 4.9 0 .83 47 0 .0011 .26 - -
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i 0 900   940 9000 0 .53 41 0 .019 4.9 0 .87 47 0 .0033 .26 - -
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i 0 900   4100 7800 0 .42 44 0 .018 4.8 0 .83 49 0 .0011 .26 - -
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i 0 900   3900 7500 0 .53 41 0 .020 5.0 0 .87 49 0 .0014 .30 - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i 0 710   290 9000 0 .56 41 0 .018 5.0 0 .69 49 0 .0011 .26 - -
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i 0 620   350 7000 0 .53 42 0 .018 4.8 0 .64 49 0 .0013 .35 - -
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i 0 900   2800 12000 0 .53 41 0 .019 4.8 0 .84 49 0 .0012 .31 - -
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i 0 900   1800 11000 0 .58 41 0 .018 4.8 0 .64 49 0 .0011 .26 - -
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i 0 900   2500 9100 0 .66 44 0 .022 4.8 0 .83 49 0 .0012 .26 - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i 0 900   1400 6400 - - - - 0 .66 44 0 .019 4.9
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i 0 900   1000 10000 - - - - 0 .50 42 0 .019 4.8
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i 0 900   4300 9000 - - - - 0 .60 44 0 .019 4.9
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i 0 900   4000 8300 - - - - 0 .60 42 0 .020 5.0
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i 0 660   420 7100 - - - - 0 .55 41 0 .019 5.0
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i 0 680   410 7200 - - - - 0 .56 44 0 .019 5.0
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i 0 770   300 8600 - - - - 0 .43 44 0 .019 4.8
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i 0 900   3000 11000 - - - - 0 .59 41 0 .019 4.8
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i 0 900   820 9100 - - - - 0 .70 42 0 .024 4.9
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i 0 900   1900 9500 - - - - 0 .55 43 0 .017 4.8
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i 0 900   1500 8800 - - - - 0 .55 42 0 .018 4.9
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i 0 67   610 660 - - - - 0 .58 43 0 .020 4.8
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i 0 900   940 9000 - - - - 0 .54 43 0 .019 4.9
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i 0 900   4200 9100 - - - - 0 .54 42 0 .023 4.8
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i 0 900   3900 7400 - - - - 0 .55 41 0 .020 4.9
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i 0 550   300 7000 - - - - 0 .54 41 0 .019 5.0
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i 0 630   380 7100 - - - - 0 .63 42 0 .021 4.9
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i 0 810   260 9700 - - - - 0 .58 41 0 .018 4.9
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i 0 900   2800 10000 - - - - 0 .59 41 0 .018 4.8
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i 0 900   920 8800 - - - - 0 .71 43 0 .021 4.9
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i 0 900   2400 7700 - - - - 0 .72 44 0 .027 4.8
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i 0 900   4200 11000 0 .57 41 0 .019 4.9 0 .66 49 0 .0013 .27 - -
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i 0 900   1700 8200 0 .41 44 0 .017 4.9 0 .65 49 0 .0013 .26 - -
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup_true-termination.i 0 900   2300 9300 0 .58 42 0 .019 4.9 0 .86 50 0 .0013 .30 - -
list-ext2-properties/list_and_tree_cnstr_false-unreach-call_false-termination.i 0 530   820 6000 0 .52 42 0 .018 4.9 0 .65 49 0 .0011 .28 - -
list-ext2-properties/list_and_tree_cnstr_true-unreach-call_false-termination.i 0 530   840 5900 - - - - 0 .62 44 0 .020 4.8
list-ext2-properties/simple_and_skiplist_2lvl_false-unreach-call.i 0 750   760 8800 0 .59 41 0 .019 4.8 0 .83 47 0 .0012 .27 - -
list-ext2-properties/simple_and_skiplist_2lvl_true-unreach-call.i 0 750   760 9200 - - - - 0 .61 44 0 .024 4.8
list-ext2-properties/simple_search_value_false-unreach-call.i 0 250   3900 3100 0 92    1800 0 49     7000   0 3.9  260 0 .62   19    - -
list-ext2-properties/simple_search_value_true-unreach-call.i 0 900   3300 9000 - - - - 0 .65 41 0 .023 4.9
ldv-sets/test_add_false-unreach-call_true-termination.i 0 22   250 170 0 .40 44 0 .020 5.0 0 .87 49 0 .0016 .26 - -
ldv-sets/test_mutex_double_lock_false-unreach-call_true-termination.i 0 25   270 210 0 .61 41 0 .019 4.9 0 .86 49 0 .0012 .34 - -
ldv-sets/test_mutex_double_unlock_false-unreach-call.i 0 26   270 210 0 .54 43 0 .019 4.9 0 .87 50 0 .0013 .26 - -
ldv-sets/test_mutex_unbounded_false-unreach-call.i 0 290   4500 2700 0 .56 44 0 .018 4.8 0 .65 49 0 .0011 .26 - -
ldv-sets/test_mutex_unlock_at_exit_false-unreach-call.i 0 24   270 180 0 .55 41 0 .018 4.9 0 .84 49 0 .0013 .26 - -
ldv-sets/test_add_true-unreach-call_true-termination.i 0 22   260 160 - - - - 0 .62 43 0 .019 4.9
ldv-sets/test_mutex_true-unreach-call.i 0 26   260 230 - - - - 0 .54 41 0 .019 4.9
ldv-sets/test_mutex_unbounded_true-unreach-call.i 0 290   4500 3000 - - - - 0 .56 42 0 .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 129 55000   170000 590000 71 -239 200 10000 71 23 260 21000 71 0 100 7700 71 -11 16    480 110 138 510 21000 110 138 970 25000
    correct results 92 161 1700   30000 16000 17 17 50 4400 23 23 140 6400 0 21 21 13    390 69 138 490 19000 69 138 970 24000
        correct true 69 138 960   21000 7700 0 0 0 0 69 138 490 19000 69 138 970 24000
        correct false 23 23 750   9100 8000 17 17 50 4400 23 23 140 6400 0 21 21 13    390 0 0
    correct-unconfimed results 2 0 280   4300 3300 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 2 0 280   4300 3300 0 0 0 0 0 0
    incorrect results 1 -32 6.3 290 46 8 -256 31 2100 0 0 1 -32 .73 18 0 0
        incorrect true 1 -32 6.3 290 46 8 -256 31 2100 0 0 1 -32 .73 18 0 0
        incorrect false 0 0 0 0 0 0 0
score (181 tasks, max score: 291) 129 -239 23 0 -11 138 138
Run set veriabs.sv-comp18.ReachSafety-Heap cpa-seq-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Heap uautomizer-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-veriabs.sv-comp18-violation-witness.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-veriabs.sv-comp18-correctness-witness.ReachSafety-Heap uautomizer-validate-correctness-witnesses-veriabs.sv-comp18-correctness-witness.ReachSafety-Heap