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-BitVectors
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)
bitvector/byte_add_false-unreach-call_true-no-overflow.i false(unreach-call) 0 wit inspect 1.1   1.1   9.2  41   0      0     timeout 94    78    2200 1200 true 9.7 5.1 120 330 - -
bitvector/sum02_false-unreach-call_true-no-overflow.i timeout 0 wit inspect 900     890     11000    13000   0      0     error (invalid witness file) .51 .34 13 39 error (invalid witness file) 7.3 3.8 91 300 - -
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 1.7   1.7   21    9.0 0      0     - - true 9.9  5.3  130   330 true 400   350   8300 1400
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 2.0   2.0   28    9.7 0      0     - - true 9.2  5.0  94   330 true 420   370   11000 1300
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 29     29     380    490   0      0     - - true 8.8  7.0  260   310 timeout 960   950   17000 530
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect .59  .71  12    47   0      36     - - true 130    130    2900   480 timeout 960   950   27000 630
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect .68  .68  7.5  11   0      0     - - true 120    110    3100   470 timeout 960   950   27000 650
bitvector/gcd_4_true-unreach-call_true-no-overflow.i true 2 wit inspect 1.7   1.7   23    22   0      0     - - true 8.5  5.8  100   310 timeout 960   940   23000 890
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect .26  .26  2.9  8.3 0      0     - - true 7.0  4.4  130   340 true 96   76   2500 620
bitvector/jain_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .23  .23  2.2  7.8 0      0     - - out of memory 280    270    6100   7000 true 7.4 4.0 140 320
bitvector/jain_2_true-unreach-call_true-no-overflow.i true 2 wit inspect .23  .23  2.4  7.7 0      0     - - out of memory 240    240    3300   7000 true 7.5 4.0 140 320
bitvector/jain_4_true-unreach-call_true-no-overflow.i true 2 wit inspect .24  .34  3.1  43   0      35     - - out of memory 210    210    4400   7000 true 6.9 3.8 130 320
bitvector/jain_5_true-unreach-call_true-no-overflow.i true 1 wit inspect .21  .21  2.4  7.7 0      0     - - out of memory 360    350    6900   7000 timeout 960   810   17000 3200
bitvector/jain_6_true-unreach-call_true-no-overflow.i true 2 wit inspect .24  .24  2.6  7.7 0      0     - - out of memory 180    180    6200   7000 true 9.9 5.2 96 320
bitvector/jain_7_true-unreach-call_true-no-overflow.i true 2 wit inspect .24  .24  3.1  7.5 0      0     - - out of memory 300    290    5700   7000 true 7.9 4.3 140 330
bitvector/modulus_true-unreach-call_true-no-overflow.i true 2 wit inspect 1.8   1.8   20    49   0      0     - - true 14    12    310   340 unknown 34   29   650 330
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .26  .26  2.7  7.7 0      0     - - true 5.3  2.9  89   280 true 60   48   940 510
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 2 wit inspect .28  .28  3.6  7.5 0      0     - - true 6.1  3.4  70   290 timeout 960   930   17000 960
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect .68  .67  6.9  7.8 0      0     - - true 21    17    370   350 timeout 960   950   18000 1000
bitvector/sum02_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900     900     11000    5200   0      0     - - error (invalid witness file) .56 .35 10   39 error (invalid witness file) 6.1 3.2 100 300
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect .028 .028 .26 8.1 0      0     false(unreach-call) 16    9.0  310 490 true 8.0 4.3 120 320 - -
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect .064 .064 .17 8.1 0      0     false(unreach-call) 19    11    420 500 true 9.5 5.1 170 330 - -
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect .040 .040 .22 8.1 0      .11  false(unreach-call) 11    5.8  190 440 true 8.1 4.3 160 320 - -
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 4.0   4.0   37    8.7 0      .36  - - true 55    46    520   970 true 51   28   740 800
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 3.7   3.7   43    8.2 0      .11  - - true 19    11    320   590 true 64   35   790 1100
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 3.7   3.7   41    8.2 0      0     - - true 16    9.5  270   560 true 48   25   510 910
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c true 1 wit inspect 3.3   3.3   37    8.3 0      0     - - timeout 900    890    17000   1400 timeout 960   930   21000 1300
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 3.3   3.3   35    8.3 0      0     - - timeout 910    900    24000   5200 true 56   30   910 1100
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 3.3   3.3   37    8.3 0      0     - - timeout 900    900    20000   4100 true 44   24   760 1100
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 3.2   3.2   40    8.3 0      0     - - timeout 910    890    17000   4300 true 41   22   560 1100
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 3.4   3.4   37    8.2 0      0     - - timeout 910    900    13000   5300 true 44   23   540 1000
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 3.1   3.1   34    8.3 0      0     - - out of memory 870    860    16000   7000 true 44   24   620 1000
bitvector/soft_float_1_true-unreach-call_true-no-overflow.c.cil.c true 2 wit inspect 79     78     890    120   0      .086 - - timeout 900    850    20000   6200 true 130   110   3700 840
bitvector/soft_float_2_true-unreach-call_true-no-overflow.c.cil.c true 2 wit inspect 3.3   3.3   34    9.1 0      .11  - - out of memory 840    760    19000   7000 true 79   66   1700 860
bitvector/soft_float_3_true-unreach-call_true-no-overflow.c.cil.c true 1 wit inspect 3.0   3.0   35    8.6 0      0     - - out of memory 860    790    18000   7000 timeout 960   920   23000 1900
bitvector/soft_float_4_true-unreach-call_true-no-overflow.c.cil.c true 2 wit inspect 42     42     400    51   0      .22  - - true 290    280    10000   770 true 360   320   8100 900
bitvector/soft_float_5_true-unreach-call_true-no-overflow.c.cil.c true 2 wit inspect 2.9   2.8   29    8.7 0      0     - - out of memory 900    810    15000   7000 true 24   13   370 580
bitvector-regression/implicitfloatconversion_false-unreach-call.c false(unreach-call) 1 wit inspect .053 .053 .33 7.6 0      0     false(unreach-call) 3.5  2.0  73 280 false(unreach-call) 11   6.0 200 300 - -
bitvector-regression/implicitunsignedconversion_false-unreach-call.c false(unreach-call) 1 wit inspect .047 .047 .40 7.6 0      0     false(unreach-call) 3.4  1.9  64 260 false(unreach-call) 6.6 3.5 140 310 - -
bitvector-regression/integerpromotion_false-unreach-call.c false(unreach-call) 1 wit inspect .050 .050 .40 7.8 0      0     false(unreach-call) 3.4  1.9  44 270 false(unreach-call) 11   6.1 210 310 - -
bitvector-regression/recHanoi03_false-unreach-call.c aborted 0 wit inspect .19  .19  2.5  7.8 0      0     error (invalid witness file) .52 .34 13 40 error (invalid witness file) 6.1 3.2 120 300 - -
bitvector-regression/signextension2_false-unreach-call.c false(unreach-call) 1 wit inspect .087 .087 .87 7.9 0      0     false(unreach-call) 3.5  2.0  82 270 false(unreach-call) 7.2 3.8 140 320 - -
bitvector-regression/signextension_false-unreach-call.c false(unreach-call) 1 wit inspect .11  .11  .87 7.7 0      0     false(unreach-call) 3.6  2.0  68 270 false(unreach-call) 7.7 4.2 98 310 - -
bitvector-regression/implicitunsignedconversion_true-unreach-call.c true 2 wit inspect .038 .039 .35 7.7 0      .11  - - true 3.4  1.9  66   250 true 7.2 3.9 160 320
bitvector-regression/integerpromotion_true-unreach-call.c true 2 wit inspect .040 .040 .29 7.7 0      0     - - true 3.2  1.8  58   250 true 12   6.2 220 320
bitvector-regression/signextension2_true-unreach-call.c true 2 wit inspect .083 .084 .88 7.9 0      0     - - true 3.2  1.8  41   260 true 7.8 4.1 150 320
bitvector-regression/signextension_true-unreach-call.c true 2 wit inspect .12  .12  .77 7.9 0      0     - - true 4.2  2.4  47   260 true 7.5 4.0 160 310
bitvector-loops/diamond_false-unreach-call2.i false(unreach-call) 1 wit inspect .54  .54  5.5  7.7 0      0     false(unreach-call) 4.1  2.3  82 290 true 7.9 4.3 160 320 - -
bitvector-loops/overflow_false-unreach-call1.i unknown 0 wit inspect .067 .078 .23 7.8 .0041 2.8   error (invalid witness file) .50 .32 11 40 error (invalid witness file) 6.5 3.5 85 300 - -
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i aborted 0 wit inspect .13  .13  .97 7.7 0      0     error (invalid witness file) .54 .34 12 40 error (invalid witness file) 5.6 3.0 86 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 50 76 2000   2000   25000   19000 .0041 75    50 160 120 3500 4400   50 110   60   1900 4400   50 11000 11000 230000 100000   50 11000 10000 230000 30000  
    correct results 41 73 200   200   2200   1100 0      73    9 68 38 1300 3100   9 78   42   1400 2800   19 9100 8700 190000 89000   25 7800 7300 170000 23000  
        correct true 32 64 200   190   2200   1000 0      72    0 0 0 0 0   4 0   0   0 0   19 9100 8700 190000 89000   25 7800 7300 170000 23000  
        correct false 9 9 1.0 1.0 9.0 71 0      .11 9 68 38 1300 3100   5 78   42   1400 2800   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 4 3 7.6 7.6 83   65 0      0    0 94 78 2200 1200   1 9.7 5.1 120 330   0 2100 2000 42000 15000   0 2900 2700 61000 6400  
        correct-unconfirmed true 3 3 6.5 6.5 74   25 0      0    0 0 0 0 0   1 0   0   0 0   0 2100 2000 42000 15000   0 2900 2700 61000 6400  
        correct-unconfirmed false 1 0 1.1 1.1 9.2 41 0      0    0 94 78 2200 1200   0 9.7 5.1 120 330   0 0 0 0 0   0 0 0 0 0  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (50 tasks, max score: 86) 76
Run set sv-comp17.ReachSafety-BitVectors