Tool BLAST 2.7.3 Cascade 0.1 CBMC 4.9 CPAchecker 1.3.10-svcomp15 ESBMC 1.24 Forest Perentie 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-20 14:54 [[ 14-12-21 23:30 ]] 14-12-20 11:27 [[ 14-12-20 14:02 ]] 14-12-19 16:19 [[ 14-12-21 23:26 ]] 14-12-19 16:18 [[ 14-12-20 10:06 ]] 14-12-19 16:19 [[ 14-12-20 10:07 ]] 14-12-19 17:21 [[ 14-12-22 07:33 ]] 14-12-19 17:22 [[ 14-12-20 10:05 ]] 14-12-20 18:50 [[ 14-12-21 21:13 ]] 14-12-19 17:20 [[ 14-12-22 07:45 ]] 14-12-19 17:19 [[ 14-12-21 23:15 ]] 14-12-19 17:19 [[ 14-12-20 10:09 ]]
Options -alias empty -enable-recursion -noprofile -cref -sv-comp -lattice -include-lattice symb -nosserr [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/blast.14-12-20_1454.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/blast-2.7.3/bin/witness.graphml -setprop spec.singlePathMatching=true -setprop parser.transformTokensToLines=false -tokenize -useTokenizer ]] -trace [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/cascade.14-12-20_1127.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-12-19_1619.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-12-19_1618.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-19_1619.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 ]] -svcomp [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/forest.14-12-19_1721.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/forest_svcomp_15/witness.graphml -setprop spec.singlePathMatching=false -setprop parser.transformTokensToLines=false ]] [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/perentie.14-12-19_1722.logfiles/sv-comp15.${sourcefile_name}.log.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-12-19_1720.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-12-19_1719.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-12-19_1719.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 status time(s) memory(MB) time(s) for witness
loops/array_false-unreach-call.i witness confirmed 0.57 16 1.5  witness invalid (error (invalid c code)) 0.94 93 1.3  witness confirmed 0.12 23 1.4  witness confirmed 2.7  210 1.5  witness confirmed 0.12 11 1.5  ??? 0.53 45 -    witness confirmed 4.9  530 1.4  witness confirmed 0.29 32 1.4  witness confirmed 1.0  48 1.4  witness confirmed 5.5  250 1.5  witness confirmed 5.8  250 1.5 
loops/bubble_sort_false-unreach-call.i exception (gremlins) 0.032 13 -    unknown 1.3  92 -    witness confirmed 1.4  130 2.3  witness confirmed 30    900 2.7  out of memory 580    15000 -    ??? 1.9  46 -    no conclusion 5.1  530 -    unknown 0.47 36 -    witness confirmed 4.8  270 2.5  timeout 920    1400 -    timeout 920    1400 -   
loops/count_up_down_false-unreach-call_true-termination.i witness confirmed 0.077 14 1.4  witness invalid (error (invalid c code)) 0.91 94 1.4  witness confirmed 0.12 23 1.4  witness confirmed 1.6  160 1.4  witness confirmed 0.12 11 1.4  witness confirmed 1.2  45 1.4  witness confirmed 4.3  520 1.4  witness confirmed 0.29 32 1.4  witness confirmed 0.93 52 1.4  witness confirmed 5.4  250 1.4  witness confirmed 5.4  250 1.4 
loops/eureka_01_false-unreach-call.i witness confirmed 3.9  32 1.6  true 850    740 -    witness confirmed 0.30 29 1.5  witness confirmed 80    700 1.6  witness confirmed 7.4  56 1.7  witness confirmed 120    45 1.5  no conclusion 4.1  520 -    unknown 0.32 44 -    witness confirmed 1.7  96 1.7  witness confirmed 150    400 1.7  witness confirmed 360    460 1.6 
loops/for_bounded_loop1_false-unreach-call_true-termination.i witness confirmed 1.1  17 1.4  witness invalid (error (invalid c code)) 0.94 93 1.4  witness confirmed 0.12 23 1.4  witness confirmed 3.4  230 1.5  witness confirmed 0.096 12 1.5  witness confirmed 2.6  46 1.4  witness confirmed 5.3  530 1.4  witness confirmed 0.30 35 1.4  witness confirmed 1.3  79 1.6  witness confirmed 5.9  240 1.5  witness confirmed 5.9  250 1.5 
loops/insertion_sort_false-unreach-call.i witness confirmed 4.8  19 1.5  true 850    450 -    witness confirmed 2.7  270 1.4  timeout 920    310 -    witness confirmed 3.8  32 1.8  ??? 0.57 45 -    witness confirmed 14    820 1.4  unknown 0.21 35 -    witness confirmed 1.3  87 1.6  witness confirmed 110    350 1.5  timeout 920    660 -   
loops/invert_string_false-unreach-call.i witness confirmed 1.2  19 1.5  witness invalid (error (invalid c code)) 220    250 1.4  witness confirmed 0.36 37 1.5  timeout 910    650 -    witness confirmed 0.25 13 1.7  ??? 0.55 45 -    witness confirmed 6.3  530 1.5  unknown 0.19 36 -    witness confirmed 1.3  79 1.6  witness confirmed 10.0  300 1.6  witness confirmed 8.5  270 1.5 
loops/linear_search_false-unreach-call.i witness confirmed 0.060 16 1.5  witness invalid (error (invalid c code)) 4.4  180 1.4  true 0.55 27 -    unknown 3.2  230 -    true 0.098 12 -    ??? 0.55 45 -    no conclusion 4.0  520 -    witness confirmed 0.27 33 1.5  true 1.4  55 -    unknown 5.3  240 -    unknown 5.1  240 -   
loops/ludcmp_false-unreach-call.i witness confirmed 1.8  20 1.9  out of memory 670    15000 -    witness confirmed 1.6  170 2.4  timeout 920    1400 -    witness unconfirmed 28    28 1.9  witness confirmed 1.2  49 1.5  no conclusion 4.1  510 -    witness confirmed 0.24 35 1.6  witness confirmed 74    480 1.7  unknown 6.1  240 -    unknown 5.6  240 -   
loops/matrix_false-unreach-call_true-termination.i exception (gremlins) 0.047 7.0 -    witness invalid (error (invalid c code)) 0.99 93 1.4  unknown 0.13 26 -    witness confirmed 68    1100 1.5  unknown 0.13 18 -    ??? 0.58 46 -    no conclusion 4.1  520 -    unknown 0.047 8.0 -    witness confirmed 1.7  81 1.6  unknown 5.2  240 -    unknown 5.3  240 -   
loops/n.c24_false-unreach-call.i timeout 920    430 -    timeout 920    7000 -    out of memory 210    15000 -    timeout 920    3400 -    true 0.051 14 -    ??? 0.73 46 -    no conclusion 4.3  530 -    timeout 920    2500 -    true 540    1700 -    timeout 920    4400 -    unknown 30    6000 -   
loops/nec11_false-unreach-call.i witness confirmed 0.049 15 1.5  witness invalid (error (invalid c code)) 0.94 94 1.3  witness confirmed 0.11 23 1.4  witness confirmed 1.6  170 1.4  witness confirmed 0.14 12 1.4  witness confirmed 1.4  46 1.4  witness confirmed 4.6  520 1.4  witness confirmed 0.13 32 1.4  witness confirmed 0.93 48 1.4  witness confirmed 6.5  250 1.4  witness confirmed 5.4  250 1.4 
loops/nec20_false-unreach-call.i witness confirmed 0.28 17 1.4  witness invalid (error (invalid c code)) 0.90 93 1.3  witness confirmed 0.29 39 1.8  witness confirmed 1.7  170 1.4  witness confirmed 0.16 12 1.5  witness confirmed 520    45 1.4  witness confirmed 29    3100 3.2  witness confirmed 0.29 34 1.5  witness confirmed 0.87 55 1.5  witness confirmed 5.7  250 1.4  witness confirmed 5.9  250 1.5 
loops/s3_false-unreach-call.i witness confirmed 22    45 34    unknown 1.0  85 -    witness confirmed 62    1000 32    out of memory 150    15000 -    witness confirmed 31    580 34    ??? 24    48 -    no conclusion 5.5  520 -    witness confirmed 4.9  70 33    unknown 0.35 17 -    unknown 71    1300 -    unknown 170    2000 -   
loops/string_false-unreach-call.i witness confirmed 1.7  18 2.0  witness invalid (error (invalid c code)) 1.4  110 1.5  witness confirmed 0.22 25 1.9  witness confirmed 1.9  210 1.8  witness confirmed 0.32 14 1.9  witness confirmed 50    45 1.7  no conclusion 4.1  520 -    witness confirmed 0.33 44 1.7  witness unconfirmed 1.3  81 1.5  unknown 5.4  240 -    unknown 5.1  240 -   
loops/sum01_bug02_false-unreach-call_true-termination.i witness confirmed 22    25 1.5  witness invalid (error (invalid c code)) 0.99 94 1.4  witness confirmed 0.28 24 1.5  witness confirmed 3.5  230 1.7  witness confirmed 0.087 11 1.6  witness confirmed 18    45 1.4  witness confirmed 8.3  570 1.5  witness confirmed 0.28 37 1.4  witness confirmed 0.95 61 1.5  unknown 5.4  240 -    unknown 5.6  250 -   
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i witness confirmed 11    20 1.5  witness invalid (error (invalid c code)) 0.98 95 1.4  witness confirmed 0.19 23 1.4  witness confirmed 3.2  230 1.6  witness confirmed 0.11 11 1.5  witness confirmed 10    45 1.7  witness confirmed 6.4  530 1.5  witness confirmed 0.22 36 1.4  witness unconfirmed 0.95 56 1.5  unknown 5.4  250 -    unknown 5.8  250 -   
loops/sum01_false-unreach-call_true-termination.i witness confirmed 35    28 1.5  witness invalid (error (invalid c code)) 1.0  99 1.4  true 0.28 23 -    witness confirmed 4.2  230 1.7  witness confirmed 0.11 12 1.6  witness confirmed 35    45 1.4  witness confirmed 11    610 1.6  witness confirmed 0.36 38 1.4  witness confirmed 1.5  63 1.5  unknown 5.4  250 -    unknown 5.6  250 -   
loops/sum03_false-unreach-call_true-termination.i witness confirmed 5.5  25 1.6  witness invalid (error (invalid c code)) 1.1  99 1.4  witness confirmed 0.28 23 1.5  witness confirmed 2.0  200 1.7  witness unconfirmed 0.11 12 1.7  witness confirmed 48    45 1.9  witness confirmed 12    830 1.5  witness confirmed 0.25 38 1.8  witness confirmed 1.7  72 1.6  witness confirmed 12    400 1.7  witness confirmed 32    680 1.7 
loops/sum04_false-unreach-call_true-termination.i witness confirmed 1.4  16 1.4  witness invalid (error (invalid c code)) 0.94 94 1.3  witness confirmed 0.26 23 1.5  witness confirmed 1.7  170 1.5  witness unconfirmed 0.096 12 1.5  witness confirmed 0.55 45 1.4  witness confirmed 8.3  570 1.4  witness confirmed 0.27 37 1.4  witness unconfirmed 0.92 52 1.4  witness confirmed 6.9  280 1.5  witness confirmed 7.0  270 1.5 
loops/sum_array_false-unreach-call.i witness confirmed 0.73 21 1.5  witness invalid (error (invalid c code)) 1.0  90 1.3  witness confirmed 0.13 24 1.5  witness confirmed 6.2  280 1.6  witness confirmed 0.33 14 1.6  ??? 0.55 45 -    witness confirmed 5.5  520 1.4  witness confirmed 0.23 39 1.4  witness confirmed 1.6  82 1.7  witness unconfirmed 6.0  250 1.4  witness confirmed 6.0  250 1.5 
loops/terminator_01_false-unreach-call_false-termination.i witness confirmed 0.073 15 1.4  witness invalid (error (invalid c code)) 0.84 91 1.4  witness confirmed 0.10 23 1.4  witness confirmed 1.6  160 1.4  witness confirmed 0.10 12 1.4  witness confirmed 1.4  45 1.4  no conclusion 3.9  520 -    witness confirmed 0.45 32 1.4  witness confirmed 0.87 51 1.4  witness confirmed 5.6  250 1.5  witness confirmed 5.7  250 1.4 
loops/terminator_02_false-unreach-call_true-termination.i witness confirmed 0.074 15 1.6  witness invalid (error (invalid c code)) 0.91 91 1.4  witness confirmed 0.11 23 1.4  witness confirmed 1.6  170 1.4  witness confirmed 0.23 13 1.5  witness confirmed 2.1  45 1.4  witness confirmed 4.4  510 1.4  witness confirmed 0.15 33 1.4  witness confirmed 0.97 59 1.4  witness confirmed 5.6  250 1.4  witness confirmed 5.5  250 1.4 
loops/terminator_03_false-unreach-call_true-termination.i witness confirmed 0.16 16 1.4  witness invalid (error (invalid c code)) 1.4  93 1.3  unknown 0.12 23 -    witness confirmed 2.4  210 1.4  witness confirmed 0.13 12 1.5  witness confirmed 2.9  45 1.4  witness confirmed 4.4  520 1.4  witness confirmed 0.19 32 1.4  witness confirmed 0.94 56 1.4  witness confirmed 5.5  250 1.5  witness confirmed 5.6  250 1.4 
loops/trex01_false-unreach-call_true-termination.i witness confirmed 0.078 15 1.5  witness invalid (error (invalid c code)) 0.96 92 1.6  witness confirmed 0.13 24 1.5  witness confirmed 1.7  160 1.5  witness confirmed 0.12 13 1.4  witness confirmed 1.6  45 1.4  no conclusion 12    520 -    witness confirmed 0.20 31 1.4  witness confirmed 0.92 48 1.4  witness confirmed 5.2  250 1.5  witness confirmed 5.8  250 1.5 
loops/trex02_false-unreach-call_true-termination.i witness confirmed 0.094 15 1.4  witness invalid (error (invalid c code)) 0.90 92 1.4  witness confirmed 0.11 23 1.4  witness confirmed 1.7  160 1.4  witness confirmed 0.15 12 1.4  witness confirmed 1.7  45 1.4  witness confirmed 4.4  530 1.4  witness confirmed 0.17 32 1.4  witness confirmed 0.88 52 1.4  witness confirmed 5.7  250 1.4  witness confirmed 5.5  250 1.5 
loops/trex03_false-unreach-call_true-termination.i witness confirmed 0.068 13 1.4  witness invalid (error (invalid c code)) 1.0  92 1.4  witness confirmed 0.11 24 1.4  witness confirmed 2.4  220 1.6  witness confirmed 0.12 14 1.5  witness confirmed 3.6  45 1.4  witness confirmed 4.6  530 1.4  witness confirmed 0.18 34 1.4  witness confirmed 1.0  72 1.4  witness confirmed 5.6  250 1.4  witness confirmed 5.9  240 1.4 
loops/verisec_NetBSD-libc__loop_false-unreach-call.i witness confirmed 0.58 16 1.4  witness invalid (error (invalid c code)) 0.96 92 1.4  witness confirmed 0.21 23 1.4  witness confirmed 1.6  170 1.7  witness confirmed 0.15 12 1.5  witness confirmed 2.7  45 1.4  no conclusion 4.0  520 -    witness confirmed 0.16 34 1.4  witness confirmed 0.95 60 1.4  witness confirmed 7.3  280 1.6  witness confirmed 6.7  260 1.5 
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call.i witness confirmed 42    37 1.9  witness invalid (error (invalid c code)) 1.3  110 1.4  witness invalid (error (invalid c code)) 0.29 27 1.4  witness confirmed 1.9  200 1.8  witness unconfirmed 0.67 18 1.6  ??? 0.59 45 -    no conclusion 4.1  520 -    witness confirmed 0.31 40 1.8  witness confirmed 1.3  86 1.7  witness timeout 9.2  290 91    witness timeout 7.9  280 91   
loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i true 0.46 18 -    witness invalid (error (invalid c code)) 1.5  140 1.5  true 0.31 25 -    true 2.7  210 -    witness confirmed 0.20 13 1.7  true 83    45 -    no conclusion 4.3  520 -    true 0.16 32 -    true 1.4  60 -    witness unconfirmed 24    300 1.5  witness confirmed 19    420 1.5 
loops/vogal_false-unreach-call.i timeout 920    320 -    witness invalid (error (invalid c code)) 3.8  230 1.5  witness confirmed 0.42 31 2.8  witness confirmed 2.3  200 2.8  witness confirmed 0.82 22 2.1  witness confirmed 240    45 2.2  no conclusion 4.1  520 -    witness confirmed 1.6  82 2.6  witness confirmed 7.0  130 2.9  witness unconfirmed 130    1000 1.7  witness confirmed 17    660 3.3 
loops/while_infinite_loop_4_false-unreach-call_true-termination.i witness confirmed 0.082 13 1.4  witness invalid (error (invalid c code)) 0.87 92 1.4  witness confirmed 0.12 23 1.4  witness confirmed 1.6  160 1.4  witness confirmed 0.14 12 1.6  witness confirmed 20    1400 1.4  true 4.8  530 -    witness confirmed 0.30 32 1.4  witness confirmed 0.97 51 1.4  witness confirmed 5.7  250 1.5  witness confirmed 5.4  250 1.4 
loops/array_true-unreach-call.i true 0.90 17 -    true 12    1600 -    true 0.54 24 -    true 2.3  210 -    true 0.058 11 -    ??? 0.51 45 -    true 5.1  530 -    true 0.16 29 -    true 1.3  47 -    true 5.9  250 -    true 5.8  240 -   
loops/bubble_sort_true-unreach-call.i true 0.031 12 -    timeout 920    11000 -    true 3.0  62 -    true 62    1200 -    true 0.25 18 -    ??? 0.58 45 -    no conclusion 4.1  520 -    true 0.20 27 -    true 1.6  72 -    unknown 5.0  240 -    unknown 5.1  240 -   
loops/count_up_down_true-unreach-call_true-termination.i false(reach) 0.075 16 -    true 850    720 -    true 0.59 26 -    timeout 900    1100 -    true 0.049 11 -    true 710    45 -    true 5.6  530 -    true 0.15 27 -    true 1.3  53 -    unknown 25    270 -    unknown 19    270 -   
loops/eureka_01_true-unreach-call.i timeout 920    710 -    true 860    1700 -    true 0.68 26 -    true 1.8  150 -    true 0.062 12 -    true 260    45 -    no conclusion 4.0  520 -    unknown 60    370 -    true 7.5  160 -    timeout 920    1000 -    unknown 48    1300 -   
loops/eureka_05_true-unreach-call.i false(reach) 8.0  23 -    timeout 910    5500 -    true 0.52 23 -    true 1.5  140 -    true 0.058 12 -    true 48    45 -    no conclusion 19    530 -    unknown 0.98 52 -    true 1.7  70 -    true 16    660 -    true 18    670 -   
loops/for_infinite_loop_1_true-unreach-call_false-termination.i true 0.038 10.0 -    true 31    1200 -    true 0.54 23 -    true 62    1800 -    true 0.069 12 -    true 580    45 -    true 5.1  530 -    true 0.14 27 -    true 1.4  56 -    true 5.3  250 -    true 5.9  250 -   
loops/for_infinite_loop_2_true-unreach-call_false-termination.i true 0.035 11 -    true 32    1300 -    true 0.53 23 -    true 62    1200 -    true 0.059 12 -    true 430    45 -    true 5.0  510 -    true 0.25 27 -    true 1.4  54 -    true 5.4  250 -    true 5.7  240 -   
loops/insertion_sort_true-unreach-call.i false(reach) 4.2  19 -    true 850    320 -    true 850    3800 -    timeout 920    460 -    timeout 920    200 -    ??? 0.47 45 -    no conclusion 590    6700 -    unknown 0.21 36 -    true 26    92 -    unknown 520    2400 -    timeout 920    650 -   
loops/invert_string_true-unreach-call.i false(reach) 1.9  27 -    true 870    2800 -    true 0.53 23 -    true 2.8  210 -    true 0.065 12 -    ??? 0.52 45 -    true 11    570 -    unknown 0.22 37 -    true 1.6  63 -    true 17    660 -    true 24    670 -   
loops/linear_sea.ch_true-unreach-call.i false(reach) 0.063 14 -    true 850    1500 -    true 0.73 30 -    unknown 63    1200 -    true 0.091 12 -    ??? 0.56 45 -    no conclusion 4.1  520 -    false(reach) 0.17 34 -    false(reach) 0.92 61 -    unknown 5.3  240 -    unknown 5.2  240 -   
loops/lu.cmp_true-unreach-call.i true 53    72 -    timeout 920    12000 -    true 0.78 24 -    true 1.6  140 -    true 0.074 13 -    true 180    49 -    no conclusion 4.1  520 -    true 0.38 31 -    true 6.7  200 -    unknown 5.5  240 -    unknown 5.4  240 -   
loops/matrix_true-unreach-call_true-termination.i exception (gremlins) 0.057 7.0 -    timeout 920    6900 -    true 0.53 23 -    true 3.2  250 -    unknown 0.049 12 -    ??? 0.56 45 -    no conclusion 4.1  510 -    unknown 0.046 9.0 -    true 1.3  53 -    unknown 5.2  240 -    unknown 5.2  240 -   
loops/n.c11_true-unreach-call.i true 0.85 16 -    true 320    1900 -    true 0.51 24 -    true 1.4  140 -    true 0.051 12 -    true 720    45 -    true 9.2  560 -    true 0.32 31 -    true 1.3  51 -    true 6.6  270 -    true 5.9  250 -   
loops/n.c40_true-unreach-call.i false(reach) 0.31 17 -    true 9.3  290 -    true 0.55 23 -    true 2.4  210 -    true 0.065 11 -    true 2.4  45 -    true 9.2  840 -    true 0.14 27 -    true 1.5  63 -    true 340    320 -    true 340    310 -   
loops/nec40_true-unreach-call.i false(reach) 0.35 15 -    true 8.2  280 -    true 0.53 23 -    true 2.4  210 -    true 0.051 12 -    true 2.3  45 -    true 9.5  830 -    true 0.14 27 -    true 1.5  63 -    true 350    310 -    true 350    300 -   
loops/string_true-unreach-call.i true 0.91 17 -    true 50    3900 -    true 0.66 31 -    true 1.8  140 -    true 0.095 12 -    true 840    45 -    no conclusion 4.1  520 -    true 0.20 28 -    true 1.7  65 -    true 12    410 -    true 7.4  270 -   
loops/sum01_true-unreach-call_true-termination.i true 1.3  17 -    true 590    520 -    true 0.54 24 -    timeout 900    800 -    true 0.080 12 -    true 840    45 -    true 5.8  530 -    true 0.27 31 -    true 1.3  51 -    unknown 5.4  250 -    unknown 6.6  240 -   
loops/sum03_true-unreach-call_false-termination.i true 0.20 17 -    true 160    560 -    true 0.54 23 -    true 120    1200 -    true 0.078 11 -    true 340    46 -    true 5.4  530 -    true 0.15 27 -    true 1.4  56 -    timeout 920    990 -    timeout 920    970 -   
loops/sum04_true-unreach-call_true-termination.i true 1.1  18 -    true 3.3  170 -    true 0.51 23 -    true 1.4  140 -    true 0.070 11 -    true 6.1  45 -    true 9.6  570 -    true 0.30 27 -    true 1.2  51 -    true 7.4  270 -    true 7.4  270 -   
loops/sum_array_true-unreach-call.i false(reach) 0.70 19 -    true 850    1300 -    true 32    610 -    timeout 920    1000 -    true 0.57 14 -    ??? 0.63 45 -    no conclusion 54    2400 -    unknown 0.31 38 -    true 1.9  76 -    timeout 920    620 -    timeout 920    670 -   
loops/terminator_02_true-unreach-call_true-termination.i true 0.88 21 -    timeout 920    210 -    true 0.80 31 -    true 2.3  200 -    true 0.16 13 -    true 2.3  45 -    true 5.0  520 -    true 0.27 27 -    true 1.4  57 -    true 5.6  250 -    true 5.9  250 -   
loops/terminator_03_true-unreach-call_true-termination.i true 0.39 18 -    true 13    1100 -    true 0.61 28 -    true 2.3  210 -    timeout 920    130 -    true 840    45 -    true 5.1  530 -    true 0.14 30 -    true 1.3  50 -    true 5.7  240 -    true 5.9  250 -   
loops/trex01_true-unreach-call.i true 0.91 16 -    true 68    4000 -    true 0.86 34 -    true 180    1100 -    true 0.087 12 -    true 840    45 -    no conclusion 12    530 -    true 0.32 30 -    true 1.2  50 -    true 5.8  250 -    true 5.6  250 -   
loops/trex02_true-unreach-call_true-termination.i true 0.15 15 -    true 16    2600 -    true 0.65 27 -    true 2.2  200 -    true 0.090 12 -    true 850    45 -    true 5.3  530 -    true 0.15 29 -    true 1.3  55 -    true 5.9  240 -    true 5.8  250 -   
loops/trex03_true-unreach-call.i false(reach) 0.083 13 -    true 860    5100 -    true 1.2  39 -    true 2.8  210 -    true 0.11 13 -    true 840    45 -    true 28    2900 -    true 0.18 31 -    true 1.5  58 -    true 6.1  240 -    true 5.4  250 -   
loops/trex04_true-unreach-call_false-termination.i true 0.49 17 -    true 3.5  210 -    true 0.64 27 -    true 2.3  210 -    true 0.12 13 -    true 840    45 -    no conclusion 4.2  520 -    true 0.20 30 -    true 1.3  53 -    true 5.5  250 -    true 5.4  250 -   
loops/veris.c_NetBSD-libc__loop_true-unreach-call.i true 0.25 15 -    true 160    780 -    true 0.54 23 -    true 65    330 -    true 0.054 12 -    true 2.8  45 -    no conclusion 4.0  520 -    true 0.16 27 -    true 1.4  60 -    true 5.7  250 -    true 6.4  250 -   
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call.i true 0.043 13 -    true 10    480 -    true 89    63 -    true 62    1100 -    true 0.13 13 -    ??? 0.57 45 -    no conclusion 4.2  520 -    true 0.20 28 -    true 1.7  72 -    true 5.8  250 -    true 6.4  250 -   
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call.i true 0.29 15 -    true 6.7  260 -    true 0.52 24 -    true 2.6  220 -    true 0.082 12 -    true 40    45 -    no conclusion 4.2  510 -    true 0.13 27 -    true 1.4  56 -    true 5.8  250 -    true 7.1  280 -   
loops/vogal_true-unreach-call.i timeout 920    380 -    timeout 920    12000 -    true 0.71 30 -    true 65    1200 -    true 0.18 12 -    true 840    45 -    no conclusion 4.0  520 -    unknown 0.36 45 -    true 2.2  74 -    true 42    660 -    true 630    980 -   
loops/while_infinite_loop_1_true-unreach-call_false-termination.i true 0.047 11 -    true 33    1400 -    true 0.52 23 -    true 1.4  140 -    true 0.043 11 -    true 450    45 -    true 4.6  530 -    true 0.13 27 -    true 1.3  57 -    true 5.5  240 -    true 5.4  240 -   
loops/while_infinite_loop_2_true-unreach-call_false-termination.i true 0.028 12 -    true 31    1300 -    true 0.48 23 -    true 1.4  140 -    true 0.051 11 -    true 590    45 -    true 4.6  520 -    true 0.13 27 -    true 1.4  57 -    true 5.5  250 -    true 6.3  250 -   
loops/while_infinite_loop_3_true-unreach-call_false-termination.i true 0.049 11 -    true 60    1300 -    true 0.49 23 -    true 1.4  130 -    true 0.049 11 -    true 850    45 -    true 4.8  510 -    true 0.14 27 -    true 1.4  57 -    true 5.6  250 -    true 5.7  250 -   
loop-acceleration/array_false-unreach-call1.i timeout 920    320 -    witness invalid (error (invalid c code)) 74    1900 2.4  true 0.65 72 -    witness confirmed 52    1300 4.3  true 0.053 11 -    witness confirmed 0.54 45 3.1  witness confirmed 72    2900 5.3  timeout 920    4300 -    witness unconfirmed 13    200 1.5  timeout 920    990 -    timeout 920    1200 -   
loop-acceleration/array_false-unreach-call2.i timeout 920    510 -    true 72    1900 -    true 0.68 80 -    witness confirmed 48    5000 6.1  true 0.073 12 -    witness confirmed 0.68 45 6.5  witness confirmed 530    3300 13    timeout 920    7500 -    witness unconfirmed 270    620 12    timeout 920    660 -    timeout 920    1200 -   
loop-acceleration/array_false-unreach-call3.i timeout 920    440 -    true 28    490 -    true 0.53 30 -    witness confirmed 9.8  470 5.4  true 0.075 11 -    true 840    45 -    no conclusion 67    2900 -    witness confirmed 50    1400 4.4  true 1.4  51 -    timeout 920    990 -    timeout 920    990 -   
loop-acceleration/const_false-unreach-call1.i timeout 920    200 -    witness invalid (error (invalid c code)) 5.5  210 2.3  true 0.48 23 -    witness confirmed 7.1  380 5.5  true 0.042 11 -    witness confirmed 0.59 45 4.3  witness confirmed 19    1400 6.5  witness confirmed 18    370 4.3  witness unconfirmed 3.4  98 1.9  timeout 920    580 -    timeout 920    990 -   
loop-acceleration/diamond_false-unreach-call1.i witness confirmed 67    81 12    true 850    4200 -    true 0.57 26 -    witness confirmed 5.1  260 11    true 0.081 11 -    witness confirmed 220    45 8.6  witness confirmed 19    1400 4.9  witness confirmed 0.41 43 11    true 1.3  54 -    witness confirmed 150    660 1.9  witness confirmed 150    310 2.0 
loop-acceleration/functions_false-unreach-call1.i timeout 920    290 -    true 8.6  1300 -    true 0.51 23 -    timeout 920    1900 -    true 0.066 11 -    witness timeout 0.95 45 91    no conclusion 12    530 -    timeout 920    220 -    true 1.3  54 -    timeout 920    990 -    timeout 920    980 -   
loop-acceleration/multivar_false-unreach-call1.i witness confirmed 0.093 16 1.4  witness invalid (error (invalid c code)) 0.92 92 1.3  unknown 0.10 23 -    witness confirmed 1.6  160 1.4  witness confirmed 0.11 12 1.5  witness confirmed 1.2  45 1.4  witness confirmed 4.3  530 1.4  witness confirmed 0.15 30 1.4  witness confirmed 0.90 52 1.4  witness confirmed 5.4  250 1.5  witness confirmed 5.4  250 1.4 
loop-acceleration/nested_false-unreach-call1.i timeout 920    260 -    true 220    8400 -    true 0.53 23 -    timeout 920    1300 -    true 0.060 11 -    witness timeout 3.0  45 91    timeout 920    2900 -    timeout 920    410 -    out of memory 39    15000 -    timeout 920    1000 -    timeout 920    1000 -   
loop-acceleration/phases_false-unreach-call1.i exception (gremlins) 0.11 15 -    true 4.4  230 -    true 0.50 23 -    timeout 920    1100 -    true 0.053 11 -    witness timeout 0.79 45 91    no conclusion 320    2900 -    timeout 920    240 -    true 1.2  51 -    timeout 920    660 -    unknown 41    410 -   
loop-acceleration/phases_false-unreach-call2.i witness confirmed 0.070 12 1.4  witness invalid (error (invalid c code)) 0.91 90 1.3  witness confirmed 0.11 23 1.4  witness confirmed 1.6  160 1.4  witness confirmed 0.68 39 1.4  witness confirmed 1.6  45 1.4  no conclusion 4.4  520 -    witness confirmed 0.31 32 1.4  witness confirmed 0.95 54 1.4  unknown 5.3  240 -    unknown 5.3  240 -   
loop-acceleration/simple_false-unreach-call1.i exception (gremlins) 850    260 -    true 2.7  150 -    true 0.49 23 -    timeout 920    1200 -    true 0.061 11 -    witness timeout 0.76 45 91    no conclusion 89    2900 -    timeout 920    220 -    out of memory 51    15000 -    timeout 920    670 -    timeout 920    1200 -   
loop-acceleration/simple_false-unreach-call2.i witness confirmed 0.072 14 1.4  witness invalid (error (invalid c code)) 0.91 90 1.4  unknown 0.091 23 -    witness confirmed 1.6  160 1.4  witness confirmed 0.10 11 1.4  witness confirmed 0.98 46 1.3  witness confirmed 4.2  530 1.3  witness confirmed 0.18 30 1.3  witness confirmed 0.89 45 1.4  witness confirmed 5.4  240 1.4  witness confirmed 5.5  250 1.4 
loop-acceleration/simple_false-unreach-call3.i witness confirmed 0.063 12 1.4  witness invalid (error (invalid c code)) 0.92 90 1.4  witness confirmed 0.11 23 1.4  witness confirmed 1.6  160 1.4  witness confirmed 0.10 11 1.5  witness confirmed 0.54 45 1.4  witness confirmed 4.3  530 1.4  witness confirmed 0.16 29 1.4  witness confirmed 0.86 46 1.4  witness confirmed 5.3  250 1.5  witness confirmed 5.6  240 1.4 
loop-acceleration/simple_false-unreach-call4.i exception (gremlins) 1.4  28 -    true 2.1  140 -    true 0.51 23 -    timeout 920    1300 -    true 0.071 11 -    witness timeout 0.80 45 91    no conclusion 92    2900 -    timeout 920    9900 -    out of memory 50    15000 -    timeout 920    660 -    timeout 920    1200 -   
loop-acceleration/underapprox_false-unreach-call1.i witness confirmed 1.5  17 1.4  witness invalid (error (invalid c code)) 0.95 91 1.4  witness confirmed 0.25 23 1.4  witness confirmed 1.7  170 1.4  witness confirmed 0.10 11 1.6  witness confirmed 0.56 45 1.4  witness confirmed 6.0  530 1.5  witness confirmed 0.15 32 1.4  witness unconfirmed 0.91 49 1.4  witness confirmed 6.1  250 1.4  witness confirmed 7.0  250 1.5 
loop-acceleration/underapprox_false-unreach-call2.i witness confirmed 1.00 18 1.4  witness invalid (error (invalid c code)) 0.95 90 1.4  witness confirmed 0.26 23 1.4  witness confirmed 1.6  170 1.4  witness confirmed 0.084 11 1.6  witness confirmed 0.60 46 1.4  witness confirmed 6.2  510 1.5  witness confirmed 0.15 32 1.4  witness unconfirmed 0.88 49 1.3  witness confirmed 6.1  250 1.5  witness confirmed 6.0  250 1.5 
loop-acceleration/array_true-unreach-call1.i timeout 920    330 -    true 71    1900 -    true 0.62 72 -    true 43    190 -    true 0.068 11 -    true 310    45 -    timeout 920    8600 -    true 0.15 30 -    true 5.8  130 -    timeout 920    510 -    timeout 920    980 -   
loop-acceleration/array_true-unreach-call2.i timeout 920    510 -    true 71    1900 -    true 0.68 80 -    false(reach) 46    4800 -    true 0.059 11 -    true 350    45 -    timeout 920    6200 -    unknown 380    3700 -    true 58    400 -    timeout 920    1000 -    timeout 920    1000 -   
loop-acceleration/array_true-unreach-call3.i true 0.24 15 -    true 130    660 -    true 0.53 27 -    true 4.2  220 -    true 0.062 11 -    true 620    45 -    true 4.9  520 -    true 0.19 31 -    true 1.2  51 -    true 6.1  250 -    true 5.7  250 -   
loop-acceleration/array_true-unreach-call4.i timeout 920    440 -    true 8.9  300 -    true 0.52 28 -    true 3.8  220 -    true 0.072 11 -    true 840    45 -    no conclusion 64    2900 -    unknown 52    1500 -    true 1.3  51 -    timeout 920    990 -    timeout 920    990 -   
loop-acceleration/const_true-unreach-call1.i true 0.26 15 -    true 2.8  150 -    true 0.49 23 -    true 2.6  190 -    true 0.059 11 -    true 300    45 -    true 5.1  530 -    true 0.16 27 -    true 1.9  79 -    timeout 920    990 -    timeout 920    1200 -   
loop-acceleration/diamond_true-unreach-call1.i false(reach) 66    84 -    true 850    4200 -    true 0.60 27 -    true 190    1300 -    true 0.083 11 -    true 450    45 -    true 37    2900 -    false(reach) 0.43 43 -    true 1.3  51 -    true 560    500 -    true 790    460 -   
loop-acceleration/diamond_true-unreach-call2.i false(reach) 100    52 -    true 850    7600 -    true 1.2  50 -    true 5.7  260 -    true 0.48 12 -    true 76    45 -    true 18    1400 -    false(reach) 0.35 43 -    true 1.7  68 -    true 14    390 -    true 21    1200 -   
loop-acceleration/functions_true-unreach-call1.i timeout 920    240 -    true 8.5  1300 -    true 0.50 23 -    timeout 920    1900 -    true 0.056 12 -    true 430    45 -    no conclusion 12    530 -    true 0.13 27 -    true 1.2  51 -    timeout 920    650 -    timeout 920    970 -   
loop-acceleration/multivar_true-unreach-call1.i true 0.10 17 -    true 3.2  170 -    true 0.67 28 -    true 63    1800 -    true 0.075 11 -    true 840    45 -    true 5.3  530 -    true 0.28 27 -    true 1.3  51 -    true 5.9  240 -    true 5.3  250 -   
loop-acceleration/nested_true-unreach-call1.i timeout 920    330 -    true 250    8700 -    true 0.53 23 -    timeout 920    1300 -    true 0.071 12 -    true 300    45 -    timeout 920    2900 -    true 0.15 27 -    out of memory 39    15000 -    timeout 920    1000 -    timeout 920    1200 -   
loop-acceleration/overflow_true-unreach-call1.i true 0.16 15 -    true 2.7  150 -    true 0.49 23 -    true 120    1100 -    true 0.075 11 -    true 300    45 -    true 4.8  530 -    true 0.30 27 -    true 1.2  53 -    timeout 920    650 -    timeout 920    990 -   
loop-acceleration/phases_true-unreach-call1.i exception (gremlins) 0.11 16 -    true 4.5  230 -    true 0.48 23 -    segmentation fault 180    1100 -    true 0.059 11 -    true 230    45 -    no conclusion 320    2900 -    timeout 920    240 -    true 1.3  51 -    timeout 920    650 -    unknown 42    420 -   
loop-acceleration/phases_true-unreach-call2.i false(reach) 0.47 16 -    true 4.7  240 -    true 5.2  120 -    true 2.6  210 -    true 0.70 39 -    false(reach) 1.6  46 -    no conclusion 4.4  530 -    false(reach) 0.14 32 -    true 1.5  55 -    unknown 5.3  240 -    unknown 5.3  240 -   
loop-acceleration/simple_true-unreach-call1.i exception (gremlins) 850    260 -    true 2.7  150 -    true 0.47 25 -    timeout 920    1100 -    true 0.056 11 -    true 300    45 -    true 5.2  530 -    true 0.16 22 -    out of memory 50    15000 -    timeout 920    990 -    timeout 920    1000 -   
loop-acceleration/simple_true-unreach-call2.i exception (gremlins) 0.096 16 -    true 3.0  170 -    true 0.56 27 -    true 2.1  210 -    true 0.084 11 -    true 710    45 -    true 4.7  530 -    true 0.23 27 -    true 1.2  53 -    true 5.3  250 -    true 5.4  250 -   
loop-acceleration/simple_true-unreach-call3.i false(reach) 0.052 15 -    true 4.5  310 -    true 0.51 23 -    timeout 920    1800 -    true 0.069 11 -    true 840    45 -    true 5.0  520 -    true 0.13 26 -    true 1.2  54 -    timeout 920    660 -    timeout 920    990 -   
loop-acceleration/simple_true-unreach-call4.i exception (gremlins) 2.0  30 -    true 2.5  140 -    true 0.49 23 -    true 120    1100 -    true 0.068 11 -    true 300    45 -    true 5.0  520 -    true 0.15 22 -    out of memory 51    15000 -    timeout 920    650 -    timeout 920    1200 -   
loop-acceleration/underapprox_true-unreach-call1.i true 0.68 16 -    true 3.2  170 -    true 0.48 23 -    true 1.4  140 -    true 0.070 11 -    true 2.7  45 -    true 5.0  530 -    true 0.16 26 -    true 1.2  49 -    true 6.8  270 -    true 6.8  270 -   
loop-acceleration/underapprox_true-unreach-call2.i true 0.22 15 -    true 2.7  160 -    true 0.51 23 -    true 1.4  130 -    true 0.055 11 -    true 3.2  45 -    true 5.6  520 -    true 0.16 27 -    true 1.2  50 -    true 6.5  270 -    true 6.2  250 -   
loop-invgen/id_trans_false-unreach-call.i exception (gremlins) 0.51 18 -    witness invalid (error (invalid c code)) 0.92 95 1.4  unknown 0.10 24 -    true 3.7  220 -    witness unconfirmed 0.094 12 1.6  witness confirmed 350    45 1.5  witness confirmed 5.3  530 1.4  unknown 0.29 30 -    witness confirmed 1.3  76 1.6  witness confirmed 5.9  250 1.5  witness confirmed 6.1  250 1.4 
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call.i true 15    28 -    true 850    500 -    true 50    58 -    timeout 900    310 -    true 2.0  15 -    true 420    45 -    true 7.0  530 -    true 0.17 32 -    true 1.6  71 -    timeout 920    650 -    timeout 920    980 -   
loop-invgen/NetBSD_loop_true-unreach-call.i true 0.76 18 -    true 860    860 -    true 0.55 25 -    true 63    2200 -    true 0.055 12 -    true 390    45 -    true 6.1  530 -    true 0.27 31 -    true 1.5  64 -    true 6.8  270 -    true 13    570 -   
loop-invgen/SpamAssassin-loop_true-unreach-call.i true 280    150 -    true 850    4400 -    true 850    860 -    true 100    610 -    true 240    520 -    true 840    45 -    no conclusion 140    2900 -    true 0.25 31 -    true 19    180 -    true 7.8  270 -    timeout 920    1200 -   
loop-invgen/apache-escape-absolute_true-unreach-call.i true 14    41 -    true 850    1500 -    true 850    230 -    true 5.4  260 -    true 240    85 -    true 840    45 -    true 96    2900 -    true 0.30 37 -    true 3.2  130 -    true 8.3  270 -    timeout 920    1200 -   
loop-invgen/apache-get-tag_true-unreach-call.i true 7.9  34 -    true 850    660 -    true 26    120 -    timeout 910    450 -    true 1.8  20 -    true 850    45 -    true 90    2900 -    true 0.27 32 -    true 3.0  110 -    true 6.8  270 -    timeout 920    1200 -   
loop-invgen/down_true-unreach-call.i timeout 920    320 -    true 850    6000 -    true 0.65 27 -    timeout 920    890 -    true 0.080 11 -    true 840    45 -    no conclusion 490    2900 -    true 0.19 31 -    true 1.4  60 -    timeout 920    1000 -    timeout 920    970 -   
loop-invgen/fragtest_simple_true-unreach-call.i timeout 920    220 -    true 860    5200 -    true 0.67 28 -    timeout 920    1100 -    true 0.085 12 -    true 840    45 -    no conclusion 350    2900 -    true 0.17 34 -    true 1.6  61 -    timeout 920    990 -    timeout 920    980 -   
loop-invgen/half_2_true-unreach-call.i exception (gremlins) 0.075 16 -    true 850    4700 -    true 0.72 29 -    timeout 900    2100 -    true 0.071 12 -    true 840    45 -    no conclusion 100    2900 -    true 0.28 34 -    false(reach) 1.1  68 -    unknown 5.4  240 -    unknown 5.2  240 -   
loop-invgen/heapsort_true-unreach-call.i exception (gremlins) 0.22 19 -    true 850    4700 -    true 850    2300 -    true 140    390 -    true 68    330 -    true 850    45 -    no conclusion 260    3000 -    unknown 0.55 33 -    true 15    170 -    unknown 110    350 -    timeout 920    660 -   
loop-invgen/id_build_true-unreach-call.i true 0.52 19 -    out of memory 33    15000 -    true 2.0  31 -    timeout 900    470 -    true 0.25 30 -    true 310    45 -    true 7.2  560 -    true 0.29 34 -    true 1.3  49 -    true 5.9  250 -    timeout 920    1200 -   
loop-invgen/large_const_true-unreach-call.i exception (gremlins) 140    85 -    out of memory 160    15000 -    true 0.71 31 -    true 2.5  210 -    true 0.14 13 -    true 14    45 -    true 9.1  570 -    timeout 920    3200 -    true 1.6  68 -    true 7.0  270 -    true 6.6  270 -   
loop-invgen/nest-if3_true-unreach-call.i false(reach) 0.47 16 -    true 850    9100 -    true 47    320 -    timeout 920    1200 -    true 0.67 37 -    true 840    45 -    true 13    810 -    true 0.20 32 -    true 1.6  62 -    true 5.7  240 -    true 38    680 -   
loop-invgen/nested6_true-unreach-call.i true 160    79 -    true 860    11000 -    true 850    610 -    timeout 920    1600 -    true 13    210 -    true 840    45 -    true 90    3000 -    true 0.28 32 -    true 2.3  83 -    true 7.7  270 -    timeout 920    990 -   
loop-invgen/nested9_true-unreach-call.i true 0.73 17 -    true 860    610 -    true 170    340 -    timeout 920    1700 -    true 0.52 63 -    true 270    45 -    true 8.9  560 -    true 0.92 47 -    true 1.6  69 -    timeout 920    720 -    timeout 920    400 -   
loop-invgen/sendmail-close-angle_true-unreach-call.i exception (gremlins) 12    33 -    true 860    670 -    true 0.71 27 -    timeout 910    950 -    true 0.065 12 -    true 830    45 -    true 43    1500 -    true 0.23 32 -    false(reach) 1.1  79 -    timeout 920    650 -    timeout 920    1600 -   
loop-invgen/seq_true-unreach-call.i timeout 920    240 -    true 850    1700 -    true 1.1  29 -    timeout 920    1000 -    true 0.095 12 -    true 840    45 -    no conclusion 610    2900 -    true 0.21 34 -    true 1.6  59 -    timeout 920    990 -    timeout 920    970 -   
loop-invgen/string_concat-noarr_true-unreach-call.i timeout 920    290 -    true 860    3900 -    true 3.6  280 -    timeout 920    1200 -    true 0.15 21 -    true 840    45 -    no conclusion 170    2900 -    true 0.20 32 -    true 1.4  58 -    timeout 900    990 -    true 180    990 -   
loop-invgen/up_true-unreach-call.i timeout 920    300 -    true 860    7800 -    true 0.61 26 -    timeout 920    1200 -    true 0.082 11 -    true 840    45 -    no conclusion 120    2900 -    true 0.16 31 -    true 1.4  60 -    timeout 920    990 -    timeout 920    960 -   
loop-lit/afnp2014_true-unreach-call.c.i true 1.5  16 -    true 250    3700 -    true 0.54 26 -    true 4.6  210 -    true 0.066 12 -    true 460    45 -    true 17    1400 -    true 0.17 31 -    true 1.4  57 -    true 5.9  250 -    timeout 920    990 -   
loop-lit/bhmr2007_true-unreach-call.c.i true 0.036 12 -    true 8.8  1300 -    true 5.3  43 -    true 62    1100 -    true 0.066 12 -    true 840    45 -    true 10    580 -    true 0.27 27 -    true 4.0  55 -    unknown 4.9  240 -    unknown 4.9  240 -   
loop-lit/cggmp2005_true-unreach-call.c.i true 0.49 16 -    true 3.3  170 -    true 0.49 23 -    true 1.4  140 -    true 0.068 11 -    true 3.0  45 -    true 6.3  530 -    true 0.18 30 -    true 1.2  55 -    true 6.1  250 -    true 8.1  250 -   
loop-lit/cggmp2005_variant_true-unreach-call.c.i false(reach) 0.19 15 -    true 850    1000 -    true 0.68 29 -    timeout 900    300 -    true 0.094 12 -    true 840    45 -    true 6.1  530 -    true 0.12 27 -    true 1.3  51 -    unknown 5.5  250 -    unknown 5.6  250 -   
loop-lit/cggmp2005b_true-unreach-call.c.i true 0.80 16 -    out of memory 380    15000 -    true 0.52 23 -    true 1.8  150 -    true 0.070 12 -    true 230    45 -    true 6.0  530 -    true 0.14 27 -    true 5.1  180 -    timeout 920    660 -    true 500    720 -   
loop-lit/css2003_true-unreach-call.c.i false(reach) 0.075 13 -    true 440    900 -    true 0.65 29 -    true 2.4  210 -    true 0.071 12 -    true 210    45 -    true 6.0  530 -    true 0.14 31 -    true 1.4  60 -    timeout 920    1000 -    timeout 920    660 -   
loop-lit/ddlm2013_true-unreach-call.c.i false(reach) 18    24 -    out of memory 120    15000 -    true 0.68 31 -    timeout 920    830 -    true 0.21 12 -    true 840    45 -    no conclusion 850    2900 -    true 0.25 32 -    true 1.5  58 -    timeout 920    660 -    timeout 920    660 -   
loop-lit/gj2007_true-unreach-call.c.i timeout 920    280 -    true 7.2  240 -    true 0.52 23 -    true 1.7  140 -    true 0.072 11 -    true 230    45 -    true 32    2900 -    true 880    490 -    true 1.3  51 -    true 670    980 -    true 220    990 -   
loop-lit/gj2007b_true-unreach-call.c.i true 3.3  20 -    true 850    910 -    true 0.60 25 -    segmentation fault 62    2200 -    true 0.067 12 -    true 840    45 -    true 41    2400 -    true 0.19 31 -    true 1.3  56 -    true 6.4  270 -    true 6.8  280 -   
loop-lit/gr2006_true-unreach-call.c.i timeout 920    200 -    true 5.8  250 -    true 0.53 23 -    true 1.7  140 -    true 0.066 12 -    true 300    45 -    no conclusion 170    2900 -    timeout 920    280 -    true 1.3  51 -    true 120    1000 -    true 270    1200 -   
loop-lit/gsv2008_true-unreach-call.c.i true 0.42 18 -    true 850    4400 -    true 0.72 29 -    true 2.3  210 -    true 0.070 13 -    true 520    81 -    true 5.6  530 -    timeout 920    110 -    true 1.4  51 -    true 5.8  240 -    true 5.4  240 -   
loop-lit/hhk2008_true-unreach-call.c.i true 0.039 12 -    true 2.7  160 -    true 10    36 -    true 1.4  140 -    true 0.066 12 -    true 840    45 -    true 5.9  530 -    true 0.15 27 -    false(reach) 0.97 51 -    unknown 4.9  240 -    unknown 5.2  240 -   
loop-lit/jm2006_true-unreach-call.c.i exception (gremlins) 2.9  30 -    true 760    850 -    true 0.61 26 -    true 63    350 -    true 0.066 11 -    true 840    45 -    true 6.0  530 -    true 0.15 27 -    true 1.3  51 -    timeout 920    990 -    timeout 920    710 -   
loop-lit/jm2006_variant_true-unreach-call.c.i true 16    36 -    true 850    1000 -    true 0.63 26 -    true 62    1800 -    true 0.078 12 -    true 840    45 -    true 6.5  530 -    true 0.18 31 -    true 1.3  51 -    timeout 920    560 -    timeout 920    1000 -   
loop-lit/mcmillan2006_true-unreach-call.c.i false(reach) 1.0  17 -    true 850    830 -    true 57    1100 -    false(reach) 3.2  220 -    true 0.84 12 -    ??? 0.31 4.0 -    no conclusion 3.9  520 -    unknown 0.15 35 -    true 1.5  62 -    timeout 920    650 -    timeout 920    490 -   
loop-new/count_by_1_true-unreach-call.i true 0.23 15 -    true 2.7  150 -    true 0.52 23 -    true 120    1100 -    true 0.056 11 -    true 230    45 -    true 5.2  530 -    true 0.14 21 -    true 1.3  51 -    timeout 920    990 -    timeout 920    990 -   
loop-new/count_by_1_variant_true-unreach-call.i true 0.25 16 -    true 110    850 -    true 0.52 23 -    timeout 920    1700 -    true 0.075 11 -    true 370    45 -    true 4.9  520 -    timeout 920    230 -    true 1.4  54 -    timeout 920    1000 -    timeout 920    1200 -   
loop-new/count_by_2_true-unreach-call.i exception (gremlins) 240    150 -    true 2.3  150 -    true 0.48 23 -    timeout 920    1900 -    true 0.065 11 -    true 300    45 -    no conclusion 86    2900 -    true 0.13 27 -    true 1.2  50 -    timeout 920    980 -    timeout 920    1200 -   
loop-new/count_by_k_true-unreach-call.i false(reach) 0.063 12 -    true 57    1100 -    true 0.62 28 -    timeout 920    2700 -    true 0.058 12 -    true 230    45 -    no conclusion 440    2900 -    timeout 920    31 -    true 1.3  50 -    timeout 920    480 -    timeout 920    990 -   
loop-new/count_by_nondet_true-unreach-call.i timeout 920    250 -    true 99    2900 -    true 0.56 27 -    timeout 920    1700 -    true 0.13 12 -    true 710    45 -    no conclusion 120    2900 -    timeout 920    8900 -    true 1.4  57 -    timeout 920    980 -    timeout 920    1200 -   
loop-new/gauss_sum_true-unreach-call.i false(reach) 0.086 12 -    true 330    1900 -    true 0.59 24 -    timeout 900    780 -    true 0.074 11 -    true 840    45 -    no conclusion 4.3  520 -    timeout 920    31 -    false(reach) 0.90 59 -    unknown 5.5  240 -    unknown 5.2  250 -   
loop-new/half_true-unreach-call.i exception (gremlins) 1.4  19 -    true 850    970 -    true 0.55 24 -    timeout 900    870 -    true 0.068 12 -    true 540    45 -    true 9.9  570 -    false(reach) 0.26 34 -    true 1.3  56 -    timeout 920    650 -    timeout 920    990 -   
loop-new/nested_true-unreach-call.i false(reach) 0.067 17 -    true 850    3000 -    true 3.7  140 -    true 350    1000 -    true 0.091 12 -    true 840    45 -    timeout 920    3300 -    true 85    300 -    true 1.3  53 -    true 29    700 -    true 44    690 -   
../../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 status time(s) memory(MB) time(s) for witness
total files 142 24000 11000 93 142 43000 310000 51 142 5100 31000 78 142 38000 120000 82 142 3100 19000 87 142 46000 7700 520 142 12000 180000 64 142 16000 50000 98 142 1500 100000 70 142 45000 74000 130 142 49000 88000 130
correct results 79 790 1700 93 83 32000 160000 0 122 4900 15000 77 95 2600 46000 82 120 620 3300 79 115 45000 6600 64 82 1600 73000 64 103 1100 5700 98 115 370 8600 47 70 2900 22000 38 68 4300 25000 42
false negatives 1 0.46 18 0 10 2900 18000 0 13 6.6 420 0 2 6.4 430 0 12 0.79 140 0 2 930 90 0 1 4.8 530 0 1 0.16 32 0 7 550 2000 0 0 - - - 0 - - -
false positives 21 200 460 0 0 - - - 0 - - - 2 49 5000 0 0 - - - 1 1.6 46 0 0 - - - 5 1.4 190 0 5 5.0 320 0 0 - - - 0 - - -
false properties 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - - 0 - - -
score (142 files, max score: 235) -14 - - - 46 - - - 59 - - - 118 - - - 66 - - - 168 - - - 125 - - - 130 - - - 86 - - - 115 - - - 109 - - -
Tool BLAST 2.7.3 Cascade 0.1 CBMC 4.9 CPAchecker 1.3.10-svcomp15 ESBMC 1.24 Forest Perentie Seahorn SMACK Ultimate Automizer r12950 Ultimate Kojak r12950