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