Tool DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017
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-11 11:24:16 CET [[ 2017-01-14 21:58:42 CET ]] [[ 2017-01-14 22:27:33 CET ]] [[ 2017-01-14 22:07:52 CET ]] [[ 2017-01-14 22:42:14 CET ]]
Run set sv-comp17.ReachSafety-Floats
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-11_1124.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    900    8200   470 .85 0      .64 .41 7.5 40 6.1 3.2 110 300
floats-cdfpl/newton_1_5_false-unreach-call.i 0 890    900    6700   480 .85 0      .58 .36 9.6 40 7.1 3.7 79 300
floats-cdfpl/newton_1_6_false-unreach-call.i 0 890    900    7700   450 .85 0      .60 .38 9.3 40 5.7 3.0 100 300
floats-cdfpl/newton_1_7_false-unreach-call.i 0 890    900    7500   470 .85 0      .54 .35 14   40 6.1 3.2 120 310
floats-cdfpl/newton_1_8_false-unreach-call.i 1 880    880    8400   460 .85 0      30    28    430   700 37   29   550 990
floats-cdfpl/newton_2_6_false-unreach-call.i 0 890    900    6900   760 .85 0      .51 .34 11   40 6.5 3.4 87 290
floats-cdfpl/newton_2_7_false-unreach-call.i 0 890    900    6800   760 .85 0      .50 .31 10   40 6.5 3.4 120 300
floats-cdfpl/newton_2_8_false-unreach-call.i 0 890    900    6500   760 .85 0      .49 .31 7.9 39 5.6 3.0 110 310
floats-cdfpl/newton_3_6_false-unreach-call.i 0 890    900    7100   1200 .85 0      .67 .43 7.8 40 7.2 3.8 71 300
floats-cdfpl/newton_3_7_false-unreach-call.i 0 890    900    8400   1100 .85 0      .62 .40 10   45 6.3 3.3 120 290
floats-cdfpl/newton_3_8_false-unreach-call.i 0 890    900    11000   1100 .85 0      .67 .42 7.2 42 6.4 3.4 61 300
floats-cdfpl/sine_1_false-unreach-call.i 1 180    180    1900   240 .84 0      3.3  1.9  70   280 32   25   380 890
floats-cdfpl/sine_2_false-unreach-call.i 1 89    89    890   200 .84 0      3.7  2.1  57   270 97   89   1200 2600
floats-cdfpl/sine_3_false-unreach-call.i 1 65    65    570   180 .84 .13   4.1  2.3  50   270 94   88   1200 3400
floats-cdfpl/square_1_false-unreach-call.i 1 590    590    4100   200 .84 0      3.7  2.0  56   280 50   43   600 970
floats-cdfpl/square_2_false-unreach-call.i 0 890    900    7400   260 .84 0      .51 .32 12   40 7.4 3.9 110 320
floats-cdfpl/square_3_false-unreach-call.i 0 890    900    6300   350 .84 0      .64 .41 10   44 5.4 2.9 120 290
floats-cdfpl/newton_1_1_true-unreach-call.i 0 890    900    9600   410 .85 0      .62 .39 9.8 39 5.8 3.1 92 300
floats-cdfpl/newton_1_2_true-unreach-call.i 0 890    900    9900   400 .85 0      .69 .44 8.6 42 5.6 3.0 50 300
floats-cdfpl/newton_1_3_true-unreach-call.i 0 890    900    6500   470 .85 0      .50 .33 11   39 6.1 3.2 110 300
floats-cdfpl/newton_2_1_true-unreach-call.i 0 890    900    11000   690 .85 0      .66 .42 8.4 43 5.4 2.9 65 300
floats-cdfpl/newton_2_2_true-unreach-call.i 0 890    900    8200   770 .85 0      .56 .35 16   42 6.1 3.2 75 310
floats-cdfpl/newton_2_3_true-unreach-call.i 0 890    900    8900   760 .85 0      .49 .32 7.5 39 5.6 3.0 80 300
floats-cdfpl/newton_2_4_true-unreach-call.i 0 890    900    9400   690 .85 0      .61 .40 8.4 41 5.1 2.8 58 290
floats-cdfpl/newton_2_5_true-unreach-call.i 0 890    900    8200   760 .85 0      .52 .33 9.5 39 7.0 3.6 100 310
floats-cdfpl/newton_3_1_true-unreach-call.i 0 890    900    11000   1000 .85 0      .58 .36 11   39 5.8 3.1 74 300
floats-cdfpl/newton_3_2_true-unreach-call.i 0 890    900    8800   1000 .85 0      .49 .32 11   39 5.7 3.0 54 300
floats-cdfpl/newton_3_3_true-unreach-call.i 0 890    900    9700   970 .85 0      .62 .40 8.4 40 6.6 3.4 70 300
floats-cdfpl/newton_3_4_true-unreach-call.i 0 890    900    7500   1100 .85 0      .60 .38 8.5 40 5.5 2.9 87 280
floats-cdfpl/newton_3_5_true-unreach-call.i 0 890    900    6900   1100 .85 0      .51 .33 12   41 6.0 3.2 90 300
floats-cdfpl/sine_4_true-unreach-call.i 0 890    900    7700   310 .84 0      .62 .39 11   40 7.1 3.8 55 300
floats-cdfpl/sine_5_true-unreach-call.i 0 890    900    8800   310 .84 0      .66 .42 7.9 40 5.9 3.1 88 300
floats-cdfpl/sine_6_true-unreach-call.i 0 890    900    9000   310 .84 0      .66 .42 8.3 41 5.6 3.0 87 300
floats-cdfpl/sine_7_true-unreach-call.i 0 890    900    6500   310 .84 0      .49 .32 8.8 40 6.3 3.3 120 290
floats-cdfpl/sine_8_true-unreach-call.i 0 890    900    7400   310 .84 0      .51 .33 13   39 5.9 3.1 100 310
floats-cdfpl/square_4_true-unreach-call.i 0 890    900    6900   250 .84 0      .69 .44 7.2 42 6.7 3.5 77 300
floats-cdfpl/square_5_true-unreach-call.i 0 890    900    6200   350 .84 0      .58 .37 10   40 6.1 3.2 93 290
floats-cdfpl/square_6_true-unreach-call.i 0 890    900    7800   250 .84 0      .69 .44 6.2 45 5.8 3.1 110 300
floats-cdfpl/square_7_true-unreach-call.i 0 890    900    8200   260 .84 0      .51 .33 9.7 40 6.0 3.2 89 300
floats-cdfpl/square_8_true-unreach-call.i 0 890    900    7100   200 1.7  0      .52 .33 11   40 5.5 2.9 89 290
floats-cbmc-regression/float-div1_true-unreach-call.i 2 36    33    380   370 3.5  0      7.9  4.7  66   340 90   81   860 690
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i 2 24    11    210   2200 3.7  .066  13    8.9  140   670 38   26   430 730
floats-cbmc-regression/float-no-simp1_true-unreach-call.i 2 3.1  1.7  30   270 3.4  0      3.7  2.1  51   260 11   5.8 110 300
floats-cbmc-regression/float-no-simp2_true-unreach-call.i 2 290    280    3400   320 3.5  .016  22    19    320   320 57   51   720 450
floats-cbmc-regression/float-no-simp3_true-unreach-call.i 2 3.1  1.7  29   270 3.5  0      3.5  2.0  77   270 11   6.0 190 300
floats-cbmc-regression/float-no-simp4_true-unreach-call.i 2 6.4  3.3  64   300 3.5  0      6.3  3.4  110   270 22   13   270 490
floats-cbmc-regression/float-no-simp6_true-unreach-call.i 2 3.2  1.7  32   250 3.4  0      3.6  2.0  64   260 13   7.1 180 320
floats-cbmc-regression/float-no-simp7_true-unreach-call.i 2 3.0  1.7  32   260 3.4  0      3.3  1.9  75   250 12   6.2 160 320
floats-cbmc-regression/float-no-simp8_true-unreach-call.i 2 4.3  2.4  44   280 3.4  0      5.8  3.1  45   270 13   6.8 110 300
floats-cbmc-regression/float-rounding1_true-unreach-call.i 0 8.9  3.9  81   440 3.6  0      6.7  3.6  70   280 6.3 3.4 79 310
floats-cbmc-regression/float-to-double1_true-unreach-call.i 2 29    26    390   320 3.5  .033  5.3  2.9  91   290 190   190   3900 450
floats-cbmc-regression/float-to-double2_true-unreach-call.i 2 3.0  1.7  27   250 3.4  0      3.7  2.1  32   260 12   6.6 230 310
floats-cbmc-regression/float-zero-sum1_true-unreach-call.i 2 3.1  1.7  33   260 3.4  0      3.6  2.0  70   260 6.0 3.2 93 310
floats-cbmc-regression/float11_true-unreach-call.i 2 3.4  1.9  33   260 3.4  .0041 3.5  2.0  51   250 13   6.9 130 320
floats-cbmc-regression/float12_true-unreach-call.i 2 7.6  5.8  86   280 3.4  0      3.4  1.9  53   260 19   13   180 300
floats-cbmc-regression/float13_true-unreach-call.i 2 3.0  1.7  27   260 3.4  0      4.5  2.5  47   260 13   7.4 210 320
floats-cbmc-regression/float14_true-unreach-call.i 2 4.3  2.5  42   270 3.4  .19   5.8  3.2  74   270 13   7.3 230 310
floats-cbmc-regression/float18_true-unreach-call.i 2 18    16    230   260 39    0      26    22    600   440 6.7 3.5 72 330
floats-cbmc-regression/float19_true-unreach-call.i 2 7.3  4.5  69   330 3.5  33      5.8  3.1  85   280 16   9.3 200 300
floats-cbmc-regression/float1_true-unreach-call.i 2 3.0  1.7  31   230 3.4  0      3.4  1.9  75   260 11   5.8 130 300
floats-cbmc-regression/float20_true-unreach-call.i 2 22    21    230   260 3.4  0      3.9  2.2  58   260 27   21   600 410
floats-cbmc-regression/float21_true-unreach-call.i 2 30    27    300   310 3.5  0      7.5  4.2  77   300 68   61   1100 620
floats-cbmc-regression/float22_true-unreach-call.i 0 17    17    200   51 84    0      .51 .33 11   41 6.0 3.2 130 290
floats-cbmc-regression/float2_true-unreach-call.i 2 2.9  1.7  27   220 3.4  0      3.3  1.9  70   260 12   6.4 180 300
floats-cbmc-regression/float3_true-unreach-call.i 2 7.7  6.3  80   300 3.4  33      3.5  2.1  69   280 19   13   270 330
floats-cbmc-regression/float4_true-unreach-call.i 2 320    320    3300   590 3.5  0      63    61    1800   340 94   87   1300 540
floats-cbmc-regression/float5_true-unreach-call.i 2 16    15    190   250 3.4  0      4.2  2.4  49   270 38   32   960 300
floats-cbmc-regression/float6_true-unreach-call.i 2 3.6  2.2  34   260 3.4  .0041 3.9  2.2  77   270 13   7.2 160 310
floats-cbmc-regression/float7_true-unreach-call.i 2 3.0  1.7  33   260 3.4  0      4.0  2.3  49   260 6.8 3.6 82 300
floats-cbmc-regression/float8_true-unreach-call.i 2 7.9  4.9  75   340 3.5  .0041 6.4  3.7  110   290 14   7.5 140 310
floats-cbmc-regression/float_lib1_true-unreach-call.i 2 4.5  2.7  48   260 3.4  0      5.5  3.0  81   270 11   6.1 170 300
floats-cbmc-regression/float_lib2_true-unreach-call.i 2 4.4  2.5  48   280 3.4  0      5.4  2.9  89   280 20   11   200 460
float-benchs/cast_float_ptr_false-unreach-call.c 1 .39 .39 5.0 49 .85 0      2.7  1.5  42   160 7.0 3.7 110 300
float-benchs/cast_union_loose_false-unreach-call.c 1 .49 .49 6.0 49 .85 0      5.0  2.9  62   290 6.3 3.3 100 310
float-benchs/cast_union_tight_false-unreach-call.c 1 1.1  1.1  14   49 .85 0      2.6  1.5  37   160 6.4 3.4 110 310
float-benchs/float_int_inv_square_false-unreach-call.c 1 17    17    220   69 .85 .041  4.7  2.7  52   280 13   7.3 210 320
float-benchs/inv_square_false-unreach-call.c 1 .48 .48 5.1 41 .85 0      3.8  2.2  83   290 13   6.9 190 320
float-benchs/nan_double_false-unreach-call.c 1 .37 .37 3.9 48 .85 0      3.3  1.9  72   260 7.1 3.8 130 310
float-benchs/nan_float_false-unreach-call.c 1 .37 .37 4.4 48 .85 0      3.2  1.8  67   270 6.9 3.7 140 310
float-benchs/sin_interpolated_index_false-unreach-call.c 1 130    130    1300   440 .86 .28   4.5  2.5  66   280 97   90   1300 3400
float-benchs/sqrt_poly2_false-unreach-call.c 1 290    290    2600   340 .86 0      3.0  1.7  37   170 10   5.5 170 300
float-benchs/Muller_Kahan_true-unreach-call.c 0 890    900    11000   1200 15    0      .57 .37 10   39 5.4 2.9 88 300
float-benchs/Rump_double_true-unreach-call.c 2 3.1  1.7  32   260 3.4  0      3.4  1.9  37   260 22   16   230 790
float-benchs/Rump_float_true-unreach-call.c 2 3.0  1.7  29   240 3.4  0      4.0  2.3  44   260 14   8.7 210 380
float-benchs/addsub_double_exact_true-unreach-call.c 2 3.1  1.7  34   260 3.4  0      4.2  2.3  40   260 14   7.5 200 320
float-benchs/addsub_float_exact_true-unreach-call.c 2 2.9  1.6  32   250 3.4  0      4.0  2.3  40   260 20   11   140 320
float-benchs/addsub_float_inexact_true-unreach-call.c 2 3.2  1.7  31   270 3.4  0      4.5  2.5  45   260 16   8.5 99 330
float-benchs/arctan_Pade_true-unreach-call.c 0 890    900    7800   1100 .85 0      .61 .39 9.5 40 5.9 3.1 94 300
float-benchs/bary_diverge_true-unreach-call.c 0 890    900    10000   270 7.6  0      .48 .32 12   40 6.3 3.3 130 300
float-benchs/cast_float_union_true-unreach-call.c 2 3.1  1.7  30   260 3.4  0      3.4  1.9  38   260 11   5.6 170 300
float-benchs/cos_polynomial_true-unreach-call.c 0 890    900    7500   620 .85 0      .64 .41 7.2 39 5.3 2.9 120 290
float-benchs/divmul_buf_diverge_true-unreach-call.c 0 890    900    9400   280 24    0      .60 .39 7.8 40 6.1 3.2 96 310
float-benchs/divmul_diverge_true-unreach-call.c 0 890    900    9700   260 21    0      .49 .31 12   39 7.1 3.7 67 300
float-benchs/drift_tenth_true-unreach-call.c 0 890    900    7400   490 24    0      .59 .39 8.5 40 5.1 2.8 56 290
float-benchs/exp_loop_true-unreach-call.c 0 890    900    7500   380 13    0      .49 .32 10   41 5.8 3.1 110 300
float-benchs/feedback_diverge_true-unreach-call.c 0 890    900    8400   310 19    0      .67 .43 7.6 43 5.5 2.9 110 290
float-benchs/filter1_true-unreach-call.c 0 890    900    7100   300 5.9  0      .63 .41 7.6 44 6.0 3.2 71 300
float-benchs/filter2_alt_true-unreach-call.c 0 890    900    8600   230 4.4  0      .59 .36 9.6 41 5.8 3.1 71 290
float-benchs/filter2_iterated_true-unreach-call.c 0 890    900    7700   6500 2.7  0      .53 .33 12   40 7.3 3.8 140 320
float-benchs/filter2_reinit_true-unreach-call.c 0 890    900    6900   250 1.7  0      .53 .35 13   42 5.4 2.9 88 290
float-benchs/filter2_set_true-unreach-call.c 0 890    900    7400   440 1.7  0      .52 .33 12   40 5.8 3.0 68 300
float-benchs/filter2_true-unreach-call.c 0 890    900    7000   530 3.4  0      .51 .34 11   39 5.6 3.0 84 300
float-benchs/filter_iir_true-unreach-call.c 0 890    900    11000   780 2.5  0      .60 .38 7.2 40 5.2 2.8 86 290
float-benchs/float_double_true-unreach-call.c 2 3.2  1.7  28   270 3.4  0      3.1  1.8  62   250 12   6.8 160 310
float-benchs/image_filter_true-unreach-call.c 0 890    900    8300   3100 3.4  0      .53 .34 14   40 5.4 2.9 84 290
float-benchs/interpolation2_true-unreach-call.c 0 710    700    7300   350 11    .11   58    55    870   560 960   950   21000 570
float-benchs/interpolation_true-unreach-call.c 0 140    140    1500   320 12    0      70    67    1100   480 180   170   3600 7000
float-benchs/inv_sqrt_Quake_true-unreach-call.c -16 320    320    2800   260 3.4  .0041 4.4  2.6  74   310 6.4 3.4 99 310
float-benchs/inv_square_int_true-unreach-call.c 2 27    25    330   310 3.4  0      3.5  2.0  47   270 39   34   540 350
float-benchs/inv_square_true-unreach-call.c 2 5.3  3.5  58   290 3.4  0      3.6  2.1  67   270 59   53   610 330
float-benchs/loop_true-unreach-call.c 0 890    900    9200   320 25    0      .61 .40 5.2 40 6.2 3.3 65 300
float-benchs/mea8000_true-unreach-call.c 0 890    900    8500   2000 2.6  .086  .52 .34 12   42 6.5 3.5 70 300
float-benchs/nan_double_range_true-unreach-call.c 2 3.8  1.9  35   290 3.4  .0041 3.6  2.0  54   260 13   7.1 230 330
float-benchs/nan_float_range_true-unreach-call.c 2 3.8  2.0  35   280 3.4  0      4.1  2.3  45   260 18   10   150 310
float-benchs/rlim_exit_true-unreach-call.c 0 890    900    12000   220 21    0      .66 .42 7.4 42 5.9 3.1 120 300
float-benchs/rlim_invariant_true-unreach-call.c 0 890    900    9300   450 4.4  0      5.8  3.6  100   330 190   180   3100 630
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call.c 0 890    900    7700   1700 .86 0      .65 .42 7.6 39 5.6 3.0 87 300
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call.c 0 890    900    6400   1700 .86 0      .70 .43 4.5 43 5.7 3.0 51 300
float-benchs/sin_interpolated_index_true-unreach-call.c 0 890    900    7900   480 .86 .10   .62 .41 7.7 39 6.4 3.4 130 300
float-benchs/sin_interpolated_negation_true-unreach-call.c 0 890    900    7500   2100 .86 0      .64 .43 8.2 41 5.6 3.0 52 300
float-benchs/sin_interpolated_smallrange_true-unreach-call.c 0 890    900    6200   1800 .86 0      .50 .31 7.5 39 6.2 3.3 79 310
float-benchs/sqrt_Householder_constant_true-unreach-call.c 0 890    900    8800   1000 2.5  0      .54 .35 8.6 42 5.5 2.9 80 300
float-benchs/sqrt_Householder_interval_true-unreach-call.c 0 890    900    7000   620 3.4  0      .61 .39 6.5 40 7.4 3.9 64 310
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c 0 890    900    10000   1300 1.7  0      .50 .32 8.2 40 6.9 3.6 76 300
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c 0 890    900    7900   1100 2.5  0      .53 .35 8.7 39 5.7 3.0 72 300
float-benchs/sqrt_biNewton_pseudoconstant_true-unreach-call.c 0 890    900    8300   1400 1.7  16      .55 .35 8.6 39 6.9 3.6 94 320
float-benchs/sqrt_poly_true-unreach-call.c 0 890    900    11000   490 .85 0      .52 .34 11   40 5.3 2.8 63 290
float-benchs/water_pid_true-unreach-call.c 0 890    900    7800   580 5.1  0      .52 .33 11   40 6.4 3.4 130 300
float-benchs/zonotope_2_true-unreach-call.c 0 44    43    590   76 170    0      .54 .35 8.6 42 5.3 2.9 63 300
float-benchs/zonotope_3_true-unreach-call.c 2 210    190    2300   1800 4.2  .0041 9.3  6.5  110   400 960   840   21000 4900
float-benchs/zonotope_loose_true-unreach-call.c 2 92    90    1000   350 3.4  0      4.3  2.8  100   320 550   540   5000 1200
float-benchs/zonotope_tight_true-unreach-call.c 2 110    110    1000   350 3.4  0      4.5  2.9  81   320 540   540   6200 1100
floats-esbmc-regression/Double_div_true-unreach-call.i 0 890    900    6500   270 5.9  0      .50 .32 7.3 41 5.8 3.1 90 300
floats-esbmc-regression/Float_div_true-unreach-call.i 0 890    900    8300   670 47    0      .50 .33 12   41 5.4 2.9 87 290
floats-esbmc-regression/ceil_nondet_true-unreach-call.i 0 17    12    170   450 3.7  0      6.4  3.4  62   280 11   5.7 160 300
floats-esbmc-regression/ceil_true-unreach-call.i 2 4.3  2.5  39   270 3.4  0      5.5  3.0  84   280 5.8 3.1 110 290
floats-esbmc-regression/copysign_true-unreach-call.i 2 4.6  2.9  38   320 3.4  44      6.0  3.2  79   270 6.1 3.3 130 300
floats-esbmc-regression/digits_for_true-unreach-call.i 2 32    30    270   260 4.2  .0082 900    900    19000   1000 960   950   13000 1400
floats-esbmc-regression/digits_while_true-unreach-call.i 2 31    30    330   260 4.2  0      900    900    13000   970 960   950   16000 3100
floats-esbmc-regression/fabs_true-unreach-call.i 2 5.8  2.9  50   300 3.5  0      5.5  3.0  77   260 13   6.8 160 310
floats-esbmc-regression/fdim_true-unreach-call.i 2 4.4  2.5  43   270 3.4  0      6.5  3.5  76   270 6.8 3.7 68 290
floats-esbmc-regression/floor_nondet_true-unreach-call.i 0 14    9.2  150   420 3.6  0      5.2  2.9  110   270 10   5.6 120 310
floats-esbmc-regression/floor_true-unreach-call.i 2 4.4  2.5  42   280 3.4  0      5.9  3.2  93   270 6.9 3.6 100 300
floats-esbmc-regression/fmax_true-unreach-call.i 2 4.1  2.4  43   260 3.4  .016  6.1  3.3  74   270 5.6 3.0 71 290
floats-esbmc-regression/fmin_true-unreach-call.i 2 4.3  2.4  43   270 3.4  0      6.9  3.7  54   270 6.0 3.2 72 300
floats-esbmc-regression/fmod2_true-unreach-call.i -16 5.4  2.8  46   290 3.5  .0041 5.6  3.0  110   290 10   5.4 100 300
floats-esbmc-regression/fmod3_true-unreach-call.i -16 4.9  2.6  45   280 3.6  .0041 5.8  3.1  81   300 10   5.4 160 300
floats-esbmc-regression/fmod_true-unreach-call.i 2 4.2  2.5  42   270 3.4  .29   6.7  3.6  68   280 6.1 3.2 86 300
floats-esbmc-regression/isgreater_true-unreach-call.i 2 4.3  2.5  40   270 3.4  .0041 5.3  2.9  94   260 11   5.7 160 300
floats-esbmc-regression/isgreaterequal_true-unreach-call.i 2 4.2  2.4  43   270 3.4  0      6.4  3.4  76   270 11   5.7 110 300
floats-esbmc-regression/isless_true-unreach-call.i 2 4.2  2.4  41   270 3.4  0      6.7  3.6  70   270 11   5.9 220 300
floats-esbmc-regression/islessequal_true-unreach-call.i 2 4.4  2.4  39   270 3.4  0      5.7  3.0  110   280 11   5.7 180 310
floats-esbmc-regression/islessgreater_true-unreach-call.i 2 4.1  2.4  41   270 3.4  0      5.3  2.8  70   280 12   6.3 240 320
floats-esbmc-regression/isunordered_true-unreach-call.i 2 4.1  2.4  44   260 3.4  .016  6.2  3.4  75   280 10   5.5 110 300
floats-esbmc-regression/lrint_true-unreach-call.i 0 8.7  3.9  78   480 3.6  34      6.9  3.7  51   270 6.3 3.4 68 310
floats-esbmc-regression/modf_true-unreach-call.i 2 4.2  2.5  46   270 3.4  0      5.3  2.9  96   270 7.2 3.8 84 330
floats-esbmc-regression/nan_true-unreach-call.i 2 4.1  2.4  40   270 3.4  .0041 6.7  3.6  60   270 14   7.3 270 330
floats-esbmc-regression/nearbyint2_true-unreach-call.i 0 9.1  3.9  74   440 3.6  0      6.8  3.6  71   270 6.0 3.2 69 300
floats-esbmc-regression/nearbyint_true-unreach-call.i 0 11    4.7  91   470 3.6  0      9.5  5.0  70   310 6.4 3.4 90 290
floats-esbmc-regression/remainder_true-unreach-call.i 2 4.5  2.7  51   270 3.4  .016  6.6  3.6  85   270 7.8 4.2 82 310
floats-esbmc-regression/rint2_true-unreach-call.i 0 9.3  4.1  86   320 3.6  0      5.5  3.0  81   270 7.1 3.7 98 310
floats-esbmc-regression/rint_true-unreach-call.i 0 11    4.7  91   470 3.6  0      9.4  5.0  73   300 6.3 3.3 73 310
floats-esbmc-regression/round_nondet_true-unreach-call.i 0 17    12    170   440 3.6  0      6.3  3.4  66   270 11   5.7 150 300
floats-esbmc-regression/round_true-unreach-call.i 2 20    12    32   270 3.4  0      5.4  2.9  69   280 6.3 3.3 110 300
floats-esbmc-regression/rounding_functions_true-unreach-call.i 2 5.1  3.3  51   260 3.4  .016  7.2  3.9  87   270 6.2 3.3 98 300
floats-esbmc-regression/trunc_nondet_2_true-unreach-call.i 0 890    900    12000   97 2.5  0      9.2  4.9  83   330 10   5.7 170 300
floats-esbmc-regression/trunc_nondet_true-unreach-call.i 0 12    7.0  110   430 3.7  .020  5.3  2.9  110   270 11   5.6 140 310
floats-esbmc-regression/trunc_true-unreach-call.i 2 4.4  2.7  43   300 3.4  34      6.7  3.6  71   260 8.1 4.2 120 330
floats-esbmc-regression/Double_div_bad_false-unreach-call.i 0 890    900    10000   640 14    0      .63 .40 8.9 39 8.8 4.6 92 320
floats-esbmc-regression/Float_div_bad_false-unreach-call.i 0 890    900    7900   650 49    0      .73 .48 7.4 43 8.0 4.2 81 310
floats-esbmc-regression/digits_bad_for_false-unreach-call.i 1 24    22    230   270 4.3  0      6.1  3.3  130   290 98   71   890 3000
floats-esbmc-regression/digits_bad_while_false-unreach-call.i 1 26    23    210   280 4.4  0      6.3  3.4  110   300 97   85   1200 730
../../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 100 70000 70000 660000 89000 980 200     172 99 67 1600 5100   172 760 610 9900 23000   172 2500 2300   42000 28000   172 7100 6300 110000 63000  
    correct results 82 148 3800 3600 36000 25000 280 140     12 90 62 1400 4500   7 670 560 8500 18000   64 2200 2100   38000 20000   40 5300 4800 80000 33000  
        correct true 66 132 1500 1400 16000 22000 260 140     7 0 0 0 0   0 0 0 0 0   64 2200 2100   38000 20000   40 5300 4800 80000 33000  
        correct false 16 16 2300 2300 20000 3000 21 .45  5 90 62 1400 4500   7 670 560 8500 18000   0 0 0   0 0   0 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 3 -48 330 320 2900 830 10 .012 0 0 0 0 0   0 0 0 0 0   3 16 8.8 270 890   0 27 14 360 910  
        incorrect true 0
        incorrect false 3 -48 330 320 2900 830 10 .012 0 0 0 0 0   0 0 0 0 0   3 16 8.8 270 890   0 27 14 360 910  
score (172 tasks, max score: 314) 100
Run set sv-comp17.ReachSafety-Floats