Tool SMACK+Corral 1.7.2
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-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-13 11:09:55 CET [[ 2017-01-15 01:36:45 CET ]] [[ 2017-01-15 02:12:47 CET ]] [[ 2017-01-15 01:38:53 CET ]] [[ 2017-01-15 02:35:07 CET ]]
Run set sv-comp17.ReachSafety-Floats
Options -w error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-13_1109.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 0 890     890     7200    580   1.1  2.6   .50 .32 9.8 40 5.8 3.1 76 310
floats-cdfpl/newton_1_5_false-unreach-call.i 1 490     490     4000    530   1.1  2.7   3.2  1.8  67   270 6.9 3.6 88 310
floats-cdfpl/newton_1_6_false-unreach-call.i 1 380     380     2700    540   1.1  2.7   3.3  1.9  68   270 6.5 3.5 69 310
floats-cdfpl/newton_1_7_false-unreach-call.i 1 460     460     4000    530   1.1  1.9   3.4  1.9  71   280 7.5 3.9 68 320
floats-cdfpl/newton_1_8_false-unreach-call.i 1 250     250     2200    500   1.1  2.7   3.1  1.8  32   280 6.6 3.6 81 320
floats-cdfpl/newton_2_6_false-unreach-call.i 0 890     890     7800    930   1.1  2.7   .53 .34 15   41 6.2 3.3 61 310
floats-cdfpl/newton_2_7_false-unreach-call.i 0 890     890     6900    990   1.1  2.5   .51 .34 9.7 40 6.5 3.4 78 310
floats-cdfpl/newton_2_8_false-unreach-call.i 0 890     890     7200    980   1.1  2.5   .54 .34 13   41 6.8 3.6 72 300
floats-cdfpl/newton_3_6_false-unreach-call.i 0 890     890     7400    1300   1.1  2.5   .57 .36 9.2 43 5.4 2.9 68 300
floats-cdfpl/newton_3_7_false-unreach-call.i 0 890     890     8500    1300   1.1  0     .54 .37 9.7 41 5.6 2.9 57 300
floats-cdfpl/newton_3_8_false-unreach-call.i 0 890     890     9900    1400   1.1  2.5   .49 .32 10   39 6.0 3.2 95 300
floats-cdfpl/sine_1_false-unreach-call.i 1 140     140     1100    300   1.1  2.8   3.5  1.9  47   270 6.4 3.4 47 310
floats-cdfpl/sine_2_false-unreach-call.i 1 62     62     540    280   1.1  2.6   3.3  1.8  53   270 10   5.4 58 320
floats-cdfpl/sine_3_false-unreach-call.i 1 51     51     380    280   1.1  2.7   3.3  1.8  50   280 6.4 3.4 98 320
floats-cdfpl/square_1_false-unreach-call.i 1 83     83     780    150   1.1  2.6   3.3  1.9  73   270 7.5 4.0 82 310
floats-cdfpl/square_2_false-unreach-call.i 1 130     130     1200    170   1.1  2.7   3.8  2.1  43   270 7.2 3.8 140 310
floats-cdfpl/square_3_false-unreach-call.i 1 200     200     2400    170   1.1  2.9   3.2  1.8  64   270 6.5 3.5 94 310
floats-cdfpl/newton_1_1_true-unreach-call.i 0 890     890     6700    570   1.1  0     .50 .32 9.6 41 5.4 2.9 96 290
floats-cdfpl/newton_1_2_true-unreach-call.i 0 890     890     7900    570   1.1  0     .49 .32 6.5 40 6.2 3.3 93 310
floats-cdfpl/newton_1_3_true-unreach-call.i 0 890     890     6800    580   1.1  0     .52 .33 11   40 7.8 4.0 120 310
floats-cdfpl/newton_2_1_true-unreach-call.i 0 890     890     6600    980   1.1  2.5   .53 .35 11   39 6.0 3.1 82 300
floats-cdfpl/newton_2_2_true-unreach-call.i 0 890     890     6900    970   1.1  0     .51 .33 12   42 5.8 3.1 110 300
floats-cdfpl/newton_2_3_true-unreach-call.i 0 890     890     8400    960   1.1  2.5   .59 .37 13   43 6.2 3.3 100 300
floats-cdfpl/newton_2_4_true-unreach-call.i 0 890     890     6300    960   1.1  2.5   .54 .35 14   40 6.3 3.3 92 290
floats-cdfpl/newton_2_5_true-unreach-call.i 0 890     890     7000    980   1.1  0     .53 .35 9.4 39 7.1 3.7 73 310
floats-cdfpl/newton_3_1_true-unreach-call.i 0 890     890     7000    1300   1.1  0     .49 .32 12   39 7.6 4.0 75 290
floats-cdfpl/newton_3_2_true-unreach-call.i 0 890     890     6600    1300   1.1  2.5   .47 .30 10   39 6.3 3.3 91 300
floats-cdfpl/newton_3_3_true-unreach-call.i 0 890     890     9500    1300   1.1  2.5   .64 .41 9.3 39 7.9 4.1 110 340
floats-cdfpl/newton_3_4_true-unreach-call.i 0 890     890     9800    1300   1.1  2.5   .62 .39 8.2 40 5.6 3.0 99 290
floats-cdfpl/newton_3_5_true-unreach-call.i 0 890     890     6400    1300   1.1  0     .56 .35 6.7 39 7.1 3.8 83 300
floats-cdfpl/sine_4_true-unreach-call.i 0 890     890     9200    470   1.1  0     .48 .30 6.7 39 5.7 3.0 110 300
floats-cdfpl/sine_5_true-unreach-call.i 0 890     890     7200    470   1.1  0     .50 .34 3.5 40 6.7 3.5 96 310
floats-cdfpl/sine_6_true-unreach-call.i 0 890     890     5900    480   1.1  18     .53 .33 9.9 41 6.1 3.2 93 290
floats-cdfpl/sine_7_true-unreach-call.i 0 890     890     8400    470   1.1  2.5   .52 .32 9.1 39 6.3 3.3 91 300
floats-cdfpl/sine_8_true-unreach-call.i 0 890     890     7600    380   1.1  2.5   .51 .33 4.2 39 7.2 3.8 95 310
floats-cdfpl/square_4_true-unreach-call.i 0 890     890     7300    870   1.1  2.5   .47 .32 3.6 40 7.7 4.0 73 300
floats-cdfpl/square_5_true-unreach-call.i 0 890     890     7500    870   1.1  2.5   .62 .40 7.2 39 6.7 3.5 93 320
floats-cdfpl/square_6_true-unreach-call.i 0 890     890     6300    880   1.1  2.5   .67 .42 9.8 43 6.0 3.2 88 300
floats-cdfpl/square_7_true-unreach-call.i 0 890     890     6300    870   1.1  2.5   .51 .33 8.0 40 7.5 4.0 77 300
floats-cdfpl/square_8_true-unreach-call.i 2 160     160     1300    170   1.1  0     25    23    840   340 260   250   4200 7000
floats-cbmc-regression/float-div1_true-unreach-call.i 2 6.8   6.8   67    160   1.2  2.7   6.3  3.8  120   330 91   83   2500 690
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i 0 .64  .67  7.6  45   1.6  2.7   .52 .33 12   39 7.5 4.0 84 300
floats-cbmc-regression/float-no-simp1_true-unreach-call.i 2 .88  1.0   8.9  71   1.1  18     3.6  2.0  58   250 11   6.1 230 310
floats-cbmc-regression/float-no-simp2_true-unreach-call.i 2 45     45     550    140   1.2  0     21    18    530   320 68   58   970 460
floats-cbmc-regression/float-no-simp3_true-unreach-call.i 2 .82  .91  8.0  52   1.1  0     3.5  2.0  63   260 11   6.0 200 300
floats-cbmc-regression/float-no-simp4_true-unreach-call.i 2 1.0   1.1   12    82   1.4  2.6   6.0  3.2  110   280 28   16   370 540
floats-cbmc-regression/float-no-simp6_true-unreach-call.i 2 .77  .84  12    57   1.1  0     3.8  2.1  56   260 14   7.3 270 320
floats-cbmc-regression/float-no-simp7_true-unreach-call.i 2 .81  .91  9.4  51   1.1  0     3.3  1.8  58   260 16   8.5 160 320
floats-cbmc-regression/float-no-simp8_true-unreach-call.i 2 .92  1.0   12    72   1.1  2.7   5.5  3.0  110   280 13   6.9 240 290
floats-cbmc-regression/float-rounding1_true-unreach-call.i 0 .058 .058 .39 7.2 0    0     .59 .37 8.7 41 7.3 3.8 71 300
floats-cbmc-regression/float-to-double1_true-unreach-call.i 2 3.9   3.9   44    87   1.2  2.7   5.2  2.9  120   280 200   190   4100 450
floats-cbmc-regression/float-to-double2_true-unreach-call.i 2 .80  .91  9.3  58   1.1  2.7   3.3  1.8  64   260 14   7.3 190 310
floats-cbmc-regression/float-zero-sum1_true-unreach-call.i 2 .81  .89  8.2  53   1.1  2.5   4.5  2.5  50   260 6.4 3.4 96 300
floats-cbmc-regression/float11_true-unreach-call.i 2 .80  .87  7.8  52   1.1  0     3.4  1.9  62   260 13   7.3 230 320
floats-cbmc-regression/float12_true-unreach-call.i 2 1.1   1.2   15    74   1.1  0     3.4  1.9  82   260 20   14   470 310
floats-cbmc-regression/float13_true-unreach-call.i 2 .82  .91  10    55   1.1  2.7   4.5  2.5  41   260 15   8.0 210 320
floats-cbmc-regression/float14_true-unreach-call.i 2 .87  .93  9.8  67   1.2  2.7   5.4  2.9  120   270 16   9.0 250 310
floats-cbmc-regression/float18_true-unreach-call.i 2 .80  .87  10    61   1.1  2.6   30    26    530   440 7.8 4.1 94 310
floats-cbmc-regression/float19_true-unreach-call.i 2 1.1   1.1   13    68   1.2  2.7   5.2  2.8  120   280 16   9.1 270 310
floats-cbmc-regression/float1_true-unreach-call.i 2 .80  .89  9.3  56   1.1  2.7   4.3  2.4  47   260 14   7.4 180 310
floats-cbmc-regression/float20_true-unreach-call.i 2 2.2   2.2   24    110   1.1  2.7   3.6  2.0  72   260 26   21   570 400
floats-cbmc-regression/float21_true-unreach-call.i 2 56     56     680    270   1.2  2.7   7.1  4.0  81   300 110   97   1800 630
floats-cbmc-regression/float22_true-unreach-call.i 0 73     72     520    15000   1.2  0     .48 .30 9.3 40 6.5 3.5 91 290
floats-cbmc-regression/float2_true-unreach-call.i 2 .81  .91  8.2  57   1.1  2.7   3.5  2.0  84   260 14   7.5 240 310
floats-cbmc-regression/float3_true-unreach-call.i 2 1.1   1.2   14    85   1.1  0     3.5  2.0  78   280 25   18   430 360
floats-cbmc-regression/float4_true-unreach-call.i 2 52     52     600    150   1.2  2.7   68    65    1700   340 97   90   2600 520
floats-cbmc-regression/float5_true-unreach-call.i 2 1.2   1.2   14    63   1.1  0     3.5  2.0  57   260 33   27   640 320
floats-cbmc-regression/float6_true-unreach-call.i 2 .83  .92  11    60   1.2  2.7   3.9  2.2  69   260 18   9.7 200 320
floats-cbmc-regression/float7_true-unreach-call.i 2 .80  .88  12    61   1.1  2.7   3.5  1.9  68   260 6.3 3.4 110 300
floats-cbmc-regression/float8_true-unreach-call.i 2 .82  .93  9.3  60   1.2  2.7   5.7  3.4  130   280 16   9.0 160 330
floats-cbmc-regression/float_lib1_true-unreach-call.i 2 .91  1.0   10    69   1.2  0     7.1  3.8  70   280 14   7.7 170 300
floats-cbmc-regression/float_lib2_true-unreach-call.i 2 2.4   2.5   24    250   1.2  .13  6.5  3.5  74   280 17   9.7 280 460
float-benchs/cast_float_ptr_false-unreach-call.c 0 890     890     7500    3000   1.1  2.5   .49 .34 4.1 40 6.3 3.3 67 300
float-benchs/cast_union_loose_false-unreach-call.c 1 3.9   4.0   46    120   1.1  2.7   3.6  2.0  60   270 5.6 3.0 70 300
float-benchs/cast_union_tight_false-unreach-call.c 1 4.7   4.7   50    140   1.1  2.7   3.6  2.0  71   280 5.6 3.0 61 300
float-benchs/float_int_inv_square_false-unreach-call.c 1 1.3   1.3   17    67   1.1  2.7   3.4  1.9  67   280 8.6 4.5 69 320
float-benchs/inv_square_false-unreach-call.c 1 .87  .87  11    61   1.1  2.7   3.3  1.8  56   270 7.2 3.8 89 320
float-benchs/nan_double_false-unreach-call.c 1 .80  .89  10    49   1.1  0     3.6  2.0  69   280 6.7 3.6 80 320
float-benchs/nan_float_false-unreach-call.c 1 .78  .84  11    59   1.1  .13  3.2  1.8  60   260 7.3 3.9 92 310
float-benchs/sin_interpolated_index_false-unreach-call.c 1 160     160     1300    580   1.2  2.8   3.6  2.1  69   280 18   12   160 980
float-benchs/sqrt_poly2_false-unreach-call.c 0 .15  .15  1.7  24   .29 0     .59 .38 13   45 6.5 3.4 82 320
float-benchs/Muller_Kahan_true-unreach-call.c 0 33     33     390    15000   1.5  2.5   .53 .35 7.4 41 5.5 2.9 110 300
float-benchs/Rump_double_true-unreach-call.c 2 230     230     2700    540   1.1  0     3.5  2.0  73   260 26   19   520 790
float-benchs/Rump_float_true-unreach-call.c 2 22     22     230    200   1.1  2.7   4.0  2.3  45   260 17   10   270 380
float-benchs/addsub_double_exact_true-unreach-call.c 2 .84  .91  9.6  62   1.1  2.7   4.3  2.4  44   260 17   9.1 190 320
float-benchs/addsub_float_exact_true-unreach-call.c 2 .80  .86  9.2  51   1.1  0     3.7  2.1  58   260 15   8.3 180 310
float-benchs/addsub_float_inexact_true-unreach-call.c 2 .86  .93  8.2  60   1.1  2.6   3.9  2.2  36   250 15   8.3 150 300
float-benchs/arctan_Pade_true-unreach-call.c 0 890     890     6900    1700   1.1  0     .54 .36 9.5 42 7.2 3.8 79 300
float-benchs/bary_diverge_true-unreach-call.c 0 890     890     9800    1900   1.1  2.5   .61 .40 11   41 6.6 3.5 100 310
float-benchs/cast_float_union_true-unreach-call.c 2 .84  .92  8.9  61   1.1  2.7   4.4  2.5  49   270 10   5.4 170 310
float-benchs/cos_polynomial_true-unreach-call.c 0 890     890     7500    460   1.1  0     .56 .37 10   40 6.7 3.6 88 300
float-benchs/divmul_buf_diverge_true-unreach-call.c 2 59     59     650    2600   1.1  0     900    900    17000   1700 960   820   23000 4900
float-benchs/divmul_diverge_true-unreach-call.c 2 35     35     340    2500   1.1  0     900    900    17000   2700 960   820   27000 4700
float-benchs/drift_tenth_true-unreach-call.c 2 .82  .93  9.1  55   1.1  0     13    11    200   340 180   170   4000 630
float-benchs/exp_loop_true-unreach-call.c 0 890     890     9200    2000   1.2  0     .54 .35 9.1 39 7.3 3.8 82 300
float-benchs/feedback_diverge_true-unreach-call.c 0 890     890     7400    1700   1.1  2.5   .53 .33 14   39 7.0 3.7 76 290
float-benchs/filter1_true-unreach-call.c 0 890     890     8800    2700   1.1  0     .47 .31 4.9 39 7.1 3.8 71 300
float-benchs/filter2_alt_true-unreach-call.c 0 890     890     8100    3300   1.1  20     .49 .31 11   39 5.5 3.0 96 290
float-benchs/filter2_iterated_true-unreach-call.c 0 40     40     430    15000   1.2  2.5   .49 .33 3.9 39 7.4 3.9 130 300
float-benchs/filter2_reinit_true-unreach-call.c 0 890     890     10000    7700   1.1  2.5   .56 .36 7.5 41 6.1 3.2 75 300
float-benchs/filter2_set_true-unreach-call.c 0 890     890     4000    13000   1.2  2.5   .52 .33 11   40 6.2 3.3 68 290
float-benchs/filter2_true-unreach-call.c 0 890     890     8100    6300   1.1  2.5   .54 .34 12   40 6.1 3.2 95 310
float-benchs/filter_iir_true-unreach-call.c 0 40     40     420    15000   1.2  2.5   .52 .33 7.6 42 7.1 3.7 96 300
float-benchs/float_double_true-unreach-call.c 2 .83  .91  8.9  60   1.1  2.7   3.3  1.9  74   250 16   8.8 190 320
float-benchs/image_filter_true-unreach-call.c 0 60     59     700    15000   2.0  0     .50 .32 9.1 40 6.3 3.3 100 290
float-benchs/interpolation2_true-unreach-call.c 0 890     890     3800    1700   1.2  2.5   .50 .33 6.5 42 5.5 2.9 120 300
float-benchs/interpolation_true-unreach-call.c 0 890     890     6500    2400   1.1  0     .55 .35 12   41 6.2 3.3 99 310
float-benchs/inv_sqrt_Quake_true-unreach-call.c 0 .056 .057 .47 7.3 0    0     .50 .33 11   39 6.3 3.3 94 310
float-benchs/inv_square_int_true-unreach-call.c 2 1.5   1.6   17    82   1.1  19     3.7  2.1  60   270 70   63   1400 340
float-benchs/inv_square_true-unreach-call.c 2 .95  .99  11    67   1.1  2.7   4.5  2.5  53   270 72   65   1600 330
float-benchs/loop_true-unreach-call.c 0 890     890     9700    1100   1.1  2.9   .57 .37 10   39 7.0 3.7 82 290
float-benchs/mea8000_true-unreach-call.c 0 .46  .46  5.4  58   .61 0     .48 .32 5.9 40 6.8 3.6 100 300
float-benchs/nan_double_range_true-unreach-call.c 2 .79  .90  9.3  56   1.1  2.7   4.7  2.6  48   260 15   8.0 160 330
float-benchs/nan_float_range_true-unreach-call.c 2 .84  .92  8.7  60   1.1  0     3.9  2.2  55   260 16   9.4 230 310
float-benchs/rlim_exit_true-unreach-call.c 0 890     890     9400    290   1.3  2.5   .62 .39 7.8 39 7.1 3.8 80 290
float-benchs/rlim_invariant_true-unreach-call.c 2 540     540     4700    1000   1.1  .13  6.1  3.8  100   320 500   490   10000 640
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call.c 0 890     890     10000    1200   1.2  2.5   .57 .36 10   40 7.3 3.8 110 320
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call.c 0 890     890     7700    1200   1.2  2.5   .53 .34 13   40 5.8 3.1 99 290
float-benchs/sin_interpolated_index_true-unreach-call.c 0 890     890     7200    720   1.2  19     .48 .32 11   39 5.4 2.9 93 310
float-benchs/sin_interpolated_negation_true-unreach-call.c 0 41     40     480    15000   1.3  2.5   .54 .34 12   40 7.6 4.1 88 300
float-benchs/sin_interpolated_smallrange_true-unreach-call.c 0 38     37     400    15000   1.3  1.8   .66 .42 8.3 44 7.0 3.7 86 300
float-benchs/sqrt_Householder_constant_true-unreach-call.c 0 40     39     410    15000   1.1  0     .54 .35 11   41 5.4 2.9 98 280
float-benchs/sqrt_Householder_interval_true-unreach-call.c 0 41     41     320    15000   1.2  2.5   .51 .32 9.9 39 5.8 3.1 98 310
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c 0 41     41     350    15000   1.2  2.7   .55 .34 7.0 40 6.5 3.4 100 300
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c 0 39     39     460    15000   1.2  0     .57 .36 9.1 39 7.0 3.7 77 290
float-benchs/sqrt_biNewton_pseudoconstant_true-unreach-call.c 0 40     40     360    15000   1.2  0     .50 .34 6.7 39 6.8 3.6 68 290
float-benchs/sqrt_poly_true-unreach-call.c 2 750     750     5900    520   1.1  2.7   90    88    2300   460 550   550   13000 1400
float-benchs/water_pid_true-unreach-call.c 0 890     890     8800    9000   1.1  2.5   .53 .33 7.2 43 7.0 3.7 85 310
float-benchs/zonotope_2_true-unreach-call.c 2 260     260     3000    470   1.3  2.7   900    900    16000   1100 960   950   24000 1200
float-benchs/zonotope_3_true-unreach-call.c 2 22     22     220    310   1.2  2.6   6.0  3.9  130   350 960   830   18000 4700
float-benchs/zonotope_loose_true-unreach-call.c 2 8.9   8.9   73    210   1.1  2.7   4.5  2.8  100   330 780   770   15000 1500
float-benchs/zonotope_tight_true-unreach-call.c 2 12     12     110    220   1.1  0     4.1  2.6  67   290 780   770   12000 1400
floats-esbmc-regression/Double_div_true-unreach-call.i 0 890     890     8600    12000   1.1  2.5   .54 .34 13   39 5.6 3.0 110 300
floats-esbmc-regression/Float_div_true-unreach-call.i 2 680     680     7100    2000   1.1  0     4.1  2.4  84   290 280   270   9200 660
floats-esbmc-regression/ceil_nondet_true-unreach-call.i 0 .072 .073 .39 7.3 0    0     .49 .31 8.6 40 5.7 3.0 94 290
floats-esbmc-regression/ceil_true-unreach-call.i 0 .61  .63  8.0  44   1.2  2.7   .57 .38 8.0 40 8.4 4.3 72 300
floats-esbmc-regression/copysign_true-unreach-call.i 2 .89  .99  10    63   1.2  .13  5.9  3.2  87   280 7.4 4.0 97 310
floats-esbmc-regression/digits_for_true-unreach-call.i 2 .85  .96  11    60   1.2  2.6   900    900    15000   1000 960   950   16000 1400
floats-esbmc-regression/digits_while_true-unreach-call.i 2 .81  .89  9.1  55   1.1  2.7   900    900    16000   970 960   950   14000 3100
floats-esbmc-regression/fabs_true-unreach-call.i 2 .83  .93  11    60   1.1  2.7   5.5  2.9  110   270 12   6.7 240 300
floats-esbmc-regression/fdim_true-unreach-call.i 2 .80  .89  11    64   1.1  2.6   6.7  3.6  58   270 5.9 3.2 90 290
floats-esbmc-regression/floor_nondet_true-unreach-call.i 0 .058 .058 .30 7.1 0    0     .48 .32 8.4 39 6.0 3.2 100 290
floats-esbmc-regression/floor_true-unreach-call.i 0 .61  .62  6.2  45   1.2  2.7   .60 .39 9.1 40 6.0 3.2 66 300
floats-esbmc-regression/fmax_true-unreach-call.i 2 .82  .91  8.6  60   1.1  2.7   6.9  3.7  71   280 6.7 3.5 110 310
floats-esbmc-regression/fmin_true-unreach-call.i 2 .83  .93  11    54   1.1  2.7   6.4  3.5  77   280 7.9 4.1 86 330
floats-esbmc-regression/fmod2_true-unreach-call.i 0 36     36     450    15000   1.2  2.5   .52 .34 7.5 41 7.4 4.0 62 300
floats-esbmc-regression/fmod3_true-unreach-call.i 0 37     36     470    15000   1.2  2.5   .55 .34 13   41 6.1 3.2 120 300
floats-esbmc-regression/fmod_true-unreach-call.i 0 .62  .64  8.2  41   1.2  .13  .48 .30 9.9 40 7.8 4.1 79 300
floats-esbmc-regression/isgreater_true-unreach-call.i 2 .83  .93  9.1  60   1.1  2.7   6.5  3.5  67   280 14   7.4 140 320
floats-esbmc-regression/isgreaterequal_true-unreach-call.i 2 .80  .90  8.3  57   1.1  0     7.0  3.8  72   270 12   6.6 170 300
floats-esbmc-regression/isless_true-unreach-call.i 2 .84  .93  9.2  56   1.1  2.7   6.2  3.3  85   270 12   6.2 190 310
floats-esbmc-regression/islessequal_true-unreach-call.i 2 .83  .93  9.5  55   1.1  2.7   6.1  3.3  93   280 12   6.3 210 320
floats-esbmc-regression/islessgreater_true-unreach-call.i 2 .83  .93  9.6  58   1.1  2.7   5.2  2.8  96   270 13   6.7 160 300
floats-esbmc-regression/isunordered_true-unreach-call.i 2 .80  .91  10    59   1.1  2.7   5.1  2.8  97   270 13   6.9 140 300
floats-esbmc-regression/lrint_true-unreach-call.i 0 .063 .064 .39 7.5 0    0     .54 .33 13   40 5.7 3.0 120 290
floats-esbmc-regression/modf_true-unreach-call.i 2 9.9   9.9   100    170   1.2  2.7   5.4  2.9  110   280 8.0 4.2 100 310
floats-esbmc-regression/nan_true-unreach-call.i 2 .85  .92  9.6  62   1.1  2.7   5.3  2.9  110   280 16   8.5 210 300
floats-esbmc-regression/nearbyint2_true-unreach-call.i 0 .078 .078 .40 7.3 0    0     .53 .34 10   41 5.6 3.0 100 290
floats-esbmc-regression/nearbyint_true-unreach-call.i 0 .076 .076 .52 7.5 0    0     .66 .41 7.7 40 8.1 4.3 75 300
floats-esbmc-regression/remainder_true-unreach-call.i 0 .077 .077 .43 7.3 0    0     .56 .36 14   42 7.1 3.8 80 300
floats-esbmc-regression/rint2_true-unreach-call.i 0 .063 .063 .44 7.5 0    0     .51 .31 9.2 40 7.3 3.9 93 300
floats-esbmc-regression/rint_true-unreach-call.i 0 .063 .063 .53 7.5 0    0     .56 .37 9.2 42 7.3 3.9 88 300
floats-esbmc-regression/round_nondet_true-unreach-call.i 0 .062 .062 .33 7.2 0    0     .54 .34 13   42 7.4 3.9 79 300
floats-esbmc-regression/round_true-unreach-call.i 0 .61  .62  8.8  38   1.2  .070 .62 .40 11   41 6.3 3.4 110 300
floats-esbmc-regression/rounding_functions_true-unreach-call.i 2 1.2   1.2   14    150   1.3  2.7   7.3  3.9  82   270 6.9 3.6 130 300
floats-esbmc-regression/trunc_nondet_2_true-unreach-call.i 0 .066 .066 .34 7.5 0    0     .48 .31 6.3 40 6.7 3.5 110 300
floats-esbmc-regression/trunc_nondet_true-unreach-call.i 0 .071 .071 .37 7.2 0    0     .62 .40 8.6 40 7.8 4.2 78 300
floats-esbmc-regression/trunc_true-unreach-call.i 0 .59  .60  6.4  43   1.2  2.6   .58 .36 8.0 40 7.5 3.9 80 300
floats-esbmc-regression/Double_div_bad_false-unreach-call.i 0 890     890     11000    12000   1.1  2.5   .50 .32 8.7 39 7.3 3.8 79 300
floats-esbmc-regression/Float_div_bad_false-unreach-call.i 0 890     890     8900    2200   1.1  0     .49 .31 7.1 42 5.4 2.9 46 290
floats-esbmc-regression/digits_bad_for_false-unreach-call.i 1 .91  1.0   9.7  70   1.2  18     3.8  2.2  65   280 15   8.6 130 300
floats-esbmc-regression/digits_bad_while_false-unreach-call.i 1 .85  .94  10    62   1.1  2.7   3.8  2.1  49   280 11   6.3 76 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 153 51000 51000 450000 340000 180 380 172 71 41 1200 5600   172 220 120 2400 10000   172 5100 4900 93000 28000   172 11000 9900 220000 75000  
    correct results 86 153 5400 5400 50000 20000 97 210 18 65 37 1100 5200   17 160 87 1700 6600   62 5000 4900 92000 25000   42 10000 9600 210000 52000  
        correct true 67 134 3000 3000 29000 15000 76 150 18 0 0 0 0   17 0 0 0 0   62 5000 4900 92000 25000   42 10000 9600 210000 52000  
        correct false 19 19 2400 2400 21000 4600 21 61 0 65 37 1100 5200   0 160 87 1700 6600   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 (172 tasks, max score: 314) 153
Run set sv-comp17.ReachSafety-Floats