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-Floats
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)
floats-cdfpl/newton_1_4_false-unreach-call.i false(unreach-call) 1 wit inspect 42     42     460    550   0      0      timeout 92   91   1900 2700 true 6.9 3.7 150 320 - -
floats-cdfpl/newton_1_5_false-unreach-call.i false(unreach-call) 1 wit inspect 31     31     270    560   0      0      false(unreach-call) 66   64   2000 620 true 8.9 4.7 95 330 - -
floats-cdfpl/newton_1_6_false-unreach-call.i false(unreach-call) 1 wit inspect 57     57     540    560   0      0      false(unreach-call) 19   18   410 530 true 8.5 4.5 99 320 - -
floats-cdfpl/newton_1_7_false-unreach-call.i false(unreach-call) 1 wit inspect 51     51     630    560   0      0      false(unreach-call) 36   34   900 1100 true 7.1 3.8 110 310 - -
floats-cdfpl/newton_1_8_false-unreach-call.i false(unreach-call) 1 wit inspect 23     23     210    560   0      .0041 false(unreach-call) 25   24   770 690 true 10   5.4 100 330 - -
floats-cdfpl/newton_2_6_false-unreach-call.i false(unreach-call) 1 wit inspect 120     120     1100    1900   0      0      timeout 92   91   1600 2300 true 9.0 4.8 96 310 - -
floats-cdfpl/newton_2_7_false-unreach-call.i false(unreach-call) 1 wit inspect 82     82     660    1900   0      0      timeout (false(unreach-call)) 90   88   1600 1500 true 8.5 4.5 120 320 - -
floats-cdfpl/newton_2_8_false-unreach-call.i false(unreach-call) 1 wit inspect 76     77     620    1900   0      36      false(unreach-call) 26   24   650 730 true 6.7 3.6 90 300 - -
floats-cdfpl/newton_3_6_false-unreach-call.i false(unreach-call) 1 wit inspect .031 .032 .12 7.7 0      0      timeout 92   91   1800 2800 true 7.4 3.9 170 330 - -
floats-cdfpl/newton_3_7_false-unreach-call.i false(unreach-call) 1 wit inspect 460     460     3500    4500   0      0      false(unreach-call) 87   85   2400 1800 true 6.7 3.6 140 320 - -
floats-cdfpl/newton_3_8_false-unreach-call.i false(unreach-call) 1 wit inspect 200     200     1500    4500   0      0      false(unreach-call) 81   79   2000 2200 true 7.3 3.9 87 310 - -
floats-cdfpl/sine_1_false-unreach-call.i false(unreach-call) 1 wit inspect 65     65     700    250   0      0      false(unreach-call) 49   47   1600 680 false(unreach-call) 27   22   760 900 - -
floats-cdfpl/sine_2_false-unreach-call.i false(unreach-call) 1 wit inspect 110     110     1100    240   0      0      timeout 92   91   2600 3100 timeout 97   91   1700 2900 - -
floats-cdfpl/sine_3_false-unreach-call.i false(unreach-call) 1 wit inspect 82     82     690    240   0      0      false(unreach-call) 41   40   1100 1200 timeout 97   90   1900 2700 - -
floats-cdfpl/square_1_false-unreach-call.i false(unreach-call) 1 wit inspect 56     56     730    93   0      0      false(unreach-call) 75   73   2100 680 false(unreach-call) 56   48   910 970 - -
floats-cdfpl/square_2_false-unreach-call.i false(unreach-call) 1 wit inspect 70     70     840    100   0      0      false(unreach-call) 48   47   1100 770 timeout 97   90   1800 1600 - -
floats-cdfpl/square_3_false-unreach-call.i false(unreach-call) 1 wit inspect 140     140     1700    100   0      0      timeout 92   90   2100 2800 timeout 97   90   1700 1900 - -
floats-cdfpl/newton_1_1_true-unreach-call.i true 2 wit inspect .026 .026 .13 7.7 0      0      - - timeout 900    900    20000   740 out of memory 240   240   7300 7000
floats-cdfpl/newton_1_2_true-unreach-call.i true 2 wit inspect .015 .016 .18 7.9 0      0      - - timeout 900    900    19000   550 out of memory 230   230   5200 7000
floats-cdfpl/newton_1_3_true-unreach-call.i true 2 wit inspect .020 .022 .14 7.9 0      0      - - timeout 900    900    16000   520 out of memory 200   200   2500 7000
floats-cdfpl/newton_2_1_true-unreach-call.i true 2 wit inspect .032 .032 .12 7.9 0      0      - - timeout 900    900    13000   560 out of memory 240   230   6200 7000
floats-cdfpl/newton_2_2_true-unreach-call.i true 2 wit inspect .036 .036 .11 7.6 0      0      - - timeout 900    900    9200   560 out of memory 210   200   3400 7000
floats-cdfpl/newton_2_3_true-unreach-call.i true 2 wit inspect .043 .044 .14 7.8 0      0      - - timeout 900    900    9800   550 out of memory 260   250   4800 7000
floats-cdfpl/newton_2_4_true-unreach-call.i true 2 wit inspect .036 .036 .13 7.6 0      0      - - timeout 900    900    8400   600 out of memory 220   220   6000 7000
floats-cdfpl/newton_2_5_true-unreach-call.i true 2 wit inspect .021 .021 .17 7.7 0      0      - - timeout 900    900    16000   770 out of memory 260   250   6500 7000
floats-cdfpl/newton_3_1_true-unreach-call.i true 2 wit inspect .021 .021 .16 7.7 0      0      - - timeout 900    900    18000   890 out of memory 200   200   4900 7000
floats-cdfpl/newton_3_2_true-unreach-call.i true 2 wit inspect .025 .025 .13 7.5 0      0      - - timeout 900    900    11000   610 out of memory 210   200   5400 7000
floats-cdfpl/newton_3_3_true-unreach-call.i true 2 wit inspect .024 .024 .14 7.6 0      0      - - timeout 900    900    19000   730 out of memory 250   240   5300 7000
floats-cdfpl/newton_3_4_true-unreach-call.i true 2 wit inspect .041 .041 .13 7.6 0      0      - - timeout 900    900    13000   740 out of memory 220   210   7200 7000
floats-cdfpl/newton_3_5_true-unreach-call.i true 2 wit inspect .029 .030 .12 7.7 0      0      - - timeout 900    900    25000   860 out of memory 260   250   5600 7000
floats-cdfpl/sine_4_true-unreach-call.i true 2 wit inspect .026 .026 .13 8.0 0      0      - - timeout 900    900    17000   560 out of memory 240   230   3900 7000
floats-cdfpl/sine_5_true-unreach-call.i true 2 wit inspect .028 .029 .11 7.7 0      0      - - timeout 900    900    17000   520 out of memory 270   260   4900 7000
floats-cdfpl/sine_6_true-unreach-call.i true 2 wit inspect .025 .025 .13 7.9 0      0      - - timeout 900    900    16000   630 out of memory 250   240   5200 7000
floats-cdfpl/sine_7_true-unreach-call.i true 2 wit inspect .020 .020 .20 7.8 0      0      - - timeout 900    900    16000   400 out of memory 250   240   5600 7000
floats-cdfpl/sine_8_true-unreach-call.i true 2 wit inspect 280     280     2400    250   0      0      - - timeout 900    900    16000   500 out of memory 230   220   4900 7000
floats-cdfpl/square_4_true-unreach-call.i true 2 wit inspect 200     200     2200    100   0      0      - - timeout 900    900    14000   610 out of memory 250   250   4000 7000
floats-cdfpl/square_5_true-unreach-call.i true 2 wit inspect 260     260     2800    110   0      0      - - true 550    550    8600   500 out of memory 290   290   3900 7000
floats-cdfpl/square_6_true-unreach-call.i true 2 wit inspect 210     210     2200    100   0      0      - - true 750    750    18000   610 out of memory 260   250   2900 7000
floats-cdfpl/square_7_true-unreach-call.i true 2 wit inspect 180     180     2000    92   0      0      - - true 280    270    2600   510 out of memory 300   300   6700 7000
floats-cdfpl/square_8_true-unreach-call.i true 2 wit inspect 56     56     590    91   0      0      - - true 25    24    410   340 out of memory 300   290   5900 7000
floats-cbmc-regression/float-div1_true-unreach-call.i true 2 wit inspect .15  .15  1.3  8.2 0      0      - - true 6.1  3.6  140   340 true 88   80   2100 680
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i true 2 wit inspect .12  .12  1.6  8.3 0      0      - - true 12    8.2  210   660 true 45   30   660 730
floats-cbmc-regression/float-no-simp1_true-unreach-call.i true 2 wit inspect .081 .081 .27 7.6 0      0      - - true 3.3  1.9  71   260 true 12   6.3 220 310
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true 2 wit inspect .14  .15  1.1  8.2 0      0      - - true 25    22    340   320 true 58   51   770 450
floats-cbmc-regression/float-no-simp3_true-unreach-call.i true 2 wit inspect .061 .062 .37 7.8 .0082 .21   - - true 3.2  1.8  50   260 true 15   7.9 150 310
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true 2 wit inspect .15  .15  1.2  8.0 0      0      - - true 6.9  3.7  90   290 true 22   13   420 510
floats-cbmc-regression/float-no-simp6_true-unreach-call.i true 2 wit inspect .091 .12  .39 14   .0082 7.2    - - true 4.4  2.5  47   260 true 14   7.7 250 320
floats-cbmc-regression/float-no-simp7_true-unreach-call.i true 2 wit inspect .042 .042 .32 7.8 0      0      - - true 3.3  1.9  63   260 true 12   6.6 210 310
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true 2 wit inspect .17  .28  1.6  44   0      36      - - true 5.3  2.9  96   270 true 13   7.3 210 300
floats-cbmc-regression/float-rounding1_true-unreach-call.i true 2 wit inspect .12  .12  1.4  8.1 0      0      - - error 5.4  2.9  110   280 unknown 7.6 4.0 150 320
floats-cbmc-regression/float-to-double1_true-unreach-call.i true 2 wit inspect .44  .44  5.8  8.3 0      0      - - true 5.5  3.0  96   280 true 130   120   1800 490
floats-cbmc-regression/float-to-double2_true-unreach-call.i true 2 wit inspect .066 .069 .47 7.8 .0082 .48   - - true 3.7  2.1  49   250 true 12   6.5 190 310
floats-cbmc-regression/float-zero-sum1_true-unreach-call.i true 2 wit inspect .067 .067 .37 7.8 .0082 .0041 - - true 3.8  2.2  59   260 unknown 6.0 3.2 100 300
floats-cbmc-regression/float11_true-unreach-call.i true 2 wit inspect .061 .062 .42 7.9 .0082 .31   - - true 3.4  1.9  62   260 true 13   7.3 260 320
floats-cbmc-regression/float12_true-unreach-call.i true 2 wit inspect .20  .20  2.3  8.5 0      0      - - true 3.7  2.1  69   260 true 18   12   260 310
floats-cbmc-regression/float13_true-unreach-call.i true 2 wit inspect .15  .15  1.5  7.9 0      0      - - true 3.5  2.0  66   250 true 13   7.1 280 320
floats-cbmc-regression/float14_true-unreach-call.i true 2 wit inspect .12  .12  1.5  8.4 0      .26   - - true 5.7  3.0  76   280 true 16   9.3 200 290
floats-cbmc-regression/float18_true-unreach-call.i true 2 wit inspect .066 .070 .55 8.2 .0082 .45   - - true 24    21    560   440 unknown 5.6 3.1 110 290
floats-cbmc-regression/float19_true-unreach-call.i true 2 wit inspect .17  .17  2.3  8.3 0      .074  - - true 6.3  3.4  76   280 true 14   8.3 290 300
floats-cbmc-regression/float1_true-unreach-call.i true 2 wit inspect .066 .066 .45 7.8 0      0      - - true 3.5  2.0  66   260 true 12   6.4 230 310
floats-cbmc-regression/float20_true-unreach-call.i true 2 wit inspect .33  .45  4.1  47   0      35      - - true 4.3  2.4  53   260 true 29   22   620 410
floats-cbmc-regression/float21_true-unreach-call.i true 2 wit inspect .15  .15  1.1  8.2 0      0      - - true 6.8  3.9  90   310 true 72   64   1100 620
floats-cbmc-regression/float22_true-unreach-call.i true 2 wit inspect .060 .062 .53 7.9 .012  .13   - - false(unreach-call) 6.0  3.3  96   290 unknown 17   9.4 260 320
floats-cbmc-regression/float2_true-unreach-call.i true 2 wit inspect .16  .26  .92 43   0      35      - - true 3.6  2.0  74   260 true 12   6.8 170 320
floats-cbmc-regression/float3_true-unreach-call.i true 2 wit inspect .078 .078 .56 7.6 0      0      - - true 4.1  2.4  60   280 true 20   13   330 340
floats-cbmc-regression/float4_true-unreach-call.i true 2 wit inspect .11  .11  1.3  8.2 0      0      - - true 67    64    1400   340 true 97   89   2500 520
floats-cbmc-regression/float5_true-unreach-call.i true 2 wit inspect .37  .37  4.9  9.2 0      0      - - true 4.0  2.3  58   270 true 38   32   880 310
floats-cbmc-regression/float6_true-unreach-call.i true 2 wit inspect .074 .076 .46 7.8 .012  .39   - - true 4.8  2.7  54   260 true 14   7.7 250 320
floats-cbmc-regression/float7_true-unreach-call.i true 2 wit inspect .054 .055 .30 7.7 0      0      - - true 3.3  1.9  57   250 unknown 6.3 3.3 120 300
floats-cbmc-regression/float8_true-unreach-call.i true 2 wit inspect .14  .14  1.1  8.1 0      0      - - true 6.7  4.0  72   290 true 14   7.7 280 300
floats-cbmc-regression/float_lib1_true-unreach-call.i true 2 wit inspect .12  .12  1.2  8.0 0      0      - - true 5.3  2.9  100   270 error 14   7.6 170 300
floats-cbmc-regression/float_lib2_true-unreach-call.i true 2 wit inspect .067 .069 .56 8.3 .0082 .070  - - true 5.8  3.1  83   270 true 17   9.5 350 460
float-benchs/cast_float_ptr_false-unreach-call.c false(unreach-call) 1 wit inspect .10  .10  1.3  7.6 0      0      false(unreach-call) 4.0 2.2 70 280 unknown 6.0 3.2 100 310 - -
float-benchs/cast_union_loose_false-unreach-call.c false(unreach-call) 1 wit inspect .13  .13  1.2  7.7 0      0      false(unreach-call) 4.1 2.3 80 280 unknown 7.2 3.8 91 300 - -
float-benchs/cast_union_tight_false-unreach-call.c false(unreach-call) 1 wit inspect .11  .11  1.2  7.8 0      0      false(unreach-call) 3.9 2.2 93 280 unknown 6.7 3.6 130 320 - -
float-benchs/float_int_inv_square_false-unreach-call.c false(unreach-call) 1 wit inspect .56  .56  6.0  11   0      0      false(unreach-call) 3.8 2.2 76 280 false(unreach-call) 13   7.2 230 310 - -
float-benchs/inv_square_false-unreach-call.c false(unreach-call) 1 wit inspect .42  .42  5.7  9.3 0      0      false(unreach-call) 3.8 2.2 61 290 false(unreach-call) 14   7.5 200 310 - -
float-benchs/nan_double_false-unreach-call.c false(unreach-call) 1 wit inspect .053 .053 .32 7.7 0      0      false(unreach-call) 3.6 2.0 74 280 false(unreach-call) 7.1 3.7 130 310 - -
float-benchs/nan_float_false-unreach-call.c false(unreach-call) 1 wit inspect .046 .046 .48 7.6 0      0      false(unreach-call) 3.5 2.0 62 280 false(unreach-call) 9.0 4.8 87 310 - -
float-benchs/sin_interpolated_index_false-unreach-call.c false(unreach-call) 1 wit inspect .022 .023 .20 8.1 0      0      unknown 3.6 2.0 79 270 true 21   14   310 900 - -
float-benchs/sqrt_poly2_false-unreach-call.c false(unreach-call) 1 wit inspect .12  .12  1.4  7.9 0      .070  false(unreach-call) 12   9.8 270 520 error 12   6.6 160 310 - -
float-benchs/Muller_Kahan_true-unreach-call.c out of memory 0 wit inspect 15     15     190    15000   0      0      - - error (invalid witness file) .60 .39 8.3 40 error (invalid witness file) 5.5 2.9 100 300
float-benchs/Rump_double_true-unreach-call.c true 2 wit inspect .065 .067 .41 7.9 .0082 .32   - - true 3.6  2.0  61   260 true 23   17   460 790
float-benchs/Rump_float_true-unreach-call.c true 2 wit inspect .10  .11  .41 7.9 .0082 .070  - - true 3.7  2.1  72   260 true 19   11   200 390
float-benchs/addsub_double_exact_true-unreach-call.c true 2 wit inspect .037 .040 .36 7.9 0      0      - - true 3.5  2.0  63   260 true 16   8.6 200 320
float-benchs/addsub_float_exact_true-unreach-call.c true 2 wit inspect .042 .042 .27 7.8 0      0      - - true 3.7  2.1  63   260 true 13   7.3 260 320
float-benchs/addsub_float_inexact_true-unreach-call.c true 2 wit inspect .041 .041 .35 7.6 0      0      - - true 4.3  2.4  46   260 true 13   7.0 200 320
float-benchs/arctan_Pade_true-unreach-call.c true 2 wit inspect 470     470     3500    1900   0      36      - - true 14    12    340   510 error 190   180   6300 2700
float-benchs/bary_diverge_true-unreach-call.c true 2 wit inspect 850     850     11000    510   0      0      - - error (invalid witness file) .50 .32 9.1 39 error (invalid witness file) 5.5 3.0 120 290
float-benchs/cast_float_union_true-unreach-call.c true 2 wit inspect .10  .10  1.1  7.9 0      0      - - true 3.2  1.8  64   250 error 11   5.7 230 300
float-benchs/cos_polynomial_true-unreach-call.c true 2 wit inspect 850     850     4800    1300   0      .037  - - error (invalid witness file) .67 .42 7.6 41 error (invalid witness file) 6.1 3.2 130 300
float-benchs/divmul_buf_diverge_true-unreach-call.c true 2 wit inspect .045 .045 .15 7.9 0      0      - - timeout 900    900    19000   1700 timeout 960   820   21000 4800
float-benchs/divmul_diverge_true-unreach-call.c true 2 wit inspect .033 .033 .15 7.6 0      0      - - timeout 900    900    24000   2700 timeout 960   820   15000 4800
float-benchs/drift_tenth_true-unreach-call.c true 2 wit inspect .21  .21  2.0  7.8 0      0      - - true 9.7  7.8  95   340 true 160   150   3100 650
float-benchs/exp_loop_true-unreach-call.c unknown 0 wit inspect 8.6   8.6   100    94   0      0      - - error (invalid witness file) .53 .35 6.6 40 error (invalid witness file) 6.2 3.3 120 300
float-benchs/feedback_diverge_true-unreach-call.c true 2 wit inspect .028 .029 .12 7.8 0      0      - - timeout 900    900    28000   2000 timeout 960   820   26000 4700
float-benchs/filter1_true-unreach-call.c true 2 wit inspect 850     850     10000    310   0      0      - - error (invalid witness file) .60 .38 8.7 40 error (invalid witness file) 6.4 3.4 120 310
float-benchs/filter2_alt_true-unreach-call.c true 2 wit inspect 850     850     12000    190   0      0      - - error (invalid witness file) .64 .40 8.3 40 error (invalid witness file) 6.9 3.7 83 290
float-benchs/filter2_iterated_true-unreach-call.c out of memory 0 wit inspect 30     30     340    15000   0      0      - - error (invalid witness file) .50 .33 7.4 42 error (invalid witness file) 6.0 3.2 120 290
float-benchs/filter2_reinit_true-unreach-call.c true 2 wit inspect 850     850     9300    360   0      0      - - error (invalid witness file) .49 .32 9.5 39 error (invalid witness file) 6.3 3.3 110 300
float-benchs/filter2_set_true-unreach-call.c true 2 wit inspect 850     850     10000    440   0      0      - - error (invalid witness file) .50 .32 9.5 40 error (invalid witness file) 7.1 3.7 64 290
float-benchs/filter2_true-unreach-call.c true 2 wit inspect 850     850     12000    250   0      0      - - error (invalid witness file) .69 .43 8.7 41 error (invalid witness file) 5.7 3.0 93 290
float-benchs/filter_iir_true-unreach-call.c true 2 wit inspect 850     850     6500    650   0      0      - - error (invalid witness file) .69 .44 8.9 41 error (invalid witness file) 5.8 3.1 120 290
float-benchs/float_double_true-unreach-call.c true 2 wit inspect .078 .080 .46 7.8 .0082 .34   - - true 3.3  1.9  71   260 true 13   7.1 250 320
float-benchs/image_filter_true-unreach-call.c out of memory 0 wit inspect 18     18     180    15000   0      0      - - error (invalid witness file) .52 .35 9.1 40 error (invalid witness file) 7.4 3.8 130 310
float-benchs/interpolation2_true-unreach-call.c true 2 wit inspect .11  .11  1.1  7.7 0      .11   - - true 51    49    1400   560 timeout 960   950   19000 580
float-benchs/interpolation_true-unreach-call.c true 2 wit inspect .13  .13  1.0  8.1 0      .22   - - true 68    65    1300   470 out of memory 210   200   5400 7000
float-benchs/inv_sqrt_Quake_true-unreach-call.c true 2 wit inspect 8.9   8.9   130    48   0      0      - - unknown 6.2  3.8  75   320 unknown 6.9 3.6 110 320
float-benchs/inv_square_int_true-unreach-call.c true 2 wit inspect .14  .14  1.5  8.8 0      0      - - true 3.6  2.1  62   270 true 89   82   1700 340
float-benchs/inv_square_true-unreach-call.c true 2 wit inspect .72  .72  9.3  9.1 0      0      - - true 3.5  2.0  51   280 true 39   32   1100 330
float-benchs/loop_true-unreach-call.c unknown 0 wit inspect .21  .21  2.3  7.8 0      0      - - error (invalid witness file) .52 .35 7.0 39 error (invalid witness file) 5.8 3.1 100 300
float-benchs/mea8000_true-unreach-call.c out of memory 0 wit inspect 480     480     6700    15000   0      0      - - error (invalid witness file) .64 .41 7.7 40 error (invalid witness file) 5.7 3.1 93 290
float-benchs/nan_double_range_true-unreach-call.c true 2 wit inspect .14  .26  .92 43   0      35      - - true 3.6  2.0  49   250 true 12   6.6 250 310
float-benchs/nan_float_range_true-unreach-call.c true 2 wit inspect .16  .16  1.7  7.7 0      0      - - true 4.2  2.4  52   260 true 14   8.2 280 310
float-benchs/rlim_exit_true-unreach-call.c true 2 wit inspect 850     850     10000    380   0      35      - - error (invalid witness file) .58 .37 9.7 42 error (invalid witness file) 5.9 3.1 110 300
float-benchs/rlim_invariant_true-unreach-call.c true 2 wit inspect 850     850     10000    410   0      0      - - error (invalid witness file) .49 .32 13   40 error (invalid witness file) 5.5 3.0 97 290
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call.c true 2 wit inspect .018 .018 .20 8.0 0      .066  - - error 4.2  2.3  52   260 out of memory 500   490   4700 7000
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call.c true 2 wit inspect .026 .027 .15 7.9 0      0      - - error 4.1  2.3  74   270 out of memory 530   520   8200 7000
float-benchs/sin_interpolated_index_true-unreach-call.c true 2 wit inspect .038 .038 .14 7.8 0      0      - - error 4.1  2.2  59   270 out of memory 110   110   2100 7000
float-benchs/sin_interpolated_negation_true-unreach-call.c true 2 wit inspect .027 .038 .25 12   0      3.9    - - error 5.5  3.0  57   290 out of memory 510   510   11000 7000
float-benchs/sin_interpolated_smallrange_true-unreach-call.c true 2 wit inspect .025 .026 .15 7.8 0      0      - - error 5.4  3.0  60   280 out of memory 660   650   16000 7000
float-benchs/sqrt_Householder_constant_true-unreach-call.c unknown 0 wit inspect 23     23     300    6100   0      0      - - error (invalid witness file) .64 .40 8.3 39 error (invalid witness file) 7.0 3.6 130 310
float-benchs/sqrt_Householder_interval_true-unreach-call.c true 2 wit inspect 850     850     5400    940   0      0      - - error (invalid witness file) .66 .41 7.4 40 error (invalid witness file) 7.0 3.7 81 290
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c true 2 wit inspect 850     850     5600    1200   0      0      - - error (invalid witness file) .49 .33 11   39 error (invalid witness file) 5.6 3.0 120 300
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c true 2 wit inspect 850     850     6500    720   0      0      - - error (invalid witness file) .51 .32 12   40 error (invalid witness file) 6.3 3.3 130 300
float-benchs/sqrt_biNewton_pseudoconstant_true-unreach-call.c true 2 wit inspect 850     850     8500    1400   0      0      - - error (invalid witness file) .48 .30 8.2 39 error (invalid witness file) 6.5 3.4 140 310
float-benchs/sqrt_poly_true-unreach-call.c true 2 wit inspect 20     20     270    85   0      0      - - true 77    76    850   470 true 550   550   14000 1400
float-benchs/water_pid_true-unreach-call.c out of memory 0 wit inspect 22     22     250    15000   0      0      - - error (invalid witness file) .65 .42 7.4 40 error (invalid witness file) 5.7 3.0 110 300
float-benchs/zonotope_2_true-unreach-call.c true 2 wit inspect .036 .036 .13 7.8 0      0      - - timeout 900    900    16000   1100 timeout 960   950   18000 1000
float-benchs/zonotope_3_true-unreach-call.c true 2 wit inspect .024 .026 .14 7.8 0      0      - - true 5.7  3.8  140   350 timeout 960   840   27000 4900
float-benchs/zonotope_loose_true-unreach-call.c true 2 wit inspect 13     13     150    79   0      0      - - true 4.1  2.7  71   320 true 620   610   13000 1200
float-benchs/zonotope_tight_true-unreach-call.c true 2 wit inspect 14     14     180    79   0      0      - - true 4.2  2.6  100   320 true 630   620   17000 1100
floats-esbmc-regression/Double_div_true-unreach-call.i true 2 wit inspect .055 .056 .47 7.9 .0082 .30   - - true 5.5  3.5  78   330 error 150   140   4400 1400
floats-esbmc-regression/Float_div_true-unreach-call.i true 2 wit inspect .11  .14  .51 14   .0082 7.2    - - true 4.1  2.3  81   290 error 170   170   4300 510
floats-esbmc-regression/ceil_nondet_true-unreach-call.i true 2 wit inspect .11  .11  1.5  8.2 0      0      - - error 6.1  3.3  79   270 unknown 11   5.8 220 300
floats-esbmc-regression/ceil_true-unreach-call.i true 2 wit inspect .061 .062 .55 8.2 .0082 .078  - - true 5.7  3.1  72   280 unknown 6.7 3.5 130 300
floats-esbmc-regression/copysign_true-unreach-call.i true 2 wit inspect .10  .10  .56 8.3 .0082 .40   - - true 6.8  3.6  76   270 unknown 7.5 4.0 110 310
floats-esbmc-regression/digits_for_true-unreach-call.i true 2 wit inspect .056 .058 .57 7.8 .0082 .42   - - timeout 900    900    25000   1000 timeout 960   950   14000 1400
floats-esbmc-regression/digits_while_true-unreach-call.i true 2 wit inspect .058 .061 .48 7.7 .0082 .58   - - timeout 900    900    21000   1000 timeout 960   950   29000 3100
floats-esbmc-regression/fabs_true-unreach-call.i true 2 wit inspect .064 .064 .58 7.9 .0082 .045  - - true 6.5  3.5  74   260 true 14   7.4 230 300
floats-esbmc-regression/fdim_true-unreach-call.i true 2 wit inspect .068 .070 .57 8.0 .0082 .32   - - true 5.7  3.1  73   280 unknown 6.4 3.4 120 300
floats-esbmc-regression/floor_nondet_true-unreach-call.i true 2 wit inspect .13  .13  1.2  8.1 0      0      - - error 5.2  2.8  120   270 unknown 11   5.7 170 300
floats-esbmc-regression/floor_true-unreach-call.i true 2 wit inspect .078 .078 .53 8.2 .0082 0      - - true 6.0  3.3  91   280 unknown 7.5 4.0 93 310
floats-esbmc-regression/fmax_true-unreach-call.i true 2 wit inspect .097 .097 .55 8.1 .0082 0      - - true 5.2  2.9  95   270 unknown 6.1 3.3 110 300
floats-esbmc-regression/fmin_true-unreach-call.i true 2 wit inspect .076 .081 .58 8.0 .0082 1.0    - - true 5.5  3.0  95   270 unknown 6.5 3.4 130 300
floats-esbmc-regression/fmod2_true-unreach-call.i true 2 wit inspect .11  .11  1.1  8.2 0      0      - - false(unreach-call) 11    5.6  94   320 unknown 11   5.7 200 310
floats-esbmc-regression/fmod3_true-unreach-call.i true 2 wit inspect .11  .11  1.0  8.0 0      0      - - false(unreach-call) 7.1  3.8  84   320 unknown 12   6.2 210 310
floats-esbmc-regression/fmod_true-unreach-call.i true 2 wit inspect .058 .059 .59 8.0 .0082 .20   - - true 5.4  2.9  97   270 unknown 6.9 3.6 100 310
floats-esbmc-regression/isgreater_true-unreach-call.i true 2 wit inspect .059 .059 .60 8.1 .0082 0      - - true 5.5  3.0  100   280 error 11   5.9 230 300
floats-esbmc-regression/isgreaterequal_true-unreach-call.i true 2 wit inspect .066 .068 .51 8.2 .0082 .19   - - true 6.1  3.3  81   280 error 11   5.9 180 310
floats-esbmc-regression/isless_true-unreach-call.i true 2 wit inspect .11  .18  .68 27   .0082 21      - - true 6.1  3.3  86   270 error 12   6.2 190 320
floats-esbmc-regression/islessequal_true-unreach-call.i true 2 wit inspect .070 .074 .64 8.2 .0082 .41   - - true 5.8  3.1  80   270 error 11   5.8 210 310
floats-esbmc-regression/islessgreater_true-unreach-call.i true 2 wit inspect .067 .067 .50 8.0 .0082 .074  - - true 6.5  3.5  74   270 error 11   5.8 250 300
floats-esbmc-regression/isunordered_true-unreach-call.i true 2 wit inspect .082 .12  .56 17   .0082 11      - - true 6.0  3.2  92   280 error 11   6.0 190 310
floats-esbmc-regression/lrint_true-unreach-call.i true 2 wit inspect .092 .12  .64 14   .016  7.0    - - error 5.5  2.9  89   270 unknown 6.8 3.6 150 310
floats-esbmc-regression/modf_true-unreach-call.i true 2 wit inspect .13  .13  1.1  8.1 0      .074  - - true 5.2  2.7  86   270 unknown 6.5 3.4 120 310
floats-esbmc-regression/nan_true-unreach-call.i true 2 wit inspect .12  .12  1.2  8.3 0      .11   - - true 5.2  2.8  110   280 true 14   7.7 280 320
floats-esbmc-regression/nearbyint2_true-unreach-call.i true 2 wit inspect .085 .085 .45 8.2 .016  .0041 - - error 6.6  3.5  71   270 unknown 6.2 3.3 110 300
floats-esbmc-regression/nearbyint_true-unreach-call.i true 2 wit inspect .12  .20  .64 28   .016  22      - - error 6.6  3.5  140   290 unknown 6.1 3.2 110 290
floats-esbmc-regression/remainder_true-unreach-call.i true 2 wit inspect .11  .11  .47 8.1 .0082 .86   - - true 5.5  3.0  80   280 unknown 6.4 3.4 130 300
floats-esbmc-regression/rint2_true-unreach-call.i true 2 wit inspect .068 .070 .58 8.1 .016  .28   - - error 5.6  3.0  130   270 unknown 5.8 3.1 110 300
floats-esbmc-regression/rint_true-unreach-call.i true 2 wit inspect .084 .11  .98 15   .016  7.6    - - error 8.2  4.4  89   300 unknown 9.1 4.8 95 320
floats-esbmc-regression/round_nondet_true-unreach-call.i true 2 wit inspect .11  .11  1.5  8.0 0      0      - - error 5.5  2.9  110   270 unknown 11   5.8 190 300
floats-esbmc-regression/round_true-unreach-call.i true 2 wit inspect .064 .064 .52 8.2 .0082 0      - - true 5.7  3.0  88   280 unknown 6.3 3.3 120 300
floats-esbmc-regression/rounding_functions_true-unreach-call.i true 2 wit inspect .064 .066 .50 8.3 .0082 .078  - - true 7.2  3.9  81   280 unknown 6.2 3.3 120 300
floats-esbmc-regression/trunc_nondet_2_true-unreach-call.i true 2 wit inspect .11  .11  1.2  7.9 0      0      - - unknown 7.8  4.2  100   320 unknown 11   5.9 250 300
floats-esbmc-regression/trunc_nondet_true-unreach-call.i true 2 wit inspect .12  .12  1.1  8.0 0      0      - - error 5.6  3.0  120   270 unknown 11   5.9 230 310
floats-esbmc-regression/trunc_true-unreach-call.i true 2 wit inspect .097 .097 .46 8.2 .0082 0      - - true 5.9  3.2  81   270 unknown 7.7 4.1 130 350
floats-esbmc-regression/Double_div_bad_false-unreach-call.i false(unreach-call) 1 wit inspect .057 .060 .60 7.8 .0082 .63   out of memory 62   53   1700 7000 true 22   15   420 580 - -
floats-esbmc-regression/Float_div_bad_false-unreach-call.i false(unreach-call) 1 wit inspect .053 .054 .48 8.0 .0082 .41   false(unreach-call) 23   19   620 2000 true 18   10   210 320 - -
floats-esbmc-regression/digits_bad_for_false-unreach-call.i false(unreach-call) 1 wit inspect .11  .30  1.1  64   .0082 59      false(unreach-call) 5.3 2.9 110 290 true 17   9.7 190 310 - -
floats-esbmc-regression/digits_bad_while_false-unreach-call.i false(unreach-call) 1 wit inspect .045 .050 .77 7.8 .0082 .98   false(unreach-call) 6.0 3.3 140 290 true 17   9.9 150 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 172 298 16000 16000 160000 110000 .40  410 172 1200 1200 30000 38000   172 730 580 12000 19000   172 25000 25000 470000 51000   172 20000 19000 420000 270000  
    correct results 164 298 15000 15000 150000 32000 .40  410 22 1200 1200 30000 38000   22 730 580 12000 19000   78 25000 25000 470000 51000   42 20000 19000 420000 270000  
        correct true 134 268 14000 14000 140000 13000 .37  310 0 0 0 0 0   16 0 0 0 0   75 25000 25000 470000 51000   42 20000 19000 420000 270000  
        correct false 30 30 1700 1700 15000 19000 .033 96 22 1200 1200 30000 38000   6 730 580 12000 19000   3 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 (172 tasks, max score: 314) 298
Run set sv-comp17.ReachSafety-Floats