Tool Cascade 0.1 CBMC 4.9 CPAchecker 1.3.10-svcomp15 ESBMC 1.24 Forester PredatorHP Seahorn SMACK Ultimate Automizer r12950 Ultimate Kojak r12950
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host cayman[1-8]
OS Linux 3.13.0
System CPU: Intel Core i7-4770 @ 3.40 GHz with 8 cores, frequency: 3.4 GHz; RAM: 33 GB
Date of execution 14-12-18 12:10 [[ 14-12-19 11:22 ]] 14-11-19 20:34 [[ 14-12-21 23:35 ]] 14-11-15 15:53 [[ 14-12-21 23:23 ]] 14-12-13 18:39 [[ 14-12-19 11:24 ]] 14-12-11 13:52 14-11-19 17:13 [[ 14-12-22 07:42 ]] 14-12-20 18:50 [[ 14-12-21 21:13 ]] 14-11-26 16:05 [[ 14-12-22 07:46 ]] 14-11-12 22:41 [[ 14-12-21 23:12 ]] 14-11-16 20:08 [[ 14-12-21 23:18 ]]
Options -trace [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/cascade.14-12-18_1210.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/Cascade-4113-patch/out/${sourcefile_name}/witness.graphml -setprop spec.singlePathMatching=false -setprop parser.transformTokensToLines=false ]] --32 [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/cbmc.14-11-19_2034.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/cbmc-sv-comp-2015/witness.graphml -setprop spec.singlePathMatching=false -setprop parser.transformTokensToLines=false ]] -sv-comp15 -disable-java-assertions -heap 10000m [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/cpachecker.14-11-15_1553.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/CPAchecker-1.3.10-svcomp15-unix/output/witness.graphml -setprop spec.singlePathMatching=false -setprop parser.transformTokensToLines=true ]] [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/esbmc.14-12-13_1839.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/esbmc-v1.24.1/witness.graphml -setprop spec.singlePathMatching=false -setprop parser.transformTokensToLines=false ]] --trace witness.graphml --witness ./witness.graphml [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/predatorhp.14-11-19_1713.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/predator-hp-script/witness.graphml -setprop spec.singlePathMatching=false -setprop parser.transformTokensToLines=false ]] --cex=witness.graphml [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/seahorn.14-12-20_1850.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/seahorn-svcomp15/witness.graphml -setprop spec.singlePathMatching=false -setprop parser.transformTokensToLines=false ]] --errorwitness witness.graphml [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/smack.14-11-26_1605.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/smack-corral/witness.graphml -setprop spec.singlePathMatching=false -setprop parser.transformTokensToLines=true -tokenize -deletePragmas ]] 32bit precise [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/ultimateautomizer.14-11-12_2241.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/UltimateAutomizer/witness.graphml -setprop spec.singlePathMatching=false -setprop parser.transformTokensToLines=false ]] 32bit precise [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/ultimatekojak.14-11-16_2008.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/UltimateKojak/witness.graphml -setprop spec.singlePathMatching=false -setprop parser.transformTokensToLines=false ]]
../../sv-benchmarks/c/ status time(s) memory(MB) time(s) for witness status time(s) memory(MB) time(s) for witness status time(s) memory(MB) time(s) for witness status time(s) memory(MB) time(s) for witness status time(s) memory(MB) time(s) for witness status time(s) memory(MB) time(s) for witness status time(s) memory(MB) time(s) for witness status time(s) memory(MB) time(s) for witness status time(s) memory(MB) time(s) for witness status time(s) memory(MB) time(s) for witness
heap-manipulation/bubble_sort_linux_false-unreach-call.i unknown 1.2  86 -    witness confirmed 2.0  200 2.1  witness confirmed 130    1500 2.6  out of memory 530    15000 -    unknown 0.055 9.0 -    witness confirmed 1.1  23 2.0  unknown 0.51 35 -    witness confirmed 3.5  200 2.1  timeout 920    830 -    timeout 920    1300 -   
heap-manipulation/dll_of_dll_false-unreach-call.i unknown 0.82 71 -    witness ignored (recursion) 0.42 37 1.9  witness ignored (recursion) 3.0  210 2.1  out of memory 210    15000 -    unknown 0.088 9.0 -    witness ignored (recursion) 34    64 1.8  witness ignored (recursion) 0.31 38 1.8  witness ignored (recursion) 2.9  160 1.8  unknown 14    430 -    timeout 920    1200 -   
heap-manipulation/merge_sort_false-unreach-call.i witness invalid (error (invalid c code)) 92    240 1.7  unknown 0.63 67 -    witness confirmed 7.2  580 2.1  timeout 920    5300 -    unknown 0.044 8.0 -    witness confirmed 1.0  21 1.8  witness confirmed 0.33 44 1.8  witness confirmed 17    890 1.9  unknown 6.3  240 -    unknown 5.5  240 -   
heap-manipulation/sll_to_dll_rev_false-unreach-call.i unknown 850    350 -    witness invalid (error (invalid c code)) 0.37 35 1.8  timeout 920    6800 -    timeout 920    5100 -    unknown 0.083 9.0 -    witness confirmed 13    96 1.8  witness confirmed 0.34 49 1.8  witness confirmed 8.1  150 2.2  timeout 920    1500 -    timeout 920    1400 -   
heap-manipulation/bubble_sort_linux_true-unreach-call.i unknown 1.2  87 -    true 850    4600 -    timeout 920    1500 -    out of memory 540    15000 -    true 0.88 23 -    true 1.8  50 -    unknown 0.43 37 -    timeout 920    260 -    timeout 920    780 -    timeout 920    1000 -   
heap-manipulation/dll_of_dll_true-unreach-call.i unknown 0.80 73 -    true 850    2400 -    false(reach) 3.1  210 -    out of memory 210    15000 -    unknown 0.10 9.0 -    true 2.7  59 -    false(reach) 0.34 38 -    false(reach) 2.9  160 -    unknown 13    430 -    timeout 920    1600 -   
heap-manipulation/merge_sort_true-unreach-call.i true 850    750 -    true 850    6100 -    timeout 920    1200 -    out of memory 240    15000 -    true 0.14 12 -    true 2.2  33 -    false(reach) 0.34 40 -    false(reach) 20    900 -    unknown 5.4  240 -    unknown 5.3  240 -   
heap-manipulation/sll_to_dll_rev_true-unreach-call.i unknown 850    360 -    true 850    7200 -    timeout 920    1600 -    timeout 920    5100 -    unknown 0.090 9.0 -    true 3.3  54 -    false(reach) 0.31 51 -    true 340    260 -    timeout 920    1400 -    timeout 920    1200 -   
list-properties/alternating_list_false-unreach-call.i witness invalid (error (invalid c code)) 9.1  140 1.7  witness confirmed 0.23 27 1.8  witness confirmed 5.0  260 2.1  witness confirmed 2.4  45 1.8  unknown 0.043 8.0 -    witness confirmed 1.4  25 1.8  true 0.20 28 -    witness confirmed 1.3  91 1.9  witness confirmed 6.3  250 1.8  witness confirmed 6.4  250 1.8 
list-properties/list_false-unreach-call.i unknown 850    270 -    unknown 0.26 31 -    witness confirmed 3.9  240 2.0  timeout 920    3300 -    unknown 0.056 8.0 -    witness confirmed 14    21 1.7  true 0.18 28 -    witness confirmed 2.5  91 2.0  witness confirmed 43    660 1.8  witness confirmed 14    410 1.7 
list-properties/list_flag_false-unreach-call.i witness invalid (error (invalid c code)) 5.1  130 1.7  witness confirmed 0.23 27 1.8  witness confirmed 5.0  300 2.1  witness confirmed 3.4  47 2.0  unknown 0.050 8.0 -    witness confirmed 1.3  20 1.8  true 0.21 28 -    witness confirmed 1.3  90 1.9  witness confirmed 7.4  280 1.8  witness confirmed 6.7  250 1.7 
list-properties/list_search_false-unreach-call.i unknown 850    280 -    witness confirmed 0.42 27 1.8  witness confirmed 5.1  280 2.2  witness confirmed 1.6  19 1.8  unknown 0.039 9.0 -    witness confirmed 1.0  20 1.7  witness confirmed 0.28 36 1.7  witness confirmed 1.1  74 1.8  timeout 920    910 -    timeout 920    510 -   
list-properties/simple_false-unreach-call.i witness invalid (error (invalid c code)) 3.3  110 1.6  unknown 0.22 27 -    witness confirmed 5.1  260 2.1  witness confirmed 2.3  44 1.7  unknown 0.048 8.0 -    witness confirmed 1.0  19 1.7  true 0.17 27 -    witness confirmed 1.2  84 1.9  witness confirmed 7.3  270 1.8  witness confirmed 6.6  250 1.7 
list-properties/splice_false-unreach-call.i witness invalid (error (invalid c code)) 10    140 1.7  witness confirmed 0.25 27 1.8  witness confirmed 6.1  260 2.2  timeout 920    2200 -    unknown 0.044 9.0 -    witness confirmed 1.8  22 1.8  true 0.21 30 -    witness confirmed 1.6  78 2.1  witness confirmed 7.4  270 1.9  witness confirmed 6.7  270 1.8 
list-properties/alternating_list_true-unreach-call.i true 850    610 -    true 21    200 -    false(reach) 6.8  400 -    true 0.12 17 -    unknown 0.042 8.0 -    timeout 920    3300 -    true 0.19 27 -    true 2.0  66 -    unknown 470    380 -    timeout 920    960 -   
list-properties/list_flag_true-unreach-call.i true 850    750 -    true 25    300 -    timeout 920    390 -    true 0.35 46 -    unknown 0.028 8.0 -    true 1.8  20 -    true 0.32 28 -    true 2.2  71 -    unknown 500    2500 -    timeout 920    880 -   
list-properties/list_search_true-unreach-call.i unknown 850    290 -    true 1.3  29 -    true 6.1  300 -    true 0.093 21 -    true 0.14 10.0 -    true 3.2  21 -    false(reach) 0.26 39 -    true 1.6  67 -    unknown 73    280 -    timeout 920    1200 -   
list-properties/list_true-unreach-call.i unknown 850    280 -    true 850    6800 -    timeout 920    1200 -    timeout 920    3300 -    unknown 0.042 8.0 -    true 1.8  21 -    true 0.19 28 -    true 6.0  100 -    unknown 470    660 -    timeout 920    1100 -   
list-properties/simple_built_from_end_true-unreach-call.i true 850    410 -    true 12    110 -    false(reach) 6.2  380 -    true 0.31 51 -    unknown 0.067 13 -    true 1.8  20 -    true 0.17 27 -    true 1.9  68 -    timeout 920    1900 -    timeout 920    950 -   
list-properties/simple_true-unreach-call.i true 850    400 -    true 29    240 -    timeout 920    290 -    false(reach) 2.4  45 -    true 0.030 8.0 -    true 1.9  20 -    true 0.16 27 -    true 1.9  64 -    timeout 920    1800 -    timeout 920    2600 -   
list-properties/splice_true-unreach-call.i true 850    670 -    true 210    1900 -    timeout 920    3900 -    timeout 920    2200 -    unknown 0.037 9.0 -    timeout 920    2000 -    true 0.35 28 -    false(reach) 1.5  100 -    timeout 920    1200 -    timeout 920    1200 -   
ldv-regression/1_3.c_false-unreach-call.i witness invalid (error (invalid c code)) 0.95 92 1.3  witness confirmed 0.22 25 1.7  witness confirmed 2.7  210 1.5  witness confirmed 0.14 12 1.7  unknown 0.041 8.0 -    witness confirmed 1.1  18 1.5  witness confirmed 0.14 31 1.4  witness confirmed 0.96 56 1.5  witness confirmed 6.4  250 1.4  witness confirmed 5.9  250 1.4 
ldv-regression/alt_test.c_false-unreach-call.i witness invalid (error (invalid c code)) 1.4  110 1.7  witness confirmed 0.23 29 1.9  witness confirmed 5.9  390 2.4  witness confirmed 4.4  22 2.0  unknown 0.035 8.0 -    witness confirmed 1.1  20 2.0  witness confirmed 0.17 33 1.9  witness confirmed 0.88 57 2.0  witness confirmed 6.5  260 2.0  witness confirmed 6.4  250 1.9 
ldv-regression/callfpointer.c_false-unreach-call.i unknown 0.45 61 -    witness confirmed 0.12 23 1.4  witness confirmed 1.6  160 1.4  unknown 0.055 3.0 -    unknown 0.058 8.0 -    witness confirmed 1.0  18 1.4  true 0.32 27 -    witness confirmed 0.79 50 1.4  witness confirmed 5.2  240 1.5  witness confirmed 5.6  250 1.4 
ldv-regression/fo_test.c_false-unreach-call.i witness invalid (error (invalid c code)) 1.4  100 1.6  unknown 0.22 28 -    witness confirmed 2.4  200 2.0  witness confirmed 3.1  20 1.9  unknown 0.033 8.0 -    witness confirmed 1.1  20 1.8  witness confirmed 0.18 32 1.8  witness confirmed 0.92 48 1.8  unknown 5.4  240 -    unknown 5.3  240 -   
ldv-regression/mutex_lock_int.c_false-unreach-call.i witness invalid (error (invalid c code)) 0.93 93 1.4  unknown 0.088 23 -    witness confirmed 2.4  210 1.5  witness confirmed 0.096 12 1.4  unknown 0.049 7.0 -    witness confirmed 1.0  18 1.4  witness confirmed 0.17 32 1.4  witness confirmed 0.92 51 1.4  witness confirmed 5.8  250 1.4  witness confirmed 5.8  250 1.4 
ldv-regression/mutex_lock_struct.c_false-unreach-call.i witness invalid (error (invalid c code)) 0.90 93 1.3  witness invalid (error (invalid c code)) 0.098 23 1.3  witness confirmed 2.5  210 1.5  witness confirmed 0.17 12 1.7  unknown 0.027 7.0 -    witness confirmed 1.0  18 1.4  witness confirmed 0.13 32 1.4  witness confirmed 0.92 55 1.4  witness confirmed 5.9  250 1.4  witness confirmed 5.8  250 1.4 
ldv-regression/recursive_list.c_false-unreach-call.i witness invalid (error (invalid c code)) 150    180 1.7  unknown 0.20 25 -    witness confirmed 1.7  180 1.4  witness confirmed 0.13 13 1.6  unknown 0.030 7.0 -    witness confirmed 1.1  18 1.5  witness confirmed 0.18 32 1.4  witness confirmed 0.97 57 1.5  witness confirmed 5.8  250 1.5  witness confirmed 6.3  250 1.4 
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i witness invalid (error (invalid c code)) 1.1  97 1.4  witness confirmed 0.13 24 1.5  witness confirmed 1.8  170 1.5  witness confirmed 0.31 12 1.6  unknown 0.045 8.0 -    witness confirmed 1.0  19 1.5  witness confirmed 0.20 34 1.5  witness confirmed 1.0  63 1.9  witness confirmed 5.7  250 1.7  witness confirmed 6.3  250 1.6 
ldv-regression/rule60_list2.c_false-unreach-call_1.i witness invalid (error (invalid c code)) 1.5  100 1.6  witness confirmed 0.13 26 1.9  witness confirmed 2.4  210 2.1  witness confirmed 2.4  18 2.0  unknown 0.040 8.0 -    witness confirmed 1.1  20 1.8  witness confirmed 0.22 33 1.8  witness confirmed 1.1  67 2.2  witness confirmed 19    670 1.9  witness confirmed 16    670 1.9 
ldv-regression/stateful_check_false-unreach-call.i witness invalid (error (invalid c code)) 1.2  100 1.5  witness confirmed 0.21 25 1.8  witness confirmed 2.0  200 1.9  witness confirmed 0.34 13 1.7  unknown 0.053 8.0 -    witness confirmed 1.0  19 1.7  witness confirmed 0.23 36 2.1  witness confirmed 1.5  87 2.5  witness confirmed 7.0  270 1.9  witness confirmed 67    1200 1.8 
ldv-regression/test_while_int.c_false-unreach-call.i witness invalid (error (invalid c code)) 0.93 90 1.4  witness confirmed 0.20 23 1.4  witness confirmed 1.6  170 1.4  witness unconfirmed 0.15 12 1.4  unknown 0.034 7.0 -    witness confirmed 1.0  18 1.4  witness confirmed 0.30 34 1.4  witness confirmed 0.99 56 1.5  witness confirmed 6.2  250 1.5  witness confirmed 5.7  250 1.5 
ldv-regression/test_while_int.c_false-unreach-call_1.i witness invalid (error (invalid c code)) 0.91 92 1.4  witness confirmed 0.20 23 1.4  witness confirmed 1.6  160 1.5  witness unconfirmed 0.094 12 1.4  unknown 0.034 7.0 -    witness confirmed 1.0  17 1.4  witness confirmed 0.27 34 1.4  witness confirmed 0.93 48 1.4  witness confirmed 5.7  250 1.5  witness confirmed 5.5  250 1.4 
ldv-regression/alias_of_return.c_true-unreach-call.i true 0.55 76 -    true 0.49 23 -    true 2.1  210 -    true 0.062 11 -    unknown 0.045 7.0 -    true 1.0  17 -    true 0.16 27 -    true 1.3  54 -    true 5.8  250 -    true 5.6  250 -   
ldv-regression/alias_of_return.c_true-unreach-call_1.i true 0.55 74 -    true 0.50 23 -    true 2.2  200 -    true 0.063 12 -    unknown 0.032 7.0 -    true 1.0  17 -    true 0.12 25 -    true 1.2  47 -    true 5.6  250 -    true 5.2  250 -   
ldv-regression/alias_of_return_2.c_true-unreach-call.i true 0.63 78 -    true 0.52 23 -    true 2.2  200 -    true 0.070 12 -    unknown 0.034 7.0 -    true 1.0  16 -    true 0.12 22 -    true 1.3  52 -    true 5.9  250 -    true 5.9  250 -   
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i true 0.55 76 -    true 0.52 23 -    true 2.2  200 -    true 0.073 12 -    unknown 0.030 7.0 -    true 1.0  17 -    true 0.13 27 -    true 1.2  47 -    true 6.9  250 -    true 6.5  250 -   
ldv-regression/ex3_forlist.c_true-unreach-call.i true 860    1300 -    true 0.52 24 -    true 1.4  140 -    true 0.074 12 -    unknown 0.027 7.0 -    true 1.0  20 -    unknown 0.24 38 -    true 1.8  78 -    true 85    290 -    true 48    690 -   
ldv-regression/just_assert.c_true-unreach-call.i true 0.54 74 -    true 0.58 25 -    true 1.4  130 -    true 0.058 11 -    true 0.044 10.0 -    true 1.0  17 -    true 0.14 27 -    true 1.2  49 -    true 5.4  250 -    true 5.4  240 -   
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i true 0.57 76 -    true 0.51 23 -    true 2.1  200 -    true 0.077 12 -    unknown 0.033 7.0 -    true 1.0  18 -    true 0.31 27 -    true 1.2  51 -    true 6.2  250 -    true 6.0  250 -   
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i true 0.59 76 -    true 0.51 23 -    true 2.2  210 -    true 0.071 12 -    unknown 0.043 7.0 -    true 1.0  18 -    true 0.13 27 -    true 1.3  49 -    true 6.4  250 -    true 5.9  250 -   
ldv-regression/nested_structure.c_true-unreach-call.i unknown 850    260 -    true 0.52 23 -    true 2.2  200 -    true 0.077 12 -    true 0.044 10.0 -    true 1.0  16 -    true 0.12 27 -    true 1.3  51 -    true 6.4  270 -    true 5.8  250 -   
ldv-regression/nested_structure_noptr.c_true-unreach-call.i true 0.56 76 -    true 0.52 23 -    true 1.4  130 -    true 0.072 12 -    true 0.058 10.0 -    true 1.0  16 -    true 0.16 24 -    true 1.3  51 -    true 5.3  250 -    true 5.4  250 -   
ldv-regression/nested_structure_noptr_true-unreach-call.i true 0.59 74 -    true 0.54 23 -    true 1.4  140 -    true 0.058 12 -    true 0.092 18 -    true 1.0  17 -    true 0.12 27 -    true 1.3  51 -    true 5.3  250 -    true 5.2  250 -   
ldv-regression/nested_structure_ptr.c_true-unreach-call.i unknown 850    250 -    true 0.53 23 -    true 2.2  200 -    true 0.057 12 -    true 0.055 10.0 -    true 1.0  17 -    true 0.16 27 -    true 1.2  47 -    true 8.5  290 -    true 5.8  250 -   
ldv-regression/nested_structure_ptr_true-unreach-call.i unknown 850    250 -    true 0.52 24 -    true 2.2  200 -    true 0.063 12 -    true 0.046 10.0 -    true 1.1  17 -    true 0.13 21 -    true 1.3  51 -    true 21    300 -    true 8.3  270 -   
ldv-regression/nested_structure_true-unreach-call.i unknown 850    260 -    true 0.50 23 -    true 2.2  210 -    true 0.062 12 -    true 0.052 10.0 -    true 1.0  18 -    true 0.14 27 -    true 1.2  51 -    true 7.1  270 -    true 6.6  240 -   
ldv-regression/oomInt.c_true-unreach-call.i true 0.53 74 -    true 0.52 24 -    true 1.4  140 -    true 0.074 12 -    unknown 0.026 7.0 -    true 1.0  18 -    true 0.16 27 -    true 1.2  50 -    true 5.7  250 -    true 5.5  250 -   
ldv-regression/oomInt.c_true-unreach-call_1.i true 0.56 73 -    true 0.50 23 -    true 1.4  130 -    true 0.071 12 -    unknown 0.053 7.0 -    true 1.0  18 -    true 0.32 27 -    true 1.3  49 -    true 5.7  250 -    true 5.5  250 -   
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i true 0.69 79 -    true 0.56 24 -    true 1.4  130 -    true 0.072 12 -    unknown 0.039 8.0 -    true 1.8  19 -    true 0.20 30 -    true 1.3  56 -    true 5.9  250 -    true 6.7  270 -   
ldv-regression/rule60_list.c_true-unreach-call.i true 0.88 85 -    true 1.2  27 -    true 3.1  210 -    true 0.069 17 -    unknown 0.051 8.0 -    true 1.0  20 -    unknown 0.19 31 -    true 1.4  51 -    true 7.0  270 -    true 7.3  270 -   
ldv-regression/rule60_list2.c_true-unreach-call.i true 1.1  88 -    true 0.62 26 -    true 1.6  140 -    true 0.098 17 -    unknown 0.045 8.0 -    true 1.0  20 -    false(reach) 0.21 34 -    true 1.4  57 -    true 18    660 -    true 13    420 -   
ldv-regression/sizeofparameters_test.c_true-unreach-call.i true 0.78 79 -    true 0.58 25 -    true 1.5  140 -    false(reach) 1.5  17 -    unknown 0.048 8.0 -    true 1.0  18 -    true 0.30 27 -    true 1.2  53 -    true 5.5  250 -    true 5.5  250 -   
ldv-regression/structure_assignment.c_true-unreach-call.i true 0.76 85 -    true 0.49 23 -    true 2.1  200 -    true 0.067 12 -    unknown 0.052 8.0 -    true 1.1  17 -    true 0.12 27 -    true 1.3  47 -    true 5.3  240 -    true 5.6  250 -   
ldv-regression/test_address.c_true-unreach-call.i unknown 0.79 77 -    true 0.60 26 -    true 3.0  210 -    true 0.074 17 -    unknown 0.036 8.0 -    true 1.0  19 -    true 0.13 26 -    true 1.3  49 -    true 5.8  250 -    true 5.5  250 -   
ldv-regression/test_cut_trace.c_true-unreach-call.i true 0.58 73 -    true 0.50 23 -    true 1.4  140 -    true 0.066 12 -    true 0.065 10.0 -    true 1.0  17 -    true 0.29 27 -    true 1.3  50 -    true 5.3  250 -    true 5.5  250 -   
ldv-regression/test_malloc-1_true-unreach-call.i true 0.88 83 -    true 1.2  27 -    true 3.1  210 -    true 0.071 17 -    true 0.039 8.0 -    true 1.0  19 -    false(reach) 0.30 32 -    true 1.3  53 -    true 5.7  250 -    true 6.1  250 -   
ldv-regression/test_malloc-2_true-unreach-call.i true 0.80 82 -    true 0.56 26 -    true 3.2  210 -    true 0.059 17 -    true 0.045 10.0 -    true 1.0  18 -    true 0.64 27 -    true 1.3  50 -    true 5.7  250 -    true 5.5  250 -   
ldv-regression/test_overflow.c_true-unreach-call.i true 1.1  87 -    true 0.64 28 -    true 1.7  150 -    false(reach) 4.3  22 -    unknown 0.040 8.0 -    true 1.1  21 -    true 0.16 27 -    true 1.2  50 -    true 5.9  250 -    true 5.5  250 -   
ldv-regression/test_union.c_true-unreach-call.i true 0.53 74 -    true 0.52 23 -    true 1.7  140 -    true 0.048 11 -    unknown 0.035 7.0 -    true 1.0  17 -    true 0.17 27 -    true 1.2  49 -    true 5.6  250 -    true 5.6  250 -   
ldv-regression/test_union.c_true-unreach-call_1.i true 0.57 74 -    true 0.48 23 -    true 1.4  130 -    true 0.072 12 -    unknown 0.043 7.0 -    true 1.0  18 -    true 0.29 27 -    true 1.3  51 -    true 5.4  250 -    true 5.6  250 -   
ldv-regression/test_union_cast-1_true-unreach-call.i true 0.57 76 -    true 0.50 24 -    true 1.4  130 -    unknown 0.031 2.0 -    unknown 0.047 7.0 -    true 1.0  18 -    true 0.13 27 -    true 1.2  56 -    true 5.5  240 -    true 5.3  250 -   
ldv-regression/test_union_cast-2_true-unreach-call.i true 0.56 78 -    true 0.54 23 -    true 2.2  210 -    unknown 0.035 2.0 -    unknown 0.053 7.0 -    true 1.0  17 -    true 0.14 27 -    true 1.3  49 -    true 5.9  250 -    true 5.7  250 -   
ldv-regression/test_union_cast.c_true-unreach-call.i true 0.56 77 -    true 0.50 23 -    true 2.2  200 -    unknown 0.026 2.0 -    unknown 0.048 7.0 -    true 1.0  15 -    true 0.31 27 -    true 1.2  50 -    true 5.5  250 -    true 5.5  250 -   
ldv-regression/test_union_cast.c_true-unreach-call_1.i true 0.58 76 -    true 0.50 23 -    true 1.4  130 -    unknown 0.029 2.0 -    unknown 0.032 7.0 -    true 1.0  17 -    true 0.28 27 -    true 1.2  49 -    true 5.4  250 -    true 5.6  250 -   
ldv-regression/volatile_alias.c_true-unreach-call.i true 0.54 74 -    true 0.51 23 -    true 2.1  210 -    true 0.057 11 -    true 0.054 10.0 -    true 1.0  17 -    true 0.12 27 -    true 1.2  49 -    true 6.1  250 -    true 5.4  250 -   
ldv-regression/volatile_alias.c_true-unreach-call_1.i true 0.56 74 -    true 0.48 23 -    true 2.1  210 -    true 0.059 11 -    true 0.051 10.0 -    true 1.0  18 -    true 0.14 27 -    true 1.3  49 -    true 6.0  250 -    true 5.8  250 -   
ddv-machzwd/ddv_machzwd_all_false-unreach-call.i unknown 1.8  130 -    true 32    490 -    witness confirmed 10    500 5.2  witness invalid (error (invalid c code)) 210    1300 2.9  unknown 0.12 16 -    witness confirmed 1.0  47 3.7  true 0.35 28 -    witness confirmed 27    1100 3.8  unknown 5.5  240 -    unknown 5.6  240 -   
ddv-machzwd/ddv_machzwd_inw_false-unreach-call.i unknown 1.8  130 -    witness invalid (error (invalid c code)) 27    490 3.0  witness confirmed 8.8  500 4.6  witness invalid (error (invalid c code)) 160    1200 3.1  unknown 0.12 15 -    witness confirmed 1.0  45 3.7  true 0.37 28 -    witness confirmed 16    780 3.8  unknown 5.4  240 -    unknown 5.3  240 -   
ddv-machzwd/ddv_machzwd_outb_false-unreach-call.i unknown 1.8  130 -    true 31    500 -    witness confirmed 9.6  500 4.5  witness invalid (error (invalid c code)) 210    1200 2.9  unknown 0.12 15 -    witness confirmed 1.0  44 3.5  true 0.36 28 -    witness confirmed 21    930 3.6  unknown 5.4  240 -    unknown 5.6  240 -   
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call.i unknown 1.7  130 -    true 850    350 -    true 63    260 -    true 1.3  160 -    unknown 0.12 16 -    unknown 4.7  47 -    true 0.37 28 -    true 31    890 -    unknown 5.4  240 -    unknown 5.7  240 -   
ddv-machzwd/ddv_machzwd_inb_true-unreach-call.i unknown 1.8  130 -    true 850    350 -    true 63    260 -    true 1.3  160 -    unknown 0.12 15 -    unknown 4.5  46 -    true 0.37 28 -    true 31    880 -    unknown 5.6  240 -    unknown 5.3  240 -   
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call.i unknown 1.8  120 -    true 850    350 -    true 63    270 -    true 1.3  160 -    unknown 0.11 15 -    unknown 4.3  47 -    true 0.37 28 -    true 31    880 -    unknown 5.4  240 -    unknown 5.3  240 -   
ddv-machzwd/ddv_machzwd_inl_true-unreach-call.i unknown 1.8  130 -    true 850    350 -    true 63    260 -    true 1.3  160 -    unknown 0.098 15 -    unknown 4.5  47 -    true 0.35 28 -    true 31    880 -    unknown 5.2  240 -    unknown 5.6  240 -   
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call.i unknown 1.8  130 -    true 850    350 -    true 63    260 -    true 1.3  160 -    unknown 0.11 15 -    unknown 4.5  48 -    true 0.35 28 -    true 31    880 -    unknown 5.4  240 -    unknown 5.3  240 -   
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call.i unknown 1.8  130 -    true 850    350 -    true 63    260 -    true 1.3  160 -    unknown 0.13 15 -    unknown 4.5  47 -    true 0.34 28 -    true 31    880 -    unknown 5.5  240 -    unknown 5.3  240 -   
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call.i unknown 1.8  130 -    true 850    350 -    true 63    260 -    true 1.3  160 -    unknown 0.11 15 -    unknown 4.4  49 -    true 0.37 28 -    true 31    890 -    unknown 5.2  240 -    unknown 5.7  240 -   
ddv-machzwd/ddv_machzwd_outl_true-unreach-call.i unknown 1.8  130 -    true 850    350 -    true 63    260 -    true 1.3  160 -    unknown 0.12 15 -    unknown 4.5  45 -    true 0.35 28 -    true 31    880 -    unknown 5.7  240 -    unknown 5.3  240 -   
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call.i unknown 1.8  130 -    true 850    350 -    true 63    260 -    true 1.3  160 -    unknown 0.12 15 -    unknown 4.4  46 -    true 0.35 28 -    true 31    890 -    unknown 5.4  240 -    unknown 5.6  240 -   
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call.i unknown 1.8  130 -    true 850    350 -    true 63    260 -    true 1.3  160 -    unknown 0.10 15 -    unknown 4.5  47 -    true 0.48 28 -    true 31    890 -    unknown 5.2  240 -    unknown 6.7  240 -   
../../sv-benchmarks/c/ status time(s) memory(MB) time(s) for witness status time(s) memory(MB) time(s) for witness status time(s) memory(MB) time(s) for witness status time(s) memory(MB) time(s) for witness status time(s) memory(MB) time(s) for witness status time(s) memory(MB) time(s) for witness status time(s) memory(MB) time(s) for witness status time(s) memory(MB) time(s) for witness status time(s) memory(MB) time(s) for witness status time(s) memory(MB) time(s) for witness
total files 80 15000 14000 25 80 13000 36000 30 80 8300 35000 54 80 8800 110000 35 80 5.7 780 - 80 2000 7400 47 80 20 2400 25 80 1800 18000 51 80 9400 33000 27 80 13000 36000 26
correct results 35 6000 7000 0 69 13000 35000 24 69 930 17000 54 55 37 2400 23 16 1.8 180 - 68 140 1600 47 61 14 1800 25 76 820 17000 51 50 460 14000 27 50 420 15000 26
false negatives 0 - - - 2 63 990 0 0 - - - 0 - - - 0 - - - 0 - - - 9 2.4 250 0 0 - - - 0 - - - 0 - - -
false positives 0 - - - 0 - - - 3 16 990 0 3 8.1 84 0 0 - - - 0 - - - 6 1.8 240 0 3 24 1200 0 0 - - - 0 - - -
false properties 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - -
score (80 files, max score: 135) 70 - - - 100 - - - 96 - - - 79 - - - 32 - - - 111 - - - -37 - - - 109 - - - 84 - - - 84 - - -
Tool Cascade 0.1 CBMC 4.9 CPAchecker 1.3.10-svcomp15 ESBMC 1.24 Forester PredatorHP Seahorn SMACK Ultimate Automizer r12950 Ultimate Kojak r12950