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