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