Tool DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-11-30 16:01:31 CET 2017-12-01 08:31:47 CET 2017-12-01 08:56:50 CET 2017-12-01 08:59:39 CET 2017-12-01 09:01:39 CET 2017-12-01 08:10:33 CET 2017-12-01 08:38:18 CET
Run set depthk.sv-comp18.ReachSafety-Floats cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Floats uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Floats cpa-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Floats fshell-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-Floats cpa-seq-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.ReachSafety-Floats uautomizer-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.ReachSafety-Floats
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const --full-output --validate ../../results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true --graphml-witness ../../results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
floats-cdfpl/newton_1_4_false-unreach-call_true-termination.i 0 890    400 7500   0 .55 43 0 .021 4.8 0 .88 50 0 .0016 .29 - -
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i 0 890    480 8000   0 .54 43 0 .047 4.8 0 .84 47 0 .0014 .26 - -
floats-cdfpl/newton_1_6_false-unreach-call_true-termination.i 0 890    400 7900   0 .55 44 0 .020 4.9 0 .88 49 0 .0012 .26 - -
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i 0 890    400 8700   0 .53 43 0 .018 5.0 0 .87 47 0 .0014 .30 - -
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i 0 890    460 7500   0 .54 42 0 .018 5.0 0 .85 49 0 .0012 .34 - -
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i 0 890    710 8400   0 .57 44 0 .019 5.0 0 .86 49 0 .0011 .34 - -
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i 0 890    700 9200   0 .56 43 0 .020 5.0 0 .85 47 0 .0013 .30 - -
floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i 0 890    760 8100   0 .57 43 0 .019 4.8 0 .88 49 0 .0013 .29 - -
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i 0 890    1000 9100   0 .54 43 0 .018 4.9 0 .85 49 0 .0012 .29 - -
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i 0 890    1000 8100   0 .54 42 0 .021 5.0 0 .85 49 0 .0013 .26 - -
floats-cdfpl/newton_3_8_false-unreach-call_true-termination.i 0 890    1100 6900   0 .40 41 0 .019 4.9 0 .84 49 0 .0013 .26 - -
floats-cdfpl/sine_1_false-unreach-call_true-termination.i 1 190    240 1600   -32 2.9  260 -32 4.6   210   0 2.8  180 1 .59   18    - -
floats-cdfpl/sine_2_false-unreach-call_true-termination.i 1 97    200 970   -32 3.0  260 -32 5.7   280   0 2.8  180 1 .59   18    - -
floats-cdfpl/sine_3_false-unreach-call_true-termination.i 1 65    180 620   -32 2.9  250 -32 4.4   210   0 2.8  180 1 .58   18    - -
floats-cdfpl/square_1_false-unreach-call_true-termination.i 1 570    210 4500   -32 2.1  260 -32 4.4   220   0 2.8  210 1 .59   18    - -
floats-cdfpl/square_2_false-unreach-call_true-termination.i 0 890    250 9000   0 .53 42 0 .020 4.8 0 .88 49 0 .0013 .26 - -
floats-cdfpl/square_3_false-unreach-call_true-termination.i 0 890    350 6400   0 .52 41 0 .019 4.9 0 .84 49 0 .0014 .26 - -
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i 0 890    410 8900   - - - - 0 .55 43 0 .020 4.9
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i 0 890    400 8300   - - - - 0 .55 45 0 .025 4.8
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i 0 890    400 8800   - - - - 0 .62 45 0 .018 4.9
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i 0 890    680 8600   - - - - 0 .63 43 0 .019 4.9
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i 0 890    700 9100   - - - - 0 .54 43 0 .019 4.8
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i 0 890    710 9300   - - - - 0 .55 43 0 .019 5.0
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i 0 890    710 9500   - - - - 0 .51 43 0 .018 4.9
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i 0 890    760 8400   - - - - 0 .52 41 0 .020 4.9
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i 0 890    1000 10000   - - - - 0 .53 43 0 .019 4.9
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i 0 890    1000 9000   - - - - 0 .52 43 0 .019 4.8
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i 0 890    930 8900   - - - - 0 .64 41 0 .019 4.9
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i 0 890    990 9900   - - - - 0 .62 43 0 .019 4.8
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i 0 890    1200 7700   - - - - 0 .56 43 0 .020 4.9
floats-cdfpl/sine_4_true-unreach-call_true-termination.i 0 890    310 10000   - - - - 0 .54 43 0 .022 4.8
floats-cdfpl/sine_5_true-unreach-call_true-termination.i 0 890    310 9900   - - - - 0 .52 43 0 .019 4.8
floats-cdfpl/sine_6_true-unreach-call_true-termination.i 0 890    320 7000   - - - - 0 .62 44 0 .019 4.9
floats-cdfpl/sine_7_true-unreach-call_true-termination.i 0 890    310 8100   - - - - 0 .52 41 0 .018 4.8
floats-cdfpl/sine_8_true-unreach-call_true-termination.i 0 890    310 8400   - - - - 0 .63 41 0 .018 4.8
floats-cdfpl/square_4_true-unreach-call_true-termination.i 0 890    250 7700   - - - - 0 .53 43 0 .018 4.9
floats-cdfpl/square_5_true-unreach-call_true-termination.i 0 890    350 8900   - - - - 0 .56 43 0 .049 4.8
floats-cdfpl/square_6_true-unreach-call_true-termination.i 0 890    260 6600   - - - - 0 .56 44 0 .019 4.8
floats-cdfpl/square_7_true-unreach-call_true-termination.i 0 890    350 11000   - - - - 0 .51 43 0 .048 4.9
floats-cdfpl/square_8_true-unreach-call_true-termination.i 0 890    200 9900   - - - - 0 .73 43 0 .020 4.9
floats-cbmc-regression/float-div1_true-unreach-call.i 2 37    370 370   - - - - 2 4.9  320 2 33     600  
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i 2 25    2000 220   - - - - 2 11    790 2 32     710  
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i 2 3.1  270 33   - - - - 2 2.9  250 2 9.1   240  
floats-cbmc-regression/float-no-simp2_true-unreach-call.i 2 300    330 3000   - - - - 2 16    300 2 41     400  
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i 2 3.2  260 30   - - - - 2 3.2  250 2 9.2   220  
floats-cbmc-regression/float-no-simp4_true-unreach-call.i 2 6.3  310 66   - - - - 2 4.1  260 2 37     580  
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i 2 3.2  250 28   - - - - 2 3.0  250 2 11     290  
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i 2 3.1  260 33   - - - - 2 3.9  250 2 9.5   250  
floats-cbmc-regression/float-no-simp8_true-unreach-call.i 2 4.3  260 39   - - - - 2 3.9  260 2 10     300  
floats-cbmc-regression/float-rounding1_true-unreach-call.i 0 9.1  450 82   - - - - 0 4.9  250 0 3.7   200  
floats-cbmc-regression/float-to-double1_true-unreach-call.i 2 29    320 350   - - - - 2 4.7  260 2 130     420  
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i 2 3.1  260 32   - - - - 2 3.0  250 2 9.8   240  
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i 2 3.1  260 30   - - - - 2 3.1  250 2 12     300  
floats-cbmc-regression/float11_true-unreach-call_true-termination.i 2 3.4  250 33   - - - - 2 3.0  250 2 7.1   250  
floats-cbmc-regression/float12_true-unreach-call_true-termination.i 2 7.7  290 85   - - - - 2 3.8  250 2 15     260  
floats-cbmc-regression/float13_true-unreach-call_true-termination.i 2 3.2  250 27   - - - - 2 3.0  250 2 11     320  
floats-cbmc-regression/float14_true-unreach-call.i 2 4.3  270 40   - - - - 2 3.9  250 2 9.1   290  
floats-cbmc-regression/float18_true-unreach-call.i 2 18    270 270   - - - - 2 25    410 0 3.6   200  
floats-cbmc-regression/float19_true-unreach-call.i 2 7.3  300 78   - - - - 2 5.0  260 2 10     280  
floats-cbmc-regression/float1_true-unreach-call_true-termination.i 2 3.1  260 30   - - - - 2 3.1  250 2 9.0   230  
floats-cbmc-regression/float20_true-unreach-call_true-termination.i 2 24    250 270   - - - - 2 3.1  250 2 15     410  
floats-cbmc-regression/float21_true-unreach-call.i 2 30    310 370   - - - - 2 8.4  300 2 82     610  
floats-cbmc-regression/float22_true-unreach-call_true-termination.i 0 18    51 260   - - - - 0 .64 41 0 .023 4.9
floats-cbmc-regression/float2_true-unreach-call_true-termination.i 2 3.2  240 28   - - - - 2 4.0  250 2 10     280  
floats-cbmc-regression/float3_true-unreach-call_true-termination.i 2 7.5  250 85   - - - - 2 4.2  270 2 13     330  
floats-cbmc-regression/float4_true-unreach-call.i 2 310    590 3400   - - - - 2 78    330 2 78     450  
floats-cbmc-regression/float5_true-unreach-call_true-termination.i 2 16    260 240   - - - - 2 3.0  260 2 26     280  
floats-cbmc-regression/float6_true-unreach-call_true-termination.i 2 3.5  260 34   - - - - 2 3.6  250 2 11     290  
floats-cbmc-regression/float8_true-unreach-call.i 2 7.5  340 81   - - - - 2 8.2  270 2 11     300  
floats-cbmc-regression/float_lib1_true-unreach-call.i 0 3.9  150 47   - - - - 0 2.1  140 0 9.8   260  
floats-cbmc-regression/float_lib2_true-unreach-call.i 2 4.4  260 43   - - - - 2 4.2  260 2 17     530  
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c 0 .41 48 4.8 0 2.3  160 -32 5.0   230   0 2.7  180 0 .58   18    - -
float-benchs/cast_union_loose_false-unreach-call_true-termination.c 1 .51 49 5.5 -32 3.2  250 -32 4.6   220   0 3.0  180 1 .59   18    - -
float-benchs/cast_union_tight_false-unreach-call_true-termination.c 1 1.2  48 14   -32 3.0  260 -32 3.4   230   0 3.0  210 1 .59   18    - -
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c 1 17    66 220   -32 3.1  260 -32 4.8   210   0 2.7  180 1 .59   18    - -
float-benchs/inv_Newton_false-unreach-call.c 0 890    340 7300   0 .55 43 0 .020 5.0 0 .87 49 0 .0011 .32 - -
float-benchs/inv_square_false-unreach-call_true-termination.c 1 .46 40 5.6 -32 3.0  250 -32 4.2   210   0 3.0  210 1 .60   18    - -
float-benchs/nan_double_false-unreach-call_true-termination.c 0 .36 48 4.8 -32 3.3  270 -32 4.6   220   0 3.1  180 -32 .59   18    - -
float-benchs/nan_float_false-unreach-call_true-termination.c 0 .35 48 5.0 -32 2.9  260 -32 4.5   210   0 2.8  180 -32 .58   18    - -
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c 1 110    410 1100   -32 3.8  260 -32 6.3   400   0 3.1  210 1 .66   18    - -
float-benchs/sqrt_poly2_false-unreach-call.c 1 290    340 2800   0 2.3  160 -32 5.1   230   0 2.6  170 1 .61   18    - -
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c 0 890    1200 6700   - - - - 0 .55 44 0 .042 4.8
float-benchs/Rump_double_true-unreach-call_true-termination.c 2 3.3  300 30   - - - - 2 3.3  250 2 23     990  
float-benchs/Rump_float_true-unreach-call_true-termination.c 2 3.1  270 29   - - - - 2 2.9  250 2 14     430  
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c 2 3.1  270 28   - - - - 2 2.9  250 2 9.5   270  
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c 2 3.1  260 29   - - - - 2 3.2  250 2 9.9   250  
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c 2 3.0  260 27   - - - - 2 3.7  250 2 9.1   250  
float-benchs/arctan_Pade_true-unreach-call_true-termination.c 0 890    1100 11000   - - - - 0 .58 43 0 .019 5.0
float-benchs/bary_diverge_true-unreach-call_true-termination.c 0 890    260 10000   - - - - 0 .52 43 0 .018 4.8
float-benchs/cast_float_union_true-unreach-call.c 2 3.1  250 32   - - - - 2 3.1  240 2 4.6   220  
float-benchs/cos_polynomial_true-unreach-call_true-termination.c 0 890    610 8200   - - - - 0 .57 44 0 .018 4.9
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c 0 890    270 9500   - - - - 0 .55 43 0 .018 4.9
float-benchs/divmul_diverge_true-unreach-call_true-termination.c 0 890    270 13000   - - - - 0 .50 41 0 .019 5.0
float-benchs/drift_tenth_true-unreach-call_true-termination.c 0 890    490 7700   - - - - 0 .63 44 0 .018 4.8
float-benchs/exp_loop_true-unreach-call.c 0 890    410 8100   - - - - 0 .53 44 0 .037 5.0
float-benchs/feedback_diverge_true-unreach-call_true-termination.c 0 890    330 8200   - - - - 0 .54 41 0 .018 4.9
float-benchs/filter1_true-unreach-call_true-termination.c 0 890    280 8400   - - - - 0 .59 43 0 .018 5.0
float-benchs/filter2_alt_true-unreach-call.c 0 890    230 9700   - - - - 0 .59 43 0 .018 5.0
float-benchs/filter2_iterated_true-unreach-call.c 0 900    6500 8200   - - - - 0 .60 44 0 .019 4.8
float-benchs/filter2_reinit_true-unreach-call_true-termination.c 0 890    250 9500   - - - - 0 .61 43 0 .018 4.8
float-benchs/filter2_set_true-unreach-call_true-termination.c 0 890    450 7500   - - - - 0 .71 43 0 .019 5.0
float-benchs/filter2_true-unreach-call_true-termination.c 0 890    550 8500   - - - - 0 .69 42 0 .019 4.9
float-benchs/filter_iir_true-unreach-call.c 0 890    750 8400   - - - - 0 .61 42 0 .018 5.0
float-benchs/float_double_true-unreach-call_true-termination.c 2 3.1  250 30   - - - - 2 3.1  250 2 9.4   260  
float-benchs/image_filter_true-unreach-call.c 0 890    3100 7200   - - - - 0 .53 43 0 .020 4.9
float-benchs/interpolation2_true-unreach-call_true-termination.c 0 630    320 7200   - - - - 0 900    590 0 960     760  
float-benchs/interpolation_true-unreach-call_true-termination.c 0 130    310 1400   - - - - 2 14    370 0 960     870  
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c -16 320    270 3100   - - - - 2 3.1  260 2 150     940  
float-benchs/inv_square_int_true-unreach-call_true-termination.c 2 27    300 360   - - - - 2 3.1  260 2 16     310  
float-benchs/inv_square_true-unreach-call_true-termination.c 2 5.2  280 56   - - - - 2 3.4  260 2 58     370  
float-benchs/loop_true-unreach-call.c 0 890    320 10000   - - - - 0 .53 43 0 .018 4.8
float-benchs/mea8000_true-unreach-call.c 0 890    1900 11000   - - - - 0 .69 44 0 .018 4.9
float-benchs/nan_double_range_true-unreach-call_true-termination.c 2 3.6  280 37   - - - - 2 3.1  250 2 9.1   240  
float-benchs/nan_float_range_true-unreach-call_true-termination.c 2 3.6  270 35   - - - - 2 3.1  260 2 11     260  
float-benchs/rlim_exit_true-unreach-call_true-termination.c 0 890    200 9900   - - - - 0 .78 43 0 .018 5.0
float-benchs/rlim_invariant_true-unreach-call_true-termination.c 0 890    440 8600   - - - - 2 5.9  310 0 440     780  
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call_true-termination.c 0 890    1700 5600   - - - - 0 .60 43 0 .019 4.8
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call_true-termination.c 0 890    1700 6900   - - - - 0 .62 44 0 .021 4.8
float-benchs/sin_interpolated_index_true-unreach-call_true-termination.c 0 890    490 6100   - - - - 0 .66 44 0 .019 4.8
float-benchs/sin_interpolated_negation_true-unreach-call.c 0 890    2100 6800   - - - - 0 .51 44 0 .018 4.8
float-benchs/sin_interpolated_smallrange_true-unreach-call.c 0 890    1800 6100   - - - - 0 .66 43 0 .019 5.0
float-benchs/sqrt_Householder_constant_true-unreach-call.c 0 890    1000 12000   - - - - 0 .72 44 0 .019 4.9
float-benchs/sqrt_Householder_interval_true-unreach-call.c 0 890    620 7700   - - - - 0 .50 42 0 .019 4.9
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c 0 890    1200 7200   - - - - 0 .53 41 0 .020 5.0
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c 0 890    1100 7200   - - - - 0 .54 42 0 .019 4.9
float-benchs/sqrt_biNewton_pseudoconstant_true-unreach-call.c 0 890    1400 7000   - - - - 0 .52 41 0 .019 4.9
float-benchs/sqrt_poly_true-unreach-call_true-termination.c 0 890    500 6900   - - - - 0 .58 43 0 .018 4.8
float-benchs/water_pid_true-unreach-call_true-termination.c 0 890    580 7600   - - - - 0 .70 41 0 .019 4.9
float-benchs/zonotope_2_true-unreach-call_true-termination.c 0 45    76 610   - - - - 0 .60 43 0 .019 4.8
float-benchs/zonotope_3_true-unreach-call_true-termination.c 2 200    2300 2000   - - - - 2 5.7  340 0 960     5100  
float-benchs/zonotope_loose_true-unreach-call_true-termination.c 2 90    350 890   - - - - 2 5.1  310 2 110     940  
float-benchs/zonotope_tight_true-unreach-call_true-termination.c 2 110    350 960   - - - - 2 5.1  310 2 110     950  
floats-esbmc-regression/Double_div_true-unreach-call.i 0 890    260 8000   - - - - 0 .63 44 0 .019 4.8
floats-esbmc-regression/Float_div_true-unreach-call.i 0 890    610 12000   - - - - 0 .55 41 0 .019 4.9
floats-esbmc-regression/ceil_nondet_true-unreach-call.i 0 17    460 170   - - - - 0 4.3  260 0 9.1   270  
floats-esbmc-regression/ceil_true-unreach-call.i 2 4.3  270 48   - - - - 2 4.0  260 0 3.7   210  
floats-esbmc-regression/copysign_true-unreach-call.i 2 4.5  270 48   - - - - 2 4.0  250 0 3.8   210  
floats-esbmc-regression/digits_for_true-unreach-call.i -16 19    76 280   - - - - 0 4.0  270 2 5.2   250  
floats-esbmc-regression/digits_while_true-unreach-call.i -16 19    76 230   - - - - 0 4.0  260 2 5.3   320  
floats-esbmc-regression/fabs_true-unreach-call.i 2 5.8  300 59   - - - - 2 4.3  260 2 9.6   280  
floats-esbmc-regression/fdim_true-unreach-call.i 2 4.2  260 45   - - - - 2 4.9  250 0 3.4   200  
floats-esbmc-regression/floor_nondet_true-unreach-call.i 0 14    440 160   - - - - 0 5.2  260 0 7.3   210  
floats-esbmc-regression/floor_true-unreach-call.i 2 4.3  270 44   - - - - 2 4.1  260 0 3.8   200  
floats-esbmc-regression/fmax_true-unreach-call.i 2 4.2  260 44   - - - - 2 4.2  260 2 9.1   260  
floats-esbmc-regression/fmin_true-unreach-call.i 2 4.1  270 39   - - - - 2 4.2  260 2 6.1   280  
floats-esbmc-regression/fmod2_true-unreach-call.i -16 5.0  280 46   - - - - 0