Tool ESBMC ESBMC version 4.6.0 64-bit x86_64 linux 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* [apollon073; apollon077; apollon078; apollon119; apollon130] apollon* [apollon077; apollon078; apollon091; apollon114] apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 33553 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-01 12:59:33 CET 2017-12-02 09:20:19 CET 2017-12-02 10:53:45 CET 2017-12-02 11:06:16 CET 2017-12-02 11:21:21 CET 2017-12-02 06:57:43 CET 2017-12-02 09:56:59 CET
Run set esbmc-kind.sv-comp18.ReachSafety-Heap cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-Heap uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.ReachSafety-Heap uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.ReachSafety-Heap
Options -s kinduction -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-01_1259.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/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-01_1259.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/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-kind.2017-12-01_1259.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/esbmc-kind.2017-12-01_1259.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 3.5   89 40    0 3.7  210 -32 6.4   260   0 2.2  210 0 .62   18    - -
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i 0 900     12000 5700    0 .50 41 0 .020 4.8 0 .66 49 0 .0011 .26 - -
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i 1 .40  29 3.1  1 4.5  270 -32 7.5   300   0 2.4  210 -32 .64   18    - -
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i 0 1.1   30 9.6  0 6.1  280 -32 6.0   260   0 2.5  220 -32 .64   18    - -
heap-manipulation/tree_false-unreach-call_false-valid-deref.i 0 .69  29 5.8  0 1.8  180 -32 7.0   280   0 2.9  190 0 .59   18    - -
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i 0 .73  29 5.2  0 2.8  180 -32 8.2   290   0 2.9  190 0 .58   18    - -
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i 0 900     11000 8200    - - - - 0 .55 43 0 .025 4.8
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i 0 900     3200 7000    - - - - 0 .72 42 0 .019 4.9
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i 0 900     12000 6600    - - - - 0 .68 41 0 .019 4.8
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i 0 900     4500 9800    - - - - 0 .54 42 0 .026 5.0
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i 0 900     3000 10000    - - - - 0 .54 43 0 .018 4.9
heap-manipulation/tree_true-unreach-call.i 0 900     4200 8600    - - - - 0 .57 43 0 .024 4.9
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i 1 .34  29 3.2  1 3.9  270 -32 3.4   230   0 2.2  210 -32 .66   18    - -
list-properties/list_false-unreach-call_false-valid-memcleanup.i 1 .57  30 6.1  1 4.7  270 1 6.0   260   0 2.3  210 -32 .67   18    - -
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i 1 .36  29 2.9  1 3.9  270 1 4.1   270   0 3.1  210 1 .63   18    - -
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i 1 .93  29 8.1  1 4.1  270 -32 6.4   280   0 3.4  210 1 .65   18    - -
list-properties/simple_false-unreach-call_false-valid-memcleanup.i 1 .37  29 4.0  1 2.6  270 1 6.1   270   0 2.3  210 -32 .65   18    - -
list-properties/splice_false-unreach-call_false-valid-memcleanup.i 1 .39  29 3.5  1 4.9  270 -32 5.4   250   0 3.2  210 -32 .63   18    - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i 0 900     5400 8600    - - - - 0 .62 44 0 .019 5.0
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i 0 900     3400 10000    - - - - 0 .59 43 0 .020 4.8
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i 2 .30  27 3.0  - - - - 2 26    520 2 85     1100  
list-properties/list_true-unreach-call_false-valid-memtrack.i 0 900     1600 10000    - - - - 0 .74 44 0 .024 4.9
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i 0 900     2900 9100    - - - - 0 .61 41 0 .019 4.9
list-properties/simple_true-unreach-call_false-valid-memtrack.i 0 900     3400 10000    - - - - 0 .54 41 0 .021 4.8
list-properties/splice_true-unreach-call_false-valid-memtrack.i 0 900     3400 9500    - - - - 0 .52 44 0 .018 4.8
ldv-regression/1_3_true-termination.c_false-unreach-call.i 1 .21  28 2.0  1 3.0  270 1 5.4   260   0 2.0  210 1 .58   18    - -
ldv-regression/alt_test_true-termination.c_false-unreach-call.i 1 .12  29 1.1  1 3.9  270 -32 4.8   230   0 2.4  210 1 .67   19    - -
ldv-regression/callfpointer_true-termination.c_false-unreach-call.i 0 .074 26 .79 0 .57 43 0 .018 4.9 0 .86 50 0 .0015 .26 - -
ldv-regression/fo_test_true-termination.c_false-unreach-call.i 1 .18  28 1.1  1 4.1  260 -32 4.8   230   0 2.3  210 1 .64   18    - -
ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i 1 .10  28 .84 1 3.1  260 -32 5.5   270   0 1.9  180 1 .56   18    - -
ldv-regression/mutex_lock_struct_true-termination.c_false-unreach-call.i 1 .20  28 1.6  1 3.2  250 1 4.9   240   0 2.9  210 1 .56   18    - -
ldv-regression/recursive_list_true-termination.c_false-unreach-call.i 1 .19  28 1.8  1 3.3  260 -32 5.4   230   0 2.9  210 1 .57   19    - -
ldv-regression/rule57_ebda_blast_true-termination.c_false-unreach-call.i 0 .34  29 3.4  -32 4.4  260 -32 5.2   230   0 2.8  210 0 .56   18    - -
ldv-regression/rule60_list2_true-termination.c_false-unreach-call_1.i 1 .25  29 2.8  1 3.9  270 -32 5.1   240   0 3.3  210 -32 .63   18    - -
ldv-regression/stateful_check_false-unreach-call_false-termination.i 1 .24  28 2.2  1 2.4  260 -32 5.4   220   0 2.1  210 -32 .60   18    - -
ldv-regression/test_while_int_true-termination.c_false-unreach-call.i 1 .12  28 .85 1 2.2  260 -32 5.8   260   0 2.7  180 1 .58   18    - -
ldv-regression/test_while_int_true-termination.c_false-unreach-call_1.i 1 .11  28 .74 1 2.3  260 -32 5.1   250   0 2.0  210 1 .56   18    - -
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call.i 2 .073 26 .77 - - - - 2 4.0  250 2 8.5   270  
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i 2 .072 26 .78 - - - - 2 4.0  250 2 6.0   260  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call.i 2 .10  26 .67 - - - - 2 3.5  250 2 6.2   270  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call_1.i 2 .072 26 .82 - - - - 2 3.8  250 2 5.3   260  
ldv-regression/ex3_forlist_true-termination.c_true-unreach-call.i 2 .20  27 1.7  - - - - 2 21    490 2 34     730  
ldv-regression/just_assert_true-termination.c_true-unreach-call.i 2 .10  26 .74 - - - - 2 3.6  240 2 4.9   220  
ldv-regression/mutex_lock_int_true-termination.c_true-unreach-call_1.i 2 .10  26 .84 - - - - 2 3.9  250 2 6.6   260  
ldv-regression/mutex_lock_struct_true-termination.c_true-unreach-call_1.i 2 .072 26 .70 - - - - 2 3.9  250 2 4.6   260  
ldv-regression/nested_structure_noptr_true-termination.c_true-unreach-call.i 2 .084 26 .89 - - - - 2 3.3  250 2 5.9   240  
ldv-regression/nested_structure_noptr_true-unreach-call_true-termination.i 2 .097 26 .71 - - - - 2 3.6  250 2 5.9   260  
ldv-regression/nested_structure_ptr_true-termination.c_true-unreach-call.i 2 .083 26 .77 - - - - 2 3.7  250 2 13     470  
ldv-regression/nested_structure_ptr_true-unreach-call_true-termination.i 2 .095 27 .78 - - - - 2 3.6  250 2 6.6   360  
ldv-regression/nested_structure_true-termination.c_true-unreach-call.i 2 .079 26 .69 - - - - 2 3.8  250 2 7.8   280  
ldv-regression/nested_structure_true-unreach-call_true-termination.i 2 .082 26 .74 - - - - 2 3.5  250 2 9.3   290  
ldv-regression/oomInt_true-termination.c_true-unreach-call.i 2 .094 26 .74 - - - - 2 3.8  250 2 3.8   260  
ldv-regression/oomInt_true-termination.c_true-unreach-call_1.i 2 .11  26 .70 - - - - 2 3.5  250 2 4.9   250  
ldv-regression/rule57_ebda_blast_true-termination.c_true-unreach-call_1.i 2 .085 27 1.1  - - - - 2 4.1  250 2 6.8   260  
ldv-regression/rule60_list2_true-termination.c_true-unreach-call.i 2 .14  27 1.2  - - - - 2 4.8  250 2 16     650  
ldv-regression/rule60_list_true-termination.c_true-unreach-call.i 2 .11  27 .73 - - - - 2 4.7  260 2 6.4   380  
ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i 2 .11  27 .75 - - - - 2 3.6  260 2 5.4   260  
ldv-regression/structure_assignment_true-termination.c_true-unreach-call.i 2 .11  26 .68 - - - - 2 3.1  250 2 5.1   250  
ldv-regression/test_address_true-termination.c_true-unreach-call.i 2 .079 27 .76 - - - - 2 4.0  250 2 6.0   260  
ldv-regression/test_cut_trace_true-termination.c_true-unreach-call.i 2 .088 26 .65 - - - - 2 2.5  250 2 5.0   260  
ldv-regression/test_malloc-1_true-unreach-call_true-termination.i 2 .10  27 .86 - - - - 2 4.7  250 2 6.9   260  
ldv-regression/test_malloc-2_true-unreach-call_true-termination.i 2 .077 26 .92 - - - - 2 4.1  250 2 7.7   260  
ldv-regression/test_overflow_true-termination.c_true-unreach-call.i 2 .11  27 .78 - - - - 2 5.1  250 2 4.7   260  
ldv-regression/test_union_cast-1_true-unreach-call_true-termination.i 2 .17  29 1.8  - - - - 2 3.1  250 2 5.5   260  
ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i 2 .16  27 1.6  - - - - 2 3.9  250 2 4.0   280  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call.i 2 .13  27 1.5  - - - - 2 3.8  250 2 5.5   260  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call_1.i 2 .18  29 1.5  - - - - 2 3.2  250 2 5.4   260  
ldv-regression/test_union_true-termination.c_true-unreach-call.i 2 .076 26 .76 - - - - 2 3.2  250 2 3.3   260  
ldv-regression/test_union_true-termination.c_true-unreach-call_1.i 2 .099 26 .79 - - - - 2 3.4  250 2 5.4   260  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call.i 2 .097 26 .76 - - - - 2 3.4  250 2 6.5   270  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i 2 .086 26 .77 - - - - 2 3.9  250 2 6.1   270  
ldv-regression/test02_false-unreach-call_true-termination.c 1 .12  28 .79 1 2.1  260 1 4.6   220   0 1.9  180 1 .56   18    - -
ldv-regression/test06_false-unreach-call_true-termination.c 1 .082 28 .76 1 3.1  260 -32 3.6   230   0 2.0  210 1 .56   18    - -
ldv-regression/test08_false-unreach-call_true-termination.c 1 .12  28 .88 1 3.3  260 -32 4.7   230   0 1.9  180 1 .56   18    - -
ldv-regression/test12_false-unreach-call_true-termination.c 1 .10  28 1.1  1 3.9  260 1 4.9   230   0 2.9  210 1 .56   18    - -
ldv-regression/test21_false-unreach-call_true-termination.c 0 .37  28 3.1  0 2.9  160 1 5.4   260   0 2.7  170 0 .54   18    - -
ldv-regression/test22_false-unreach-call.c 0 .54  28 4.7  0 2.0  170 -32 5.5   260   0 2.6  180 0 .52   18    - -
ldv-regression/test23_false-unreach-call.c 0 2.8   31 39    0 2.7  170 -32 6.6   270   0 2.7  180 0 .53   18    - -
ldv-regression/test24_false-unreach-call.c 0 2.4   51 33    0 .54 42 0 .020 4.9 0 .65 49 0 .0017 .26 - -
ldv-regression/test25_false-unreach-call_true-termination.c 0 .93  40 11    0 .39 44 0 .021 5.0 0 .66 49 0 .0011 .26 - -
ldv-regression/test26_false-unreach-call_true-termination.c 1 .079 28 .82 1 3.0  260 -32 3.3   230   0 2.0  180 1 .56   18    - -
ldv-regression/test27_false-unreach-call_true-termination.c 1 .88  28 8.0  1 3.8  280 -32 4.7   240   0 3.0  210 0 .58   18    - -
ldv-regression/test28_false-unreach-call_true-termination.c 1 .23  28 2.7  1 2.4  260 1 5.8   260   0 2.0  210 1 .60   18    - -
ldv-regression/test29_false-unreach-call_true-termination.c 1 .40  28 3.6  -32 3.9  260 1 6.4   260   0 2.0  210 1 .61   18    - -
ldv-regression/test30_false-unreach-call_true-termination.c 1 .084 28 .84 1 2.2  260 -32 5.3   230   0 2.8  210 1 .57   18    - -
ldv-regression/test01_true-unreach-call_true-termination.c 2 .095 26 .79 - - - - 2 3.1  250 2 6.4   260  
ldv-regression/test03_true-unreach-call_true-termination.c 2 .077 26 .66 - - - - 2 3.1  250 2 8.2   270  
ldv-regression/test04_true-unreach-call_true-termination.c 2 .095 26 .86 - - - - 2 3.2  250 2 6.3   300  
ldv-regression/test05_true-unreach-call_true-termination.c 2 .079 26 .80 - - - - 2 4.1  250 2 10     490  
ldv-regression/test07_true-unreach-call_true-termination.c 2 .098 26 .71 - - - - 2 2.4  250 2 8.9   350  
ldv-regression/test09_true-unreach-call_true-termination.c 2 .086 26 .84 - - - - 2 3.2  250 2 8.5   340  
ldv-regression/test10_true-unreach-call_true-termination.c 2 .076 26 .78 - - - - 2 3.5  260 2 15     490  
ldv-regression/test11_true-unreach-call_true-termination.c 2 .073 26 .78 - - - - 2 3.3  250 2 8.1   280  
ldv-regression/test13_true-unreach-call_true-termination.c 2 .071 26 .92 - - - - 2 3.3  250 2 3.7   260  
ldv-regression/test14_true-unreach-call_true-termination.c 2 .10  26 .94 - - - - 2 3.4  250 2 7.2   280  
ldv-regression/test15_true-unreach-call_true-termination.c 2 .11  26 .63 - - - - 2 3.7  250 2 8.0   270  
ldv-regression/test16_true-unreach-call_true-termination.c 2 .077 26 .77 - - - - 2 3.3  250 2 8.0   280  
ldv-regression/test17_true-unreach-call_true-termination.c 2 .11  26 .71 - - - - 2 3.5  250 2 5.8   260  
ldv-regression/test18_true-unreach-call_true-termination.c 2 .11  26 .70 - - - - 2 3.0  250 2 7.9   300  
ldv-regression/test19_true-unreach-call_true-termination.c 2 .11  26 .65 - - - - 2 3.6  250 2 11     340  
ldv-regression/test20_true-unreach-call_true-termination.c 2 .11  26 .76 - - - - 2 3.8  250 2 6.1   270  
ldv-regression/test21_true-unreach-call_true-termination.c 2 .11  26 1.1  - - - - 2 4.1  250 2 9.1   320  
ldv-regression/test22_true-unreach-call.c 2 .98  27 13    - - - - 2 6.2  290 2 24     640  
ldv-regression/test23_true-unreach-call.c 2 2.3   30 26    - - - - 2 7.2  290 2 240     750  
ldv-regression/test24_true-unreach-call_true-termination.c 2 4.2   32 57    - - - - 2 6.8  280 2 10     430  
ldv-regression/test25_true-unreach-call.c 2 2.6   39 37    - - - - 2 16    440 2 31     550  
ldv-regression/test26_true-unreach-call_true-termination.c 2 .10  26 .68 - - - - 2 3.2  250 2 9.4   290  
ldv-regression/test27_true-unreach-call_true-termination.c 2 .20  27 2.0  - - - - 2 33    490 2 150     820  
ldv-regression/test28_true-unreach-call_true-termination.c 2 .082 26 .90 - - - - 2 3.1  250 2 8.6   270  
ldv-regression/test29_true-unreach-call_true-termination.c 2 .11  26 .73 - - - - 2 3.4  250 2 7.5   260  
ldv-regression/test30_true-unreach-call_true-termination.c 2 .10  26 .60 - - - - 2 3.1  250 2 9.9   440  
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i 1 .24  42 2.5  1 8.4  350 -32 13     470   0 5.1  290 1 1.1    19    - -
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i 1 .21  42 2.8  1 5.5  350 -32 9.5   460   0 3.3  270 1 1.1    18    - -
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i 1 .24  42 2.4  1 9.6  350 -32 14     470   0 3.2  270 1 1.1    19    - -
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i 2 .40  56 4.9  - - - - 2 6.5  280 2 14     430  
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i 2 .39  56 4.4  - - - - 2 6.9  290 2 13     440  
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i 2 .38  56 5.4  - - - - 2 5.7  280 2 12     430  
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i 2 .37  57 5.0  - - - - 2 8.2  280 2 12     430  
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i 2 .42  56 3.8  - - - - 2 6.2  280 2 13     430  
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i 2 .44  56 4.3  - - - - 2 6.5  300 2 13     430  
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i 2 .41  56 4.6  - - - - 2 6.7  280 2 13     440  
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i 2 .39  56 4.6  - - - - 2 6.9  280 2 15     430  
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i 2 .38  56 5.0  - - - - 2 6.2  280 2 13     430  
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i 2 .39  57 4.3  - - - - 2 7.8  280 2 12     430  
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i 1 .88  31 7.6  1 3.2  280 1 17     590   0 3.3  210 0 .62   18    - -
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i 1 .51  29 5.2  1 4.9  270 1 6.3   280   0 2.3  210 1 .63   18    - -
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i 1 .35  29 3.4  1 2.5  270 1 6.9   280   0 3.4  210 1 .68   18    - -
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i 1 1.1   30 10    1 2.9  270 -32 6.0   260   0 2.4  210 -32 .63   18    - -
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i 1 .57  29 4.9  1 2.9  270 -32 5.9   270   0 2.3  210 1 .63   19    - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i 1 1.1   30 8.9  1 5.5  270 -32 5.8   250   0 2.4  210 -32 .66   18    - -
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i 1 .73  29 6.2  1 2.6  270 1 6.9   290   0 2.3  210 1 .63   18    - -
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i 1 .52  29 4.3  1 3.8  270 -32 6.5   280   0 2.4  210 1 .63   18    - -
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i 0 .44  29 6.7  0 2.7  180 1 6.5   290   0 2.1  180 0 .61   18    - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i 1 .83  30 7.4  1 4.5  270 -32 6.6   300   0 2.4  210 0 .62   18    - -
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i 1 .73  29 6.6  1 2.8  270 -32 3.9   250   0 2.4  210 -32 .63   18    - -
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i 1 .49  29 4.2  1 3.9  270 1 6.2   280   0 2.3  210 1 .63   18    - -
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i 1 .29  29 3.0  1 4.0  260 1 6.3   270   0 2.3  210 1 .63   18    - -
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i 1 .91  30 10    1 5.1  270 -32 5.9   260   0 3.4  210 -32 .63   18    - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i 1 .44  29 2.9  1 2.8  260 -32 5.9   270   0 3.2  210 1 .63   18    - -
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i 1 .66  29 8.0  1 5.1  270 -32 6.3   280   0 2.3  210 -32 .63   18    - -
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i 1 .63  29 5.0  1 2.8  260 1 4.4   300   0 3.1  210 1 .63   18    - -
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i 0 .65  29 6.2  0 1.8  180 -32 6.2   290   0 2.8  180 0 .61   18    - -
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i 0 .40  29 3.6  0 3.4  180 1 6.1   270   0 2.1  180 0 .58   18    - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i 0 900     1200 9600    - - - - 0 .72 43 0 .020 4.8
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i 0 900     2500 10000    - - - - 0 .54 43 0 .019 4.9
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i 0 900     4000 10000    - - - - 0 .67 42 0 .019 4.8
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i 0 900     3900 9100    - - - - 0 .58 43 0 .018 4.9
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i 0 900     4100 7800    - - - - 0 .53 45 0 .020 4.8
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i 0 900     5800 11000    - - - - 0 .73 43 0 .019 4.9
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i 0 900     2800 9900    - - - - 0 .69 44 0 .018 4.9
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i 0 900     1900 9000    - - - - 0 .63 43 0 .021 5.0
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i 0 900     1300 9600    - - - - 0 .72 41 0 .024 4.8
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i 0 900     3100 7700    - - - - 0 .57 42 0 .019 4.8
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i 0 900     1200 9400    - - - - 0 .68 43 0 .020 4.9
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i 0 900     230 13000    - - - - 0 .54 43 0 .022 4.8
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i 0 900     2100 8900    - - - - 0 .52 41 0 .019 4.9
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i 0 900     3700 7800    - - - - 0 .59 41 0 .019 4.8
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i 0 900     3600 8200    - - - - 0 .53 42 0 .018 4.8
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i 0 900     2900 12000    - - - - 0 .56 43 0 .018 4.9
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i 0 900     3100 12000    - - - - 0 .54 42 0 .019 4.9
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i 0 900     2000 11000    - - - - 0 .56 41 0 .018 4.8
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i 0 900     1600 11000    - - - - 0 .67 43 0 .019 5.0
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i 0 900     1300 12000    - - - - 0 .56 43 0 .019 4.9
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i 0 900     2800 7600    - - - - 0 .62 44 0 .019 4.8
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i 1 .64  30 5.5  0 91    2000 -32 3.6   240   0 3.4  210 1 .65   18    - -
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i 0 6.7   44 65    0 1.9  180 0 97     2900   0 2.1  180 0 .61   19    - -
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup_true-termination.i 0 .27  29 2.4  0 2.0  170 1 4.1   270   0 1.9  180 0 .61   18    - -
list-ext2-properties/list_and_tree_cnstr_false-unreach-call_false-termination.i 1 .88  33 8.2  1 4.6  270 -32 6.4   290   0 2.4  210 1 .63   18    - -
list-ext2-properties/list_and_tree_cnstr_true-unreach-call_false-termination.i 0 900     2200 9500    - - - - 0 .59 41 0 .018 5.0
list-ext2-properties/simple_and_skiplist_2lvl_false-unreach-call.i 1 .51  30 5.3  1 4.5  260 1 6.6   280   0 3.2  210 -32 .63   18    - -
list-ext2-properties/simple_and_skiplist_2lvl_true-unreach-call.i 0 900     1800 10000    - - - - 0 .54 41 0 .017 4.8
list-ext2-properties/simple_search_value_false-unreach-call.i 1 3.3   39 33    1 5.7  310 -32 6.1   280   0 2.4  210 1 .62   19    - -
list-ext2-properties/simple_search_value_true-unreach-call.i 0 900     4500 9300    - - - - 0 .41 43 0 .019 4.9
ldv-sets/test_add_false-unreach-call_true-termination.i 0 .060 15 .28 0 .40 43 0 .023 4.8 0 .64 49 0 .0011 .26 - -
ldv-sets/test_mutex_double_lock_false-unreach-call_true-termination.i 0 .060 15 .30 0 .57 44 0 .019 4.8 0 .65 49 0 .0035 .26 - -
ldv-sets/test_mutex_double_unlock_false-unreach-call.i 0 .036 15 .23 0 .67 43 0 .021 4.9 0 .69 49 0 .0010 .29 - -
ldv-sets/test_mutex_unbounded_false-unreach-call.i 0 .061 15 .20 0 .40 43 0 .019 4.9 0 .67 49 0 .0036 .27 - -
ldv-sets/test_mutex_unlock_at_exit_false-unreach-call.i 0 .036 15 .32 0 .56 43 0 .022 4.8 0 .66 49 0 .0021 .29 - -
ldv-sets/test_add_true-unreach-call_true-termination.i 0 .063 15 .28 - - - - 0 .71 46 0 .024 4.8
ldv-sets/test_mutex_true-unreach-call.i 0 .034 15 .35 - - - - 0 .67 42 0 .023 4.8
ldv-sets/test_mutex_unbounded_true-unreach-call.i 0 .058 15 .32 - - - - 0 .62 42 0 .019 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 191 33000 140000 350000 71 -17 320   18000 71 -1259 470 20000 71 0 170 13000 71 -415 39   1100 110 142 400 21000 110 142 1100 26000
    correct results 120 191 44 3700 450 47 47 180   13000 21 21 130 5900 0 33 33 21   610 71 142 380 19000 71 142 1100 25000
        correct true 71 142 20 2200 230 0 0 0 0 71 142 380 19000 71 142 1100 25000
        correct false 49 49 24 1500 220 47 47 180   13000 21 21 130 5900 0 33 33 21   610 0 0
    correct-unconfimed results 13 0 18 450 190 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 13 0 18 450 190 0 0 0 0 0 0
    incorrect results 0 2 -64 8.4 520 40 -1280 240 11000 0 14 -448 8.9 260 0 0
        incorrect true 0 2 -64 8.4 520 40 -1280 240 11000 0 14 -448 8.9 260 0 0
        incorrect false 0 0 0 0 0 0 0
score (181 tasks, max score: 291) 191 -17 -1259 0 -415 142 142
Run set esbmc-kind.sv-comp18.ReachSafety-Heap cpa-seq-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-Heap uautomizer-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-esbmc-kind.sv-comp18-violation-witness.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.ReachSafety-Heap uautomizer-validate-correctness-witnesses-esbmc-kind.sv-comp18-correctness-witness.ReachSafety-Heap