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