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* [apollon010; apollon035; apollon045; apollon077; apollon078; apollon138] [apollon007; apollon077; apollon078; apollon143] 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-01 08:49:27 CET 2017-12-01 22:53:44 CET 2017-12-01 23:38:04 CET 2017-12-01 23:47:42 CET 2017-12-01 23:55:24 CET 2017-12-01 22:20:30 CET 2017-12-01 23:01:53 CET
Run set esbmc-incr.sv-comp18.ReachSafety-Heap cpa-seq-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Heap uautomizer-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.ReachSafety-Heap uautomizer-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.ReachSafety-Heap
Options -s incr -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-01_0849.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-incr.2017-12-01_0849.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-01_0849.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-incr.2017-12-01_0849.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/esbmc-incr.2017-12-01_0849.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/esbmc-incr.2017-12-01_0849.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 .48  30 4.2  0 3.0  180 -32 6.5   270   0 2.2  210 0 .62   18    - -
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i 0 900     9600 5400    0 .57 46 0 .019 4.8 0 .84 49 0 .0011 .26 - -
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i 1 .77  37 9.0  1 4.9  270 -32 5.2   310   0 2.4  210 -32 .67   18    - -
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i 0 .42  29 3.9  0 4.6  280 -32 4.5   270   0 3.4  210 -32 .65   18    - -
heap-manipulation/tree_false-unreach-call_false-valid-deref.i 1 .77  30 9.3  1 4.1  270 -32 6.1   280   0 3.4  210 1 .64   18    - -
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i 0 1.2   29 12    0 3.3  170 -32 9.1   300   0 2.1  180 0 .58   18    - -
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i 0 900     5500 7700    - - - - 0 .64 43 0 .019 5.0
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i 0 900     3300 8500    - - - - 0 .64 42 0 .020 4.9
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i 0 900     9600 5600    - - - - 0 .71 43 0 .019 4.8
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i 0 900     3800 9800    - - - - 0 .53 43 0 .020 5.0
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i 0 900     3500 9600    - - - - 0 .69 43 0 .023 5.0
heap-manipulation/tree_true-unreach-call.i 0 900     3900 7900    - - - - 0 .71 43 0 .020 4.8
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i 1 .39  29 3.5  1 4.3  260 -32 5.3   240   0 3.1  210 -32 .63   19    - -
list-properties/list_false-unreach-call_false-valid-memcleanup.i 0 .71  31 7.2  0 3.4  170 1 6.2   280   0 2.0  180 0 .58   18    - -
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i 1 .46  29 3.7  1 3.7  260 1 5.7   260   0 3.2  210 1 .62   18    - -
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i 1 1.0   29 9.5  1 4.7  270 -32 6.6   260   0 3.2  210 1 .62   18    - -
list-properties/simple_false-unreach-call_false-valid-memcleanup.i 1 .46  29 4.3  1 4.6  260 1 5.6   260   0 3.4  210 -32 .63   19    - -
list-properties/splice_false-unreach-call_false-valid-memcleanup.i 1 .54  29 5.0  1 4.1  270 -32 3.8   250   0 3.2  210 -32 .63   18    - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i 0 900     5300 8300    - - - - 0 .70 44 0 .020 4.9
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i 0 900     3400 9300    - - - - 0 .65 43 0 .019 4.9
list-properties/list_search_true-unreach-call_false-valid-memcleanup.i 2 .24  27 2.3  - - - - 2 22    530 2 74     1100  
list-properties/list_true-unreach-call_false-valid-memtrack.i 0 900     1700 9800    - - - - 0 .67 43 0 .021 4.9
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i 0 900     2800 9400    - - - - 0 .41 42 0 .018 5.0
list-properties/simple_true-unreach-call_false-valid-memtrack.i 0 900     3300 8500    - - - - 0 .58 45 0 .019 4.9
list-properties/splice_true-unreach-call_false-valid-memtrack.i 0 900     3500 9300    - - - - 0 .79 43 0 .019 4.8
ldv-regression/1_3_true-termination.c_false-unreach-call.i 1 .24  28 1.9  1 3.4  260 1 5.1   260   0 2.0  210 1 .58   18    - -
ldv-regression/alt_test_true-termination.c_false-unreach-call.i 1 .092 28 1.1  1 4.5  260 -32 4.6   230   0 2.3  210 1 .65   18    - -
ldv-regression/callfpointer_true-termination.c_false-unreach-call.i 0 .078 26 .68 0 .53 41 0 .045 4.9 0 .84 50 0 .0012 .26 - -
ldv-regression/fo_test_true-termination.c_false-unreach-call.i 1 .17  28 1.2  1 4.7  270 -32 4.8   230   0 2.3  210 1 .65   18    - -
ldv-regression/mutex_lock_int_true-termination.c_false-unreach-call.i 1 .10  28 .84 1 3.0  260 -32 5.3   260   0 2.0  180 1 .57   18    - -
ldv-regression/mutex_lock_struct_true-termination.c_false-unreach-call.i 1 .16  28 1.7  1 3.2  260 1 4.7   220   0 2.7  210 1 .56   18    - -
ldv-regression/recursive_list_true-termination.c_false-unreach-call.i 1 .18  28 1.7  1 3.4  260 -32 5.0   230   0 2.9  210 1 .60   18    - -
ldv-regression/rule57_ebda_blast_true-termination.c_false-unreach-call.i 0 .37  28 3.4  -32 3.4  260 -32 4.9   230   0 2.8  210 0 .57   18    - -
ldv-regression/rule60_list2_true-termination.c_false-unreach-call_1.i 1 .26  29 2.9  1 4.9  270 -32 4.4   230   0 3.1  210 -32 .63   19    - -
ldv-regression/stateful_check_false-unreach-call_false-termination.i 1 .24  28 2.2  1 4.3  290 -32 3.5   250   0 3.1  210 -32 .59   18    - -
ldv-regression/test_while_int_true-termination.c_false-unreach-call.i 1 .11  28 .72 1 3.7  260 -32 5.5   260   0 1.9  210 1 .57   18    - -
ldv-regression/test_while_int_true-termination.c_false-unreach-call_1.i 1 .077 28 .97 1 3.5  260 -32 4.8   250   0 2.8  180 1 .57   18    - -
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call.i 2 .096 26 .80 - - - - 2 3.9  250 2 6.1   270  
ldv-regression/alias_of_return_2_true-termination.c_true-unreach-call_1.i 2 .074 26 .87 - - - - 2 2.9  250 2 5.7   260  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call.i 2 .069 26 1.0  - - - - 2 2.9  250 2 5.9   270  
ldv-regression/alias_of_return_true-termination.c_true-unreach-call_1.i 2 .079 26 .66 - - - - 2 3.6  250 2 6.6   260  
ldv-regression/ex3_forlist_true-termination.c_true-unreach-call.i 2 .082 27 .84 - - - - 2 15    460 2 27     700  
ldv-regression/just_assert_true-termination.c_true-unreach-call.i 2 .10  26 .70 - - - - 2 3.3  250 2 4.3   220  
ldv-regression/mutex_lock_int_true-termination.c_true-unreach-call_1.i 2 .092 26 .75 - - - - 2 3.1  250 2 6.3   260  
ldv-regression/mutex_lock_struct_true-termination.c_true-unreach-call_1.i 2 .075 26 .72 - - - - 2 3.7  250 2 6.8   270  
ldv-regression/nested_structure_noptr_true-termination.c_true-unreach-call.i 2 .095 26 .82 - - - - 2 3.6  250 2 5.9   240  
ldv-regression/nested_structure_noptr_true-unreach-call_true-termination.i 2 .095 26 .73 - - - - 2 3.7  250 2 5.2   260  
ldv-regression/nested_structure_ptr_true-termination.c_true-unreach-call.i 2 .11  26 .71 - - - - 2 2.1  250 2 12     470  
ldv-regression/nested_structure_ptr_true-unreach-call_true-termination.i 2 .088 26 .77 - - - - 2 4.2  250 2 9.6   390  
ldv-regression/nested_structure_true-termination.c_true-unreach-call.i 2 .10  26 .68 - - - - 2 4.0  250 2 8.5   290  
ldv-regression/nested_structure_true-unreach-call_true-termination.i 2 .11  26 .61 - - - - 2 4.1  250 2 9.8   290  
ldv-regression/oomInt_true-termination.c_true-unreach-call.i 2 .092 26 .70 - - - - 2 3.9  250 2 4.1   270  
ldv-regression/oomInt_true-termination.c_true-unreach-call_1.i 2 .11  26 .64 - - - - 2 3.6  250 2 6.1   270  
ldv-regression/rule57_ebda_blast_true-termination.c_true-unreach-call_1.i 2 .079 27 .91 - - - - 2 4.3  250 2 6.5   270  
ldv-regression/rule60_list2_true-termination.c_true-unreach-call.i 2 .12  27 1.3  - - - - 2 5.2  260 2 24     640  
ldv-regression/rule60_list_true-termination.c_true-unreach-call.i 2 .10  27 .88 - - - - 2 4.2  260 2 12     380  
ldv-regression/sizeofparameters_test_true-termination.c_true-unreach-call.i 2 .077 26 .81 - - - - 2 4.5  250 2 5.5   260  
ldv-regression/structure_assignment_true-termination.c_true-unreach-call.i 2 .10  26 .75 - - - - 2 4.0  250 2 5.0   250  
ldv-regression/test_address_true-termination.c_true-unreach-call.i 2 .082 27 .79 - - - - 2 3.5  250 2 6.0   260  
ldv-regression/test_cut_trace_true-termination.c_true-unreach-call.i 2 .071 26 .78 - - - - 2 3.2  250 2 6.6   260  
ldv-regression/test_malloc-1_true-unreach-call_true-termination.i 2 .11  27 .62 - - - - 2 4.1  260 2 8.2   260  
ldv-regression/test_malloc-2_true-unreach-call_true-termination.i 2 .081 27 .81 - - - - 2 4.4  250 2 6.1   270  
ldv-regression/test_overflow_true-termination.c_true-unreach-call.i 2 .088 27 .88 - - - - 2 3.9  250 2 5.3   260  
ldv-regression/test_union_cast-1_true-unreach-call_true-termination.i 2 .13  29 1.5  - - - - 2 3.5  240 2 5.6   260  
ldv-regression/test_union_cast-2_true-unreach-call_true-termination.i 2 .13  27 1.3  - - - - 2 3.0  250 2 4.3   260  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call.i 2 .14  27 1.7  - - - - 2 3.9  250 2 3.5   270  
ldv-regression/test_union_cast_true-termination.c_true-unreach-call_1.i 2 .17  29 1.4  - - - - 2 3.8  250 2 5.4   260  
ldv-regression/test_union_true-termination.c_true-unreach-call.i 2 .075 26 .76 - - - - 2 3.7  240 2 5.1   270  
ldv-regression/test_union_true-termination.c_true-unreach-call_1.i 2 .10  26 .79 - - - - 2 3.0  250 2 5.8   260  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call.i 2 .10  26 .65 - - - - 2 3.8  250 2 6.0   270  
ldv-regression/volatile_alias_true-termination.c_true-unreach-call_1.i 2 .075 26 .83 - - - - 2 2.2  250 2 6.1   280  
ldv-regression/test02_false-unreach-call_true-termination.c 1 .082 28 .90 1 2.9  260 1 5.5   220   0 2.8  180 1 .60   18    - -
ldv-regression/test06_false-unreach-call_true-termination.c 1 .086 28 .81 1 3.1  250 -32 5.6   240   0 2.0  190 1 .58   18    - -
ldv-regression/test08_false-unreach-call_true-termination.c 1 .084 28 .96 1 3.9  260 -32 4.7   230   0 2.0  210 1 .55   18    - -
ldv-regression/test12_false-unreach-call_true-termination.c 1 .11  28 1.2  1 3.4  270 1 4.8   230   0 2.8  180 1 .57   18    - -
ldv-regression/test21_false-unreach-call_true-termination.c 0 .41  28 2.8  0 2.9  170 1 5.3   260   0 1.7  180 0 .53   18    - -
ldv-regression/test22_false-unreach-call.c 0 .46  28 5.2  0 2.3  160 -32 5.7   260   0 2.6  180 0 .53   18    - -
ldv-regression/test23_false-unreach-call.c 0 3.2   32 39    0 2.4  170 -32 5.7   270   0 2.7  180 0 .55   18    - -
ldv-regression/test24_false-unreach-call.c 0 .71  41 8.5  0 .53 45 0 .020 5.0 0 .89 50 0 .0012 .26 - -
ldv-regression/test25_false-unreach-call_true-termination.c 0 .60  32 7.2  0 .73 45 0 .018 4.9 0 .87 49 0 .0011 .26 - -
ldv-regression/test26_false-unreach-call_true-termination.c 1 .094 28 1.0  1 3.2  260 -32 4.4   220   0 2.8  190 1 .57   18    - -
ldv-regression/test27_false-unreach-call_true-termination.c 1 1.3   29 11    1 5.0  280 -32 5.1   240   0 3.1  210 0 .59   18    - -
ldv-regression/test28_false-unreach-call_true-termination.c 1 .24  28 2.3  1 3.4  280 1 6.3   260   0 2.8  210 1 .57   18    - -
ldv-regression/test29_false-unreach-call_true-termination.c 1 .37  28 3.2  -32 4.0  260 1 5.0   270   0 2.9  210 1 .58   18    - -
ldv-regression/test30_false-unreach-call_true-termination.c 1 .079 28 .87 1 3.7  270 -32 3.6   250   0 2.7  190 1 .56   18    - -
ldv-regression/test01_true-unreach-call_true-termination.c 2 .10  26 .74 - - - - 2 3.9  250 2 5.3   260  
ldv-regression/test03_true-unreach-call_true-termination.c 2 .094 26 .71 - - - - 2 3.8  250 2 6.7   280  
ldv-regression/test04_true-unreach-call_true-termination.c 2 .11  26 .74 - - - - 2 3.8  250 2 6.9   270  
ldv-regression/test05_true-unreach-call_true-termination.c 2 .073 26 .86 - - - - 2 4.1  250 2 11     490  
ldv-regression/test07_true-unreach-call_true-termination.c 2 .093 26 .78 - - - - 2 3.9  250 2 8.5   340  
ldv-regression/test09_true-unreach-call_true-termination.c 2 .077 26 .81 - - - - 2 3.5  250 2 11     320  
ldv-regression/test10_true-unreach-call_true-termination.c 2 .11  26 .69 - - - - 2 3.9  250 2 8.6   490  
ldv-regression/test11_true-unreach-call_true-termination.c 2 .11  26 .68 - - - - 2 3.0  250 2 8.9   280  
ldv-regression/test13_true-unreach-call_true-termination.c 2 .073 26 .68 - - - - 2 3.5  250 2 5.5   270  
ldv-regression/test14_true-unreach-call_true-termination.c 2 .10  26 .75 - - - - 2 3.8  250 2 6.5   260  
ldv-regression/test15_true-unreach-call_true-termination.c 2 .072 26 .86 - - - - 2 3.8  250 2 7.4   290  
ldv-regression/test16_true-unreach-call_true-termination.c 2 .072 26 .80 - - - - 2 2.9  250 2 7.6   280  
ldv-regression/test17_true-unreach-call_true-termination.c 2 .10  26 .71 - - - - 2 3.7  250 2 5.6   260  
ldv-regression/test18_true-unreach-call_true-termination.c 2 .079 26 .63 - - - - 2 4.0  250 2 8.6   300  
ldv-regression/test19_true-unreach-call_true-termination.c 2 .096 26 .68 - - - - 2 2.1  250 2 10     360  
ldv-regression/test20_true-unreach-call_true-termination.c 2 .11  26 .72 - - - - 2 4.0  250 2 3.9   260  
ldv-regression/test21_true-unreach-call_true-termination.c 2 .097 26 1.0  - - - - 2 3.3  250 2 7.6   310  
ldv-regression/test22_true-unreach-call.c 2 .85  26 10    - - - - 2 7.3  290 2 20     630  
ldv-regression/test23_true-unreach-call.c 2 2.2   29 26    - - - - 2 8.4  290 2 250     760  
ldv-regression/test24_true-unreach-call_true-termination.c 2 3.9   32 48    - - - - 2 4.8  270 2 9.5   410  
ldv-regression/test25_true-unreach-call.c 2 1.7   31 23    - - - - 2 20    440 2 27     550  
ldv-regression/test26_true-unreach-call_true-termination.c 2 .11  26 .63 - - - - 2 3.1  250 2 9.1   300  
ldv-regression/test27_true-unreach-call_true-termination.c 2 .16  27 1.6  - - - - 2 34    480 2 190     800  
ldv-regression/test28_true-unreach-call_true-termination.c 2 .079 26 .83 - - - - 2 3.0  250 2 7.3   270  
ldv-regression/test29_true-unreach-call_true-termination.c 2 .10  26 .75 - - - - 2 3.5  250 2 9.1   270  
ldv-regression/test30_true-unreach-call_true-termination.c 2 .073 26 .71 - - - - 2 3.0  250 2 12     450  
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i 1 .21  42 3.0  1 8.3  350 -32 9.1   470   0 4.9  260 1 1.1    19    - -
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i 1 .21  42 2.8  1 9.2  350 -32 13     440   0 5.1  280 1 1.1    18    - -
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i 1 .20  42 2.2  1 7.9  350 -32 12     470   0 5.0  290 1 1.1    18    - -
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i 0 900     8100 9900    - - - - 0 .67 43 0 .019 4.9
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i 0 900     8100 10000    - - - - 0 .77 46 0 .025 4.8
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i 0 900     8100 8600    - - - - 0 .70 44 0 .024 4.9
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i 0 900     7800 8800    - - - - 0 .69 44 0 .018 4.8
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i 0 900     8100 9500    - - - - 0 .56 43 0 .018 4.9
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i 0 900     8100 9700    - - - - 0 .39 43 0 .023 5.0
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i 0 900     7700 8500    - - - - 0 .55 43 0 .019 4.9
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i 0 900     8100 11000    - - - - 0 .62 43 0 .023 4.8
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i 0 900     7800 8100    - - - - 0 .74 41 0 .018 5.0
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i 0 900     8100 8200    - - - - 0 .68 42 0 .018 4.9
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i 1 .43  29 4.1  1 4.3  270 -32 6.5   290   0 3.3  210 0 .65   18    - -
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i 1 .32  29 2.7  1 4.6  270 1 8.4   350   0 2.3  210 1 .63   18    - -
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i 1 .33  29 2.4  1 4.7  260 1 6.2   280   0 3.2  210 1 .63   18    - -
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i 1 1.5   31 13    1 4.8  270 -32 6.0   260   0 3.5  210 -32 .63   18    - -
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i 1 .26  29 2.1  1 3.7  260 -32 5.7   270   0 2.3  210 1 .65   18    - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i 1 1.3   32 14    1 4.3  270 -32 5.8   260   0 3.3  210 -32 .63   18    - -
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i 1 .51  29 4.2  1 3.8  270 1 6.3   280   0 3.2  210 1 .63   18    - -
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i 1 .78  30 7.4  1 4.0  270 -32 6.7   280   0 3.3  210 1 .64   18    - -
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i 1 .45  29 4.0  1 3.8  270 -32 5.8   270   0 3.2  210 1 .66   18    - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i 1 1.1   33 10    1 4.8  270 -32 7.2   310   0 3.6  210 0 .63   18    - -
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i 1 1.1   31 8.9  1 4.2  270 -32 6.3   290   0 3.5  210 -32 .63   18    - -
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i 1 .29  29 2.2  1 4.3  280 1 8.5   340   0 3.3  210 1 .62   18    - -
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i 1 .26  29 2.8  1 4.7  260 1 6.1   280   0 3.2  210 1 .62   18    - -
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i 1 1.2   31 12    1 3.1  280 -32 5.9   260   0 2.5  210 -32 .63   18    - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i 1 .21  29 1.7  1 4.1  270 -32 5.5   270   0 3.2  210 1 .63   18    - -
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i 1 .95  31 8.1  1 5.0  270 -32 6.7   290   0 2.3  210 -32 .64   18    - -
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i 1 .44  29 3.7  1 4.1  270 1 6.1   270   0 2.3  210 1 .64   18    - -
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i 1 .90  29 7.5  1 5.4  270 -32 4.3   280   0 2.5  210 1 .65   18    - -
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i 1 .38  29 3.1  1 3.9  260 1 5.9   270   0 3.3  210 1 .67   18    - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i 0 900     1200 10000    - - - - 0 .67 41 0 .022 4.8
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i 0 900     2500 9200    - - - - 0 .63 44 0 .019 5.0
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i 0 900     3900 8000    - - - - 0 .62 43 0 .019 4.8
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i 0 900     3900 8900    - - - - 0 .54 43 0 .020 4.8
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i 0 900     3900 10000    - - - - 0 .71 44 0 .019 5.0
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i 0 900     6400 9400    - - - - 0 .55 43 0 .018 4.9
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i 0 900     2800 11000    - - - - 0 .52 43 0 .019 4.8
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i 0 900     1900 9200    - - - - 0 .52 44 0 .019 4.9
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i 0 900     1000 10000    - - - - 0 .71 44 0 .023 4.8
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i 0 900     3200 8400    - - - - 0 .69 42 0 .024 4.8
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i 0 900     1100 11000    - - - - 0 .65 42 0 .021 4.9
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i 0 900     210 11000    - - - - 0 .70 43 0 .019 5.0
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i 0 900     2100 8900    - - - - 0 .46 44 0 .020 4.8
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i 0 900     3600 10000    - - - - 0 .59 43 0 .024 4.8
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i 0 900     3500 9800    - - - - 0 .75 43 0 .023 4.8
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i 0 900     3000 12000    - - - - 0 .55 42 0 .019 4.9
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i 0 900     2800 9900    - - - - 0 .57 44 0 .025 5.0
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i 0 900     2100 10000    - - - - 0 .69 45 0 .019 4.9
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i 0 900     1400 11000    - - - - 0 .73 46 0 .021 4.9
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i 0 900     1200 10000    - - - - 0 .69 44 0 .025 4.8
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i 0 900     2700 8800    - - - - 0 .68 41 0 .019 4.8
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i 1 .21  29 2.0  1 5.2  270 -32 3.9   270   0 2.3  210 1 .62   18    - -
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i 0 8.4   53 93    0 3.1  170 0 97     3300   0 2.0  180 0 .58   19    - -
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup_true-termination.i 1 .19  28 2.1  1 5.4  260 1 4.3   270   0 3.3  210 1 .64   18    - -
list-ext2-properties/list_and_tree_cnstr_false-unreach-call_false-termination.i 0 1.3   40 15    0 3.2  180 -32 6.9   280   0 2.9  180 0 .59   18    - -
list-ext2-properties/list_and_tree_cnstr_true-unreach-call_false-termination.i 0 900     2300 11000    - - - - 0 .82 43 0 .018 4.8
list-ext2-properties/simple_and_skiplist_2lvl_false-unreach-call.i 1 .74  32 6.9  1 4.9  260 1 4.9   290   0 3.1  210 -32 .64   18    - -
list-ext2-properties/simple_and_skiplist_2lvl_true-unreach-call.i 0 900     2000 8800    - - - - 0 .54 42 0 .023 4.8
list-ext2-properties/simple_search_value_false-unreach-call.i 1 4.0   42 41    1 8.2  310 -32 6.3   280   0 3.6  210 1 .64   19    - -
list-ext2-properties/simple_search_value_true-unreach-call.i 0 900     4800 11000    - - - - 0 .72 43 0 .022 4.9
ldv-sets/test_add_false-unreach-call_true-termination.i 0 .034 15 .27 0 .53 41 0 .019 4.9 0 .89 49 0 .0030 .26 - -
ldv-sets/test_mutex_double_lock_false-unreach-call_true-termination.i 0 .038 15 .23 0 .55 41 0 .020 4.8 0 .67 49 0 .0016 .29 - -
ldv-sets/test_mutex_double_unlock_false-unreach-call.i 0 .036 15 .33 0 .69 41 0 .018 4.8 0 .87 49 0 .0012 .27 - -
ldv-sets/test_mutex_unbounded_false-unreach-call.i 0 .063 15 .24 0 .55 43 0 .020 4.9 0 .89 51 0 .0011 .26 - -
ldv-sets/test_mutex_unlock_at_exit_false-unreach-call.i 0 .057 15 .32 0 .66 44 0 .018 4.8 0 .84 49 0 .0037 .26 - -
ldv-sets/test_add_true-unreach-call_true-termination.i 0 .032 15 .34 - - - - 0 .46 44 0 .019 4.8
ldv-sets/test_mutex_true-unreach-call.i 0 .037 15 .25 - - - - 0 .63 41 0 .021 4.9
ldv-sets/test_mutex_unbounded_true-unreach-call.i 0 .033 15 .33 - - - - 0 .71 43 0 .018 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 174 42000 210000 440000 71 -13 270   16000 71 -1325 460 20000 71 0 190 13000 71 -379 39   1100 110 122 340 18000 110 122 990 21000
    correct results 113 174 41 3200 410 51 51 230   14000 19 19 110 5200 0 37 37 24   680 61 122 310 16000 61 122 990 21000
        correct true 61 122 14 1600 160 0 0 0 0 61 122 310 16000 61 122 990 21000
        correct false 52 52 27 1600 260 51 51 230   14000 19 19 110 5200 0 37 37 24   680 0 0
    correct-unconfimed results 10 0 17 330 180 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 10 0 17 330 180 0 0 0 0 0 0
    incorrect results 0 2 -64 7.4 520 42 -1344 250 12000 0 13 -416 8.2 240 0 0
        incorrect true 0 2 -64 7.4 520 42 -1344 250 12000 0 13 -416 8.2 240 0 0
        incorrect false 0 0 0 0 0 0 0
score (181 tasks, max score: 291) 174 -13 -1325 0 -379 122 122
Run set esbmc-incr.sv-comp18.ReachSafety-Heap cpa-seq-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Heap uautomizer-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Heap cpa-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Heap fshell-witness2test-validate-violation-witnesses-esbmc-incr.sv-comp18-violation-witness.ReachSafety-Heap cpa-seq-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.ReachSafety-Heap uautomizer-validate-correctness-witnesses-esbmc-incr.sv-comp18-correctness-witness.ReachSafety-Heap