Tool 2LS 0.5.0
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 20:02:31 CET ]] [[ 2017-01-14 18:18:08 CET ]] [[ 2017-01-14 20:29:39 CET ]]
Run set sv-comp17.ReachSafety-Floats
Options --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.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/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.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 1 14     14     160    62 0      0     92    91    1100 2900 97   91   1400 3400
floats-cdfpl/newton_1_5_false-unreach-call.i 1 13     13     150    57 0      0     62    61    930 610 80   73   1600 2200
floats-cdfpl/newton_1_6_false-unreach-call.i 1 11     11     110    54 0      0     17    16    220 530 58   52   750 1700
floats-cdfpl/newton_1_7_false-unreach-call.i 1 8.6   8.5   77    48 0      0     33    31    470 1100 71   65   1400 2000
floats-cdfpl/newton_1_8_false-unreach-call.i 1 5.6   5.6   59    52 0      0     25    23    760 700 31   25   530 1000
floats-cdfpl/newton_2_6_false-unreach-call.i 1 98     98     1300    190 0      0     92    90    850 2400 97   90   1000 2900
floats-cdfpl/newton_2_7_false-unreach-call.i 1 87     87     740    180 0      0     92    90    1300 1500 97   91   2100 2500
floats-cdfpl/newton_2_8_false-unreach-call.i 1 110     110     940    190 0      0     24    22    540 720 97   90   1400 2400
floats-cdfpl/newton_3_6_false-unreach-call.i 1 630     630     7500    630 0      0     92    91    1300 3000 97   91   2200 3800
floats-cdfpl/newton_3_7_false-unreach-call.i 1 260     260     2600    400 0      .34  87    85    780 1700 97   90   3400 3500
floats-cdfpl/newton_3_8_false-unreach-call.i 1 89     89     930    210 0      0     75    73    720 2200 59   53   1200 1400
floats-cdfpl/sine_1_false-unreach-call.i 1 1.9   1.9   25    37 0      0     3.3  1.9  53 270 26   20   300 890
floats-cdfpl/sine_2_false-unreach-call.i 1 1.4   1.4   16    34 0      0     3.1  1.8  60 270 97   90   1800 2800
floats-cdfpl/sine_3_false-unreach-call.i 1 2.5   2.5   29    37 0      0     3.3  1.9  62 270 97   91   820 3000
floats-cdfpl/square_1_false-unreach-call.i 1 .87  .86  11    33 0      0     3.6  2.0  72 270 39   33   540 980
floats-cdfpl/square_2_false-unreach-call.i 1 2.0   2.0   25    34 0      0     3.3  1.9  69 270 87   81   1400 1800
floats-cdfpl/square_3_false-unreach-call.i 1 2.3   2.3   33    35 0      0     3.3  1.9  65 260 97   92   2000 2000
floats-cdfpl/newton_1_1_true-unreach-call.i 2 210     210     1600    130 0      0     900    900    15000   660 270   260   3300 7000
floats-cdfpl/newton_1_2_true-unreach-call.i 2 46     46     400    84 0      0     900    900    17000   550 210   210   3900 7000
floats-cdfpl/newton_1_3_true-unreach-call.i 2 180     180     1600    140 0      0     900    900    19000   530 230   220   4100 7000
floats-cdfpl/newton_2_1_true-unreach-call.i 2 140     140     1100    220 0      0     900    900    16000   530 260   250   4100 7000
floats-cdfpl/newton_2_2_true-unreach-call.i 2 110     110     890    210 0      0     900    900    20000   510 230   220   2300 7000
floats-cdfpl/newton_2_3_true-unreach-call.i 2 210     210     1800    290 0      0     900    900    17000   490 230   220   2100 7000
floats-cdfpl/newton_2_4_true-unreach-call.i 2 410     410     4900    450 0      0     900    900    16000   540 230   230   2400 7000
floats-cdfpl/newton_2_5_true-unreach-call.i 2 280     280     2000    370 0      0     900    900    19000   730 260   260   4600 7000
floats-cdfpl/newton_3_1_true-unreach-call.i 2 400     400     3200    500 0      0     900    900    17000   890 200   200   3900 7000
floats-cdfpl/newton_3_2_true-unreach-call.i 2 360     360     2800    500 0      0     900    900    18000   600 220   210   3100 7000
floats-cdfpl/newton_3_3_true-unreach-call.i 2 510     510     4800    580 0      .34  900    900    23000   730 250   250   3400 7000
floats-cdfpl/newton_3_4_true-unreach-call.i 2 620     620     5100    640 0      0     900    900    19000   810 210   200   4900 7000
floats-cdfpl/newton_3_5_true-unreach-call.i 2 430     430     5000    500 0      0     900    900    18000   870 220   220   4700 7000
floats-cdfpl/sine_4_true-unreach-call.i 2 500     500     5700    110 0      0     900    900    18000   570 220   210   3000 7000
floats-cdfpl/sine_5_true-unreach-call.i 2 8.3   8.3   100    40 0      0     900    900    14000   510 210   210   2500 7000
floats-cdfpl/sine_6_true-unreach-call.i 2 3.6   3.6   49    40 0      0     900    900    16000   630 240   240   5600 7000
floats-cdfpl/sine_7_true-unreach-call.i 2 2.6   2.6   32    38 0      0     900    900    13000   400 240   230   3400 7000
floats-cdfpl/sine_8_true-unreach-call.i 2 15     15     210    54 0      0     900    900    15000   510 200   200   3400 7000
floats-cdfpl/square_4_true-unreach-call.i 2 130     130     1800    190 0      0     900    900    20000   580 210   210   3800 7000
floats-cdfpl/square_5_true-unreach-call.i 2 140     140     1700    190 0      0     520    520    10000   510 230   220   4900 7000
floats-cdfpl/square_6_true-unreach-call.i 2 120     120     1400    190 0      0     840    840    15000   600 270   260   3100 7000
floats-cdfpl/square_7_true-unreach-call.i 2 50     50     590    120 0      0     280    280    3300   500 350   340   5200 7000
floats-cdfpl/square_8_true-unreach-call.i 2 1.2   1.2   14    33 0      0     25    24    520   340 290   280   5200 7000
floats-cbmc-regression/float-div1_true-unreach-call.i 2 .30  .29  3.1  35 .0082 0     6.2  3.7  130   340 100   92   1500 700
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i 2 .99  .98  10    110 .0082 0     13    8.7  260   720 37   24   640 730
floats-cbmc-regression/float-no-simp1_true-unreach-call.i 2 .10  .098 .68 22 0      0     3.2  1.8  64   260 12   6.4 250 300
floats-cbmc-regression/float-no-simp2_true-unreach-call.i 2 .70  .73  7.7  41 .0082 10     21    19    440   320 58   51   1600 460
floats-cbmc-regression/float-no-simp3_true-unreach-call.i 2 .10  .098 .88 23 0      0     4.0  2.2  48   260 11   6.1 190 300
floats-cbmc-regression/float-no-simp4_true-unreach-call.i 2 .33  .33  2.7  35 .0082 .066 6.9  3.7  120   290 24   14   360 510
floats-cbmc-regression/float-no-simp6_true-unreach-call.i 2 .12  .12  .86 22 0      0     4.1  2.3  61   260 14   7.7 240 310
floats-cbmc-regression/float-no-simp7_true-unreach-call.i 2 .12  .11  .72 22 0      0     4.2  2.3  53   260 12   6.5 260 310
floats-cbmc-regression/float-no-simp8_true-unreach-call.i 2 .20  .19  2.0  28 .0082 0     6.9  3.7  77   280 13   7.0 180 300
floats-cbmc-regression/float-rounding1_true-unreach-call.i 2 .23  .22  1.6  28 .0082 .016 6.5  3.5  66   280 6.5 3.4 130 310
floats-cbmc-regression/float-to-double1_true-unreach-call.i 2 .25  .24  1.9  30 .0082 0     5.2  2.9  100   280 210   200   3600 460
floats-cbmc-regression/float-to-double2_true-unreach-call.i 2 .10  .097 .71 22 0      0     3.5  2.0  71   260 12   6.5 220 310
floats-cbmc-regression/float-zero-sum1_true-unreach-call.i 2 .081 .079 1.0  22 0      0     3.7  2.1  62   260 6.3 3.4 120 300
floats-cbmc-regression/float11_true-unreach-call.i 2 .12  .11  .80 22 0      0     3.9  2.2  63   250 13   6.9 190 310
floats-cbmc-regression/float12_true-unreach-call.i 2 .089 .086 .88 22 0      0     4.3  2.4  49   260 19   13   330 310
floats-cbmc-regression/float13_true-unreach-call.i 2 .14  .14  1.1  23 0      0     4.4  2.4  51   260 15   7.8 240 320
floats-cbmc-regression/float14_true-unreach-call.i 2 .21  .21  1.4  28 .0082 0     6.6  3.5  80   270 14   8.2 180 300
floats-cbmc-regression/float18_true-unreach-call.i 0 900     900     9400    1800 .0082 0     .57 .36 8.8 44 5.6 3.0 110 290
floats-cbmc-regression/float19_true-unreach-call.i 2 .19  .18  1.8  28 .0082 0     6.0  3.3  70   280 15   8.5 220 310
floats-cbmc-regression/float1_true-unreach-call.i 2 .097 .094 .73 22 0      0     4.1  2.3  37   250 11   6.1 210 300
floats-cbmc-regression/float20_true-unreach-call.i 2 .11  .11  1.3  25 0      0     4.3  2.4  64   260 29   22   600 400
floats-cbmc-regression/float21_true-unreach-call.i 2 .30  .29  2.2  30 .0082 0     6.9  3.9  100   300 68   59   1100 620
floats-cbmc-regression/float22_true-unreach-call.i 2 .097 .095 .82 22 0      0     6.4  3.5  100   290 16   8.5 280 330
floats-cbmc-regression/float2_true-unreach-call.i 2 .080 .079 .89 22 0      0     4.5  2.5  47   260 13   6.8 200 300
floats-cbmc-regression/float3_true-unreach-call.i 2 .098 .097 .95 24 0      0     3.9  2.3  74   290 22   15   360 330
floats-cbmc-regression/float4_true-unreach-call.i 2 8.6   8.6   140    51 .0082 0     81    78    1200   340 95   87   2100 530
floats-cbmc-regression/float5_true-unreach-call.i 2 .093 .090 .87 23 0      0     4.4  2.5  54   270 33   26   570 330
floats-cbmc-regression/float6_true-unreach-call.i 2 .14  .13  .93 23 0      0     5.3  2.9  55   270 16   8.7 270 320
floats-cbmc-regression/float7_true-unreach-call.i 2 .079 .077 .79 22 0      0     3.8  2.1  53   250 6.2 3.3 120 300
floats-cbmc-regression/float8_true-unreach-call.i 2 .54  .54  5.5  29 .0082 0     7.3  4.2  64   290 13   7.2 190 310
floats-cbmc-regression/float_lib1_true-unreach-call.i 2 .40  .39  4.4  32 .0082 0     6.7  3.6  91   270 15   8.0 190 300
floats-cbmc-regression/float_lib2_true-unreach-call.i 2 .23  .23  1.9  29 .0082 .066 5.8  3.1  74   270 18   10   240 460
float-benchs/cast_float_ptr_false-unreach-call.c 1 .13  .12  1.1  23 .0041 0     3.9  2.2  66 280 5.9 3.2 130 300
float-benchs/cast_union_loose_false-unreach-call.c 1 .15  .14  .93 25 .0041 .17  4.2  2.4  38 300 6.1 3.3 140 300
float-benchs/cast_union_tight_false-unreach-call.c 1 .12  .11  1.2  24 .0041 0     4.1  2.3  72 290 6.6 3.6 63 290
float-benchs/float_int_inv_square_false-unreach-call.c 1 .18  .17  1.2  26 .0041 0     3.7  2.1  77 270 13   7.4 260 320
float-benchs/inv_square_false-unreach-call.c 1 .17  .16  1.0  26 .0041 0     4.0  2.2  84 280 12   6.6 210 310
float-benchs/nan_double_false-unreach-call.c 1 .096 .090 1.2  22 .0041 0     3.5  2.0  43 280 7.1 3.8 130 320
float-benchs/nan_float_false-unreach-call.c 1 .11  .11  .92 22 .0041 0     3.6  2.0  53 280 7.2 3.8 140 310
float-benchs/sin_interpolated_index_false-unreach-call.c 1 6.5   6.5   71    220 .0041 0     3.7  2.1  69 270 97   90   3200 5200
float-benchs/sqrt_poly2_false-unreach-call.c 1 .99  .98  8.5  39 .0041 0     3.5  1.9  63 280 11   5.7 180 300
float-benchs/Muller_Kahan_true-unreach-call.c 0 900     900     10000    450 .0041 0     .65 .41 7.9 40 5.8 3.0 100 300
float-benchs/Rump_double_true-unreach-call.c 2 .13  .13  1.6  25 .0041 0     3.8  2.1  56   260 23   17   430 810
float-benchs/Rump_float_true-unreach-call.c 2 .13  .12  1.0  23 .0041 0     3.3  1.9  61   260 16   9.8 320 400
float-benchs/addsub_double_exact_true-unreach-call.c 2 .10  .10  .82 22 .0041 0     4.4  2.5  51   260 13   7.1 270 310
float-benchs/addsub_float_exact_true-unreach-call.c 2 .11  .11  .78 22 .0041 0     3.6  2.0  74   260 13   7.2 230 310
float-benchs/addsub_float_inexact_true-unreach-call.c 2 .088 .086 1.0  22 .0041 0     3.5  2.0  68   260 12   6.7 220 310
float-benchs/arctan_Pade_true-unreach-call.c 2 140     140     1600    500 .0041 0     16    14    280   510 45   39   610 1200
float-benchs/bary_diverge_true-unreach-call.c 0 900     900     9600    390 .0041 .10  .55 .36 13   41 6.7 3.5 130 310
float-benchs/cast_float_union_true-unreach-call.c 2 .13  .12  .86 23 .0041 0     3.7  2.1  62   260 10   5.6 180 300
float-benchs/cos_polynomial_true-unreach-call.c 2 9.4   9.4   92    88 .0041 0     900    900    16000   1200 400   390   3600 7000
float-benchs/divmul_buf_diverge_true-unreach-call.c 2 .67  .67  7.2  32 .0041 0     4.0  2.2  52   280 960   820   24000 4800
float-benchs/divmul_diverge_true-unreach-call.c 0 900     900     9000    490 .0041 0     .49 .31 12   39 7.5 3.9 88 290
float-benchs/drift_tenth_true-unreach-call.c 2 .68  .68  8.2  36 .0041 0     3.8  2.1  50   260 160   150   3500 640
float-benchs/exp_loop_true-unreach-call.c 2 35     35     380    240 .0041 0     5.1  2.8  62   280 960   950   19000 1100
float-benchs/feedback_diverge_true-unreach-call.c 0 900     900     11000    1400 .0041 0     .67 .42 8.9 40 5.7 3.0 96 300
float-benchs/filter1_true-unreach-call.c 0 900     900     11000    1100 .0041 0     .53 .34 12   42 8.1 4.3 97 290
float-benchs/filter2_alt_true-unreach-call.c 0 900     900     8600    440 .0041 0     .57 .36 10   42 5.4 2.9 91 290
float-benchs/filter2_iterated_true-unreach-call.c 0 900     900     8500    420 .0041 0     .47 .31 10   39 5.4 3.0 110 290
float-benchs/filter2_reinit_true-unreach-call.c 0 900     900     8900    340 .0041 0     .63 .41 5.6 40 6.3 3.3 140 310
float-benchs/filter2_set_true-unreach-call.c 0 900     900     11000    330 .0041 0     .49 .32 13   40 5.6 3.0 120 290
float-benchs/filter2_true-unreach-call.c 0 900     900     9600    490 .0041 0     .51 .33 7.4 41 6.0 3.2 110 300
float-benchs/filter_iir_true-unreach-call.c 2 .43  .43  6.2  53 .0041 0     900    900    19000   3000 6.5 3.4 120 300
float-benchs/float_double_true-unreach-call.c 2 .12  .11  .69 22 .0041 0     3.4  1.9  58   260 13   7.0 250 310
float-benchs/image_filter_true-unreach-call.c 0 900     900     12000    1100 .0041 0     .51 .32 11   40 6.3 3.3 120 300
float-benchs/interpolation2_true-unreach-call.c 2 .56  .56  8.2  28 .0041 0     47    45    1500   560 960   950   18000 570
float-benchs/interpolation_true-unreach-call.c 2 .24  .24  2.3  27 .0041 0     61    58    1600   480 210   210   5300 7000
float-benchs/inv_sqrt_Quake_true-unreach-call.c 2 .24  .24  2.2  28 .0041 0     5.3  3.2  96   320 6.8 3.6 120 310
float-benchs/inv_square_int_true-unreach-call.c 2 .16  .16  1.2  26 .0041 0     4.4  2.5  49   270 26   20   650 320
float-benchs/inv_square_true-unreach-call.c 2 .14  .14  1.2  26 .0041 0     4.6  2.6  50   270 77   70   920 370
float-benchs/loop_true-unreach-call.c 0 900     900     10000    270 .0041 0     .62 .39 7.9 39 5.7 3.0 91 300
float-benchs/mea8000_true-unreach-call.c 0 900     900     7400    2100 .0041 0     .67 .42 8.2 40 6.4 3.4 130 300
float-benchs/nan_double_range_true-unreach-call.c 2 .11  .10  .97 22 .0041 0     3.9  2.2  56   270 13   7.3 210 320
float-benchs/nan_float_range_true-unreach-call.c 2 .13  .12  .77 22 .0041 0     4.1  2.3  58   260 17   9.8 250 310
float-benchs/rlim_exit_true-unreach-call.c 0 900     900     12000    1700 .0041 0     .53 .34 12   43 5.9 3.1 120 290
float-benchs/rlim_invariant_true-unreach-call.c 0 900     900     13000    1500 .0041 0     .50 .32 12   40 6.0 3.2 120 310
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call.c 0 900     900     8200    700 .0041 0     .66 .42 8.7 40 5.9 3.2 120 300
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call.c 0 900     900     7500    700 .0041 10     .79 .50 7.5 41 5.8 3.2 130 300
float-benchs/sin_interpolated_index_true-unreach-call.c 0 900     900     7200    700 .0041 0     .50 .32 10   40 6.9 3.6 110 300
float-benchs/sin_interpolated_negation_true-unreach-call.c 0 900     900     7000    440 .0041 0     .49 .31 9.0 40 5.8 3.1 100 300
float-benchs/sin_interpolated_smallrange_true-unreach-call.c 0 900     900     8400    320 .0041 0     .65 .40 8.8 40 5.7 3.0 110 290
float-benchs/sqrt_Householder_constant_true-unreach-call.c 0 900     900     8000    240 .0041 0     .58 .38 9.2 40 6.2 3.2 130 300
float-benchs/sqrt_Householder_interval_true-unreach-call.c 0 900     900     11000    320 .0041 0     .66 .41 7.5 39 6.1 3.2 120 300
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c 0 900     900     6600    270 .0041 0     .54 .34 11   39 6.1 3.2 110 300
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c 0 900     900     6200    330 .0041 0     .67 .43 8.4 41 5.7 3.0 110 300
float-benchs/sqrt_biNewton_pseudoconstant_true-unreach-call.c 0 900     900     6600    380 .0041 0     .62 .39 9.6 41 6.0 3.2 80 300
float-benchs/sqrt_poly_true-unreach-call.c 2 1.1   1.1   13    48 .0041 0     97    95    1900   470 560   550   12000 1400
float-benchs/water_pid_true-unreach-call.c 0 900     900     12000    1100 .0041 0     .49 .32 12   39 5.9 3.2 110 300
float-benchs/zonotope_2_true-unreach-call.c 0 900     900     7900    890 .0041 0     .60 .39 9.3 40 6.1 3.2 120 290
float-benchs/zonotope_3_true-unreach-call.c 0 900     900     11000    1400 .0041 0     .51 .33 11   41 5.8 3.1 110 290
float-benchs/zonotope_loose_true-unreach-call.c 2 .38  .38  4.3  30 .0041 0     5.3  3.4  67   320 720   710   12000 1400
float-benchs/zonotope_tight_true-unreach-call.c 2 .22  .22  1.9  30 .0041 0     5.2  3.3  64   320 620   610   9300 1200
floats-esbmc-regression/Double_div_true-unreach-call.i 2 2.9   2.9   41    46 0      0     3.7  2.1  34   260 130   120   1700 1400
floats-esbmc-regression/Float_div_true-unreach-call.i 2 .70  .70  8.1  30 0      0     3.9  2.2  42   260 240   230   3500 710
floats-esbmc-regression/ceil_nondet_true-unreach-call.i 2 3.2   3.2   40    71 .025  .082 6.1  3.3  120   290 12   6.1 230 300
floats-esbmc-regression/ceil_true-unreach-call.i 2 .49  .48  3.8  31 .025  .15  5.8  3.1  120   280 6.2 3.2 75 300
floats-esbmc-regression/copysign_true-unreach-call.i 2 .36  .36  2.6  29 .016  .066 6.7  3.6  65   270 6.6 3.5 120 300
floats-esbmc-regression/digits_for_true-unreach-call.i 0 900     900     7900    510 0      0     .59 .37 10   39 7.6 4.0 76 290
floats-esbmc-regression/digits_while_true-unreach-call.i 0 900     900     8500    520 0      0     .55 .34 13   42 5.8 3.1 120 300
floats-esbmc-regression/fabs_true-unreach-call.i 2 .22  .22  2.0  28 .0082 0     6.9  3.7  74   280 13   6.8 200 310
floats-esbmc-regression/fdim_true-unreach-call.i 2 .24  .24  1.9  29 .0082 .25  5.0  2.7  96   270 6.8 3.6 110 310
floats-esbmc-regression/floor_nondet_true-unreach-call.i 2 3.2   3.2   42    73 .025  .082 7.9  4.2  84   280 12   6.6 230 300
floats-esbmc-regression/floor_true-unreach-call.i 2 .44  .43  4.9  31 .025  .082 5.9  3.2  100   280 6.8 3.6 110 320
floats-esbmc-regression/fmax_true-unreach-call.i 2 .32  .31  3.7  31 .016  0     6.7  3.6  71   270 6.3 3.4 120 290
floats-esbmc-regression/fmin_true-unreach-call.i 2 .35  .34  3.0  30 .016  0     6.0  3.2  99   280 6.5 3.5 120 310
floats-esbmc-regression/fmod2_true-unreach-call.i 2 .91  .90  12    76 .033  .016 9.0  4.8  110   310 11   5.8 200 300
floats-esbmc-regression/fmod3_true-unreach-call.i 2 .96  .95  9.0  79 .033  .082 9.0  4.8  120   320 11   5.8 200 310
floats-esbmc-regression/fmod_true-unreach-call.i 2 .89  .89  8.0  63 .033  .016 6.4  3.5  100   290 7.4 4.0 160 310
floats-esbmc-regression/isgreater_true-unreach-call.i 2 .21  .21  1.6  28 .0082 0     6.6  3.6  73   280 11   5.6 130 300
floats-esbmc-regression/isgreaterequal_true-unreach-call.i 2 .21  .21  1.5  28 .0082 0     6.1  3.3  73   270 12   6.2 200 300
floats-esbmc-regression/isless_true-unreach-call.i 2 .21  .21  1.9  28 .0082 0     6.0  3.3  52   270 11   5.8 200 300
floats-esbmc-regression/islessequal_true-unreach-call.i 2 .23  .23  1.4  28 .0082 0     6.4  3.5  75   270 12   6.4 160 300
floats-esbmc-regression/islessgreater_true-unreach-call.i 2 .21  .21  2.1  28 .0082 0     7.1  3.8  67   280 14   7.3 150 310
floats-esbmc-regression/isunordered_true-unreach-call.i 2 .28  .28  2.7  28 .016  0     6.4  3.4  66   270 11   5.7 150 300
floats-esbmc-regression/lrint_true-unreach-call.i 2 .51  .50  3.9  30 .025  .082 7.8  4.2  87   280 6.9 3.6 140 310
floats-esbmc-regression/modf_true-unreach-call.i 2 .41  .39  3.1  30 .025  .082 5.8  3.1  65   280 6.7 3.5 140 310
floats-esbmc-regression/nan_true-unreach-call.i 2 .27  .26  2.5  30 .0082 .23  5.9  3.2  80   270 13   7.0 210 310
floats-esbmc-regression/nearbyint2_true-unreach-call.i 2 .53  .52  4.2  31 .025  .25  6.2  3.3  130   290 7.1 3.7 140 300
floats-esbmc-regression/nearbyint_true-unreach-call.i 2 .46  .46  6.0  31 .025  .016 8.1  4.3  170   290 8.5 4.5 85 310
floats-esbmc-regression/remainder_true-unreach-call.i 2 1.1   1.1   10    86 .033  .016 7.4  4.1  75   280 6.7 3.5 130 300
floats-esbmc-regression/rint2_true-unreach-call.i 2 .50  .49  4.4  31 .025  .16  6.2  3.3  97   290 7.2 3.8 120 300
floats-esbmc-regression/rint_true-unreach-call.i 2 .51  .50  4.3  31 .025  .016 8.9  4.7  150   310 7.0 3.7 130 300
floats-esbmc-regression/round_nondet_true-unreach-call.i 2 3.6   3.6   44    100 .016  .016 7.0  3.8  83   290 12   6.1 200 300
floats-esbmc-regression/round_true-unreach-call.i 2 .53  .52  5.8  35 .025  .082 7.8  4.2  90   280 6.9 3.7 120 300
floats-esbmc-regression/rounding_functions_true-unreach-call.i 2 .52  .51  5.2  31 .025  .15  6.2  3.3  110   270 6.9 3.6 130 300
floats-esbmc-regression/trunc_nondet_2_true-unreach-call.i 2 1.9   1.9   23    35 .025  .016 7.2  3.9  130   320 11   5.6 110 310
floats-esbmc-regression/trunc_nondet_true-unreach-call.i 2 2.4   2.4   34    74 .025  .016 6.4  3.4  110   290 12   6.3 220 300
floats-esbmc-regression/trunc_true-unreach-call.i 2 .48  .47  4.2  31 .025  .25  6.6  3.6  95   280 6.0 3.2 88 310
floats-esbmc-regression/Double_div_bad_false-unreach-call.i 0 900     900     11000    490 0      0     .61 .39 12 44 5.8 3.1 120 290
floats-esbmc-regression/Float_div_bad_false-unreach-call.i 0 900     900     11000    330 0      0     .49 .31 10 40 5.1 2.8 92 290
floats-esbmc-regression/digits_bad_for_false-unreach-call.i 0 900     900     7600    450 0      0     .52 .33 12 40 5.7 3.0 130 290
floats-esbmc-regression/digits_bad_while_false-unreach-call.i 0 900     900     7500    450 0      0     .48 .31 11 40 6.3 3.4 110 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 248 38000 38000 390000 37000 1.0   23    172 750 710 10000 22000   172 1500 1400 29000 47000   172 21000 21000 410000 44000   172 13000 12000 230000 220000  
    correct results 137 248 6400 6400 64000 12000 .89  13    20 750 700 9900 21000   12 1500 1300 28000 46000   73 21000 21000 410000 43000   43 13000 12000 230000 220000  
        correct true 111 222 5100 5100 50000 9400 .86  13    6 0 0 0 0   0 0 0 0 0   70 21000 21000 410000 43000   43 13000 12000 230000 220000  
        correct false 26 26 1300 1300 15000 2700 .037 .51 14 750 700 9900 21000   12 1500 1300 28000 46000   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) 248
Run set sv-comp17.ReachSafety-Floats