Tool symbiotic 5.0.0-KLEE:1faddfe0-dg:12c34aac-symbiotic:5e14b94d-minisat:3db58943-llvm-instrumentation:cd767593-stp:17249213 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* [apollon005; apollon043; apollon077; apollon078; apollon087; apollon118] [apollon061; apollon077; apollon078; apollon086; apollon134] [apollon038; apollon077; apollon078; apollon083] [apollon077; apollon078; apollon161] 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 22:41:19 CET 2017-12-02 21:10:50 CET 2017-12-02 22:39:24 CET 2017-12-02 22:51:52 CET 2017-12-02 23:01:21 CET 2017-12-02 19:44:15 CET 2017-12-02 21:36:25 CET
Run set symbiotic.sv-comp18.ReachSafety-Heap cpa-seq-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Heap uautomizer-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.ReachSafety-Heap uautomizer-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.ReachSafety-Heap
Options --witness witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-01_2241.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/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-01_2241.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/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/symbiotic.2017-12-01_2241.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 1 .21 11 2.9 0 6.3  280 -32 6.3   260   0 2.7  220 1 .67   19    - -
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i 0 .23 11 3.0 0 3.8  280 -32 6.3   270   0 2.5  210 -32 .67   18    - -
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i 1 .23 11 2.7 1 4.1  270 -32 6.3   270   0 2.5  220 -32 .64   18    - -
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i 0 .21 11 2.5 0 5.2  270 -32 4.1   260   0 3.8  230 -32 .63   18    - -
heap-manipulation/tree_false-unreach-call_false-valid-deref.i 0 .20 11 2.2 0 4.6  270 -32 5.8   250   0 2.4  210 -32 .68   18    - -
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i 0 .20 11 2.2 0 5.2  270 -32 5.6   240   0 2.4  210 -32 .63   18    - -
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i 0 900    520 12000   - - - - 0 .55 44 0 .021 5.0
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i 0 900    370 11000   - - - - 0 .54 44 0 .024 4.8
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i 0 900    6400 4600   - - - - 0 .68 43 0 .019 4.9
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i 0 900    600 10000   - - - - 0 .76 43 0 .019 4.9
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i 0 900    4500 9100   - - - - 0 .42 44 0 .024 5.0
heap-manipulation/tree_true-unreach-call.i 0 900    2200 8100   - - - - 0 .58 42 0 .018 4.9
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i 1 .21 11 1.9 1 4.3  260 -32 3.5   230   0 2.4  210 -32 .62   18    - -
list-properties/list_false-unreach-call_false-valid-memcleanup.i 0 .18 11 2.4 0 4.8  270 -32 3.7   240   0 2.3  210 -32 .62   18    - -
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i 1 .19 11 2.2 1 4.6  270 -32 3.5   250   0 2.4  210 1 .62   18    - -
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i 1 .18 11 1.7 0 6.1  270 -32 6.8   230   0 2.4  210 1 .62   18    - -
list-properties/simple_false-unreach-call_false-valid-memcleanup.i 1 .20 11 2.0 1 5.0  270 -32 6.5   230   0 3.5  210 -32 .63   18    - -
list-properties/splice_false-unreach-call_false-valid-memcleanup.i 1 .21 11 2.0 1 4.3  270 -32 5.1   240   0 2.4  220 -32 .64   18    - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i 0 900    1600 7400   - - - - 0 .57 44 0 .019 5.0
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i 0 900    260 13000   - - - - 0 .62 43 0 .019 4.9
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i 2 .17 11 1.9 - - - - 2 25    530 2 73     1100  
list-properties/list_true-unreach-call_false-valid-memtrack.i 0 900    1300 10000   - - - - 0 .55 43 0 .020 4.9
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i 0 900    1500 9900   - - - - 0 .56 44 0 .019 4.9
list-properties/simple_true-unreach-call_false-valid-memtrack.i 0 900    1300 7200   - - - - 0 .58 43 0 .021 4.9
list-properties/splice_true-unreach-call_false-valid-memtrack.i 0 900    1400 8800   - - - - 0 .60 42 0 .024 5.0
ldv-regression/1_3_true-termination.c_false-unreach-call.i 1 .16 11 1.8 1 3.4  260 -32 4.4   230   0 2.8  210 1 .61   18    - -
ldv-regression/alt_test_true-termination.c_false-unreach-call.i 1 .18 11 1.6 1 5.4  280 -32 5.0   240   0 3.5  210 1 .66   18    - -
ldv-regression/callfpointer_true-termination.c_false-unreach-call.i 1 .15 11 1.7 1 3.2  250 1 4.6   230   0 2.8  180 1 .57   18    - -
ldv-regression/fo_test_true-termination.c_false-unreach-call.i 1 .20 11 2.0 1 5.4  260 -32 3.2   230   0 3.5  210 1 .63   18    - -
ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i 1 .16 11 1.8 1 3.2  260 -32 5.6   260   0 2.8  180 1 .60   18    - -
ldv-regression/mutex_lock_struct_true-termination.c_false-unreach-call.i 1 .16 11 1.6 1 3.0  260 -32 5.3   260   0 1.9  180 1 .60   18    - -
ldv-regression/recursive_list_true-termination.c_false-unreach-call.i 1 .17 11 1.5 1 3.6  260 -32 3.2   230   0 2.1  210 1 .58   18    - -
ldv-regression/rule57_ebda_blast_true-termination.c_false-unreach-call.i 1 .20 11 2.4 1 3.0  270 -32 4.8   230   0 2.9  210 0 .58   18    - -
ldv-regression/rule60_list2_true-termination.c_false-unreach-call_1.i 1 .19 11 2.3 1 3.0  270 -32 3.9   260   0 2.3  210 -32 .66   18    - -
ldv-regression/stateful_check_false-unreach-call_false-termination.i 1 .22 11 2.6 1 4.6  270 -32 4.7   230   0 2.0  210 -32 .60   18    - -
ldv-regression/test_while_int_true-termination.c_false-unreach-call.i 1 .17 11 1.6 1 4.0  250 -32 5.3   260   0 1.9  200 1 .58   18    - -
ldv-regression/test_while_int_true-termination.c_false-unreach-call_1.i 1 .15 11 1.9 1 3.0  260 -32 5.1   250   0 1.9  190 1 .59   18    - -
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call.i 2 .12 11 1.3 - - - - 2 4.2  250 2 7.4   270  
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i 2 .12 11 1.6 - - - - 2 3.2  250 2 5.9   260  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call.i 2 .15 11 1.3 - - - - 2 2.0  250 2 6.8   270  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call_1.i 2 .14 11 1.6 - - - - 2 3.5  250 2 5.2   260  
ldv-regression/ex3_forlist_true-termination.c_true-unreach-call.i 2 .18 11 1.6 - - - - 2 18    460 2 30     690  
ldv-regression/just_assert_true-termination.c_true-unreach-call.i 2 .12 11 1.4 - - - - 2 3.4  240 2 3.4   220  
ldv-regression/mutex_lock_int_true-termination.c_true-unreach-call_1.i 2 .14 11 1.2 - - - - 2 3.0  250 2 6.9   260  
ldv-regression/mutex_lock_struct_true-termination.c_true-unreach-call_1.i 2 .15 11 1.4 - - - - 2 3.0  250 2 6.4   260  
ldv-regression/nested_structure_noptr_true-termination.c_true-unreach-call.i 2 .15 11 1.3 - - - - 2 3.0  250 2 4.8   240  
ldv-regression/nested_structure_noptr_true-unreach-call_true-termination.i 2 .17 11 1.4 - - - - 2 3.4  250 2 5.6   260  
ldv-regression/nested_structure_ptr_true-termination.c_true-unreach-call.i 2 .15 11 1.5 - - - - 2 3.1  250 2 9.1   470  
ldv-regression/nested_structure_ptr_true-unreach-call_true-termination.i 2 .16 11 1.6 - - - - 2 3.5  250 2 13     400  
ldv-regression/nested_structure_true-termination.c_true-unreach-call.i 2 .15 11 1.4 - - - - 2 3.5  250 2 8.3   290  
ldv-regression/nested_structure_true-unreach-call_true-termination.i 2 .14 11 1.7 - - - - 2 3.9  250 2 8.6   290  
ldv-regression/oomInt_true-termination.c_true-unreach-call.i 2 .14 11 1.4 - - - - 2 3.5  250 2 5.9   270  
ldv-regression/oomInt_true-termination.c_true-unreach-call_1.i 2 .12 11 1.7 - - - - 2 3.6  250 2 3.7   280  
ldv-regression/rule57_ebda_blast_true-termination.c_true-unreach-call_1.i 2 .22 11 2.2 - - - - 2 3.6  250 2 6.5   270  
ldv-regression/rule60_list2_true-termination.c_true-unreach-call.i 2 .20 11 2.0 - - - - 2 5.1  270 2 15     670  
ldv-regression/rule60_list_true-termination.c_true-unreach-call.i 2 .15 11 1.6 - - - - 2 4.0  260 2 11     370  
ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i 2 .15 11 1.4 - - - - 2 4.7  260 2 4.8   260  
ldv-regression/structure_assignment_true-termination.c_true-unreach-call.i 2 .15 11 1.5 - - - - 2 3.1  250 2 4.7   250  
ldv-regression/test_address_true-termination.c_true-unreach-call.i 2 .15 11 1.6 - - - - 2 4.2  250 2 6.3   260  
ldv-regression/test_cut_trace_true-termination.c_true-unreach-call.i 2 .12 11 1.3 - - - - 2 3.0  250 2 5.1   260  
ldv-regression/test_malloc-1_true-unreach-call_true-termination.i 2 .14 11 2.0 - - - - 2 3.9  250 2 6.4   260  
ldv-regression/test_malloc-2_true-unreach-call_true-termination.i 2 .16 11 1.7 - - - - 2 3.5  250 2 6.1   260  
ldv-regression/test_overflow_true-termination.c_true-unreach-call.i 2 .14 11 1.9 - - - - 2 4.2  250 2 5.3   260  
ldv-regression/test_union_cast-1_true-unreach-call_true-termination.i 2 .14 11 1.6 - - - - 2 3.3  250 2 5.7   260  
ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i 2 .14 11 1.6 - - - - 2 3.5  250 2 5.6   260  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call.i 2 .15 11 1.6 - - - - 2 3.5  250 2 6.2   260  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call_1.i 2 .14 11 1.2 - - - - 2 3.0  250 2 5.7   260  
ldv-regression/test_union_true-termination.c_true-unreach-call.i 2 .14 11 1.5 - - - - 2 3.2  250 2 5.0   270  
ldv-regression/test_union_true-termination.c_true-unreach-call_1.i 2 .15 11 1.3 - - - - 2 2.9  250 2 3.6   260  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call.i 2 .15 11 1.6 - - - - 2 3.1  250 2 6.6   280  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i 2 .12 11 1.1 - - - - 2 3.7  250 2 6.3   270  
ldv-regression/test02_false-unreach-call_true-termination.c 1 .16 11 1.4 1 2.2  260 1 4.8   220   0 2.0  190 1 .60   18    - -
ldv-regression/test06_false-unreach-call_true-termination.c 1 .14 11 1.5 1 2.3  260 -32 3.3   230   0 2.0  210 1 .60   18    - -
ldv-regression/test08_false-unreach-call_true-termination.c 1 .16 11 1.9 1 4.0  260 -32 4.6   230   0 1.9  210 1 .57   18    - -
ldv-regression/test12_false-unreach-call_true-termination.c 1 .15 11 1.6 1 3.3  260 1 3.3   230   0 1.9  180 1 .60   18    - -
ldv-regression/test21_false-unreach-call_true-termination.c 1 .20 12 2.4 1 2.3  270 -32 3.9   250   0 1.9  210 1 .59   18    - -
ldv-regression/test22_false-unreach-call.c 1 .26 12 2.6 1 2.6  280 -32 3.4   230   0 2.8  210 -32 .57   18    - -
ldv-regression/test23_false-unreach-call.c 1 .28 13 3.4 1 14    290 -32 4.9   240   0 2.8  210 -32 .58   18    - -
ldv-regression/test24_false-unreach-call.c 1 .20 14 2.4 1 4.6  290 -32 3.4   220   0 2.0  210 -32 .58   18    - -
ldv-regression/test25_false-unreach-call_true-termination.c 1 .20 14 2.3 1 14    300 -32 3.4   240   0 2.9  210 1 .60   18    - -
ldv-regression/test26_false-unreach-call_true-termination.c 1 .15 11 1.8 1 3.2  260 -32 3.3   220   0 2.7  180 1 .57   18    - -
ldv-regression/test27_false-unreach-call_true-termination.c 0 .52 13 7.1 0 .64 41 0 .018 5.0 0 .69 49 0 .0011 .28 - -
ldv-regression/test28_false-unreach-call_true-termination.c 1 .17 11 1.9 1 3.0  260 -32 4.5   230   0 2.0  210 1 .61   19    - -
ldv-regression/test29_false-unreach-call_true-termination.c 1 .16 11 1.7 1 3.1  260 -32 3.3   240   0 2.0  210 1 .61   18    - -
ldv-regression/test30_false-unreach-call_true-termination.c 1 .15 11 1.5 1 2.3  270 -32 4.7   230   0 2.1  200 1 .56   18    - -
ldv-regression/test01_true-unreach-call_true-termination.c 2 .12 11 1.3 - - - - 2 3.4  250 2 6.7   270  
ldv-regression/test03_true-unreach-call_true-termination.c 2 .12 11 1.4 - - - - 2 4.0  250 2 6.8   270  
ldv-regression/test04_true-unreach-call_true-termination.c 2 .13 11 1.4 - - - - 2 3.1  250 2 8.0   270  
ldv-regression/test05_true-unreach-call_true-termination.c 2 .15 11 1.4 - - - - 2 3.6  250 2 13     490  
ldv-regression/test07_true-unreach-call_true-termination.c 2 .12 11 1.4 - - - - 2 3.1  250 2 8.6   340  
ldv-regression/test09_true-unreach-call_true-termination.c 2 .15 11 1.5 - - - - 2 3.5  250 2 9.8   350  
ldv-regression/test10_true-unreach-call_true-termination.c 2 .14 11 1.6 - - - - 2 4.1  260 2 12     490  
ldv-regression/test11_true-unreach-call_true-termination.c 2 .12 11 1.4 - - - - 2 3.6  250 2 7.8   270  
ldv-regression/test13_true-unreach-call_true-termination.c 2 .15 11 1.6 - - - - 2 3.8  250 2 5.3   260  
ldv-regression/test14_true-unreach-call_true-termination.c 2 .13 11 1.4 - - - - 2 3.6  260 2 4.9   260  
ldv-regression/test15_true-unreach-call_true-termination.c 2 .14 11 1.4 - - - - 2 3.1  250 2 7.3   280  
ldv-regression/test16_true-unreach-call_true-termination.c 2 .13 11 1.4 - - - - 2 2.2  250 2 8.5   300  
ldv-regression/test17_true-unreach-call_true-termination.c 2 .14 11 1.4 - - - - 2 2.8  250 2 6.3   250  
ldv-regression/test18_true-unreach-call_true-termination.c 2 .15 11 1.4 - - - - 2 2.9  250 2 8.6   300  
ldv-regression/test19_true-unreach-call_true-termination.c 2 .15 11 1.2 - - - - 2 3.8  250 2 11     360  
ldv-regression/test20_true-unreach-call_true-termination.c 2 .15 11 1.4 - - - - 2 3.7  250 2 5.7   260  
ldv-regression/test21_true-unreach-call_true-termination.c 2 .14 11 1.4 - - - - 2 3.9  250 2 8.0   310  
ldv-regression/test22_true-unreach-call.c 2 .15 11 1.4 - - - - 2 6.3  290 2 25     640  
ldv-regression/test23_true-unreach-call.c 2 .13 11 1.8 - - - - 2 6.9  310 2 260     760  
ldv-regression/test24_true-unreach-call_true-termination.c 2 .15 11 1.4 - - - - 2 5.9  290 2 11     410  
ldv-regression/test25_true-unreach-call.c 2 .15 11 1.4 - - - - 2 15    430 2 26     550  
ldv-regression/test26_true-unreach-call_true-termination.c 2 .15 11 1.5 - - - - 2 3.9  250 2 9.3   290  
ldv-regression/test27_true-unreach-call_true-termination.c 2 .15 11 1.6 - - - - 2 31    480 2 180     780  
ldv-regression/test28_true-unreach-call_true-termination.c 2 .18 11 1.7 - - - - 2 2.9  250 2 7.5   270  
ldv-regression/test29_true-unreach-call_true-termination.c 2 .19 11 1.6 - - - - 2 3.6  250 2 4.8   270  
ldv-regression/test30_true-unreach-call_true-termination.c 2 .15 11 1.6 - - - - 2 4.2  250 2 7.0   450  
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i 1 .47 17 5.3 1 8.3  360 -32 8.4   460   0 3.6  280 1 1.1    18    - -
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i 1 .47 15 4.9 1 6.1  370 -32 8.7   470   0 3.6  280 1 1.1    18    - -
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i 1 .45 16 5.2 1 11    360 -32 8.6   440   0 5.2  270 1 1.1    18    - -
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i 2 .32 14 3.9 - - - - 2 6.2  280 2 18     430  
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i 2 .32 14 4.3 - - - - 2 4.3  300 2 8.6   430  
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i 2 .35 14 3.9 - - - - 2 6.9  280 2 12     430  
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i 2 .32 14 4.0 - - - - 2 6.9  280 2 12     430  
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i 2 .34 14 4.2 - - - - 2 6.9  280 2 14     430  
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i 2 .32 14 4.0 - - - - 2 6.8  280 2 14     440  
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i 2 .34 14 3.5 - - - - 2 7.7  280 2 12     430  
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i 2 .34 14 4.1 - - - - 2 6.1  280 2 14     430  
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i 2 .32 14 4.0 - - - - 2 7.5  270 2 11     420  
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i 2 .31 14 4.8 - - - - 2 6.1  280 2 12     430  
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i 1 .19 11 2.2 0 5.4  280 -32 6.6   280   0 2.4  210 1 .65   18    - -
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i 1 .17 11 1.8 0 4.1  260 -32 3.7   250   0 2.4  220 1 .66   18    - -
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i 1 .18 11 2.5 1 4.2  270 -32 5.4   250   0 2.3  210 1 .62   18    - -
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i 0 .22 11 2.2 0 4.0  260 -32 4.0   260   0 3.6  220 -32 .65   18    - -
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i 1 .17 11 2.0 0 4.7  270 -32 3.9   250   0 2.4  210 1 .64   19    - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i 0 .20 11 1.9 0 4.2  270 -32 3.9   250   0 3.3  210 -32 .63   18    - -
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i 1 .18 11 2.1 1 4.6  260 -32 5.6   240   0 2.4  220 1 .63   18    - -
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i 1 .21 11 2.4 1 5.2  270 -32 5.5   250   0 2.3  210 1 .64   18    - -
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i 1 .20 11 2.1 0 3.3  270 -32 5.2   240   0 2.3  210 1 .63   18    - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i 0 900    2200 7200   0 .70 43 0 .019 4.9 0 .87 49 0 .0011 .26 - -
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i 0 .22 15 2.0 0 5.4  280 -32 3.9   250   0 2.4  210 -32 .63   18    - -
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i 1 .17 11 1.8 1 3.2  270 -32 3.6   240   0 3.5  220 1 .64   18    - -
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i 1 .21 11 2.0 1 5.5  270 -32 5.5   250   0 2.4  210 1 .63   18    - -
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i 0 .19 11 2.5 0 4.8  270 -32 5.8   260   0 3.4  210 -32 .63   18    - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i 1 .17 11 1.6 0 4.5  270 -32 3.3   250   0 2.3  210 1 .62   18    - -
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i 0 .19 11 1.8 0 4.6  270 -32 5.6   240   0 3.6  220 -32 .64   18    - -
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i 1 .20 11 2.0 1 5.0  260 -32 5.0   240   0 3.4  210 1 .63   18    - -
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i 1 .21 12 2.0 0 4.2  260 -32 3.9   250   0 3.4  210 1 .66   18    - -
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i 1 .19 11 1.9 1 2.8  270 -32 5.3   240   0 2.3  210 1 .67   18    - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i 0 900    5500 7800   - - - - 0 .55 43 0 .018 5.0
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i 0 900    5200 8600   - - - - 0 .65 43 0 .022 4.8
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i 0 900    4200 6000   - - - - 0 .58 43 0 .019 5.0
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i 0 900    2200 9900   - - - - 0 .67 43 0 .021 4.9
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i 0 900    4900 6200   - - - - 0 .62 43 0 .024 4.9
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i 0 900    5100 4000   - - - - 0 .61 43 0 .048 4.8
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i 0 900    5900 11000   - - - - 0 .39 43 0 .020 4.8
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i 0 900    5000 10000   - - - - 0 .67 45 0 .020 4.8
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i 0 900    330 11000   - - - - 0 .61 43 0 .026 4.8
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i 0 900    110 9200   - - - - 0 .51 41 0 .018 4.8
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i 0 900    5900 5200   - - - - 0 .66 44 0 .024 5.0
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i 0 900    4500 5000   - - - - 0 .62 44 0 .018 4.8
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i 0 900    5000 11000   - - - - 0 .55 43 0 .024 4.9
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i 0 900    4100 6000   - - - - 0 .55 44 0 .021 4.8
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i 0 900    2500 11000   - - - - 0 .67 43 0 .020 4.9
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i 0 900    5200 4900   - - - - 0 .54 45 0 .020 4.9
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i 0 900    5100 5000   - - - - 0 .52 41 0 .019 4.8
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i 0 900    6200 11000   - - - - 0 .68 44 0 .021 4.9
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i 0 900    5000 9400   - - - - 0 .54 41 0 .018 4.9
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i 0 900    400 11000   - - - - 0 .54 43 0 .024 4.9
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i 0 900    110 8200   - - - - 0 .53 43 0 .020 4.9
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i 1 .18 11 2.1 1 7.8  380 -32 5.2   240   0 3.6  220 1 .63   18    - -
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i 0 1.9  31 25   0 92    1900 -32 5.1   240   0 2.4  210 -32 .62   18    - -
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup_true-termination.i 1 .18 11 2.1 1 5.4  270 -32 5.3   230   0 3.4  210 1 .62   18    - -
list-ext2-properties/list_and_tree_cnstr_false-unreach-call_false-termination.i 1 .20 11 2.1 0 5.8  270 -32 6.1   250   0 2.4  220 1 .63   18    - -
list-ext2-properties/list_and_tree_cnstr_true-unreach-call_false-termination.i 0 900    1400 10000   - - - - 0 .64 44 0 .021 5.0
list-ext2-properties/simple_and_skiplist_2lvl_false-unreach-call.i 1 .18 11 2.1 1 5.2  270 -32 5.7   250   0 3.7  230 -32 .66   18    - -
list-ext2-properties/simple_and_skiplist_2lvl_true-unreach-call.i 0 900    1300 9200   - - - - 0 .58 43 0 .018 5.0
list-ext2-properties/simple_search_value_false-unreach-call.i 1 .18 11 2.0 0 5.2  290 -32 5.5   240   0 2.4  210 1 .64   18    - -
list-ext2-properties/simple_search_value_true-unreach-call.i 0 900    590 11000   - - - - 0 .72 44 0 .019 4.9
ldv-sets/test_add_false-unreach-call_true-termination.i 1 .20 11 2.5 1 4.5  270 -32 3.6   250   0 2.4  210 0 .57   18    - -
ldv-sets/test_mutex_double_lock_false-unreach-call_true-termination.i 1 .22 11 2.1 1 6.2  270 -32 5.6   250   0 2.4  220 0 .60   18    - -
ldv-sets/test_mutex_double_unlock_false-unreach-call.i 0 .21 11 2.4 0 48    910 -32 5.1   250   0 3.6  220 0 .61   18    - -
ldv-sets/test_mutex_unbounded_false-unreach-call.i 0 .21 11 2.6 0 6.5  270 -32 5.8   260   0 2.5  220 0 .58   18    - -
ldv-sets/test_mutex_unlock_at_exit_false-unreach-call.i 0 .21 11 2.1 0 48    910 -32 5.8   260   0 2.5  210 0 .60   18    - -
ldv-sets/test_add_true-unreach-call_true-termination.i 2 .20 11 2.2 - - - - 2 5.5  290 0 320     860  
ldv-sets/test_mutex_true-unreach-call.i 2 .22 11 2.3 - - - - 2 290    3700 0 960     1400  
ldv-sets/test_mutex_unbounded_true-unreach-call.i 0 900    8100 8800   - - - - 0 .39 43 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 201 34000   120000 330000 71 45 500 22000 71 -2109 340 17000 71 0 190 15000 71 -630 44 1300 110 146 680 25000 110 142 2400 28000
    correct results 128 201 24   1500 260 45 45 210 12000 3 3 13 680 0 42 42 27 770 73 146 660 23000 71 142 1100 25000
        correct true 73 146 13   820 140 0 0 0 0 73 146 660 23000 71 142 1100 25000
        correct false 55 55 11   640 120 45 45 210 12000 3 3 13 680 0 42 42 27 770 0 0
    correct-unconfimed results 14 0 4.6 180 55 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 14 0 4.6 180 55 0 0 0 0 0 0
    incorrect results 0 0 66 -2112 330 17000 0 21 -672 13 390 0 0
        incorrect true 0 0 66 -2112 330 17000 0 21 -672 13 390 0 0
        incorrect false 0 0 0 0 0 0 0
score (181 tasks, max score: 291) 201 45 -2109 0 -630 146 142
Run set symbiotic.sv-comp18.ReachSafety-Heap cpa-seq-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Heap uautomizer-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-symbiotic.sv-comp18-violation-witness.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.ReachSafety-Heap uautomizer-validate-correctness-witnesses-symbiotic.sv-comp18-correctness-witness.ReachSafety-Heap