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