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 11:31:18 CET [[ 2017-01-14 22:07:55 CET ]] [[ 2017-01-14 22:45:22 CET ]] [[ 2017-01-14 22:11:49 CET ]] [[ 2017-01-14 23:12:14 CET ]]
Run set sv-comp17.ReachSafety-Floats
Options -s fixed [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-11_1131.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 35    35    310   200 2.5 0      timeout 92   91   1700 2500 timeout 97   91   1100 3600 - -
floats-cdfpl/newton_1_5_false-unreach-call.i false(unreach-call) 1 wit inspect 19    19    110   180 2.5 0      false(unreach-call) 77   74   1200 620 false(unreach-call) 67   61   870 2200 - -
floats-cdfpl/newton_1_6_false-unreach-call.i false(unreach-call) 1 wit inspect 8.7  8.7  81   180 2.5 0      false(unreach-call) 19   17   520 540 false(unreach-call) 57   51   820 1700 - -
floats-cdfpl/newton_1_7_false-unreach-call.i false(unreach-call) 1 wit inspect 8.2  8.2  77   180 2.5 0      false(unreach-call) 34   32   1200 1100 timeout (false(unreach-call)) 95   88   610 2000 - -
floats-cdfpl/newton_1_8_false-unreach-call.i false(unreach-call) 1 wit inspect 14    14    130   190 2.5 0      false(unreach-call) 24   23   750 700 false(unreach-call) 30   24   290 990 - -
floats-cdfpl/newton_2_6_false-unreach-call.i false(unreach-call) 1 wit inspect 26    26    220   360 2.5 0      timeout 92   91   2700 2400 timeout 97   91   750 3400 - -
floats-cdfpl/newton_2_7_false-unreach-call.i false(unreach-call) 1 wit inspect 17    17    170   350 2.5 .0041 false(unreach-call) 85   83   2400 1500 timeout 97   91   1300 2600 - -
floats-cdfpl/newton_2_8_false-unreach-call.i false(unreach-call) 1 wit inspect 11    11    130   350 2.5 0      false(unreach-call) 25   24   650 720 timeout 97   91   1400 2200 - -
floats-cdfpl/newton_3_6_false-unreach-call.i false(unreach-call) 1 wit inspect 24    24    230   530 2.5 0      timeout 93   91   1700 2600 timeout 97   91   2100 3700 - -
floats-cdfpl/newton_3_7_false-unreach-call.i false(unreach-call) 1 wit inspect 72    72    540   540 2.5 0      timeout 92   90   2000 1800 timeout 97   91   1200 3900 - -
floats-cdfpl/newton_3_8_false-unreach-call.i false(unreach-call) 1 wit inspect 56    56    560   530 2.5 0      false(unreach-call) 81   79   2400 2200 false(unreach-call) 53   47   530 1400 - -
floats-cdfpl/sine_1_false-unreach-call.i false(unreach-call) 1 wit inspect 4.9  4.9  53   120 2.5 0      true 4.2 2.4 44 280 false(unreach-call) 27   22   420 900 - -
floats-cdfpl/sine_2_false-unreach-call.i false(unreach-call) 1 wit inspect 16    16    170   130 2.5 0      true 4.0 2.3 46 270 timeout 97   91   2100 3900 - -
floats-cdfpl/sine_3_false-unreach-call.i false(unreach-call) 1 wit inspect 10    10    95   130 2.5 0      true 3.3 1.8 64 270 timeout 97   91   1200 3000 - -
floats-cdfpl/square_1_false-unreach-call.i false(unreach-call) 1 wit inspect 7.2  7.2  72   120 2.5 0      true 3.4 1.9 65 270 false(unreach-call) 42   37   630 970 - -
floats-cdfpl/square_2_false-unreach-call.i false(unreach-call) 1 wit inspect 6.3  6.3  76   120 2.5 0      true 3.1 1.8 52 270 false(unreach-call) 83   77   1500 1800 - -
floats-cdfpl/square_3_false-unreach-call.i false(unreach-call) 1 wit inspect 5.7  5.7  81   120 2.5 0      true 3.8 2.2 56 270 timeout 97   91   1600 2500 - -
floats-cdfpl/newton_1_1_true-unreach-call.i true 2 wit inspect 39    40    370   200 2.7 0      - - timeout 900    900    14000   670 out of memory 250   240   3300 7000
floats-cdfpl/newton_1_2_true-unreach-call.i true 2 wit inspect 45    45    480   210 2.5 0      - - timeout 900    900    15000   550 out of memory 230   220   2400 7000
floats-cdfpl/newton_1_3_true-unreach-call.i true 2 wit inspect 47    47    530   200 2.5 0      - - timeout 900    900    16000   510 out of memory 200   190   1600 7000
floats-cdfpl/newton_2_1_true-unreach-call.i true 2 wit inspect 89    89    730   390 2.5 .0041 - - timeout 900    900    13000   530 out of memory 240   230   2600 7000
floats-cdfpl/newton_2_2_true-unreach-call.i true 2 wit inspect 150    150    1500   440 2.5 0      - - timeout 900    900    15000   510 out of memory 230   230   3900 7000
floats-cdfpl/newton_2_3_true-unreach-call.i true 2 wit inspect 140    140    960   420 2.5 0      - - timeout 900    900    15000   480 out of memory 230   230   2700 7000
floats-cdfpl/newton_2_4_true-unreach-call.i true 2 wit inspect 130    130    1000   410 2.5 .0041 - - timeout 900    900    13000   540 out of memory 220   210   2000 7000
floats-cdfpl/newton_2_5_true-unreach-call.i true 2 wit inspect 250    250    2000   430 2.5 0      - - timeout 900    900    16000   750 out of memory 250   240   1700 7000
floats-cdfpl/newton_3_1_true-unreach-call.i true 2 wit inspect 390    390    3000   680 2.5 0      - - timeout 900    900    17000   870 out of memory 200   190   2900 7000
floats-cdfpl/newton_3_2_true-unreach-call.i true 2 wit inspect 370    370    2700   660 2.5 0      - - timeout 900    900    13000   570 out of memory 190   180   1600 7000
floats-cdfpl/newton_3_3_true-unreach-call.i true 2 wit inspect 350    350    2900   660 2.5 0      - - timeout 900    900    11000   710 out of memory 240   230   3400 7000
floats-cdfpl/newton_3_4_true-unreach-call.i true 2 wit inspect 360    360    2500   660 2.5 0      - - timeout 900    900    19000   830 out of memory 190   190   2800 7000
floats-cdfpl/newton_3_5_true-unreach-call.i true 2 wit inspect 310    310    2400   640 2.5 0      - - timeout 900    900    14000   820 out of memory 210   200   2700 7000
floats-cdfpl/sine_4_true-unreach-call.i true 2 wit inspect 290    290    2200   180 2.5 0      - - timeout 900    900    13000   560 out of memory 210   200   1800 7000
floats-cdfpl/sine_5_true-unreach-call.i true 2 wit inspect 18    18    210   130 2.5 0      - - timeout 900    900    13000   520 out of memory 250   240   3200 7000
floats-cdfpl/sine_6_true-unreach-call.i true 2 wit inspect 18    18    180   130 2.5 0      - - timeout 900    900    16000   660 out of memory 190   190   1800 7000
floats-cdfpl/sine_7_true-unreach-call.i true 2 wit inspect 19    19    200   130 2.5 0      - - timeout 900    900    12000   440 out of memory 200   190   2300 7000
floats-cdfpl/sine_8_true-unreach-call.i true 2 wit inspect 14    14    150   130 2.5 0      - - timeout 900    900    13000   530 out of memory 230   220   3900 7000
floats-cdfpl/square_4_true-unreach-call.i true 2 wit inspect 170    170    1300   160 2.5 0      - - timeout 900    900    18000   580 out of memory 220   220   3300 7000
floats-cdfpl/square_5_true-unreach-call.i true 2 wit inspect 59    59    510   140 2.5 0      - - true 560    560    9000   510 out of memory 250   240   3000 7000
floats-cdfpl/square_6_true-unreach-call.i true 2 wit inspect 21    21    230   120 2.5 0      - - true 890    890    15000   610 out of memory 310   300   3900 7000
floats-cdfpl/square_7_true-unreach-call.i true 2 wit inspect 43    43    390   130 2.5 0      - - true 340    340    5200   500 out of memory 290   280   4100 7000
floats-cdfpl/square_8_true-unreach-call.i true 2 wit inspect 7.5  7.5  87   120 2.7 0      - - true 28    27    590   350 out of memory 250   250   4000 7000
floats-cbmc-regression/float-div1_true-unreach-call.i true 2 wit inspect 2.1  2.1  24   110 2.5 0      - - true 6.6  3.8  99   340 true 80   73   1100 700
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i true 2 wit inspect .36 .36 4.4 34 1.7 0      - - true 9.7  6.7  92   660 true 33   22   380 720
floats-cbmc-regression/float-no-simp1_true-unreach-call.i true 2 wit inspect .14 .14 1.7 23 1.8 0      - - true 4.1  2.3  39   260 true 13   6.8 100 320
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true 2 wit inspect 3.7  3.7  53   72 2.5 0      - - true 27    24    380   320 true 57   51   1100 470
floats-cbmc-regression/float-no-simp3_true-unreach-call.i true 2 wit inspect .14 .14 1.4 23 1.7 0      - - true 3.5  2.0  45   260 true 13   6.7 150 300
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true 2 wit inspect .45 .45 4.7 35 2.5 .16   - - true 7.1  3.8  74   280 true 25   15   580 520
floats-cbmc-regression/float-no-simp6_true-unreach-call.i true 2 wit inspect .14 .14 1.5 23 1.7 0      - - true 3.9  2.2  35   260 true 13   7.0 150 310
floats-cbmc-regression/float-no-simp7_true-unreach-call.i true 2 wit inspect .16 .16 1.4 23 1.7 0      - - true 4.0  2.3  35   260 true 13   6.9 270 310
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true 2 wit inspect .23 .23 3.0 27 1.7 0      - - true 5.8  3.1  64   270 true 12   6.8 180 310
floats-cbmc-regression/float-rounding1_true-unreach-call.i true 2 wit inspect .43 .43 4.5 34 2.5 0      - - error 6.1  3.3  78   270 unknown 6.0 3.2 70 300
floats-cbmc-regression/float-to-double1_true-unreach-call.i true 2 wit inspect .56 .56 6.4 38 2.6 0      - - true 6.8  3.7  67   280 true 220   220   3600 470
floats-cbmc-regression/float-to-double2_true-unreach-call.i true 2 wit inspect .14 .14 1.4 23 1.7 0      - - true 3.6  2.0  39   260 true 12   6.3 120 320
floats-cbmc-regression/float-zero-sum1_true-unreach-call.i true 2 wit inspect .19 .19 2.3 24 2.5 0      - - true 4.1  2.3  45   260 unknown 6.4 3.5 100 300
floats-cbmc-regression/float11_true-unreach-call.i true 2 wit inspect .16 .16 2.3 24 1.7 0      - - true 4.1  2.3  52   260 true 13   7.0 140 320
floats-cbmc-regression/float12_true-unreach-call.i true 2 wit inspect .28 .28 3.4 26 2.5 0      - - true 4.1  2.3  63   260 true 21   15   480 320
floats-cbmc-regression/float13_true-unreach-call.i true 2 wit inspect .14 .14 1.5 23 1.7 .0082 - - true 4.5  2.5  51   260 true 14   7.3 220 330
floats-cbmc-regression/float14_true-unreach-call.i true 2 wit inspect .23 .23 2.6 27 1.7 0      - - true 6.3  3.4  75   270 true 13   7.5 200 290
floats-cbmc-regression/float18_true-unreach-call.i true 2 wit inspect .52 .52 5.4 39 1.8 0      - - true 30    25    410   440 unknown 6.3 3.4 92 300
floats-cbmc-regression/float19_true-unreach-call.i true 2 wit inspect .35 .35 3.9 26 2.5 0      - - true 5.2  2.8  83   280 true 13   7.6 170 300
floats-cbmc-regression/float1_true-unreach-call.i true 2 wit inspect .13 .13 1.7 23 1.7 0      - - true 3.8  2.1  65   270 true 12   6.7 160 310
floats-cbmc-regression/float20_true-unreach-call.i true 2 wit inspect .60 .60 7.8 46 2.5 0      - - true 3.7  2.0  64   260 true 26   20   540 410
floats-cbmc-regression/float21_true-unreach-call.i true 2 wit inspect .53 .53 5.4 39 2.5 0      - - true 6.8  3.8  110   310 true 72   64   990 630
floats-cbmc-regression/float22_true-unreach-call.i true 2 wit inspect .45 .44 5.1 36 2.5 .0082 - - false(unreach-call) 7.0  3.8  74   290 unknown 15   8.0 170 330
floats-cbmc-regression/float2_true-unreach-call.i true 2 wit inspect .15 .15 1.4 23 1.7 0      - - true 4.3  2.4  44   260 true 12   6.7 150 310
floats-cbmc-regression/float3_true-unreach-call.i true 2 wit inspect .67 .67 7.9 50 2.5 0      - - true 4.4  2.6  57   280 true 20   14   390 340
floats-cbmc-regression/float4_true-unreach-call.i true 2 wit inspect 14    14    160   110 2.5 0      - - true 66    63    1000   340 true 94   87   1600 530
floats-cbmc-regression/float5_true-unreach-call.i true 2 wit inspect .33 .33 3.9 26 2.5 0      - - true 4.5  2.6  55   270 true 34   28   930 320
floats-cbmc-regression/float6_true-unreach-call.i true 2 wit inspect .24 .24 3.0 24 2.5 0      - - true 4.7  2.6  68   270 true 16   8.5 140 310
floats-cbmc-regression/float7_true-unreach-call.i true 2 wit inspect .20 .20 2.1 23 2.5 0      - - true 3.8  2.2  39   250 unknown 7.6 4.0 71 310
floats-cbmc-regression/float8_true-unreach-call.i true 2 wit inspect 1.1  1.1  13   43 2.5 0      - - true 6.0  3.4  70   310 true 14   7.6 240 310
floats-cbmc-regression/float_lib1_true-unreach-call.i true 2 wit inspect .28 .28 3.3 28 1.7 0      - - true 6.3  3.4  83   270 error 11   6.1 170 300
floats-cbmc-regression/float_lib2_true-unreach-call.i true 2 wit inspect .25 .25 2.9 27 1.7 0      - - true 6.1  3.3  84   270 true 16   8.9 120 450
float-benchs/cast_float_ptr_false-unreach-call.c false(unreach-call) 1 wit inspect .34 .34 4.1 32 2.5 0      assertion 2.5 1.4 38 170 unknown 6.1 3.2 100 310 - -
float-benchs/cast_union_loose_false-unreach-call.c false(unreach-call) 1 wit inspect .56 .56 6.0 43 2.5 0      true 4.3 2.4 48 270 unknown 6.2 3.3 99 300 - -
float-benchs/cast_union_tight_false-unreach-call.c false(unreach-call) 1 wit inspect .61 .61 6.9 45 2.5 0      assertion 2.5 1.5 34 160 unknown 6.9 3.6 120 320 - -
float-benchs/float_int_inv_square_false-unreach-call.c false(unreach-call) 1 wit inspect .40 .40 4.8 35 2.6 0      false(unreach-call) 3.7 2.2 69 270 false(unreach-call) 12   6.7 120 320 - -
float-benchs/inv_square_false-unreach-call.c false(unreach-call) 1 wit inspect .35 .35 3.4 31 2.5 0      true 4.2 2.5 78 290 false(unreach-call) 12   6.8 200 310 - -
float-benchs/nan_double_false-unreach-call.c false(unreach-call) 1 wit inspect .19 .19 2.2 25 2.5 0      false(unreach-call) 3.9 2.2 67 280 false(unreach-call) 6.9 3.7 100 320 - -
float-benchs/nan_float_false-unreach-call.c false(unreach-call) 1 wit inspect .20 .20 2.3 25 2.5 0      false(unreach-call) 4.7 2.6 46 270 false(unreach-call) 7.3 3.8 130 310 - -
float-benchs/sin_interpolated_index_false-unreach-call.c false(unreach-call) 1 wit inspect 8.4  8.4  94   320 2.5 0      assertion 3.2 1.8 40 170 timeout 97   90   2300 3500 - -
float-benchs/sqrt_poly2_false-unreach-call.c false(unreach-call) 1 wit inspect 7.9  7.9  78   270 2.5 0      assertion 2.7 1.5 52 170 error 9.9 5.3 120 310 - -
float-benchs/Muller_Kahan_true-unreach-call.c true 2 wit inspect .18 .18 1.8 23 1.7 0      - - timeout 900    900    13000   2700 timeout 960   910   13000 6800
float-benchs/Rump_double_true-unreach-call.c true 2 wit inspect .15 .15 1.4 23 1.7 0      - - true 4.1  2.3  50   260 true 24   17   540 800
float-benchs/Rump_float_true-unreach-call.c true 2 wit inspect .13 .13 1.4 24 1.7 0      - - true 4.0  2.2  47   260 true 14   8.5 120 380
float-benchs/addsub_double_exact_true-unreach-call.c true 2 wit inspect .13 .13 1.5 23 1.7 0      - - true 4.5  2.5  45   260 true 14   7.5 180 320
float-benchs/addsub_float_exact_true-unreach-call.c true 2 wit inspect .13 .13 1.5 23 1.7 0      - - true 3.9  2.2  49   260 true 14   7.3 190 320
float-benchs/addsub_float_inexact_true-unreach-call.c true 2 wit inspect .12 .12 1.5 23 1.7 0      - - true 3.2  1.8  45   260 true 13   7.0 200 320
float-benchs/arctan_Pade_true-unreach-call.c true 2 wit inspect 96    96    610   1200 2.5 0      - - true 14    12    260   510 error 37   32   620 1200
float-benchs/bary_diverge_true-unreach-call.c true 2 wit inspect 13    13    140   3500 2.5 .0082 - - timeout 900    900    15000   1200 timeout 960   950   19000 840
float-benchs/cast_float_union_true-unreach-call.c true 2 wit inspect .16 .16 1.4 23 1.7 0      - - true 4.1  2.3  49   260 error 11   6.1 140 300
float-benchs/cos_polynomial_true-unreach-call.c true 2 wit inspect 36    36    300   550 2.5 0      - - timeout 900    900    16000   1200 out of memory 320   310   6400 7000
float-benchs/divmul_buf_diverge_true-unreach-call.c true 2 wit inspect 11    11    120   2700 2.5 0      - - timeout 900    900    13000   1700 timeout 960   820   15000 4800
float-benchs/divmul_diverge_true-unreach-call.c true 2 wit inspect 11    10    120   3700 2.5 0      - - timeout 900    900    13000   2100 timeout 960   810   15000 4800
float-benchs/drift_tenth_true-unreach-call.c true 2 wit inspect .17 .17 1.5 23 1.7 0      - - true 13    10    240   340 error 130   120   1500 600
float-benchs/exp_loop_true-unreach-call.c true 2 wit inspect 11    11    110   3100 2.5 0      - - out of memory 560    540    9100   7000 timeout 960   950   17000 1400
float-benchs/feedback_diverge_true-unreach-call.c true 2 wit inspect 11    10    110   3300 2.5 0      - - timeout 900    900    15000   1700 timeout 960   820   16000 4700
float-benchs/filter1_true-unreach-call.c true 2 wit inspect 11    11    130   3800 2.5 0      - - true 8.7  6.5  160   410 timeout 960   950   12000 980
float-benchs/filter2_alt_true-unreach-call.c true 2 wit inspect 11    11    110   4600 2.5 0      - - timeout 900    900    14000   910 timeout 960   950   16000 870
float-benchs/filter2_iterated_true-unreach-call.c true 2 wit inspect 12    12    150   3000 2.5 0      - - timeout 900    900    14000   1600 error 52   46   760 2200
float-benchs/filter2_reinit_true-unreach-call.c true 2 wit inspect 14    14    150   3800 2.5 0      - - timeout 900    900    15000   920 timeout 960   950   9300 2500
float-benchs/filter2_set_true-unreach-call.c true 2 wit inspect 14    13    140   4200 2.5 0      - - timeout 900    900    18000   1900 timeout 960   950   11000 4800
float-benchs/filter2_true-unreach-call.c true 2 wit inspect 13    13    130   4300 2.5 0      - - timeout 900    900    15000   1400 timeout 960   950   13000 2800
float-benchs/filter_iir_true-unreach-call.c true 2 wit inspect 14    14    160   4200 2.5 0      - - timeout 900    900    12000   2800 unknown 6.6 3.5 80 320
float-benchs/float_double_true-unreach-call.c true 2 wit inspect .16 .16 1.3 23 1.7 0      - - true 3.7  2.1  46   260 true 12   6.8 220 310
float-benchs/image_filter_true-unreach-call.c true 2 wit inspect 11    11    140   1300 2.5 0      - - out of memory 56    48    1000   7000 unknown 6.6 3.5 110 310
float-benchs/interpolation2_true-unreach-call.c true 2 wit inspect 2.6  2.6  28   85 2.5 0      - - true 54    52    1300   550 timeout 960   950   10000 580
float-benchs/interpolation_true-unreach-call.c true 2 wit inspect 1.5  1.5  15   63 2.5 0      - - true 64    62    1500   480 out of memory 180   170   3600 7000
float-benchs/inv_sqrt_Quake_true-unreach-call.c true 2 wit inspect 1.2  1.2  14   61 2.5 0      - - unknown 6.1  3.7  57   310 unknown 5.8 3.1 93 290
float-benchs/inv_square_int_true-unreach-call.c true 2 wit inspect .37 .37 4.3 33 2.5 0      - - true 4.6  2.7  46   270 true 26   20   550 330
float-benchs/inv_square_true-unreach-call.c true 2 wit inspect .34 .34 3.6 29 2.5 0      - - true 4.3  2.4  42   270 true 82   77   1600 350
float-benchs/loop_true-unreach-call.c true 2 wit inspect .25 .24 2.8 40 2.0 0      - - timeout 900    900    14000   2100 timeout 960   950   12000 900
float-benchs/mea8000_true-unreach-call.c true 2 wit inspect 310    310    3500   7000 2.7 0      - - timeout 900    890    14000   4000 unknown 6.5 3.4 98 300
float-benchs/nan_double_range_true-unreach-call.c true 2 wit inspect .20 .20 2.3 24 2.5 0      - - true 4.1  2.3  50   260 true 13   7.0 160 310
float-benchs/nan_float_range_true-unreach-call.c true 2 wit inspect .19 .19 2.5 24 2.5 0      - - true 4.2  2.3  60   260 true 15   8.3 240 310
float-benchs/rlim_exit_true-unreach-call.c true 2 wit inspect 11    11    120   3600 2.5 0      - - timeout 900    900    13000   2100 timeout 960   850   14000 3600
float-benchs/rlim_invariant_true-unreach-call.c true 2 wit inspect 12    12    120   3800 2.5 0      - - true 6.4  3.9  91   330 error 99   92   1200 570
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call.c unknown 0 wit inspect 900    900    5000   3200 1.7 0      - - error (invalid witness file) .56 .36 11   42 error (invalid witness file) 6.7 3.5 92 320
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call.c unknown 0 wit inspect 900    900    6700   4400 1.7 0      - - error (invalid witness file) .65 .41 4.9 41 error (invalid witness file) 5.6 3.0 60 290
float-benchs/sin_interpolated_index_true-unreach-call.c unknown 0 wit inspect 900    900    6900   650 1.7 0      - - error (invalid witness file) .62 .41 7.8 39 error (invalid witness file) 5.5 2.9 47 300
float-benchs/sin_interpolated_negation_true-unreach-call.c true 2 wit inspect 92    92    870   1700 2.5 0      - - error 6.4  3.4  120   300 out of memory 510   500   6000 7000
float-benchs/sin_interpolated_smallrange_true-unreach-call.c true 2 wit inspect 530    530    4300   13000 2.5 0      - - error 7.1  3.8  63   290 out of memory 630   620   7400 7000
float-benchs/sqrt_Householder_constant_true-unreach-call.c true 2 wit inspect .35 .35 4.5 27 1.8 0      - - timeout 900    900    15000   1700 error 590   580   7100 2900
float-benchs/sqrt_Householder_interval_true-unreach-call.c true 2 wit inspect 16    15    180   3600 2.5 0      - - timeout 900    900    15000   1200 error 470   470   8800 3000
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c true 2 wit inspect 50    50    690   3600 2.5 0      - - timeout 900    900    18000   2000 error 480   470   5600 2800
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c true 2 wit inspect 50    50    630   3600 2.5 0      - - timeout 900    900    19000   3100 error 470   460   5600 2800
float-benchs/sqrt_biNewton_pseudoconstant_true-unreach-call.c true 2 wit inspect 61    61    740   4400 2.5 0      - - timeout 900    900    14000   2100 error 160   150   1800 1800
float-benchs/sqrt_poly_true-unreach-call.c true 2 wit inspect 11    11    100   300 2.5 0      - - true 95    93    1800   470 true 560   550   7000 1400
float-benchs/water_pid_true-unreach-call.c true 2 wit inspect .27 .27 3.3 29 1.8 0      - - timeout 900    900    14000   1800 error 130   130   1500 2600
float-benchs/zonotope_2_true-unreach-call.c true 2 wit inspect .53 .53 5.9 81 2.3 0      - - timeout 900    900    18000   1200 timeout 960   950   22000 1200
float-benchs/zonotope_3_true-unreach-call.c true 2 wit inspect 11    10    130   3600 2.5 0      - - true 7.6  4.9  100   350 timeout 960   830   16000 4700
float-benchs/zonotope_loose_true-unreach-call.c true 2 wit inspect 2.1  2.0  21   110 2.5 0      - - true 4.7  3.0  69   320 true 620   620   5300 1200
float-benchs/zonotope_tight_true-unreach-call.c true 2 wit inspect 2.1  2.1  26   110 2.5 0      - - true 4.5  2.9  87   310 true 750   750   7000 1400
floats-esbmc-regression/Double_div_true-unreach-call.i true 2 wit inspect .22 .22 2.3 30 1.9 0      - - true 11    6.3  130   360 true 430   420   4800 2600
floats-esbmc-regression/Float_div_true-unreach-call.i true 2 wit inspect .15 .15 1.7 23 1.7 0      - - true 7.0  3.8  73   300 true 230   220   3300 700
floats-esbmc-regression/ceil_nondet_true-unreach-call.i true 2 wit inspect .58 .58 7.7 44 2.5 0      - - error 5.2  2.8  90   270 unknown 11   5.8 160 300
floats-esbmc-regression/ceil_true-unreach-call.i true 2 wit inspect .32 .32 4.0 26 2.5 0      - - true 5.7  3.1  110   270 unknown 7.3 3.8 110 320
floats-esbmc-regression/copysign_true-unreach-call.i true 2 wit inspect .25 .25 3.1 27 1.7 0      - - true 6.4  3.5  82   270 unknown 5.6 3.0 57 300
floats-esbmc-regression/digits_for_true-unreach-call.i true 2 wit inspect .15 .15 1.7 23 1.7 0      - - timeout 900    900    11000   1000 timeout 960   950   13000 1400
floats-esbmc-regression/digits_while_true-unreach-call.i true 2 wit inspect .16 .16 1.8 23 1.7 0      - - timeout 900    900    14000   970 timeout 960   950   10000 3100
floats-esbmc-regression/fabs_true-unreach-call.i true 2 wit inspect .26 .26 2.9 27 1.7 0      - - true 5.9  3.2  99   280 true 16   8.4 140 310
floats-esbmc-regression/fdim_true-unreach-call.i true 2 wit inspect .27 .27 2.4 26 1.7 0      - - true 6.5  3.5  71   280 unknown 7.2 3.8 100 320
floats-esbmc-regression/floor_nondet_true-unreach-call.i true 2 wit inspect .59 .59 6.6 44 2.5 0      - - error 5.9  3.2  84   270 unknown 11   5.9 170 310
floats-esbmc-regression/floor_true-unreach-call.i true 2 wit inspect .33 .32 3.7 26 2.5 0      - - true 6.6  3.5  68   280 unknown 6.2 3.3 110 300
floats-esbmc-regression/fmax_true-unreach-call.i true 2 wit inspect .27 .26 2.2 27 1.7 0      - - true 5.9  3.2  100   280 unknown 6.3 3.3 92 300
floats-esbmc-regression/fmin_true-unreach-call.i true 2 wit inspect .23 .23 2.4 27 1.7 0      - - true 5.2  2.8  95   270 unknown 6.4 3.4 87 310
floats-esbmc-regression/fmod2_true-unreach-call.i true 2 wit inspect .34 .34 4.6 27 2.5 0      - - false(unreach-call) 9.1  4.9  71   310 unknown 11   5.7 190 300
floats-esbmc-regression/fmod3_true-unreach-call.i true 2 wit inspect .34 .33 4.1 26 2.5 0      - - false(unreach-call) 7.4  3.9  130   310 unknown 11   5.8 150 330
floats-esbmc-regression/fmod_true-unreach-call.i true 2 wit inspect .23 .23 3.0 27 1.7 0      - - true 6.8  3.7  77   280 unknown 7.3 3.9 97 310
floats-esbmc-regression/isgreater_true-unreach-call.i true 2 wit inspect .23 .23 3.2 27 1.7 0      - - true 5.3  2.9  76   270 error 10   5.5 140 310
floats-esbmc-regression/isgreaterequal_true-unreach-call.i true 2 wit inspect .24 .24 2.7 26 1.7 0      - - true 6.8  3.6  75   270 error 10   5.4 72 310
floats-esbmc-regression/isless_true-unreach-call.i true 2 wit inspect .23 .23 2.8 27 1.7 0      - - true 6.9  3.7  58   280 error 10   5.5 150 310
floats-esbmc-regression/islessequal_true-unreach-call.i true 2 wit inspect .24 .24 2.7 27 1.7 0      - - true 6.7  3.6  79   280 error 10   5.6 170 300
floats-esbmc-regression/islessgreater_true-unreach-call.i true 2 wit inspect .25 .25 2.5 27 1.7 0      - - true 5.5  3.0  60   270 error 9.8 5.3 110 300
floats-esbmc-regression/isunordered_true-unreach-call.i true 2 wit inspect .26 .26 2.4 27 1.7 .27   - - true 6.0  3.2  72   270 error 13   7.0 160 300
floats-esbmc-regression/lrint_true-unreach-call.i true 2 wit inspect .38 .38 4.3 26 2.5 0      - - error 5.7  3.1  87   270 unknown 8.0 4.2 63 300
floats-esbmc-regression/modf_true-unreach-call.i true 2 wit inspect .32 .32 4.7 26 2.5 0      - - true 5.7  3.1  65   270 unknown 6.0 3.2 72 300
floats-esbmc-regression/nan_true-unreach-call.i true 2 wit inspect .26 .26 2.8 27 1.7 0      - - true 6.1  3.3  100   280 true 13   6.9 170 300
floats-esbmc-regression/nearbyint2_true-unreach-call.i true 2 wit inspect .38 .38 4.2 26 2.5 0      - - error 6.8  3.7  70   270 unknown 6.8 3.6 85 310
floats-esbmc-regression/nearbyint_true-unreach-call.i true 2 wit inspect .37 .36 3.9 26 2.5 0      - - error 9.2  4.9  88   290 unknown 6.2 3.3 79 310
floats-esbmc-regression/remainder_true-unreach-call.i true 2 wit inspect .37 .37 4.0 26 2.5 0      - - true 5.9  3.2  95   270 unknown 6.5 3.4 100 300
floats-esbmc-regression/rint2_true-unreach-call.i true 2 wit inspect .40 .40 4.6 26 2.5 0      - - error 5.4  2.9  85   280 unknown 5.8 3.1 64 290
floats-esbmc-regression/rint_true-unreach-call.i true 2 wit inspect .40 .39 4.3 26 2.5 0      - - error 7.2  3.8  130   300 unknown 5.8 3.1 120 300
floats-esbmc-regression/round_nondet_true-unreach-call.i true 2 wit inspect 1.3  1.3  15   87 2.6 0      - - error 6.2  3.4  44   270 unknown 10   5.5 130 300
floats-esbmc-regression/round_true-unreach-call.i true 2 wit inspect .42 .42 4.9 28 2.6 0      - - true 7.3  3.9  71   280 unknown 7.2 3.8 86 300
floats-esbmc-regression/rounding_functions_true-unreach-call.i true 2 wit inspect .47 .47 6.8 29 2.6 0      - - true 7.2  3.9  70   280 unknown 6.3 3.3 100 300
floats-esbmc-regression/trunc_nondet_2_true-unreach-call.i true 2 wit inspect 2.3  2.3  27   47 2.5 0      - - unknown 6.8  3.7  110   330 unknown 11   5.8 210 310
floats-esbmc-regression/trunc_nondet_true-unreach-call.i true 2 wit inspect .61 .61 7.0 44 2.5 0      - - error 5.9  3.2  75   280 unknown 11   6.0 110 310
floats-esbmc-regression/trunc_true-unreach-call.i true 2 wit inspect .32 .32 3.7 26 2.5 0      - - true 6.3  3.4  90   290 unknown 6.2 3.3 110 300
floats-esbmc-regression/Double_div_bad_false-unreach-call.i false(unreach-call) 1 wit inspect .20 .19 2.1 23 1.7 .094  out of memory 58   53   1700 7000 true 7.0 3.7 120 320 - -
floats-esbmc-regression/Float_div_bad_false-unreach-call.i false(unreach-call) 1 wit inspect .14 .14 1.8 23 1.7 0      false(unreach-call) 29   23   420 2000 true 7.7 4.1 100 330 - -
floats-esbmc-regression/digits_bad_for_false-unreach-call.i false(unreach-call) 1 wit inspect .15 .15 1.8 23 1.7 .094  false(unreach-call) 5.7 3.1 86 280 true 12   6.9 150 310 - -
floats-esbmc-regression/digits_bad_while_false-unreach-call.i false(unreach-call) 1 wit inspect .18 .18 1.5 23 1.7 .094  false(unreach-call) 7.4 4.0 84 290 true 11   6.5 140 300 - -
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
total 172 308 7900 7900 63000 120000 390 .75 172 870 810 20000 30000   172 1500 1400 22000 48000   172 42000 42000 680000 98000   172 31000 29000 430000 300000  
    correct results 169 308 5200 5200 45000 110000 390 .75 21 870 810 20000 30000   15 1500 1400 22000 48000   80 42000 42000 680000 98000   43 31000 29000 430000 290000  
        correct true 139 278 4800 4800 41000 110000 320 .46 8 0 0 0 0   4 0 0 0 0   77 42000 42000 680000 98000   43 31000 29000 430000 290000  
        correct false 30 30 360 360 3300 5200 72 .29 13 870 810 20000 30000   11 1500 1400 22000 48000   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) 308
Run set sv-comp17.ReachSafety-Floats