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