Tool ESBMC ESBMC version 3.1 64-bit x86_64 linux
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-12 12:02:41 CET [[ 2017-01-14 22:52:01 CET ]] [[ 2017-01-15 00:27:39 CET ]] [[ 2017-01-14 23:20:04 CET ]] [[ 2017-01-15 00:48:54 CET ]]
Run set sv-comp17.ReachSafety-Floats
Options -s kinduction [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-12_1202.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 900     900     7000    470 .84 0   .47 .31 7.4 39 5.5 2.9 120 290
floats-cdfpl/newton_1_5_false-unreach-call.i 0 900     900     7300    480 .84 0   .50 .32 9.6 39 6.0 3.2 130 300
floats-cdfpl/newton_1_6_false-unreach-call.i 0 900     900     6600    440 .84 0   .50 .32 10   40 6.2 3.2 120 300
floats-cdfpl/newton_1_7_false-unreach-call.i 0 900     900     6500    460 .84 0   .49 .31 8.1 40 6.3 3.3 110 300
floats-cdfpl/newton_1_8_false-unreach-call.i 0 900     900     7100    450 .84 0   .48 .31 8.9 39 5.9 3.2 120 300
floats-cdfpl/newton_2_6_false-unreach-call.i 0 900     900     5800    760 .84 0   .55 .35 9.4 41 5.6 3.0 110 290
floats-cdfpl/newton_2_7_false-unreach-call.i 0 900     900     6800    750 .84 0   .50 .32 8.5 40 6.0 3.2 120 300
floats-cdfpl/newton_2_8_false-unreach-call.i 0 900     900     7600    760 .84 0   .50 .32 4.5 40 5.7 3.1 110 300
floats-cdfpl/newton_3_6_false-unreach-call.i 0 900     900     7000    1100 .84 0   .53 .33 12   40 6.7 3.5 130 300
floats-cdfpl/newton_3_7_false-unreach-call.i 0 900     900     7700    1100 .84 0   .53 .35 6.2 41 5.8 3.1 120 300
floats-cdfpl/newton_3_8_false-unreach-call.i 0 900     900     7000    1100 .84 0   .53 .33 11   40 6.3 3.4 120 300
floats-cdfpl/sine_1_false-unreach-call.i 1 180     180     1900    240 .84 0   5.3  3.0  39   270 26   20   260 890
floats-cdfpl/sine_2_false-unreach-call.i 1 90     90     920    190 .84 0   3.3  1.8  54   270 97   91   930 3800
floats-cdfpl/sine_3_false-unreach-call.i 1 59     60     530    180 .84 0   3.3  1.8  40   280 89   83   810 3500
floats-cdfpl/square_1_false-unreach-call.i 1 570     570     4100    200 .84 0   3.5  1.9  35   270 40   34   390 970
floats-cdfpl/square_2_false-unreach-call.i 0 900     900     10000    350 .99 0   .50 .32 11   39 6.3 3.3 130 310
floats-cdfpl/square_3_false-unreach-call.i 0 900     900     7200    350 .84 0   .55 .35 11   42 5.9 3.2 85 310
floats-cdfpl/newton_1_1_true-unreach-call.i 0 900     900     7600    450 .84 0   .54 .35 7.4 44 6.0 3.1 130 300
floats-cdfpl/newton_1_2_true-unreach-call.i 0 900     900     3800    420 .99 0   .48 .31 8.9 40 6.1 3.2 120 300
floats-cdfpl/newton_1_3_true-unreach-call.i 0 900     900     8300    460 .84 0   .59 .38 8.1 40 5.9 3.1 97 300
floats-cdfpl/newton_2_1_true-unreach-call.i 0 900     900     9800    760 .84 0   .66 .40 6.1 43 5.9 3.2 120 300
floats-cdfpl/newton_2_2_true-unreach-call.i 0 900     900     7400    770 .84 0   .49 .31 6.6 39 5.3 2.8 110 280
floats-cdfpl/newton_2_3_true-unreach-call.i 0 900     900     8100    760 .84 0   .52 .35 11   39 6.6 3.4 130 300
floats-cdfpl/newton_2_4_true-unreach-call.i 0 900     900     10000    740 .84 0   .66 .42 6.5 42 6.3 3.3 110 290
floats-cdfpl/newton_2_5_true-unreach-call.i 0 900     900     6800    760 .84 0   .58 .38 5.1 40 6.8 3.6 130 310
floats-cdfpl/newton_3_1_true-unreach-call.i 0 900     900     7500    1100 .84 0   .46 .30 6.8 40 6.1 3.2 120 300
floats-cdfpl/newton_3_2_true-unreach-call.i 0 900     900     2500    990 .99 0   .54 .35 11   44 5.4 3.0 100 280
floats-cdfpl/newton_3_3_true-unreach-call.i 0 900     900     7700    1000 .84 0   .52 .33 11   40 5.7 3.0 120 290
floats-cdfpl/newton_3_4_true-unreach-call.i 0 900     900     7300    950 .84 0   .48 .31 10   39 5.8 3.1 110 290
floats-cdfpl/newton_3_5_true-unreach-call.i 0 900     900     7100    1100 .84 0   .63 .40 4.4 40 6.0 3.2 120 300
floats-cdfpl/sine_4_true-unreach-call.i 0 900     900     2100    220 .99 0   .49 .32 11   40 6.1 3.2 130 300
floats-cdfpl/sine_5_true-unreach-call.i 0 900     900     7800    300 .84 0   .54 .36 11   41 6.5 3.4 130 320
floats-cdfpl/sine_6_true-unreach-call.i 0 900     900     9100    310 .84 0   .49 .35 13   40 5.9 3.1 120 300
floats-cdfpl/sine_7_true-unreach-call.i 0 900     900     7300    300 .84 0   .50 .31 9.8 41 6.1 3.2 110 300
floats-cdfpl/sine_8_true-unreach-call.i 0 900     900     6900    300 .84 0   .52 .35 10   40 5.5 3.0 92 300
floats-cdfpl/square_4_true-unreach-call.i 0 900     900     7600    350 .84 0   .50 .33 11   40 5.4 2.9 110 290
floats-cdfpl/square_5_true-unreach-call.i 0 900     900     6400    350 .84 0   .50 .33 11   40 5.2 2.8 110 280
floats-cdfpl/square_6_true-unreach-call.i 0 900     900     7600    350 .84 0   .51 .33 8.3 41 6.7 3.6 84 300
floats-cdfpl/square_7_true-unreach-call.i 0 900     900     6300    250 .84 0   .56 .37 7.2 40 5.8 3.1 110 300
floats-cdfpl/square_8_true-unreach-call.i 0 900     900     7100    200 .84 0   .55 .35 12   42 6.4 3.4 100 300
floats-cbmc-regression/float-div1_true-unreach-call.i 2 14     14     180    130 .84 0   5.6  3.4  110   340 83   76   750 690
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i 2 .20  .20  2.0  28 .84 0   9.9  6.9  170   670 33   22   410 710
floats-cbmc-regression/float-no-simp1_true-unreach-call.i 2 .078 .078 .79 23 .84 0   3.4  1.9  53   260 11   6.0 170 310
floats-cbmc-regression/float-no-simp2_true-unreach-call.i 2 140     140     1600    93 .84 0   15    12    190   320 58   52   1300 460
floats-cbmc-regression/float-no-simp3_true-unreach-call.i 2 .10  .10  .70 23 .84 0   3.5  2.0  34   260 11   5.8 180 300
floats-cbmc-regression/float-no-simp4_true-unreach-call.i 2 .15  .15  1.6  27 .84 0   5.7  3.1  78   270 24   14   400 500
floats-cbmc-regression/float-no-simp6_true-unreach-call.i 2 .075 .075 .75 23 .84 0   3.4  1.9  38   260 13   7.2 200 310
floats-cbmc-regression/float-no-simp7_true-unreach-call.i 2 .073 .074 .74 23 .84 0   4.0  2.2  35   250 12   6.5 180 320
floats-cbmc-regression/float-no-simp8_true-unreach-call.i 2 .13  .13  1.4  26 .84 0   5.1  2.8  68   270 12   6.7 170 290
floats-cbmc-regression/float-rounding1_true-unreach-call.i 2 .28  .28  3.5  29 .84 0   4.9  2.7  62   270 6.3 3.4 120 300
floats-cbmc-regression/float-to-double1_true-unreach-call.i 2 11     11     140    55 .84 0   5.3  2.9  110   280 170   160   2600 470
floats-cbmc-regression/float-to-double2_true-unreach-call.i 2 .077 .076 .89 23 .84 0   3.4  1.9  48   250 12   6.5 200 310
floats-cbmc-regression/float-zero-sum1_true-unreach-call.i 2 .077 .076 .89 23 .84 0   3.8  2.1  66   260 6.6 3.5 130 300
floats-cbmc-regression/float11_true-unreach-call.i 2 .088 .089 1.1  24 .84 0   3.4  1.9  57   250 12   6.7 180 320
floats-cbmc-regression/float12_true-unreach-call.i 2 1.9   1.9   26    36 .84 0   3.4  1.9  57   260 19   13   340 320
floats-cbmc-regression/float13_true-unreach-call.i 2 .087 .086 .78 23 .84 0   4.1  2.3  67   260 13   6.9 170 320
floats-cbmc-regression/float14_true-unreach-call.i 2 .13  .13  1.2  26 .84 0   4.7  2.6  44   270 13   7.5 210 300
floats-cbmc-regression/float18_true-unreach-call.i 0 .16  .15  1.2  26 .98 0   .49 .32 7.9 39 6.2 3.3 120 300
floats-cbmc-regression/float19_true-unreach-call.i 2 3.5   3.5   6.9  30 .84 0   5.3  2.9  71   280 14   8.1 230 310
floats-cbmc-regression/float1_true-unreach-call.i 2 .092 .092 .75 23 .84 0   3.3  1.8  57   260 11   5.9 190 290
floats-cbmc-regression/float20_true-unreach-call.i 2 9.9   9.9   110    91 .84 0   3.6  2.0  64   260 26   20   360 420
floats-cbmc-regression/float21_true-unreach-call.i 2 12     12     140    64 .84 0   6.4  3.6  92   310 69   62   800 610
floats-cbmc-regression/float22_true-unreach-call.i 0 .072 .072 .84 24 .84 0   .50 .33 6.0 41 5.8 3.1 110 300
floats-cbmc-regression/float2_true-unreach-call.i 2 .082 .084 .82 23 .84 0   3.2  1.8  50   260 13   6.9 200 310
floats-cbmc-regression/float3_true-unreach-call.i 2 2.1   2.1   26    47 .84 0   3.4  2.0  45   280 19   13   240 320
floats-cbmc-regression/float4_true-unreach-call.i 2 130     130     1500    94 .84 0   48    46    580   340 96   89   2200 540
floats-cbmc-regression/float5_true-unreach-call.i 2 6.4   6.4   78    45 .84 0   4.3  2.4  39   270 32   26   550 310
floats-cbmc-regression/float6_true-unreach-call.i 2 .13  .13  1.0  24 .84 0   3.8  2.1  57   260 13   7.3 220 320
floats-cbmc-regression/float7_true-unreach-call.i 2 .10  .099 .75 23 .84 0   3.4  1.9  61   260 6.2 3.3 100 300
floats-cbmc-regression/float8_true-unreach-call.i 2 .13  .13  1.4  26 .84 0   5.7  3.4  89   290 13   7.3 220 310
floats-cbmc-regression/float_lib1_true-unreach-call.i 2 .14  .14  1.9  26 .84 0   5.3  2.9  78   270 12   6.4 200 300
floats-cbmc-regression/float_lib2_true-unreach-call.i 2 .14  .14  1.5  26 .99 0   6.9  3.7  74   280 16   9.2 200 450
float-benchs/cast_float_ptr_false-unreach-call.c 1 .11  .11  1.0  23 .84 0   2.5  1.4  46   170 6.1 3.3 110 300
float-benchs/cast_union_loose_false-unreach-call.c 1 .18  .18  2.1  27 .99 0   3.8  2.1  59   270 7.3 3.8 140 330
float-benchs/cast_union_tight_false-unreach-call.c 1 .90  .90  10    37 .84 0   2.4  1.3  29   170 6.6 3.5 130 310
float-benchs/float_int_inv_square_false-unreach-call.c 1 .43  .43  5.1  33 .99 0   3.7  2.1  58   280 12   7.0 180 310
float-benchs/inv_square_false-unreach-call.c 1 .15  .15  2.1  23 .84 0   3.8  2.2  75   290 12   6.4 170 310
float-benchs/nan_double_false-unreach-call.c 1 .099 .099 .76 23 .84 0   3.9  2.2  46   270 7.2 3.8 150 320
float-benchs/nan_float_false-unreach-call.c 1 .079 .078 .74 23 .84 0   3.2  1.8  51   270 7.0 3.7 120 310
float-benchs/sin_interpolated_index_false-unreach-call.c 1 250     250     2300    880 .84 0   3.7  2.0  50   270 97   91   1100 3500
float-benchs/sqrt_poly2_false-unreach-call.c 1 300     300     2800    340 .84 0   2.5  1.4  53   160 11   5.7 190 310
float-benchs/Muller_Kahan_true-unreach-call.c 0 900     900     3100    870 .84 0   .50 .32 10   39 6.0 3.2 120 300
float-benchs/Rump_double_true-unreach-call.c 2 .11  .11  .77 23 .84 0   3.3  1.9  42   260 22   16   250 780
float-benchs/Rump_float_true-unreach-call.c 2 .075 .075 .79 23 .84 0   3.8  2.1  64   260 15   8.8 190 370
float-benchs/addsub_double_exact_true-unreach-call.c 2 .081 .081 .72 23 .84 0   3.4  1.9  57   250 13   7.0 240 320
float-benchs/addsub_float_exact_true-unreach-call.c 2 .085 .084 .84 23 .84 0   3.5  1.9  60   250 12   6.8 230 310
float-benchs/addsub_float_inexact_true-unreach-call.c 2 .10  .10  .74 23 .84 0   3.8  2.1  67   260 13   7.0 200 340
float-benchs/arctan_Pade_true-unreach-call.c 0 900     900     8500    1100 .84 0   .50 .33 9.1 40 6.1 3.2 110 310
float-benchs/bary_diverge_true-unreach-call.c 0 900     900     8600    4300 .99 0   .51 .32 12   39 6.9 3.6 140 310
float-benchs/cast_float_union_true-unreach-call.c 2 .079 .079 .97 23 .84 0   3.6  2.0  60   260 10   5.5 150 310
float-benchs/cos_polynomial_true-unreach-call.c 0 900     900     7400    610 .84 0   .50 .32 8.1 40 5.8 3.1 120 300
float-benchs/divmul_buf_diverge_true-unreach-call.c 0 900     900     11000    520 .84 0   .50 .31 9.9 39 5.8 3.1 130 300
float-benchs/divmul_diverge_true-unreach-call.c 0 900     900     8200    430 .84 0   .52 .33 11   43 5.7 3.0 77 300
float-benchs/drift_tenth_true-unreach-call.c 2 180     180     1500    210 .84 0   11    9.0  260   350 170   160   2500 630
float-benchs/exp_loop_true-unreach-call.c 0 900     900     8000    790 .84 0   .47 .29 6.5 39 6.0 3.2 120 300
float-benchs/feedback_diverge_true-unreach-call.c 0 900     900     7600    460 .84 0   .53 .33 10   41 5.8 3.1 120 300
float-benchs/filter1_true-unreach-call.c 0 900     900     8000    270 .84 0   .66 .42 7.0 39 5.9 3.2 110 300
float-benchs/filter2_alt_true-unreach-call.c 0 900     900     10000    280 .84 0   .50 .33 4.4 41 6.5 3.4 110 320
float-benchs/filter2_iterated_true-unreach-call.c 0 870     870     10000    15000 .84 0   .53 .35 8.4 41 5.8 3.1 120 290
float-benchs/filter2_reinit_true-unreach-call.c 0 900     900     4600    220 .84 0   .52 .32 9.4 41 7.3 3.8 140 310
float-benchs/filter2_set_true-unreach-call.c 0 900     900     8700    560 .99 0   .49 .33 7.5 40 6.1 3.3 120 300
float-benchs/filter2_true-unreach-call.c 0 900     900     8600    400 .84 0   .52 .35 3.8 42 5.3 2.9 86 290
float-benchs/filter_iir_true-unreach-call.c 0 900     900     7800    440 .84 0   .53 .35 8.2 39 7.1 3.7 85 290
float-benchs/float_double_true-unreach-call.c 2 .072 .072 .77 23 .84 0   4.1  2.3  35   260 13   6.8 220 320
float-benchs/image_filter_true-unreach-call.c 0 900     900     8000    2200 .84 0   .62 .39 8.0 40 6.8 3.6 140 310
float-benchs/interpolation2_true-unreach-call.c 2 610     610     7200    320 .84 0   46    44    650   550 960   950   14000 610
float-benchs/interpolation_true-unreach-call.c 2 150     150     1400    220 .84 0   49    46    720   480 170   160   3500 7000
float-benchs/inv_sqrt_Quake_true-unreach-call.c 2 130     130     1300    100 .84 0   5.0  3.1  78   320 6.4 3.3 98 300
float-benchs/inv_square_int_true-unreach-call.c 2 3.2   3.2   42    40 .84 0   3.5  2.0  60   270 41   34   760 340
float-benchs/inv_square_true-unreach-call.c 2 .72  .72  11    25 .84 0   3.6  2.0  61   270 79   73   910 360
float-benchs/loop_true-unreach-call.c 0 900     900     9700    660 .84 0   .52 .34 4.1 40 5.9 3.1 110 300
float-benchs/mea8000_true-unreach-call.c 0 900     900     8800    2100 .84 0   .51 .33 12   41 6.1 3.2 110 310
float-benchs/nan_double_range_true-unreach-call.c 2 .085 .085 .82 23 .84 0   3.4  1.9  61   260 13   6.8 230 300
float-benchs/nan_float_range_true-unreach-call.c 2 .096 .096 2.5  23 .84 0   3.5  2.0  72   260 14   8.0 210 310
float-benchs/rlim_exit_true-unreach-call.c 0 900     900     9300    340 .84 0   .56 .36 8.6 39 5.9 3.1 120 300
float-benchs/rlim_invariant_true-unreach-call.c 0 900     900     13000    250 .84 0   .48 .32 11   40 6.0 3.2 110 300
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call.c 0 900     900     5500    2200 .84 0   .51 .32 11   40 6.4 3.4 130 300
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call.c 0 900     900     8100    2500 .84 0   .56 .35 9.9 43 5.9 3.1 110 300
float-benchs/sin_interpolated_index_true-unreach-call.c 0 900     900     11000    940 .84 0   .50 .32 12   40 6.0 3.2 100 300
float-benchs/sin_interpolated_negation_true-unreach-call.c 0 900     900     6500    2100 .84 0   .55 .35 11   40 5.8 3.1 100 300
float-benchs/sin_interpolated_smallrange_true-unreach-call.c 0 900     900     6000    2200 .84 0   .50 .33 12   39 6.6 3.4 100 310
float-benchs/sqrt_Householder_constant_true-unreach-call.c 0 900     900     7500    1000 .99 0   .50 .32 8.4 40 5.4 2.9 91 290
float-benchs/sqrt_Householder_interval_true-unreach-call.c 0 900     900     7700    810 .84 0   .49 .32 7.2 39 7.5 3.9 110 300
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c 0 900     900     7700    1300 .84 0   .50 .32 5.1 40 5.6 3.0 98 290
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c 0 900     900     7800    1100 .99 0   .54 .34 8.4 40 5.6 3.0 120 290
float-benchs/sqrt_biNewton_pseudoconstant_true-unreach-call.c 0 900     900     9400    1500 .84 0   .51 .33 10   40 5.9 3.2 120 290
float-benchs/sqrt_poly_true-unreach-call.c 0 900     900     6500    490 .84 0   .52 .33 11   40 5.4 2.9 110 290
float-benchs/water_pid_true-unreach-call.c 0 900     900     7800    850 .84 0   .52 .34 6.8 40 5.4 2.9 76 290
float-benchs/zonotope_2_true-unreach-call.c 0 900     900     8700    1200 .84 0   .51 .34 12   43 6.0 3.2 100 300
float-benchs/zonotope_3_true-unreach-call.c 2 23     23     250    110 .84 0   6.1  3.9  97   350 960   840   13000 4900
float-benchs/zonotope_loose_true-unreach-call.c 2 40     40     530    150 .84 0   4.7  3.0  120   330 720   710   8500 1400
float-benchs/zonotope_tight_true-unreach-call.c 2 52     52     480    150 .99 0   4.3  2.8  69   320 550   540   5100 1100
floats-esbmc-regression/Double_div_true-unreach-call.i 0 900     900     9300    510 .84 0   .51 .33 9.6 39 6.0 3.2 130 300
floats-esbmc-regression/Float_div_true-unreach-call.i 0 900     900     8100    1200 .84 0   .51 .34 7.8 39 5.8 3.1 120 290
floats-esbmc-regression/ceil_nondet_true-unreach-call.i 2 4.0   4.0   58    70 .84 0   5.3  2.9  89   270 11   6.0 190 310
floats-esbmc-regression/ceil_true-unreach-call.i 2 .15  .15  1.7  26 .84 0   5.7  3.0  110   280 6.3 3.3 110 300
floats-esbmc-regression/copysign_true-unreach-call.i 2 .16  .16  1.4  26 .99 0   5.5  2.9  98   270 6.7 3.6 130 310
floats-esbmc-regression/digits_for_true-unreach-call.i 0 900     900     9400    2200 .84 0   .52 .32 4.4 41 5.5 3.0 100 290
floats-esbmc-regression/digits_while_true-unreach-call.i 0 900     900     7400    2200 .84 0   .50 .33 9.2 39 5.8 3.1 110 300
floats-esbmc-regression/fabs_true-unreach-call.i 2 .15  .15  1.4  26 .84 0   5.2  2.8  93   270 12   6.6 180 290
floats-esbmc-regression/fdim_true-unreach-call.i 2 .12  .12  1.2  26 .84 0   5.6  3.1  74   270 6.7 3.5 130 310
floats-esbmc-regression/floor_nondet_true-unreach-call.i 2 2.9   2.9   37    68 .84 0   5.9  3.2  78   270 12   6.1 150 320
floats-esbmc-regression/floor_true-unreach-call.i 2 .16  .16  1.3  26 .84 0   5.2  2.8  97   270 6.7 3.6 110 320
floats-esbmc-regression/fmax_true-unreach-call.i 2 .12  .12  1.4  26 .84 0   5.1  2.7  82   270 5.9 3.2 120 290
floats-esbmc-regression/fmin_true-unreach-call.i 2 .12  .12  1.3  26 .84 0   5.3  2.8  82   270 6.5 3.5 120 310
floats-esbmc-regression/fmod2_true-unreach-call.i 2 .25  .25  2.7  890 .84 0   7.9  4.2  120   310 11   5.7 150 310
floats-esbmc-regression/fmod3_true-unreach-call.i 2 .84  .84  2.6  880 .84 0   7.7  4.1  130   300 11   6.1 180 320
floats-esbmc-regression/fmod_true-unreach-call.i 2 .15  .15  1.5  26 .84 0   5.5  3.0  110   270 7.0 3.7 97 320
floats-esbmc-regression/isgreater_true-unreach-call.i 2 .12  .12  1.4  26 .84 0   5.7  3.1  100   270 11   5.7 180 310
floats-esbmc-regression/isgreaterequal_true-unreach-call.i 2 .12  .12  1.4  26 .92 0   5.4  2.9  110   270 11   5.8 160 310
floats-esbmc-regression/isless_true-unreach-call.i 2 .12  .12  1.2  26 .84 0   5.3  2.9  96   270 11   5.8 180 300
floats-esbmc-regression/islessequal_true-unreach-call.i 2 .15  .15  1.1  26 .84 0   5.2  2.8  82   270 10   5.5 140 300
floats-esbmc-regression/islessgreater_true-unreach-call.i 2 .14  .14  1.2  26 .84 0   5.4  3.0  72   270 11   5.7 170 310
floats-esbmc-regression/isunordered_true-unreach-call.i 2 .13  .13  1.4  26 .84 0   5.2  2.8  86   270 11   5.7 170 300
floats-esbmc-regression/lrint_true-unreach-call.i 2 .26  .26  2.9  880 .84 0   5.6  3.0  78   270 6.7 3.5 140 310
floats-esbmc-regression/modf_true-unreach-call.i 2 .15  .15  1.4  26 .84 0   5.2  2.8  86   280 6.6 3.5 130 300
floats-esbmc-regression/nan_true-unreach-call.i 2 .12  .12  1.2  26 .84 0   5.4  2.9  72   280 13   7.1 190 310
floats-esbmc-regression/nearbyint2_true-unreach-call.i 2 .16  .16  1.8  26 .84 0   5.7  3.1  110   270 6.5 3.5 110 320
floats-esbmc-regression/nearbyint_true-unreach-call.i 2 .60  .60  7.4  37 .84 0   8.4  4.4  66   300 6.5 3.5 130 300
floats-esbmc-regression/remainder_true-unreach-call.i 2 .26  .26  2.6  880 .84 0   5.4  3.0  87   280 6.9 3.6 130 310
floats-esbmc-regression/rint2_true-unreach-call.i 2 .17  .17  1.7  26 .84 0   5.9  3.2  76   270 6.2 3.3 130 300
floats-esbmc-regression/rint_true-unreach-call.i 2 .47  .47  6.1  36 .84 0   6.7  3.6  110   290 6.9 3.6 110 310
floats-esbmc-regression/round_nondet_true-unreach-call.i 2 12     12     120    120 .84 0   5.2  2.8  88   270 11   6.0 170 320
floats-esbmc-regression/round_true-unreach-call.i 2 .27  .27  3.2  890 .84 0   6.9  3.7  77   270 6.3 3.4 110 300
floats-esbmc-regression/rounding_functions_true-unreach-call.i 2 .20  .20  2.3  28 .84 0   6.1  3.2  81   280 6.7 3.5 130 300
floats-esbmc-regression/trunc_nondet_2_true-unreach-call.i 2 290     290     3500    970 .84 0   7.3  3.9  94   320 11   5.6 160 310
floats-esbmc-regression/trunc_nondet_true-unreach-call.i 2 1.8   1.8   21    60 .84 0   6.5  3.5  93   270 12   6.1 180 320
floats-esbmc-regression/trunc_true-unreach-call.i 2 .13  .13  1.6  26 .84 0   6.6  3.5  85   280 6.9 3.6 120 310
floats-esbmc-regression/Double_div_bad_false-unreach-call.i 0 900     900     8700    1400 .84 0   .53 .36 8.2 40 5.9 3.2 130 310
floats-esbmc-regression/Float_div_bad_false-unreach-call.i 0 900     900     9400    1600 .84 0   .51 .33 10   40 6.1 3.2 100 300
floats-esbmc-regression/digits_bad_for_false-unreach-call.i 0 900     900     8600    2100 .84 0   .50 .32 9.0 40 6.3 3.3 110 300
floats-esbmc-regression/digits_bad_while_false-unreach-call.i 0 900     900     8300    2200 .84 0   .54 .35 9.2 44 6.5 3.4 97 310
../../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 173 73000 73000 630000 96000 150 0   172 54 31 790 3900   172 520 410 6600 20000   172 580 390 8700 26000   172 5300 4600 75000 60000  
    correct results 93 173 3300 3300 33000 11000 79 0   9 45 25 630 3200   7 420 360 4700 15000   68 550 370 8200 23000   41 4900 4400 68000 41000  
        correct true 80 160 1800 1800 20000 9000 68 0   8 0 0 0 0   0 0 0 0 0   66 550 370 8200 23000   41 4900 4400 68000 41000  
        correct false 13 13 1500 1500 13000 2200 11 0   1 45 25 630 3200   7 420 360 4700 15000   2 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) 173
Run set sv-comp17.ReachSafety-Floats