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-11 15:09:43 CET [[ 2017-01-14 22:26:56 CET ]] [[ 2017-01-14 23:59:25 CET ]] [[ 2017-01-14 22:42:14 CET ]] [[ 2017-01-15 00:15:34 CET ]]
Run set sv-comp17.ReachSafety-Floats
Options -s falsi [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-11_1509.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     9400    470 .84 0   .51 .33 11   41 5.7 3.0 80 300
floats-cdfpl/newton_1_5_false-unreach-call.i 0 900     900     8300    480 .84 0   .54 .34 12   41 6.9 3.6 100 310
floats-cdfpl/newton_1_6_false-unreach-call.i 0 900     900     7400    440 .84 0   .71 .45 8.8 45 6.3 3.3 71 300
floats-cdfpl/newton_1_7_false-unreach-call.i 0 900     900     6700    460 .84 0   .50 .31 12   39 6.0 3.2 110 300
floats-cdfpl/newton_1_8_false-unreach-call.i 1 880     880     7700    460 .99 0   26    24    330   700 30   24   490 990
floats-cdfpl/newton_2_6_false-unreach-call.i 0 900     900     7200    760 .84 0   .61 .39 7.8 43 6.3 3.3 70 320
floats-cdfpl/newton_2_7_false-unreach-call.i 0 900     900     7300    760 .84 0   .49 .32 9.7 39 6.4 3.3 75 300
floats-cdfpl/newton_2_8_false-unreach-call.i 0 900     900     8000    760 .84 0   .52 .34 5.3 42 6.7 3.5 92 310
floats-cdfpl/newton_3_6_false-unreach-call.i 0 900     900     7800    1100 .84 0   .56 .34 12   40 5.9 3.2 110 300
floats-cdfpl/newton_3_7_false-unreach-call.i 0 900     900     8500    1100 .84 0   .67 .42 8.2 41 6.1 3.2 130 300
floats-cdfpl/newton_3_8_false-unreach-call.i 0 900     900     8700    1100 .84 0   .55 .36 13   42 5.7 3.0 100 290
floats-cdfpl/sine_1_false-unreach-call.i 1 170     170     1600    240 .84 0   4.2  2.4  48   270 29   22   370 890
floats-cdfpl/sine_2_false-unreach-call.i 1 92     92     710    190 .84 0   4.1  2.3  51   270 97   91   1200 3000
floats-cdfpl/sine_3_false-unreach-call.i 1 62     62     510    180 .84 0   3.9  2.2  34   270 93   87   840 3400
floats-cdfpl/square_1_false-unreach-call.i 1 540     540     5600    200 .84 0   3.7  2.0  51   290 46   40   690 980
floats-cdfpl/square_2_false-unreach-call.i 0 900     900     8000    350 .84 0   .54 .36 11   39 6.7 3.6 77 300
floats-cdfpl/square_3_false-unreach-call.i 0 900     900     7000    350 .84 0   .52 .35 8.3 41 5.7 3.1 89 300
floats-cdfpl/newton_1_1_true-unreach-call.i 0 900     900     7200    450 .84 0   .49 .31 8.4 39 5.5 2.9 110 290
floats-cdfpl/newton_1_2_true-unreach-call.i 0 900     900     6900    460 .84 0   .52 .33 9.5 39 7.0 3.7 130 320
floats-cdfpl/newton_1_3_true-unreach-call.i 0 900     900     6800    460 .84 0   .51 .33 9.5 41 6.6 3.5 150 320
floats-cdfpl/newton_2_1_true-unreach-call.i 0 900     900     7900    740 .84 0   .49 .32 11   40 6.4 3.4 130 300
floats-cdfpl/newton_2_2_true-unreach-call.i 0 900     900     6500    770 .84 0   .55 .34 10   40 5.6 3.0 95 300
floats-cdfpl/newton_2_3_true-unreach-call.i 0 900     900     8200    760 .84 0   .50 .32 9.7 41 5.6 3.0 110 300
floats-cdfpl/newton_2_4_true-unreach-call.i 0 900     900     7000    740 .84 0   .53 .35 12   39 5.9 3.1 120 300
floats-cdfpl/newton_2_5_true-unreach-call.i 0 900     900     8000    760 .84 0   .52 .34 12   41 5.9 3.1 130 300
floats-cdfpl/newton_3_1_true-unreach-call.i 0 900     900     7500    1100 .84 0   .52 .33 11   40 6.1 3.3 120 300
floats-cdfpl/newton_3_2_true-unreach-call.i 0 900     900     8300    1100 .84 0   .48 .32 13   39 6.3 3.3 120 300
floats-cdfpl/newton_3_3_true-unreach-call.i 0 900     900     6600    1000 .84 0   .50 .32 12   39 6.2 3.3 84 300
floats-cdfpl/newton_3_4_true-unreach-call.i 0 900     900     7500    940 .84 0   .53 .35 13   39 6.8 3.6 98 300
floats-cdfpl/newton_3_5_true-unreach-call.i 0 900     900     7200    1100 .84 0   .50 .33 8.1 40 6.2 3.3 120 290
floats-cdfpl/sine_4_true-unreach-call.i 0 900     900     8800    300 .84 0   .51 .33 9.0 41 5.9 3.1 88 310
floats-cdfpl/sine_5_true-unreach-call.i 0 900     900     8300    300 .84 0   .49 .32 12   39 6.1 3.2 110 300
floats-cdfpl/sine_6_true-unreach-call.i 0 900     900     8400    310 .84 0   .53 .34 12   40 5.9 3.2 110 300
floats-cdfpl/sine_7_true-unreach-call.i 0 900     900     7200    300 .84 0   .72 .45 6.4 43 5.9 3.1 100 290
floats-cdfpl/sine_8_true-unreach-call.i 0 900     900     7300    300 .84 0   .51 .33 11   41 6.3 3.3 120 290
floats-cdfpl/square_4_true-unreach-call.i 0 900     900     6700    250 .84 0   .51 .34 7.1 40 6.0 3.2 130 300
floats-cdfpl/square_5_true-unreach-call.i 0 900     900     6200    350 .84 0   .50 .32 11   40 6.3 3.3 130 300
floats-cdfpl/square_6_true-unreach-call.i 0 900     900     7500    350 .84 0   .48 .31 7.0 39 6.7 3.5 120 320
floats-cdfpl/square_7_true-unreach-call.i 0 900     900     8800    250 .84 0   .49 .31 7.4 39 6.3 3.3 140 300
floats-cdfpl/square_8_true-unreach-call.i 0 900     900     6200    200 .84 0   .51 .32 9.4 40 5.9 3.1 120 300
floats-cbmc-regression/float-div1_true-unreach-call.i 0 900     900     12000    3400 .84 0   .68 .44 8.5 44 5.9 3.2 110 290
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i 0 900     890     14000    420 .84 0   .49 .33 9.2 40 6.5 3.4 120 310
floats-cbmc-regression/float-no-simp1_true-unreach-call.i 0 900     830     12000    9500 .84 0   .50 .33 11   40 6.0 3.2 120 290
floats-cbmc-regression/float-no-simp2_true-unreach-call.i 0 900     900     9000    230 .84 0   .50 .32 10   39 6.2 3.3 130 300
floats-cbmc-regression/float-no-simp3_true-unreach-call.i 0 900     830     12000    9300 .84 0   .53 .36 9.5 43 6.2 3.3 130 300
floats-cbmc-regression/float-no-simp4_true-unreach-call.i 0 200     200     2600    15000 .84 0   .61 .41 6.2 40 6.2 3.3 120 310
floats-cbmc-regression/float-no-simp6_true-unreach-call.i 0 900     860     12000    7000 .84 0   .48 .31 7.5 40 6.5 3.4 120 320
floats-cbmc-regression/float-no-simp7_true-unreach-call.i 0 900     850     12000    11000 .84 0   .53 .35 12   42 5.9 3.2 120 300
floats-cbmc-regression/float-no-simp8_true-unreach-call.i 0 900     830     12000    5500 .84 0   .52 .32 9.2 40 7.2 3.9 89 290
floats-cbmc-regression/float-rounding1_true-unreach-call.i 0 520     520     6800    15000 .84 0   .57 .35 9.9 39 6.5 3.4 130 300
floats-cbmc-regression/float-to-double1_true-unreach-call.i 0 900     900     11000    1300 .84 0   .47 .31 9.7 40 5.7 3.1 110 300
floats-cbmc-regression/float-to-double2_true-unreach-call.i 0 900     830     13000    8800 .84 0   .52 .34 9.4 44 5.7 3.0 130 290
floats-cbmc-regression/float-zero-sum1_true-unreach-call.i 0 64     59     790    15000 .84 0   .53 .35 11   41 6.0 3.1 110 300
floats-cbmc-regression/float11_true-unreach-call.i 0 900     830     13000    3000 .84 0   .52 .33 11   40 6.1 3.2 120 300
floats-cbmc-regression/float12_true-unreach-call.i 0 900     900     11000    5400 .84 0   .56 .36 9.7 41 6.9 3.6 120 310
floats-cbmc-regression/float13_true-unreach-call.i 0 900     860     15000    5100 .84 0   .50 .32 9.8 41 6.1 3.2 130 290
floats-cbmc-regression/float14_true-unreach-call.i 0 900     860     11000    4700 .84 0   .49 .32 11   40 5.7 3.1 120 290
floats-cbmc-regression/float18_true-unreach-call.i 0 900     880     13000    3700 .84 0   .50 .33 10   40 5.8 3.1 120 290
floats-cbmc-regression/float19_true-unreach-call.i 0 900     900     14000    6200 .84 0   .48 .30 6.9 39 6.6 3.5 130 300
floats-cbmc-regression/float1_true-unreach-call.i 0 900     840     11000    7800 .84 0   .51 .33 4.6 40 6.2 3.2 110 300
floats-cbmc-regression/float20_true-unreach-call.i 0 900     900     8400    3200 .84 0   .48 .33 9.1 43 5.7 3.0 110 290
floats-cbmc-regression/float21_true-unreach-call.i 0 900     900     13000    1400 .84 0   .50 .32 13   40 6.6 3.5 130 310
floats-cbmc-regression/float22_true-unreach-call.i 0 .078 .078 .81 24 .84 0   .50 .34 4.2 39 6.0 3.2 120 300
floats-cbmc-regression/float2_true-unreach-call.i 0 900     840     12000    7600 .84 0   .55 .35 7.4 43 6.4 3.4 130 310
floats-cbmc-regression/float3_true-unreach-call.i 0 900     900     10000    7300 .84 0   .50 .34 4.0 40 5.7 3.1 110 290
floats-cbmc-regression/float4_true-unreach-call.i 0 900     900     9500    230 .84 0   .57 .38 7.8 40 6.2 3.3 110 310
floats-cbmc-regression/float5_true-unreach-call.i 0 900     900     11000    2300 .84 0   .49 .31 11   40 5.5 3.0 110 290
floats-cbmc-regression/float6_true-unreach-call.i 0 510     490     980    15000 .84 0   .54 .35 12   43 5.9 3.1 120 300
floats-cbmc-regression/float7_true-unreach-call.i 0 45     44     600    15000 .84 0   .55 .37 11   44 5.8 3.1 120 300
floats-cbmc-regression/float8_true-unreach-call.i 0 64     59     870    15000 .84 0   .50 .32 8.4 40 6.2 3.3 120 300
floats-cbmc-regression/float_lib1_true-unreach-call.i 0 900     850     12000    1000 .99 0   .48 .32 13   41 6.4 3.4 120 300
floats-cbmc-regression/float_lib2_true-unreach-call.i 0 900     840     13000    1300 .84 0   .51 .33 12   39 6.5 3.4 93 320
float-benchs/cast_float_ptr_false-unreach-call.c 1 .092 .091 1.1  23 .84 0   2.6  1.5  44   160 6.0 3.2 96 300
float-benchs/cast_union_loose_false-unreach-call.c 1 .21  .21  2.4  27 .84 0   3.8  2.1  56   270 6.2 3.3 100 300
float-benchs/cast_union_tight_false-unreach-call.c 1 .89  .89  10    37 .84 0   2.5  1.4  52   160 6.0 3.2 99 300
float-benchs/float_int_inv_square_false-unreach-call.c 1 .42  .42  4.4  33 .84 0   3.9  2.2  52   280 14   7.8 250 320
float-benchs/inv_square_false-unreach-call.c 1 .19  .19  1.7  23 .84 0   3.7  2.2  60   290 13   7.2 220 330
float-benchs/nan_double_false-unreach-call.c 1 .10  .10  .72 23 .84 0   3.9  2.2  28   270 8.8 4.7 69 310
float-benchs/nan_float_false-unreach-call.c 1 .098 .098 .77 23 .84 0   3.5  2.0  64   270 8.9 4.6 74 310
float-benchs/sin_interpolated_index_false-unreach-call.c 1 260     260     2100    880 .84 0   4.1  2.3  65   270 97   90   1100 3400
float-benchs/sqrt_poly2_false-unreach-call.c 1 340     340     2700    340 .84 0   2.5  1.4  40   170 9.8 5.2 68 300
float-benchs/Muller_Kahan_true-unreach-call.c 0 900     850     13000    2100 .84 0   .54 .34 9.6 40 6.3 3.4 110 300
float-benchs/Rump_double_true-unreach-call.c 0 900     840     11000    3300 .84 0   .51 .33 6.6 40 6.0 3.1 130 300
float-benchs/Rump_float_true-unreach-call.c 0 900     830     13000    3800 .84 0   .62 .41 5.2 41 6.1 3.2 120 300
float-benchs/addsub_double_exact_true-unreach-call.c 0 900     850     14000    9100 .84 0   .50 .33 12   41 5.8 3.1 99 300
float-benchs/addsub_float_exact_true-unreach-call.c 0 900     850     11000    9400 .84 0   .51 .33 8.9 40 5.7 3.0 130 300
float-benchs/addsub_float_inexact_true-unreach-call.c 0 900     850     12000    9500 .84 0   .49 .31 9.0 39 5.1 2.8 100 280
float-benchs/arctan_Pade_true-unreach-call.c 0 900     900     7300    1100 .84 0   .52 .32 12   40 6.4 3.4 130 310
float-benchs/bary_diverge_true-unreach-call.c 0 900     900     11000    2000 .84 0   .51 .33 7.4 40 5.4 2.9 100 290
float-benchs/cast_float_union_true-unreach-call.c 0 900     860     12000    12000 .84 0   .48 .32 6.8 40 6.2 3.3 110 300
float-benchs/cos_polynomial_true-unreach-call.c 0 900     900     8300    610 .84 0   .61 .40 7.7 41 6.1 3.2 130 300
float-benchs/divmul_buf_diverge_true-unreach-call.c 0 900     890     11000    490 .84 0   .69 .44 9.9 40 6.0 3.2 100 300
float-benchs/divmul_diverge_true-unreach-call.c 0 900     890     12000    480 .84 0   .58 .36 9.1 41 5.7 3.0 100 300
float-benchs/drift_tenth_true-unreach-call.c 0 900     820     11000    6900 .84 0   .47 .30 4.5 39 6.5 3.4 120 300
float-benchs/exp_loop_true-unreach-call.c 0 900     900     12000    1400 .96 0   .50 .32 4.7 41 7.4 3.8 150 320
float-benchs/feedback_diverge_true-unreach-call.c 0 900     890     11000    520 .84 0   .61 .37 8.1 39 5.9 3.1 120 300
float-benchs/filter1_true-unreach-call.c 0 900     900     8500    260 .84 0   .52 .33 11   42 6.2 3.3 120 310
float-benchs/filter2_alt_true-unreach-call.c 0 900     900     8000    250 .84 0   .58 .37 14   44 5.6 3.0 110 300
float-benchs/filter2_iterated_true-unreach-call.c 0 540     540     7000    15000 .84 0   .50 .33 11   40 5.3 2.9 80 290
float-benchs/filter2_reinit_true-unreach-call.c 0 900     900     7200    240 .84 0   .50 .32 11   39 6.0 3.2 110 290
float-benchs/filter2_set_true-unreach-call.c 0 900     900     8700    530 .84 0   .57 .37 12   43 6.0 3.2 120 300
float-benchs/filter2_true-unreach-call.c 0 900     900     9300    380 .84 0   .53 .35 10   42 6.2 3.2 110 300
float-benchs/filter_iir_true-unreach-call.c 0 900     900     8100    420 .84 0   .63 .40 6.0 39 6.2 3.3 110 300
float-benchs/float_double_true-unreach-call.c 0 900     840     11000    9900 .84 0   .49 .31 9.9 39 6.2 3.2 130 300
float-benchs/image_filter_true-unreach-call.c 0 900     900     11000    2200 .84 0   .52 .33 12   39 6.0 3.2 120 310
float-benchs/interpolation2_true-unreach-call.c 0 900     900     9400    270 .84 0   .52 .34 13   40 6.2 3.3 120 310
float-benchs/interpolation_true-unreach-call.c 0 900     900     9100    1000 .84 0   .53 .33 9.6 40 6.1 3.3 120 300
float-benchs/inv_sqrt_Quake_true-unreach-call.c 0 900     900     11000    330 .84 0   .58 .38 6.5 42 6.1 3.2 110 300
float-benchs/inv_square_int_true-unreach-call.c 0 900     900     6500    2500 .84 0   .49 .32 11   40 5.4 2.9 110 290
float-benchs/inv_square_true-unreach-call.c 0 900     900     12000    7500 .99 0   .54 .34 11   42 5.9 3.2 110 300
float-benchs/loop_true-unreach-call.c 0 900     840     12000    2700 .84 0   .53 .34 9.4 42 5.8 3.1 120 300
float-benchs/mea8000_true-unreach-call.c 0 900     900     12000    1100 .84 0   .63 .40 9.5 43 5.8 3.2 130 290
float-benchs/nan_double_range_true-unreach-call.c 0 57     52     630    15000 .84 0   .49 .32 12   39 6.4 3.3 90 310
float-benchs/nan_float_range_true-unreach-call.c 0 79     78     1100    15000 .84 0   .51 .32 10   41 5.9 3.2 130 290
float-benchs/rlim_exit_true-unreach-call.c 0 900     900     9200    590 .84 0   .49 .32 11   39 5.7 3.0 110 290
float-benchs/rlim_invariant_true-unreach-call.c 0 900     900     10000    170 .84 0   .52 .35 7.0 40 5.9 3.1 84 300
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call.c 0 900     900     5000    2200 .84 0   .50 .32 9.0 39 6.0 3.2 110 300
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call.c 0 900     900     7000    2400 .84 0   .52 .34 8.5 40 6.1 3.2 130 300
float-benchs/sin_interpolated_index_true-unreach-call.c 0 900     900     7800    930 .84 0   .49 .32 8.5 39 5.8 3.1 100 300
float-benchs/sin_interpolated_negation_true-unreach-call.c 0 900     900     5900    2100 .84 0   .52 .33 11   40 6.0 3.2 99 290
float-benchs/sin_interpolated_smallrange_true-unreach-call.c 0 900     900     7100    2200 .84 0   .55 .35 13   44 6.0 3.2 120 300
float-benchs/sqrt_Householder_constant_true-unreach-call.c 0 900     880     14000    1600 .84 0   .54 .34 12   42 5.7 3.0 120 300
float-benchs/sqrt_Householder_interval_true-unreach-call.c 0 900     900     7900    770 .84 0   .49 .32 11   40 5.8 3.1 87 310
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c 0 900     900     3200    1200 .98 0   .48 .32 5.9 39 7.5 3.9 140 340
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c 0 900     900     8700    1100 .84 0   .52 .32 7.9 42 5.7 3.0 110 290
float-benchs/sqrt_biNewton_pseudoconstant_true-unreach-call.c 0 900     900     7400    1400 .84 0   .55 .35 14   43 5.7 3.0 120 290
float-benchs/sqrt_poly_true-unreach-call.c 0 900     900     10000    490 .84 0   .67 .43 6.4 42 5.7 3.1 100 290
float-benchs/water_pid_true-unreach-call.c 0 900     880     12000    5200 .84 0   .51 .33 9.7 40 6.2 3.3 130 300
float-benchs/zonotope_2_true-unreach-call.c 0 900     880     12000    6000 .84 0   .50 .32 11   39 6.0 3.2 85 300
float-benchs/zonotope_3_true-unreach-call.c 0 900     890     11000    950 .84 0   .62 .39 7.9 40 5.6 3.0 100 290
float-benchs/zonotope_loose_true-unreach-call.c 0 900     900     10000    1200 .84 0   .63 .39 10   44 5.7 3.0 120 290
float-benchs/zonotope_tight_true-unreach-call.c 0 900     900     8300    1000 .84 0   .51 .32 8.4 42 6.6 3.4 130 300
floats-esbmc-regression/Double_div_true-unreach-call.i 0 900     850     11000    2400 .84 0   .49 .33 6.4 42 5.8 3.1 97 300
floats-esbmc-regression/Float_div_true-unreach-call.i 0 900     790     12000    4700 .84 0   .50 .33 4.1 42 6.0 3.2 110 300
floats-esbmc-regression/ceil_nondet_true-unreach-call.i 0 900     900     11000    4800 .84 0   .50 .31 12   40 6.2 3.3 140 300
floats-esbmc-regression/ceil_true-unreach-call.i 0 150     140     1600    15000 .84 0   .51 .32 8.6 40 6.1 3.2 120 300
floats-esbmc-regression/copysign_true-unreach-call.i 0 900     850     10000    8700 .84 0   .51 .33 10   41 6.4 3.4 130 290
floats-esbmc-regression/digits_for_true-unreach-call.i 0 900     870     13000    1800 .84 0   .49 .31 10   40 5.9 3.1 130 290
floats-esbmc-regression/digits_while_true-unreach-call.i 0 900     870     12000    1800 .84 0   .52 .33 10   41 6.8 3.5 120 310
floats-esbmc-regression/fabs_true-unreach-call.i 0 900     830     11000    9400 .84 0   .47 .29 4.0 39 6.2 3.3 130 310
floats-esbmc-regression/fdim_true-unreach-call.i 0 900     840     12000    10000 .84 0   .55 .35 12   44 6.2 3.3 110 300
floats-esbmc-regression/floor_nondet_true-unreach-call.i 0 900     900     11000    6700 .84 0   .50 .32 12   40 6.0 3.2 120 290
floats-esbmc-regression/floor_true-unreach-call.i 0 150     140     2100    15000 .84 0   .51 .32 11   40 6.3 3.3 110 310
floats-esbmc-regression/fmax_true-unreach-call.i 0 900     840     14000    11000 .84 0   .50 .33 12   40 6.4 3.4 120 310
floats-esbmc-regression/fmin_true-unreach-call.i 0 900     840     12000    11000 .84 0   .62 .40 9.7 40 5.7 3.1 120 290
floats-esbmc-regression/fmod2_true-unreach-call.i 0 1.9   1.8   26    15000 .84 0   .55 .35 11   40 6.7 3.5 120 300
floats-esbmc-regression/fmod3_true-unreach-call.i 0 1.9   1.8   27    15000 .84 0   .54 .35 4.4 40 5.9 3.2 110 290
floats-esbmc-regression/fmod_true-unreach-call.i 0 900     860     11000    7100 .84 0   .51 .33 10   41 6.2 3.2 120 300
floats-esbmc-regression/isgreater_true-unreach-call.i 0 900     850     12000    15000 .84 0   .50 .33 10   42 5.8 3.1 130 290
floats-esbmc-regression/isgreaterequal_true-unreach-call.i 0 900     810     12000    14000 .84 0   .49 .32 12   39 6.5 3.4 120 310
floats-esbmc-regression/isless_true-unreach-call.i 0 900     850     11000    15000 .84 0   .56 .35 12   42 6.0 3.3 120 290
floats-esbmc-regression/islessequal_true-unreach-call.i 0 900     810     11000    14000 .84 0   .52 .34 12   42 5.9 3.1 120 290
floats-esbmc-regression/islessgreater_true-unreach-call.i 0 900     850     12000    13000 .84 0   .49 .32 12   40 7.2 3.8 130 330
floats-esbmc-regression/isunordered_true-unreach-call.i 0 900     840     11000    13000 .99 0   .50 .32 11   40 6.2 3.3 130 300
floats-esbmc-regression/lrint_true-unreach-call.i 0 7.6   7.4   21    15000 .84 0   .51 .34 12   40 5.6 3.0 110 290
floats-esbmc-regression/modf_true-unreach-call.i 0 140     130     1800    15000 .84 0   .47 .31 6.8 39 7.5 3.9 100 310
floats-esbmc-regression/nan_true-unreach-call.i 0 900     870     11000    11000 .84 0   .51 .33 13   40 6.0 3.2 120 290
floats-esbmc-regression/nearbyint2_true-unreach-call.i 0 190     180     2200    15000 .84 0   .53 .34 6.5 41 6.9 3.6 130 320
floats-esbmc-regression/nearbyint_true-unreach-call.i 0 240     230     2900    15000 .84 0   .53 .35 5.8 42 5.9 3.2 110 300
floats-esbmc-regression/remainder_true-unreach-call.i 0 2.0   1.9   24    15000 .84 0   .51 .32 10   39 6.4 3.4 100 310
floats-esbmc-regression/rint2_true-unreach-call.i 0 220     210     2700    15000 .84 0   .52 .32 10   40 5.6 3.0 110 290
floats-esbmc-regression/rint_true-unreach-call.i 0 260     250     3600    15000 .84 0   .57 .37 9.5 43 6.6 3.5 110 310
floats-esbmc-regression/round_nondet_true-unreach-call.i 0 900     900     10000    3200 .84 0   .57 .35 6.6 40 5.9 3.2 120 300
floats-esbmc-regression/round_true-unreach-call.i 0 2.3   2.3   33    15000 .84 0   .58 .37 6.9 40 6.7 3.5 100 310
floats-esbmc-regression/rounding_functions_true-unreach-call.i 0 440     430     5400    15000 .84 0   .48 .32 7.0 40 6.7 3.6 130 320
floats-esbmc-regression/trunc_nondet_2_true-unreach-call.i 0 900     900     11000    3200 .84 0   .51 .33 12   40 6.1 3.2 110 300
floats-esbmc-regression/trunc_nondet_true-unreach-call.i 0 900     900     11000    9600 .84 0   .55 .35 11   43 6.2 3.2 120 300
floats-esbmc-regression/trunc_true-unreach-call.i 0 160     140     1600    15000 .84 0   .52 .34 11   39 6.4 3.4 130 300
floats-esbmc-regression/Double_div_bad_false-unreach-call.i 1 61     57     860    320 .84 0   67    61    670   7000 6.7 3.6 130 320
floats-esbmc-regression/Float_div_bad_false-unreach-call.i 1 .84  .76  12    25 .84 0   28    22    420   2000 6.8 3.6 100 310
floats-esbmc-regression/digits_bad_for_false-unreach-call.i 1 .21  .21  2.8  23 .84 0   6.2  3.4  77   290 15   8.4 180 300
floats-esbmc-regression/digits_bad_while_false-unreach-call.i 1 .23  .22  4.9  23 .84 0   6.6  3.5  74   300 12   6.8 200 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 18 120000 120000 1400000 800000 150 0   172 190 140 2300 14000 172 580 450 7400 20000 172 75 48 1400 5800   172 870 460 16000 43000  
    correct results 18 18 2400 2400 22000 3100 15 0   13 180 140 2200 14000 11 500 420 6300 16000 0 0 0 0 0   0 0 0 0 0  
        correct true 0
        correct false 18 18 2400 2400 22000 3100 15 0   5 180 140 2200 14000 7 500 420 6300 16000 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) 18
Run set sv-comp17.ReachSafety-Floats