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