Tool symbiotic KLEE:7f3c74aa-dg:96e851cf-symbiotic:69a1d8e6-minisat:3db58943-stp:39fa956f-LLVMInstrumentation:f750b24a
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 11:10:58 CET [[ 2017-01-15 02:01:54 CET ]] [[ 2017-01-15 02:34:25 CET ]] [[ 2017-01-15 02:04:28 CET ]] [[ 2017-01-15 03:02:21 CET ]]
Run set sv-comp17.ReachSafety-Floats
Options --witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-13_1110.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 0 .14  .14  1.7  9.4 .012 0    .59 .37 6.0 40 6.2 3.3 110 300
floats-cdfpl/newton_1_5_false-unreach-call.i 0 .16  .16  1.7  9.4 .012 0    .50 .32 12   40 6.3 3.3 88 300
floats-cdfpl/newton_1_6_false-unreach-call.i 0 .16  .16  1.8  9.4 .012 0    .48 .32 11   41 7.3 3.8 76 290
floats-cdfpl/newton_1_7_false-unreach-call.i 0 .17  .17  1.4  9.4 .012 0    .63 .42 9.0 40 6.2 3.3 140 310
floats-cdfpl/newton_1_8_false-unreach-call.i 0 .17  .16  1.8  9.2 .012 0    .60 .37 10   39 5.6 2.9 81 290
floats-cdfpl/newton_2_6_false-unreach-call.i 0 .16  .16  1.7  9.3 .012 0    .60 .37 9.6 39 7.2 3.8 85 290
floats-cdfpl/newton_2_7_false-unreach-call.i 0 .17  .16  1.6  9.3 .012 0    .56 .36 9.9 39 5.9 3.1 120 290
floats-cdfpl/newton_2_8_false-unreach-call.i 0 .17  .16  1.6  9.4 .012 0    .51 .34 7.7 39 7.0 3.7 86 300
floats-cdfpl/newton_3_6_false-unreach-call.i 0 .16  .16  1.6  9.4 .012 0    .63 .40 11   45 6.3 3.3 77 300
floats-cdfpl/newton_3_7_false-unreach-call.i 0 .14  .14  1.7  9.4 .012 0    .52 .32 9.0 41 6.9 3.6 100 300
floats-cdfpl/newton_3_8_false-unreach-call.i 0 .14  .14  1.9  9.3 .012 0    .49 .32 12   40 7.9 4.1 110 320
floats-cdfpl/sine_1_false-unreach-call.i 0 .14  .14  1.5  9.3 .012 0    .50 .32 14   41 7.1 3.8 69 300
floats-cdfpl/sine_2_false-unreach-call.i 0 .17  .17  1.8  9.4 .012 0    .55 .34 9.2 40 6.5 3.5 73 290
floats-cdfpl/sine_3_false-unreach-call.i 0 .17  .16  1.6  9.2 .012 0    .56 .36 14   43 6.1 3.2 110 300
floats-cdfpl/square_1_false-unreach-call.i 0 .15  .15  1.5  9.3 .012 0    .55 .34 13   42 6.4 3.4 100 300
floats-cdfpl/square_2_false-unreach-call.i 0 .14  .14  1.6  9.3 .012 0    .54 .33 12   39 7.1 3.7 78 300
floats-cdfpl/square_3_false-unreach-call.i 0 .15  .14  1.9  9.4 .012 0    .54 .35 6.5 41 6.9 3.7 77 290
floats-cdfpl/newton_1_1_true-unreach-call.i 0 .16  .15  1.8  9.4 .012 0    .58 .36 12   42 7.9 4.2 73 310
floats-cdfpl/newton_1_2_true-unreach-call.i 0 .18  .18  1.6  9.4 .012 0    .55 .36 9.8 39 5.9 3.1 100 300
floats-cdfpl/newton_1_3_true-unreach-call.i 0 .15  .14  1.4  9.5 .012 0    .51 .32 9.6 41 5.8 3.1 120 300
floats-cdfpl/newton_2_1_true-unreach-call.i 0 .15  .15  1.9  9.4 .012 0    .64 .42 6.5 41 9.1 4.7 79 320
floats-cdfpl/newton_2_2_true-unreach-call.i 0 .14  .14  1.8  9.3 .012 0    .58 .36 8.3 40 6.3 3.4 88 300
floats-cdfpl/newton_2_3_true-unreach-call.i 0 .15  .14  1.7  9.4 .012 0    .59 .38 9.6 40 7.1 3.8 93 300
floats-cdfpl/newton_2_4_true-unreach-call.i 0 .17  .17  1.9  9.4 .012 0    .65 .41 8.9 40 6.7 3.5 100 300
floats-cdfpl/newton_2_5_true-unreach-call.i 0 .18  .18  1.8  9.3 .012 0    .51 .34 11   43 6.1 3.2 130 310
floats-cdfpl/newton_3_1_true-unreach-call.i 0 .16  .16  1.8  9.6 .012 0    .60 .38 5.8 39 7.5 3.9 80 310
floats-cdfpl/newton_3_2_true-unreach-call.i 0 .18  .18  2.0  9.4 .012 0    .54 .35 11   40 8.0 4.2 98 310
floats-cdfpl/newton_3_3_true-unreach-call.i 0 .20  .34  2.4  22   .012 13    .61 .39 8.2 40 6.7 3.6 110 300
floats-cdfpl/newton_3_4_true-unreach-call.i 0 .17  .16  1.8  9.3 .012 0    .50 .32 9.6 41 7.1 3.7 85 300
floats-cdfpl/newton_3_5_true-unreach-call.i 0 .18  .18  1.7  9.4 .012 0    .55 .36 12   40 5.8 3.1 110 300
floats-cdfpl/sine_4_true-unreach-call.i 0 .18  .17  1.9  9.4 .012 0    .48 .32 6.9 39 6.8 3.6 83 300
floats-cdfpl/sine_5_true-unreach-call.i 0 .17  .17  1.7  9.3 .012 0    .49 .32 9.8 39 7.4 3.9 87 300
floats-cdfpl/sine_6_true-unreach-call.i 0 .18  .17  1.7  9.4 .012 0    .60 .39 7.4 40 6.8 3.5 97 290
floats-cdfpl/sine_7_true-unreach-call.i 0 .22  .34  1.6  17   .012 7.8  .51 .33 13   42 7.5 4.0 87 300
floats-cdfpl/sine_8_true-unreach-call.i 0 .14  .13  2.0  9.3 .012 0    .49 .33 10   40 5.6 3.0 110 300
floats-cdfpl/square_4_true-unreach-call.i 0 .18  .18  1.7  9.2 .012 0    .59 .39 6.6 40 7.9 4.1 75 300
floats-cdfpl/square_5_true-unreach-call.i 0 .14  .14  1.7  9.3 .012 0    .52 .34 5.4 39 7.3 3.9 79 290
floats-cdfpl/square_6_true-unreach-call.i 0 .17  .17  1.8  9.3 .012 0    .55 .36 8.9 39 7.6 4.0 100 310
floats-cdfpl/square_7_true-unreach-call.i 0 .15  .15  1.6  9.4 .012 0    .56 .34 13   42 6.8 3.6 140 340
floats-cdfpl/square_8_true-unreach-call.i 0 .14  .14  1.4  9.5 .012 0    .58 .37 7.7 39 5.6 3.0 68 300
floats-cbmc-regression/float-div1_true-unreach-call.i 0 .19  .17  2.0  9.5 .12  .13 .51 .33 10   40 6.2 3.3 130 300
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i 0 .22  .20  2.0  9.8 .15  0    .55 .35 12   41 8.1 4.2 110 300
floats-cbmc-regression/float-no-simp1_true-unreach-call.i 2 .16  .16  1.3  9.3 .012 0    3.6  2.0  45   250 13   7.1 120 300
floats-cbmc-regression/float-no-simp2_true-unreach-call.i 0 .19  .17  2.4  9.5 .14  0    .50 .31 11   40 7.0 3.7 85 290
floats-cbmc-regression/float-no-simp3_true-unreach-call.i 2 .13  .13  1.5  9.3 .012 0    4.1  2.3  34   260 14   7.5 160 300
floats-cbmc-regression/float-no-simp4_true-unreach-call.i 0 .23  .21  2.3  9.6 .14  0    .52 .34 11   40 5.6 3.0 100 300
floats-cbmc-regression/float-no-simp6_true-unreach-call.i 2 .15  .14  1.6  9.4 .012 0    4.1  2.3  58   260 14   7.5 240 320
floats-cbmc-regression/float-no-simp7_true-unreach-call.i 2 .15  .15  1.4  9.3 .012 0    3.5  1.9  50   250 12   6.6 160 330
floats-cbmc-regression/float-no-simp8_true-unreach-call.i 2 .18  .16  2.3  9.6 .12  0    5.4  2.9  65   280 16   8.7 210 300
floats-cbmc-regression/float-rounding1_true-unreach-call.i 0 .14  .12  1.3  9.5 .14  0    .73 .45 9.4 43 7.7 4.0 74 300
floats-cbmc-regression/float-to-double1_true-unreach-call.i 0 .18  .16  2.4  9.6 .12  0    .64 .40 7.4 40 6.5 3.4 110 310
floats-cbmc-regression/float-to-double2_true-unreach-call.i 2 .16  .15  1.3  9.2 .012 0    3.3  1.9  77   260 14   7.7 190 310
floats-cbmc-regression/float-zero-sum1_true-unreach-call.i 2 .13  .13  1.4  9.4 .012 0    4.4  2.4  41   260 7.3 3.9 100 310
floats-cbmc-regression/float11_true-unreach-call.i 2 .14  .14  1.1  9.4 .012 0    3.4  1.9  68   260 16   8.3 260 330
floats-cbmc-regression/float12_true-unreach-call.i 0 .17  .17  1.5  9.3 .012 0    .49 .33 7.1 41 5.8 3.0 100 300
floats-cbmc-regression/float13_true-unreach-call.i 2 .15  .15  1.6  9.5 .012 0    3.5  2.0  74   260 18   9.5 160 320
floats-cbmc-regression/float14_true-unreach-call.i 0 .17  .15  2.0  9.6 .12  0    .57 .36 11   42 5.7 3.1 95 300
floats-cbmc-regression/float18_true-unreach-call.i 2 .20  .18  2.4  9.4 .12  0    28    24    530   430 7.1 3.7 130 310
floats-cbmc-regression/float19_true-unreach-call.i 0 .17  .15  2.2  9.5 .12  0    .63 .41 8.7 39 7.2 3.8 100 300
floats-cbmc-regression/float1_true-unreach-call.i 2 .16  .15  1.4  9.3 .012 0    4.2  2.4  49   260 14   7.7 150 310
floats-cbmc-regression/float20_true-unreach-call.i 0 .18  .17  1.8  9.4 .012 0    .60 .38 9.1 40 6.7 3.6 76 290
floats-cbmc-regression/float21_true-unreach-call.i 0 .20  .17  1.9  9.5 .14  0    .50 .33 9.3 40 8.2 4.3 91 300
floats-cbmc-regression/float22_true-unreach-call.i 2 .16  .16  1.3  9.3 .012 0    7.5  4.0  82   290 14   7.6 230 320
floats-cbmc-regression/float2_true-unreach-call.i 2 .13  .13  1.6  9.5 .012 0    3.3  1.8  51   260 15   8.1 200 310
floats-cbmc-regression/float3_true-unreach-call.i 2 .17  .17  1.6  9.7 .012 0    4.5  2.6  45   280 24   16   300 340
floats-cbmc-regression/float4_true-unreach-call.i 0 .22  .20  2.0  9.6 .14  0    .50 .32 9.6 39 7.6 4.0 79 290
floats-cbmc-regression/float5_true-unreach-call.i 0 .16  .16  1.7  9.3 .012 0    .54 .35 10   39 8.1 4.2 87 300
floats-cbmc-regression/float6_true-unreach-call.i 0 .16  .16  1.6  9.3 .012 0    .63 .39 10   41 7.3 3.8 90 300
floats-cbmc-regression/float7_true-unreach-call.i 2 .16  .15  1.4  9.4 .012 0    4.2  2.4  44   250 5.4 2.9 110 290
floats-cbmc-regression/float8_true-unreach-call.i 0 .23  .21  2.4  9.7 .13  0    .49 .33 12   39 6.1 3.2 100 300
floats-cbmc-regression/float_lib1_true-unreach-call.i 0 .17  .15  2.1  9.5 .14  0    .53 .33 11   41 6.3 3.3 99 290
floats-cbmc-regression/float_lib2_true-unreach-call.i 0 .17  .15  1.9  9.6 .14  0    .51 .32 13   39 6.1 3.2 81 300
float-benchs/cast_float_ptr_false-unreach-call.c 0 .17  .17  1.5  9.4 .012 .13 .55 .34 13   40 5.9 3.1 120 300
float-benchs/cast_union_loose_false-unreach-call.c 1 .17  .17  1.7  9.3 .012 0    4.1  2.3  85   290 6.2 3.3 140 310
float-benchs/cast_union_tight_false-unreach-call.c 0 .16  .16  1.6  9.6 .012 0    .48 .31 8.9 42 6.5 3.4 100 290
float-benchs/float_int_inv_square_false-unreach-call.c 1 .19  .19  2.0  12   .012 0    3.7  2.1  65   280 12   6.8 150 310
float-benchs/inv_square_false-unreach-call.c 0 .17  .17  1.6  9.4 .012 0    .55 .35 11   40 6.6 3.5 87 300
float-benchs/nan_double_false-unreach-call.c 0 .16  .16  1.6  9.3 .012 0    .51 .32 11   39 6.4 3.4 96 290
float-benchs/nan_float_false-unreach-call.c 0 .16  .16  1.5  9.2 .012 0    .55 .35 11   39 6.1 3.2 97 300
float-benchs/sin_interpolated_index_false-unreach-call.c 0 .16  .16  1.9  9.3 .025 0    .74 .46 7.5 44 7.6 4.0 85 300
float-benchs/sqrt_poly2_false-unreach-call.c 0 .18  .18  1.8  9.3 .012 0    .47 .32 8.9 40 6.9 3.6 110 300
float-benchs/Muller_Kahan_true-unreach-call.c 2 .13  .13  1.5  9.2 .012 0    900    900    13000   2700 750   690   12000 7000
float-benchs/Rump_double_true-unreach-call.c 2 .16  .16  1.6  9.2 .012 .32 3.4  1.9  61   260 29   22   380 790
float-benchs/Rump_float_true-unreach-call.c 2 .13  .13  1.5  9.4 .012 0    3.5  2.0  49   260 15   8.7 240 380
float-benchs/addsub_double_exact_true-unreach-call.c 2 .15  .15  1.4  9.4 .012 0    4.8  2.7  43   260 12   6.9 170 310
float-benchs/addsub_float_exact_true-unreach-call.c 2 .22  .34  2.0  18   .012 8.9  4.3  2.4  43   260 13   7.1 260 330
float-benchs/addsub_float_inexact_true-unreach-call.c 2 .15  .14  1.4  9.3 .012 0    3.5  2.0  72   250 14   7.4 240 330
float-benchs/arctan_Pade_true-unreach-call.c 0 .16  .16  1.8  9.4 .012 0    .49 .32 9.7 40 5.8 3.1 110 290
float-benchs/bary_diverge_true-unreach-call.c 0 900     900     12000    42   .012 0    .50 .33 7.7 39 5.8 3.1 84 300
float-benchs/cast_float_union_true-unreach-call.c 2 .14  .14  1.6  9.5 .012 0    3.5  2.0  65   250 12   6.4 140 300
float-benchs/cos_polynomial_true-unreach-call.c 0 .18  .18  1.7  9.5 .012 0    .64 .41 11   42 5.8 3.1 110 300
float-benchs/divmul_buf_diverge_true-unreach-call.c 0 900     900     9300    3600   .012 7.7  .51 .32 12   42 5.5 3.0 120 300
float-benchs/divmul_diverge_true-unreach-call.c 0 900     900     8500    3800   .012 0    .52 .33 11   39 6.9 3.7 85 300
float-benchs/drift_tenth_true-unreach-call.c 2 .14  .13  1.5  9.3 .012 0    11    8.6  270   340 170   160   2200 650
float-benchs/exp_loop_true-unreach-call.c 0 .16  .16  2.1  9.3 .012 0    .51 .33 11   41 6.2 3.3 130 300
float-benchs/feedback_diverge_true-unreach-call.c 0 900     900     8200    3600   .012 0    .63 .40 8.9 40 5.8 3.1 120 300
float-benchs/filter1_true-unreach-call.c 0 900     900     12000    3600   .012 0    .61 .38 8.6 40 6.0 3.2 110 300
float-benchs/filter2_alt_true-unreach-call.c 0 900     900     12000    45   .012 0    .64 .40 6.9 41 6.0 3.2 95 290
float-benchs/filter2_iterated_true-unreach-call.c 0 900     920     11000    15000   .012 0    .64 .41 9.5 41 7.1 3.7 79 300
float-benchs/filter2_reinit_true-unreach-call.c 0 900     900     11000    51   .012 0    .47 .31 4.8 41 7.4 4.0 83 300
float-benchs/filter2_set_true-unreach-call.c 0 .19  .18  2.0  9.5 .012 0    .55 .35 7.4 39 7.5 3.9 87 310
float-benchs/filter2_true-unreach-call.c 0 900     900     11000    46   .012 0    .63 .41 8.1 42 5.0 2.7 75 280
float-benchs/filter_iir_true-unreach-call.c 0 900     900     11000    47   .012 0    .56 .36 9.5 40 6.2 3.3 85 300
float-benchs/float_double_true-unreach-call.c 2 .13  .12  1.7  9.5 .012 0    3.3  1.9  62   250 13   6.9 230 310
float-benchs/image_filter_true-unreach-call.c 0 .24  .23  2.3  11   .025 0    .52 .33 11   42 7.3 3.9 72 320
float-benchs/interpolation2_true-unreach-call.c 0 .16  .16  1.7  9.5 .012 0    .48 .30 7.9 39 7.4 3.9 83 300
float-benchs/interpolation_true-unreach-call.c 0 .17  .17  2.0  9.6 .012 0    .53 .35 11   41 5.8 3.1 130 300
float-benchs/inv_sqrt_Quake_true-unreach-call.c 0 .15  .15  2.2  9.4 .012 0    .49 .32 8.7 39 6.7 3.6 86 300
float-benchs/inv_square_int_true-unreach-call.c 2 .18  .18  1.6  10   .012 .32 3.5  2.0  59   270 39   33   480 350
float-benchs/inv_square_true-unreach-call.c 0 .17  .17  1.8  9.4 .012 0    .49 .31 12   40 7.3 3.8 85 300
float-benchs/loop_true-unreach-call.c 2 11     11     180    770   .012 0    900    900    12000   1900 960   950   21000 830
float-benchs/mea8000_true-unreach-call.c 0 900     900     10000    320   .037 0    .68 .43 9.9 43 7.3 3.8 77 290
float-benchs/nan_double_range_true-unreach-call.c 0 .17  .17  1.6  9.4 .012 0    .50 .32 12   40 6.5 3.4 93 290
float-benchs/nan_float_range_true-unreach-call.c 0 .14  .14  1.6  9.3 .012 0    .57 .35 7.7 41 7.2 3.8 77 300
float-benchs/rlim_exit_true-unreach-call.c 0 900     900     13000    41   .012 0    .64 .42 8.7 40 6.8 3.6 71 290
float-benchs/rlim_invariant_true-unreach-call.c 0 900     900     11000    41   .012 0    .68 .43 8.0 40 7.7 4.0 91 310
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call.c 0 .18  .18  1.9  9.3 .025 0    .54 .34 12   40 6.8 3.6 71 300
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call.c 0 .16  .16  1.7  9.3 .025 0    .51 .33 12   42 7.3 3.8 77 310
float-benchs/sin_interpolated_index_true-unreach-call.c 0 .16  .16  1.9  9.3 .025 0    .52 .33 12   39 5.7 3.0 110 300
float-benchs/sin_interpolated_negation_true-unreach-call.c 0 .18  .18  1.7  9.3 .025 0    .50 .31 5.3 40 6.0 3.2 100 290
float-benchs/sin_interpolated_smallrange_true-unreach-call.c 0 .16  .16  2.1  9.5 .025 0    .48 .32 10   40 6.3 3.3 120 300
float-benchs/sqrt_Householder_constant_true-unreach-call.c 2 .14  .14  1.5  9.1 .012 0    900    900    14000   1700 640   620   11000 2900
float-benchs/sqrt_Householder_interval_true-unreach-call.c 0 .17  .17  2.2  9.3 .012 0    .68 .43 8.2 41 5.5 3.0 74 300
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c 0 .16  .16  1.9  9.5 .012 0    .49 .32 11   39 6.3 3.3 130 300
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c 0 .18  .18  1.8  9.4 .012 0    .66 .43 6.6 40 6.2 3.3 97 300
float-benchs/sqrt_biNewton_pseudoconstant_true-unreach-call.c 0 .16  .16  1.8  9.4 .012 0    .53 .35 12   40 5.8 3.1 94 300
float-benchs/sqrt_poly_true-unreach-call.c 0 .15  .15  1.8  9.5 .012 0    .53 .33 9.1 39 7.6 4.0 86 300
float-benchs/water_pid_true-unreach-call.c 2 .16  .15  1.4  9.2 .012 0    900    900    11000   1800 310   300   5400 3500
float-benchs/zonotope_2_true-unreach-call.c 2 1.0   1.0   13    56   .012 0    900    900    14000   1100 960   950   18000 1300
float-benchs/zonotope_3_true-unreach-call.c 0 900     900     11000    41   .012 0    .52 .35 11   42 6.7 3.5 73 310
float-benchs/zonotope_loose_true-unreach-call.c 0 .16  .16  1.9  9.4 .012 0    .58 .36 8.1 39 5.9 3.1 130 300
float-benchs/zonotope_tight_true-unreach-call.c 0 .18  .18  1.9  9.4 .012 0    .59 .37 5.6 40 5.5 3.0 100 280
floats-esbmc-regression/Double_div_true-unreach-call.i 2 .13  .13  1.7  9.5 .012 0    4.3  2.7  69   330 150   140   3000 1400
floats-esbmc-regression/Float_div_true-unreach-call.i 2 .13  .13  1.6  9.4 .012 0    4.9  2.8  70   300 260   250   5800 730
floats-esbmc-regression/ceil_nondet_true-unreach-call.i 0 .098 .098 .71 9.4 .12  0    .61 .39 7.5 39 6.4 3.5 88 290
floats-esbmc-regression/ceil_true-unreach-call.i 0 .13  .13  1.4  9.6 .11  0    .54 .34 12   39 6.6 3.5 110 300
floats-esbmc-regression/copysign_true-unreach-call.i 0 .14  .14  1.6  9.6 .11  0    .66 .42 6.1 39 7.1 3.7 94 300
floats-esbmc-regression/digits_for_true-unreach-call.i 2 .16  .16  1.4  9.4 .012 .45 900    900    9700   1000 960   950   13000 1500
floats-esbmc-regression/digits_while_true-unreach-call.i 2 .15  .15  1.8  9.3 .012 0    900    900    14000   970 960   950   14000 3100
floats-esbmc-regression/fabs_true-unreach-call.i 0 .14  .14  1.5  9.6 .11  0    .57 .36 10   40 6.2 3.3 120 290
floats-esbmc-regression/fdim_true-unreach-call.i 0 .15  .15  1.3  9.5 .11  0    .48 .32 8.4 39 5.7 3.0 120 300
floats-esbmc-regression/floor_nondet_true-unreach-call.i 0 .098 .097 .78 9.5 .12  0    .49 .33 5.1 40 8.1 4.3 81 310
floats-esbmc-regression/floor_true-unreach-call.i 0 .12  .12  1.8  9.6 .11  0    .62 .41 8.2 39 7.4 3.9 69 290
floats-esbmc-regression/fmax_true-unreach-call.i 0 .12  .12  1.3  9.6 .11  0    .62 .39 7.4 42 6.6 3.5 110 300
floats-esbmc-regression/fmin_true-unreach-call.i 0 .12  .12  1.5  9.5 .11  0    .51 .32 10   41 7.5 3.9 78 300
floats-esbmc-regression/fmod2_true-unreach-call.i 0 .14  .14  1.7  9.6 .11  0    .58 .37 11   41 7.8 4.1 100 320
floats-esbmc-regression/fmod3_true-unreach-call.i 0 .14  .14  2.1  9.4 .11  0    .56 .34 7.4 39 6.9 3.7 82 300
floats-esbmc-regression/fmod_true-unreach-call.i 2 .13  .13  1.7  9.7 .11  0    5.6  3.0  55   270 7.2 3.8 130 330
floats-esbmc-regression/isgreater_true-unreach-call.i 2 .14  .14  1.5  9.4 .11  0    5.4  2.9  130   280 12   6.4 210 310
floats-esbmc-regression/isgreaterequal_true-unreach-call.i 2 .15  .15  1.5  9.5 .11  0    5.3  2.9  120   270 11   5.6 190 300
floats-esbmc-regression/isless_true-unreach-call.i 2 .16  .16  1.5  9.5 .11  0    6.7  3.6  60   270 15   7.9 140 340
floats-esbmc-regression/islessequal_true-unreach-call.i 2 .13  .13  1.3  9.4 .11  0    5.1  2.7  100   270 11   5.9 190 310
floats-esbmc-regression/islessgreater_true-unreach-call.i 2 .14  .14  1.6  9.5 .11  0    5.1  2.8  55   270 14   7.2 160 310
floats-esbmc-regression/isunordered_true-unreach-call.i 2 .14  .13  1.6  9.4 .11  0    5.5  3.0  94   270 11   5.6 180 300
floats-esbmc-regression/lrint_true-unreach-call.i 0 .074 .073 .76 9.5 .12  0    .49 .33 11   40 6.3 3.3 120 290
floats-esbmc-regression/modf_true-unreach-call.i 0 .15  .15  1.4  9.5 .11  0    .51 .33 7.7 39 6.3 3.3 93 300
floats-esbmc-regression/nan_true-unreach-call.i 0 .12  .12  1.5  9.5 .12  0    .49 .31 8.7 39 8.4 4.4 87 320
floats-esbmc-regression/nearbyint2_true-unreach-call.i 0 .10  .10  .85 9.7 .12  0    .54 .34 11   43 5.8 3.1 71 290
floats-esbmc-regression/nearbyint_true-unreach-call.i 0 .076 .076 .85 9.5 .12  0    .50 .32 9.2 40 6.2 3.3 120 310
floats-esbmc-regression/remainder_true-unreach-call.i 0 .13  .12  1.5  9.5 .11  0    .52 .32 12   40 7.3 3.8 93 320
floats-esbmc-regression/rint2_true-unreach-call.i 0 .075 .074 .71 9.5 .12  0    .50 .33 12   41 6.7 3.6 96 300
floats-esbmc-regression/rint_true-unreach-call.i 0 .094 .095 .79 9.5 .12  0    .65 .41 7.7 43 7.9 4.1 88 300
floats-esbmc-regression/round_nondet_true-unreach-call.i 0 .074 .074 .84 9.6 .12  0    .50 .32 13   40 6.9 3.6 85 300
floats-esbmc-regression/round_true-unreach-call.i 0 .13  .12  1.5  9.5 .11  0    .51 .33 13   40 6.5 3.4 120 310
floats-esbmc-regression/rounding_functions_true-unreach-call.i 0 .13  .12  1.3  9.5 .11  0    .63 .40 6.0 40 5.8 3.1 100 300
floats-esbmc-regression/trunc_nondet_2_true-unreach-call.i 0 .14  .14  1.8  9.5 .12  0    .53 .36 9.7 41 6.8 3.7 71 290
floats-esbmc-regression/trunc_nondet_true-unreach-call.i 0 .10  .10  .91 9.5 .12  0    .59 .38 8.5 40 7.2 3.8 76 300
floats-esbmc-regression/trunc_true-unreach-call.i 0 .13  .12  1.5  9.4 .11  0    .48 .32 9.3 40 6.5 3.4 120 310
floats-esbmc-regression/Double_div_bad_false-unreach-call.i 1 .17  .17  1.8  12   .012 .45 57    52    1700   7000 97   62   1300 5900
floats-esbmc-regression/Float_div_bad_false-unreach-call.i 1 .14  .13  1.7  9.4 .012 0    22    18    510   2000 96   75   1200 2100
floats-esbmc-regression/digits_bad_for_false-unreach-call.i 1 .16  .16  1.4  9.3 .012 0    5.2  2.9  83   280 18   13   320 380
floats-esbmc-regression/digits_bad_while_false-unreach-call.i 1 .13  .13  1.8  9.3 .012 0    6.3  3.4  110   290 26   20   630 460
../../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 86 13000    13000    150000 33000 7.3   39    172 110 89 2900 11000   172 410 260 6000 17000   172 6500 6400 91000 24000   172 7200 6600 120000 63000  
    correct results 46 86 19    19    260 1300 1.5   10    5 98 81 2600 10000   3 260 180 3800 9500   33 6500 6400 91000 20000   20 6500 6200 110000 33000  
        correct true 40 80 18    18    250 1200 1.4   10    0 0 0 0 0   2 0 0 0 0   32 6500 6400 91000 20000   20 6500 6200 110000 33000  
        correct false 6 6 .96 .95 10 61 .074 .45 5 98 81 2600 10000   1 260 180 3800 9500   1 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) 86
Run set sv-comp17.ReachSafety-Floats