Tool 2LS 0.7.2-sv-comp19 CBMC CBMC Path 5.10 () CPAchecker 1.7-svn 29852 DepthK 3.1 DIVINE ESBMC version 6.0.0 64-bit x86_64 linux PeSCo 1.7-svn b8d6131600+ Pinaka 0.1 skink 2.0 SMACK 1.9.3 symbiotic 6.0.3-77d4af47 ULTIMATE Automizer 0.1.23-635dfa2a ULTIMATE Kojak 0.1.23-635dfa2a ULTIMATE Taipan 0.1.23-635dfa2a VeriAbs 1.3.10 VeriFuzz 1.0.0
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-04 22:44:17 CET 2018-12-04 22:48:40 CET 2018-12-04 22:45:10 CET 2018-12-05 05:46:16 CET 2018-12-05 09:36:33 CET 2018-12-10 10:00:20 CET 2018-12-06 11:06:04 CET 2018-12-06 11:03:31 CET 2018-12-06 12:44:04 CET 2018-12-06 20:14:43 CET 2018-12-07 12:00:55 CET 2018-12-07 19:13:55 CET 2018-12-07 21:42:05 CET 2018-12-08 07:42:40 CET 2018-12-08 11:04:44 CET 2018-12-08 14:19:36 CET 2018-12-10 16:50:17 CET 2018-12-09 02:47:33 CET
Run set 2ls.sv-comp19_prop-reachsafety.ReachSafety-Floats cbmc.sv-comp19_prop-reachsafety.ReachSafety-Floats cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Floats depthk.sv-comp19_prop-reachsafety.ReachSafety-Floats divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-Floats divine-smt.sv-comp19_prop-reachsafety.ReachSafety-Floats esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Floats pesco.sv-comp19_prop-reachsafety.ReachSafety-Floats pinaka.sv-comp19_prop-reachsafety.ReachSafety-Floats skink.sv-comp19_prop-reachsafety.ReachSafety-Floats smack.sv-comp19_prop-reachsafety.ReachSafety-Floats symbiotic.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer.sv-comp19_prop-reachsafety.ReachSafety-Floats ukojak.sv-comp19_prop-reachsafety.ReachSafety-Floats utaipan.sv-comp19_prop-reachsafety.ReachSafety-Floats veriabs.sv-comp19_prop-reachsafety.ReachSafety-Floats verifuzz.sv-comp19_prop-reachsafety.ReachSafety-Floats
Options --graphml-witness witness.graphml --graphml-witness witness.graphml --graphml-witness witness.graphml -svcomp19 -heap 10000M -benchmark -timelimit 900s --no-symbolic -s kinduction -svcomp19-pesco -heap 10000M -stack 2048k -benchmark -timelimit 900s --graphml-witness witness.graphml -w error-witness.graphml --witness witness.graphml --full-output --full-output --full-output
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score
floats-cdfpl/newton_1_4_false-unreach-call_true-termination.i 6.8   61 84    1 14     60   150    1 9.2   54   96    1 74   450 650 1 26    99 360   1 8.3 430 110 0 8.3 430 110 0 25     93 350    1 46 1200 360 1 3.9  72 46   1 34   2900 310 0 880    1100 7300   0 .19  17 1.8  0 32   700 260 1 84   1100 800 0 32   700 270 1 87   370 660 1 15   150 170 1
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i 6.3   60 68    1 6.6   47   72    1 7.3   51   89    1 57   440 410 1 33    99 420   1 8.3 430 130 0 8.3 430 110 0 33     93 440    1 62 1200 450 1 4.2  73 51   1 34   2900 280 0 880    1200 6000   0 .17  17 1.9  0 94   730 640 1 77   1100 690 0 91   720 760 1 67   370 520 1 6.0 150 66 1
floats-cdfpl/newton_1_6_false-unreach-call_true-termination.i 2.6   51 32    1 4.3   42   44    1 5.5   44   72    1 44   450 360 1 42    100 580   1 8.1 430 99 0 8.3 430 95 0 41     92 520    1 27 1200 180 1 1.8  72 25   1 34   2900 280 0 880    970 6900   0 .17  17 1.8  0 64   710 480 1 81   1100 640 0 64   710 490 1 56   380 460 1 8.8 150 84 1
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i 2.4   50 25    1 8.4   49   87    1 2.4   41   31    1 22   440 210 1 9.0  100 130   1 8.2 430 110 0 8.2 430 91 0 8.8   92 120    1 26 1300 230 1 3.1  73 43   1 37   2900 350 0 880    960 6500   0 .17  18 2.2  0 250   760 1500 1 80   1100 700 0 250   760 1800 1 29   370 270 1 11   150 140 1
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i 3.9   53 41    1 7.4   49   95    1 .92  38   11    1 16   440 130 1 39    99 520   1 8.3 430 95 0 8.5 430 110 0 39     91 460    1 22 1200 170 1 1.9  72 28   1 33   2900 290 0 880    1400 5300   0 .20  18 2.1  0 25   710 220 1 83   1100 720 0 24   700 220 1 25   370 210 1 6.9 150 83 1
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i 3.5   90 32    1 77     160   660    1 57     140   600    1 140   610 1100 1 130    200 1700   1 8.3 430 110 0 8.3 430 110 0 130     190 1700    1 35 1300 250 0 22    96 260   1 35   2900 330 0 880    2100 6400   0 .18  17 2.1  0 130   860 980 0 73   1500 710 0 120   860 850 0 160   460 1400 0 60   150 890 1
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i 6.7   94 63    1 120     230   1200    1 53     140   490    1 84   600 590 1 120    200 1400   1 8.2 430 100 0 8.4 430 100 0 120     190 1400    1 33 1300 240 0 23    97 270   1 34   2900 330 0 880    1500 6800   0 .18  17 1.9  0 330   910 2300 1 65   1400 530 0 330   920 2700 1 98   460 750 0 24   150 310 1
floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i 17     120 170    1 25     100   310    1 21     99   270    1 43   610 310 1 61    200 740   1 8.1 430 130 0 8.5 430 100 0 61     190 730    1 42 1300 350 1 20    95 290   1 33   2900 280 0 880    2100 6000   0 .19  18 2.1  0 34   850 290 1 54   1400 520 0 34   840 290 1 69   460 560 1 19   200 200 1
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i 40     210 400    1 430     480   4500    1 340     460   3200    1 300   780 1900 1 100    300 980   1 8.2 430 100 0 8.2 430 120 0 100     290 1400    1 410 1900 2900 1 73    150 770   1 35   2900 310 0 880    3200 6800   0 .21  17 1.6  0 900   1100 6800 0 69   2000 640 0 900   1100 8200 0 360   570 3400 1 74   220 750 1
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i 64     220 680    1 75     200   830    1 38     150   360    1 200   780 1300 1 120    280 1400   1 8.4 430 120 0 8.4 430 100 0 120     280 1500    1 300 2000 2000 1 42    120 460   1 35   2900 320 0 880    2100 6800   0 .20  17 1.7  0 47   930 390 1 71   1900 540 0 49   940 470 1 270   570 1900 1 67   230 570 1
floats-cdfpl/newton_3_8_false-unreach-call_true-termination.i 35     190 440    1 55     180   540    1 84     220   820    1 170   780 980 1 130    310 1500   1 8.2 430 100 0 8.4 430 130 0 130     300 1600    1 29 1500 210 0 32    130 360   1 35   2900 320 0 880    2800 5800   0 .17  17 1.6  0 610   1100 5200 0 63   2000 520 0 610   1100 4500 0 230   570 1800 0 37   200 320 1
floats-cdfpl/sine_1_false-unreach-call_true-termination.i .74  24 8.4  1 .90  22   10    1 .91  21   11    1 9.0 380 110 1 20    71 320   1 8.2 430 120 0 8.3 430 110 0 20     64 280    1 110 1400 1000 1 1.9  65 30   1 31   2800 250 1 750    700 6300   0 .18  18 2.1  0 200   700 1700 0 34   590 260 0 200   700 1600 0 17   340 170 0 7.4 150 77 1
floats-cdfpl/sine_2_false-unreach-call_true-termination.i .58  24 7.1  1 4.1   31   58    1 1.4   23   18    1 45   410 390 1 20    71 240   1 8.2 430 110 0 8.3 430 110 0 20     64 300    1 21 1100 180 1 .47 61 4.3 1 32   2800 260 1 880    610 6600   0 .19  17 2.2  0 380   810 3600 1 35   610 300 0 380   810 3000 1 50   360 520 1 4.5 150 47 1
floats-cdfpl/sine_3_false-unreach-call_true-termination.i 1.6   31 19    1 .98  21   13    1 1.3   23   17    1 270   540 2700 1 19    71 310   1 8.3 430 110 0 8.3 430 110 0 19     64 240    1 45 1200 450 1 1.8  65 20   1 28   2800 230 0 680    530 5100   0 .17  18 2.3  0 360   760 2900 1 34   590 260 0 360   740 3600 1 210   440 1800 1 6.3 150 67 1
floats-cdfpl/square_1_false-unreach-call_true-termination.i .90  26 11    1 1.7   24   21    1 1.6   23   21    1 18   400 150 1 4.8  64 73   1 8.1 430 110 0 8.2 430 110 0 4.7   57 55    1 29 1200 230 1 .80 61 8.8 1 33   1300 290 0 390    200 2700   0 .17  17 2.2  0 80   460 670 1 29   370 210 0 81   460 660 1 25   350 210 1 7.4 150 94 1
floats-cdfpl/square_2_false-unreach-call_true-termination.i .99  26 12    1 1.8   24   21    0 2.1   26   25    1 180   590 1800 1 6.9  62 85   1 8.3 430 98 0 8.4 430 100 0 6.8   55 78    1 200 1400 1500 1 1.2  64 13   0 32   1300 320 0 830    280 6700   0 .21  17 1.7  0 88   460 700 1 29   370 230 0 86   460 780 1 200   500 1400 1 76   150 1000 1
floats-cdfpl/square_3_false-unreach-call_true-termination.i .71  24 8.2  1 1.5   23   19    0 1.5   26   18    1 62   430 560 1 7.6  63 110   1 8.1 430 93 0 8.3 430 120 0 7.5   55 95    1 71 1300 620 1 1.3  65 19   0 33   1200 310 0 880    280 9500   0 .20  17 1.7  0 180   570 1400 1 29   370 240 0 180   550 1400 1 69   360 560 0 9.2 150 120 1
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i 8.6   63 90    2 230     150   2200    2 320     95   2200    2 900   620 5800 0 110    100 1400   0 8.2 430 93 0 8.6 430 110 0 36     93 480    2 900 1600 5800 0 4.9  78 62   2 34   2900 320 0 880    1600 6700   0 .17  17 2.0  0 900   1000 7600 0 78   1100 570 0 900   1000 5500 0 93   770 680 2 860   150 11000 0
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i 7.8   63 110    2 140     110   1100    2 100     85   1100    2 900   600 6700 0 120    100 1700   0 8.2 430 98 0 8.3 430 100 0 39     94 570    2 900 1600 6100 0 5.7  78 85   2 33   2900 290 0 880    990 6600   0 .20  17 2.0  0 900   810 6200 0 77   1100 600 0 900   820 6400 0 96   770 840 2 860   150 12000 0
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i 10     64 110    2 170     110   1600    2 410     140   4900    2 900   610 6100 0 130    100 1800   0 8.3 430 110 0 8.3 430 110 0 44     93 650    2 900 1600 6400 0 6.2  79 81   2 34   2900 310 0 880    1200 6400   0 .17  17 1.9  0 900   990 7200 0 80   1100 620 0 900   980 5400 0 94   760 680 2 860   150 10000 0
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i 21     130 240    2 260     210   3100    2 300     240   2800    2 900   540 7300 0 480    200 6000   0 8.2 430 100 0 8.4 430 110 0 160     190 1900    2 900 1700 6600 0 15    120 200   2 44   2900 500 0 880    1500 7900   0 .18  17 1.7  0 900   920 5900 0 73   1500 690 0 900   920 6300 0 130   880 1200 2 860   150 10000 0
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i 32     130 280    2 550     310   4600    2 320     240   3000    2 900   860 8000 0 510    200 5900   0 8.2 430 110 0 8.2 430 88 0 170     190 2000    2 900 2000 6500 0 16    110 200   2 35   2900 330 0 880    2500 5700   0 .17  18 2.0  0 900   1000 6100 0 64   1500 500 0 900   1000 6600 0 140   890 1300 2 860   150 10000 0
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i 27     130 280    2 350     340   2900    2 430     440   4200    2 900   550 6300 0 480    200 5800   0 8.4 430 100 0 8.3 430 98 0 160     190 1800    2 900 1700 6100 0 17    100 180   2 41   2900 400 0 880    2600 5200   0 .17  18 1.9  0 900   1100 6800 0 74   1600 610 0 900   1000 6500 0 130   880 1400 2 860   150 12000 0
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i 33     130 330    2 550     360   4800    2 510     280   4400    2 900   620 8600 0 470    200 6500   0 8.3 430 99 0 8.3 430 96 0 160     190 2100    2 900 1700 6400 0 15    100 180   2 35   2900 330 0 880    1500 5200   0 .20  18 1.9  0 900   1200 7800 0 80   1500 630 0 900   1200 6400 0 140   890 1700 2 860   150 11000 0
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i 51     130 470    2 830     590   8000    2 700     660   6700    2 900   610 8500 0 540    200 6900   0 8.2 430 95 0 8.2 430 100 0 180     190 2100    2 900 1700 6800 0 21    110 250   2 34   2900 350 0 880    1800 7000   0 .19  18 1.7  0 900   920 8000 0 64   1500 630 0 900   910 8600 0 170   890 1400 2 860   150 11000 0
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i 81     220 940    2 870     550   9600    0 880     520   9000    0 900   610 6000 0 890    300 12000   0 8.2 430 110 0 8.3 430 100 0 450     290 5100    2 900 1700 6700 0 43    150 440   2 35   2900 410 0 880    3300 5400   0 .17  18 1.8  0 900   1100 5900 0 62   2000 570 0 900   1100 5400 0 190   980 1600 2 860   230 12000 0
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i 73     210 580    2 880     480   6000    0 670     430   7200    2 900   570 6900 0 900    310 9600   0 8.3 430 110 0 8.3 430 100 0 700     300 11000    2 900 1700 6700 0 35    150 490   2 35   2900 310 0 880    2300 7100   0 .20  17 1.6  0 900   1100 6000 0 70   2000 600 0 900   1100 6500 0 220   970 2000 2 860   230 12000 0
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i 74     190 740    2 880     550   7900    0 720     450   6300    2 900   700 6500 0 900    300 13000   0 8.1 430 98 0 8.3 430 100 0 460     300 6500    2 900 1900 7200 0 50    130 510   2 35   2900 330 0 880    3500 6000   0 .18  18 1.8  0 900   1100 6100 0 63   2000 560 0 900   1100 6700 0 220   980 2300 2 860   270 10000 0
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i 110     210 980    2 880     540   8500    0 880     600   7400    0 900   710 7200 0 900    310 10000   0 8.1 430 120 0 8.4 430 97 0 630     300 7000    2 900 1900 6100 0 46    140 580   2 35   2900 390 0 880    2800 11000   0 .20  18 2.1  0 900   1100 5700 0 73   2000 630 0 900   1100 6000 0 210   990 1900 2 860   240 9900 0
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i 74     220 720    2 880     850   8200    0 880     480   8500    0 900   570 7400 0 900    310 9800   0 8.1 430 110 0 8.4 430 110 0 620     310 6000    2 900 1700 8000 0 54    130 680   2 35   2900 310 0 880    2400 5600   0 .17  19 2.0  0 900   1100 5900 0 65   1900 540 0 900   1100 5200 0 250   980 2100 2 870   230 10000 0
floats-cdfpl/sine_4_true-unreach-call_true-termination.i 25     41 290    2 710     85   8100    2 880     110   10000    0 900   500 5300 0 100    73 1500   0 8.3 430 100 0 8.4 430 120 0 34     64 450    2 900 1500 6600 0 39    74 520   2 32   2800 330 0 880    620 5300   0 .19  17 1.8  0 900   810 8000 0 34   600 280 0 900   810 6100 0 110   670 1400 2 860   150 12000 0
floats-cdfpl/sine_5_true-unreach-call_true-termination.i 1.7   33 21    2 220     77   3100    2 250     86   3100    2 900   500 6700 0 53    72 570   0 8.2 430 110 0 8.6 430 99 0 17     64 220    2 900 1500 7600 0 2.6  70 36   2 33   2800 310 0 880    600 6500   0 .17  18 1.8  0 900   860 5900 0 35   590 270 0 900   860 7300 0 79   680 700 2 860   150 10000 0
floats-cdfpl/sine_6_true-unreach-call_true-termination.i 1.9   31 23    2 19     44   280    2 220     100   2500    2 900   650 7600 0 62    72 760   0 8.3 430 98 0 8.5 430 120 0 20     64 300    2 900 1700 4900 0 2.5  70 35   2 32   2800 300 0 880    600 6500   0 .20  17 2.1  0 900   850 7700 0 34   590 310 0 900   850 6300 0 79   680 910 2 860   150 10000 0
floats-cdfpl/sine_7_true-unreach-call_true-termination.i 1.2   27 17    2 5.9   29   81    2 220     87   3000    2 590   590 4800 2 44    72 570   0 8.3 430 92 0 8.2 430 94 0 14     64 150    2 690 1600 5500 2 2.0  71 25   2 32   2800 310 0 880    630 6000   0 .17  18 2.1  0 900   900 9200 0 35   600 320 0 900   880 6500 0 79   670 750 2 860   150 12000 0
floats-cdfpl/sine_8_true-unreach-call_true-termination.i 1.7   31 24    2 62     60   680    2 40     60   570    2 460   550 4100 2 53    72 790   0 8.2 430 100 0 8.3 430 110 0 17     63 220    2 560 1600 4800 2 2.6  70 38   2 31   2800 270 0 880    720 6500   0 .18  17 2.0  0 900   840 6300 0 34   600 280 0 900   840 7600 0 79   670 660 2 860   150 11000 0
floats-cdfpl/square_4_true-unreach-call_true-termination.i 55     50 800    2 270     110   3600    2 250     140   3900    2 540   570 3900 2 87    66 1100   0 8.1 430 98 0 8.3 430 90 0 29     57 330    2 540 1400 5000 2 190    86 2400   2 32   1300 390 0 880    370 7800   0 .17  17 1.8  0 840   760 5400 2 28   360 210 0 810   780 6000 2 170   500 1900 2 860   150 10000 0
floats-cdfpl/square_5_true-unreach-call_true-termination.i 25     50 360    2 260     110   3100    2 250     110   2400    2 430   510 2900 2 41    67 580   0 8.3 430 100 0 8.4 430 120 0 13     59 180    2 450 1300 3100 2 130    89 1700   2 32   1600 300 0 880    370 9700   0 .17  17 1.8  0 880   860 6300 2 27   360 270 0 880   830 6600 2 310   520 3800 2 860   150 11000 0
floats-cdfpl/square_6_true-unreach-call_true-termination.i 79     68 1100    2 93     62   1200    2 130     90   1500    2 220   500 1600 2 36    67 570   0 8.3 430 110 0 8.2 430 110 0 12     55 180    2 240 1300 1600 2 25    75 330   2 32   1300 270 0 880    560 7700   0 .17  17 1.8  0 900   790 6300 0 28   370 210 0 900   790 6500 0 120   510 1400 2 860   150 12000 0
floats-cdfpl/square_7_true-unreach-call_true-termination.i 85     68 1000    2 66     56   860    2 30     42   390    2 760   490 6700 2 22    65 310   0 8.1 430 110 0 8.4 430 100 0 7.1   61 110    2 750 1300 5700 2 5.9  74 72   2 32   1300 270 0 880    370 9200   0 .16  18 2.3  0 530   850 4600 2 28   360 260 0 510   800 4600 2 87   510 730 2 860   150 12000 0
floats-cdfpl/square_8_true-unreach-call_true-termination.i .79  25 10    2 1.8   21   26    2 2.0   21   24    2 56   370 500 2 17    65 270   0 8.3 430 97 0 8.2 430 110 0 5.5   62 71    2 65 1300 570 2 1.3  68 16   2 32   1300 350 0 880    370 7200   0 .17  17 2.0  0 74   640 580 2 28   370 230 0 73   630 520 2 79   500 610 2 860   150 10000 0
floats-cbmc-regression/float-div1_true-unreach-call.i .30  38 3.3  2 .34  15   5.2  2 .35  17   4.8  2 4.9 350 41 2 10    77 140   0 8.2 430 95 0 8.2 430 120 0 3.2   68 42    2 17 1200 120 2 .96 81 10   2 10   300 88 0 37    250 440   2 .17  15 1.7  0 42   890 400 2 18   480 160 0 43   940 360 2 50   770 460 2 900   180 11000 0
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i .92  120 12    2 .29  24   3.1  2 .31  26   4.5  2 10   800 110 2 1.0  67 11   0 8.3 430 88 0 8.4 430 110 0 .14  28 1.5  2 31 2100 270 2 .95 85 11   2 19   580 170 2 290    590 1900   2 .20  15 1.6  0 13   340 100 0 13   340 100 0 13   330 95 0 45   810 400 2 900   180 13000 0
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i .097 23 .73 2 .043 7.3 .33 2 .065 6.0 .20 2 2.8 250 27 2 .79 65 9.1 0 8.2 370 110 2 8.0 370 130 2 .075 26 .90 2 13 1100 88 2 .36 58 3.2 2 3.6 210 36 2 2.5  74 31   2 .15  16 2.2  2 13   350 100 2 13   340 98 2 12   340 100 2 16   410 140 2 900   150 10000 0
floats-cbmc-regression/float-no-simp2_true-unreach-call.i .69  29 10    2 1.7   10   19    2 1.6   11   22    2 13   330 120 2 6.0  66 68   0 1.6 200 22 0 1.7 200 21 0 1.8   36 27    2 25 1200 230 2 1.5  68 20   2 12   370 110 2 91    190 1100   2 .17  17 1.7  0 48   480 510 2 15   400 160 0 47   480 530 2 69   530 790 2 870   180 12000 0
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i .10  23 1.1  2 .050 7.7 .39 2 .042 6.0 .31 2 2.9 250 30 2 .77 67 8.6 0 8.0 370 110 2 8.1 370 120 2 .080 26 1.1  2 12 1000 77 2 .34 58 3.2 2 3.7 200 37 2 2.5  74 33   2 .14  15 1.6  2 13   360 110 2 12   340 97 2 12   360 110 2 17   430 140 2 900   150 11000 0
floats-cbmc-regression/float-no-simp4_true-unreach-call.i .31  37 3.4  2 .17  9.3 2.6  2 .19  12   2.7  2 4.4 300 42 2 .93 67 9.5 0 1.6 200 22 0 1.7 200 24 0 .14  27 1.4  2 15 1200 95 2 .86 69 7.5 2 16   480 160 2 7.6  290 77   2 .17  16 2.1  0 15   390 140 2 14   370 110 0 15   370 130 2 63   670 640 2 900   180 11000 0
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i .090 24 .91 2 .043 6.6 .40 2 .080 5.6 .22 2 3.0 250 30 2 .80 66 8.2 0 8.0 370 110 2 8.1 370 92 2 .10  26 .79 2 11 1100 90 2 .35 58 3.3 2 3.8 210 37 2 2.6  73 28   2 .14  17 1.6  2 14   360 120 2 16   380 140 2 14   360 110 2 18   430 160 2 900   150 12000 0
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i .10  23 .87 2 .11  5.6 .24 2 .040 6.4 .22 2 2.9 250 26 2 .79 66 8.2 0 8.1 370 91 2 8.0 370 86 2 .085 26 .74 2 13 1000 84 2 .35 58 3.5 2 3.7 210 33 2 2.6  72 34   2 .15  15 1.5  2 12   330 100 2 13   360 110 2 13   370 110 2 16   420 140 2 900   150 12000 0
floats-cbmc-regression/float-no-simp8_true-unreach-call.i .22  28 1.6  2 .079 8.0 .80 2 .12  8.5 .72 2 4.1 290 37 2 .82 65 8.7 0 8.2 430 100 0 8.3 430 140 0 .087 26 .88 2 14 1100 100 2 .74 68 6.3 2 4.0 210 33 2 2.6  73 32   2 .15  16 1.3  2 13   350 110 0 13   340 100 0 14   330 110 0 25   410 200 2 900   170 13000 0
floats-cbmc-regression/float-rounding1_true-unreach-call.i .21  28 1.7  2 .087 7.2 .78 2 .094 9.2 .78 2 4.0 270 33 0 .98 66 13   0 8.2 430 120 0 8.3 430 100 0 .14  27 1.6  2 18 1300 140 0 .73 68 7.1 2 8.2 250 77 0 2.7  79 32   2 .093 13 .68 0 7.3 330 61 0 7.3 340 54 0 7.2 330 59 0 21   420 170 2 900   180 12000 0
floats-cbmc-regression/float-to-double1_true-unreach-call.i .22  28 2.1  2 .14  6.8 1.2  2 .13  9.6 1.5  2 4.0 290 39 2 1.4  66 16   0 8.2 430 100 0 8.2 430 100 0 .28  27 3.1  2 15 1200 120 2 .74 68 7.1 2 11   320 95 2 2.9  130 42   2 .14  16 1.5  0 23   390 270 2 14   370 120 0 25   400 280 2 56   450 650 2 900   180 11000 0
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i .086 24 .90 2 .049 6.2 .25 2 .11  5.5 .21 2 2.7 250 25 2 .81 67 8.2 0 7.9 370 94 2 8.1 370 96 2 .094 26 .71 2 13 1000 89 2 .34 58 3.3 2 3.7 200 29 2 2.5  73 31   2 .13  15 1.6  2 13   360 100 2 12   330 100 2 13   360 110 2 16   420 160 2 900   150 10000 0
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i .12  24 .85 2 .052 6.5 .31 2 .040 5.8 .29 2 3.0 250 27 2 .82 66 8.4 0 8.4 370 100 2 8.0 370 93 2 .085 26 .86 2 13 1200 100 2 .36 58 3.2 2 4.0 220 36 2 2.5  74 36   2 .14  15 1.7  2 13   350 97 2 14   350 110 2 12   340 110 2 18   410 170 2 900   150 12000 0
floats-cbmc-regression/float11_true-unreach-call_true-termination.i .096 24 .88 2 .047 6.6 .37 2 .041 6.5 .29 2 2.9 260 28 2 .82 66 9.1 0 8.2 370 97 2 8.1 370 120 2 .095 26 .97 2 13 1000 90 2 .36 58 3.7 2 3.6 210 36 2 2.5  72 31   2 .13  15 1.5  2 13   340 110 2 15   360 110 2 13   370 120 2 17   410 150 2 900   200 11000 0
floats-cbmc-regression/float12_true-unreach-call_true-termination.i .096 24 .96 2 .085 6.4 .76 2 .060 6.5 .42 2 2.8 260 27 2 1.2  66 13   0 8.2 430 99 0 1.7 200 21 0 .20  26 2.6  2 13 1000 91 2 .36 58 2.7 2 17   360 150 2 4.2  100 53   2 .18  17 1.6  0 17   360 170 2 18   350 160 2 18   350 180 2 26   440 320 2 900   150 11000 0
floats-cbmc-regression/float13_true-unreach-call_true-termination.i .14  24 1.3  2 .054 6.4 .32 2 .051 6.6 .30 2 3.0 250 26 2 .78 66 8.1 0 8.1 370 120 2 8.2 370 99 2 .081 26 .80 2 13 1000 88 2 .37 58 3.9 2 3.7 200 35 2 2.5  74 29   2 .15  16 1.4  2 14   370 100 2 16   370 120 2 14   370 120 2 17   420 150 2 900   150 13000 0
floats-cbmc-regression/float14_true-unreach-call.i .18  28 2.2  2 .11  7.7 .84 2 .075 9.7 .76 2 4.2 280 43 2 .82 67 8.9 0 8.3 430 110 0 8.4 430 110 0 .092 26 .96 2 14 1100 90 2 .70 67 8.3 2 9.2 300 88 2 2.6  87 35   2 .15  15 1.5  0 14   370 110 2 14   360 110 0 14   370 110 2 26   430 200 2 900   190 12000 0
floats-cbmc-regression/float18_true-unreach-call.i 900     2400 10000    0 .19  7.8 2.3  2 .18  9.5 2.2  2 4.0 280 33 0 900    2300 12000   0 8.2 430 100 0 8.4 430 110 0 270     1200 3100    2 12 1300 94 2 .74 67 6.0 2 3.9 210 32 2 2.5  72 33   2 .17  16 1.7  2 12   340 98 0 13   330 100 0 12   320 110 0 45   810 370 2 900   180 13000 0
floats-cbmc-regression/float19_true-unreach-call.i .21  28 1.8  2 .097 7.1 .72 2 .091 9.6 .89 2 4.2 290 40 2 1.0  66 11   0 8.3 430 99 0 8.4 430 120 0 .16  26 1.8  2 15 1200 120 2 .72 67 7.2 2 11   340 120 2 3.0  100 36   2 .18  16 1.6  0 15   390 110 2 14   360 120 0 15   370 120 2 28   430 220 2 900   180 12000 0
floats-cbmc-regression/float1_true-unreach-call_true-termination.i .091 24 .70 2 .078 6.1 .22 2 .041 5.9 .27 2 2.9 250 28 2 .81 66 9.2 0 8.1 370 110 2 8.0 370 89 2 .081 26 .78 2 12 1000 89 2 .36 58 3.0 2 3.8 200 40 2 2.6  80 32   2 .13  15 1.8  2 13   360 110 2 13   360 94 2 13   360 110 2 17   480 160 2 900   150 11000 0
floats-cbmc-regression/float20_true-unreach-call_true-termination.i .14  24 1.3  2 .095 7.9 .85 2 .097 8.1 .77 2 3.0 260 30 2 .94 66 11   0 8.4 430 110 0 8.2 430 97 0 .13  30 1.4  2 13 1000 85 2 .36 59 4.2 2 7.4 330 65 -16 8.0  140 93   2 .19  18 2.1  0 19   390 180 2 49   520 540 2 18   390 160 2 25   490 240 2 900   150 9300 0
floats-cbmc-regression/float21_true-unreach-call.i .25  31 2.8  2 .21  8.4 2.6  2 .19  11   1.7  2 7.8 330 83 2 1.5  67 17   0 8.2 430 110 0 8.4 430 100 0 .32  27 3.5  2 21 1200 160 2 .84 69 9.4 2 15   390 150 2 120    450 940   2 .16  16 1.7  0 59   500 620 2 21   410 190 0 56   500 650 2 66   590 690 2 900   180 13000 0
floats-cbmc-regression/float22_true-unreach-call_true-termination.i .12  24 .70 2 .060 6.4 .55 2 .059 6.1 .64 2 3.2 270 29 2 .97 67 11   0 8.1 370 92 2 8.2 370 99 2 .19  26 1.9  2 15 1200 130 2 .39 59 2.9 2 4.1 220 41 2 5.1  110 71   2 .15  16 1.8  2 170   780 2100 2 900   790 13000 0 200   750 2400 2 56   650 590 2 900   150 12000 0
floats-cbmc-regression/float2_true-unreach-call_true-termination.i .091 24 1.3  2 .072 5.9 .27 2 .037 6.2 .35 2 2.9 260 30 2 .89 67 10   0 8.1 370 110 2 8.1 370 96 2 .10  26 1.1  2 12 1000 81 2 .36 58 3.8 2 3.6 210 33 2 2.5  72 32   2 .13  15 1.5  2 14   360 110 2 14   350 120 2 13   360 120 2 18   430 160 2 900   150 11000 0
floats-cbmc-regression/float3_true-unreach-call_true-termination.i .15  24 .93 2 .078 7.2 .76 2 .073 7.2 .56 2 3.0 280 29 2 .80 67 8.7 0 8.1 370 97 2 8.3 370 100 2 .10  26 .81 2 13 1000 98 2 .35 58 3.9 2 6.1 300 56 2 4.2  120 56   2 .15  17 1.8  0 16   350 160 2 17   340 140 2 17   360 160 2 25   440 230 2 900   150 11000 0
floats-cbmc-regression/float4_true-unreach-call.i 9.5   46 120    2 9.7   25   130    2 10     26   120    2 51   360 670 2 3.1  67 38   0 8.1 430 100 0 8.4 430 110 0 .83  31 10    2 63 1200 690 2 4.2  100 58   2 18   370 170 2 88    190 1100   2 .15  16 1.9  0 86   510 1200 2 16   410 150 0 87   510 1000 2 100   520 1400 2 860   180 11000 0
floats-cbmc-regression/float5_true-unreach-call_true-termination.i .11  24 .78 2 .075 6.3 .60 2 .075 7.4 .64 2 3.1 260 29 2 1.4  65 16   0 8.3 430 120 0 8.2 430 98 0 .28  27 3.5  2 13 1000 88 2 .36 58 3.1 2 6.1 300 57 2 5.5  97 67   2 .16  17 2.1  0 23   330 260 2 37   360 520 2 23   360 240 2 42   440 460 2 900   150 9800 0
floats-cbmc-regression/float6_true-unreach-call_true-termination.i .11  24 .99 2 .069 5.9 .49 2 .099 6.1 .50 2 3.1 260 33 2 .83 66 8.5 0 8.2 430 100 0 8.4 430 93 0 .096 26 1.0  2 14 1100 90 2 .37 59 3.4 2 16   390 140 2 2.7  78 33   2 .17  17 2.0  0 15   370 120 2 20   470 180 2 15   380 120 2 18   420 170 2 900   150 13000 0
floats-cbmc-regression/float8_true-unreach-call.i .53  28 6.3  2 .63  7.7 8.6  2 .65  9.9 8.7  2 7.0 300 79 2 .84 68 9.0 0 1.6 200 22 0 1.7 200 20 0 .11  26 1.0  2 18 1200 160 2 1.1  67 12   2 12   320 110 2 2.6  73 34   2 .16  16 1.7  0 15   370 120 2 14   360 100 0 15   390 120 2 26   430 210 2 900   180 12000 0
floats-cbmc-regression/float_lib1_true-unreach-call.i 6.6   35 66    2 .14  8.6 1.8  2 .14  11   1.4  2 4.2 260 40 2 2.7  67 30   0 8.2 430 110 0 8.3 430 94 0 .54  27 7.0  2 15 1300 120 2 .81 69 9.0 2 13   380 120 2 2.8  80 32   2 .14  16 1.7  0 12   310 90 0 13   340 100 0 12   310 98 0 26   430 200 2 900   180 12000 0
floats-cbmc-regression/float_lib2_true-unreach-call.i .23  29 2.1  2 .13  8.3 1.1  2 .14  11   1.4  2 4.2 290 43 2 .84 67 9.1 0 8.3 430 100 0 8.2 430 110 0 .097 27 1.1  2 14 1100 100 2 .85 68 7.1 2 11   320 100 2 9.3  290 110   2 .13  16 1.5  0 15   370 140 2 14   370 100 0 15   380 120 2 31   610 270 2 900   180 11000 0
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c .096 24 1.2  0 .068 9.2 .61 1 .082 8.9 .46 1 3.1 270 29 1 .18 33 1.6 1 8.4 430 120 0 8.2 430 100 0 .094 26 1.0  1 12 1200 89 1 .37 59 4.5 1 11   320 100 1 3.9  88 57   0 .17  17 2.1  0 16   370 130 1 13   330 110 1 14   330 120 1 9.4 270 84 1 3.7 150 35 1
float-benchs/cast_union_loose_false-unreach-call_true-termination.c .12  24 1.5  1 .083 9.5 .57 1 .085 8.8 .54 1 3.3 280 35 1 .21 33 2.4 1 8.2 430 110 0 8.5 430 110 0 .17  26 1.6  1 14 1100 110 1 .38 59 3.0 0 12   360 120 1 4.7  94 59   0 .19  19 1.8  0 13   350 99 1 14   370 130 1 14   370 110 1 9.9 290 92 1 3.8 150 38 1
float-benchs/cast_union_tight_false-unreach-call_true-termination.c .13  24 1.5  1 .085 9.6 .68 1 .076 9.1 .84 1 3.2 290 29 1 .21 34 2.8 1 8.1 430 100 0 1.7 200 24 0 .15  27 1.7  1 12 1200 94 1 .36 59 3.4 0 14   390 110 1 4.3  100 57   0 .16  17 1.8  0 14   370 110 1 15   360 130 1 13   330 100 1 9.6 280 87 1 3.6 150 33 1
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c .14  24 1.4  1 .091 9.0 .89 1 .13  9.2 .68 1 3.1 280 32 1 .45 36 4.9 1 8.1 430 99 0 1.7 200 22 0 .36  28 5.4  1 12 1200 82 1 .37 59 3.3 1 22   470 190 1 4.0  89 48   1 .22  20 2.8  1 14   370 120 1 15   350 130 1 13   360 110 1 7.5 280 68 1 3.5 150 39 1
float-benchs/inv_Newton_false-unreach-call.c 900     1300 9400    0 880     780   5900    0 880     540   6400    0 5.4 350 60 1 890    300 13000   0 8.3 430 110 0 8.5 430 110 0 900     300 7600    0 14 1300 110 1 900    270 6400   0 84   1000 670 0 880    810 8800   0 .17  18 2.3  0 900   2000 6400 0 68   420 610 0 900   2000 7100 0 560   430 4100 0 27   150 350 1
float-benchs/inv_Newton_false-unreach-call.c.p+cfa-reducer.c .083 24 .82 0 880     12000   4900    0 880     500   8000    0 4.7 350 45 1 88    15000 960   0 8.1 430 100 0 8.2 430 100 0 450     530 4300    -32 14 1300 110 1 900    480 8200   0 200   3100 2100 0 880    650 8900   0 .16  17 1.8  0 900   1800 6600 0 48   430 400 0 900   1800 6100 0 140   15000 1500 0 11   150 140 1
float-benchs/inv_square_false-unreach-call_true-termination.c .14  24 1.3  1 .073 9.7 .70 1 .096 8.8 .48 1 3.1 280 33 1 .37 36 5.2 1 8.3 430 100 0 8.3 430 110 0 .30  28 3.9  1 14 1100 100 1 .37 59 3.7 1 22   510 180 1 3.5  81 45   0 .17  18 2.3  0 13   330 110 1 13   330 110 1 13   370 120 1 7.4 280 69 1 900   150 11000 0
float-benchs/nan_double_false-unreach-call_true-termination.c .11  24 1.0  1 .071 9.0 .40 1 .066 9.5 .42 1 2.9 260 27 1 .14 33 1.6 1 8.2 430 99 0 8.3 430 100 0 .083 26 .97 1 13 1100 92 1 .36 59 3.7 1 9.7 300 90 1 3.2  72 35   0 .15  17 1.8  0 13   360 110 1 13   370 92 1 12   350 100 1 7.2 270 65 1 3.6 150 39 1
float-benchs/nan_float_false-unreach-call_true-termination.c .11  24 1.1  1 .054 9.3 .69 1 .061 9.9 .49 1 2.8 270 26 1 .13 33 1.7 1 8.4 430 110 0 8.3 430 100 0 .076 26 .93 1 13 1100 93 1 .36 59 3.0 1 11   330 110 1 3.2  72 39   0 .16  17 2.0  0 13   370 100 1 12   320 100 1 12   350 110 1 7.2 270 66 1 3.7 200 35 1
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c 3.3   260 34    1 2.6   190   29    1 .25  18   2.1  1 5.5 420 51 1 9.2  110 110   1 8.1 430 120 0 8.4 430 100 0 9.2   100 120    1 15 1200 120 1 .55 62 6.7 1 31   670 340 1 880    3200 7100   0 .18  17 1.8  0 410   2100 4100 1 49   1200 490 0 410   2100 4400 1 15   340 130 1 7.0 280 71 1
float-benchs/sqrt_poly2_false-unreach-call.c .56  41 6.2  1 .53  35   5.9  1 .33  32   4.1  1 15   570 160 1 58    150 840   1 8.1 430 99 0 8.4 430 96 0 58     150 800    1 30 1400 280 1 .66 69 7.0 1 15   470 140 1 880    480 6000   0 .17  17 2.1  0 19   600 170 0 100   720 890 0 19   600 160 0 18   440 170 1 4.1 150 38 1
float-benchs/Muller_Kahan_true-unreach-call.c.p+cfa-reducer.c .10  24 .92 0 .34  7.0 3.0  2 .31  6.3 2.4  2 3.7 260 31 2 .99 67 13   0 8.1 370 110 2 8.1 370 130 2 .10  26 .81 2 15 1200 99 2 .47 59 4.0 2 37   1400 400 0 35    15000 410   0 .14  16 1.6  2 900   2800 9700 0 900   1800 11000 0 900   5600 12000 0 120   1200 1300 2 900   150 11000 0
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c 900     820 8100    0 .31  6.5 3.4  2 .25  6.2 3.3  2 3.8 260 39 2 900    1200 11000   0 8.1 370 100 2 8.2 370 110 2 21     260 280    2 16 1200 110 2 .44 58 3.9 2 42   1400 470 0 36    15000 390   0 .14  16 1.8  2 900   4500 9100 0 900   1900 10000 0 900   7700 9700 0 110   1400 1100 2 900   150 13000 0
float-benchs/Rump_double_true-unreach-call_true-termination.c .15  24 1.5  2 .049 6.9 .39 2 .045 6.4 .32 2 2.9 250 25 2 .78 65 8.2 0 8.0 370 110 2 8.1 370 100 2 .087 26 .90 2 13 1000 82 2 .37 59 3.0 2 3.5 220 33 2 270    740 2400   2 .14  15 1.9  2 24   1000 210 2 27   1600 240 0 24   1000 210 2 28   1100 240 2 900   150 11000 0
float-benchs/Rump_float_true-unreach-call_true-termination.c .12  24 .93 2 .056 7.1 .31 2 .11  6.3 .26 2 2.9 260 25 2 .80 67 8.9 0 8.0 370 110 2 8.0 370 94 2 .10  26 .83 2 11 1200 88 2 .37 59 3.2 2 3.8 210 35 2 95    280 840   2 .15  16 1.8  2 15   450 120 2 24   580 180 0 16   450 130 2 18   520 160 2 900   150 10000 0
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c .15  24 .77 2 .051 7.0 .46 2 .042 6.4 .34 2 2.8 260 28 2 .80 65 9.5 0 7.9 370 93 2 8.2 370 100 2 .085 26 .98 2 13 1000 87 2 .38 59 3.1 2 3.9 220 42 2 2.6  82 33   2 .14  15 1.5  2 13   370 99 2 15   330 140 2 13   340 110 2 15   420 140 2 900   150 13000 0
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c .094 24 .96 2 .050 7.0 .32 2 .044 6.3 .30 2 2.8 250 24 2 .78 65 8.5 0 8.1 370 100 2 8.1 370 97 2 .098 26 1.5  2 13 1000 92 2 .36 59 3.6 2 3.5 220 36 2 2.6  75 38   2 .14  15 1.8  2 13   360 110 2 13   370 120 2 13   360 95 2 16   430 150 2 900   150 12000 0
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c .11  24 .58 2 .049 7.4 .41 2 .041 6.3 .30 2 2.9 260 27 2 .79 66 8.8 0 8.1 370 110 2 8.1 370 100 2 .075 26 .75 2 13 1000 82 2 .37 59 3.0 2 4.0 220 34 2 2.6  75 32   2 .14  15 1.7  2 13   360 120 2 13   360 98 2 13   360 120 2 15   420 130 2 900   150 13000 0
float-benchs/arctan_Pade_true-unreach-call_true-termination.c 59     260 660    2 97     300   1100    2 82     380   1100    2 22   500 260 2 780    510 8900   0 8.2 430 93 0 8.4 430 100 0 250     490 3100    2 32 1400 280 2 5.2  250 78   2 59   2300 540 0 880    4400 7100   0 .18  17 2.4  0 120   2600 1100 0 77   890 610 0 120   2600 1200 0 220   1200 2000 2 870   260 12000 0
float-benchs/bary_diverge_true-unreach-call_true-termination.c 900     420 7800    0 880     1400   9900    0 720     15000   8800    0 910   3100 9000 0 890    200 11000   0 8.2 430 94 0 8.3 430 110 0 900     330 12000    0 920 2600 8100 0 110    15000 1300   0 170   2900 2500 0 880    410 6900   0 900     48 11000    0 900   1100 8600 0 22   360 210 0 900   1000 9500 0 120   990 1400 2 900   150 13000 0
float-benchs/cast_float_union_true-unreach-call.c .11  24 .84 2 .13  5.7 .29 2 .047 6.3 .32 2 3.0 250 28 2 .79 67 9.5 0 8.2 430 100 0 8.4 430 130 0 .11  26 .78 2 13 1100 83 2 .39 59 3.3 0 3.7 230 34 2 2.6  74 32   2 .15  16 1.6  2 7.6 350 58 2 7.9 340 63 2 7.7 350 58 2 13   450 120 2 900   150 12000 0
float-benchs/cos_polynomial_true-unreach-call_true-termination.c 7.0   110 61    2 48     96   360    2 290     160   1900    2 900   1500 9000 0 350    240 4900   0 8.3 430 96 0 8.4 430 100 0 120     240 1400    2 900 2500 6100 0 18    520 200   2 23   570 220 0 880    640 5400   0 .18  17 2.3  0 900   3000 5900 0 150   980 1000 0 900   3000 7100 0 88   930 780 2 860   150 12000 0
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c 900     410 9100    0 880     3100   5900    0 510     15000   5700    0 960   4500 6900 0 900    330 12000   0 8.1 430 100 0 8.3 430 130 0 900     5200 10000    0 910 4400 8900 0 900    4700 6900   0 59   2200 810 0 880    640 7500   0 900     2800 8600    0 900   2600 12000 0 900   5400 8400 0 900   2600 8000 0 900   12000 7300 0 860   150 12000 0
float-benchs/divmul_diverge_true-unreach-call_true-termination.c 900     380 10000    0 880     6200   6900    0 510     15000   5900    0 970   4300 8200 0 900    330 11000   0 8.1 430 110 0 8.5 430 100 0 900     8300 11000    0 910 3000 8300 0 900    4800 6100   0 52   1700 660 0 880    490 8000   0 900     2800 10000    0 900   2600 13000 0 900   5100 9000 0 900   3600 11000 0 900   13000 8100 0 860   150 11000 0
float-benchs/drift_tenth_true-unreach-call.c.p+cfa-reducer.c .56  24 6.4  2 .095 7.1 .71 2 .073 6.6 .54 2 2.8 240 28 2 9.5  67 120   0 8.0 370 92 2 8.1 370 110 2 .42  30 5.2  2 110 1600 1600 2 .36 59 3.3 2 3.8 210 36 2 2.5  74 34   2 .17  16 1.7  2 900   910 9000 0 31   510 300 0 770   920 7600 2 53   520 600 2 900   150 14000 0
float-benchs/drift_tenth_true-unreach-call_true-termination.c .60  24 7.5  2 .080 7.2 .56 2 .12  6.2 .40 2 2.7 250 28 2 9.4  67 130   0 8.0 370 110 2 8.1 370 110 2 .43  29 4.9  2 22 1200 210 2 .36 59 3.0 2 3.5 210 39 2 2.5  72 34   2 .14  16 1.5  2 900   900 7400 0 900   700 8500 0 900   960 7000 2 59   530 620 2 900   150 11000 0
float-benchs/exp_loop_true-unreach-call.c 20     240 240    2 1.0   20   15    2 7.6   22   110    2 840   8700 7900 2 670    300 8400   0 8.2 430 91 0 8.5 430 120 0 12     67 170    2 850 9700 8000 2 1.3  240 15   2 59   1700 680 0 880    640 7500   0 .18  17 2.1  0 900   1300 9000 0 27   380 240 0 900   1400 8800 0 380   1000 3600 2 900   150 10000 0
float-benchs/feedback_diverge_true-unreach-call_true-termination.c 900     2100 9400    0 880     1800   9100    0 620     15000   7000    0 970   4800 8100 0 900    250 11000   0 8.2 430 120 0 8.3 430 100 0 900     8400 8900    0 960 5300 10000 0 900    300 12000   0 65   1700 810 0 880    640 8100   0 900     2800 8400    0 900   2600 11000 0 900   5200 9000 0 900   2100 7500 0 900   8400 8500 0 860   150 11000 0
float-benchs/filter1_true-unreach-call.c.p+cfa-reducer.c .086 24 .97 0 880     2500   9400    0 .046 6.6 .28 0 20   890 170 2 900    580 10000   0 8.3 430 110 0 8.4 430 110 0 900     1100 10000    0 30 1700 210 2 900    860 9300   0 98   910 1200 0 880    500 8100   0 900     2800 11000    0 900   1100 11000 0 49   460 540 0 900   1100 11000 0 840   830 5800 0 900   150 10000 0
float-benchs/filter1_true-unreach-call.c.v+lhb-reducer.c .10  24 .83 0 880     2800   8700    0 .079 6.5 .28 0 31   1100 230 2 320    15000 3800   0 8.2 430 110 0 8.4 430 100 0 56     140 780    2 49 2100 440 2 900    1000 12000   0 140   2000 2200 0 880    640 6800   0 900     2800 8400    0 900   1100 8700 0 52   480 520 0 900   1200 10000 0 900   1200 7600 0 900   160 11000 0
float-benchs/filter1_true-unreach-call.c.v+nlh-reducer.c .11  25 .90 0 880     2800   11000    0 .053 6.4 .36 0 28   900 220 2 340    15000 4300   0 8.2 430 99 0 8.2 430 100 0 59     140 740    2 45 1700 410 2 900    980 11000   0 140   1800 1800 0 880    460 8100   0 900     2800 9900    0 870   1100 11000 2 66   540 610 0 900   1100 8700 0 900   1200 8000 0 900   160 11000 0
float-benchs/filter1_true-unreach-call_true-termination.c 900     1800 11000    0 880     1600   9500    0 880     4100   11000    0 20   880 170 2 900    680 12000   0 8.3 430 110 0 8.5 430 100 0 50     100 760    2 28 1400 200 2 900    900 6100   0 54   550 520 0 880    780 11000   0 900     2600 9200    0 220   720 2800 2 43   400 400 0 220   780 1900 2 69   780 690 2 900   150 11000 0
float-benchs/filter2_alt_true-unreach-call.c 900     210 10000    0 880     340   9600    0 880     220   11000    0 900   1100 10000 0 900    240 12000   0 8.3 430 120 0 8.3 430 93 0 900     250 10000    0 900 1900 7100 0 900    260 10000   0 120   2800 1500 0 880    360 8000   0 900     48 11000    0 900   1000 7800 0 22   350 190 0 900   1000 8200 0 900   870 9400 0 900   160 11000 0
float-benchs/filter2_iterated_true-unreach-call.c 900     610 7300    0 560     15000   8100    0 420     15000   5700    0 900   2200 10000 0 900    750 11000   0 8.0 370 90 2 8.1 370 97 2 900     1100 12000    0 900 3000 8800 0 900    10000 13000   0 100   2100 1600 0 880    8300 13000   0 900     14000 14000    0 38   2200 430 0 23   2200 200 0 40   2200 480 0 290   920 2700 0 7.5 150 96 0
float-benchs/filter2_reinit_true-unreach-call_true-termination.c 900     780 7500    0 880     740   8700    0 .98  33   15    0 960   3300 10000 0 890    390 11000   0 8.2 430 99 0 8.4 430 100 0 900     400 12000    0 960 4100 9600 0 630    15000 8200   0 58   780 510 0 880    710 8000   0 900     65 9600    0 900   2500 8400 0 53   450 510 0 900   2500 8900 0 820   1000 7100 0 860   150 12000 0
float-benchs/filter2_set_true-unreach-call_true-termination.c 900     560 5000    0 880     1800   8100    0 880     540   8500    0 960   3700 12000 0 900    310 10000   0 8.3 430 100 0 8.3 430 92 0 900     380 8800    0 960 3500 10000 0 900    810 10000   0 59   990 490 0 880    580 7700   0 .17  17 2.0  0 900   3800 8100 0 35   540 270 0 600   3900 4800 0 860   870 7100 0 860   150 11000 0
float-benchs/filter2_true-unreach-call_true-termination.c 900     680 8200    0 870     710   9700    0 880     290   8700    0 960   2900 11000 0 900    310 9400   0 8.3 430 110 0 8.4 430 110 0 900     350 12000    0 960 3100 11000 0 900    590 9500   0 54   810 570 0 880    600 7600   0 900     56 11000    0 900   2900 10000 0 34   420 270 0 900   2700 9300 0 900   710 7300 0 860   150 12000 0
float-benchs/filter_iir_true-unreach-call.c 900     310 9000    0 880     850   7300    0 880     380   8900    0 3.7 300 29 2 900    480 9600   0 8.2 430 98 0 8.2 430 100 0 900     560 12000    0 13 1200 100 2 900    1100 11000   0 13   310 120 0 880    680 7200   0 900     54 10000    0 900   2700 8400 0 220   1200 2100 0 900   2600 8400 0 93   1300 980 2 860   210 9600 0
float-benchs/float_double_true-unreach-call_true-termination.c .13  24 .72 2 .050 7.8 .32 2 .044 6.4 .27 2 2.8 250 27 2 .80 66 8.9 0 8.1 370 98 2 8.1 370 110 2 .076 26 .68 2 11 1200 86 2 .37 59 3.4 2 3.8 210 41 2 2.5  77 30   2 .14  16 1.5  2 13   370 130 2 12   330 93 2 14   360 110 2 15   400 140 2 900   150 11000 0
float-benchs/image_filter_true-unreach-call.c 900     1000 9300    0 880     3000   6600    0 880     5500   10000    0 330   15000 3900 0 900    510 10000   0 8.3 430 97 0 8.4 430 120 0 900     1900 9300    0 260 15000 2700 0 900    12000 6700   0 46   3900 470 0 68    15000 500   0 .24  21 2.8  0 900   620 12000 0 900   520 12000 0 900   630 13000 0 92   3000 990 0 870   400 9600 0
float-benchs/interpolation2_true-unreach-call.c.p+cfa-reducer.c .093 24 .86 0 .91  29   11    2 .98  29   13    2 24   660 260 2 2.5  67 30   0 8.0 430 110 0 8.1 430 110 0 3.0   49 39    2 46 1500 560 2 .59 75 6.8 2 70   1800 540 2 190    240 2200   2 .17  18 1.9  0 900   1600 6700 0 28   380 320 0 900   1600 7300 0 66   520 620 2 900   160 12000 0
float-benchs/interpolation2_true-unreach-call.c.v+cfa-reducer.c .082 24 .91 0 .94  29   13    2 .97  29   11    2 270   790 3500 2 9.2  100 100   0 8.1 430 98 0 8.3 430 100 0 3.1   50 48    2 290 1500 3900 2 .61 76 5.6 2 70   1800 580 2 190    210 2000   2 .16  18 1.7  0 900   1600 6000 0 900   1500 7300 0 900   1600 7300 0 84   520 900 2 900   160 14000 0
float-benchs/interpolation2_true-unreach-call.c.v+nlh-reducer.c .092 25 .78 0 1.1   29   13    2 1.3   30   16    2 25   490 280 2 2.6  67 33   0 8.1 430 110 0 8.2 430 100 0 2.6   59 32    2 32 1400 350 2 .62 76 6.1 2 56   1900 630 0 230    220 2100   2 .20  22 2.0  0 900   1600 7900 0 900   1500 8900 0 900   1700 7400 0 71   520 680 2 900   160 11000 0
float-benchs/interpolation2_true-unreach-call_true-termination.c .39  24 3.6  2 .52  12   7.4  2 .65  12   8.3  2 23   620 240 2 5.3  68 64   0 8.3 430 110 0 8.2 430 130 0 4.2   45 47    2 28 1400 260 2 .57 66 6.3 2 79   1900 610 2 190    220 2500   2 .17  18 2.2  0 900   1600 7400 0 27   380 230 0 900   1600 8000 0 78   510 740 2 900   150 11000 0
float-benchs/interpolation_true-unreach-call.c.p+cfa-reducer.c .11  24 .81 0 .62  20   6.5  2 .62  21   8.5  2 16   610 140 2 1.9  67 24   0 8.2 430 120 0 8.5 430 120 0 2.0   41 29    2 24 1400 180 2 .47 66 3.9 2 66   1800 470 2 70    160 710   2 .17  17 1.7  0 900   1500 9800 0 390   1100 3300 0 900   1500 6200 0 61   520 650 2 900   160 12000 0
float-benchs/interpolation_true-unreach-call.c.v+cfa-reducer.c .090 24 .65 0 .58  20   8.0  2 .57  21   7.2  2 23   580 250 2 4.2  79 55   0 8.3 430 110 0 8.5 430 110 0 2.0   41 29    2 32 1400 350 2 .47 66 5.1 2 66   1800 470 2 84    210 790   2 .16  17 2.1  0 900   1500 7600 0 900   1500 6700 0 900   1500 7800 0 69   510 730 2 900   150 11000 0
float-benchs/interpolation_true-unreach-call.c.v+nlh-reducer.c .093 24 .88 0 .67  21   8.3  2 .75  21   10    2 19   460 250 2 2.0  67 24   0 8.2 430 99 0 8.4 430 90 0 1.7   48 26    2 27 1400 250 2 .48 67 5.1 2 54   1700 560 0 100    200 1200   2 .16  17 2.2  0 900   1500 8100 0 900   1300 7700 0 900   1500 6400 0 66   490 710 2 900   160 11000 0
float-benchs/interpolation_true-unreach-call_true-termination.c .20  24 2.9  2 .25  8.7 3.0  2 .36  9.6 5.0  2 14   550 140 2 2.1  67 26   0 8.2 430 110 0 8.4 430 94 0 2.2   39 33    2 21 1300 170 2 .45 61 4.3 2 78   1700 530 2 77    150 1200   2 .19  17 2.0  0 900   1700 7600 0 190   790 2200 0 900   1600 7000 0 170   510 2000 2 900   200 11000 0
float-benchs/inv_Newton_true-unreach-call.c 900     1000 8500    0 880     440   7200    0 880     390   7700    0 900   2500 8600 0 900    280 13000   0 8.1 430 120 0 8.4 430 100 0 900     300 10000    0 900 3500 8800 0 900    220 5500   0 76   1000 640 0 880    800 7800   0 .17  18 2.4  0 500   1600 4900 0 25   380 220 2 550   1900 3900 0 580   410 4500 0 900   150 11000 0
float-benchs/inv_sqrt_Quake_true-unreach-call.c.v+cfa-reducer.c .088 24 .72 0 .39  18   5.2  2 .94  20   10    2 4.6 310 43 2 9.7  65 110   0 8.2 430 94 0 8.3 430 120 0 4.5   48 58    2 16 1200 120 2 .73 71 7.8 2 13   410 130 2 720    340 5300   2 .16  17 1.8  0 120   1700 950 0 34   440 290 0 120   1700 890 0 52   550 570 2 900   150 14000 0
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c .28  24 3.7  2 .46  12   5.7  2 .24  12   3.1  2 3.4 280 33 2 3.9  66 43   0 8.1 430 110 0 8.4 430 100 0 1.1   40 14    2 14 1100 110 2 .76 61 9.0 2 38   840 290 2 150    170 1600   2 .17  18 2.4  0 110   1800 1000 2 55   370 620 0 110   1800 930 2 48   670 480 2 860   150 11000 0
float-benchs/inv_square_int_true-unreach-call_true-termination.c .13  24 1.2  2 .14  6.9 .92 2 .11  7.2 1.0  2 3.1 260 29 2 1.6  66 21   0 8.3 430 120 0 1.8 200 22 0 .36  29 4.4  2 15 1200 100 2 .40 59 3.3 2 27   470 230 2 4.1  89 52   2 .18  19 2.4  2 20   340 190 2 18   360 140 2 21   370 230 2 24   440 260 2 900   150 11000 0
float-benchs/inv_square_true-unreach-call_true-termination.c .12  24 1.3  2 .14  6.3 .59 2 .084 6.9 .78 2 2.9 270 27 2 1.5  66 16   0 8.1 430 120 0 8.3 430 110 0 .30  28 4.3  2 14 1100 100 2 .38 59 3.1 2 6.2 310 50 2 3.9  81 51   2 .19  18 1.8  0 66   370 870 2 17   350 170 2 67   370 790 2 47   440 470 2 900   150 11000 0
float-benchs/loop_true-unreach-call.c 900     330 7300    0 360     15000   5500    0 260     15000   3400    0 960   1200 13000 0 900    300 13000   0 440   2300 4400 2 450   2300 4300 2 900     1800 13000    0 900 3700 8700 0 900    14000 11000   0 37   1300 400 0 880    480 7800   2 13     740 180    2 180   450 2300 2 110   660 1300 0 220   540 2500 2 78   680 900 2 900   150 11000 0
float-benchs/mea8000_true-unreach-call.c 900     2800 9400    0 250     14000   2900    0 100     15000   1200    0 5.5 320 51 0 900    1500 11000   0 1.2 170 13 0 1.3 170 17 0 900     1900 8200    0 920 8100 8700 0 51    15000 680   0 27   830 230 0 1.3  49 17   0 900     51 9200    0 900   6200 6800 0 900   5500 11000 0 900   6700 9300 0 540   15000 4300 0 4.5 160 45 0
float-benchs/nan_double_range_true-unreach-call_true-termination.c .10  24 .78 2 .050 6.1 .36 2 .049 6.8 .43 2 2.8 250 25 2 .80 65 8.4 0 8.2 430 100 0 8.4 430 110 0 .075 26 .92 2 12 1200 88 2 .36 59 3.4 2 10   300 110 2 2.5  72 31   2 .16  18 1.8  0 12   330 110 2 14   370 100 2 13   350 98 2 16   410 140 2 900   150 12000 0
float-benchs/nan_float_range_true-unreach-call_true-termination.c .13  24 .72 2 .067 6.6 .33 2 .053 6.5 .35 2 3.0 260 25 2 .80 66 8.4 0 8.1 430 120 0 8.3 430 100 0 .11  26 .82 2 11 1200 88 2 .36 58 3.0 2 10   300 110 2 2.6  74 41   2 .17  17 2.3  0 13   340 120 2 13   330 100 2 14   370 130 2 18   440 200 2 900   150 12000 0
float-benchs/rlim_exit_true-unreach-call_true-termination.c 900     2400 12000    0 880     5300   6600    0 170     15000   2500    0 960   4200 8500 0 900    230 12000   0 8.2 430 120 0 8.4 430 98 0 900     12000 10000    0 960 4800 9100 0 900    2000 9700   0 110   1700 1500 0 880    660 8100   0 900     51 12000    0 900   1700 12000 0 900   5200 12000 0 900   1300 7900 0 100   15000 1300 0 900   150 11000 0
float-benchs/rlim_invariant_true-unreach-call.c.p+cfa-reducer.c .12  24 .73 0 880     1500   7900    0 880     2300   12000    0 13   460 98 2 900    1300 12000   0 8.2 430 98 0 8.4 430 95 0 900     1400 8900    0 22 1300 160 2 900    1200 8300   0 570   4100 5500 0 880    440 9100   0 900     54 12000    0 900   1100 10000 0 110   530 1600 0 900   1100 11000 0 900   1800 6900 0 900   150 12000 0
float-benchs/rlim_invariant_true-unreach-call.c.v+lhb-reducer.c .16  25 1.7  0 880     2500   6700    0 880     2500   11000    0 17   660 130 2 270    15000 3100   0 8.3 430 100 0 8.1 430 99 0 590     680 6400    2 26 1600 200 2 900    1300 9800   0 170   2100 2100 0 880    410 9200   0 900     54 9900    0 900   1000 6800 0 170   570 2500 0 900   1000 9900 0 900   3000 11000 0 900   170 11000 0
float-benchs/rlim_invariant_true-unreach-call.c.v+nlh-reducer.c .47  84 5.3  0 880     2500   6500    0 880     2600   10000    0 17   670 120 2 280    15000 3100   0 8.1 430 120 0 8.5 430 110 0 620     700 7200    2 25 1600 160 2 900    1200 5800   0 170   2000 2500 0 880    450 6600   0 900     54 12000    0 900   1000 8000 0 72   480 860 0 900   990 7600 0 900   1400 8400 0 860   170 11000 0
float-benchs/rlim_invariant_true-unreach-call_true-termination.c 900     2300 9700    0 880     1100   6300    0 880     3200   11000    0 9.5 400 74 2 61    170 860   0 8.2 430 110 0 8.3 430 130 0 4.1   39 53    2 20 1300 130 2 130    15000 1800   0 860   4300 9300 0 880    420 9000   0 900     51 9800    0 830   1000 9300 2 57   460 840 0 900   1000 14000 0 60   600 610 2 900   190 10000 0
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call_true-termination.c 900     300 9700    0 880     630   7100    0 870     530   12000    0 900   880 10000 0 900    500 10000   0 8.2 430 92 0 8.4 430 120 0 900     480 12000    0 900 2000 10000 0 13    420 140   2 28   670 290 0 880    3100 6800   0 .18  17 2.2  0 900   1800 6800 0 78   1400 620 0 900   1800 7000 0 900   290 11000 0 870   280 11000 0
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call_true-termination.c 900     310 7800    0 880     630   7700    0 880     510   11000    0 900   1000 10000 0 900    480 11000   0 8.2 430 130 0 8.4 430 100 0 900     490 9800    0 900 1900 7900 0 21    420 210   2 28   690 290 0 880    3700 11000   0 .20  18 2.1  0 900   1800 7000 0 81   1400 660 0 900   1800 7500 0 900   290 11000 0 860   290 11000 0
float-benchs/sin_interpolated_index_true-unreach-call_true-termination.c 900     300 11000    0 880     610   8100    0 880     470   11000    0 900   600 10000 0 710    120 10000   0 8.4 430 97 0 8.5 430 110 0 230     110 2900    2 900 1600 11000 0 170    130 2200   2 29   730 320 0 880    3300 6800   0 .17  17 2.1  0 900   2300 10000 0 46   1200 430 0 900   2400 9100 0 900   290 14000 0 870   280 12000 0
float-benchs/sin_interpolated_negation_true-unreach-call.c 900     540 7200    0 880     4900   6900    0 880     3000   11000    0 900   3400 8700 0 900    920 9100   0 8.2 430 100 0 8.3 430 100 0 900     1700 9200    0 900 4400 8600 0 83    15000 920   0 680   6500 9300 0 880    4600 8600   0 .18  19 2.0  0 900   2400 9300 0 580   2200 4500 0 900   2100 6700 0 340   1500 2900 2 860   500 12000 0
float-benchs/sin_interpolated_smallrange_true-unreach-call.c 900     450 6500    0 870     3500   6800    0 880     1400   12000    0 900   5600 12000 0 900    870 11000   0 8.3 430 120 0 8.4 430 110 0 900     1200 11000    0 900 6100 11000 0 200    15000 1800   0 28   670 290 0 880    3100 7800   0 .20  19 2.0  0 570   3200 4500 0 73   1300 600 0 570   3300 4200 0 230   1500 2100 2 860   300 11000 0
float-benchs/sqrt_Householder_constant_true-unreach-call.c 900     340 7700    0 .85  10   13    2 .79  10   13    2 4.6 270 40 2 900    1100 8600   0 8.2 370 100 2 8.3 370 96 2 900     1400 11000    0 16 1200 110 2 .57 59 5.3 2 470   3500 4100 0 880    2400 6400   0 .15  15 1.7  2 230   3100 1700 0 220   1800 1600 0 250   3000 1800 0 110   1500 1000 2 900   150 13000 0
float-benchs/sqrt_Householder_constant_true-unreach-call.c.p+cfa-reducer.c .092 24 .82 0 1.1   13   14    2 1.1   14   15    2 4.9 270 45 2 900    6900 9200   0 8.1 370 100 2 8.2 370 110 2 140     15000 1500    0 16 1400 120 2 .66 59 6.8 2 470   3600 3200 0 880    8600 9300   0 .16  15 1.9  2 380   3400 3100 0 190   1800 1600 0 840   3900 7800 0 110   1500 1100 2 900   150 11000 0
float-benchs/sqrt_Householder_interval_true-unreach-call.c 900     320 9500    0 880     820   6700    0 880     610   6900    0 900   1600 10000 0 900    500 8400   0 8.1 430 97 0 8.3 430 100 0 900     490 9700    0 900 1800 11000 0 900    370 8100   0 23   720 240 0 880    2600 6800   0 .17  18 1.8  0 160   2700 1300 0 100   1800 990 0 160   2800 1400 0 900   1200 8800 0 860   170 12000 0
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c 900     430 6600    0 880     2700   8900    0 870     340   8500    0 900   3600 9700 0 900    1100 10000   0 8.2 430 94 0 8.4 430 110 0 900     1200 8600    0 900 2200 9800 0 900    700 7700   0 23   700 210 0 880    2500 7700   0 .18  17 2.1  0 110   2600 970 0 110   1800 1300 0 93   2600 790 0 220   15000 2100 0 860   170 11000 0
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c 900     490 6000    0 880     2600   7900    0 880     420   8300    0 900   2500 10000 0 900    850 11000   0 8.1 430 87 0 8.4 430 99 0 900     1200 9200    0 900 2000 9800 0 900    520 7900   0 23   650 210 0 880    2400 6500   0 .17  17 1.8  0 120   2600 1000 0 120   1800 1100 0 120   2600 1200 0 300   15000 3100 0 860   150 11000 0
float-benchs/sqrt_biNewton_pseudoconstant_true-unreach-call.c 900     370 6300    0 880     3300   8900    0 880     460   9200    0 900   3000 8700 0 900    530 8700   0 8.2 430 110 0 8.4 430 98 0 900     1300 10000    0 900 2300 11000 0 900    750 8300   0 23   730 240 0 880    4100 10000   0 .18  18 2.3  0 100   2700 840 0 84   1800 770 0 110   2700 1200 0 97   15000 1100 0 860   180 12000 0
float-benchs/sqrt_poly_true-unreach-call_true-termination.c 1.1   53 12    2 2.0   43   23    2 .89  42   10    2 31   490 370 2 51    160 620   0 8.1 430 95 0 8.2 430 110 0 17     150 200    2 41 1400 370 2 .88 88 10   2 36   700 370 2 880    690 6500   0 .17  18 1.8  0 150   1600 1200 2 100   850 810 0 150   1600 1100 2 76   760 780 2 860   150 10000 0
float-benchs/water_pid_true-unreach-call_true-termination.c 900     800 6900    0 .59  11   7.7  2 .54  7.9 6.6  2 5.1 270 42 2 370    210 4500   0 8.2 370 99 2 8.1 370 96 2 19     120 310    2 15 1200 100 2 .53 59 6.2 2 460   3800 3300 0 880    470 7800   0 .14  16 1.7  2 170   2900 1600 0 110   1800 830 0 150   3000 1500 0 100   1700 1000 2 900   150 11000 0
float-benchs/zonotope_2_true-unreach-call_true-termination.c 900     330 8700    0 110     4500   1500    2 93     1900   1400    2 970   3600 6800 0 900    370 10000   0 22   410 240 2 22   410 250 2 900     5000 11000    0 960 4700 9700 0 110    2000 1500   2 830   3300 6000 0 580    1000 4900   2 1.2   64 20    2 900   2300 8500 0 230   660 2000 0 900   2100 8300 0 210   1800 2500 2 900   150 14000 0
float-benchs/zonotope_3_true-unreach-call.c.p+cfa-reducer.c .092 25 .82 0 870     13000   8700    0 880     6300   6200    0 960   4900 8400 0 4.8  78 60   0 8.1 430 97 0 8.3 430 79 0 .30  28 3.8  2 120 1800 1100 2 900    3700 6200   0 130   2400 1800 0 560    760 4100   2 900     55 11000    0 900   3700 13000 0 900   5300 11000 0 710   6200 5700 2 900   6000 9300 0 900   160 12000 0
float-benchs/zonotope_3_true-unreach-call.c.v+lhb-reducer.c .13  28 1.1  0 880     13000   10000    0 880     2900   6600    0 970   4200 8900 0 7.0  110 96   0 8.2 430 110 0 8.4 430 100 0 1.7   54 25    2 140 2100 1400 2 900    3700 6000   0 270   2900 3500 0 880    6400 8400   0 900     56 10000    0 900   3600 14000 0 900   5500 12000 0 900   9100 7400 0 900   3200 8200 0 870   230 12000 0
float-benchs/zonotope_3_true-unreach-call_true-termination.c 900     2100 12000    0 250     14000   2800    0 280     15000   3400    0 960   5200 10000 0 1.3  66 17   0 8.1 430 91 0 8.2 430 97 0 3.7   49 46    2 21 1400 170 2 240    15000 3300   0 47   1700 460 0 760    640 5400   2 900     52 9800    0 900   5300 10000 0 900   5600 11000 0 900   1300 7800 0 83   2600 840 2 900   150 13000 0
float-benchs/zonotope_loose_true-unreach-call.c.v+cfa-reducer.c .089 24 .84 0 .40  23   5.0  2 .55  23   7.1  2 4.1 320 42 2 5.0  68 60   0 8.1 430 110 0 8.1 430 93 0 5.7   66 73    2 13 1200 99 2 .59 82 6.7 2 22   1000 170 2 190    520 1700   2 .17  17 1.8  0 280   1300 2300 2 50   710 480 0 320   1400 3300 2 48   760 500 2 860   150 11000 0
float-benchs/zonotope_loose_true-unreach-call_true-termination.c .19  24 2.0  2 .34  17   4.0  2 .28  17   3.9  2 3.6 310 36 2 9.0  69 110   0 8.2 430 100 0 8.5 430 120 0 2.8   57 33    2 15 1100 100 2 .51 73 5.4 2 32   1100 330 2 170    490 1200   2 .17  17 2.2  0 130   1100 1100 2 72   760 750 0 160   1200 1400 2 47   930 460 2 900   150 12000 0
float-benchs/zonotope_tight_true-unreach-call_true-termination.c .21  24 2.1  2 .25  17   3.0  2 .28  17   3.3  2 3.7 320 33 2 9.2  69 130   0 8.3 430 110 0 8.3 430 110 0 2.9   58 33    2 13 1200 100 2 .52 72 5.0 2 32   1100 310 2 210    480 1500   2 .17  17 1.9  0 170   1200 1500 2 66   750 660 0 160   1200 1200 2 47   940 500 2 900   150 12000 0
floats-esbmc-regression/Double_div_true-unreach-call.i 2.6   46 33    2 1.7   14   18    2 .82  11   12    2 6.3 500 49 2 900    460 12000   0 8.2 370 100 2 8.3 370 95 2 14     100 170    2 22 1500 200 2 .63 58 6.2 2 27   1100 270 0 880    1900 10000   0 .14  15 1.7  2 370   2900 3500 2 130   1100 1300 0 410   2700 4500 2 48   730 480 2 3.5 150 32 0
floats-esbmc-regression/Float_div_true-unreach-call.i .59  24 7.2  2 .19  6.6 2.0  2 .22  6.3 1.8  2 3.8 270 38 2 900    250 12000   0 8.3 370 110 2 8.3 370 110 2 1.1   32 12    2 14 1100 110 2 .40 58 4.2 2 27   1000 250 0 880    1000 7300   2 .15  16 1.7  2 250   770 3100 2 65   460 830 0 340   770 3800 2 48   500 610 2 3.4 150 34 0
floats-esbmc-regression/ceil_nondet_true-unreach-call.i 3.5   89 42    2 4.5   34   54    2 49     100   680    2 4.2 290 38 0 2.5  67 31   0 8.1 430 110 0 8.3 430 110 0 .63  36 8.7  2 17 1200 130 0 4.0  99 48   2 9.8 250 140 0 5.2  120 65   2 .076 14 .79 0 12   330 95 0 11   310 94 0 13   340 99 0 34   470 300 2 870   180 11000 0
floats-esbmc-regression/ceil_true-unreach-call.i .44  34 4.0  2 .21  11   2.9  2 .23  14   2.3  2 4.1 290 41 2 .88 67 10   0 8.1 430 100 0 8.3 430 98 0 .094 26 1.1  2 14 1300 110 2 1.5  71 15   2 11   330 100 2 2.8  88 33   2 .13  16 1.6  0 13   340 100 0 12   310 94 0 13   340 100 0 24   410 190 2 900   180 12000 0
floats-esbmc-regression/copysign_true-unreach-call.i .32  31 2.7  2 .17  10   1.7  2 .16  13   1.9  2 4.3 290 39 2 .88 66 9.6 0 8.3 430 100 0 8.1 430 110 0 .094 27 1.0  2 14 1200 110 2 1.1  70 12   2 10   310 85 2 .83 33 11   0 .13  15 1.2  0 13   340 120 0 13   340 110 0 12   320 96 0 25   410 220 2 900   180 13000 0
floats-esbmc-regression/digits_for_true-unreach-call.i 670     730 6700    2 .24  6.1 2.7  2 .24  6.6 2.4  2 960   3800 7200 0 900    360 11000   0 8.0 370 130 2 8.2 370 94 2 4.0   71 56    2 160 2100 1200 0 .39 58 3.7 2 57   1500 790 0 2.6  72 32   2 .14  16 1.5  2 900   3100 7000 0 59   520 580 0 900   2600 7500 0 58   720 550 2 900   150 11000 0
floats-esbmc-regression/digits_while_true-unreach-call.i 670     730 7100    2 .29  7.0 3.7  2 .28  6.6 2.7  2 910   2300 8000 0 890    360 11000   0 8.1 370 94 2 8.0 370 95 2 4.0   72 53    2 73 2500 610 0 .40 58 3.3 2 57   1700 780 0 2.5  71 35   2 .14  16 1.7  2 900   3100 10000 0 64   520 570 0 900   2700 6700 0 57   730 610 2 900   150 12000 0
floats-esbmc-regression/fabs_true-unreach-call.i .23  28 2.0  2 .090 7.9 .86 2 .089 9.7 1.0  2 4.0 260 41 2 .89 66 9.1 0 8.2 430 99 0 8.2 430 99 0 .091 27 1.1  2 14 1300 97 2 .76 67 5.4 2 9.7 310 88 2 2.7  75 38   2 .13  15 1.5  0 14   370 100 2 14   360 130 0 14   370 120 2 24   440 200 2 900   180 13000 0
floats-esbmc-regression/fdim_true-unreach-call.i .22  30 2.0  2 .11  8.3 1.0  2 .16  10   .96 2 3.8 260 34 2 .84 66 9.0 0 8.1 430 110 0 8.5 430 120 0 .095 26 1.0  2 12 1300 97 2 .79 68 6.8 2 11   330 100 2 2.8  83 35   2 .17  15 1.3  0 14   360 110 2 14   360 110 0 15   370 120 2 25   430 210 2 900   180 11000 0
floats-esbmc-regression/floor_nondet_true-unreach-call.i 3.7   88 44    2 4.5   34   59    2 49     100   630    2 4.3 290 35 0 2.5  67 31   0 8.2 430 110 0 8.1 430 97 0 .64  36 7.9  2 18 1200 130 0 5.3  100 68   2 8.2 250 81 0 7.1  120 87   2 .075 13 .95 0 12   340 100 0 11   320 85 0 12   340 110 0 34   460 360 2 870   180 11000 0
floats-esbmc-regression/floor_true-unreach-call.i .46  34 3.9  2 .21  11   2.5  2 .25  14   3.0  2 4.1 290 36 2 .87 67 10   0 8.2 430 120 0 8.3 430 100 0 .10  27 2.0  2 15 1200 130 2 1.5  71 15   2 11   320 92 2 2.8  87 37   2 .14  15 1.8  0 13   340 110 0 13   320 110 0 12   310 100 0 24   420 190 2 900   220 10000 0
floats-esbmc-regression/fmax_true-unreach-call.i .32  31 2.8  2 .12  8.0 1.3  2 .12  11   1.4  2 3.9 260 34 2 .86 65 9.3 0 8.3 430 110 0 8.5 430 100 0 .091 26 1.0  2 14 1100 110 2 1.1  70 10   2 3.9 220 36 2 2.5  72 30   2 .13  15 1.6  0 13   370 110 2 14   360 110 0 14   360 120 2 23   400 180 2 900   180 11000 0
floats-esbmc-regression/fmin_true-unreach-call.i .34  32 3.1  2 .12  8.4 1.3  2 .13  11   1.3  2 3.8 260 38 2 .86 66 11   0 8.2 430 95 0 8.3 430 98 0 .11  26 1.0  2 14 1100 120 2 1.1  70 11   2 3.9 210 35 2 2.6  73 31   2 .13  16 1.5  0 14   370 97 2 13   360 120 0 14   360 120 2 23   430 210 2 900   180 10000 0
floats-esbmc-regression/fmod2_true-unreach-call.i .95  96 9.3  2 .21  11   2.3  2 .22  14   3.1  2 7.7 500 77 2 .86 65 9.1 0 8.3 430 96 0 8.3 430 100 0 .11  26 1.9  2 20 1400 170 2 1.9  71 18   2 11   340 100 2 39    15000 550   0 .20  16 1.5  0 13   330 88 0 13   330 100 0 13   330 94 0 32   620 290 2 900   180 12000 0
floats-esbmc-regression/fmod3_true-unreach-call.i .93  95 9.1  2 .22  11   2.5  2 .24  14   3.0  2 7.3 500 69 2 .86 66 10   0 8.2 430 100 0 8.5 430 110 0 .096 26 1.0  2 19 1400 150 2 1.8  71 18   2 11   350 95 2 38    15000 570   0 .16  16 1.8  0 12   320 110 0 12   320 92 0 13   340 93 0 33   670 280 2 900   180 12000 0
floats-esbmc-regression/fmod_true-unreach-call.i .92  83 8.5  2 .22  11   2.6  2 .23  14   2.7  2 3.9 260 35 2 .87 66 9.8 0 8.2 430 98 0 8.3 430 120 0 .10  26 2.0  2 14 1100 110 2 1.9  71 15   2 3.9 220 40 2 38    15000 440   0 .15  20 1.9  2 12   330 100 0 13   340 110 0 11   300 86 0 24   430 200 2 900   180 10000 0
floats-esbmc-regression/isgreater_true-unreach-call.i .20  28 1.9  2 .078 7.9 .73 2 .081 9.3 .60 2 4.0 260 37 2 .87 66 8.6 0 8.1 370 100 2 8.4 370 110 2 .085 27 1.1  2 13 1300 110 2 .73 67 6.7 2 3.8 210 40 2 2.5  72 30   2 .15  15 1.6  2 15   370 120 2 14   390 130 0 14   370 120 2 23   430 190 2 900   170 10000 0
floats-esbmc-regression/isgreaterequal_true-unreach-call.i .20  28 1.6  2 .074 7.6 1.2  2 .072 10   .68 2 4.0 260 35 2 .88 66 9.8 0 8.1 370 100 2 8.2 370 97 2 .087 26 1.1  2 14 1100 98 2 .71 67 8.1 2 4.0 220 38 2 2.6  72 33   2 .16  15 1.5  2 14   360 110 2 14   360 120 0 14   360 110 2 24   410 200 2 900   180 11000 0
floats-esbmc-regression/isless_true-unreach-call.i .20  28 1.8  2 .076 7.5 .67 2 .073 10   .69 2 4.0 270 34 2 .81 65 8.9 0 8.2 370 99 2 8.2 370 99 2 .090 27 1.1  2 13 1300 100 2 .69 67 7.0 2 3.8 210 36 2 2.5  72 38   2 .14  15 1.5  2 14   370 110 2 14   360 110 0 14   370 120 2 23   420 210 2 900   180 11000 0
floats-esbmc-regression/islessequal_true-unreach-call.i .20  28 1.9  2 .11  7.2 .70 2 .078 10   .65 2 3.9 270 39 2 .82 67 9.0 0 8.3 370 110 2 8.3 370 98 2 .095 26 .97 2 14 1100 110 2 .70 67 7.4 2 3.4 210 32 2 2.6  72 35   2 .14  15 1.6  2 15   360 120 2 14   360 110 0 14   370 130 2 24   430 210 2 900   180 13000 0
floats-esbmc-regression/islessgreater_true-unreach-call.i .22  28 2.1  2 .074 7.4 .69 2 .073 9.9 .67 2 3.9 270 39 2 .83 65 8.9 0 8.0 370 110 2 8.1 370 100 2 .089 27 .93 2 12 1300 110 2 .71 67 7.4 2 3.5 220 37 2 2.6  72 36   2 .18  20 1.7  2 15   360 120 2 13   360 110 0 14   360 110 2 24   410 200 2 900   180 13000 0
floats-esbmc-regression/isunordered_true-unreach-call.i .28  28 2.2  2 .079 7.7 .78 2 .078 9.6 .77 2 3.8 260 37 2 .82 66 9.2 0 8.1 370 99 2 8.4 370 100 2 .089 26 1.0  2 12 1300 95 2 .73 67 7.3 2 3.9 220 43 2 2.6  72 33   2 .15  16 1.5  2 15   370 130 2 14   370 120 0 15   370 140 2 23   410 180 2 900   180 12000 0
floats-esbmc-regression/lrint_true-unreach-call.i .47  33 4.3  2 .22  11   2.5  2 .25  14   2.6  2 3.9 270 36 0 .90 66 11   0 8.4 430 100 0 8.3 430 120 0 .14  27 1.2  2 17 1400 130 0 1.6  71 15   2 8.6 270 80 0 38    240 310   2 .082 13 .87 0 7.5 320 61 0 6.3 310 48 0 7.0 330 53 0 26   430 180 2 900   180 12000 0
floats-esbmc-regression/modf_true-unreach-call.i .40  32 3.3  2 .18  10   2.0  2 .23  14   1.9  2 3.9 270 36 2 .88 66 9.3 0 8.1 430 92 0 8.2 430 100 0 .13  26 1.1  2 13 1300 100 2 1.5  70 13   2 7.8 230 78 0 140    550 1100   2 .14  16 1.7  0 7.2 330 55 0 7.8 330 63 0 7.3 330 61 0 25   470 220 2 900   190 11000 0
floats-esbmc-regression/nan_true-unreach-call.i .26  32 2.1  2 .11  7.4 .67 2 .11  9.0 .77 2 4.1 280 36 2 .86 66 9.4 0 8.1 430 110 0 8.3 430 100 0 .087 26 .92 2 14 1100 110 2 .70 67 9.1 2 9.6 310 91 2 2.9  110 36   2 .14  16 1.6  0 15   390 110 2 15   360 110 0 15   380 110 2 24   420 190 2 2.4 160 23 0
floats-esbmc-regression/nearbyint2_true-unreach-call.i .49  34 4.9  2 .22  11   2.6  2 .23  14   3.5  2 4.0 270 38 0 .93 66 9.8 0 8.3 430 100 0 8.4 430 120 0 .12  27 1.1  2 17 1400 150 0 1.6  72 16   2 7.3 220 66 0 8.0  140 97   2 .090 18 .85 0 7.4 320 57 0 7.3 310 59 0 7.2 330 57 0 25   530 210 2 900   180 12000 0
floats-esbmc-regression/nearbyint_true-unreach-call.i .49  34 4.3  2 .38  11   4.8  2 .41  14   5.6  2 10   470 89 0 .93 67 9.7 0 8.1 430 110 0 8.3 430 120 0 .16  27 2.0  2 19 1200 150 0 1.6  72 14   2 7.4 210 67 0 21    230 230   2 .095 13 .77 0 6.4 320 56 0 7.6 330 57 0 7.4 350 56 0 220   900 2200 2 900   180 14000 0
floats-esbmc-regression/remainder_true-unreach-call.i 1.1   110 12    2 .25  11   3.0  2 .24  14   2.7  2 4.3 290 43 2 .96 67 10   0 8.4 430 120 0 8.3 430 110 0 .13  27 1.6  2 16 1100 110 2 1.9  72 16   2 14   370 140 2 2.8  82 33   2 .15  15 1.4  0 12   310 110 0 12   320 98 0 12   330 94 0 25   420 210 2 900   170 14000 0
floats-esbmc-regression/rint2_true-unreach-call.i .49  34 4.6  2 .22  11   3.0  2 .23  14   2.6  2 3.9 270 36 0 .89 66 9.8 0 8.3 430 110 0 8.4 430 110 0 .11  27 .94 2 17 1400 120 0 1.5  71 15   2 6.8 210 66 0 8.2  140 100   2 .078 13 .82 0 6.9 320 52 0 6.9 320 55 0 7.0 340 51 0 26   550 200 2 900   180 12000 0
floats-esbmc-regression/rint_true-unreach-call.i .50  34 4.3  2 .38  11   5.6  2 .41  14   5.6  2 11   470 97 0 .90 66 11   0 8.1 430 99 0 8.2 430 100 0 .15  27 1.9  2 20 1200 140 0 1.6  71 15   2 7.4 210 64 0 21    230 190   2 .074 13 .91 0 7.1 350 61 0 7.2 330 56 0 6.4 330 57 0 220   900 2900 2 900   180 12000 0
floats-esbmc-regression/round_nondet_true-unreach-call.i 3.9   120 49    2 5.0   47   68    2 880     2400   12000    0 4.3 290 38 0 3.4  67 39   0 8.2 430 120 0 8.4 430 120 0 .95  40 12    2 18 1200 130 0 5.3  600 64   2 7.4 260 73 0 880    410 8800   0 .070 13 .74 0 12   320 110 0 12   340 110 0 12   330 88 0 35   430 310 2 870   180 13000 0
floats-esbmc-regression/round_true-unreach-call.i .53  41 6.4  2 .24  12   2.9  2 .27  14   3.0  2 4.6 290 39 2 .96 66 10   0 8.2 430 95 0 8.2 430 120 0 .14  27 1.6  2 16 1100 120 2 1.6  72 15   2 14   390 150 2 9.3  130 110   2 .15  16 1.7  0 13   340 110 0 13   320 110 0 12   340 100 0 26   430 210 2 900   170 11000 0
floats-esbmc-regression/rounding_functions_true-unreach-call.i .50  36 4.8  2 .26  11   3.1  2 .24  14   3.0  2 4.3 270 41 2 .97 66 11   0 8.3 430 99 0 8.2 430 110 0 .14  27 1.7  2 14 1300 120 2 1.6  71 16   2 3.9 220 37 2 2.8  81 35   2 .13  16 1.6  0 14   370 130 0 14   360 120 0 14   360 100 0 26   430 210 2 860   180 10000 0
floats-esbmc-regression/trunc_nondet_2_true-unreach-call.i 1.9   40 22    2 2.7   16   38    2 2.1   17   30    2 5.8 300 67 2 7.2  65 89   0 8.2 430 89 0 8.2 430 100 0 2.2   33 32    2 18 1200 150 2 2.8  76 28   2 32   510 360 2 57    130 680   2 .17  16 1.9  0 130   620 1200 2 14   420 110 0 120   600 1300 2 33   420 310 2 870   230 10000 0
floats-esbmc-regression/trunc_nondet_true-unreach-call.i 2.2   90 25    2 3.1   34   47    2 40     100   520    2 4.3 290 37 0 2.2  67 27   0 8.4 430 110 0 8.6 430 130 0 .58  35 7.0  2 18 1200 150 0 4.1  100 62   2 7.9 250 73 0 4.4  110 63   2 .079 13 .91 0 12   340 95 0 12   320 100 0 12   330 110 0 32   420 300 2 870   180 11000 0
floats-esbmc-regression/trunc_true-unreach-call.i .45  34 4.1  2 .21  12   2.9  2 .23  14   2.3  2 3.9 270 33 2 .86 65 9.2 0 8.2 430 89 0 8.3 430 100 0 .10  26 1.0  2 15 1200 120 2 1.5  71 15   2 10   320 100 2 2.8  86 36   2 .13  16 1.6  0 13   350 100 0 13   350 110 0 12   310 91 0 24   410 220 2 900   180 10000 0
floats-esbmc-regression/Double_div_bad_false-unreach-call.i 900     410 10000    0 5.8   33   67    1 3.9   41   58    1 200   4800 2300 1 900    460 11000   0 8.6 430 100 1 8.6 430 100 1 44     370 600    1 900 5400 6700 0 5.8  59 88   1 27   940 260 0 880    1700 8600   0 .17  16 2.0  1 260   2800 2300 0 55   990 510 0 360   4100 3300 0 13   270 100 1 3.5 150 37 1
floats-esbmc-regression/Float_div_bad_false-unreach-call.i 900     360 12000    0 .53  10   5.1  1 .41  9.9 5.3  1 14   690 110 1 900    350 11000   0 8.3 430 120 1 8.3 430 99 1 2.1   39 32    1 24 1300 190 1 .76 58 8.2 1 27   980 290 0 880    970 7100   0 .17  17 1.9  1 900   1900 7300 0 52   420 520 0 900   1900 10000 0 13   270 91 1 3.6 150 39 1
floats-esbmc-regression/digits_bad_for_false-unreach-call.i 900     760 7900    0 .27  9.9 3.2  1 .28  9.3 3.0  1 960   3600 7700 0 900    350 12000   0 7.8 430 96 0 7.8 430 110 0 6.8   73 85    1 30 1700 250 0 .51 58 5.8 1 59   1700 690 0 3.2  72 40   1 .17  15 2.4  1 900   2900 6600 0 900   740 7100 0 900   2500 7000 0 18   350 140 0 3.4 160 35 1
floats-esbmc-regression/digits_bad_while_false-unreach-call.i 900     760 6800    0 .31  10   2.9  1 .27  9.5 3.7  1 910   1900 7800 0 900    340 11000   0 7.9 430 100 0 8.2 430 110 0 6.8   73 100    1 27 1900 220 0 .50 58 5.1 1 57   1700 690 0 3.3  72 39   1 .16  16 2.0  1 900   3000 7800 0 68   520 630 0 900   2600 7500 0 13   260 98 1 3.5 150 36 1
floats-esbmc-regression/Double_div_true-unreach-call.i.p+cfa-reducer.c 1.8   42 25    2 1.8   13   20    2 .80  9.0 10    2 6.4 500 54 2 900    420 11000   0 8.5 370 100 2 8.3 370 100 2 14     120 210    2 24 1700 200 2 .63 59 6.9 2 26   980 250 0 880    1600 6800   0 .15  16 1.8  2 300   2700 2700 2 55   890 500 0 320   2700 3200 2 180   780 1900 2 3.5 150 32 0
floats-esbmc-regression/Float_div_true-unreach-call.i.p+cfa-reducer.c .71  27 8.2  2 .22  6.5 2.8  2 .19  6.5 2.0  2 3.8 260 30 2 900    760 10000   0 8.1 370 110 2 8.2 370 99 2 3.8   59 47    2 15 1100 110 2 .42 59 3.5 2 26   900 270 0 880    2100 8200   0 .13  16 1.8  2 460   2800 3600 0 91   800 750 0 650   4000 5700 0 180   740 2100 2 3.3 150 34 0
floats-esbmc-regression/Double_div_bad_false-unreach-call.i.p+cfa-reducer.c 900     450 8500    0 5.8   34   76    1 3.9   41   51    1 210   5500 2500 1 900    470 11000   0 8.7 430 120 1 8.7 430 110 1 45     430 600    1 900 5600 7400 0 5.9  59 70   1 27   940 280 0 880    1700 9600   0 .18  17 1.8  1 250   2700 2000 0 60   1000 640 0 360   4100 3800 0 13   300 100 1 3.4 150 37 1
floats-esbmc-regression/Float_div_bad_false-unreach-call.i.p+cfa-reducer.c 900     560 7900    0 .51  11   5.7  1 .45  10   6.0  1 13   540 120 1 900    750 10000   0 8.2 430 130 1 8.3 430 100 1 5.5   67 71    1 24 1300 170 1 .74 59 7.9 1 27   900 290 0 880    2100 7700   0 .16  16 1.6  1 340   2700 2400 0 24   490 190 0 510   3700 4600 0 12   270 98 1 3.5 150 37 1
float-newlib/double_req_bl_0210_true-unreach-call.c .16  29 1.0  0 .090 7.9 .77 2 .085 10   .65 2 56   2800 460 2 900    12000 7700   0 8.2 370 110 2 8.2 370 110 2 .58  84 6.4  2 210 4000 2200 2 .41 63 3.6 2 15   1000 120 2 310    2400 2500   2 .26  16 3.0  2 210   1400 1800 2 900   1900 6500 0 210   1500 2100 2 130   1900 1100 2 870   190 11000 0
float-newlib/double_req_bl_0220a_true-unreach-call.c .15  29 1.2  0 .10  8.3 .93 2 .082 10   1.0  2 56   2900 460 2 900    12000 7600   0 8.3 370 100 2 8.2 370 96 2 .51  82 5.0  2 600 5000 7900 2 .41 64 5.6 2 15   1000 110 2 800    4000 5900   2 .25  16 2.5  2 95   1200 770 2 900   1900 6800 0 98   1200 800 2 130   1700 1200 2 870   180 10000 0
float-newlib/double_req_bl_0220b_true-unreach-call.c .12  29 .95 0 .095 8.2 .71 2 .12  9.7 .82 2 54   2600 480 2 900    12000 7400   0 8.2 370 100 2 8.2 370 99 2 .52  83 5.1  2 900 4500 9100 0 .41 63 3.6 2 15   1000 95 2 880    3600 7400   0 .26  16 3.4  2 98   1200 820 2 900   1900 7300 0 100   1200 940 2 170   1900 1400 2 870   180 13000 0
float-newlib/double_req_bl_0240a_true-unreach-call.c .13  29 1.2  0 .11  7.8 .74 2 .074 10   .82 2 54   2700 530 2 900    12000 8400   0 8.3 370 110 2 8.1 370 120 2 .56  86 7.2  2 210 4600 2400 2 .41 63 3.9 2 16   1100 120 2 120    720 1000   2 .25  16 3.0  2 75   1000 760 2 510   1500 3800 2 72   990 660 2 130   1900 1200 2 860   180 9500 0
float-newlib/double_req_bl_0240b_true-unreach-call.c .13  29 1.3  0 .13  7.9 .85 2 .078 11   .70 2 56   2800 530 2 900    12000 7600   0 8.2 370 120 2 8.0 370 120 2 .58  86 6.4  2 210 3900 2200 2 .40 63 3.8 2 15   1000 110 2 180    2200 1700   2 .26  16 3.0  2 76   990 720 2 480   1500 3900 2 76   970 660 2 160   2000 1700 2 860   180 10000 0
float-newlib/double_req_bl_0250a_true-unreach-call.c .43  57 6.0  2 .063 6.6 .55 2 .057 6.9 .54 2 38   2200 370 2 1.2  65 14   0 8.2 370 100 2 8.1 370 100 2 .30  47 3.5  2 79 2800 830 2 .41 60 3.4 2 6.0 400 61 2 440    3500 4800   2 .18  15 2.0  2 79   2200 660 2 180   2200 2000 2 140   2400 1200 2 130   1900 1100 2 900   170 14000 0
float-newlib/double_req_bl_0250b_true-unreach-call.c .43  57 6.2  2 .084 6.3 .38 2 .062 7.3 .39 2 40   2200 330 2 1.3  66 17   0 8.3 370 110 2 8.2 370 110 2 .30  47 3.2  2 82 2800 780 2 .38 60 3.2 2 5.8 340 55 2 420    3500 4000   2 .21  15 1.6  2 150   2500 1400 2 160   2100 1500 2 78   2200 780 2 130   2000 1300 2 900   170 12000 0
float-newlib/double_req_bl_0260_true-unreach-call.c .41  53 4.9  2 .058 7.1 .56 2 .079 7.2 .40 2 41   2000 390 2 1.3  66 15   0 8.2 370 93 2 8.1 370 120 2 .27  47 3.2  2 84 2800 810 2 .39 60 3.9 2 5.7 330 52 2 460    3900 4300   2 .18  15 2.1  2 160   2500 1300 2 190   2300 1700 2 79   2200 650 2 130   1900 1200 2 900   160 11000 0
float-newlib/double_req_bl_0270a_true-unreach-call.c .57  89 6.3  2 .056 6.2 .58 2 .056 6.8 .42 2 38   2200 370 2 1.3  67 16   0 8.3 370 100 2 8.0 370 99 2 .28  47 3.9  2 61 2800 530 2 .36 60 4.2 2 5.8 340 57 2 420    1700 3900   2 .18  15 2.1  2 82   2200 920 2 180   2500 1300 2 89   2200 800 2 93   2000 870 2 900   160 14000 0
float-newlib/double_req_bl_0270b_true-unreach-call.c .56  89 7.1  2 .053 6.5 .52 2 .050 7.2 .61 2 40   2200 360 2 1.2  65 16   0 8.2 370 100 2 8.0 370 97 2 .31  48 3.4  2 61 2800 520 2 .41 60 3.3 2 5.8 330 52 2 420    1700 4900   2 .20  15 1.9  2 100   2300 940 2 180   2500 1300 2 85   2300 930 2 94   2000 970 2 900   160 11000 0
float-newlib/double_req_bl_0281_true-unreach-call.c 1.8   320 19    2 1.8   240   27    2 880     3800   10000    0 40   2300 350 2 1.6  72 21   0 8.2 430 110 0 8.3 430 110 0 .52  77 5.8  2 81 2800 740 2 .40 60 3.6 2 190   3500 2000 0 290    320 2600   2 .19  17 2.3  0 33   1500 320 2 110   1600 830 2 34   1500 270 2 51   1900 550 2 860   390 12000 0
float-newlib/double_req_bl_0310_true-unreach-call.c .12  29 1.3  0 .086 8.1 .85 2 .11  9.6 .71 2 59   2600 490 2 900    12000 8300   0 8.0 370 120 2 8.3 370 120 2 .57  84 6.5  2 900 4700 9500 0 .42 63 3.6 2 15   1000 110 2 160    1400 1500   2 .27  16 3.2  2 300   1500 2700 2 900   1900 7500 0 300   1500 2800 2 160   1900 1400 2 860   180 13000 0
float-newlib/double_req_bl_0320_true-unreach-call.c .12  28 1.4  0 9.0   790   92    2 180     15000   2700    0 53   2600 430 2 900    12000 10000   0 8.3 430 100 0 8.4 430 110 0 .92  120 14    2 270 4200 2800 2 .43 64 3.5 2 410   4500 3500 0 880    4100 9300   0 .28  18 3.4  0 93   1300 800 2 900   1900 6900 0 96   1300 870 2 340   6400 3100 2 860   770 11000 0
float-newlib/double_req_bl_0330a_true-unreach-call.c .13  28 1.4  0 .086 8.3 .78 2 .082 9.8 .73 2 54   2900 500 2 900    12000 7800   0 8.2 370 100 2 8.3 370 100 2 .61  86 6.2  2 900 5300 9100 0 .41 64 3.5 2 15   1000 110 2 110    940 1300   2 .26  16 3.1  2 74   980 640 2 480   1500 3600 2 73   1000 610 2 130   1800 1000 2 870   170 11000 0
float-newlib/double_req_bl_0330b_true-unreach-call.c .13  29 1.0  0 .11  8.0 .80 2 .078 11   .77 2 52   2400 450 2 900    12000 8400   0 8.2 370 88 2 8.4 370 88 2 .56  86 6.5  2 900 5200 7500 0 .46 64 4.2 2 15   1000 120 2 110    980 900   2 .26  16 3.2  2 75   1000 560 2 500   1500 3900 2 79   990 670 2 170   1800 1500 2 860   170 11000 0
float-newlib/double_req_bl_0460_true-unreach-call.c 3.2   450 32    2 9.3   360   100    2 880     1500   12000    0 44   2100 390 2 110    1100 1100   0 8.2 430 120 0 8.4 430 110 0 21     1000 190    2 250 3400 2700 2 .43 66 5.2 2 170   4200 1600 0 880    7800 8200   0 .24  17 2.1  0 170   3100 1500 2 150   2500 1400 0 120   2900 1300 2 130   1800 1200 2 860   460 12000 0
float-newlib/double_req_bl_0470_true-unreach-call.c .47  58 5.4  2 .061 6.4 .56 2 .061 7.4 .41 2 42   2100 360 2 .98 66 10   0 8.2 370 120 2 8.2 370 100 2 .14  27 1.2  2 260 3400 2300 2 .37 60 4.1 2 6.4 360 55 2 460    2600 4600   2 .18  15 2.1  2 85   2500 730 2 180   2500 1500 0 140   2800 1100 2 110   1800 1100 2 900   170 11000 0
float-newlib/double_req_bl_0480_true-unreach-call.c .68  100 7.7  2 .073 6.1 .43 2 .057 7.5 .50 2 45   2200 420 2 1.1  66 12   0 8.3 370 120 2 8.3 370 120 2 .17  28 1.7  2 900 3600 9800 0 .38 61 3.7 2 6.4 360 61 2 880    6100 7800   0 .17  16 2.2  2 73   2400 740 2 160   2500 1300 0 73   2400 740 2 110   1800 1100 2 900   170 11000 0
float-newlib/double_req_bl_0490a_true-unreach-call.c .47  59 5.4  2 .066 7.2 .65 2 .057 8.4 .59 2 42   2100 360 2 1.0  68 11   0 8.2 370 100 2 8.1 370 100 2 .12  28 1.3  2 250 3400 1800 2 .41 61 3.3 2 7.1 470 67 2 450    3200 4400   2 .18  15 2.3  2 110   2600 920 2 150   2500 1400 0 86   2500 770 2 110   1800 1000 2 900   170 11000 0
float-newlib/double_req_bl_0490b_true-unreach-call.c .48  58 5.4  2 .062 6.3 .42 2 .055 7.4 .57 2 43   2200 370 2 .99 67 11   0 8.1 370 95 2 8.3 370 100 2 .13  28 1.3  2 260 3400 2400 2 .40 60 3.4 2 6.5 360 60 2 550    3300 5700   2 .17  15 2.0  2 130   2700 1200 2 150   2500 1200 0 87   2500 830 2 110   1800 1000 2 900   160 12000 0
float-newlib/double_req_bl_0520_true-unreach-call.c .13  29 1.0  0 .083 8.8 .90 2 .11  9.5 .72 2 68   3900 600 2 900    12000 7400   0 8.3 370 100 2 8.2 370 96 2 .69  99 7.6  2 180 4800 1600 2 .40 63 3.7 2 15   1000 120 2 270    3700 2800   2 .27  16 2.6  2 300   2600 3100 2 520   2700 4700 2 300   2600 2800 2 140   2600 1200 2 860   170 13000 0
float-newlib/double_req_bl_0530a_true-unreach-call.c .13  29 1.4  0 .087 8.2 .90 2 .13  9.6 .83 2 68   4100 570 2 900    12000 8500   0 8.2 370 120 2 8.3 370 110 2 .61  94 6.8  2 900 5000 9500 0 .45 64 2.7 2 15   1000 120 2 880    4900 9800   0 .25  15 3.4  2 140   2500 1300 2 650   2800 4800 0 110   2200 1200 2 150   2500 1400 2 870   190 12000 0
float-newlib/double_req_bl_0530b_true-unreach-call.c .13  29 1.3  0 .088 8.0 .78 2 .082 9.6 .95 2 77   3900 670 2 900    12000 7800   0 8.3 370 100 2 8.2 370 120 2 .60  94 7.1  2 900 4500 10000 0 .43 64 4.7 2 15   1000 100 2 880    4800 7300   0 .27  16 3.6  2 110   2200 870 2 660   2800 4700 0 120   2200 1200 2 160   2600 1600 2 860   180 9500 0
float-newlib/double_req_bl_0550a_true-unreach-call.c .13  29 1.1  0 .076 8.4 .82 2 .073 9.5 .81 2 71   3900 650 2 900    12000 8800   0 8.3 370 100 2 8.3 370 100 2 .67  100 9.6  2 170 4800 1900 2 .41 63 4.2 2 16   1000 110 2 100    1300 1000   2 .26  16 3.1  2 92   2200 870 2 470   2500 3400 2 89   2200 870 2 140   2500 1200 2 860   180 10000 0
float-newlib/double_req_bl_0550b_true-unreach-call.c .15  29 1.1  0 .088 8.2 .78 2 .078 10   .85 2 74   4200 680 2 900    12000 9200   0 8.3 370 100 2 8.4 370 110 2 .72  100 7.4  2 180 4800 1700 2 .42 63 4.5 2 15   1000 110 2 94    1500 880   2 .26  16 3.4  2 90   2200 930 2 480   2500 4000 2 86   2200 980 2 160   2600 1400 2 860   190 11000 0
float-newlib/double_req_bl_0620a_true-unreach-call.c .29  50 3.2  2 .11  6.2 .32 2 .082 5.7 .29 2 11   1100 100 2 1.1  66 12   0 8.5 370 95 2 8.2 370 97 2 .17  35 2.1  2 29 2100 290 2 .36 60 4.1 2 4.6 270 46 2 53    1600 500   2 .16  16 2.4  2 170   2100 1400 2 260   2500 2400 2 170   2100 1400 2 80   1300 760 2 900   160 11000 0
float-newlib/double_req_bl_0620b_true-unreach-call.c .28  50 3.9  2 .077 6.1 .32 2 .051 5.9 .34 2 11   1100 120 2 1.1  65 12   0 8.2 370 95 2 8.5 370 110 2 .17  35 2.0  2 29 2100 270 2 .37 60 4.1 2 4.6 280 41 2 80    1400 610   2 .15  15 2.0  2 210   2100 1600 2 260   2500 2600 2 190   2100 2000 2 73   1300 690 2 900   160 12000 0
float-newlib/double_req_bl_0621a_true-unreach-call.c .29  46 4.0  2 .052 6.9 .49 2 .046 6.7 .42 2 11   1200 110 2 1.1  65 14   0 8.2 370 100 2 8.4 370 95 2 .18  35 2.1  2 29 2100 250 2 .38 60 3.3 2 4.2 270 45 2 18    640 170   2 .15  16 1.8  2 900   1700 7200 0 900   3100 7500 0 900   1700 6700 0 95   1400 820 2 900   160 11000 0
float-newlib/double_req_bl_0621b_true-unreach-call.c .34  46 3.3  2 .095 6.1 .27 2 .099 6.5 .32 2 11   1100 120 2 1.1  66 11   0 8.2 370 120 2 8.1 370 100 2 .17  35 1.9  2 31 2100 290 2 .38 60 3.5 2 4.6 280 40 2 11    590 140   2 .15  15 1.7  2 900   1600 8000 0 900   5200 9000 0 900   1700 6800 0 74   1400 660 2 900   160 12000 0
float-newlib/double_req_bl_0660a_true-unreach-call.c 1.5   290 18    2 2.8   210   35    2 16     210   190    2 14   1300 130 2 1.8  74 21   0 8.1 430 100 0 8.2 430 94 0 .44  66 4.6  2 34 2200 290 2 .38 60 3.3 2 17   490 160 2 10    1000 120   2 .18  17 2.3  0 110   2300 1100 0 360   2500 4400 2 100   2300 1100 0 120   3600 1000 2 860   280 10000 0
float-newlib/double_req_bl_0660b_true-unreach-call.c 1.6   290 20    2 3.3   210   35    2 17     220   260    2 14   1300 130 2 1.7  75 20   0 8.2 430 100 0 8.4 430 120 0 .38  66 4.5  2 34 2200 310 2 .40 60 3.4 2 16   460 140 2 12    780 130   2 .19  18 2.3  0 98   2300 1100 0 320   2500 3500 2 110   2300 1100 0 120   1800 1100 2 860   290 11000 0
float-newlib/double_req_bl_0661a_true-unreach-call.c 1.5   290 16    2 3.4   220   43    2 33     210   410    2 14   1300 140 2 1.7  75 24   0 8.3 430 110 0 8.4 430 110 0 .40  66 5.2  2 33 2400 320 2 .39 60 4.4 2 17   540 140 2 150    2200 1900   2 .19  18 2.3  0 260   2300 3000 2 470   2700 4700 0 260   2300 2800 0 120   1700 1100 2 860   280 11000 0
float-newlib/double_req_bl_0661b_true-unreach-call.c 1.5   290 22    2 4.6   220   52    2 31     220   380    2 14   1300 150 2 1.7  75 24   0 8.4 430 100 0 8.2 430 92 0 .39  67 5.9  2 34 2300 390 2 .40 60 4.0 2 18   550 150 2 880    4400 6800   0 .20  18 2.4  0 250   2400 2800 0 510   2900 5200 0 270   2300 2500 2 120   3600 1100 2 860   250 12000 0
float-newlib/double_req_bl_0662a_true-unreach-call.c 2.8   430 31    2 .10  8.3 1.2  2 .10  8.3 1.4  2 13   1300 170 2 1.9  84 19   0 8.2 430 100 0 8.3 430 90 0 .45  75 4.7  2 33 2400 310 2 .39 60 3.3 2 16   470 130 2 14    740 140   2 .18  18 2.2  0 130   1700 1200 2 250   2400 1900 0 140   1600 1300 2 96   1700 870 2 900   220 13000 0
float-newlib/double_req_bl_0662b_true-unreach-call.c 2.8   430 36    2 .10  8.4 .91 2 .12  8.3 1.1  2 14   1300 140 2 1.8  84 21   0 8.2 430 100 0 8.2 430 120 0 .44  75 4.5  2 34 2200 290 2 .38 60 3.1 2 16   560 130 2 81    1900 670   2 .18  17 2.3  0 430   2800 3800 0 480   2500 4600 2 410   2800 3600 0 120   1700 930 2 900   160 11000 0
float-newlib/double_req_bl_0663a_true-unreach-call.c 2.7   430 33    2 .12  7.9 1.3  2 .11  8.4 1.3  2 14   1300 140 2 1.8  84 21   0 8.1 430 120 0 8.3 430 100 0 .44  75 5.1  2 34 2200 290 2 .38 60 3.6 2 16   460 130 2 19    1100 190   2 .20  17 2.1  0 110   1500 1200 2 480   2700 5400 2 110   1500 1100 2 110   1800 940 2 900   160 12000 0
float-newlib/double_req_bl_0663b_true-unreach-call.c 2.8   430 33    2 .11  8.2 .92 2 .11  8.5 1.1  2 13   1300 130 2 1.8  83 23   0 8.3 430 110 0 8.3 430 100 0 .43  75 4.9  2 34 2200 280 2 .39 60 3.3 2 17   540 140 2 12    1000 140   2 .18  18 2.2  0 430   2500 3900 2 530   2700 5800 2 520   2700 4600 2 100   1800 870 2 900   170 10000 0
float-newlib/double_req_bl_0670_true-unreach-call.c 3.5   410 36    2 8.1   360   86    2 98     340   1200    2 13   1400 130 2 26    560 220   0 8.2 430 110 0 8.3 430 94 0 8.2   550 110    2 33 2400 310 2 .40 60 3.6 2 45   2100 420 0 11    600 130   2 .18  17 2.3  0 170   1600 1800 2 320   2500 2700 2 130   1500 1300 2 130   4100 1200 2 860   540 11000 0
float-newlib/double_req_bl_0680a_true-unreach-call.c .56  99 7.2  2 .085 6.3 .37 2 .060 6.7 .49 2 14   1300 140 2 1.6  70 17   0 8.1 370 110 2 8.2 370 94 2 .33  62 3.7  2 33 2200 340 2 .38 60 3.4 2 5.7 310 51 2 2.9  97 34   2 .19  16 1.9  2 100   1500 1200 2 320   2700 3600 2 100   1500 1100 2 100   1800 860 2 900   170 13000 0
float-newlib/double_req_bl_0680b_true-unreach-call.c .53  98 6.8  2 .071 6.9 .40 2 .088 6.2 .44 2 14   1300 160 2 1.6  70 18   0 8.1 370 110 2 8.3 370 100 2 .34  61 3.9  2 34 2200 300 2 .38 60 4.2 2 5.7 310 56 2 3.0  100 37   2 .16  15 1.8  2 85   1400 810 2 340   2500 3100 2 83   1500 930 2 110   1700 1100 2 900   160 11000 0
float-newlib/double_req_bl_0681a_true-unreach-call.c .51  99 8.4  2 .068 6.4 .51 2 .11  6.2 .38 2 14   1300 150 2 1.6  70 16   0 8.1 370 98 2 8.3 370 96 2 .34  61 3.7  2 34 2200 320 2 .38 60 3.5 2 5.7 310 56 2 12    790 130   2 .16  16 1.9  2 84   1500 810 2 300   2600 2800 2 89   1500 850 2 100   1700 870 2 900   170 12000 0
float-newlib/double_req_bl_0681b_true-unreach-call.c .54  99 7.1  2 .064 6.7 .59 2 .065 6.7 .46 2 14   1300 170 2 1.6  70 17   0 8.0 370 110 2 8.1 370 100 2 .37  61 4.2  2 34 2200 300 2 .43 60 3.5 2 5.6 380 54 2 4.4  140 56   2 .16  15 1.9  2 78   1500 980 2 320   2500 2900 2 72   1500 770 2 100   1700 870 2 900   160 11000 0
float-newlib/double_req_bl_0682a_true-unreach-call.c 2.3   380 25    2 2.5   200   30    2 28     200   360    2 14   1200 150 2 2.2  110 24   0 8.1 430 93 0 8.5 430 110 0 .58  97 5.9  2 34 2200 380 2 .43 60 3.5 2 17   480 130 2 20    1700 250   2 .20  17 2.0  0 130   1500 1200 2 450   2800 4000 0 130   1600 1400 2 97   1600 800 2 870   210 11000 0
float-newlib/double_req_bl_0682b_true-unreach-call.c 2.2   380 24    2 2.4   200   34    2 29     200   450    2 14   1200 150 2 2.2  110 26   0 8.2 430 100 0 8.3 430 90 0 .57  97 7.7  2 35 2200 340 2 .42 60 3.2 2 17   550 160 2 5.2  420 77   2 .18  18 2.4  0 110   1500 1100 2 670   2700 7700 0 120   1500 1200 2 99   1600 850 2 860   210 10000 0
float-newlib/double_req_bl_0683a_true-unreach-call.c 2.2   380 27    2 2.5   200   30    2 57     200   660    2 14   1300 160 2 2.3  110 24   0 8.2 430 110 0 8.4 430 99 0 .56  98 8.0  2 34 2200 340 2 .41 60 3.4 2 19   580 160 2 6.6  690 79   2 .19  18 2.3  0 130   2300 1300 0 320   2700 2800 0 140   2400 1700 0 110   1700 990 2 870   210 13000 0
float-newlib/double_req_bl_0683b_true-unreach-call.c 2.2   380 24    2 2.5   200   32    2 56     200   810    2 14   1300 140 2 2.4  110 27   0 8.2 430 91 0 8.5 430 100 0 .59  98 5.5  2 46 2300 550 2 .41 60 4.7 2 19   590 160 2 40    1400 340   2 .18  18 2.3  0 130   2400 1600 0 580   2700 6300 0 130   2300 1600 2 100   1700 1000 2 870   210 10000 0
float-newlib/double_req_bl_0684a_true-unreach-call.c 1.9   270 20    2 .13  8.9 1.4  2 .14  9.5 1.2  2 13   1200 130 2 1.7  78 18   0 8.1 430 110 0 8.3 430 120 0 .41  70 4.8  2 33 2200 330 2 .42 60 3.1 2 15   410 130 2 200    2700 1800   2 .22  18 3.6  2 900   2000 8900 0 250   2400 2200 0 900   2400 7800 0 100   1700 860 2 900   170 12000 0
float-newlib/double_req_bl_0684b_true-unreach-call.c 1.8   270 24    2 .13  9.1 1.4  2 .12  9.5 1.4  2 13   1200 160 2 1.7  78 19   0 8.1 430 120 0 8.3 430 110 0 .42  69 4.7  2 33 2200 310 2 .40 60 3.5 2 16   410 140 2 290    2500 2700   2 .22  17 2.7  2 620   2400 6200 0 750   2700 7600 0 900   2000 8600 0 98   1700 900 2 900   160 12000 0
float-newlib/double_req_bl_0685a_true-unreach-call.c .57  96 6.2  2 .059 6.9 .61 2 .053 7.2 .53 2 14   1300 160 2 1.6  70 18   0 8.1 370 100 2 8.4 370 120 2 .33  62 4.2  2 34 2200 310 2 .38 60 3.8 2 5.8 310 47 2 3.0  110 43   2 .18  15 2.0  2 160   2100 1700 2 410   2700 3700 0 130   1700 1300 2 100   1800 880 2 900   170 11000 0
float-newlib/double_req_bl_0685b_true-unreach-call.c .52  94 6.1  2 .071 6.8 .43 2 .055 7.3 .49 2 13   1300 150 2 1.6  70 18   0 8.1 370 100 2 8.2 370 110 2 .36  61 3.7  2 34 2200 360 2 .40 60 3.7 2 5.8 310 56 2 5.8  800 64   2 .16  15 2.0  2 180   2000 2000 2 500   2700 4900 2 170   2000 1800 2 100   1800 910 2 900   170 13000 0
float-newlib/double_req_bl_0686a_true-unreach-call.c .54  94 6.2  2 .080 6.3 .51 2 .056 7.1 .40 2 13   1300 150 2 1.6  70 17   0 8.1 370 110 2 8.3 370 120 2 .33  62 4.0  2 32 2400 300 2 .38 60 3.8 2 5.6 310 50 2 3.0  110 36   2 .17  16 2.0  2 160   2000 2100 2 390   2800 3700 2 160   2100 2300 2 100   1800 900 2 900   170 9700 0
float-newlib/double_req_bl_0686b_true-unreach-call.c .58  96 6.6  2 .060 6.4 .48 2 .057 6.6 .45 2 14   1300 150 2 1.6  70 18   0 8.0 370 110 2 8.1 370 120 2 .33  62 3.8  2 34 2200 330 2 .37 60 4.2 2 5.5 310 50 2 3.1  120 40   2 .16  15 2.1  2 150   2100 1800 2 380   2700 4000 2 150   2100 1800 2 97   1800 990 2 900   160 10000 0
float-newlib/double_req_bl_0720_true-unreach-call.c .17  24 1.7  2 .054 6.3 .51 2 .048 6.3 .46 2 900   3400 13000 0 .86 67 11   0 8.0 370 100 2 8.0 370 97 2 .11  27 1.0  2 100 1900 1100 2 .38 60 3.1 2 4.3 280 43 2 360    800 3000   2 .16  15 2.7  2 86   1000 850 2 45   780 470 2 140   1400 1600 2 140   1400 1200 2 900   160 11000 0
float-newlib/double_req_bl_0730a_true-unreach-call.c .17  25 2.0  2 .064 6.4 .42 2 .048 7.4 .43 2 13   530 100 2 .86 66 9.5 0 8.0 370 100 2 8.2 370 110 2 .10  27 1.1  2 22 1400 140 2 .39 60 3.5 2 4.6 280 43 2 400    930 3700   2 .16  15 2.1  2 66   850 630 2 45   820 420 2 82   860 680 2 140   1500 1200 2 900   160 11000 0
float-newlib/double_req_bl_0730b_true-unreach-call.c .18  24 1.7  2 .055 6.7 .45 2 .054 6.7 .46 2 14   650 100 2 .88 67 11   0 8.0 370 98 2 8.1 370 100 2 .10  27 1.0  2 22 1400 150 2 .36 60 4.2 2 4.3 280 41 2 360    670 4200   2 .16  16 2.0  2 29   860 320 2 44   950 420 2 29   860 310 2 140   1500 1300 2 900   160 12000 0
float-newlib/double_req_bl_0730c_true-unreach-call.c .20  25 1.6  2 .090 6.2 .47 2 .058 6.3 .43 2 12   620 87 2 .86 66 10   0 8.1 370 110 2 8.3 370 100 2 .093 27 .96 2 22 1400 180 2 .37 60 4.1 2 4.7 280 43 2 390    990 3900   2 .16  15 2.0  2 35   900 390 2 120   1200 1300 2 35   940 310 2 69   910 640 2 900   160 12000 0
float-newlib/double_req_bl_0740_true-unreach-call.c .17  25 2.1  2 .068 6.8 .31 2 .050 6.5 .34 2 11   620 94 2 .86 67 9.1 0 8.1 370 110 2 8.1 370 110 2 .096 27 1.0  2 21 1400 170 2 .36 60 4.1 2 4.9 280 44 2 330    320 4700   2 .17  15 1.9  2 54   770 490 2 36   780 380 2 61   780 580 2 140   1400 1200 2 900   160 11000 0
float-newlib/double_req_bl_0832_true-unreach-call.c .86  140 9.1  2 2.0   120   24    2 5.4   120   66    2 9.5 890 93 2 1.6  66 17   0 8.2 430 130 0 8.3 430 100 0 .35  56 4.4  2 29 1900 300 2 .38 60 4.2 2 130   2300 1000 2 100    2400 980   2 .19  18 1.8  0 130   1600 1300 2 250   1900 2600 2 130   1700 1100 2 63   1000 580 2 860   170 11000 0
float-newlib/double_req_bl_0833_true-unreach-call.c .26  43 2.8  2 .056 6.2 .47 2 .065 6.7 .35 2 9.0 830 90 2 .99 67 11   0 8.1 370 100 2 8.3 370 120 2 .14  30 1.7  2 27 1800 250 2 .37 59 3.9 2 4.4 270 39 2 130    1900 1300   2 .15  16 1.9  2 130   1700 1200 2 160   1200 1200 2 120   1700 1200 2 64   1000 660 2 900   160 13000 0
float-newlib/double_req_bl_0834_true-unreach-call.c .28  43 3.1  2 .069 6.6 .35 2 .10  5.9 .33 2 9.3 820 94 2 .85 68 9.5 0 8.4 370 110 2 8.4 370 100 2 .10  27 1.2  2 24 1800 190 2 .36 59 4.0 2 4.4 280 38 2 75    1800 790   2 .15  15 1.6  2 110   1500 840 2 120   1000 990 2 110   1500 830 2 71   1000 680 2 900   160 11000 0
float-newlib/double_req_bl_0870b_true-unreach-call.c .67  100 7.7  2 .12  8.5 1.2  2 .12  10   1.1  2 75   4100 760 2 2.4  97 24   0 8.3 430 94 0 8.4 430 97 0 .89  110 8.6  2 89 4000 820 2 .74 64 8.8 2 19   560 150 2 590    4000 6300   2 .25  17 2.8  0 300   3000 2600 2 500   2400 4300 2 200   2100 1800 2 150   3200 1200 2 900   170 12000 0
float-newlib/double_req_bl_0872a_true-unreach-call.c 3.0   540 34    2 .14  8.0 .98 2 .094 10   .91 2 73   3900 640 2 2.5  110 26   0 8.1 370 120 2 8.4 430 94 0 .91  120 9.7  2 84 4000 750 2 .76 64 6.5 2 7.3 480 60 2 340    330 5000   2 .23  16 2.8  2 270   3000 2500 2 410   2200 2800 2 280   3000 2600 2 140   3100 1400 2 900   170 11000 0
float-newlib/double_req_bl_0872b_true-unreach-call.c 3.0   540 37    2 .094 8.4 .91 2 .10  11   .97 2 75   4000 590 2 2.6  110 29   0 8.2 370 120 2 8.3 430 110 0 .97  120 8.8  2 87 3900 830 2 .73 64 7.7 2 7.4 480 67 2 380    330 3200   2 .23  15 3.1  2 290   2900 3000 2 400   2000 3200 2 270   2900 2600 2 150   3200 1300 2 900   180 11000 0
float-newlib/double_req_bl_0873a_true-unreach-call.c .63  96 7.3  2 .094 9.6 .94 2 .14  10   .88 2 73   3800 650 2 2.1  87 22   0 8.1 370 91 2 8.2 370 120 2 .72  98 9.4  2 85 3900 710 2 .77 64 6.5 2 7.7 490 62 2 330    320 3700   2 .24  15 2.6  2 260   2300 2200 2 420   2200 3400 2 240   2300 2000 2 150   3200 1300 2 900   170 12000 0
float-newlib/double_req_bl_0873b_true-unreach-call.c .61  96 6.6  2 .093 8.9 .98 2 .10  11   1.0  2 78   3900 700 2 2.1  87 24   0 8.2 370 110 2 8.4 370 100 2 .74  98 8.8  2 86 3900 660 2 .77 64 6.2 2 7.4 480 70 2 330    350 3600   2 .24  15 2.6  2 250   2300 2200 2 440   2100 3500 2 250   2300 2300 2 150   3200 1300 2 900   170 12000 0
float-newlib/double_req_bl_0874_true-unreach-call.c 2.3   400 26    2 .20  11   2.0  2 .17  13   2.0  2 72   4000 600 2 3.0  140 40   0 8.2 430 99 0 8.3 430 89 0 1.0   130 11    2 95 4900 870 2 .82 65 8.0 2 21   690 170 2 820    6800 8400   2 .30  17 3.3  0 220   2300 1900 2 340   2100 3500 0 220   2200 1800 2 150   3100 1200 2 900   170 11000 0
float-newlib/double_req_bl_0876_true-unreach-call.c 2.3   400 25    2 .17  12   2.0  2 .16  13   1.8  2 71   3700 640 2 2.7  110 27   0 8.2 430 100 0 8.4 430 110 0 .92  110 13    2 86 4000 720 2 .79 65 6.3 2 19   570 150 2 670    4300 6100   2 .28  18 3.6  0 220   2200 2400 2 730   2700 7500 0 250   2300 2500 2 150   3100 1200 2 900   170 11000 0
float-newlib/double_req_bl_0882_true-unreach-call.c .77  120 10    2 .22  14   2.7  2 .20  17   2.4  2 74   4000 680 2 2.4  97 34   0 8.3 430 100 0 8.2 430 130 0 .95  110 10    2 89 4000 890 2 .91 100 8.9 2 23   880 200 2 690    5100 6200   2 .26  17 2.8  0 310   2700 2600 0 900   2800 9000 0 380   2800 3000 0 150   3100 1500 2 900   180 10000 0
float-newlib/double_req_bl_0883_true-unreach-call.c .78  120 8.0  2 .18  15   2.6  2 .19  17   2.5  2 75   3900 690 2 2.5  97 27   0 8.2 430 110 0 8.4 430 130 0 .87  110 11    2 90 3900 810 2 .79 68 7.5 2 23   750 230 2 880    7400 9200   0 .25  18 3.2  0 900   2700 7800 0 900   2800 9200 0 570   2500 4700 2 140   3100 1300 2 900   180 10000 0
float-newlib/double_req_bl_0910a_true-unreach-call.c .27  38 2.8  2 .067 6.7 .43 2 .055 6.7 .35 2 11   1100 110 2 1.0  67 11   0 8.2 370 120 2 8.2 370 100 2 .16  34 1.8  2 27 2100 230 2 .38 59 3.7 2 4.7 280 41 2 2.7  88 35   2 .15  15 1.8  2 210   2000 1800 2 390   2600 3400 0 210   2000 1900 2 70   1300 630 2 900   160 11000 0
float-newlib/double_req_bl_0910b_true-unreach-call.c .25  39 3.0  2 .061 6.7 .44 2 .067 5.8 .34 2 12   1100 120 2 1.0  67 11   0 8.1 370 100 2 8.3 370 120 2 .16  34 2.0  2 26 2200 210 2 .38 60 3.1 2 4.7 280 42 2 2.8  88 33   2 .18  15 1.8  2 76   1600 660 2 340   2400 2600 0 87   1600 860 2 70   1300 720 2 900   160 12000 0
float-newlib/double_req_bl_0920a_true-unreach-call.c 1.4   220 20    2 2.8   200   34    2 3.7   200   54    2 12   1100 130 2 26    410 330   0 8.4 430 100 0 8.2 430 110 0 8.6   400 98    2 26 2100 200 2 .41 59 3.7 2 200   2700 2300 2 120    1800 910   2 .17  18 2.0  0 94   1600 820 2 340   2600 3100 0 99   1600 1000 2 87   1600 800 2 860   270 11000 0
float-newlib/double_req_bl_0920b_true-unreach-call.c .28  40 3.2  2 .058 6.2 .52 2 .060 6.2 .31 2 12   1100 130 2 1.0  67 12   0 8.2 370 130 2 8.2 370 100 2 .16  34 2.1  2 27 2100 220 2 .41 60 3.0 2 4.8 280 45 2 2.8  94 38   2 .17  15 1.8  2 75   1500 670 2 430   2400 3100 2 77   1500 750 2 69   1300 640 2 900   160 10000 0
float-newlib/double_req_bl_0921_true-unreach-call.c .27  40 4.2  2 .068 6.5 .49 2 .051 6.3 .46 2 12   1100 120 2 1.1  67 12   0 8.2 370 98 2 8.2 370 110 2 .21  33 1.7  2 26 2200 220 2 .36 60 3.5 2 4.7 280 40 2 8.3  820 110   2 .16  15 1.8  2 100   1900 930 2 400   2500 2900 2 100   1900 1000 2 68   1300 660 2 900   160 11000 0
float-newlib/double_req_bl_0930_true-unreach-call.c .25  39 2.7  2 .072 7.0 .51 2 .097 5.9 .36 2 11   1100 150 2 1.0  67 12   0 8.1 370 98 2 8.4 370 120 2 .16  34 2.0  2 26 2200 220 2 .42 60 3.5 2 4.4 280 39 2 220    1400 1700   2 .20  15 1.6  2 98   1700 900 2 340   2500 2800 0 100   1700 1000 2 89   1300 770 2 900   160 11000 0
float-newlib/double_req_bl_0931_true-unreach-call.c .28  40 2.9  2 .072 6.4 .33 2 .047 7.0 .54 2 12   1100 140 2 1.0  66 11   0 8.0 370 100 2 8.2 370 89 2 .16  34 2.2  2 27 2200 220 2 .36 60 3.9 2 4.6 280 42 2 36    940 330   2 .15  15 1.8  2 81   1700 680 2 360   2400 2800 2 83   1800 800 2 70   1300 690 2 900   160 12000 0
float-newlib/double_req_bl_0960b_true-unreach-call.c .31  42 2.9  2 .059 6.8 .55 2 .049 7.0 .54 2 14   1300 150 2 1.1  66 14   0 8.1 370 100 2 8.3 370 89 2 .21  42 2.5  2 31 2300 310 2 .40 60 3.8 2 5.3 310 45 2 2.8  100 32   2 .16  15 2.0  2 68   1400 720 2 400   2500 2400 2 70   1500 610 2 76   1600 770 2 900   160 12000 0
float-newlib/double_req_bl_0970a_true-unreach-call.c 1.5   250 19    2 3.5   220   38    2 7.0   220   96    2 14   1300 150 2 61    470 730   0 8.2 430 96 0 8.3 430 110 0 20     460 230    2 30 2400 260 2 .42 60 4.7 2 230   3100 1900 2 13    800 120   2 .21  17 2.0  0 76   1400 640 2 410   2600 3300 0 77   1400 610 2 92   2400 820 2 860   300 12000 0
float-newlib/double_req_bl_0970b_true-unreach-call.c .29  44 3.1  2 .062 6.3 .42 2 .058 6.5 .41 2 14   1300 150 2 1.2  66 12   0 8.2 370 130 2 8.3 370 95 2 .20  42 3.0  2 30 2300 300 2 .37 60 3.6 2 5.3 310 54 2 5.6  190 63   2 .16  15 2.1  2 77   1400 730 2 430   2500 3000 2 67   1400 590 2 74   1700 650 2 900   160 13000 0
float-newlib/double_req_bl_0971_true-unreach-call.c .31  43 4.6  2 .058 6.5 .45 2 .052 7.3 .42 2 14   1300 120 2 1.2  67 13   0 8.4 370 95 2 8.2 370 100 2 .20  42 2.5  2 30 2300 230 2 .39 60 3.4 2 5.4 310 54 2 8.1  440 90   2 .17  15 1.7  2 77   1500 660 2 420   2500 3900 0 77   1500 680 2 73   1500 620 2 900   160 11000 0
float-newlib/double_req_bl_0981_true-unreach-call.c .31  43 3.7  2 .064 6.2 .40 2 .049 6.6 .60 2 14   1300 140 2 1.1  67 13   0 8.0 370 100 2 8.3 370 110 2 .20  42 2.6  2 33 2300 270 2 .37 60 4.5 2 4.9 310 50 2 4.7  170 63   2 .17  15 2.1  2 60   1400 710 2 400   2400 3200 2 63   1400 620 2 74   1500 790 2 900   160 10000 0
float-newlib/double_req_bl_1011a_true-unreach-call.c .099 24 .85 2 .053 8.0 .39 2 .057 6.2 .21 2 3.0 250 28 2 .81 66 8.4 0 7.9 370 100 2 8.2 370 95 2 .091 26 1.1  2 14 1200 97 2 .36 59 3.7 2 4.0 210 39 2 2.6  74 34   2 .14  17 1.5  2 17   400 150 2 16   350 120 2 18   400 150 2 54   580 560 2 900   150 13000 0
float-newlib/double_req_bl_1011b_true-unreach-call.c .10  24 .82 2 .067 6.4 .31 2 .047 6.2 .30 2 3.0 250 28 2 .81 67 8.5 0 8.1 370 97 2 8.1 370 99 2 .089 26 1.0  2 15 1200 100 2 .39 59 3.1 2 3.6 210 34 2 2.6  75 32   2 .14  16 1.6  2 19   390 150 2 17   370 150 0 18   410 160 2 54   620 530 2 900   150 12000 0
float-newlib/double_req_bl_1012a_true-unreach-call.c .12  24 1.1  2 .052 6.8 .36 2 .096 6.5 .28 2 2.9 260 31 2 .81 67 8.6 0 8.2 370 96 2 8.0 370 110 2 .087 26 .98 2 15 1200 96 2 .38 59 3.6 2 4.1 230 41 2 2.6  76 35   2 .14  15 1.6  2 19   410 190 2 16   360 130 2 19   430 160 2 55   580 590 2 900   160 10000 0
float-newlib/double_req_bl_1012b_true-unreach-call.c .18  24 1.0  2 .048 7.9 .41 2 .083 6.3 .23 2 3.0 260 32 2 .80 66 8.0 0 8.0 370 93 2 8.1 370 90 2 .087 26 1.0  2 14 1200 99 2 .37 59 3.1 2 3.7 230 37 2 2.6  76 33   2 .14  17 1.6  2 19   420 170 2 17   370 150 0 20   430 160 2 56   600 640 2 900   150 13000 0
float-newlib/double_req_bl_1031_true-unreach-call.c .12  24 1.1  2 .052 6.7 .46 2 .044 6.6 .49 2 3.1 270 27 2 .81 66 9.4 0 8.1 370 100 2 8.0 370 100 2 .089 26 .99 2 16 1200 110 2 .37 59 3.2 2 4.0 250 41 2 2.6  76 30   2 .15  15 1.8  2 22   450 210 2 19   390 150 2 20   450 220 2 38   510 420 2 900   150 13000 0
float-newlib/double_req_bl_1032a_true-unreach-call.c .099 24 .90 2 .095 6.0 .38 2 .053 6.6 .47 2 3.2 270 31 2 .84 66 10   0 8.0 370 94 2 8.3 370 100 2 .087 26 1.2  2 12 1200 100 2 .37 59 3.3 2 4.3 270 41 2 2.8  79 33   2 .14  15 1.8  2 21   490 220 2 19   500 160 2 22   470 200 2 40   620 380 2 900   150 11000 0
float-newlib/double_req_bl_1032b_true-unreach-call.c .13  24 .76 2 .084 6.8 .36 2 .075 6.1 .36 2 3.2 270 28 2 .81 66 8.9 0 8.2 370 120 2 8.2 370 110 2 .089 26 .98 2 16 1200 100 2 .37 59 3.3 2 4.3 270 41 2 2.7  76 33   2 .16  16 1.9  2 20   470 210 2 18   510 160 2 21   470 200 2 40   630 350 2 900   150 13000 0
float-newlib/double_req_bl_1032c_true-unreach-call.c .13  25 1.2  2 .060 6.7 .39 2 .051 6.2 .29 2 3.2 270 30 2 .82 67 8.4 0 8.2 370 120 2 7.9 370 95 2 .088 26 1.1  2 14 1200 110 2 .37 59 3.7 2 4.3 270 42 2 2.7  76 33   2 .15  15 1.8  2 23   450 220 2 17   380 160 2 24   450 220 2 48   500 590 2 900   160 11000 0
float-newlib/double_req_bl_1032d_true-unreach-call.c .13  24 1.1  2 .060 6.7 .43 2 .050 6.2 .32 2 3.2 270 34 2 .82 65 9.4 0 8.1 370 95 2 8.0 370 91 2 .093 27 .95 2 15 1200 100 2 .37 59 3.4 2 3.9 270 38 2 2.7  76 34   2 .15  16 1.9  2 24   450 230 2 18   400 140 2 23   450 220 2 44   520 430 2 900   150 10000 0
float-newlib/double_req_bl_1051_true-unreach-call.c .13  24 1.1  2 .095 6.5 .27 2 .055 6.5 .25 2 3.3 280 28 2 .80 66 9.3 0 8.2 370 110 2 8.0 370 110 2 .082 27 1.1  2 14 1200 110 2 .37 59 3.4 2 4.4 280 43 2 2.7  77 32   2 .15  16 1.7  2 26   490 260 2 24   400 240 2 27   490 260 2 45   590 460 2 900   150 11000 0
float-newlib/double_req_bl_1052a_true-unreach-call.c .13  24 1.3  2 .053 7.1 .62 2 .051 6.6 .30 2 3.4 280 30 2 .82 66 10   0 8.1 370 100 2 8.2 370 100 2 .090 26 .95 2 13 1300 97 2 .40 59 3.2 2 4.5 270 41 2 2.7  79 39   2 .17  16 2.0  2 26   520 240 2 21   400 180 2 26   510 270 2 60   510 650 2 900   160 11000 0
float-newlib/double_req_bl_1052b_true-unreach-call.c .12  25 1.2  2 .10  6.5 .30 2 .046 7.4 .38 2 3.3 270 35 2 .79 65 8.8 0 8.0 370 91 2 8.0 370 92 2 .088 27 .94 2 13 1300 93 2 .36 59 3.4 2 5.1 270 42 2 2.7  78 31   2 .15  15 1.7  2 25   510 260 2 21   400 190 2 26   510 250 2 59   450 620 2 900   160 10000 0
float-newlib/double_req_bl_1052c_true-unreach-call.c .11  25 .93 2 .10  6.1 .39 2 .058 6.3 .44 2 3.3 280 27 2 .87 66 11   0 8.0 370 99 2 8.1 370 100 2 .094 26 1.0  2 13 1200 110 2 .38 59 3.4 2 4.5 280 40 2 2.8  78 36   2 .15  15 1.8  2 55   580 670 2 24   550 240 2 37   570 360 2 61   650 640 2 900   200 11000 0
float-newlib/double_req_bl_1052d_true-unreach-call.c .14  24 .96 2 .062 6.6 .42 2 .060 6.3 .45 2 3.5 280 33 2 .82 67 8.5 0 8.1 370 95 2 8.1 370 130 2 .094 27 .97 2 14 1200 96 2 .38 59 3.4 2 4.2 270 42 2 2.7  79 33   2 .15  16 1.9  2 26   510 270 2 26   550 250 2 26   510 250 2 60   640 640 2 900   150 12000 0
float-newlib/double_req_bl_1071_true-unreach-call.c .15  24 .94 2 .054 7.2 .41 2 .055 6.6 .26 2 3.1 270 30 2 .81 65 9.0 0 8.1 370 110 2 8.0 370 97 2 .094 26 1.5  2 16 1200 100 2 .36 60 3.3 2 4.1 240 39 2 2.7  79 32   2 .15  15 2.1  2 21   470 200 2 18   350 160 2 21   480 190 2 36   520 350 2 900   150 11000 0
float-newlib/double_req_bl_1072a_true-unreach-call.c .13  24 1.1  2 .051 7.0 .40 2 .052 6.5 .29 2 3.1 270 33 2 .84 65 9.9 0 8.2 370 110 2 8.2 370 100 2 .11  27 .97 2 12 1200 95 2 .37 59 3.2 2 3.9 260 36 2 2.7  75 31   2 .18  16 1.7  2 22   450 220 2 18   400 160 2 22   450 240 2 44   530 450 2 900   160 11000 0
float-newlib/double_req_bl_1072b_true-unreach-call.c .11  24 .86 2 .065 6.6 .37 2 .10  6.6 .35 2 3.3 280 29 2 .81 66 9.7 0 8.2 370 93 2 8.0 370 94 2 .086 26 1.1  2 13 1200 110 2 .38 59 3.3 2 3.9 240 46 2 2.7  79 32   2 .14  16 1.7  2 21   500 220 2 20   490 180 2 21   490 190 2 38   640 370 2 900   150 11000 0
float-newlib/double_req_bl_1072c_true-unreach-call.c .10  24 1.0  2 .072 6.5 .33 2 .061 7.0 .44 2 3.3 270 35 2 .82 66 9.7 0 8.1 370 120 2 7.9 370 99 2 .090 26 1.2  2 16 1200 100 2 .37 59 3.3 2 4.2 240 40 2 2.7  76 39   2 .14  16 1.5  2 19   490 180 2 20   500 180 2 21   480 160 2 37   640 370 2 900   150 14000 0
float-newlib/double_req_bl_1072d_true-unreach-call.c .13  24 1.3  2 .060 6.3 .41 2 .046 6.7 .39 2 3.3 280 30 2 .83 68 8.7 0 8.0 370 110 2 8.2 370 98 2 .089 26 1.3  2 13 1200 97 2 .35 59 3.6 2 4.3 260 43 2 2.7  78 36   2 .15  16 1.7  2 22   460 210 2 18   400 150 2 22   450 210 2 45   490 460 2 900   160 11000 0
float-newlib/double_req_bl_1091_true-unreach-call.c .14  24 1.2  2 .054 6.7 .42 2 .053 6.3 .38 2 3.2 270 33 2 .82 67 9.7 0 8.0 370 100 2 8.2 370 100 2 .096 26 1.3  2 12 1200 100 2 .40 59 2.9 2 4.6 280 46 2 2.7  77 32   2 .15  16 1.8  2 26   490 260 2 22   350 210 2 26   490 290 2 51   540 490 2 900   150 11000 0
float-newlib/double_req_bl_1092a_true-unreach-call.c .11  24 1.1  2 .060 7.2 .42 2 .060 6.3 .36 2 3.4 270 35 2 .83 66 9.0 0 8.1 370 89 2 8.0 370 92 2 .089 27 1.2  2 17 1200 130 2 .35 59 3.5 2 4.1 270 38 2 2.7  78 33   2 .15  15 1.7  2 27   460 290 2 27   530 290 2 25   460 290 2 59   630 580 2 900   160 11000 0
float-newlib/double_req_bl_1092b_true-unreach-call.c .11  24 .99 2 .053 6.6 .50 2 .062 6.8 .42 2 3.3 270 33 2 .82 67 9.7 0 8.1 370 93 2 8.3 370 100 2 .092 26 1.1  2 12 1200 100 2 .38 59 3.7 2 4.4 270 38 2 2.7  77 37   2 .15  15 1.6  2 27   510 280 2 27   540 280 2 27   520 280 2 61   640 580 2 900   150 10000 0
float-newlib/double_req_bl_1092c_true-unreach-call.c .12  25 1.4  2 .056 6.6 .45 2 .049 6.4 .37 2 3.3 270 35 2 .83 66 8.9 0 8.2 370 100 2 8.1 370 92 2 .093 26 1.1  2 13 1400 98 2 .37 59 3.1 2 4.5 270 50 2 2.7  79 37   2 .16  15 1.5  2 26   500 270 2 22   430 210 2 26   500 250 2 52   630 530 2 900   160 11000 0
float-newlib/double_req_bl_1092d_true-unreach-call.c .12  25 1.5  2 .050 6.8 .48 2 .050 6.4 .40 2 3.3 270 30 2 .83 67 9.2 0 8.1 370 110 2 8.1 370 110 2 .091 26 .93 2 14 1200 120 2 .36 60 3.9 2 4.4 270 41 2 2.8  78 36   2 .15  15 1.7  2 26   500 270 2 21   420 200 2 26   510 250 2 60   620 620 2 900   200 13000 0
float-newlib/double_req_bl_1121a_true-unreach-call.c .27  25 2.9  2 .12  8.4 1.6  2 .12  9.3 1.2  2 21   1200 180 2 .99 66 11   0 8.0 430 110 0 8.7 430 110 0 .11  27 1.6  2 32 1800 270 2 .38 60 3.7 2 7.0 350 62 -16 6.4  390 83   2 .22  17 2.1  0 61   1300 660 2 210   2000 1800 2 180   1400 1900 2 79   1200 660 2 900   160 9900 0
float-newlib/double_req_bl_1121b_true-unreach-call.c .27  25 2.9  2 .12  8.6 1.2  2 .12  8.9 1.4  2 23   1000 170 2 .97 66 12   0 8.2 430 110 0 8.3 430 98 0 .14  27 1.2  2 33 1500 220 2 .39 60 3.2 2 7.1 350 58 -16 7.6  390 93   2 .19  18 2.1  0 99   1400 1000 2 230   2000 2100 2 100   1400 930 2 80   1200 640 2 900   160 12000 0
float-newlib/double_req_bl_1122a_true-unreach-call.c .27  25 2.9  2 .092 7.4 .65 2 .095 7.5 .61 2 14   700 120 2 1.0  66 12   0 8.2 430 93 0 8.2 430 100 0 .13  27 1.4  2 25 1400 180 2 .38 60 3.2 2 18   1300 160 2 14    660 180   2 .20  17 2.2  0 90   1400 940 2 190   2000 1500 2 93   1400 780 2 73   1400 630 2 900   160 12000 0
float-newlib/double_req_bl_1122b_true-unreach-call.c .27  25 3.2  2 .083 7.3 .69 2 .085 7.3 .62 2 17   820 130 2 1.0  67 12   0 8.3 430 110 0 8.3 430 100 0 .12  27 1.3  2 23 1600 170 2 .37 60 3.9 2 18   1200 140 2 12    570 150   2 .19  17 2.4  0 97   1400 920 2 220   2000 2300 2 47   1100 400 2 74   1200 610 2 900   160 10000 0
float-newlib/double_req_bl_1130a_true-unreach-call.c .28  25 2.9  2 .37  21   5.4  2 140     970   1800    2 16   700 120 2 1.0  67 11   0 8.3 430 110 0 8.4 430 100 0 .16  27 1.2  2 23 1600 160 2 .38 60 3.7 2 29   1300 300 2 46    810 590   2 .19  17 2.5  0 47   880 500 2 460   2000 6300 2 59   960 660 2 100   930 970 2 860   160 12000 0
float-newlib/double_req_bl_1131a_true-unreach-call.c .31  25 3.1  2 .30  18   3.7  2 5.8   120   87    2 16   700 110 2 1.7  67 18   0 8.3 430 100 0 8.4 430 120 0 .21  27 2.3  2 28 1700 200 2 .36 60 4.1 2 13   340 130 2 15    600 170   2 .24  18 2.5  0 44   920 400 2 190   1200 2100 2 46   910 440 2 100   960 1000 2 900   160 9800 0
float-newlib/double_req_bl_1131b_true-unreach-call.c .28  25 3.0  2 .31  18   3.9  2 5.8   120   91    2 17   590 140 2 1.6  67 19   0 8.1 430 120 0 8.4 430 100 0 .17  27 2.4  2 25 1700 170 2 .41 60 3.5 2 14   370 120 2 28    790 350   2 .22  18 2.8  0 37   890 340 2 160   1200 1700 2 45   930 410 2 100   970 1200 2 900   170 13000 0
float-newlib/double_req_bl_1211a_true-unreach-call.c .13  25 1.2  2 .062 6.0 .55 2 .11  6.5 .35 2 3.8 320 37 2 .86 65 9.4 0 8.1 370 110 2 8.3 430 99 0 .11  27 1.2  2 16 1200 130 2 .37 60 3.2 2 4.5 270 43 2 3.6  95 53   2 .17  15 1.8  2 33   580 320 2 36   580 330 0 33   600 310 2 53   760 490 2 900   160 14000 0
float-newlib/double_req_bl_1211b_true-unreach-call.c .13  24 1.4  2 .062 6.5 .43 2 .070 6.2 .49 2 3.7 320 37 2 .88 67 9.1 0 8.2 370 120 2 8.4 430 100 0 .11  27 1.2  2 15 1400 100 2 .40 59 3.3 2 4.2 270 39 2 3.2  90 45   2 .16  16 1.8  2 33   580 290 2 35   580 300 0 32   580 290 2 55   760 490 2 900   160 11000 0
float-newlib/double_req_bl_1230_true-unreach-call.c .13  24 1.2  2 .072 6.6 .30 2 .11  5.9 .30 2 3.2 260 29 2 .82 65 8.2 0 8.1 370 110 2 8.2 370 93 2 .11  26 .76 2 13 1100 92 2 .37 59 3.2 2 4.1 270 36 2 2.7  76 37   2 .16  20 1.7  2 20   480 170 2 26   630 260 2 20   480 150 2 32   520 280 2 900   150 9900 0
float-newlib/double_req_bl_1231b_true-unreach-call.c .13  24 1.7  2 .063 6.9 .65 2 .086 6.8 .74 2 3.3 270 35 2 11    15000 130   0 8.1 430 120 0 8.2 430 110 0 11     15000 150    0 27 1300 250 2 .40 59 3.4 2 12   350 110 2 2.8  74 30   2 .16  17 1.9  0 33   600 330 2 31   670 290 2 33   620 350 2 53   730 510 2 900   150 11000 0
float-newlib/double_req_bl_1232a_true-unreach-call.c .13  24 .85 2 .051 6.8 .46 2 .052 6.1 .33 2 3.3 260 29 2 .81 66 8.6 0 8.2 370 110 2 8.3 370 99 2 .098 26 1.0  2 31 1400 270 2 .35 59 3.2 2 4.0 270 40 2 2.7  76 36   2 .14  15 1.6  2 27   500 250 2 41   740 450 2 28   510 270 2 47   630 440 2 900   150 14000 0
float-newlib/double_req_bl_1250_true-unreach-call.c .13  24 1.1  2 .053 6.7 .34 2 .047 6.5 .26 2 3.2 260 34 2 .81 66 9.0 0 8.0 370 85 2 8.2 370 110 2 .082 26 1.0  2 12 1200 87 2 .38 59 3.0 2 4.4 270 47 2 2.6  74 33   2 .14  16 1.7  2 20   470 150 2 26   630 260 2 20   490 160 2 30   530 280 2 900   150 13000 0
float-newlib/double_req_bl_1251b_true-unreach-call.c .13  24 1.4  2 .087 6.5 .44 2 .088 6.4 1.2  2 3.2 260 31 2 11    15000 150   0 8.2 430 100 0 8.4 430 96 0 11     15000 150    0 30 1500 250 2 .39 59 3.1 2 12   350 110 2 2.8  75 36   2 .16  17 2.3  0 36   620 350 2 31   680 290 2 37   620 400 2 66   650 720 2 900   150 10000 0
float-newlib/double_req_bl_1252a_true-unreach-call.c .12  24 .90 2 .10  6.3 .25 2 .054 6.8 .30 2 3.3 270 30 2 .79 66 9.2 0 8.1 370 110 2 8.4 370 110 2 .094 26 1.1  2 31 1600 270 2 .37 59 3.2 2 4.4 270 42 2 2.7  76 33   2 .14  15 1.5  2 25   500 230 2 39   710 470 2 24   500 250 2 40   610 350 2 900   150 12000 0
float-newlib/double_req_bl_1300_true-unreach-call.c .11  24 .71 2 .054 6.6 .46 2 .077 6.2 .37 2 3.0 260 28 2 .79 66 9.5 0 8.0 430 98 0 8.3 430 100 0 .10  26 .75 2 14 1200 100 2 .39 59 4.8 2 12   340 99 2 3.0  89 36   2 .17  18 2.2  0 36   630 400 2 900   2100 9700 0 22   620 200 0 56   620 560 2 900   150 12000 0
float-newlib/float_req_bl_0220a_true-unreach-call.c .17  29 1.2  0 .089 8.5 .86 2 .13  9.6 .82 2 5.0 310 45 2 900    7300 9500   0 8.2 370 100 2 8.2 370 100 2 .36  59 4.1  2 74 2300 760 2 .43 64 3.6 2 14   780 100 2 180    830 1800   2 .27  16 3.6  2 76   770 790 2 900   1200 8900 0 73   780 670 2 85   650 890 2 870   170 11000 0
float-newlib/float_req_bl_0220b_true-unreach-call.c .12  29 1.7  0 .14  7.9 .72 2 .083 11   .84 2 4.8 310 46 2 900    7300 7500   0 8.1 370 97 2 8.3 370 110 2 .38  59 4.0  2 75 2300 740 2 .41 64 4.4 2 14   780 100 2 160    690 1400   2 .25  16 3.4  2 71   770 610 2 900   1100 9500 0 69   770 710 2 84   640 830 2 870   180 9900 0
float-newlib/float_req_bl_0240a_true-unreach-call.c .13  29 1.2  0 .078 7.4 .86 2 .082 10   .79 2 4.4 280 42 2 890    7300 7700   0 8.3 370 100 2 8.2 370 89 2 .39  62 5.3  2 80 2400 720 2 .45 63 3.5 2 14   780 110 2 42    490 410   2 .25  15 3.1  2 58   710 580 2 270   890 3100 2 59   760 490 2 84   660 830 2 870   170 11000 0
float-newlib/float_req_bl_0240b_true-unreach-call.c .13  29 1.4  0 .079 8.7 .86 2 .12  9.8 .77 2 4.5 290 45 2 900    7300 8500   0 8.3 370 120 2 8.3 370 95 2 .39  62 5.4  2 76 2300 670 2 .39 63 5.1 2 14   780 99 2 44    500 450   2 .25  16 3.0  2 59   710 530 2 300   920 2800 2 56   720 600 2 84   630 760 2 860   180 11000 0
float-newlib/float_req_bl_0250a_true-unreach-call.c .23  25 2.5  2 .13  6.3 .37 2 .060 7.8 .37 2 3.1 250 27 2 1.1  66 13   0 8.2 370 93 2 8.4 370 96 2 .19  34 2.1  2 30 1500 220 2 .39 60 3.2 2 5.5 310 56 2 8.7  500 110   2 .17  15 1.8  2 57   890 540 2 100   720 830 2 53   820 580 2 59   750 520 2 900   170 10000 0
float-newlib/float_req_bl_0250b_true-unreach-call.c .24  26 2.5  2 .056 7.1 .58 2 .060 6.8 .47 2 3.2 260 33 2 1.1  67 11   0 8.2 370 81 2 8.2 370 110 2 .22  34 2.3  2 29 1800 230 2 .38 60 4.5 2 5.3 310 54 2 13    650 150   2 .17  15 1.4  2 55   900 500 2 100   740 770 2 56   890 560 2 61   750 520 2 900   170 11000 0
float-newlib/float_req_bl_0260_true-unreach-call.c .22  25 2.6  2 .063 6.5 .36 2 .052 6.7 .44 2 3.0 250 28 2 1.1  66 12   0 8.2 370 96 2 8.1 370 96 2 .20  34 2.3  2 30 1600 250 2 .36 60 3.4 2 5.0 300 50 2 15    590 160   2 .19  15 1.8  2 56   880 640 2 110   720 790 2 60   890 470 2 60   750 650 2 900   160 12000 0
float-newlib/float_req_bl_0270a_true-unreach-call.c .27  35 2.9  2 .051 7.0 .54 2 .051 7.2 .53 2 3.1 250 29 2 1.1  67 14   0 8.0 370 120 2 8.3 370 100 2 .20  35 2.3  2 28 1500 230 2 .39 60 3.2 2 5.3 300 52 2 19    630 220   2 .16  15 1.8  2 54   990 520 2 99   990 760 2 59   960 510 2 61   750 650 2 900   160 13000 0
float-newlib/float_req_bl_0270b_true-unreach-call.c .27  35 3.1  2 .061 6.9 .62 2 .060 6.4 .39 2 3.1 250 24 2 1.1  66 12   0 8.3 370 97 2 8.3 370 110 2 .20  34 2.2  2 29 1600 260 2 .36 60 5.0 2 5.1 300 49 2 18    710 180   2 .16  15 1.8  2 58   950 570 2 93   1000 780 2 58   970 550 2 61   860 510 2 900   160 12000 0
float-newlib/float_req_bl_0281_true-unreach-call.c .78  120 9.7  2 1.5   96   16    2 47     160   690    2 20   830 150 2 35    280 420   0 8.3 430 100 0 8.4 430 100 0 9.6   270 120    2 30 1500 230 2 .40 61 3.8 2 190   3300 2100 0 46    900 490   2 .19  17 1.9  0 63   1000 500 2 78   2300 660 0 62   1000 550 2 80   900 630 2 860   160 9400 0
float-newlib/float_req_bl_0310_true-unreach-call.c .15  28 1.2  0 .11  7.6 .77 2 .083 9.9 .89 2 3.9 270 33 2 900    7300 8600   0 8.2 370 99 2 8.4 370 97 2 .41  59 4.4  2 80 2300 790 2 .43 64 4.1 2 15   900 110 2 37    540 440   2 .25  16 2.8  2 310   1200 3400 2 900   1300 11000 0 310   1100 3200 2 87   670 760 2 860   180 9700 0
float-newlib/float_req_bl_0320a_true-unreach-call.c .13  29 1.3  0 .086 8.4 .74 2 .12  9.7 .69 2 4.4 310 38 2 900    7300 7700   0 8.3 370 110 2 8.4 370 98 2 .37  60 4.7  2 70 2200 660 2 .42 64 4.0 2 14   780 98 2 200    790 1800   2 .24  16 3.1  2 63   780 550 2 900   1200 10000 0 71   790 560 2 85   640 700 2 870   170 12000 0
float-newlib/float_req_bl_0320b_true-unreach-call.c .14  29 1.2  0 .086 8.2 .77 2 .081 9.8 .75 2 4.3 290 41 2 900    7300 6900   0 8.2 370 120 2 8.2 370 100 2 .39  60 4.4  2 77 2300 780 2 .42 63 4.5 2 14   780 94 2 200    700 1500   2 .25  15 3.4  2 68   760 610 2 440   1000 4300 2 65   780 680 2 85   650 940 2 870   180 11000 0
float-newlib/float_req_bl_0330a_true-unreach-call.c .13  29 1.3  0 .093 8.7 .75 2 .088 10   .89 2 4.3 290 38 2 900    7300 9800   0 8.4 370 100 2 8.5 370 110 2 .40  61 4.0  2 83 2200 810 2 .40 64 4.9 2 14   770 98 2 37    500 530   2 .27  16 2.6  2 54   700 560 2 260   900 2500 2 50   690 550 2 86   670 850 2 860   220 9500 0
float-newlib/float_req_bl_0330b_true-unreach-call.c .13  29 1.3  0 .087 8.0 .88 2 .086 9.8 .72 2 4.2 280 39 2 900    7300 7600   0 8.1 370 130 2 8.3 370 110 2 .39  61 4.8  2 82 2200 840 2 .47 64 4.1 2 14   780 110 2 43    540 450   2 .25  15 3.4  2 51   700 560 2 220   910 2100 2 51   730 470 2 85   640 840 2 860   230 13000 0
float-newlib/float_req_bl_0460_true-unreach-call.c .96  160 11    2 2.2   120   26    2 12     120   170    2 20   970 170 2 29    350 380   0 8.3 430 99 0 8.5 430 100 0 9.6   340 100    2 31 1800 220 2 .39 60 3.9 2 140   3300 1200 0 57    1100 450   2 .20  18 2.1  0 73   1200 550 2 170   1200 1000 2 70   1200 590 2 80   900 640 2 860   170 10000 0
float-newlib/float_req_bl_0470_true-unreach-call.c .24  25 2.8  2 .059 6.4 .53 2 .084 6.3 .32 2 3.0 250 32 2 .88 67 9.4 0 8.1 370 110 2 8.4 370 93 2 .11  27 1.1  2 28 1500 210 2 .37 59 3.7 2 5.5 310 53 2 12    560 130   2 .17  16 1.9  2 69   1000 590 2 160   910 1100 2 69   1000 620 2 60   800 510 2 900   160 10000 0
float-newlib/float_req_bl_0480_true-unreach-call.c .30  37 3.4  2 .053 7.0 .64 2 .049 6.5 .52 2 3.1 250 28 2 .93 66 10   0 8.3 370 100 2 8.2 370 110 2 .13  27 1.6  2 28 1500 230 2 .36 60 3.9 2 5.5 310 52 2 5.5  210 74   2 .16  15 2.0  2 60   980 520 2 130   900 1100 2 58   960 560 2 60   820 550 2 900   160 14000 0
float-newlib/float_req_bl_0490a_true-unreach-call.c .25  25 2.6  2 .055 6.3 .55 2 .052 7.1 .46 2 3.0 250 27 2 .88 65 9.0 0 8.1 370 94 2 8.4 370 95 2 .11  27 1.1  2 31 1500 220 2 .37 60 3.5 2 5.5 310 51 2 17    760 180   2 .16  15 2.0  2 67   1000 570 2 160   960 1500 2 69   1000 560 2 59   800 600 2 900   160 11000 0
float-newlib/float_req_bl_0490b_true-unreach-call.c .25  25 3.3  2 .094 6.1 .62 2 .058 6.6 .34 2 3.4 270 28 2 .89 66 9.6 0 8.1 370 99 2 8.4 370 100 2 .11  27 1.3  2 30 1500 260 2 .40 60 3.2 2 5.5 310 49 2 9.5  500 100   2 .16  16 2.1  2 68   1000 530 2 160   940 1200 2 69   1000 540 2 59   800 490 2 900   170 11000 0
float-newlib/float_req_bl_0530a_true-unreach-call.c .14  29 1.2  0 .082 8.4 .94 2 .084 10   .81 2 4.2 290 39 2 900    7300 8100   0 8.4 370 97 2 8.3 370 100 2 .39  66 5.7  2 88 2700 750 2 .44 64 3.5 2 14   780 100 2 42    640 500   2 .25  16 3.0  2 67   1000 620 2 900   1300 5100 0 68   990 590 2 85   780 760 2 870   180 10000 0
float-newlib/float_req_bl_0530b_true-unreach-call.c .12  29 1.2  0 .11  8.6 .82 2 .092 11   .75 2 4.3 280 34 2 900    7300 7900   0 8.3 370 110 2 8.3 370 100 2 .40  66 6.5  2 100 2700 860 2 .43 64 3.7 2 14   780 110 2 660    1700 5200   2 .28  16 3.1  2 65   980 630 2 900   1400 7300 0 68   990 560 2 84   770 780 2 870   180 10000 0
float-newlib/float_req_bl_0550a_true-unreach-call.c .12  29 1.2  0 .087 8.7 .79 2 .081 10   .69 2 4.2 290 34 2 900    7300 8600   0 8.2 370 96 2 8.3 370 91 2 .44  69 4.7  2 93 2600 850 2 .42 64 4.5 2 14   790 100 2 33    570 390   2 .25  15 2.8  2 54   1000 490 2 210   1000 1600 2 58   990 590 2 84   770 810 2 870   180 11000 0
float-newlib/float_req_bl_0550b_true-unreach-call.c .14  29 1.2  0 .12  8.0 .73 2 .077 10   .89 2 4.1 280 39 2 900    7300 7300   0 8.1 370 120 2 8.3 370 100 2 .45  69 6.0  2 87 2600 800 2 .41 64 3.2 2 14   760 110 2 46    650 550   2 .25  16 3.0  2 54   1000 500 2 200   1000 1800 2 54   1000 510 2 83   730 700 2 870   180 12000 0
float-newlib/float_req_bl_0610_true-unreach-call.c .18  25 1.8  2 .064 6.6 .46 2 .067 6.3 .27 2 3.8 280 33 2 .96 66 11   0 8.2 370 94 2 8.2 370 100 2 .15  28 1.6  2 19 1400 140 2 .37 59 3.1 2 4.2 270 43 2 2.8  94 30   2 .15  15 1.8  2 60   800 490 2 440   2800 4000 0 76   870 650 2 58   600 690 2 900   160 11000 0
float-newlib/float_req_bl_0620a_true-unreach-call.c .17  24 1.5  2 .061 6.4 .40 2 .065 6.2 .25 2 3.7 280 30 2 .97 66 9.8 0 8.1 370 100 2 8.4 370 110 2 .15  28 1.6  2 17 1400 180 2 .38 60 3.1 2 4.9 290 49 2 10    290 91   2 .15  15 1.7  2 61   790 560 2 160   980 1200 2 78   900 740 2 60   640 530 2 900   160 10000 0
float-newlib/float_req_bl_0620b_true-unreach-call.c .18  25 1.6  2 .064 6.3 .51 2 .066 6.5 .33 2 4.0 310 38 2 .98 66 10   0 8.1 370 100 2 8.4 370 100 2 .14  28 1.5  2 16 1500 140 2 .37 59 3.4 2 4.6 280 45 2 4.6  240 58   2 .18  15 1.6  2 60   780 520 2 160   990 1400 2 77   910 810 2 60   630 570 2 900   160 11000 0
float-newlib/float_req_bl_0621a_true-unreach-call.c .17  25 1.8  2 .060 6.4 .40 2 .091 6.5 .33 2 3.2 270 31 2 .97 67 11   0 8.3 370 120 2 8.2 370 95 2 .13  27 1.9  2 19 1400 170 2 .37 59 3.5 2 4.3 280 41 2 3.5  100 44   2 .15  16 1.6  2 850   1100 7600 2 190   1000 1500 2 870   1100 8600 2 46   610 420 2 900   170 11000 0
float-newlib/float_req_bl_0621b_true-unreach-call.c .19  24 1.8  2 .076 6.4 .29 2 .093 5.6 .25 2 3.5 290 31 2 .96 66 10   0 8.1 370 100 2 8.3 370 94 2 .13  27 1.7  2 17 1500 130 2 .36 59 3.8 2 4.2 270 40 2 7.2  180 81   2 .17  16 1.6  2 340   1100 3100 2 170   1000 1300 2 370   1100 4100 2 51   600 440 2 900   160 11000 0
float-newlib/float_req_bl_0660a_true-unreach-call.c .58  96 7.0  2 1.3   72   16    2 5.4   73   74    2 6.3 530 64 2 1.4  67 16   0 8.0 430 99 0 8.3 430 94 0 .29  46 4.3  2 34 1600 250 2 .37 60 3.2 2 14   350 120 0 3.1  100 46   2 .20  17 1.9  0 43   760 410 2 180   990 1800 2 42   760 400 2 83   820 680 2 860   160 11000 0
float-newlib/float_req_bl_0660b_true-unreach-call.c .61  96 7.4  2 1.2   72   17    2 5.4   74   78    2 6.1 510 71 2 1.3  67 14   0 8.2 430 110 0 8.2 430 100 0 .26  45 3.5  2 36 1600 280 2 .38 60 3.3 2 14   400 110 0 5.8  330 74   2 .19  22 2.2  0 43   770 500 2 200   1000 1800 2 43   770 430 2 81   820 700 2 860   160 12000 0
float-newlib/float_req_bl_0661a_true-unreach-call.c .58  96 7.7  2 1.0   73   13    2 5.4   74   68    2 6.4 530 77 2 1.3  66 15   0 8.1 430 120 0 8.4 430 99 0 .29  46 3.8  2 36 1600 270 2 .39 60 3.0 2 13   360 120 0 26    450 240   2 .18  18 2.6  0 81   930 750 2 900   1300 8400 0 84   920 770 2 80   760 760 2 860   170 12000 0
float-newlib/float_req_bl_0661b_true-unreach-call.c .59  96 6.4  2 1.2   73   14    2 5.4   74   70    2 6.2 510 59 2 1.4  66 17   0 8.1 430 95 0 8.3 430 100 0 .26  46 3.0  2 32 1500 230 2 .39 60 3.3 2 13   360 130 0 30    530 330   2 .19  18 2.3  0 89   980 850 2 900   1500 8000 0 94   970 790 2 82   830 820 2 860   170 11000 0
float-newlib/float_req_bl_0662a_true-unreach-call.c .97  140 11    2 .089 7.0 .91 2 .090 7.3 .91 2 3.9 300 38 2 1.4  66 16   0 8.2 430 92 0 8.4 430 97 0 .28  50 3.2  2 32 1500 230 2 .40 60 3.9 2 13   340 110 0 13    480 120   2 .19  17 2.2  0 37   750 320 2 180   1000 1600 2 39   730 360 2 65   700 630 2 900   170 12000 0
float-newlib/float_req_bl_0662b_true-unreach-call.c .94  140 12    2 .091 6.9 .69 2 .13  7.2 .87 2 3.6 280 37 2 1.4  67 17   0 8.3 430 120 0 8.3 430 100 0 .30  50 3.2  2 31 1500 220 2 .37 60 4.6 2 14   350 130 0 9.7  360 140   2 .20  17 2.1  0 37   750 350 2 200   1000 1800 2 38   750 400 2 66   730 630 2 900   160 11000 0
float-newlib/float_req_bl_0663a_true-unreach-call.c .94  140 9.3  2 .081 7.2 .87 2 .098 7.3 .95 2 3.9 300 33 2 1.4  65 17   0 8.0 430 130 0 8.3 430 100 0 .31  50 3.5  2 35 1800 250 2 .37 60 3.5 2 13   350 110 0 5.6  320 66   2 .18  18 2.0  0 40   760 330 2 160   1100 1600 2 38   760 370 2 65   730 660 2 900   160 11000 0
float-newlib/float_req_bl_0663b_true-unreach-call.c 1.0   140 12    2 .12  6.9 .87 2 .094 7.5 .90 2 3.5 270 30 2 1.4  65 17   0 8.1 430 98 0 8.3 430 89 0 .28  51 3.2  2 33 1800 260 2 .37 60 3.3 2 13   400 130 0 38    650 370   2 .18  17 2.2  0 38   740 400 2 190   960 1600 2 38   740 360 2 65   720 750 2 900   170 13000 0
float-newlib/float_req_bl_0670_true-unreach-call.c 1.1   150 12    2 1.7   130   20    2 32     130   440    2 6.8 540 66 2 18    200 210   0 8.3 430 100 0 8.3 430 100 0 5.9   200 82    2 36 1600 260 2 .37 60 5.0 2 17   450 130 0 17    600 160   2 .18  17 2.2  0 87   850 960 2 180   1100 1800 2 86   850 950 2 83   930 780 2 860   180 10000 0
float-newlib/float_req_bl_0680a_true-unreach-call.c .27  38 3.1  2 .067 6.8 .41 2 .082 6.0 .38 2 3.5 250 34 2 1.2  66 15   0 8.2 370 120 2 8.2 370 120 2 .23  43 3.4  2 31 1800 250 2 .39 60 3.1 2 5.6 310 47 2 2.9  90 37   2 .16  15 1.8  2 38   740 440 2 180   1000 1600 2 40   740 410 2 64   760 630 2 900   160 13000 0
float-newlib/float_req_bl_0680b_true-unreach-call.c .26  38 2.5  2 .065 6.7 .55 2 .055 7.5 .51 2 3.8 280 33 2 1.3  67 17   0 8.2 370 100 2 8.3 370 120 2 .23  43 2.9  2 36 1800 280 2 .38 60 3.2 2 5.6 310 51 2 2.9  90 36   2 .16  15 2.0  2 44   810 480 2 170   1000 1800 2 47   820 450 2 63   750 580 2 900   160 9900 0
float-newlib/float_req_bl_0681a_true-unreach-call.c .25  39 3.8  2 .072 6.3 .92 2 .056 7.0 .44 2 3.9 280 39 2 1.2  67 14   0 8.1 370 110 2 8.3 370 130 2 .24  43 3.1  2 32 1500 220 2 .36 60 5.1 2 5.5 310 50 2 3.6  270 49   2 .17  15 1.7  2 39   750 360 2 160   950 1600 2 39   760 400 2 64   730 590 2 900   170 12000 0
float-newlib/float_req_bl_0681b_true-unreach-call.c .26  39 2.9  2 .077 6.6 .53 2 .089 6.2 .55 2 3.7 280 37 2 1.2  67 15   0 8.3 370 92 2 8.2 370 110 2 .24  43 3.5  2 34 1800 250 2 .37 60 3.4 2 5.5 310 49 2 3.7  270 35   2 .17  15 1.7  2 38   760 390 2 160   1000 1300 2 38   760 390 2 63   690 590 2 900   170 11000 0
float-newlib/float_req_bl_0682a_true-unreach-call.c .88  150 10    2 .91  67   11    2 9.4   68   130    2 6.8 550 66 2 1.6  72 19   0 8.3 430 110 0 8.3 430 110 0 .36  63 4.7  2 37 1600 270 2 .38 60 4.0 2 14   360 120 0 5.9  320 74   2 .18  17 2.0  0 49   810 440 2 480   2200 5800 2 50   810 490 2 66   750 650 2 860   160 10000 0
float-newlib/float_req_bl_0682b_true-unreach-call.c .89  150 10    2 .93  68   11    2 9.4   69   160    2 6.7 540 78 2 1.7  72 20   0 8.3 430 100 0 8.4 430 100 0 .36  64 5.2  2 35 1800 260 2 .39 60 3.3 2 14   400 120 0 5.7  330 62   2 .18  18 2.2  0 46   800 440 2 290   1200 3100 2 46   820 430 2 66   830 620 2 860   170 11000 0
float-newlib/float_req_bl_0683a_true-unreach-call.c .86  150 10    2 .96  68   11    2 18     77   290    2 6.6 540 69 2 1.6  72 20   0 8.2 430 100 0 8.4 430 110 0 .37  64 4.9  2 38 1600 270 2 .41 60 3.9 2 13   360 130 0 16    460 200   2 .20  17 2.1  0 45   830 450 2 320   1200 3600 2 46   790 490 2 66   780 740 2 870   160 12000 0
float-newlib/float_req_bl_0683b_true-unreach-call.c .87  150 11    2 .94  68   11    2 17     77   220    2 6.6 540 68 2 1.6  72 19   0 8.2 430 94 0 8.4 430 120 0 .36  64 4.5  2 37 1500 250 2 .39 60 3.5 2 13   370 120 0 13    430 120   2 .18  18 2.0  0 45   820 520 2 380   1300 3900 2 44   820 440 2 66   780 610 2 860   160 11000 0
float-newlib/float_req_bl_0684a_true-unreach-call.c .64  87 7.2  2 .10  7.3 1.1  2 .11  8.4 1.0  2 3.7 290 38 2 1.3  65 16   0 8.1 430 100 0 8.2 430 100 0 .26  48 3.5  2 33 1600 250 2 .38 60 3.5 2 13   350 110 0 13    460 140   2 .22  18 2.9  2 900   1000 8300 0 280   2700 2500 0 900   1000 8400 0 64   820 670 2 900   170 11000 0
float-newlib/float_req_bl_0684b_true-unreach-call.c .63  87 7.4  2 .11  7.7 1.1  2 .096 8.2 1.1  2 4.0 320 39 2 1.3  66 14   0 8.4 430 110 0 8.2 430 100 0 .29  48 3.2  2 32 1500 230 2 .39 60 3.3 2 13   350 110 0 61    440 490   2 .22  17 2.7  2 900   1100 8100 0 260   2700 2400 0 900   1000 7700 0 80   850 780 2 900   170 13000 0
float-newlib/float_req_bl_0685a_true-unreach-call.c .29  37 2.7  2 .059 7.0 .81 2 .065 6.8 .43 2 3.7 260 31 2 1.3  67 14   0 8.1 370 96 2 8.3 370 130 2 .24  43 3.1  2 34 1600 220 2 .39 60 3.3 2 5.7 310 51 2 2.9  100 40   2 .16  16 1.9  2 42   760 420 2 220   1100 2000 2 42   770 370 2 64   740 640 2 900   170 11000 0
float-newlib/float_req_bl_0685b_true-unreach-call.c .28  37 2.7  2 .064 7.3 .41 2 .062 7.4 .37 2 3.5 250 35 2 1.3  67 15   0 8.2 370 88 2 8.1 370 95 2 .23  43 2.2  2 31 1500 220 2 .36 60 4.1 2 5.2 310 55 2 2.9  89 35   2 .16  16 1.8  2 46   810 450 2 190   1000 2400 2 43   800 450 2 63   690 560 2 900   170 14000 0
float-newlib/float_req_bl_0686a_true-unreach-call.c .26  36 3.0  2 .11  6.3 .36 2 .068 6.7 .41 2 3.4 250 31 2 1.2  66 14   0 8.3 370 100 2 8.2 370 100 2 .24  43 2.9  2 37 1600 270 2 .37 60 3.9 2 5.3 310 45 2 2.9  90 40   2 .16  16 2.0  2 38   750 450 2 200   1000 1900 2 39   740 410 2 64   820 620 2 900   170 12000 0
float-newlib/float_req_bl_0686b_true-unreach-call.c .25  37 2.7  2 .062 6.9 .63 2 .083 6.3 .46 2 3.5 260 29 2 1.2  66 14   0 8.2 370 92 2 8.3 370 96 2 .23  43 3.0  2 37 1500 250 2 .39 60 4.0 2 5.6 310 53 2 3.1  100 42   2 .19  15 1.8  2 39   750 410 2 180   970 1800 2 41   730 410 2 64   660 620 2 900   160 12000 0
float-newlib/float_req_bl_0710_true-unreach-call.c .20  25 1.6  2 .18  12   2.5  2 .79  19   10    2 8.8 410 70 2 2.1  66 27   0 8.0 430 97 0 8.3 430 93 0 .54  42 6.7  2 17 1300 130 2 .43 59 3.7 2 54   1500 660 0 8.5  220 100   2 .18  17 2.4  0 290   2600 2300 2 24   2400 240 0 290   2500 2200 2 60   1700 540 2 900   150 11000 0
float-newlib/float_req_bl_0720_true-unreach-call.c .13  25 .90 2 .054 6.9 .46 2 .051 6.5 .34 2 2.9 250 27 2 .83 67 9.0 0 8.2 370 100 2 8.2 370 100 2 .098 26 1.2  2 100 1800 1200 2 .36 59 3.4 2 4.3 270 42 2 4.4  140 59   2 .15  14 1.7  2 34   570 370 2 19   370 170 2 33   580 350 2 57   600 570 2 900   150 10000 0
float-newlib/float_req_bl_0730a_true-unreach-call.c .12  25 1.0  2 .060 6.9 .37 2 .047 6.4 .36 2 2.8 250 29 2 .86 66 9.0 0 8.2 370 94 2 8.2 370 110 2 .10  27 .90 2 16 1200 110 2 .37 59 3.0 2 4.4 270 42 2 4.4  100 54   2 .15  16 1.9  2 26   460 240 2 21   440 180 2 27   460 260 2 52   570 480 2 900   150 12000 0
float-newlib/float_req_bl_0730b_true-unreach-call.c .12  24 .94 2 .056 6.7 .36 2 .042 6.6 .45 2 3.0 250 27 2 .84 68 9.2 0 8.1 370 120 2 8.3 370 100 2 .11  26 .87 2 17 1200 110 2 .37 59 3.2 2 4.5 270 42 2 4.5  150 60   2 .15  16 1.9  2 19   490 170 2 41   790 440 2 19   490 160 2 34   550 280 2 900   150 12000 0
float-newlib/float_req_bl_0730c_true-unreach-call.c .13  24 .86 2 .049 6.7 .62 2 .046 6.3 .36 2 2.9 250 27 2 .84 67 9.9 0 8.2 370 100 2 8.2 370 110 2 .092 26 .98 2 17 1200 130 2 .38 59 2.3 2 4.4 270 38 2 4.3  100 51   2 .16  15 1.7  2 19   490 150 2 26   470 270 2 19   490 160 2 33   540 280 2 900   160 10000 0
float-newlib/float_req_bl_0740_true-unreach-call.c .14  24 1.1  2 .052 6.8 .45 2 .049 6.4 .45 2 3.3 270 30 2 .82 66 10   0 8.0 370 98 2 8.2 370 98 2 .097 27 .95 2 17 1300 120 2 .38 59 2.9 2 4.1 270 37 2 4.4  150 57   2 .15  15 1.9  2 24   440 230 2 19   400 180 2 23   450 240 2 42   590 380 2 900   150 10000 0
float-newlib/float_req_bl_0831_true-unreach-call.c .15  25 1.6  2 .064 6.9 .41 2 .058 6.3 .29 2 3.5 280 33 2 .90 67 10   0 8.1 370 92 2 8.0 370 100 2 .11  27 1.3  2 18 1300 140 2 .37 59 3.1 2 4.6 270 41 2 4.3  270 45   2 .19  15 1.6  2 300   1900 3400 2 91   540 890 2 250   1700 2300 2 58   530 600 2 900   160 11000 0
float-newlib/float_req_bl_0832a_true-unreach-call.c .20  24 2.0  2 .052 6.4 .53 2 .064 5.7 .42 2 3.8 310 32 2 .90 67 9.5 0 8.3 370 120 2 8.2 370 100 2 .14  27 1.3  2 17 1300 130 2 .41 59 3.2 2 4.1 270 41 2 7.7  300 81   2 .18  16 1.6  2 100   770 930 2 110   790 1200 2 100   760 970 2 47   560 410 2 900   160 11000 0
float-newlib/float_req_bl_0832b_true-unreach-call.c .19  25 2.7  2 .11  6.2 .28 2 .051 6.6 .37 2 3.5 280 31 2 .90 67 9.6 0 8.2 370 110 2 8.2 370 100 2 .12  27 1.3  2 18 1300 150 2 .37 59 3.4 2 4.5 270 41 2 5.3  270 57   2 .15  16 1.7  2 110   780 1100 2 100   780 880 2 99   740 840 2 46   540 410 2 900   160 12000 0
float-newlib/float_req_bl_0833_true-unreach-call.c .18  24 1.8  2 .078 6.3 .33 2 .089 6.5 .30 2 3.5 280 30 2 .94 67 11   0 8.1 370 100 2 8.3 370 100 2 .12  27 1.6  2 18 1300 140 2 .41 59 2.9 2 4.5 270 44 2 18    380 220   2 .17  15 1.8  2 77   730 650 2 96   710 800 2 72   740 650 2 46   540 420 2 900   160 11000 0
float-newlib/float_req_bl_0834_true-unreach-call.c .16  24 1.5  2 .064 6.6 .44 2 .051 6.7 .42 2 3.5 280 33 2 .91 66 10   0 8.2 370 100 2 8.1 370 100 2 .14  27 1.7  2 17 1300 140 2 .36 59 4.4 2 4.5 280 48 2 4.7  220 62   2 .17  15 1.5  2 100   780 860 2 84   590 750 2 98   780 920 2 48   540 490 2 900   160 12000 0
float-newlib/float_req_bl_0870b_true-unreach-call.c .42  57 5.0  2 .12  8.7 1.2  2 .15  9.9 1.0  2 7.2 330 66 2 1.7  67 25   0 8.4 430 120 0 8.2 430 120 0 .52  70 6.0  2 49 2100 370 2 .76 65 6.6 2 15   490 130 0 86    1200 990   2 .23  18 2.7  0 60   940 500 2 94   890 790 2 56   930 470 2 71   790 660 2 900   170 11000 0
float-newlib/float_req_bl_0872a_true-unreach-call.c 1.2   190 14    2 .097 8.4 1.0  2 .12  10   .91 2 3.9 280 35 2 1.9  75 21   0 8.3 370 95 2 8.6 430 110 0 .57  79 6.8  2 49 2100 340 2 .72 65 7.6 2 6.6 430 64 2 5.0  140 57   2 .23  15 3.0  2 48   830 430 2 140   900 1500 2 51   940 570 2 68   790 640 2 900   170 11000 0
float-newlib/float_req_bl_0872b_true-unreach-call.c 1.2   190 16    2 .10  8.5 1.3  2 .10  9.9 1.7  2 3.5 250 33 2 1.9  75 21   0 8.2 370 100 2 8.4 430 100 0 .62  80 6.7  2 45 2100 320 2 .76 65 6.2 2 6.3 430 67 2 5.0  140 64   2 .24  15 2.7  2 50   920 500 2 130   880 1300 2 49   860 510 2 69   790 680 2 900   170 11000 0
float-newlib/float_req_bl_0873a_true-unreach-call.c .37  53 3.9  2 .099 9.2 1.1  2 .13  10   .78 2 3.8 280 34 2 1.6  66 19   0 8.0 370 110 2 8.3 370 110 2 .47  65 5.2  2 48 2100 370 2 .75 64 6.4 2 6.8 420 64 2 5.4  200 78   2 .21  15 2.8  2 78   1000 720 2 140   910 1300 2 74   960 640 2 68   780 610 2 900   170 10000 0
float-newlib/float_req_bl_0873b_true-unreach-call.c .38  53 3.6  2 .10  9.2 1.1  2 .13  10   .97 2 3.6 260 35 2 1.6  68 20   0 8.1 370 99 2 8.3 370 98 2 .45  65 6.4  2 47 2100 340 2 .71 64 9.2 2 6.6 420 62 2 7.3  260 100   2 .23  15 2.5  2 73   960 740 2 130   920 1500 2 73   940 610 2 69   790 610 2 900   170 12000 0
float-newlib/float_req_bl_0874_true-unreach-call.c 1.0   150 10    2 .15  10   2.0  2 .16  10   1.8  2 7.6 390 64 2 2.7  89 30   0 8.4 430 110 0 8.2 430 120 0 .80  80 12    2 49 2000 390 2 .79 66 6.8 2 16   490 140 0 120    1900 1100   2 .24  17 2.9  0 100   1100 930 2 900   1500 9700 0 90   980 800 2 69   810 570 2 900   170 11000 0
float-newlib/float_req_bl_0875_true-unreach-call.c 1.0   150 11    2 .16  9.6 3.3  2 .15  12   1.6  2 6.9 370 55 2 2.6  88 35   0 8.2 430 86 0 8.4 430 120 0 .80  79 9.5  2 47 2000 390 2 .80 65 7.5 2 16   550 130 0 83    1300 910   2 .24  17 4.0  0 88   990 820 2 100   980 1300 2 110   1100 1100 2 68   710 680 2 900   180 11000 0
float-newlib/float_req_bl_0876_true-unreach-call.c .98  150 11    2 .14  9.9 1.6  2 .21  11   1.6  2 7.9 430 66 2 2.0  77 23   0 8.2 430 100 0 8.2 430 99 0 .62  73 7.2  2 48 2300 360 2 .78 65 6.6 2 15   480 140 0 23    910 200   2 .24  18 3.1  0 100   1100 910 2 450   1400 5400 2 88   980 790 2 70   810 670 2 900   170 14000 0
float-newlib/float_req_bl_0877_true-unreach-call.c .98  150 11    2 .19  9.6 1.4  2 .16  11   1.9  2 7.3 330 60 2 2.0  77 25   0 8.3 430 96 0 8.7 430 110 0 .62  73 8.0  2 47 2100 340 2 .75 65 7.1 2 15   500 130 0 63    1300 550   2 .25  17 3.0  0 100   1100 960 2 91   930 1000 2 87   950 800 2 70   800 690 2 900   170 12000 0
float-newlib/float_req_bl_0880_true-unreach-call.c .58  78 6.4  2 4.7   50   68    2 880     11000   10000    0 910   6200 7500 0 2.3  97 32   0 8.2 430 99 0 8.2 430 94 0 1.8   130 20    2 910 6000 7800 0 40    15000 430   0 19   570 170 0 80    1300 630   2 .25  18 3.0  0 420   1600 4300 2 900   1400 12000 0 410   1500 4000 2 400   1300 3800 2 900   220 11000 0
float-newlib/float_req_bl_0881_true-unreach-call.c .55  78 7.0  2 4.8   50   61    2 880     11000   12000    0 910   7000 8200 0 2.4  95 34   0 8.3 430 95 0 8.3 430 100 0 1.9   130 23    2 910 7900 8900 0 40    15000 460   0 20   570 160 0 120    1500 1300   2 .25  18 2.7  0 360   1500 3700 2 900   1400 9400 0 350   1600 3900 2 400   1200 3300 2 900   170 11000 0
float-newlib/float_req_bl_0883_true-unreach-call.c .44  60 5.2  2 .17  12   2.1  2 .20  14   1.8  2 12   560 97 2 1.9  71 23   0 8.3 430 120 0 8.4 430 110 0 .54  70 5.0  2 51 2100 410 2 .78 65 7.0 2 16   500 150 0 63    1300 560   2 .23  18 2.8  0 170   1100 1700 2 120   2700 1500 0 190   1100 1700 2 70   790 660 2 900   170 13000 0
float-newlib/float_req_bl_0910a_true-unreach-call.c .18  25 2.1  2 .054 6.6 .48 2 .055 6.8 .45 2 3.2 250 31 2 .95 67 11   0 8.1 370 110 2 8.1 370 110 2 .14  27 1.5  2 20 1400 160 2 .39 59 3.1 2 4.5 280 45 2 2.9  120 35   2 .16  15 1.8  2 45   640 390 2 260   1000 2000 2 44   640 470 2 57   630 530 2 900   160 12000 0
float-newlib/float_req_bl_0910b_true-unreach-call.c .18  25 1.8  2 .061 6.2 .43 2 .044 6.8 .45 2 3.2 250 29 2 .94 65 10   0 8.1 370 110 2 8.2 370 110 2 .13  27 1.5  2 20 1400 160 2 .38 59 3.2 2 4.5 270 39 2 2.7  84 34   2 .16  16 1.7  2 45   620 580 2 280   1100 2100 2 44   620 440 2 57   650 560 2 900   160 13000 0
float-newlib/float_req_bl_0920a_true-unreach-call.c .55  80 6.6  2 1.7   76   18    2 1.6   77   20    2 5.4 480 51 2 1.2  67 13   0 8.3 430 110 0 8.4 430 100 0 .23  34 2.5  2 19 1600 170 2 .37 60 4.1 2 58   3100 540 0 25    500 250   2 .17  17 2.1  0 51   710 500 2 210   2400 2100 0 51   710 500 2 65   690 670 2 860   160 11000 0
float-newlib/float_req_bl_0920b_true-unreach-call.c .20  24 1.9  2 .066 6.7 .43 2 .064 6.6 .33 2 3.3 260 32 2 .95 66 10   0 7.9 370 110 2 8.3 370 94 2 .13  28 1.5  2 19 1600 150 2 .36 59 3.3 2 4.8 280 45 2 5.0  260 58   2 .17  16 1.8  2 54   670 470 2 260   1000 2000 2 52   670 480 2 56   690 540 2 900   160 11000 0
float-newlib/float_req_bl_0921_true-unreach-call.c .20  25 2.0  2 .064 6.2 .48 2 .051 6.4 .43 2 3.2 260 33 2 .96 67 10   0 8.2 370 110 2 8.4 370 120 2 .13  27 1.7  2 20 1400 150 2 .37 59 3.2 2 4.5 280 43 2 6.2  320 85   2 .18  15 1.7  2 62   700 600 2 260   2400 1900 0 66   710 620 2 56   690 570 2 900   160 12000 0
float-newlib/float_req_bl_0930_true-unreach-call.c .18  25 1.8  2 .059 6.2 .43 2 .057 6.8 .36 2 3.2 260 31 2 .96 66 12   0 8.3 370 100 2 8.3 370 120 2 .13  27 1.3  2 19 1600 150 2 .40 60 3.2 2 4.5 280 38 2 19    290 170   2 .15  15 1.8  2 190   1500 1600 0 280   2500 2100 0 190   1800 1700 0 58   690 510 2 900   160 12000 0
float-newlib/float_req_bl_0931_true-unreach-call.c .20  24 1.9  2 .11  5.7 .34 2 .049 6.5 .45 2 3.2 250 28 2 .95 66 11   0 8.2 370 87 2 8.2 370 110 2 .13  27 1.5  2 18 1600 160 2 .38 59 3.5 2 4.5 280 45 2 5.4  270 80   2 .18  15 1.6  2 52   740 490 2 270   1000 2300 2 48   740 480 2 58   690 530 2 900   160 13000 0
float-newlib/float_req_bl_0960a_true-unreach-call.c .23  28 2.1  2 .092 6.2 .40 2 .095 6.4 .39 2 3.4 250 32 2 1.0  67 12   0 8.0 370 110 2 8.2 370 100 2 .18  32 1.9  2 23 1500 170 2 .40 60 4.1 2 5.2 300 49 2 3.1  140 41   2 .17  15 1.7  2 38   620 350 2 240   980 2400 2 39   630 360 2 53   690 510 2 900   160 12000 0
float-newlib/float_req_bl_0960b_true-unreach-call.c .25  28 2.1  2 .065 6.5 .39 2 .091 6.3 .28 2 3.3 260 28 2 1.0  66 11   0 8.0 370 120 2 8.1 370 100 2 .16  32 1.8  2 23 1500 180 2 .39 60 3.1 2 4.8 300 48 2 2.8  95 36   2 .17  15 1.4  2 36   630 350 2 230   930 2400 2 38   620 350 2 59   680 550 2 900   170 11000 0
float-newlib/float_req_bl_0970a_true-unreach-call.c .65  90 6.8  2 1.3   83   13    2 2.6   84   40    2 6.4 540 72 2 1.3  67 18   0 8.1 430 100 0 8.3 430 95 0 .25  42 3.0  2 23 1500 190 2 .38 60 3.5 2 80   3300 640 0 15    460 170   2 .17  18 2.2  0 36   660 350 2 230   2400 1600 0 37   670 300 2 70   720 620 2 860   160 10000 0
float-newlib/float_req_bl_0970b_true-unreach-call.c .21  28 2.4  2 .065 6.5 .43 2 .055 6.2 .40 2 3.2 250 27 2 1.1  67 12   0 8.1 370 110 2 8.2 370 110 2 .16  32 2.0  2 22 1600 190 2 .39 60 4.2 2 5.4 310 48 2 7.4  290 75   2 .16  15 1.8  2 35   640 330 2 230   1000 1900 2 38   640 360 2 59   690 580 2 900   160 12000 0
float-newlib/float_req_bl_0971_true-unreach-call.c .23  29 2.6  2 .068 6.4 .49 2 .048 7.1 .52 2 3.5 270 36 2 1.1  66 12   0 8.2 370 110 2 8.0 370 97 2 .15  32 1.6  2 22 1500 180 2 .37 60 4.1 2 5.0 300 55 2 3.0  110 45   2 .20  15 1.7  2 41   680 370 2 900   1300 6600 0 43   690 440 2 59   680 590 2 900   160 13000 0
float-newlib/float_req_bl_0981_true-unreach-call.c .21  28 2.1  2 .062 6.4 .34 2 .10  6.3 .27 2 3.3 250 35 2 1.0  66 13   0 8.2 370 120 2 8.3 370 110 2 .16  32 2.1  2 22 1500 150 2 .38 60 3.0 2 5.3 310 49 2 3.1  110 42   2 .17  15 1.3  2 38   660 400 2 250   890 1900 2 40   650 420 2 60   640 580 2 900   160 12000 0
float-newlib/float_req_bl_1010_true-unreach-call.c .14  24 1.0  2 .054 6.4 .46 2 .055 6.4 .23 2 3.0 250 25 2 .80 65 7.8 0 8.1 370 100 2 8.4 370 110 2 .089 26 .78 2 15 1200 95 2 .36 59 3.1 2 3.9 210 36 2 2.6  74 33   2 .14  16 1.6  2 16   360 120 2 14   370 110 2 16   360 130 2 27   500 240 2 900   150 12000 0
float-newlib/float_req_bl_1011a_true-unreach-call.c .10  24 .94 2 .050 7.2 .39 2 .051 6.8 .26 2 3.1 250 27 2 .80 67 8.6 0 8.1 370 98 2 8.2 370 93 2 .082 26 .85 2 13 1200 100 2 .36 58 3.3 2 3.8 210 36 2 2.6  74 35   2 .14  16 1.8  2 16   380 140 2 15   360 140 2 17   370 140 2 30   570 270 2 900   150 11000 0
float-newlib/float_req_bl_1011b_true-unreach-call.c .098 24 .83 2 .059 7.4 .31 2 .047 6.9 .28 2 3.0 250 28 2 .84 66 11   0 8.3 370 100 2 8.3 370 100 2 .089 26 .86 2 15 1200 120 2 .37 59 3.6 2 3.9 220 40 2 2.6  74 31   2 .14  16 1.9  2 16   380 130 2 15   370 120 2 16   390 130 2 31   570 260 2 900   150 11000 0
float-newlib/float_req_bl_1012a_true-unreach-call.c .13  24 .85 2 .062 6.4 .34 2 .051 6.5 .29 2 3.0 250 25 2 .81 67 8.9 0 8.1 370 93 2 8.1 370 110 2 .090 26 1.2  2 14 1200 110 2 .36 59 2.9 2 3.9 210 44 2 2.6  73 31   2 .14  15 1.7  2 16   340 140 2 15   350 120 2 17   360 120 2 28   560 230 2 900   200 9800 0
float-newlib/float_req_bl_1012b_true-unreach-call.c .10  24 .82 2 .053 6.9 .33 2 .12  5.9 .32 2 3.0 250 30 2 .82 66 8.6 0 8.0 370 110 2 8.0 370 100 2 .10  26 .88 2 14 1100 91 2 .41 59 3.5 2 3.8 220 40 2 2.6  74 31   2 .14  16 1.6  2 16   360 120 2 16   370 120 2 16   350 120 2 28   560 280 2 900   150 13000 0
float-newlib/float_req_bl_1031_true-unreach-call.c .11  24 1.7  2 .049 7.1 .36 2 .053 6.0 .33 2 2.9 250 25 2 .82 66 9.3 0 8.1 370 110 2 8.0 370 76 2 .077 26 .93 2 15 1200 100 2 .36 59 3.8 2 3.7 230 33 2 2.6  75 35   2 .15  16 1.7  2 18   380 150 2 15   360 120 2 18   370 150 2 29   480 280 2 900   150 13000 0
float-newlib/float_req_bl_1032a_true-unreach-call.c .098 24 .94 2 .096 5.9 .27 2 .049 6.5 .32 2 3.1 250 29 2 .80 66 9.9 0 7.9 370 100 2 8.3 370 100 2 .099 26 .97 2 13 1200 98 2 .36 59 4.4 2 4.1 240 38 2 2.7  76 38   2 .14  15 1.6  2 18   450 150 2 18   440 150 2 18   450 150 2 33   580 340 2 900   150 14000 0
float-newlib/float_req_bl_1032b_true-unreach-call.c .10  24 .83 2 .056 7.6 .47 2 .093 5.4 .26 2 3.1 260 26 2 .83 67 8.6 0 8.0 370 110 2 8.5 370 98 2 .086 26 .89 2 14 1200 98 2 .38 59 3.0 2 4.2 230 42 2 2.7  75 30   2 .14  16 1.7  2 18   450 160 2 18   440 140 2 18   460 180 2 33   610 280 2 900   150 11000 0
float-newlib/float_req_bl_1032c_true-unreach-call.c .12  24 .84 2 .050 6.6 .41 2 .081 6.6 .36 2 3.0 250 28 2 .81 66 8.2 0 8.0 370 110 2 8.0 370 100 2 .083 26 .98 2 14 1200 100 2 .36 59 3.7 2 3.7 240 36 2 2.6  75 41   2 .15  16 1.7  2 18   370 150 2 16   360 140 2 17   370 150 2 30   510 260 2 900   150 10000 0
float-newlib/float_req_bl_1032d_true-unreach-call.c .11  24 1.1  2 .054 6.8 .33 2 .049 6.6 .30 2 2.9 250 27 2 .79 65 8.7 0 8.1 370 97 2 8.2 370 94 2 .081 26 .85 2 13 1200 92 2 .36 59 3.2 2 4.2 240 43 2 2.6  75 39   2 .14  16 1.7  2 17   360 140 2 15   370 120 2 18   380 150 2 30   510 310 2 900   150 13000 0
float-newlib/float_req_bl_1051_true-unreach-call.c .12  24 1.1  2 .054 6.4 .42 2 .043 6.0 .38 2 3.1 250 29 2 .82 68 8.5 0 8.0 370 93 2 8.1 370 97 2 .094 26 .98 2 15 1200 110 2 .37 59 3.1 2 4.2 240 42 2 2.6  76 34   2 .16  16 1.6  2 19   390 180 2 16   340 150 2 18   390 150 2 32   520 330 2 900   150 13000 0
float-newlib/float_req_bl_1052a_true-unreach-call.c .11  24 .96 2 .10  6.2 .36 2 .043 6.3 .34 2 3.1 260 28 2 .81 66 8.6 0 8.2 370 90 2 8.1 370 98 2 .085 26 .75 2 14 1200 99 2 .35 59 4.1 2 4.2 240 40 2 2.7  76 33   2 .15  16 1.7  2 20   410 200 2 18   370 150 2 20   410 190 2 37   530 310 2 900   150 13000 0
float-newlib/float_req_bl_1052b_true-unreach-call.c .10  24 1.3  2 .050 6.8 .49 2 .041 6.6 .43 2 3.1 250 32 2 .80 67 9.4 0 8.2 370 120 2 8.1 370 110 2 .081 26 1.2  2 12 1200 85 2 .36 59 4.1 2 4.2 240 43 2 2.6  76 30   2 .15  15 1.7  2 19   420 200 2 18   370 170 2 19   420 160 2 36   570 360 2 900   150 10000 0
float-newlib/float_req_bl_1052c_true-unreach-call.c .11  24 1.1  2 .052 7.0 .54 2 .094 5.5 .35 2 3.1 250 25 2 .82 66 9.7 0 8.2 370 110 2 8.0 370 110 2 .089 26 .97 2 16 1200 110 2 .36 59 2.8 2 4.3 240 37 2 2.7  77 42   2 .15  15 1.7  2 22   480 200 2 19   440 190 2 22   530 200 2 44   640 490 2 900   150 11000 0
float-newlib/float_req_bl_1052d_true-unreach-call.c .11  24 .75 2 .085 6.3 .36 2 .056 6.0 .28 2 3.0 250 29 2 .83 66 8.6 0 8.1 370 110 2 8.1 370 110 2 .084 26 .91 2 15 1200 100 2 .37 59 3.6 2 3.8 240 36 2 2.6  76 34   2 .15  15 1.8  2 21   460 180 2 18   450 140 2 21   470 190 2 37   580 340 2 900   150 11000 0
float-newlib/float_req_bl_1071_true-unreach-call.c .13  24 .85 2 .088 6.0 .29 2 .048 6.4 .27 2 3.1 250 26 2 .80 67 8.7 0 8.2 370 100 2 8.0 370 95 2 .084 26 1.2  2 13 1200 97 2 .35 59 2.8 2 3.6 220 38 2 2.6  74 30   2 .17  15 2.8  2 16   370 140 2 17   370 130 2 16   370 130 2 28   490 230 2 900   150 12000 0
float-newlib/float_req_bl_1072a_true-unreach-call.c .11  24 .85 2 .044 6.7 .40 2 .045 6.6 .30 2 3.0 250 26 2 .85 68 9.2 0 7.9 370 100 2 8.4 370 110 2 .095 26 1.1  2 15 1200 95 2 .36 59 3.1 2 4.1 230 34 2 2.6  76 32   2 .14  15 1.7  2 16   390 150 2 17   410 140 2 16   380 130 2 28   550 220 2 900   200 12000 0
float-newlib/float_req_bl_1072b_true-unreach-call.c .16  24 .94 2 .054 6.5 .32 2 .048 6.4 .37 2 3.0 250 26 2 .82 68 8.9 0 8.1 370 110 2 8.2 370 100 2 .088 26 1.0  2 13 1200 95 2 .37 59 3.0 2 4.0 220 43 2 2.6  76 35   2 .14  16 1.6  2 17   390 150 2 16   410 140 2 17   390 140 2 28   550 230 2 900   150 12000 0
float-newlib/float_req_bl_1072c_true-unreach-call.c .14  24 .87 2 .050 6.6 .48 2 .061 6.5 .27 2 3.0 260 26 2 .78 65 7.7 0 8.2 370 100 2 8.1 370 98 2 .094 26 .85 2 14 1200 110 2 .36 59 3.5 2 4.1 220 43 2 2.6  76 39   2 .16  16 1.5  2 17   450 150 2 21   510 200 2 18   440 150 2 34   590 340 2 900   150 12000 0
float-newlib/float_req_bl_1072d_true-unreach-call.c .12  24 .91 2 .063 6.3 .47 2 .041 6.7 .59 2 3.0 260 30 2 .81 67 8.4 0 8.2 370 96 2 7.9 370 100 2 .082 26 1.2  2 12 1200 90 2 .35 59 3.4 2 4.0 220 37 2 2.6  76 34   2 .16  15 2.0  2 18   450 160 2 21   510 200 2 18   440 150 2 33   580 290 2 900   150 9900 0
float-newlib/float_req_bl_1091_true-unreach-call.c .13  24 1.1  2 .094 5.9 .38 2 .046 6.5 .34 2 3.1 260 27 2 .84 67 9.7 0 8.0 370 91 2 8.1 370 120 2 .10  26 .78 2 15 1200 100 2 .36 59 3.0 2 3.8 240 42 2 2.6  76 37   2 .17  15 1.7  2 18   380 150 2 17   370 150 2 19   390 170 2 32   500 270 2 900   150 13000 0
float-newlib/float_req_bl_1092a_true-unreach-call.c .10  24 .89 2 .053 6.4 .39 2 .042 6.6 .40 2 3.1 250 32 2 .83 67 8.7 0 8.3 370 110 2 8.1 370 100 2 .11  26 .94 2 13 1200 110 2 .36 59 3.7 2 4.2 240 39 2 2.7  77 30   2 .14  15 1.9  2 21   470 190 2 20   440 180 2 22   470 180 2 37   560 350 2 900   150 11000 0
float-newlib/float_req_bl_1092b_true-unreach-call.c .11  24 .97 2 .053 7.0 .63 2 .055 6.4 .26 2 3.1 260 30 2 .82 66 11   0 8.1 370 97 2 8.1 370 100 2 .087 26 1.3  2 14 1200 97 2 .37 59 3.1 2 4.3 250 42 2 2.7  77 32   2 .17  16 1.6  2 22   500 210 2 19   440 150 2 22   520 230 2 44   650 380 2 900   150 10000 0
float-newlib/float_req_bl_1092c_true-unreach-call.c .11  24 .82 2 .054 7.4 .38 2 .086 6.0 .24 2 3.0 250 25 2 .86 68 9.3 0 8.2 370 100 2 8.1 370 110 2 .088 26 .86 2 13 1200 94 2 .40 59 2.9 2 4.2 240 45 2 2.7  76 33   2 .17  16 1.9  2 20   420 190 2 18   360 150 2 20   430 210 2 35   520 290 2 900   150 12000 0
float-newlib/float_req_bl_1092d_true-unreach-call.c .11  24 .94 2 .062 6.7 .34 2 .072 6.0 .21 2 3.0 260 29 2 .83 66 9.1 0 8.2 370 100 2 8.1 370 110 2 .11  26 .92 2 15 1200 100 2 .37 59 3.5 2 4.2 250 37 2 2.6  76 30   2 .17  15 1.6  2 20   420 170 2 17   370 140 2 20   410 160 2 35   530 360 2 900   150 13000 0
float-newlib/float_req_bl_1121a_true-unreach-call.c .16  24 1.4  2 .11  6.4 .52 2 .071 7.2 .71 2 5.2 310 46 2 .89 66 10   0 8.4 430 120 0 8.4 430 100 0 .098 27 1.1  2 19 1300 140 2 .36 59 3.7 2 6.4 340 58 -16 3.8  140 50   2 .17  17 1.9  0 56   610 490 2 42   560 410 2 54   630 580 2 60   580 520 2 900   200 11000 0
float-newlib/float_req_bl_1121b_true-unreach-call.c .14  24 1.8  2 .076 7.1 .67 2 .075 8.0 .77 2 5.1 310 41 2 .92 67 11   0 8.0 430 110 0 8.3 430 97 0 .13  27 1.1  2 20 1300 140 2 .39 60 3.0 2 6.0 330 52 -16 3.7  140 45   2 .17  17 2.3  0 51   630 630 2 46   590 500 2 52   630 490 2 61   590 600 2 900   160 8900 0
float-newlib/float_req_bl_1122a_true-unreach-call.c .17  24 1.3  2 .066 6.4 .61 2 .065 7.7 .57 2 6.8 350 57 2 .93 65 11   0 8.2 430 120 0 8.2 430 120 0 .10  27 1.1  2 18 1300 130 2 .39 59 3.3 2 16   1300 140 2 5.5  180 78   2 .18  17 2.2  0 50   630 460 2 36   570 340 2 48   640 490 2 62   580 530 2 900   160 12000 0
float-newlib/float_req_bl_1122b_true-unreach-call.c .17  25 1.5  2 .066 6.4 .58 2 .074 6.6 .52 2 6.4 360 63 2 .91 66 11   0 8.2 430 100 0 8.5 430 100 0 .11  27 1.5  2 16 1400 130 2 .36 59 3.6 2 17   1300 150 2 5.9  170 87   2 .19  17 2.3  0 51   630 590 2 43   600 420 2 53   640 500 2 62   590 600 2 900   160 11000 0
float-newlib/float_req_bl_1130a_true-unreach-call.c .17  25 1.2  2 .22  11   2.0  2 2.8   37   33    2 8.5 500 65 2 .91 66 9.1 0 8.3 430 110 0 8.3 430 99 0 .12  27 1.2  2 18 1200 130 2 .36 59 3.5 2 23   1300 220 2 6.7  180 76   2 .18  18 2.7  0 22   560 200 2 42   630 440 2 21   550 220 2 45   530 400 2 900   160 12000 0
float-newlib/float_req_bl_1130b_true-unreach-call.c .16  25 1.6  2 .18  11   2.2  2 2.8   37   40    2 7.7 430 61 2 .92 67 10   0 8.3 430 110 0 8.3 430 91 0 .13  27 1.1  2 18 1300 130 2 .40 59 3.4 2 30   1300 250 2 7.0  180 66   2 .17  17 2.3  0 23   570 220 2 41   630 450 2 22   570 200 2 48   530 400 2 900   160 11000 0
float-newlib/float_req_bl_1131a_true-unreach-call.c .16  24 1.9  2 .16  11   1.4  2 1.3   33   17    2 8.3 390 70 2 .92 67 10   0 8.2 430 110 0 8.3 430 110 0 .10  27 1.1  2 18 1300 120 2 .37 59 3.2 2 12   320 99 2 5.3  180 68   2 .25  22 1.6  0 24   560 200 2 30   600 310 2 23   570 200 2 48   590 450 2 900   160 11000 0
float-newlib/float_req_bl_1131b_true-unreach-call.c .17  24 1.6  2 .19  10   1.4  2 1.3   33   16    2 7.9 470 65 2 .90 67 10   0 8.2 430 100 0 8.3 430 100 0 .11  27 1.2  2 18 1300 130 2 .37 59 3.8 2 12   320 100 2 6.0  170 74   2 .21  18 2.6  0 25   590 240 2 32   600 330 2 25   580 270 2 44   570 400 2 900   160 11000 0
float-newlib/float_req_bl_1211a_true-unreach-call.c .11  24 1.4  2 .083 6.2 .46 2 .055 6.4 .33 2 3.2 250 27 2 .82 67 9.5 0 8.1 370 95 2 8.2 430 120 0 .087 27 1.1  2 14 1200 120 2 .38 59 3.7 2 4.4 250 38 2 2.8  78 32   2 .16  16 2.3  2 20   510 160 2 22   530 170 2 20   510 200 2 37   650 320 2 900   160 11000 0
float-newlib/float_req_bl_1211b_true-unreach-call.c .11  24 .96 2 .060 6.3 .35 2 .050 6.5 .39 2 3.1 250 29 2 .85 67 11   0 8.1 370 96 2 8.4 430 110 0 .10  26 1.1  2 17 1200 100 2 .37 59 3.4 2 4.4 250 45 2 2.8  78 38   2 .17  15 1.8  2 19   480 170 2 22   520 160 2 19   490 160 2 35   650 330 2 900   150 11000 0
float-newlib/float_req_bl_1230_true-unreach-call.c .12  24 .91 2 .052 6.4 .44 2 .076 6.6 .35 2 3.0 260 32 2 .83 67 9.4 0 7.9 370 120 2 8.1 370 120 2 .11  26 1.0  2 14 1100 85 2 .35 59 3.4 2 4.2 260 38 2 2.6  77 33   2 .14  16 1.6  2 19   470 170 2 15   370 120 2 19   480 170 2 29   540 250 2 900   160 11000 0
float-newlib/float_req_bl_1231_true-unreach-call.c .12  24 1.0  2 .078 7.3 .98 2 1.6   44   20    2 3.3 260 28 2 .83 65 10   0 8.1 430 98 0 8.4 430 99 0 .11  26 1.0  2 18 1300 160 2 .41 59 4.1 2 29   560 260 2 2.9  73 38   2 .16  17 1.9  0 46   780 500 2 900   1200 8800 0 57   800 590 2 63   830 680 2 900   150 13000 0
float-newlib/float_req_bl_1232a_true-unreach-call.c .11  24 .86 2 .058 6.7 .36 2 .062 6.6 .24 2 3.1 260 26 2 .81 67 9.5 0 8.0 370 100 2 8.2 370 98 2 .086 26 1.0  2 15 1300 120 2 .36 59 3.5 2 4.2 250 42 2 2.6  77 37   2 .16  15 2.1  2 19   460 190 2 20   520 190 2 19   460 160 2 31   510 290 2 900   160 12000 0
float-newlib/float_req_bl_1250_true-unreach-call.c .13  24 1.1  2 .055 6.5 .39 2 .091 5.4 .24 2 3.1 250 32 2 .81 67 9.1 0 8.0 370 100 2 8.1 370 99 2 .082 26 .87 2 14 1100 90 2 .40 59 3.1 2 4.2 250 38 2 2.6  77 36   2 .14  15 1.8  2 18   490 150 2 16   370 120 2 19   470 170 2 28   530 230 2 900   150 12000 0
float-newlib/float_req_bl_1251_true-unreach-call.c .12  24 1.2  2 .085 6.5 .76 2 1.6   44   23    2 3.2 260 35 2 .85 67 9.3 0 8.2 430 130 0 8.4 430 110 0 .095 26 1.1  2 18 1200 120 2 .44 59 4.1 2 28   590 300 2 2.8  73 39   2 .16  17 2.2  0 46   760 490 2 900   1200 9400 0 56   800 670 2 63   900 610 2 900   150 11000 0
float-newlib/float_req_bl_1252a_true-unreach-call.c .11  24 .78 2 .060 6.7 .38 2 .048 6.6 .28 2 3.0 260 30 2 .79 67 9.5 0 8.2 370 110 2 8.0 370 92 2 .090 26 .78 2 17 1300 120 2 .35 59 5.2 2 4.2 240 37 2 2.6  78 44   2 .14  16 1.7  2 19   460 160 2 20   530 180 2 18   470 150 2 32   520 280 2 900   150 12000 0
float-newlib/float_req_bl_1270a_true-unreach-call.c .41  57 4.3  2 .58  45   9.2  2 6.2   75   81    2 19   640 150 2 9.4  120 110   0 8.2 430 86 0 8.3 430 100 0 3.0   110 36    2 35 1500 250 2 .40 61 3.6 2 22   540 210 2 7.9  230 89   2 .21  18 2.7  0 120   780 1500 2 27   550 240 0 130   770 1300 2 77   710 720 2 860   160 11000 0
float-newlib/float_req_bl_1270b_true-unreach-call.c .43  58 4.0  2 .59  44   7.9  2 6.1   75   91    2 20   640 130 2 9.3  120 110   0 8.4 430 110 0 8.2 430 100 0 3.0   110 33    2 35 1800 270 2 .44 61 3.7 2 22   530 220 2 8.7  250 120   2 .22  18 2.3  0 98   780 1200 2 900   1500 12000 0 100   750 1000 2 76   620 750 2 870   160 11000 0
float-newlib/float_req_bl_1270c_true-unreach-call.c .40  57 4.6  2 .59  44   7.9  2 6.0   74   78    2 19   580 160 2 9.4  120 120   0 8.2 430 120 0 8.2 430 100 0 3.0   110 40    2 34 1500 240 2 .41 61 3.7 2 21   550 180 2 8.4  290 110   2 .24  18 2.5  0 240   840 1900 2 33   650 360 0 300   850 2400 0 80   830 890 2 860   170 8500 0
float-newlib/float_req_bl_1270d_true-unreach-call.c .39  57 5.2  2 .61  44   7.0  2 6.2   74   81    2 19   660 140 2 9.3  120 110   0 8.2 430 110 0 8.3 430 97 0 3.0   110 39    2 33 1400 240 2 .39 61 4.9 2 20   590 190 2 13    290 130   2 .22  18 2.7  0 250   820 2600 2 300   2200 2600 0 220   870 2000 0 76   760 780 2 860   160 10000 0
float-newlib/float_req_bl_1271a_true-unreach-call.c .39  58 4.3  2 .59  44   6.9  2 5.9   79   84    2 21   610 150 2 10    120 130   0 8.2 430 88 0 8.4 430 110 0 3.0   110 36    2 35 1400 250 2 .39 60 5.0 2 18   510 150 2 11    320 130   2 .22  18 2.7  0 300   860 2600 0 38   640 390 0 250   880 2100 0 80   820 740 2 870   160 11000 0
float-newlib/float_req_bl_1271b_true-unreach-call.c .43  57 4.5  2 .59  44   7.0  2 5.9   78   75    2 21   750 150 2 9.3  120 110   0 8.1 430 110 0 8.2 430 110 0 3.0   110 47    2 29 1400 210 2 .38 60 3.2 2 26   530 220 2 26    450 330   2 .22  18 3.2  0 350   910 3600 0 37   650 440 0 360   900 3200 0 81   820 780 2 870   160 11000 0
float-newlib/float_req_bl_1381_true-unreach-call.c .13  24 .93 2 .057 6.6 .37 2 .10  5.9 .28 2 3.1 260 29 2 .85 66 9.3 0 8.2 430 100 0 8.2 430 100 0 .084 26 .83 2 14 1100 97 2 .36 59 3.3 2 11   320 90 2 2.7  74 33   2 .16  18 1.9  0 14   330 130 2 15   370 110 2 16   370 130 2 27   490 240 2 900   150 13000 0
float-newlib/double_req_bl_0870a_false-unreach-call.c 2.4   400 31    1 .12  9.8 1.1  1 .11  10   1.1  1 920   5600 7200 0 .29 47 3.6 1 8.4 430 100 0 8.5 430 100 0 .26  40 3.0  1 920 4800 7600 0 .76 64 5.6 1 18   560 160 1 570    5200 8300   0 .24  18 3.2  0 77   1600 630 0 270   2000 2200 0 72   1700 590 0 29   300 230 1 340   170 4400 1
float-newlib/double_req_bl_1210_false-unreach-call.c .14  24 1.5  1 .070 9.9 .75 1 .076 8.8 .66 1 3.8 320 38 1 .16 34 2.1 1 8.2 430 96 1 8.0 430 110 1 .11  27 1.1  1 17 1300 120 1 .38 59 4.1 1 5.7 310 48 1 2.9  88 39   0 .18  15 2.0  1 29   560 270 1 900   1100 9800 0 29   560 280 1 16   340 120 1 3.9 160 36 1
float-newlib/double_req_bl_1232b_false-unreach-call.c .13  24 .91 1 .080 9.0 .45 1 .063 9.4 .63 1 3.3 270 29 1 .15 34 1.8 1 8.1 430 100 1 8.2 430 97 1 .095 26 1.1  1 33 1600 310 1 .37 59 3.0 1 5.5 300 49 1 3.5  110 45   1 .17  16 1.8  1 23   520 190 0 28   670 270 1 22   510 230 0 14   280 120 1 3.6 150 34 1
float-newlib/double_req_bl_1252b_false-unreach-call.c .16  24 .90 1 .082 9.4 .54 1 .074 9.6 .53 1 3.4 270 32 1 .16 34 1.7 1 8.1 430 120 1 8.3 430 120 1 .090 26 1.2  1 34 1300 310 1 .38 59 4.7 1 5.5 290 51 1 3.4  110 41   1 .18  16 2.0  1 24   510 220 0 26   640 230 1 23   520 260 0 14   280 120 1 3.6 150 32 1
float-newlib/float_req_bl_0870a_false-unreach-call.c 1.1   150 12    1 .16  9.5 1.0  1 .11  11   1.2  1 7.7 380 72 1 .25 39 3.2 1 8.4 430 110 0 8.0 430 99 0 .19  32 2.4  1 790 2600 7700 1 .75 64 6.8 1 16   490 130 0 37    640 510   0 .26  18 2.8  0 41   790 360 0 84   840 680 0 38   780 430 0 26   290 200 1 9.1 170 100 1
float-newlib/float_req_bl_1210_false-unreach-call.c .13  25 1.2  1 .063 8.8 1.4  1 .076 8.9 .56 1 3.3 260 33 1 .15 34 1.7 1 8.4 430 110 1 8.1 430 120 1 .11  26 .89 1 17 1300 120 1 .38 59 3.6 1 5.6 300 50 1 2.8  81 32   0 .18  16 1.8  1 18   370 140 1 900   1200 9900 0 18   380 150 1 15   290 110 1 3.5 160 36 1
float-newlib/float_req_bl_1232b_false-unreach-call.c .12  24 1.0  1 .16  9.5 .48 1 .10  9.3 .49 1 3.2 250 26 1 .15 34 1.8 1 8.1 430 100 1 8.2 430 94 1 .090 26 1.1  1 19 1200 120 1 .37 59 3.7 1 5.4 300 55 1 3.3  77 42   1 .17  15 1.9  1 17   430 170 0 19   520 150 1 18   430 160 0 15   280 100 1 3.5 160 34 1
float-newlib/float_req_bl_1252b_false-unreach-call.c .13  23 .90 1 .061 9.2 1.3  1 .086 8.8 .43 1 3.3 250 32 1 .15 34 1.8 1 8.1 430 110 1 8.3 430 100 1 .10  26 .84 1 16 1300 130 1 .36 59 3.4 1 5.5 290 58 1 3.4  81 46   1 .19  16 1.9  1 18   430 140 0 20   530 180 1 18   430 150 0 14   280 120 1 3.5 160 36 1
loop-floats-scientific-comp/loop1_true-unreach-call.c.i 900     1400 12000    0 880     560   8000    0 880     1200   10000    0 920   2700 10000 0 850    300 8400   0 8.0 430 95 0 8.3 430 99 0 900     270 12000    0 920 4200 8700 0 900    3800 5100   0 57   1700 550 0 880    510 6500   0 900     61 13000    0 900   2800 7200 0 29   430 240 0 900   2600 7000 0 900   1800 7200 0 860   150 10000 0
loop-floats-scientific-comp/loop2_true-unreach-call.c.i 900     570 7900    0 870     570   6800    0 880     880   7100    0 900   7700 12000 0 900    570 8700   0 8.1 430 110 0 8.2 430 120 0 900     250 11000    0 910 2700 9300 0 900    390 7200   0 11   290 96 0 880    580 7900   0 .19  17 2.4  0 900   2900 7200 0 57   650 490 0 900   2900 6900 0 900   820 11000 0 860   150 11000 0
loop-floats-scientific-comp/loop3_true-unreach-call.c.i 900     860 9100    0 880     520   7800    0 880     1300   8100    0 900   7800 13000 0 900    550 7600   0 8.2 430 120 0 8.3 430 100 0 900     260 10000    0 910 4600 9200 0 900    680 7200   0 11   300 97 0 880    890 6000   0 .19  18 2.0  0 840   3100 8900 0 63   510 620 0 830   3100 8400 0 900   760 8400 0 860   150 11000 0
loop-floats-scientific-comp/loop5_true-unreach-call.c.i 900     1200 9900    0 880     2100   6300    0 .092 13   1.0  0 4.6 330 39 0 100    14000 1000   0 8.3 430 100 0 1.7 200 21 0 900     1700 9600    0 18 1300 150 -16 900    12000 10000   0 8.3 270 79 0 .82 33 12   0 900     53 10000    0 12   330 120 0 13   330 110 0 12   320 110 0 900   7700 6700 0 860   180 11000 0
loop-floats-scientific-comp/loop1_false-unreach-call.c.i .22  23 1.9  1 .12  13   1.6  1 .18  11   2.1  1 3.9 290 36 1 1.7  53 20   1 8.1 430 99 0 8.3 430 100 0 1.6   46 21    1 14 1200 89 1 900    520 7000   0 23   1200 220 1 13    200 120   1 900     59 9700    0 17   410 140 1 32   430 250 1 17   410 150 1 15   300 150 1 5.5 150 57 1
loop-floats-scientific-comp/loop2_false-unreach-call.c.i .23  24 2.5  1 .20  20   2.4  1 .13  13   1.2  1 4.1 300 43 1 1.4  51 18   1 8.3 430 110 0 8.3 430 100 0 1.3   42 21    1 13 1200 100 1 900    610 6400   0 11   300 100 0 84    390 710   0 .18  18 2.1  0 26   530 220 1 60   660 550 0 23   530 200 1 25   320 220 1 5.9 150 56 1
loop-floats-scientific-comp/loop4_false-unreach-call.c.i .38  38 3.9  0 .37  26   4.5  0 .090 13   1.0  0 4.9 330 46 0 88    14000 910   0 8.2 430 130 0 1.8 200 23 0 900     2200 9700    0 19 1300 140 1 .79 71 7.0 1 8.2 270 76 0 .82 33 9.8 0 900     53 10000    0 13   340 120 0 13   300 94 0 12   310 100 0 26   340 210 1 9.5 180 100 0
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score
total 469 41000    67000 410000   721 469 44000   180000 410000 800 469 43000 240000 470000 792 469 60000 450000 560000 761 469 80000 460000 900000 36 469 4300 190000 53000 442 469 4300 190000 53000 426 469 38000 140000 440000 790 469 71000 880000 640000 737 469 33000   250000 310000 807 469 15000 400000 150000 531 469 110000 470000 1000000 688 469 24000   42000 270000 459 469 110000 530000 970000 635 469 93000 540000 890000 438 469 110000 540000 940000 635 469 56000 550000 530000 823 469 370000   81000 4800000 43
    correct results 378 2700    29000 28000   721 420 6100   18000 63000 800 417 7900 17000 83000 792 401 11000 290000 94000 761 36 980 3300 12000 36 226 2300 86000 28000 442 218 2200 83000 27000 426 432 7600 30000 93000 822 395 20000 660000 170000 753 422 1500   31000 18000 807 315 3800 150000 34000 611 348 25000 180000 240000 688 236 55   4500 660 459 330 30000 300000 280000 635 225 31000 220000 290000 438 330 31000 310000 290000 635 430 32000 390000 300000 823 43 910   7000 11000 43
        correct true 343 2500    26000 26000   686 380 5200   16000 54000 760 375 7300 15000 77000 750 360 8400 260000 75000 720 0 216 2200 82000 27000 432 208 2200 79000 26000 416 390 6600 26000 80000 780 358 17000 610000 150000 716 385 1300   29000 16000 770 296 3600 140000 32000 592 340 25000 180000 240000 680 223 52   4200 640 446 305 27000 290000 260000 610 213 31000 220000 280000 426 305 28000 290000 260000 610 393 30000 370000 290000 786 0
        correct false 35 200    2500 2200   35 40 850   2200 8800 40 42 640 1900 6300 42 41 2300 27000 19000 41 36 980 3300 12000 36 10 83 4300 1100 10 10 83 4300 1100 10 42 1100 4100 14000 42 37 2600 49000 21000 37 37 250   2600 2900 37 19 290 13000 2600 19 8 37 820 420 8 13 2.3 210 26 13 25 2600 16000 21000 25 12 220 5200 1900 12 25 2600 16000 23000 25 37 1800 13000 15000 37 43 910   7000 11000 43
    correct-unconfimed results 1 .38 38 3.9 0 3 3.7 73 44 0 0 0 0 0 0 0 3 97 4100 700 0 2 2.5 130 32 0 1 28 2800 230 0 15 3400 8600 31000 0 0 10 1200 7600 9700 0 2 350 2900 2800 0 10 1100 7600 8900 0 6 590 2500 4800 0 1 9.5 180 100 0
        correct-unconfirmed true 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        correct-unconfirmed false 1 .38 38 3.9 0 3 3.7 73 44 0 0 0 0 0 0 0 3 97 4100 700 0 2 2.5 130 32 0 1 28 2800 230 0 15 3400 8600 31000 0 0 10 1200 7600 9700 0 2 350 2900 2800 0 10 1100 7600 8900 0 6 590 2500 4800 0 1 9.5 180 100 0
    incorrect results 0 0 0 0 0 0 0 1 450 530 4300 -32 1 18 1300 150 -16 0 5 34 1700 290 -80 0 0 0 0 0 0 0
        incorrect true 0 0 0 0 0 0 0 1 450 530 4300 -32 0 0 0 0 0 0 0 0 0 0
        incorrect false 0 0 0 0 0 0 0 0 1 18 1300 150 -16 0 5 34 1700 290 -80 0 0 0 0 0 0 0
score (469 tasks, max score: 893) 721 800 792 761 36 442 426 790 737 807 531 688 459 635 438 635 823 43
Run set 2ls.sv-comp19_prop-reachsafety.ReachSafety-Floats cbmc.sv-comp19_prop-reachsafety.ReachSafety-Floats cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Floats depthk.sv-comp19_prop-reachsafety.ReachSafety-Floats divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-Floats divine-smt.sv-comp19_prop-reachsafety.ReachSafety-Floats esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Floats pesco.sv-comp19_prop-reachsafety.ReachSafety-Floats pinaka.sv-comp19_prop-reachsafety.ReachSafety-Floats skink.sv-comp19_prop-reachsafety.ReachSafety-Floats smack.sv-comp19_prop-reachsafety.ReachSafety-Floats symbiotic.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer.sv-comp19_prop-reachsafety.ReachSafety-Floats ukojak.sv-comp19_prop-reachsafety.ReachSafety-Floats utaipan.sv-comp19_prop-reachsafety.ReachSafety-Floats veriabs.sv-comp19_prop-reachsafety.ReachSafety-Floats verifuzz.sv-comp19_prop-reachsafety.ReachSafety-Floats