Tool CPAchecker 1.6.1-svn 24048
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS [Linux 4.4.0-57-generic; 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-10 22:04:57 CET [[ 2017-01-14 18:01:27 CET ]] [[ 2017-01-14 20:11:29 CET ]] [[ 2017-01-14 18:28:10 CET ]] [[ 2017-01-14 20:42:56 CET ]]
Run set sv-comp17.ReachSafety-Floats
Options -sv-comp17-k-induction -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-10_2204.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 200   100    880 3000 .0082 0      false(unreach-call) 5.6  3.9  87   440 timeout 97   91   1700 3600 - -
floats-cdfpl/newton_1_5_false-unreach-call.i false(unreach-call) 1 wit inspect 67   33    350 750 .0082 0      false(unreach-call) 69    67    1300   480 false(unreach-call) 72   67   1400 2200 - -
floats-cdfpl/newton_1_6_false-unreach-call.i false(unreach-call) 1 wit inspect 75   37    450 660 .012  0      false(unreach-call) 33    32    280   470 false(unreach-call) 54   48   760 1700 - -
floats-cdfpl/newton_1_7_false-unreach-call.i false(unreach-call) 1 wit inspect 13   5.5  92 490 .0041 0      false(unreach-call) 33    31    220   490 false(unreach-call) 76   69   930 2000 - -
floats-cdfpl/newton_1_8_false-unreach-call.i false(unreach-call) 1 wit inspect 55   27    330 920 .012  0      false(unreach-call) 22    21    310   470 false(unreach-call) 32   27   450 990 - -
floats-cdfpl/newton_2_6_false-unreach-call.i false(unreach-call) 1 wit inspect 410   210    1900 5100 .0082 0      false(unreach-call) 8.9  7.2  96   640 timeout 97   90   1700 3100 - -
floats-cdfpl/newton_2_7_false-unreach-call.i false(unreach-call) 1 wit inspect 250   120    1300 1900 .012  .025  false(unreach-call) 58    56    1100   670 timeout 97   90   990 2500 - -
floats-cdfpl/newton_2_8_false-unreach-call.i false(unreach-call) 1 wit inspect 550   280    4000 1200 .012  0      false(unreach-call) 39    38    530   660 timeout 97   91   1800 2500 - -
floats-cdfpl/newton_3_6_false-unreach-call.i timeout 0 wit inspect 960   480    4800 4600 .016  0      error (invalid witness file) .53 .34 11   40 error (invalid witness file) 5.9 3.1 110 300 - -
floats-cdfpl/newton_3_7_false-unreach-call.i false(unreach-call) 1 wit inspect 620   310    3400 2100 .012  0      timeout 92    90    1500   590 timeout 97   91   1200 3800 - -
floats-cdfpl/newton_3_8_false-unreach-call.i false(unreach-call) 1 wit inspect 660   330    3600 2800 .016  .84   timeout 93    91    1700   3200 false(unreach-call) 54   48   710 1400 - -
floats-cdfpl/sine_1_false-unreach-call.i false(unreach-call) 1 wit inspect 41   20    250 760 .0082 0      false(unreach-call) 47    45    460   440 false(unreach-call) 26   21   620 900 - -
floats-cdfpl/sine_2_false-unreach-call.i false(unreach-call) 1 wit inspect 83   41    460 1600 .0082 8.7    false(unreach-call) 4.4  2.9  64   360 timeout 97   92   1600 3400 - -
floats-cdfpl/sine_3_false-unreach-call.i false(unreach-call) 1 wit inspect 74   36    450 1300 .0082 0      timeout 92    90    710   370 timeout 97   91   1900 3400 - -
floats-cdfpl/square_1_false-unreach-call.i false(unreach-call) 1 wit inspect 68   33    370 780 .0082 0      timeout 92    90    750   480 false(unreach-call) 41   36   750 980 - -
floats-cdfpl/square_2_false-unreach-call.i false(unreach-call) 1 wit inspect 63   31    340 930 .012  0      false(unreach-call) 26    25    480   410 timeout (false(unreach-call)) 95   88   1000 1800 - -
floats-cdfpl/square_3_false-unreach-call.i false(unreach-call) 1 wit inspect 260   130    1500 3600 .0082 0      timeout 92    90    1700   410 timeout 97   91   760 2500 - -
floats-cdfpl/newton_1_1_true-unreach-call.i timeout 0 wit inspect 900   450    4800 11000 .0041 0      - - timeout 900    900    15000   680 out of memory 230   230   3900 7000
floats-cdfpl/newton_1_2_true-unreach-call.i timeout 0 wit inspect 900   450    4500 9300 .0041 0      - - timeout 900    900    28000   590 out of memory 190   190   4200 7000
floats-cdfpl/newton_1_3_true-unreach-call.i timeout 0 wit inspect 900   450    4700 12000 .0041 0      - - timeout 900    900    16000   550 out of memory 220   220   3400 7000
floats-cdfpl/newton_2_1_true-unreach-call.i timeout 0 wit inspect 910   450    4100 12000 .0041 .82   - - timeout 900    900    14000   560 out of memory 250   250   3100 7000
floats-cdfpl/newton_2_2_true-unreach-call.i timeout 0 wit inspect 910   450    4000 12000 .0041 0      - - timeout 900    900    24000   560 out of memory 220   210   3600 7000
floats-cdfpl/newton_2_3_true-unreach-call.i timeout 0 wit inspect 910   450    5100 12000 .0041 0      - - timeout 900    900    16000   520 out of memory 240   230   2800 7000
floats-cdfpl/newton_2_4_true-unreach-call.i timeout 0 wit inspect 900   450    4100 12000 .0041 0      - - timeout 900    900    20000   580 out of memory 240   230   3400 7000
floats-cdfpl/newton_2_5_true-unreach-call.i timeout 0 wit inspect 900   450    3500 11000 .0041 .025  - - timeout 900    900    17000   720 out of memory 250   250   2700 7000
floats-cdfpl/newton_3_1_true-unreach-call.i timeout 0 wit inspect 910   450    4400 12000 .0082 .82   - - timeout 900    900    15000   850 out of memory 190   190   5600 7000
floats-cdfpl/newton_3_2_true-unreach-call.i timeout 0 wit inspect 910   450    3800 13000 .0082 0      - - timeout 900    900    18000   560 out of memory 230   220   3600 7000
floats-cdfpl/newton_3_3_true-unreach-call.i timeout 0 wit inspect 910   450    4200 12000 .0082 0      - - timeout 900    900    18000   730 out of memory 240   230   2300 7000
floats-cdfpl/newton_3_4_true-unreach-call.i timeout 0 wit inspect 910   450    5600 13000 .0082 0      - - timeout 900    900    22000   810 out of memory 230   220   2500 7000
floats-cdfpl/newton_3_5_true-unreach-call.i timeout 0 wit inspect 910   450    4800 11000 .0082 0      - - timeout 900    900    13000   770 out of memory 240   230   4600 7000
floats-cdfpl/sine_4_true-unreach-call.i timeout 0 wit inspect 900   450    5100 13000 .0041 0      - - timeout 900    900    26000   560 out of memory 220   210   3300 7000
floats-cdfpl/sine_5_true-unreach-call.i timeout 0 wit inspect 900   450    4900 13000 .0041 0      - - timeout 900    900    17000   480 out of memory 240   230   4400 7000
floats-cdfpl/sine_6_true-unreach-call.i timeout 0 wit inspect 900   450    4400 14000 .0041 0      - - timeout 900    900    16000   630 out of memory 210   200   2100 7000
floats-cdfpl/sine_7_true-unreach-call.i timeout 0 wit inspect 900   450    5900 14000 .0041 0      - - timeout 900    900    17000   400 out of memory 210   210   2200 7000
floats-cdfpl/sine_8_true-unreach-call.i timeout 0 wit inspect 900   450    5000 12000 .0041 .020  - - timeout 900    900    16000   500 out of memory 210   200   5400 7000
floats-cdfpl/square_4_true-unreach-call.i timeout 0 wit inspect 900   450    4000 11000 .0041 0      - - timeout 900    900    19000   580 out of memory 220   210   2300 7000
floats-cdfpl/square_5_true-unreach-call.i timeout 0 wit inspect 900   450    4400 11000 .0041 0      - - true 520    520    11000   510 out of memory 260   260   4300 7000
floats-cdfpl/square_6_true-unreach-call.i timeout 0 wit inspect 900   450    4100 10000 .0041 0      - - true 860    860    15000   600 out of memory 250   240   4700 7000
floats-cdfpl/square_7_true-unreach-call.i true 2 wit inspect 660   330    3300 8200 .0041 0      - - true 310    310    7700   500 out of memory 370   360   5700 7000
floats-cdfpl/square_8_true-unreach-call.i true 2 wit inspect 48   23    300 810 .0041 0      - - true 28    26    400   340 out of memory 270   260   2600 7000
floats-cbmc-regression/float-div1_true-unreach-call.i true 2 wit inspect 9.1 2.3  60 540 .14   0      - - true 7.7  4.5  78   340 true 87   79   1400 690
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i true 2 wit inspect 23   5.7  160 2400 .40   0      - - true 13    9.1  180   700 true 36   24   660 730
floats-cbmc-regression/float-no-simp1_true-unreach-call.i true 2 wit inspect 2.7 .96 23 270 .0041 0      - - true 4.2  2.4  37   270 true 14   7.5 180 300
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true 2 wit inspect 25   9.8  220 530 .43   .79   - - true 17    14    530   320 true 58   51   750 470
floats-cbmc-regression/float-no-simp3_true-unreach-call.i true 2 wit inspect 2.6 .95 24 270 .0041 0      - - true 3.5  2.0  58   260 true 13   6.7 200 300
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true 2 wit inspect 5.4 1.5  41 320 .82   .0041 - - true 6.6  3.6  94   280 true 25   14   430 530
floats-cbmc-regression/float-no-simp6_true-unreach-call.i true 2 wit inspect 2.8 1.0  21 280 .0041 0      - - true 4.3  2.4  49   260 true 13   7.2 250 310
floats-cbmc-regression/float-no-simp7_true-unreach-call.i true 2 wit inspect 2.7 .99 23 260 .0041 0      - - true 4.3  2.5  46   250 true 12   6.5 190 310
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true 2 wit inspect 3.4 1.2  27 270 .0041 0      - - true 6.6  3.5  69   280 true 13   7.3 240 310
floats-cbmc-regression/float-rounding1_true-unreach-call.i error 0 wit inspect 6.4 1.7  46 440 .074  0      - - error 6.6  3.6  51   270 unknown 6.9 3.7 110 300
floats-cbmc-regression/float-to-double1_true-unreach-call.i true 2 wit inspect 5.6 1.5  45 320 .14   .0041 - - true 6.6  3.6  57   280 true 180   180   4000 460
floats-cbmc-regression/float-to-double2_true-unreach-call.i true 2 wit inspect 2.6 1.0  20 290 .0041 0      - - true 3.7  2.1  56   250 true 12   6.6 200 310
floats-cbmc-regression/float-zero-sum1_true-unreach-call.i true 2 wit inspect 2.8 1.0  27 260 .0041 0      - - true 3.4  1.9  61   250 unknown 6.1 3.3 130 300
floats-cbmc-regression/float11_true-unreach-call.i true 2 wit inspect 2.7 1.0  22 260 .0041 0      - - true 3.8  2.1  62   260 true 13   7.2 240 320
floats-cbmc-regression/float12_true-unreach-call.i true 2 wit inspect 3.1 1.0  23 270 .0041 0      - - true 4.4  2.5  45   260 true 19   13   440 310
floats-cbmc-regression/float13_true-unreach-call.i true 2 wit inspect 2.8 1.0  22 270 .0041 0      - - true 3.5  2.0  58   260 true 14   7.7 260 310
floats-cbmc-regression/float14_true-unreach-call.i true 2 wit inspect 3.4 1.1  25 280 .0041 0      - - true 6.0  3.2  70   280 true 14   7.8 270 310
floats-cbmc-regression/float18_true-unreach-call.i true 2 wit inspect 3.7 1.2  29 270 .0041 0      - - true 28    24    550   440 unknown 6.9 3.7 120 300
floats-cbmc-regression/float19_true-unreach-call.i true 2 wit inspect 4.7 1.3  34 330 .070  .0041 - - true 5.2  2.8  68   280 true 17   10   190 310
floats-cbmc-regression/float1_true-unreach-call.i true 2 wit inspect 2.8 1.0  23 270 .0041 0      - - true 4.0  2.3  54   260 true 16   8.6 200 310
floats-cbmc-regression/float20_true-unreach-call.i true 2 wit inspect 2.8 1.0  21 270 .0041 0      - - true 4.6  2.6  47   260 true 27   21   450 410
floats-cbmc-regression/float21_true-unreach-call.i true 2 wit inspect 8.6 2.0  64 500 .22   0      - - true 7.1  4.0  99   310 true 94   85   1200 630
floats-cbmc-regression/float22_true-unreach-call.i false(unreach-call) -16 wit inspect 5.0 1.4  37 320 .086  .020  - - false(unreach-call) 6.2  3.4  99   290 unknown 15   8.0 240 330
floats-cbmc-regression/float2_true-unreach-call.i true 2 wit inspect 2.9 1.1  23 290 .0041 8.8    - - true 3.7  2.1  54   260 true 17   8.9 230 320
floats-cbmc-regression/float3_true-unreach-call.i true 2 wit inspect 2.7 .96 21 260 .0041 0      - - true 3.9  2.3  70   280 true 20   14   440 340
floats-cbmc-regression/float4_true-unreach-call.i true 2 wit inspect 58   26    470 790 .29   0      - - true 67    64    1500   340 true 92   85   1600 530
floats-cbmc-regression/float5_true-unreach-call.i true 2 wit inspect 2.8 .98 23 270 .0041 0      - - true 3.3  1.9  70   270 true 31   25   500 320
floats-cbmc-regression/float6_true-unreach-call.i true 2 wit inspect 2.8 1.0  24 260 .0041 0      - - true 5.3  2.9  55   270 true 15   7.9 320 320
floats-cbmc-regression/float7_true-unreach-call.i true 2 wit inspect 2.8 1.0  23 300 .0041 0      - - true 3.7  2.1  50   260 unknown 6.7 3.6 130 310
floats-cbmc-regression/float8_true-unreach-call.i true 2 wit inspect 7.3 2.2  51 340 .070  0      - - true 5.8  3.4  84   280 true 13   7.5 230 300
floats-cbmc-regression/float_lib1_true-unreach-call.i true 2 wit inspect 3.5 1.2  28 270 .0041 0      - - true 6.1  3.3  83   270 error 13   6.7 250 310
floats-cbmc-regression/float_lib2_true-unreach-call.i true 2 wit inspect 3.6 1.2  28 270 .0041 0      - - true 6.3  3.4  80   270 true 23   13   260 430
float-benchs/cast_float_ptr_false-unreach-call.c exception 0 wit inspect 3.0 1.0  23 270 .0041 .061  error (invalid witness file) .51 .33 8.9 40 error (invalid witness file) 7.1 3.7 110 310 - -
float-benchs/cast_union_loose_false-unreach-call.c false(unreach-call) 1 wit inspect 4.2 1.3  33 310 .0041 0      false(unreach-call) 4.4  2.5  52   290 unknown 5.8 3.1 110 300 - -
float-benchs/cast_union_tight_false-unreach-call.c false(unreach-call) 1 wit inspect 4.1 1.2  28 320 .0041 0      false(unreach-call) 4.2  2.4  57   290 unknown 6.2 3.3 140 300 - -
float-benchs/float_int_inv_square_false-unreach-call.c false(unreach-call) 1 wit inspect 3.8 1.2  30 310 .0041 0      false(unreach-call) 4.1  2.3  41   290 false(unreach-call) 13   7.2 210 310 - -
float-benchs/inv_square_false-unreach-call.c false(unreach-call) 1 wit inspect 4.0 1.3  31 310 .0041 .020  false(unreach-call) 4.2  2.3  50   290 false(unreach-call) 12   6.7 220 310 - -
float-benchs/nan_double_false-unreach-call.c false(unreach-call) 1 wit inspect 3.4 1.1  29 290 .0082 0      false(unreach-call) 4.1  2.3  68   270 false(unreach-call) 7.6 4.1 130 320 - -
float-benchs/nan_float_false-unreach-call.c false(unreach-call) 1 wit inspect 3.5 1.1  28 290 .0082 0      false(unreach-call) 3.8  2.2  49   270 false(unreach-call) 7.2 3.8 150 320 - -
float-benchs/sin_interpolated_index_false-unreach-call.c false(unreach-call) 1 wit inspect 190   190    2500 550 .28   0      unknown 3.7  2.1  76   270 timeout 97   90   1800 5800 - -
float-benchs/sqrt_poly2_false-unreach-call.c false(unreach-call) 1 wit inspect 27   12    170 920 .012  0      false(unreach-call) 5.7  3.8  120   500 error 11   5.9 210 300 - -
float-benchs/Muller_Kahan_true-unreach-call.c true 2 wit inspect 4.3 1.4  31 340 .0041 0      - - timeout 900    900    17000   2600 timeout 960   910   18000 7000
float-benchs/Rump_double_true-unreach-call.c true 2 wit inspect 2.8 .97 24 270 .0041 0      - - true 3.7  2.1  58   260 true 27   20   300 790
float-benchs/Rump_float_true-unreach-call.c true 2 wit inspect 2.7 .98 24 270 .0041 0      - - true 4.0  2.2  52   260 true 16   9.4 300 390
float-benchs/addsub_double_exact_true-unreach-call.c true 2 wit inspect 2.9 .99 22 270 .0041 0      - - true 4.3  2.4  61   270 true 13   7.2 210 320
float-benchs/addsub_float_exact_true-unreach-call.c true 2 wit inspect 2.6 .98 20 260 .0041 0      - - true 3.4  1.9  72   250 true 15   8.1 270 320
float-benchs/addsub_float_inexact_true-unreach-call.c true 2 wit inspect 2.7 .98 22 260 .0041 0      - - true 4.3  2.4  49   260 true 13   7.0 270 310
float-benchs/arctan_Pade_true-unreach-call.c true 2 wit inspect 25   11    190 940 .0082 0      - - true 14    12    150   510 error 39   33   690 1200
float-benchs/bary_diverge_true-unreach-call.c timeout 0 wit inspect 900   430    8900 5000 0      0      - - timeout 900    900    20000   1100 timeout 960   950   18000 760
float-benchs/cast_float_union_true-unreach-call.c true 2 wit inspect 3.0 1.1  26 270 0      0      - - true 3.5  1.9  61   270 error 12   6.2 160 300
float-benchs/cos_polynomial_true-unreach-call.c timeout 0 wit inspect 910   450    4700 11000 .0082 0      - - timeout 900    900    17000   1200 out of memory 300   300   7600 7000
float-benchs/divmul_buf_diverge_true-unreach-call.c timeout 0 wit inspect 900   440    8300 3700 0      0      - - timeout 900    900    18000   2900 timeout 960   820   15000 4700
float-benchs/divmul_diverge_true-unreach-call.c timeout 0 wit inspect 900   440    8000 5900 0      0      - - timeout 900    900    20000   2900 timeout 960   820   25000 4700
float-benchs/drift_tenth_true-unreach-call.c true 2 wit inspect 2.8 1.0  21 270 .0041 0      - - true 12    10    260   340 true 160   150   3300 620
float-benchs/exp_loop_true-unreach-call.c true 2 wit inspect 630   610    6000 8900 0      0      - - out of memory 560    550    13000   7000 error 42   30   810 600
float-benchs/feedback_diverge_true-unreach-call.c timeout 0 wit inspect 900   440    8300 3500 0      0      - - timeout 900    900    20000   1700 timeout 960   810   18000 4700
float-benchs/filter1_true-unreach-call.c true 2 wit inspect 28   5.5  170 1300 0      0      - - true 9.1  7.2  180   430 error 16   10   260 370
float-benchs/filter2_alt_true-unreach-call.c timeout 0 wit inspect 900   890    7300 1200 .012  .020  - - timeout 900    900    13000   910 timeout 960   950   24000 570
float-benchs/filter2_iterated_true-unreach-call.c segmentation fault 0 wit inspect 20   7.1  150 1600 .012  .012  - - error (invalid witness file) .62 .39 7.2 40 error (invalid witness file) 5.2 2.8 100 290
float-benchs/filter2_reinit_true-unreach-call.c timeout 0 wit inspect 900   430    8400 3200 0      0      - - timeout 900    900    16000   1400 error 17   10   280 530
float-benchs/filter2_set_true-unreach-call.c timeout 0 wit inspect 900   420    8200 4600 0      0      - - timeout 900    900    25000   2100 error 21   14   400 690
float-benchs/filter2_true-unreach-call.c timeout 0 wit inspect 900   430    8800 4500 0      0      - - timeout 900    900    19000   1400 error 19   13   520 530
float-benchs/filter_iir_true-unreach-call.c true 2 wit inspect 3.4 1.1  26 280 .0041 0      - - timeout 900    900    21000   3000 unknown 6.7 3.6 110 290
float-benchs/float_double_true-unreach-call.c true 2 wit inspect 2.6 .96 20 270 .0041 0      - - true 3.5  2.0  54   260 true 13   6.9 190 320
float-benchs/image_filter_true-unreach-call.c segmentation fault 0 wit inspect 11   2.2  74 560 .69   .020  - - error (invalid witness file) .63 .41 9.0 40 error (invalid witness file) 6.1 3.3 110 300
float-benchs/interpolation2_true-unreach-call.c segmentation fault 0 wit inspect 11   4.0  99 390 .037  0      - - error (invalid witness file) .59 .38 9.0 40 error (invalid witness file) 5.8 3.1 110 290
float-benchs/interpolation_true-unreach-call.c segmentation fault 0 wit inspect 8.2 2.7  65 370 .037  .045  - - error (invalid witness file) .62 .40 8.5 39 error (invalid witness file) 7.4 3.9 80 300
float-benchs/inv_sqrt_Quake_true-unreach-call.c false(unreach-call) -16 wit inspect 4.7 1.5  39 330 .0041 0      - - unknown 5.1  3.1  120   320 unknown 6.3 3.4 110 310
float-benchs/inv_square_int_true-unreach-call.c true 2 wit inspect 3.8 1.2  26 300 .0041 0      - - true 3.6  2.1  79   270 true 40   34   540 350
float-benchs/inv_square_true-unreach-call.c true 2 wit inspect 3.6 1.2  27 300 .0041 0      - - true 3.5  2.0  68   270 true 39   33   980 330
float-benchs/loop_true-unreach-call.c timeout 0 wit inspect 900   890    7200 2500 0      0      - - timeout 900    900    24000   2000 timeout 960   950   17000 870
float-benchs/mea8000_true-unreach-call.c timeout (assertion) 0 wit inspect 900   390    7700 7200 0      .0082 - - error (invalid witness file) .60 .39 14   42 error (invalid witness file) 5.6 3.0 110 300
float-benchs/nan_double_range_true-unreach-call.c true 2 wit inspect 3.5 1.1  28 310 .0041 0      - - true 3.6  2.0  74   260 true 13   6.8 200 310
float-benchs/nan_float_range_true-unreach-call.c true 2 wit inspect 3.4 1.1  27 290 .0041 0      - - true 4.3  2.4  54   260 true 14   8.4 300 310
float-benchs/rlim_exit_true-unreach-call.c timeout 0 wit inspect 900   440    10000 3700 0      0      - - timeout 900    900    18000   1800 timeout 960   850   25000 4300
float-benchs/rlim_invariant_true-unreach-call.c true 2 wit inspect 15   3.4  98 670 0      0      - - true 6.6  4.2  110   330 timeout 960   950   17000 720
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call.c error 0 wit inspect 5.3 1.5  40 310 .012  0      - - error 4.4  2.5  53   260 out of memory 490   490   6500 7000
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call.c error 0 wit inspect 5.8 1.6  43 340 .012  0      - - error 4.4  2.4  65   260 out of memory 610   600   7800 7000
float-benchs/sin_interpolated_index_true-unreach-call.c error 0 wit inspect 420   420    4900 640 .20   0      - - error 5.0  2.7  59   270 out of memory 130   130   1700 7000
float-benchs/sin_interpolated_negation_true-unreach-call.c error 0 wit inspect 29   11    210 2300 0      0      - - error 6.5  3.5  60   270 out of memory 510   500   9900 7000
float-benchs/sin_interpolated_smallrange_true-unreach-call.c error 0 wit inspect 30   11    250 2100 0      0      - - error 6.2  3.3  52   290 out of memory 660   640   9900 7000
float-benchs/sqrt_Householder_constant_true-unreach-call.c true 2 wit inspect 5.2 1.4  36 290 .0041 0      - - timeout 900    900    26000   1600 error 600   590   13000 2900
float-benchs/sqrt_Householder_interval_true-unreach-call.c timeout 0 wit inspect 900   880    12000 2400 0      0      - - timeout 910    900    17000   1200 error 27   20   640 820
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c timeout 0 wit inspect 900   890    10000 2300 0      0      - - timeout 900    900    18000   2000 error 34   25   440 850
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c timeout 0 wit inspect 900   890    11000 3400 0      0      - - timeout 900    900    20000   3100 error 27   21   560 750
float-benchs/sqrt_biNewton_pseudoconstant_true-unreach-call.c timeout 0 wit inspect 900   890    9000 2300 0      0      - - timeout 900    900    17000   2100 error 26   19   350 850
float-benchs/sqrt_poly_true-unreach-call.c true 2 wit inspect 160   79    1400 820 .0041 0      - - true 95    93    1900   470 true 560   550   6300 1400
float-benchs/water_pid_true-unreach-call.c true 2 wit inspect 6.9 1.8  50 410 .0041 0      - - timeout 900    900    13000   1300 error 380   370   6300 3400
float-benchs/zonotope_2_true-unreach-call.c timeout 0 wit inspect 900   440    6200 3100 0      0      - - timeout 900    900    23000   930 timeout 960   950   16000 1000
float-benchs/zonotope_3_true-unreach-call.c true 2 wit inspect 13   2.6  77 570 0      0      - - true 7.9  5.6  140   410 timeout 960   840   16000 5100
float-benchs/zonotope_loose_true-unreach-call.c true 2 wit inspect 5.5 1.7  43 390 .0041 0      - - true 4.4  2.8  90   320 true 670   670   8200 1400
float-benchs/zonotope_tight_true-unreach-call.c true 2 wit inspect 5.5 1.8  41 380 .0041 0      - - true 5.1  3.3  62   320 true 620   620   7200 1200
floats-esbmc-regression/Double_div_true-unreach-call.i true 2 wit inspect 6.0 1.7  46 470 0      0      - - true 6.2  3.9  71   330 true 410   400   5700 2600
floats-esbmc-regression/Float_div_true-unreach-call.i true 2 wit inspect 3.9 1.2  30 290 .0041 0      - - true 4.3  2.5  83   290 true 260   250   4800 670
floats-esbmc-regression/ceil_nondet_true-unreach-call.i error 0 wit inspect 6.7 1.8  49 450 .22   0      - - error 5.6  3.0  110   280 unknown 11   5.8 180 310
floats-esbmc-regression/ceil_true-unreach-call.i true 2 wit inspect 3.5 1.1  28 270 .0041 0      - - true 5.2  2.8  110   260 unknown 6.3 3.3 120 290
floats-esbmc-regression/copysign_true-unreach-call.i true 2 wit inspect 3.6 1.2  28 280 .0041 .77   - - true 6.1  3.3  85   270 unknown 6.8 3.6 140 310
floats-esbmc-regression/digits_for_true-unreach-call.i true 2 wit inspect 3.4 1.1  27 280 .0041 0      - - timeout 900    900    16000   1000 timeout 960   950   15000 1400
floats-esbmc-regression/digits_while_true-unreach-call.i true 2 wit inspect 3.4 1.1  28 270 .0041 0      - - timeout 900    900    20000   980 timeout 960   950   14000 3100
floats-esbmc-regression/fabs_true-unreach-call.i true 2 wit inspect 5.0 1.4  37 280 .066  0      - - true 6.7  3.7  79   280 true 13   6.9 220 300
floats-esbmc-regression/fdim_true-unreach-call.i true 2 wit inspect 3.4 1.1  27 270 .0041 0      - - true 6.4  3.5  67   270 unknown 5.8 3.1 84 300
floats-esbmc-regression/floor_nondet_true-unreach-call.i error 0 wit inspect 6.6 1.7  50 450 .22   0      - - error 6.5  3.5  80   270 unknown 10   5.6 180 310
floats-esbmc-regression/floor_true-unreach-call.i true 2 wit inspect 3.5 1.2  29 270 .0041 .016  - - true 5.5  3.0  86   260 unknown 6.5 3.5 120 310
floats-esbmc-regression/fmax_true-unreach-call.i true 2 wit inspect 3.7 1.2  29 270 .0041 0      - - true 5.3  2.9  110   270 unknown 6.7 3.5 130 310
floats-esbmc-regression/fmin_true-unreach-call.i true 2 wit inspect 3.5 1.2  31 290 .0041 0      - - true 5.2  2.8  75   270 unknown 6.2 3.3 110 310
floats-esbmc-regression/fmod2_true-unreach-call.i false(unreach-call) -16 wit inspect 6.0 1.6  43 330 .16   0      - - false(unreach-call) 9.1  4.9  77   310 unknown 11   5.7 200 300
floats-esbmc-regression/fmod3_true-unreach-call.i false(unreach-call) -16 wit inspect 5.6 1.5  39 310 .16   0      - - false(unreach-call) 7.9  4.2  150   310 unknown 12   6.4 200 330
floats-esbmc-regression/fmod_true-unreach-call.i true 2 wit inspect 3.6 1.2  28 270 .0041 0      - - true 5.6  3.0  120   290 unknown 6.3 3.3 120 310
floats-esbmc-regression/isgreater_true-unreach-call.i true 2 wit inspect 3.5 1.2  27 270 .0041 0      - - true 6.5  3.5  76   270 error 11   5.7 210 300
floats-esbmc-regression/isgreaterequal_true-unreach-call.i true 2 wit inspect 3.7 1.3  29 280 .0041 8.9    - - true 5.1  2.8  94   270 error 11   5.9 250 310
floats-esbmc-regression/isless_true-unreach-call.i true 2 wit inspect 3.5 1.2  29 270 .0041 .77   - - true 6.1  3.3  79   270 error 12   6.6 170 300
floats-esbmc-regression/islessequal_true-unreach-call.i true 2 wit inspect 3.5 1.2  31 270 .0041 0      - - true 5.3  2.9  89   270 error 11   5.8 220 300
floats-esbmc-regression/islessgreater_true-unreach-call.i true 2 wit inspect 3.6 1.3  30 280 .0041 8.8    - - true 5.3  2.9  110   270 error 11   5.9 230 300
floats-esbmc-regression/isunordered_true-unreach-call.i true 2 wit inspect 3.4 1.2  27 270 .0041 0      - - true 6.4  3.5  65   270 error 11   5.8 180 300
floats-esbmc-regression/lrint_true-unreach-call.i error 0 wit inspect 7.5 1.9  54 460 .94   0      - - error 5.6  3.0  100   280 unknown 7.4 3.9 100 310
floats-esbmc-regression/modf_true-unreach-call.i true 2 wit inspect 3.5 1.2  31 270 .0041 0      - - true 6.1  3.3  82   280 unknown 7.0 3.7 140 300
floats-esbmc-regression/nan_true-unreach-call.i true 2 wit inspect 3.5 1.2  25 270 .0041 .79   - - true 6.1  3.3  84   280 true 13   7.2 220 310
floats-esbmc-regression/nearbyint2_true-unreach-call.i error 0 wit inspect 7.7 1.9  60 450 1.0    0      - - error 6.5  3.5  71   270 unknown 5.8 3.1 100 290
floats-esbmc-regression/nearbyint_true-unreach-call.i error 0 wit inspect 11   2.6  72 520 2.9    0      - - error 7.3  3.9  140   300 unknown 6.7 3.6 130 300
floats-esbmc-regression/remainder_true-unreach-call.i true 2 wit inspect 3.8 1.2  28 270 .0041 3.1    - - true 6.2  3.3  83   280 unknown 6.7 3.6 120 310
floats-esbmc-regression/rint2_true-unreach-call.i error 0 wit inspect 8.0 2.0  61 460 1.0    0      - - error 5.8  3.1  90   270 unknown 6.6 3.5 130 310
floats-esbmc-regression/rint_true-unreach-call.i error 0 wit inspect 11   2.5  84 520 2.9    0      - - error 8.0  4.3  120   290 unknown 6.3 3.4 130 300
floats-esbmc-regression/round_nondet_true-unreach-call.i error 0 wit inspect 7.4 1.9  59 450 .22   0      - - error 6.7  3.6  70   270 unknown 11   5.9 180 310
floats-esbmc-regression/round_true-unreach-call.i true 2 wit inspect 3.8 1.2  31 280 .0041 0      - - true 5.6  3.0  87   280 unknown 7.2 3.8 130 330
floats-esbmc-regression/rounding_functions_true-unreach-call.i true 2 wit inspect 4.3 1.3  36 300 .0041 0      - - true 7.9  4.2  63   270 unknown 6.3 3.3 120 310
floats-esbmc-regression/trunc_nondet_2_true-unreach-call.i false(unreach-call) -16 wit inspect 5.6 1.5  38 310 .070  0      - - unknown 8.8  4.7  80   320 unknown 11   5.8 190 300
floats-esbmc-regression/trunc_nondet_true-unreach-call.i error 0 wit inspect 6.4 1.6  46 450 .22   0      - - error 5.9  3.2  100   270 unknown 11   6.1 170 310
floats-esbmc-regression/trunc_true-unreach-call.i true 2 wit inspect 3.6 1.2  30 270 .0041 0      - - true 5.2  2.9  90   270 unknown 6.4 3.4 140 300
floats-esbmc-regression/Double_div_bad_false-unreach-call.i timeout 0 wit inspect 900   890    8800 2300 0      0      timeout 92    90    1100   1100 error 17   11   240 570 - -
floats-esbmc-regression/Float_div_bad_false-unreach-call.i false(unreach-call) 1 wit inspect 11   3.1  83 530 .086  0      timeout 92    90    1200   660 timeout 97   90   980 620 - -
floats-esbmc-regression/digits_bad_for_false-unreach-call.i false(unreach-call) 1 wit inspect 7.1 1.7  44 400 .029  0      timeout 92    90    1800   600 timeout 97   90   1900 620 - -
floats-esbmc-regression/digits_bad_while_false-unreach-call.i false(unreach-call) 1 wit inspect 8.6 1.9  57 470 .037  0      timeout 92    90    1300   620 error 15   9.4 280 360 - -
../../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 107 43000 25000   300000 420000 15    44     172 1200 1200 17000 16000   172 1600 1500 25000 48000   172 40000 40000 830000 87000   172 26000 25000 450000 290000  
    correct results 107 187 5700 3100   37000 79000 3.6  42     18 1100 1100 16000 15000   11 1600 1400 24000 47000   73 6900 6700 140000 39000   44 11000 9900 170000 70000  
        correct true 80 160 1900 1200   14000 46000 2.9  33     0 0 0 0 0   0 0 0 0 0   73 6900 6700 140000 39000   44 11000 9900 170000 70000  
        correct false 27 27 3800 1900   23000 33000 .64 9.6   18 1100 1100 16000 15000   11 1600 1400 24000 47000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 5 -80 27 7.5 200 1600 .49 .020 0 0 0 0 0   0 0 0 0 0   3 37 20 520 1500   0 54 29 930 1600  
        incorrect true 0
        incorrect false 5 -80 27 7.5 200 1600 .49 .020 0 0 0 0 0   0 0 0 0 0   3 37 20 520 1500   0 54 29 930 1600  
score (172 tasks, max score: 314) 107
Run set sv-comp17.ReachSafety-Floats