Tool ESBMC ESBMC version 3.1 64-bit x86_64 linux
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-11 15:09:43 CET [[ 2017-01-14 22:26:56 CET ]] [[ 2017-01-14 23:59:25 CET ]] [[ 2017-01-14 22:42:14 CET ]] [[ 2017-01-15 00:15:34 CET ]]
Run set sv-comp17.ReachSafety-Floats
Options -s falsi [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-11_1509.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 timeout 0 wit inspect 900     900     9400    470 .84 0   error (invalid witness file) .51 .33 11   41 error (invalid witness file) 5.7 3.0 80 300 - -
floats-cdfpl/newton_1_5_false-unreach-call.i timeout 0 wit inspect 900     900     8300    480 .84 0   error (invalid witness file) .54 .34 12   41 error (invalid witness file) 6.9 3.6 100 310 - -
floats-cdfpl/newton_1_6_false-unreach-call.i timeout 0 wit inspect 900     900     7400    440 .84 0   error (invalid witness file) .71 .45 8.8 45 error (invalid witness file) 6.3 3.3 71 300 - -
floats-cdfpl/newton_1_7_false-unreach-call.i timeout 0 wit inspect 900     900     6700    460 .84 0   error (invalid witness file) .50 .31 12   39 error (invalid witness file) 6.0 3.2 110 300 - -
floats-cdfpl/newton_1_8_false-unreach-call.i false(unreach-call) 1 wit inspect 880     880     7700    460 .99 0   false(unreach-call) 26    24    330   700 false(unreach-call) 30   24   490 990 - -
floats-cdfpl/newton_2_6_false-unreach-call.i timeout 0 wit inspect 900     900     7200    760 .84 0   error (invalid witness file) .61 .39 7.8 43 error (invalid witness file) 6.3 3.3 70 320 - -
floats-cdfpl/newton_2_7_false-unreach-call.i timeout 0 wit inspect 900     900     7300    760 .84 0   error (invalid witness file) .49 .32 9.7 39 error (invalid witness file) 6.4 3.3 75 300 - -
floats-cdfpl/newton_2_8_false-unreach-call.i timeout 0 wit inspect 900     900     8000    760 .84 0   error (invalid witness file) .52 .34 5.3 42 error (invalid witness file) 6.7 3.5 92 310 - -
floats-cdfpl/newton_3_6_false-unreach-call.i timeout 0 wit inspect 900     900     7800    1100 .84 0   error (invalid witness file) .56 .34 12   40 error (invalid witness file) 5.9 3.2 110 300 - -
floats-cdfpl/newton_3_7_false-unreach-call.i timeout 0 wit inspect 900     900     8500    1100 .84 0   error (invalid witness file) .67 .42 8.2 41 error (invalid witness file) 6.1 3.2 130 300 - -
floats-cdfpl/newton_3_8_false-unreach-call.i timeout 0 wit inspect 900     900     8700    1100 .84 0   error (invalid witness file) .55 .36 13   42 error (invalid witness file) 5.7 3.0 100 290 - -
floats-cdfpl/sine_1_false-unreach-call.i false(unreach-call) 1 wit inspect 170     170     1600    240 .84 0   true 4.2  2.4  48   270 false(unreach-call) 29   22   370 890 - -
floats-cdfpl/sine_2_false-unreach-call.i false(unreach-call) 1 wit inspect 92     92     710    190 .84 0   true 4.1  2.3  51   270 timeout 97   91   1200 3000 - -
floats-cdfpl/sine_3_false-unreach-call.i false(unreach-call) 1 wit inspect 62     62     510    180 .84 0   true 3.9  2.2  34   270 timeout (false(unreach-call)) 93   87   840 3400 - -
floats-cdfpl/square_1_false-unreach-call.i false(unreach-call) 1 wit inspect 540     540     5600    200 .84 0   true 3.7  2.0  51   290 false(unreach-call) 46   40   690 980 - -
floats-cdfpl/square_2_false-unreach-call.i timeout 0 wit inspect 900     900     8000    350 .84 0   error (invalid witness file) .54 .36 11   39 error (invalid witness file) 6.7 3.6 77 300 - -
floats-cdfpl/square_3_false-unreach-call.i timeout 0 wit inspect 900     900     7000    350 .84 0   error (invalid witness file) .52 .35 8.3 41 error (invalid witness file) 5.7 3.1 89 300 - -
floats-cdfpl/newton_1_1_true-unreach-call.i timeout 0 wit inspect 900     900     7200    450 .84 0   - - error (invalid witness file) .49 .31 8.4 39 error (invalid witness file) 5.5 2.9 110 290
floats-cdfpl/newton_1_2_true-unreach-call.i timeout 0 wit inspect 900     900     6900    460 .84 0   - - error (invalid witness file) .52 .33 9.5 39 error (invalid witness file) 7.0 3.7 130 320
floats-cdfpl/newton_1_3_true-unreach-call.i timeout 0 wit inspect 900     900     6800    460 .84 0   - - error (invalid witness file) .51 .33 9.5 41 error (invalid witness file) 6.6 3.5 150 320
floats-cdfpl/newton_2_1_true-unreach-call.i timeout 0 wit inspect 900     900     7900    740 .84 0   - - error (invalid witness file) .49 .32 11   40 error (invalid witness file) 6.4 3.4 130 300
floats-cdfpl/newton_2_2_true-unreach-call.i timeout 0 wit inspect 900     900     6500    770 .84 0   - - error (invalid witness file) .55 .34 10   40 error (invalid witness file) 5.6 3.0 95 300
floats-cdfpl/newton_2_3_true-unreach-call.i timeout 0 wit inspect 900     900     8200    760 .84 0   - - error (invalid witness file) .50 .32 9.7 41 error (invalid witness file) 5.6 3.0 110 300
floats-cdfpl/newton_2_4_true-unreach-call.i timeout 0 wit inspect 900     900     7000    740 .84 0   - - error (invalid witness file) .53 .35 12   39 error (invalid witness file) 5.9 3.1 120 300
floats-cdfpl/newton_2_5_true-unreach-call.i timeout 0 wit inspect 900     900     8000    760 .84 0   - - error (invalid witness file) .52 .34 12   41 error (invalid witness file) 5.9 3.1 130 300
floats-cdfpl/newton_3_1_true-unreach-call.i timeout 0 wit inspect 900     900     7500    1100 .84 0   - - error (invalid witness file) .52 .33 11   40 error (invalid witness file) 6.1 3.3 120 300
floats-cdfpl/newton_3_2_true-unreach-call.i timeout 0 wit inspect 900     900     8300    1100 .84 0   - - error (invalid witness file) .48 .32 13   39 error (invalid witness file) 6.3 3.3 120 300
floats-cdfpl/newton_3_3_true-unreach-call.i timeout 0 wit inspect 900     900     6600    1000 .84 0   - - error (invalid witness file) .50 .32 12   39 error (invalid witness file) 6.2 3.3 84 300
floats-cdfpl/newton_3_4_true-unreach-call.i timeout 0 wit inspect 900     900     7500    940 .84 0   - - error (invalid witness file) .53 .35 13   39 error (invalid witness file) 6.8 3.6 98 300
floats-cdfpl/newton_3_5_true-unreach-call.i timeout 0 wit inspect 900     900     7200    1100 .84 0   - - error (invalid witness file) .50 .33 8.1 40 error (invalid witness file) 6.2 3.3 120 290
floats-cdfpl/sine_4_true-unreach-call.i timeout 0 wit inspect 900     900     8800    300 .84 0   - - error (invalid witness file) .51 .33 9.0 41 error (invalid witness file) 5.9 3.1 88 310
floats-cdfpl/sine_5_true-unreach-call.i timeout 0 wit inspect 900     900     8300    300 .84 0   - - error (invalid witness file) .49 .32 12   39 error (invalid witness file) 6.1 3.2 110 300
floats-cdfpl/sine_6_true-unreach-call.i timeout 0 wit inspect 900     900     8400    310 .84 0   - - error (invalid witness file) .53 .34 12   40 error (invalid witness file) 5.9 3.2 110 300
floats-cdfpl/sine_7_true-unreach-call.i timeout 0 wit inspect 900     900     7200    300 .84 0   - - error (invalid witness file) .72 .45 6.4 43 error (invalid witness file) 5.9 3.1 100 290
floats-cdfpl/sine_8_true-unreach-call.i timeout 0 wit inspect 900     900     7300    300 .84 0   - - error (invalid witness file) .51 .33 11   41 error (invalid witness file) 6.3 3.3 120 290
floats-cdfpl/square_4_true-unreach-call.i timeout 0 wit inspect 900     900     6700    250 .84 0   - - error (invalid witness file) .51 .34 7.1 40 error (invalid witness file) 6.0 3.2 130 300
floats-cdfpl/square_5_true-unreach-call.i timeout 0 wit inspect 900     900     6200    350 .84 0   - - error (invalid witness file) .50 .32 11   40 error (invalid witness file) 6.3 3.3 130 300
floats-cdfpl/square_6_true-unreach-call.i timeout 0 wit inspect 900     900     7500    350 .84 0   - - error (invalid witness file) .48 .31 7.0 39 error (invalid witness file) 6.7 3.5 120 320
floats-cdfpl/square_7_true-unreach-call.i timeout 0 wit inspect 900     900     8800    250 .84 0   - - error (invalid witness file) .49 .31 7.4 39 error (invalid witness file) 6.3 3.3 140 300
floats-cdfpl/square_8_true-unreach-call.i timeout 0 wit inspect 900     900     6200    200 .84 0   - - error (invalid witness file) .51 .32 9.4 40 error (invalid witness file) 5.9 3.1 120 300
floats-cbmc-regression/float-div1_true-unreach-call.i timeout 0 wit inspect 900     900     12000    3400 .84 0   - - error (invalid witness file) .68 .44 8.5 44 error (invalid witness file) 5.9 3.2 110 290
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i timeout 0 wit inspect 900     890     14000    420 .84 0   - - error (invalid witness file) .49 .33 9.2 40 error (invalid witness file) 6.5 3.4 120 310
floats-cbmc-regression/float-no-simp1_true-unreach-call.i timeout 0 wit inspect 900     830     12000    9500 .84 0   - - error (invalid witness file) .50 .33 11   40 error (invalid witness file) 6.0 3.2 120 290
floats-cbmc-regression/float-no-simp2_true-unreach-call.i timeout 0 wit inspect 900     900     9000    230 .84 0   - - error (invalid witness file) .50 .32 10   39 error (invalid witness file) 6.2 3.3 130 300
floats-cbmc-regression/float-no-simp3_true-unreach-call.i timeout 0 wit inspect 900     830     12000    9300 .84 0   - - error (invalid witness file) .53 .36 9.5 43 error (invalid witness file) 6.2 3.3 130 300
floats-cbmc-regression/float-no-simp4_true-unreach-call.i out of memory 0 wit inspect 200     200     2600    15000 .84 0   - - error (invalid witness file) .61 .41 6.2 40 error (invalid witness file) 6.2 3.3 120 310
floats-cbmc-regression/float-no-simp6_true-unreach-call.i timeout 0 wit inspect 900     860     12000    7000 .84 0   - - error (invalid witness file) .48 .31 7.5 40 error (invalid witness file) 6.5 3.4 120 320
floats-cbmc-regression/float-no-simp7_true-unreach-call.i timeout 0 wit inspect 900     850     12000    11000 .84 0   - - error (invalid witness file) .53 .35 12   42 error (invalid witness file) 5.9 3.2 120 300
floats-cbmc-regression/float-no-simp8_true-unreach-call.i timeout 0 wit inspect 900     830     12000    5500 .84 0   - - error (invalid witness file) .52 .32 9.2 40 error (invalid witness file) 7.2 3.9 89 290
floats-cbmc-regression/float-rounding1_true-unreach-call.i out of memory 0 wit inspect 520     520     6800    15000 .84 0   - - error (invalid witness file) .57 .35 9.9 39 error (invalid witness file) 6.5 3.4 130 300
floats-cbmc-regression/float-to-double1_true-unreach-call.i timeout 0 wit inspect 900     900     11000    1300 .84 0   - - error (invalid witness file) .47 .31 9.7 40 error (invalid witness file) 5.7 3.1 110 300
floats-cbmc-regression/float-to-double2_true-unreach-call.i timeout 0 wit inspect 900     830     13000    8800 .84 0   - - error (invalid witness file) .52 .34 9.4 44 error (invalid witness file) 5.7 3.0 130 290
floats-cbmc-regression/float-zero-sum1_true-unreach-call.i out of memory 0 wit inspect 64     59     790    15000 .84 0   - - error (invalid witness file) .53 .35 11   41 error (invalid witness file) 6.0 3.1 110 300
floats-cbmc-regression/float11_true-unreach-call.i timeout 0 wit inspect 900     830     13000    3000 .84 0   - - error (invalid witness file) .52 .33 11   40 error (invalid witness file) 6.1 3.2 120 300
floats-cbmc-regression/float12_true-unreach-call.i timeout 0 wit inspect 900     900     11000    5400 .84 0   - - error (invalid witness file) .56 .36 9.7 41 error (invalid witness file) 6.9 3.6 120 310
floats-cbmc-regression/float13_true-unreach-call.i timeout 0 wit inspect 900     860     15000    5100 .84 0   - - error (invalid witness file) .50 .32 9.8 41 error (invalid witness file) 6.1 3.2 130 290
floats-cbmc-regression/float14_true-unreach-call.i timeout 0 wit inspect 900     860     11000    4700 .84 0   - - error (invalid witness file) .49 .32 11   40 error (invalid witness file) 5.7 3.1 120 290
floats-cbmc-regression/float18_true-unreach-call.i timeout 0 wit inspect 900     880     13000    3700 .84 0   - - error (invalid witness file) .50 .33 10   40 error (invalid witness file) 5.8 3.1 120 290
floats-cbmc-regression/float19_true-unreach-call.i timeout 0 wit inspect 900     900     14000    6200 .84 0   - - error (invalid witness file) .48 .30 6.9 39 error (invalid witness file) 6.6 3.5 130 300
floats-cbmc-regression/float1_true-unreach-call.i timeout 0 wit inspect 900     840     11000    7800 .84 0   - - error (invalid witness file) .51 .33 4.6 40 error (invalid witness file) 6.2 3.2 110 300
floats-cbmc-regression/float20_true-unreach-call.i timeout 0 wit inspect 900     900     8400    3200 .84 0   - - error (invalid witness file) .48 .33 9.1 43 error (invalid witness file) 5.7 3.0 110 290
floats-cbmc-regression/float21_true-unreach-call.i timeout 0 wit inspect 900     900     13000    1400 .84 0   - - error (invalid witness file) .50 .32 13   40 error (invalid witness file) 6.6 3.5 130 310
floats-cbmc-regression/float22_true-unreach-call.i unknown 0 wit inspect .078 .078 .81 24 .84 0   - - error (invalid witness file) .50 .34 4.2 39 error (invalid witness file) 6.0 3.2 120 300
floats-cbmc-regression/float2_true-unreach-call.i timeout 0 wit inspect 900     840     12000    7600 .84 0   - - error (invalid witness file) .55 .35 7.4 43 error (invalid witness file) 6.4 3.4 130 310
floats-cbmc-regression/float3_true-unreach-call.i timeout 0 wit inspect 900     900     10000    7300 .84 0   - - error (invalid witness file) .50 .34 4.0 40 error (invalid witness file) 5.7 3.1 110 290
floats-cbmc-regression/float4_true-unreach-call.i timeout 0 wit inspect 900     900     9500    230 .84 0   - - error (invalid witness file) .57 .38 7.8 40 error (invalid witness file) 6.2 3.3 110 310
floats-cbmc-regression/float5_true-unreach-call.i timeout 0 wit inspect 900     900     11000    2300 .84 0   - - error (invalid witness file) .49 .31 11   40 error (invalid witness file) 5.5 3.0 110 290
floats-cbmc-regression/float6_true-unreach-call.i out of memory 0 wit inspect 510     490     980    15000 .84 0   - - error (invalid witness file) .54 .35 12   43 error (invalid witness file) 5.9 3.1 120 300
floats-cbmc-regression/float7_true-unreach-call.i out of memory 0 wit inspect 45     44     600    15000 .84 0   - - error (invalid witness file) .55 .37 11   44 error (invalid witness file) 5.8 3.1 120 300
floats-cbmc-regression/float8_true-unreach-call.i out of memory 0 wit inspect 64     59     870    15000 .84 0   - - error (invalid witness file) .50 .32 8.4 40 error (invalid witness file) 6.2 3.3 120 300
floats-cbmc-regression/float_lib1_true-unreach-call.i timeout 0 wit inspect 900     850     12000    1000 .99 0   - - error (invalid witness file) .48 .32 13   41 error (invalid witness file) 6.4 3.4 120 300
floats-cbmc-regression/float_lib2_true-unreach-call.i timeout 0 wit inspect 900     840     13000    1300 .84 0   - - error (invalid witness file) .51 .33 12   39 error (invalid witness file) 6.5 3.4 93 320
float-benchs/cast_float_ptr_false-unreach-call.c false(unreach-call) 1 wit inspect .092 .091 1.1  23 .84 0   assertion 2.6  1.5  44   160 unknown 6.0 3.2 96 300 - -
float-benchs/cast_union_loose_false-unreach-call.c false(unreach-call) 1 wit inspect .21  .21  2.4  27 .84 0   true 3.8  2.1  56   270 unknown 6.2 3.3 100 300 - -
float-benchs/cast_union_tight_false-unreach-call.c false(unreach-call) 1 wit inspect .89  .89  10    37 .84 0   assertion 2.5  1.4  52   160 unknown 6.0 3.2 99 300 - -
float-benchs/float_int_inv_square_false-unreach-call.c false(unreach-call) 1 wit inspect .42  .42  4.4  33 .84 0   false(unreach-call) 3.9  2.2  52   280 false(unreach-call) 14   7.8 250 320 - -
float-benchs/inv_square_false-unreach-call.c false(unreach-call) 1 wit inspect .19  .19  1.7  23 .84 0   true 3.7  2.2  60   290 false(unreach-call) 13   7.2 220 330 - -
float-benchs/nan_double_false-unreach-call.c false(unreach-call) 1 wit inspect .10  .10  .72 23 .84 0   true 3.9  2.2  28   270 false(unreach-call) 8.8 4.7 69 310 - -
float-benchs/nan_float_false-unreach-call.c false(unreach-call) 1 wit inspect .098 .098 .77 23 .84 0   true 3.5  2.0  64   270 false(unreach-call) 8.9 4.6 74 310 - -
float-benchs/sin_interpolated_index_false-unreach-call.c false(unreach-call) 1 wit inspect 260     260     2100    880 .84 0   unknown 4.1  2.3  65   270 timeout 97   90   1100 3400 - -
float-benchs/sqrt_poly2_false-unreach-call.c false(unreach-call) 1 wit inspect 340     340     2700    340 .84 0   assertion 2.5  1.4  40   170 error 9.8 5.2 68 300 - -
float-benchs/Muller_Kahan_true-unreach-call.c timeout 0 wit inspect 900     850     13000    2100 .84 0   - - error (invalid witness file) .54 .34 9.6 40 error (invalid witness file) 6.3 3.4 110 300
float-benchs/Rump_double_true-unreach-call.c timeout 0 wit inspect 900     840     11000    3300 .84 0   - - error (invalid witness file) .51 .33 6.6 40 error (invalid witness file) 6.0 3.1 130 300
float-benchs/Rump_float_true-unreach-call.c timeout 0 wit inspect 900     830     13000    3800 .84 0   - - error (invalid witness file) .62 .41 5.2 41 error (invalid witness file) 6.1 3.2 120 300
float-benchs/addsub_double_exact_true-unreach-call.c timeout 0 wit inspect 900     850     14000    9100 .84 0   - - error (invalid witness file) .50 .33 12   41 error (invalid witness file) 5.8 3.1 99 300
float-benchs/addsub_float_exact_true-unreach-call.c timeout 0 wit inspect 900     850     11000    9400 .84 0   - - error (invalid witness file) .51 .33 8.9 40 error (invalid witness file) 5.7 3.0 130 300
float-benchs/addsub_float_inexact_true-unreach-call.c timeout 0 wit inspect 900     850     12000    9500 .84 0   - - error (invalid witness file) .49 .31 9.0 39 error (invalid witness file) 5.1 2.8 100 280
float-benchs/arctan_Pade_true-unreach-call.c timeout 0 wit inspect 900     900     7300    1100 .84 0   - - error (invalid witness file) .52 .32 12   40 error (invalid witness file) 6.4 3.4 130 310
float-benchs/bary_diverge_true-unreach-call.c timeout 0 wit inspect 900     900     11000    2000 .84 0   - - error (invalid witness file) .51 .33 7.4 40 error (invalid witness file) 5.4 2.9 100 290
float-benchs/cast_float_union_true-unreach-call.c timeout 0 wit inspect 900     860     12000    12000 .84 0   - - error (invalid witness file) .48 .32 6.8 40 error (invalid witness file) 6.2 3.3 110 300
float-benchs/cos_polynomial_true-unreach-call.c timeout 0 wit inspect 900     900     8300    610 .84 0   - - error (invalid witness file) .61 .40 7.7 41 error (invalid witness file) 6.1 3.2 130 300
float-benchs/divmul_buf_diverge_true-unreach-call.c timeout 0 wit inspect 900     890     11000    490 .84 0   - - error (invalid witness file) .69 .44 9.9 40 error (invalid witness file) 6.0 3.2 100 300
float-benchs/divmul_diverge_true-unreach-call.c timeout 0 wit inspect 900     890     12000    480 .84 0   - - error (invalid witness file) .58 .36 9.1 41 error (invalid witness file) 5.7 3.0 100 300
float-benchs/drift_tenth_true-unreach-call.c timeout 0 wit inspect 900     820     11000    6900 .84 0   - - error (invalid witness file) .47 .30 4.5 39 error (invalid witness file) 6.5 3.4 120 300
float-benchs/exp_loop_true-unreach-call.c timeout 0 wit inspect 900     900     12000    1400 .96 0   - - error (invalid witness file) .50 .32 4.7 41 error (invalid witness file) 7.4 3.8 150 320
float-benchs/feedback_diverge_true-unreach-call.c timeout 0 wit inspect 900     890     11000    520 .84 0   - - error (invalid witness file) .61 .37 8.1 39 error (invalid witness file) 5.9 3.1 120 300
float-benchs/filter1_true-unreach-call.c timeout 0 wit inspect 900     900     8500    260 .84 0   - - error (invalid witness file) .52 .33 11   42 error (invalid witness file) 6.2 3.3 120 310
float-benchs/filter2_alt_true-unreach-call.c timeout 0 wit inspect 900     900     8000    250 .84 0   - - error (invalid witness file) .58 .37 14   44 error (invalid witness file) 5.6 3.0 110 300
float-benchs/filter2_iterated_true-unreach-call.c out of memory 0 wit inspect 540     540     7000    15000 .84 0   - - error (invalid witness file) .50 .33 11   40 error (invalid witness file) 5.3 2.9 80 290
float-benchs/filter2_reinit_true-unreach-call.c timeout 0 wit inspect 900     900     7200    240 .84 0   - - error (invalid witness file) .50 .32 11   39 error (invalid witness file) 6.0 3.2 110 290
float-benchs/filter2_set_true-unreach-call.c timeout 0 wit inspect 900     900     8700    530 .84 0   - - error (invalid witness file) .57 .37 12   43 error (invalid witness file) 6.0 3.2 120 300
float-benchs/filter2_true-unreach-call.c timeout 0 wit inspect 900     900     9300    380 .84 0   - - error (invalid witness file) .53 .35 10   42 error (invalid witness file) 6.2 3.2 110 300
float-benchs/filter_iir_true-unreach-call.c timeout 0 wit inspect 900     900     8100    420 .84 0   - - error (invalid witness file) .63 .40 6.0 39 error (invalid witness file) 6.2 3.3 110 300
float-benchs/float_double_true-unreach-call.c timeout 0 wit inspect 900     840     11000    9900 .84 0   - - error (invalid witness file) .49 .31 9.9 39 error (invalid witness file) 6.2 3.2 130 300
float-benchs/image_filter_true-unreach-call.c timeout 0 wit inspect 900     900     11000    2200 .84 0   - - error (invalid witness file) .52 .33 12   39 error (invalid witness file) 6.0 3.2 120 310
float-benchs/interpolation2_true-unreach-call.c timeout 0 wit inspect 900     900     9400    270 .84 0   - - error (invalid witness file) .52 .34 13   40 error (invalid witness file) 6.2 3.3 120 310
float-benchs/interpolation_true-unreach-call.c timeout 0 wit inspect 900     900     9100    1000 .84 0   - - error (invalid witness file) .53 .33 9.6 40 error (invalid witness file) 6.1 3.3 120 300
float-benchs/inv_sqrt_Quake_true-unreach-call.c timeout 0 wit inspect 900     900     11000    330 .84 0   - - error (invalid witness file) .58 .38 6.5 42 error (invalid witness file) 6.1 3.2 110 300
float-benchs/inv_square_int_true-unreach-call.c timeout 0 wit inspect 900     900     6500    2500 .84 0   - - error (invalid witness file) .49 .32 11   40 error (invalid witness file) 5.4 2.9 110 290
float-benchs/inv_square_true-unreach-call.c timeout 0 wit inspect 900     900     12000    7500 .99 0   - - error (invalid witness file) .54 .34 11   42 error (invalid witness file) 5.9 3.2 110 300
float-benchs/loop_true-unreach-call.c timeout 0 wit inspect 900     840     12000    2700 .84 0   - - error (invalid witness file) .53 .34 9.4 42 error (invalid witness file) 5.8 3.1 120 300
float-benchs/mea8000_true-unreach-call.c timeout 0 wit inspect 900     900     12000    1100 .84 0   - - error (invalid witness file) .63 .40 9.5 43 error (invalid witness file) 5.8 3.2 130 290
float-benchs/nan_double_range_true-unreach-call.c out of memory 0 wit inspect 57     52     630    15000 .84 0   - - error (invalid witness file) .49 .32 12   39 error (invalid witness file) 6.4 3.3 90 310
float-benchs/nan_float_range_true-unreach-call.c out of memory 0 wit inspect 79     78     1100    15000 .84 0   - - error (invalid witness file) .51 .32 10   41 error (invalid witness file) 5.9 3.2 130 290
float-benchs/rlim_exit_true-unreach-call.c timeout 0 wit inspect 900     900     9200    590 .84 0   - - error (invalid witness file) .49 .32 11   39 error (invalid witness file) 5.7 3.0 110 290
float-benchs/rlim_invariant_true-unreach-call.c timeout 0 wit inspect 900     900     10000    170 .84 0   - - error (invalid witness file) .52 .35 7.0 40 error (invalid witness file) 5.9 3.1 84 300
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call.c timeout 0 wit inspect 900     900     5000    2200 .84 0   - - error (invalid witness file) .50 .32 9.0 39 error (invalid witness file) 6.0 3.2 110 300
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call.c timeout 0 wit inspect 900     900     7000    2400 .84 0   - - error (invalid witness file) .52 .34 8.5 40 error (invalid witness file) 6.1 3.2 130 300
float-benchs/sin_interpolated_index_true-unreach-call.c timeout 0 wit inspect 900     900     7800    930 .84 0   - - error (invalid witness file) .49 .32 8.5 39 error (invalid witness file) 5.8 3.1 100 300
float-benchs/sin_interpolated_negation_true-unreach-call.c timeout 0 wit inspect 900     900     5900    2100 .84 0   - - error (invalid witness file) .52 .33 11   40 error (invalid witness file) 6.0 3.2 99 290
float-benchs/sin_interpolated_smallrange_true-unreach-call.c timeout 0 wit inspect 900     900     7100    2200 .84 0   - - error (invalid witness file) .55 .35 13   44 error (invalid witness file) 6.0 3.2 120 300
float-benchs/sqrt_Householder_constant_true-unreach-call.c timeout 0 wit inspect 900     880     14000    1600 .84 0   - - error (invalid witness file) .54 .34 12   42 error (invalid witness file) 5.7 3.0 120 300
float-benchs/sqrt_Householder_interval_true-unreach-call.c timeout 0 wit inspect 900     900     7900    770 .84 0   - - error (invalid witness file) .49 .32 11   40 error (invalid witness file) 5.8 3.1 87 310
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c timeout 0 wit inspect 900     900     3200    1200 .98 0   - - error (invalid witness file) .48 .32 5.9 39 error (invalid witness file) 7.5 3.9 140 340
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c timeout 0 wit inspect 900     900     8700    1100 .84 0   - - error (invalid witness file) .52 .32 7.9 42 error (invalid witness file) 5.7 3.0 110 290
float-benchs/sqrt_biNewton_pseudoconstant_true-unreach-call.c timeout 0 wit inspect 900     900     7400    1400 .84 0   - - error (invalid witness file) .55 .35 14   43 error (invalid witness file) 5.7 3.0 120 290
float-benchs/sqrt_poly_true-unreach-call.c timeout 0 wit inspect 900     900     10000    490 .84 0   - - error (invalid witness file) .67 .43 6.4 42 error (invalid witness file) 5.7 3.1 100 290
float-benchs/water_pid_true-unreach-call.c timeout 0 wit inspect 900     880     12000    5200 .84 0   - - error (invalid witness file) .51 .33 9.7 40 error (invalid witness file) 6.2 3.3 130 300
float-benchs/zonotope_2_true-unreach-call.c timeout 0 wit inspect 900     880     12000    6000 .84 0   - - error (invalid witness file) .50 .32 11   39 error (invalid witness file) 6.0 3.2 85 300
float-benchs/zonotope_3_true-unreach-call.c timeout 0 wit inspect 900     890     11000    950 .84 0   - - error (invalid witness file) .62 .39 7.9 40 error (invalid witness file) 5.6 3.0 100 290
float-benchs/zonotope_loose_true-unreach-call.c timeout 0 wit inspect 900     900     10000    1200 .84 0   - - error (invalid witness file) .63 .39 10   44 error (invalid witness file) 5.7 3.0 120 290
float-benchs/zonotope_tight_true-unreach-call.c timeout 0 wit inspect 900     900     8300    1000 .84 0   - - error (invalid witness file) .51 .32 8.4 42 error (invalid witness file) 6.6 3.4 130 300
floats-esbmc-regression/Double_div_true-unreach-call.i timeout 0 wit inspect 900     850     11000    2400 .84 0   - - error (invalid witness file) .49 .33 6.4 42 error (invalid witness file) 5.8 3.1 97 300
floats-esbmc-regression/Float_div_true-unreach-call.i timeout 0 wit inspect 900     790     12000    4700 .84 0   - - error (invalid witness file) .50 .33 4.1 42 error (invalid witness file) 6.0 3.2 110 300
floats-esbmc-regression/ceil_nondet_true-unreach-call.i timeout 0 wit inspect 900     900     11000    4800 .84 0   - - error (invalid witness file) .50 .31 12   40 error (invalid witness file) 6.2 3.3 140 300
floats-esbmc-regression/ceil_true-unreach-call.i out of memory 0 wit inspect 150     140     1600    15000 .84 0   - - error (invalid witness file) .51 .32 8.6 40 error (invalid witness file) 6.1 3.2 120 300
floats-esbmc-regression/copysign_true-unreach-call.i timeout 0 wit inspect 900     850     10000    8700 .84 0   - - error (invalid witness file) .51 .33 10   41 error (invalid witness file) 6.4 3.4 130 290
floats-esbmc-regression/digits_for_true-unreach-call.i timeout 0 wit inspect 900     870     13000    1800 .84 0   - - error (invalid witness file) .49 .31 10   40 error (invalid witness file) 5.9 3.1 130 290
floats-esbmc-regression/digits_while_true-unreach-call.i timeout 0 wit inspect 900     870     12000    1800 .84 0   - - error (invalid witness file) .52 .33 10   41 error (invalid witness file) 6.8 3.5 120 310
floats-esbmc-regression/fabs_true-unreach-call.i timeout 0 wit inspect 900     830     11000    9400 .84 0   - - error (invalid witness file) .47 .29 4.0 39 error (invalid witness file) 6.2 3.3 130 310
floats-esbmc-regression/fdim_true-unreach-call.i timeout 0 wit inspect 900     840     12000    10000 .84 0   - - error (invalid witness file) .55 .35 12   44 error (invalid witness file) 6.2 3.3 110 300
floats-esbmc-regression/floor_nondet_true-unreach-call.i timeout 0 wit inspect 900     900     11000    6700 .84 0   - - error (invalid witness file) .50 .32 12   40 error (invalid witness file) 6.0 3.2 120 290
floats-esbmc-regression/floor_true-unreach-call.i out of memory 0 wit inspect 150     140     2100    15000 .84 0   - - error (invalid witness file) .51 .32 11   40 error (invalid witness file) 6.3 3.3 110 310
floats-esbmc-regression/fmax_true-unreach-call.i timeout 0 wit inspect 900     840     14000    11000 .84 0   - - error (invalid witness file) .50 .33 12   40 error (invalid witness file) 6.4 3.4 120 310
floats-esbmc-regression/fmin_true-unreach-call.i timeout 0 wit inspect 900     840     12000    11000 .84 0   - - error (invalid witness file) .62 .40 9.7 40 error (invalid witness file) 5.7 3.1 120 290
floats-esbmc-regression/fmod2_true-unreach-call.i out of memory 0 wit inspect 1.9   1.8   26    15000 .84 0   - - error (invalid witness file) .55 .35 11   40 error (invalid witness file) 6.7 3.5 120 300
floats-esbmc-regression/fmod3_true-unreach-call.i out of memory 0 wit inspect 1.9   1.8   27    15000 .84 0   - - error (invalid witness file) .54 .35 4.4 40 error (invalid witness file) 5.9 3.2 110 290
floats-esbmc-regression/fmod_true-unreach-call.i timeout 0 wit inspect 900     860     11000    7100 .84 0   - - error (invalid witness file) .51 .33 10   41 error (invalid witness file) 6.2 3.2 120 300
floats-esbmc-regression/isgreater_true-unreach-call.i timeout 0 wit inspect 900     850     12000    15000 .84 0   - - error (invalid witness file) .50 .33 10   42 error (invalid witness file) 5.8 3.1 130 290
floats-esbmc-regression/isgreaterequal_true-unreach-call.i timeout 0 wit inspect 900     810     12000    14000 .84 0   - - error (invalid witness file) .49 .32 12   39 error (invalid witness file) 6.5 3.4 120 310
floats-esbmc-regression/isless_true-unreach-call.i timeout 0 wit inspect 900     850     11000    15000 .84 0   - - error (invalid witness file) .56 .35 12   42 error (invalid witness file) 6.0 3.3 120 290
floats-esbmc-regression/islessequal_true-unreach-call.i timeout 0 wit inspect 900     810     11000    14000 .84 0   - - error (invalid witness file) .52 .34 12   42 error (invalid witness file) 5.9 3.1 120 290
floats-esbmc-regression/islessgreater_true-unreach-call.i timeout 0 wit inspect 900     850     12000    13000 .84 0   - - error (invalid witness file) .49 .32 12   40 error (invalid witness file) 7.2 3.8 130 330
floats-esbmc-regression/isunordered_true-unreach-call.i timeout 0 wit inspect 900     840     11000    13000 .99 0   - - error (invalid witness file) .50 .32 11   40 error (invalid witness file) 6.2 3.3 130 300
floats-esbmc-regression/lrint_true-unreach-call.i out of memory 0 wit inspect 7.6   7.4   21    15000 .84 0   - - error (invalid witness file) .51 .34 12   40 error (invalid witness file) 5.6 3.0 110 290
floats-esbmc-regression/modf_true-unreach-call.i out of memory 0 wit inspect 140     130     1800    15000 .84 0   - - error (invalid witness file) .47 .31 6.8 39 error (invalid witness file) 7.5 3.9 100 310
floats-esbmc-regression/nan_true-unreach-call.i timeout 0 wit inspect 900     870     11000    11000 .84 0   - - error (invalid witness file) .51 .33 13   40 error (invalid witness file) 6.0 3.2 120 290
floats-esbmc-regression/nearbyint2_true-unreach-call.i out of memory 0 wit inspect 190     180     2200    15000 .84 0   - - error (invalid witness file) .53 .34 6.5 41 error (invalid witness file) 6.9 3.6 130 320
floats-esbmc-regression/nearbyint_true-unreach-call.i out of memory 0 wit inspect 240     230     2900    15000 .84 0   - - error (invalid witness file) .53 .35 5.8 42 error (invalid witness file) 5.9 3.2 110 300
floats-esbmc-regression/remainder_true-unreach-call.i out of memory 0 wit inspect 2.0   1.9   24    15000 .84 0   - - error (invalid witness file) .51 .32 10   39 error (invalid witness file) 6.4 3.4 100 310
floats-esbmc-regression/rint2_true-unreach-call.i out of memory 0 wit inspect 220     210     2700    15000 .84 0   - - error (invalid witness file) .52 .32 10   40 error (invalid witness file) 5.6 3.0 110 290
floats-esbmc-regression/rint_true-unreach-call.i out of memory 0 wit inspect 260     250     3600    15000 .84 0   - - error (invalid witness file) .57 .37 9.5 43 error (invalid witness file) 6.6 3.5 110 310
floats-esbmc-regression/round_nondet_true-unreach-call.i timeout 0 wit inspect 900     900     10000    3200 .84 0   - - error (invalid witness file) .57 .35 6.6 40 error (invalid witness file) 5.9 3.2 120 300
floats-esbmc-regression/round_true-unreach-call.i out of memory 0 wit inspect 2.3   2.3   33    15000 .84 0   - - error (invalid witness file) .58 .37 6.9 40 error (invalid witness file) 6.7 3.5 100 310
floats-esbmc-regression/rounding_functions_true-unreach-call.i out of memory 0 wit inspect 440     430     5400    15000 .84 0   - - error (invalid witness file) .48 .32 7.0 40 error (invalid witness file) 6.7 3.6 130 320
floats-esbmc-regression/trunc_nondet_2_true-unreach-call.i timeout 0 wit inspect 900     900     11000    3200 .84 0   - - error (invalid witness file) .51 .33 12   40 error (invalid witness file) 6.1 3.2 110 300
floats-esbmc-regression/trunc_nondet_true-unreach-call.i timeout 0 wit inspect 900     900     11000    9600 .84 0   - - error (invalid witness file) .55 .35 11   43 error (invalid witness file) 6.2 3.2 120 300
floats-esbmc-regression/trunc_true-unreach-call.i out of memory 0 wit inspect 160     140     1600    15000 .84 0   - - error (invalid witness file) .52 .34 11   39 error (invalid witness file) 6.4 3.4 130 300
floats-esbmc-regression/Double_div_bad_false-unreach-call.i false(unreach-call) 1 wit inspect 61     57     860    320 .84 0   out of memory 67    61    670   7000 true 6.7 3.6 130 320 - -
floats-esbmc-regression/Float_div_bad_false-unreach-call.i false(unreach-call) 1 wit inspect .84  .76  12    25 .84 0   false(unreach-call) 28    22    420   2000 true 6.8 3.6 100 310 - -
floats-esbmc-regression/digits_bad_for_false-unreach-call.i false(unreach-call) 1 wit inspect .21  .21  2.8  23 .84 0   false(unreach-call) 6.2  3.4  77   290 true 15   8.4 180 300 - -
floats-esbmc-regression/digits_bad_while_false-unreach-call.i false(unreach-call) 1 wit inspect .23  .22  4.9  23 .84 0   false(unreach-call) 6.6  3.5  74   300 true 12   6.8 200 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 18 120000 120000 1400000 800000 150 0   172 190 140 2300 14000 172 580 450 7400 20000 172 75 48 1400 5800   172 870 460 16000 43000  
    correct results 18 18 2400 2400 22000 3100 15 0   13 180 140 2200 14000 11 500 420 6300 16000 0 0 0 0 0   0 0 0 0 0  
        correct true 0
        correct false 18 18 2400 2400 22000 3100 15 0   5 180 140 2200 14000 7 500 420 6300 16000 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) 18
Run set sv-comp17.ReachSafety-Floats