Tool Ceagle Ceagle 1.3 @ 53cfa89
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-57-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-10 17:21:21 CET [[ 2017-01-14 18:00:17 CET ]] [[ 2017-01-14 19:52:12 CET ]] [[ 2017-01-14 18:07:02 CET ]] [[ 2017-01-14 19:59:19 CET ]]
Run set sv-comp17.ReachSafety-Loops
Options --compiler clang-3.7 [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
loops/array_false-unreach-call_true-termination.i 0 .11  .11  1.1  7.9 0      .098  .52 .34 13   40 6.2 3.3 83 290
loops/bubble_sort_false-unreach-call.i 0 .13  .13  1.5  8.2 0      0      .48 .32 10   39 7.2 3.8 150 330
loops/count_up_down_false-unreach-call_true-termination.i 1 .16  .16  1.6  7.8 0      0      3.5  2.0  77   260 7.7 4.1 120 320
loops/eureka_01_false-unreach-call.i 0 .10  .10  1.1  7.7 0      0      .58 .36 14   43 5.9 3.1 96 300
loops/for_bounded_loop1_false-unreach-call_true-termination.i 1 .99  .98  10    7.8 0      0      3.8  2.1  60   270 9.2 4.9 95 320
loops/insertion_sort_false-unreach-call_true-termination.i 0 .10  .10  1.0  8.2 0      .33   .61 .37 13   44 5.6 3.0 86 300
loops/invert_string_false-unreach-call_true-termination.i 0 .12  .12  1.0  7.7 0      .094  .52 .33 12   40 7.0 3.7 71 290
loops/linear_search_false-unreach-call.i 0 .10  .21  2.8  44   0      37      .51 .33 13   39 5.7 3.0 80 300
loops/ludcmp_false-unreach-call.i 0 17     17     210    15000   0      0      .52 .34 13   41 5.5 2.9 75 300
loops/matrix_false-unreach-call_true-termination.i 0 .12  .12  1.2  7.9 0      .094  .53 .34 6.6 40 5.6 3.0 95 290
loops/n.c24_false-unreach-call.i 0 .10  .10  1.1  8.0 0      0      .48 .32 8.7 39 6.1 3.2 82 310
loops/nec11_false-unreach-call_false-termination.i 0 .11  .11  1.2  7.8 0      0      .52 .34 13   42 5.4 2.9 100 290
loops/nec20_false-unreach-call_true-termination.i 0 .12  .12  1.1  7.9 0      0      .54 .35 8.6 41 6.5 3.5 70 290
loops/s3_false-unreach-call.i 0 .13  .13  1.4  8.7 0      0      .51 .33 11   41 6.0 3.2 120 300
loops/string_false-unreach-call_true-termination.i 0 .12  .12  .99 7.9 0      0      .52 .33 11   43 6.4 3.4 100 300
loops/sum01_bug02_false-unreach-call_true-termination.i 1 16     16     190    40   0      0      6.0  3.2  130   300 8.5 4.5 120 320
loops/sum01_bug02_sum01_bug02_base.case_false-unreach-call_true-termination.i 1 8.5   8.5   75    53   0      36      4.4  2.4  88   270 9.2 4.9 90 320
loops/sum01_false-unreach-call_true-termination.i 1 62     61     760    250   0      0      8.0  4.3  150   310 7.4 3.9 130 320
loops/sum03_false-unreach-call_true-termination.i 1 55     54     580    38   0      .32   4.9  2.7  90   280 7.3 3.9 140 320
loops/sum04_false-unreach-call_true-termination.i 0 .063 .19  .76 43   .0041 38      .47 .32 7.3 39 6.2 3.3 87 300
loops/sum_array_false-unreach-call.i 0 .11  .12  .90 7.7 0      .094  .53 .34 13   41 7.6 4.0 80 310
loops/terminator_01_false-unreach-call_true-termination.i 0 .11  .11  1.2  7.7 0      0      .51 .33 12   40 5.8 3.1 110 300
loops/terminator_02_false-unreach-call_true-termination.i 0 .15  .15  1.6  7.9 0      0      .54 .35 13   42 8.0 4.2 84 310
loops/terminator_03_false-unreach-call_true-termination.i 1 .46  .46  5.1  7.6 0      0      3.7  2.1  71   270 7.0 3.8 140 310
loops/trex01_false-unreach-call_true-termination.i 1 .19  .19  1.9  7.8 0      0      3.7  2.1  73   280 7.4 4.0 110 320
loops/trex02_false-unreach-call_true-termination.i 0 .10  .10  .92 7.9 0      0      .57 .36 14   41 6.0 3.2 120 300
loops/trex03_false-unreach-call_true-termination.i 1 .37  .36  4.1  7.8 0      0      3.9  2.2  76   280 8.4 4.5 140 330
loops/verisec_NetBSD-libc__loop_false-unreach-call_true-termination.i 0 .031 .032 .29 7.8 .0041 .070  .50 .32 11   39 7.2 3.8 66 290
loops/verisec_OpenSER__cases1_stripFullBoth_arr_false-unreach-call_true-termination.i 0 .035 .037 .34 7.8 .0041 .074  .52 .34 12   39 5.9 3.1 82 310
loops/vogal_false-unreach-call.i 0 .11  .11  1.2  7.7 0      0      .53 .33 13   39 6.4 3.4 140 310
loops/while_infinite_loop_4_false-unreach-call_true-termination.i 0 .046 .047 .27 7.7 .0041 .066  .51 .33 12   40 5.6 3.0 90 290
loops/array_true-unreach-call_true-termination.i 0 .11  .11  .97 8.1 0      .094  .50 .32 11   41 5.7 3.0 110 300
loops/bubble_sort_true-unreach-call.i 0 .11  .11  1.2  7.9 0      .094  .64 .42 6.5 39 6.0 3.2 110 310
loops/count_up_down_true-unreach-call_true-termination.i 0 900     900     13000    7000   0      .0041 .61 .40 7.6 39 6.6 3.5 110 300
loops/eureka_01_true-unreach-call.i 0 .11  .11  1.1  7.8 0      0      .55 .35 9.5 39 5.9 3.1 110 300
loops/eureka_05_true-unreach-call_true-termination.i 0 .035 .035 .28 7.9 .0041 .0041 .52 .33 11   43 6.3 3.3 130 320
loops/for_infinite_loop_1_true-unreach-call_false-termination.i 0 .13  .13  1.4  7.9 0      0      .50 .32 9.2 43 6.2 3.2 110 300
loops/for_infinite_loop_2_true-unreach-call_false-termination.i 0 .13  .13  1.4  7.9 0      0      .56 .35 6.4 40 5.7 3.0 120 300
loops/insertion_sort_true-unreach-call_true-termination.i 0 .14  .14  1.3  8.1 0      .26   .59 .38 9.1 40 5.5 2.9 99 300
loops/invert_string_true-unreach-call_true-termination.i 0 .11  .11  1.1  8.2 0      .20   .62 .39 9.3 40 7.1 3.8 76 300
loops/linear_sea.ch_true-unreach-call.i 0 .11  .11  1.0  8.0 0      .094  .52 .35 5.9 39 6.0 3.2 100 300
loops/lu.cmp_true-unreach-call.i 0 17     17     220    15000   0      0      .70 .44 7.6 41 6.0 3.1 120 300
loops/matrix_true-unreach-call_true-termination.i 0 .13  .13  1.0  7.9 0      .11   .59 .38 8.7 39 6.1 3.2 130 300
loops/n.c11_true-unreach-call_false-termination.i 0 .13  .13  1.0  7.8 0      0      .56 .35 10   40 6.1 3.2 140 300
loops/n.c40_true-unreach-call_true-termination.i 0 .14  .14  1.1  7.7 0      0      .54 .35 7.9 40 6.0 3.1 81 300
loops/nec40_true-unreach-call_true-termination.i 0 .10  .10  1.2  7.9 0      0      .68 .43 6.1 40 6.3 3.3 120 300
loops/string_true-unreach-call_true-termination.i 0 .11  .11  1.1  8.0 0      0      .50 .33 12   40 5.6 3.0 95 290
loops/sum01_true-unreach-call_true-termination.i 0 900     900     13000    11000   0      0      .61 .37 8.7 39 6.6 3.5 110 310
loops/sum03_true-unreach-call_false-termination.i 2 .48  .48  6.2  7.6 0      0      4.4  2.5  72   280 8.1 4.3 140 330
loops/sum04_true-unreach-call_true-termination.i 0 .039 .041 .20 7.9 .0041 .066  .55 .36 11   40 6.8 3.6 84 290
loops/sum_array_true-unreach-call.i 0 .17  .25  1.3  33   0      25      .53 .34 13   40 6.0 3.2 110 310
loops/terminator_02_true-unreach-call_true-termination.i 2 1.3   1.3   14    7.8 0      0      4.4  2.4  92   270 7.6 4.1 160 320
loops/terminator_03_true-unreach-call_true-termination.i 0 900     900     10000    990   0      0      .55 .35 9.3 40 6.3 3.3 130 310
loops/trex01_true-unreach-call_true-termination.i 0 900     900     13000    8400   0      0      .52 .32 12   40 5.8 3.1 120 290
loops/trex02_true-unreach-call_true-termination.i 0 .10  .10  1.2  7.8 0      0      .66 .41 8.9 40 6.2 3.3 100 300
loops/trex03_true-unreach-call_true-termination.i 2 1.9   1.9   23    7.9 0      0      4.7  2.6  68   280 8.6 4.6 170 340
loops/trex04_true-unreach-call_false-termination.i 0 900     890     13000    6600   0      0      .56 .35 9.2 39 6.6 3.5 120 310
loops/veris.c_NetBSD-libc__loop_true-unreach-call_true-termination.i 0 .083 .083 .19 7.8 .0041 .0041 .63 .39 7.2 40 6.1 3.2 140 290
loops/veris.c_OpenSER__cases1_stripFullBoth_arr_true-unreach-call_true-termination.i 0 .11  .11  1.1  7.9 0      0      .52 .33 11   40 6.0 3.2 95 300
loops/veris.c_sendmail__tTflag_arr_one_loop_true-unreach-call_true-termination.i 0 .14  .14  .94 7.7 0      0      .56 .36 12   45 7.1 3.8 87 300
loops/vogal_true-unreach-call.i 0 .11  .11  1.2  7.6 0      .086  .51 .34 11   40 6.2 3.3 98 300
loops/while_infinite_loop_1_true-unreach-call_false-termination.i 0 .037 .048 .33 7.7 .0041 2.8    .51 .33 9.3 42 6.1 3.2 100 290
loops/while_infinite_loop_2_true-unreach-call_false-termination.i 0 .034 .035 .30 7.8 .0041 .0041 .62 .40 8.8 39 6.6 3.5 110 310
loops/while_infinite_loop_3_true-unreach-call_false-termination.i 0 .037 .037 .27 7.9 .0041 0      .50 .32 9.4 39 6.5 3.4 130 310
loop-acceleration/array_false-unreach-call1_true-termination.i 0 .11  .11  1.1  7.8 0      0      .51 .34 12   41 7.6 4.0 81 290
loop-acceleration/array_false-unreach-call2_true-termination.i 0 .099 .10  1.2  7.6 0      0      .52 .33 13   40 7.4 3.9 78 300
loop-acceleration/array_false-unreach-call3_true-termination.i 0 .11  .11  1.1  7.8 0      0      .48 .32 10   39 6.3 3.4 81 300
loop-acceleration/const_false-unreach-call1.i 0 .035 .036 .26 7.8 .0041 0      .50 .32 11   39 6.3 3.3 120 300
loop-acceleration/diamond_false-unreach-call1.i 0 900     900     12000    560   0      36      .54 .34 12   40 5.7 3.0 120 300
loop-acceleration/functions_false-unreach-call1_true-termination.i 0 .035 .037 .22 7.7 .0041 .066  .53 .33 13   39 7.4 3.9 84 300
loop-acceleration/multivar_false-unreach-call1_true-termination.i 1 .19  .19  1.7  7.9 0      0      3.7  2.0  69   270 8.8 4.6 110 320
loop-acceleration/nested_false-unreach-call1.i 0 .031 .031 .32 7.7 .0041 0      .55 .35 9.7 41 7.7 4.0 81 300
loop-acceleration/phases_false-unreach-call1.i 0 .035 .046 .30 7.9 .0041 2.9    .51 .32 10   39 7.5 4.0 79 300
loop-acceleration/phases_false-unreach-call2.i 1 .23  .23  2.2  7.9 0      0      3.5  2.0  70   270 8.7 4.6 100 320
loop-acceleration/simple_false-unreach-call1.i 0 .035 .036 .19 7.7 .0041 0      .50 .33 13   40 5.5 2.9 100 300
loop-acceleration/simple_false-unreach-call2_true-termination.i 1 .16  .16  2.0  7.6 0      0      3.9  2.2  85   280 8.6 4.6 97 320
loop-acceleration/simple_false-unreach-call3_true-termination.i 1 .17  .17  1.7  7.8 0      0      3.6  2.1  85   270 8.3 4.4 120 320
loop-acceleration/simple_false-unreach-call4.i 0 .036 .050 .32 7.8 .0041 2.9    .50 .33 9.3 41 7.4 3.9 83 300
loop-acceleration/underapprox_false-unreach-call1_true-termination.i 0 .034 .036 .28 7.9 .0041 .070  .53 .33 13   42 7.9 4.1 80 310
loop-acceleration/underapprox_false-unreach-call2_true-termination.i 0 .078 .090 .23 7.8 .0041 2.9    .51 .32 10   41 7.3 3.8 56 290
loop-acceleration/array_true-unreach-call1_true-termination.i 0 .098 .10  1.0  7.7 0      0      .47 .31 4.3 39 6.0 3.2 110 300
loop-acceleration/array_true-unreach-call2_true-termination.i 0 .14  .14  1.0  7.8 0      0      .65 .42 6.0 40 5.6 3.0 120 290
loop-acceleration/array_true-unreach-call3_true-termination.i 0 .099 .099 1.3  7.8 0      0      .50 .32 9.0 39 6.7 3.5 130 310
loop-acceleration/array_true-unreach-call4_true-termination.i 0 .13  .13  .91 7.7 0      0      .67 .42 8.6 40 5.5 3.0 110 300
loop-acceleration/const_true-unreach-call1.i 0 .078 .079 .21 7.7 .0041 0      .61 .39 8.6 40 6.0 3.2 120 300
loop-acceleration/diamond_true-unreach-call1_true-termination.i 0 900     900     11000    520   0      0      .51 .33 11   43 6.2 3.3 120 310
loop-acceleration/diamond_true-unreach-call2.i 2 740     730     8200    5800   0      .033  6.7  3.9  67   320 39   27   680 560
loop-acceleration/functions_true-unreach-call1_true-termination.i 0 .038 .038 .26 7.8 .0041 0      .61 .40 7.4 41 5.7 3.0 98 290
loop-acceleration/multivar_true-unreach-call1_true-termination.i 2 .51  .51  5.2  7.8 0      0      360    350    8000   7000 8.4 4.5 120 320
loop-acceleration/nested_true-unreach-call1.i 0 .078 .079 .25 7.8 .0041 .070  .61 .39 11   42 5.8 3.1 120 300
loop-acceleration/overflow_true-unreach-call1.i 0 .036 .040 .32 7.8 .0041 .71   .54 .35 9.5 40 6.2 3.3 120 300
loop-acceleration/phases_true-unreach-call1.i 0 .045 .045 .25 7.6 .0041 0      .61 .40 7.6 39 6.1 3.2 110 300
loop-acceleration/phases_true-unreach-call2_false-termination.i 2 1.4   1.3   16    11   0      0      900    900    17000   410 9.3 5.4 200 330
loop-acceleration/simple_true-unreach-call1.i 0 .065 .065 .21 7.8 .0041 .0041 .49 .32 13   40 6.0 3.1 120 290
loop-acceleration/simple_true-unreach-call2_true-termination.i 2 .27  .27  3.7  7.9 0      0      3.9  2.2  77   270 7.4 4.0 150 320
loop-acceleration/simple_true-unreach-call3_true-termination.i 0 .13  .13  1.8  7.8 0      0      .62 .40 7.9 40 5.8 3.1 120 300
loop-acceleration/simple_true-unreach-call4.i 0 .037 .049 .29 7.5 .0041 2.9    .51 .33 7.5 41 5.5 3.0 120 290
loop-acceleration/underapprox_true-unreach-call1_true-termination.i 0 .079 .090 .26 7.7 .0041 2.9    .52 .33 12   44 6.1 3.2 110 290
loop-acceleration/underapprox_true-unreach-call2_true-termination.i 0 .040 .052 .24 7.8 .0041 3.0    .63 .40 9.2 40 6.1 3.2 120 300
loop-invgen/id_trans_false-unreach-call_true-termination.i 1 8.6   8.6   100    110   0      0      4.0  2.2  79   290 7.8 4.1 130 320
loop-invgen/MADWiFi-encode_ie_ok_true-unreach-call_true-termination.i 0 900     900     14000    4500   0      0      .68 .43 8.8 43 6.0 3.2 130 310
loop-invgen/NetBSD_loop_true-unreach-call_true-termination.i 0 900     890     11000    12000   0      .0041 .69 .43 8.4 41 5.9 3.2 88 280
loop-invgen/SpamAssassin-loop_true-unreach-call_false-termination.i 0 900     890     13000    5000   0      0      .47 .31 9.7 39 6.2 3.3 110 320
loop-invgen/apache-escape-absolute_true-unreach-call_true-termination.i 0 900     900     11000    2800   0      0      .49 .32 12   40 6.2 3.3 99 290
loop-invgen/apache-get-tag_true-unreach-call_true-termination.i 0 900     890     11000    12000   0      0      .51 .33 9.8 40 5.8 3.1 110 290
loop-invgen/down_true-unreach-call_true-termination.i 0 900     900     11000    9100   0      0      .50 .32 11   40 5.8 3.1 120 300
loop-invgen/fragtest_simple_true-unreach-call_true-termination.i 0 900     900     11000    640   0      0      .53 .32 10   40 5.5 2.9 130 300
loop-invgen/half_2_true-unreach-call_true-termination.i 0 900     900     13000    3500   0      0      .46 .31 6.3 40 6.2 3.3 120 300
loop-invgen/heapsort_true-unreach-call_true-termination.i 0 .11  .11  1.2  7.9 0      0      .65 .40 9.2 40 6.0 3.2 100 300
loop-invgen/id_build_true-unreach-call_true-termination.i 0 900     880     11000    6200   0      0      .49 .32 12   40 5.5 2.9 110 290
loop-invgen/large_const_true-unreach-call_true-termination.i 0 .11  .11  1.2  7.8 0      0      .57 .35 7.2 39 6.1 3.2 94 280
loop-invgen/nest-if3_true-unreach-call_true-termination.i 0 900     890     11000    9700   0      0      .53 .34 11   42 5.8 3.1 110 290
loop-invgen/nested6_true-unreach-call_true-termination.i 0 900     890     13000    5500   0      0      .69 .44 7.5 41 6.2 3.2 120 300
loop-invgen/nested9_true-unreach-call_true-termination.i 0 900     900     12000    10000   0      0      .49 .31 8.1 40 5.9 3.1 120 290
loop-invgen/sendmail-close-angle_true-unreach-call_true-termination.i 0 900     890     12000    9400   0      .0041 .54 .35 8.2 43 7.0 3.7 78 300
loop-invgen/seq_true-unreach-call_true-termination.i 0 900     900     11000    9100   0      0      .54 .33 9.8 40 5.6 3.0 110 290
loop-invgen/string_concat-noarr_true-unreach-call_true-termination.i 0 900     900     9700    660   0      0      .55 .36 10   45 6.1 3.2 140 300
loop-invgen/up_true-unreach-call_true-termination.i 0 900     900     9700    11000   0      .025  .61 .39 9.1 42 6.5 3.4 110 300
loop-lit/afnp2014_true-unreach-call_true-termination.c.i 0 900     900     11000    610   0      0      .53 .35 4.2 40 5.8 3.1 100 300
loop-lit/bhmr2007_true-unreach-call_true-termination.c.i 0 900     890     13000    11000   0      0      .50 .31 13   41 6.8 3.5 110 310
loop-lit/cggmp2005_true-unreach-call_true-termination.c.i 2 6.3   6.2   69    10   0      .098  5.2  2.9  50   280 12   6.6 120 360
loop-lit/cggmp2005_variant_true-unreach-call_true-termination.c.i 0 900     890     11000    6200   0      .012  .57 .35 13   41 6.1 3.2 120 300
loop-lit/cggmp2005b_true-unreach-call_true-termination.c.i 0 900     900     14000    330   0      0      .62 .40 6.8 40 6.5 3.4 130 300
loop-lit/css2003_true-unreach-call_true-termination.c.i 0 900     900     12000    9800   0      35      .48 .30 12   40 5.8 3.1 100 300
loop-lit/ddlm2013_true-unreach-call.i 0 900     890     13000    15000   0      0      .48 .32 7.8 40 5.9 3.1 99 300
loop-lit/gj2007_true-unreach-call_true-termination.c.i 0 900     900     11000    590   0      0      .53 .33 8.9 39 6.6 3.5 75 300
loop-lit/gj2007b_true-unreach-call_true-termination.c.i 0 900     900     11000    12000   0      0      .46 .31 6.0 39 6.4 3.3 110 300
loop-lit/gr2006_true-unreach-call_true-termination.c.i 0 900     900     11000    650   0      0      .57 .35 10   42 6.1 3.3 110 300
loop-lit/gsv2008_true-unreach-call_true-termination.c.i 0 900     900     13000    8400   0      0      .59 .37 8.8 40 5.2 2.8 81 300
loop-lit/hhk2008_true-unreach-call_true-termination.c.i 0 900     900     13000    5200   0      0      .61 .39 7.4 42 6.3 3.3 77 290
loop-lit/jm2006_true-unreach-call_true-termination.c.i 0 900     900     11000    5000   0      36      .53 .34 10   40 7.3 3.9 90 300
loop-lit/jm2006_variant_true-unreach-call_true-termination.c.i 0 900     890     13000    5100   0      0      .52 .32 14   39 7.8 4.1 75 300
loop-lit/mcmillan2006_true-unreach-call_true-termination.c.i 0 .10  .10  1.1  7.8 0      0      .51 .34 9.4 39 5.7 3.1 120 300
loop-lit/gcnr2008_false-unreach-call_false-termination.i 1 .18  .18  2.1  7.8 0      0      3.7  2.1  73   270 8.5 4.5 120 320
loop-new/count_by_1_true-unreach-call_true-termination.i 0 900     900     10000    660   0      .0082 .64 .41 8.3 39 5.9 3.1 110 290
loop-new/count_by_1_variant_true-unreach-call_true-termination.i 2 .61  .60  8.4  7.8 0      0      3.8  2.1  67   280 10   5.4 200 340
loop-new/count_by_2_true-unreach-call_true-termination.i 0 900     900     10000    680   0      0      .57 .37 14   44 6.9 3.7 80 290
loop-new/count_by_k_true-unreach-call_true-termination.i 0 900     890     11000    4400   0      0      .49 .32 9.6 39 6.7 3.5 100 300
loop-new/count_by_nondet_true-unreach-call_true-termination.i 0 900     900     9500    700   0      0      .52 .34 12   44 6.0 3.2 110 300
loop-new/gauss_sum_true-unreach-call_true-termination.i 0 900     900     14000    15000   0      0      .53 .34 12   41 6.0 3.2 120 300
loop-new/half_true-unreach-call_true-termination.i 0 900     900     13000    13000   0      0      .63 .39 8.7 39 5.7 3.0 110 310
loop-new/nested_true-unreach-call_true-termination.i 0 900     900     12000    12000   0      .0041 .48 .31 13   40 6.2 3.3 120 300
loop-industry-pattern/aiob_1_true-unreach-call.c 0 20     20     230    15000   0      0      .57 .38 9.6 40 5.7 3.0 120 290
loop-industry-pattern/aiob_2_true-unreach-call.c 0 20     20     220    15000   0      0      .49 .32 10   39 5.6 3.0 85 300
loop-industry-pattern/aiob_3_true-unreach-call.c 0 20     20     240    15000   0      0      .50 .32 8.9 39 6.3 3.3 98 310
loop-industry-pattern/aiob_4_true-unreach-call.c 0 20     20     250    15000   0      0      .53 .35 9.2 40 7.4 3.9 82 300
loop-industry-pattern/mod3_true-unreach-call.c 0 1.6   1.6   19    19   0      0      .63 .40 7.1 40 5.6 3.0 91 290
loop-industry-pattern/nested_true-unreach-call.c 0 .12  .12  1.6  7.9 0      0      .51 .34 8.9 41 5.6 3.0 120 290
loop-industry-pattern/ofuf_1_true-unreach-call.c 0 33     33     440    15000   0      0      .51 .32 11   40 6.0 3.2 110 300
loop-industry-pattern/ofuf_2_true-unreach-call.c 0 32     32     390    15000   0      .12   .48 .34 4.5 40 5.9 3.1 120 300
loop-industry-pattern/ofuf_3_true-unreach-call.c 0 32     32     400    15000   0      0      .49 .32 11   40 5.8 3.1 110 300
loop-industry-pattern/ofuf_4_true-unreach-call.c 0 32     32     390    15000   0      0      .63 .40 10   41 5.9 3.1 120 290
loop-industry-pattern/ofuf_5_true-unreach-call.c 0 32     32     420    15000   0      0      .46 .30 6.8 39 6.1 3.2 110 300
loops/heavy_true-unreach-call.c 0 .14  .14  1.4  18   0      0      .62 .40 9.7 40 7.3 3.9 96 300
loops/compact_false-unreach-call.c 0 .098 .098 1.2  7.9 0      0      .55 .35 14   42 7.1 3.7 75 300
loops/heavy_false-unreach-call.c 0 .14  .14  1.5  18   0      0      .50 .32 12   39 6.1 3.2 90 300
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
total 156 33 40000 40000 520000 440000 .11 270    156 83 48 1700 5600   156 360 190 5000 16000   156 1300 1300 26000 13000   156 700 380 12000 32000  
    correct results 24 33 910 890 10000 6400 0    36    15 64 36 1300 4200   15 120 65 1800 4800   7 1300 1300 25000 9400   9 110 66 1900 3200  
        correct true 9 18 760 740 8400 5800 0    .13 0 0 0 0 0   7 0 0 0 0   7 1300 1300 25000 9400   9 110 66 1900 3200  
        correct false 15 15 150 150 1700 570 0    36    15 64 36 1300 4200   8 120 65 1800 4800   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (156 tasks, max score: 261) 33
Run set sv-comp17.ReachSafety-Loops