Tool 2LS 0.6.0 CBMC 5.8 CPAchecker 1.6.1-svn 26725 CPAchecker 1.6.1-svn 26758M CPAchecker 1.6.1-svn 26773 DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 ESBMC ESBMC version 4.6.0 64-bit x86_64 linux CPAchecker skink symbiotic 5.0.0-KLEE:1faddfe0-dg:12c34aac-symbiotic:5e14b94d-minisat:3db58943-llvm-instrumentation:cd767593-stp:17249213 ULTIMATE Automizer 0.1.23-3204b741 ULTIMATE Kojak 0.1.23-3204b741 ULTIMATE Taipan 0.1.23-3204b741 VeriAbs
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-11-30 11:20:26 CET 2017-11-30 16:01:31 CET 2017-12-01 08:49:27 CET 2017-12-01 12:59:33 CET 2017-12-01 19:00:34 CET 2017-12-01 22:03:39 CET 2017-12-01 22:41:19 CET 2017-12-02 01:06:24 CET 2017-12-02 02:33:02 CET 2017-12-02 17:23:13 CET 2017-12-02 18:04:04 CET
Run set 2ls.sv-comp18.ReachSafety-Floats cbmc.sv-comp18.ReachSafety-Floats cpa-bam-bnb.sv-comp18.ReachSafety-Floats cpa-bam-slicing.sv-comp18.ReachSafety-Floats cpa-seq.sv-comp18.ReachSafety-Floats depthk.sv-comp18.ReachSafety-Floats esbmc-incr.sv-comp18.ReachSafety-Floats esbmc-kind.sv-comp18.ReachSafety-Floats interpchecker.sv-comp18.ReachSafety-Floats skink.sv-comp18.ReachSafety-Floats symbiotic.sv-comp18.ReachSafety-Floats uautomizer.sv-comp18.ReachSafety-Floats ukojak.sv-comp18.ReachSafety-Floats utaipan.sv-comp18.ReachSafety-Floats veriabs.sv-comp18.ReachSafety-Floats
Options --graphml-witness witness.graphml --graphml-witness witness.graphml -svcomp18-bam-bnb -disable-java-assertions -heap 10000m -ldv-bam-svcomp -disable-java-assertions -heap 10000m -svcomp18 -heap 10000M -benchmark -timelimit 900s -s incr -s kinduction -sv-comp18-interpcpachecker -heap 10000M -disable-java-assertions --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
floats-cdfpl/newton_1_4_false-unreach-call_true-termination.i 4.3   56 42    1 3.1  59 31   1 3.5 290 31 1 33   390 240 0 51   350 370 1 890    400 7500   0 8.6   190 74    1 8.4   190 89    1 3.1 270 29 1 7.4 350 71 1 .16  11 1.9  0 43   690 390 1 100   1200 750 0 43   700 320 1 120   380 1100 1
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i 5.2   56 57    1 1.9  58 28   1 3.8 290 36 1 49   390 350 0 21   350 160 1 890    480 8000   0 6.8   190 81    1 6.8   190 55    1 3.0 270 28 0 7.1 360 62 1 .18  11 1.9  0 120   740 1100 1 94   1100 700 0 120   720 1100 1 75   380 650 1
floats-cdfpl/newton_1_6_false-unreach-call_true-termination.i 2.8   55 29    1 4.9  61 54   1 3.7 290 35 1 12   390 120 0 18   360 130 1 890    400 7900   0 2.9   180 29    1 2.9   180 28    1 2.9 270 25 1 7.1 340 73 1 .16  11 2.0  0 20   680 180 1 96   1100 830 0 20   680 170 1 87   380 850 1
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i 1.1   53 14    1 3.5  60 29   1 3.7 290 33 1 12   390 98 0 48   360 340 1 890    400 8700   0 10     190 100    1 10     190 91    1 2.9 260 30 1 10   350 97 1 .18  11 1.8  0 40   690 280 1 99   1100 780 0 40   700 400 1 64   380 650 1
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i 3.8   54 38    1 3.5  60 37   1 3.6 290 29 1 13   380 110 0 11   350 83 1 890    460 7500   0 7.5   190 66    1 7.4   190 64    1 3.0 280 28 1 6.8 360 59 1 .16  11 2.0  0 27   680 230 1 96   1200 660 0 26   690 270 1 41   380 400 1
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i 7.6   110 84    1 22    130 190   1 4.1 310 34 1 40   490 350 0 14   450 120 1 890    710 8400   0 16     340 130    1 16     340 140    1 3.4 290 28 0 15   350 170 0 .19  11 2.1  0 900   1100 7200 0 55   1500 460 0 900   1100 6400 0 900   230 13000 0
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i 4.1   92 47    1 28    140 260   1 3.9 310 37 1 40   490 340 0 70   460 470 1 890    700 9200   0 16     350 130    1 16     350 170    1 3.3 280 29 0 13   370 120 1 .16  11 1.8  0 130   860 1000 0 48   1400 550 0 130   860 1000 1 900   230 13000 0
floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i 12     100 120    1 4.7  91 36   1 3.8 290 32 1 14   480 140 0 15   450 120 1 890    760 8100   0 12     350 110    1 12     350 95    1 3.2 280 28 1 12   340 140 1 .16  11 1.8  0 27   840 240 1 69   1600 550 0 28   830 240 1 900   230 11000 0
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i 83     220 1100    1 50    220 600   1 4.4 320 35 0 120   600 1100 0 630   1100 4700 1 890    1000 9100   0 18     510 150    1 18     510 180    1 3.8 300 28 0 18   360 190 0 .18  11 1.9  0 900   1000 8700 0 71   2000 650 0 900   1000 6000 0 900   230 11000 0
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i 50     220 440    1 43    220 420   1 4.5 320 44 0 43   590 300 0 340   570 2400 1 890    1000 8100   0 170     520 1200    1 160     520 1200    1 3.7 300 32 0 18   370 200 0 .18  11 1.7  0 160   920 1200 0 58   2000 560 0 160   930 1200 0 900   230 12000 0
floats-cdfpl/newton_3_8_false-unreach-call_true-termination.i 29     190 250    1 29    180 260   1 4.4 310 34 1 18   590 150 0 17   560 140 1 890    1100 6900   0 11     510 100    1 11     510 100    1 3.7 290 32 0 17   370 190 0 .17  11 1.9  0 260   990 1700 0 57   2000 480 0 260   1000 1800 0 900   230 12000 0
floats-cdfpl/sine_1_false-unreach-call_true-termination.i .49  38 5.2  1 1.3  43 17   1 3.6 280 32 1 24   360 190 1 7.4 300 61 1 190    240 1600   1 5.2   130 67    1 5.7   130 48    1 2.9 280 28 1 5.7 330 52 0 .19  11 1.8  0 19   570 170 1 49   660 370 0 19   580 170 1 19   340 230 1
floats-cdfpl/sine_2_false-unreach-call_true-termination.i .64  38 9.0  1 .75 42 8.1 1 3.4 280 30 1 4.0 350 36 1 37   330 320 1 97    200 970   1 2.9   130 27    1 2.8   130 27    1 2.9 270 26 1 7.2 340 71 1 .16  11 2.0  0 23   570 240 1 51   620 460 0 23   570 230 1 51   370 460 1
floats-cdfpl/sine_3_false-unreach-call_true-termination.i .30  38 3.0  1 1.8  49 22   1 3.4 280 31 1 480   570 3900 0 6.0 300 48 1 65    180 620   1 5.6   130 57    1 5.9   130 58    1 3.0 280 25 0 7.0 360 61 0 .16  11 2.0  0 900   870 6300 0 51   620 430 0 900   900 7100 0 220   450 1800 1
floats-cdfpl/square_1_false-unreach-call_true-termination.i 1.3   38 16    1 1.0  42 14   1 3.6 290 29 1 12   360 110 0 44   360 390 1 570    210 4500   1 3.1   130 31    1 3.1   130 35    1 2.8 270 27 0 6.3 400 53 1 .18  11 1.6  0 160   500 1300 0 32   380 250 0 160   500 1400 0 32   350 400 1
floats-cdfpl/square_2_false-unreach-call_true-termination.i 1.1   37 13    1 1.2  43 15   1 3.6 290 31 1 170   490 1400 1 210   510 1600 1 890    250 9000   0 2.9   130 40    1 2.9   130 30    1 3.1 270 23 0 6.4 400 64 1 .16  11 1.5  0 81   430 620 0 28   380 210 0 77   440 890 1 200   510 1600 1
floats-cdfpl/square_3_false-unreach-call_true-termination.i .95  38 11    1 1.2  42 17   0 3.6 290 29 1 46   400 400 0 90   390 710 1 890    350 6400   0 3.3   130 37    1 3.5   130 32    1 3.0 280 25 0 5.6 310 51 1 .18  11 2.0  0 820   930 5800 0 35   380 360 0 830   930 6600 0 71   360 590 1
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i 8.3   73 78    2 18    65 180   2 3.6 290 32 -16 900   620 6500 0 900   720 6000 0 890    410 8900   0 23     200 180    2 23     200 190    2 2.9 260 29 -16 7.9 350 77 2 .19  11 2.1  0 900   1100 5700 0 110   1200 760 0 900   1100 5600 0 900   230 12000 0
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i 10     70 95    2 14    72 200   2 3.8 290 30 -16 900   820 6100 0 900   810 7500 0 890    400 8300   0 48     210 420    2 46     210 470    2 2.9 270 26 -16 7.6 330 67 2 .18  11 1.7  0 900   1000 6600 0 100   1100 750 0 900   1000 6100 0 190   380 2700 2
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i 10     73 120    2 22    66 240   2 3.6 290 36 -16 900   760 6300 0 900   620 6400 0 890    400 8800   0 46     210 380    2 45     210 370    2 2.9 280 25 -16 8.3 360 78 2 .18  11 1.7  0 900   930 5500 0 93   1200 760 0 900   920 6000 0 900   230 12000 0
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i 33     150 400    2 48    130 470   2 3.8 300 38 -16 900   700 6800 0 900   550 6200 0 890    680 8600   0 74     380 610    2 75     390 610    2 3.4 290 32 -16 21   350 230 2 .18  11 2.3  0 900   1000 8000 0 66   1400 750 0 900   1000 7500 0 900   230 13000 0
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i 28     140 230    2 55    140 600   2 3.9 290 32 -16 900   640 8200 0 900   1000 6200 0 890    700 9100   0 90     390 1000    2 91     390 610    2 3.4 280 29 -16 20   380 200 2 .19  11 1.7  0 900   1000 6400 0 67   1500 560 0 900   1000 5300 0 900   230 14000 0
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i 23     130 170    2 68    150 740   2 3.9 280 33 -16 900   750 6400 0 900   560 5700 0 890    710 9300   0 79     390 580    2 81     380 470    2 3.4 290 30 -16 15   350 170 2 .19  11 1.8  0 900   950 5800 0 62   1400 510 0 900   980 6100 0 900   230 9900 0
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i 44     140 480    2 47    130 700   2 4.1 310 36 -16 900   630 6800 0 900   650 6700 0 890    710 9500   0 88     380 840    2 91     380 700    2 3.3 280 26 -16 18   400 180 0 .17  11 2.4  0 900   1000 6100 0 59   1500 560 0 900   1000 7000 0 900   230 10000 0
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i 60     140 580    2 75    140 790   2 3.9 290 32 -16 900   630 6300 0 900   640 6900 0 890    760 8400   0 410     430 3200    2 400     430 2800    2 3.0 280 27 -16 18   400 220 0 .16  11 2.1  0 900   1000 6700 0 61   1500 520 0 900   1000 7900 0 900   230 12000 0
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i 69     200 680    2 120    190 1000   2 4.6 330 35 -16 900   630 5600 0 900   910 7700 0 890    1000 10000   0 190     610 2000    2 190     610 1500    2 3.5 280 29 -16 23   370 280 0 .18  11 2.0  0 900   1100 6000 0 66   2000 520 0 900   1100 6800 0 900   230 11000 0
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i 69     220 600    2 140    220 1400   2 4.6 330 40 -16 900   720 6200 0 900   670 5700 0 890    1000 9000   0 650     680 4400    2 670     680 4700    2 3.5 270 32 -16 19   380 190 0 .19  11 1.8  0 900   1100 7800 0 70   2000 590 0 900   1100 5600 0 900   230 10000 0
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i 98     220 850    2 160    220 1500   2 4.4 330 40 -16 900   720 6500 0 900   790 6300 0 890    930 8900   0 240     620 1600    2 250     610 2200    2 3.4 280 31 -16 21   380 250 0 .16  11 1.7  0 900   1200 6000 0 72   1900 790 0 900   1200 6800 0 900   230 12000 0
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i 81     220 790    2 120    220 1000   2 4.6 320 31 -16 900   820 6500 0 900   810 6100 0 890    990 9900   0 470     680 4700    2 450     670 3300    2 3.6 300 32 -16 17   370 190 0 .18  11 2.1  0 900   1100 5800 0 58   2000 450 0 900   1100 5800 0 900   230 11000 0
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i 90     220 890    2 110    220 1400   2 4.5 320 39 -16 900   680 6000 0 900   700 6500 0 890    1200 7700   0 500     640 3300    2 470     640 3500    2 3.5 270 32 -16 18   370 190 0 .18  11 1.8  0 900   1100 6600 0 60   2000 530 0 900   1100 6200 0 900   230 12000 0
floats-cdfpl/sine_4_true-unreach-call_true-termination.i 25     55 330    2 69    55 870   2 3.5 290 34 -16 900   590 8500 0 900   660 7500 0 890    310 10000   0 130     180 970    2 130     180 1000    2 2.9 280 28 -16 6.9 350 68 2 .16  11 2.1  0 900   860 6700 0 51   630 460 0 900   870 5600 0 900   160 11000 0
floats-cdfpl/sine_5_true-unreach-call_true-termination.i 2.0   41 24    2 5.6  48 69   2 3.6 280 30 -16 900   540 5900 0 900   750 9200 0 890    310 9900   0 19     140 170    2 18     140 200    2 2.9 280 24 -16 6.7 310 57 2 .16  11 1.9  0 900   930 6200 0 49   650 360 0 900   980 8600 0 900   160 11000 0
floats-cdfpl/sine_6_true-unreach-call_true-termination.i 1.7   38 23    2 3.2  44 41   2 3.5 280 29 -16 290   490 2900 0 900   900 7100 0 890    320 7000   0 6.7   130 85    2 7.0   130 68    2 2.9 270 26 -16 7.2 350 69 2 .19  11 1.8  0 900   840 6200 0 51   640 430 0 900   840 6100 0 200   370 2700 2
floats-cdfpl/sine_7_true-unreach-call_true-termination.i 1.4   40 17    2 3.5  49 40   2 3.5 280 35 -16 750   600 5400 0 900   820 7200 0 890    310 8100   0 6.7   130 76    2 6.7   130 90    2 2.9 280 25 -16 7.5 340 63 2 .16  11 1.8  0 900   810 6700 0 48   640 360 0 900   800 7100 0 120   360 1500 2
floats-cdfpl/sine_8_true-unreach-call_true-termination.i 1.3   39 16    2 3.0  46 34   2 3.6 280 33 -16 900   560 6800 0 780   690 6800 2 890    310 8400   0 5.4   130 57    2 5.3   130 57    2 3.0 260 27 -16 6.3 320 54 2 .16  11 2.1  0 900   860 7500 0 50   660 400 0 900   890 5500 0 900   160 11000 0
floats-cdfpl/square_4_true-unreach-call_true-termination.i 200     68 2600    2 140    63 2100   2 3.5 280 31 -16 900   680 6500 0 700   710 5300 2 890    250 7700   0 120     160 1100    2 130     160 980    2 2.9 280 29 -16 6.4 350 58 2 .18  11 1.8  0 610   820 5800 2 39   370 300 0 620   840 4200 2 900   150 14000 0
floats-cdfpl/square_5_true-unreach-call_true-termination.i 680     170 8900    2 120    63 1500   2 3.6 290 30 -16 660   630 5000 0 620   610 5100 2 890    350 8900   0 110     150 870    2 110     150 780    2 3.0 280 27 -16 6.1 330 56 2 .16  11 1.7  0 450   780 3500 2 31   380 270 0 450   770 4000 2 900   160 12000 0
floats-cdfpl/square_6_true-unreach-call_true-termination.i 62     63 810    2 13    49 140   2 3.4 280 34 -16 310   540 2500 0 440   610 3400 2 890    260 6600   0 21     130 240    2 22     130 180    2 2.9 270 29 -16 6.0 320 54 2 .16  11 2.1  0 330   840 2400 2 34   380 240 0 330   830 2200 2 900   160 13000 0
floats-cdfpl/square_7_true-unreach-call_true-termination.i 9.3   59 120    2 17    50 190   2 3.7 290 28 -16 400   490 2800 0 900   610 6000 0 890    350 11000   0 27     130 320    2 30     130 300    2 3.0 280 26 -16 6.6 330 54 2 .16  11 1.6  0 150   720 1300 2 32   370 250 0 160   740 1200 2 900   160 13000 0
floats-cdfpl/square_8_true-unreach-call_true-termination.i .72  38 10    2 1.6  43 19   2 3.5 280 28 -16 9.5 350 85 0 280   500 2800 2 890    200 9900   0 2.7   120 30    2 2.7   120 30    2 2.9 270 23 -16 6.3 340 49 2 .17  11 2.0  0 110   630 820 2 42   380 320 0 110   650 830 2 52   370 480 2
floats-cbmc-regression/float-div1_true-unreach-call.i .30  38 3.0  2 1.2  43 11   2 5.1 310 42 -16 3.6 320 36 0 10   550 86 2 37    370 370   2 1.2   110 12    2 1.2   110 13    2 4.3 290 34 -16 5.0 290 49 0 .17  11 2.1  0 31   670 310 2 110   560 1100 0 31   680 280 2 170   450 2100 2
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i .94  130 11    2 1.3  47 13   2 6.3 330 51 -16 1.8 130 18 0 7.4 410 58 2 25    2000 220   2 .13  29 1.4  2 .12  29 1.3  2 4.1 290 36 -16 4.9 300 45 0 .18  12 1.9  0 27   700 260 2 17   530 150 2 28   720 240 2 610   260 6700 0
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i .094 22 .85 2 .40 33 3.6 2 2.8 270 25 2 2.7 270 27 2 2.6 270 22 2 3.1  270 33   2 .10  26 .69 2 .070 26 .79 2 2.8 270 25 -16 3.7 230 32 2 .12  11 1.3  2 8.5 280 63 2 8.7 260 76 2 8.7 290 77 2 8.1 270 66 2
floats-cbmc-regression/float-no-simp2_true-unreach-call.i .72  33 9.3  2 3.0  39 34   2 3.6 280 32 2 3.1 270 27 2 11   310 140 2 300    330 3000   2 2.2   71 27    2 2.2   71 26    2 3.8 290 36 2 3.5 260 32 0 .17  11 1.7  0 40   440 460 2 31   360 420 0 40   450 550 2 180   450 2600 2
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i .096 23 .92 2 .41 33 3.5 2 2.7 270 23 2 2.8 270 26 2 2.6 270 23 2 3.2  260 30   2 .087 26 .80 2 .093 26 .80 2 2.8 270 23 -16 3.8 230 34 2 .14  11 1.4  2 8.4 270 73 2 8.9 260 73 2 8.4 270 76 2 8.0 270 67 2
floats-cbmc-regression/float-no-simp4_true-unreach-call.i .31  36 3.8  2 1.1  39 9.7 2 5.0 320 45 -16 3.6 290 34 0 5.0 300 42 2 6.3  310 66   2 .21  30 2.1  2 .18  30 2.1  2 900   8100 11000 0 4.7 310 43 0 .20  11 1.8  0 31   550 340 2 17   500 160 2 39   560 480 2 17   370 150 2
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i .089 23 .71 2 .39 33 4.3 2 2.9 270 28 2 2.9 270 26 2 2.4 240 19 2 3.2  250 28   2 .10  26 .83 2 .11  26 .63 2 2.7 270 23 -16 3.7 240 33 2 .15  11 1.3  2 9.3 300 85 2 11   340 96 2 9.2 310 84 2 7.8 280 64 2
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i .080 22 .99 2 .43 33 3.7 2 2.9 270 27 2 2.8 270 26 2 2.3 250 20 2 3.1  260 33   2 .095 26 .84 2 .10  26 .63 2 2.7 260 24 -16 3.6 230 33 2 .14  11 1.5  2 8.5 290 68 2 9.2 250 77 2 8.6 290 73 2 7.9 270 68 2
floats-cbmc-regression/float-no-simp8_true-unreach-call.i .19  28 1.5  2 .90 37 8.6 2 3.5 280 31 2 2.8 270 26 2 2.9 260 27 2 4.3  260 39   2 .12  27 .69 2 .085 27 .74 2 3.6 280 34 2 3.9 240 38 2 .19  11 2.2  2 9.1 310 70 2 9.7 290 78 2 9.6 320 79 2 15   280 140 2
floats-cbmc-regression/float-rounding1_true-unreach-call.i .21  28 1.5  2 .90 39 8.4 2 3.3 280 33 0 2.8 270 23 2 6.3 440 57 0 9.1  450 82   0 .21  32 2.3  2 .20  32 2.6  2 3.2 280 26 0 4.1 270 41 0 .13  11 1.5  0 3.7 220 30 0 3.7 230 27 0 3.8 230 33 0 170   370 2500 2
floats-cbmc-regression/float-to-double1_true-unreach-call.i .24  28 1.9  2 .95 37 10   2 3.7 280 27 2 2.8 270 26 2 4.9 300 40 2 29    320 350   2 .22  31 2.6  2 .24  31 2.4  2 3.5 280 34 2 3.8 240 37 0 .17  11 1.8  0 100   510 1200 2 17   280 200 2 82   490 910 2 170   300 2000 2
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i .089 22 .64 2 .39 33 3.8 2 2.7 270 25 2 2.9 270 24 2 2.3 230 21 2 3.1  260 32   2 .079 26 .67 2 .11  26 .68 2 2.8 280 22 2 3.7 230 38 2 .14  10 1.5  2 8.2 280 63 2 8.7 260 79 2 8.5 280 69 2 8.3 280 82 2
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i .11  22 .73 2 .38 33 5.1 2 3.0 270 27 2 2.8 270 27 2 2.5 250 24 2 3.1  260 30   2 .13  28 1.6  2 .14  28 1.5  2 2.7 270 28 -16 3.8 240 35 2 .15  11 1.4  2 9.8 300 76 2 9.1 250 69 2 9.3 290 78 2 9.1 270 80 2
floats-cbmc-regression/float11_true-unreach-call_true-termination.i .11  22 .82 2 .40 33 3.8 2 2.8 270 22 2 2.7 270 25 2 2.3 250 19 2 3.4  250 33   2 .12  27 1.0  2 .090 27 .94 2 2.8 270 23 2 3.4 320 40 2 .12  11 1.3  2 8.8 280 72 2 9.7 310 72 2 8.8 290 81 2 8.3 280 70 2
floats-cbmc-regression/float12_true-unreach-call_true-termination.i .10  22 .66 2 .43 33 3.5 2 2.8 270 26 2 2.8 270 24 2 2.9 270 28 2 7.7  290 85   2 .21  31 2.4  2 .18  32 2.4  2 2.7 270 22 2 5.7 310 48 0 .18  11 1.8  0 13   310 150 2 14   280 140 2 13   310 140 2 8.0 270 69 2
floats-cbmc-regression/float13_true-unreach-call_true-termination.i .12  24 1.0  2 .44 33 3.9 2 2.8 270 26 2 2.8 270 25 2 2.4 250 23 2 3.2  250 27   2 .077 26 .74 2 .10  26 .90 2 2.8 270 24 -16 3.8 240 38 2 .12  11 1.6  2 9.2 290 82 2 11   350 100 2 9.3 290 74 2 8.5 280 81 2
floats-cbmc-regression/float14_true-unreach-call.i .17  28 1.9  2 .90 37 7.8 2 3.7 280 36 2 2.8 270 27 2 3.1 260 25 2 4.3  270 40   2 .12  27 .88 2 .079 27 1.0  2 3.9 290 36 -16 3.6 240 32 0 .19  11 1.9  0 9.3 300 84 2 9.9 300 79 2 9.1 310 83 2 15   280 120 2
floats-cbmc-regression/float18_true-unreach-call.i 900     1700 10000    0 2.6  38 27   2 4.1 280 33 2 3.1 270 26 2 3.0 250 28 2 18    270 270   2 .23  27 2.1  2 .12  27 .98 2 7.7 460 57 2 3.8 240 33 2 .18  11 2.0  2 3.7 220 29 0 3.8 230 32 0 3.8 220 31 0 39   710 360 2
floats-cbmc-regression/float19_true-unreach-call.i .19  28 1.4  2 .91 37 9.0 2 5.3 320 40 -16 3.0 280 27 0 4.6 300 43 2 7.3  300 78   2 .15  29 2.3  2 .15  28 1.9  2 3.8 290 35 -16 3.7 250 34 0 .18  11 1.8  0 10   290 97 2 9.8 270 84 2 10   290 96 2 20   290 150 2
floats-cbmc-regression/float1_true-unreach-call_true-termination.i .11  22 .52 2 .39 33 4.2 2 2.7 270 27 2 2.8 270 27 2 2.5 260 19 2 3.1  260 30   2 .10  26 .75 2 .099 26 .78 2 2.7 270 24 -16 3.6 230 32 2 .12  11 1.3  2 8.6 280 78 2 8.4 260 77 2 8.5 280 77 2 7.8 270 70 2
floats-cbmc-regression/float20_true-unreach-call_true-termination.i .14  26 1.2  2 .42 35 5.6 2 2.9 270 28 2 2.9 270 29 2 2.4 250 24 2 24    250 270   2 .36  52 4.7  2 .36  52 4.4  2 2.9 280 23 -16 6.2 330 57 -16 .19  11 2.1  0 14   390 120 2 39   490 370 2 13   390 140 2 10   270 90 2
floats-cbmc-regression/float21_true-unreach-call.i .27  30 2.6  2 1.1  39 12   2 4.9 300 39 -16 3.2 280 26 0 5.1 300 49 2 30    310 370   2 .29  35 3.5  2 .28  35 2.9  2 3.8 290 31 -16 4.1 270 39 0 .18  11 1.8  0 68   580 740 2 63   630 730 2 62   600 660 2 170   570 2100 2
floats-cbmc-regression/float22_true-unreach-call_true-termination.i .11  23 .86 2 .44 33 4.0 2 3.5 290 29 0 3.0 290 28 0 4.7 300 39 -16 18    51 260   0 .60  58 7.2  2 .56  58 7.3  2 2.9 260 25 -16 3.8 250 37 2 .15  11 1.4  2 280   1100 2900 2 900   1000 9800 0 65   690 690 2 12   320 100 2
floats-cbmc-regression/float2_true-unreach-call_true-termination.i .095 22 .93 2 .40 33 4.8 2 2.7 270 25 2 2.7 270 22 2 2.3 250 23 2 3.2  240 28   2 .16  26 1.3  2 .12  26 1.3  2 3.0 270 27 2 3.6 230 32 2 .15  11 1.3  2 8.8 300 67 2 8.9 260 75 2 9.1 310 74 2 7.9 270 74 2
floats-cbmc-regression/float3_true-unreach-call_true-termination.i .11  24 1.1  2 .44 33 4.0 2 3.3 280 34 0 2.8 270 24 2 2.3 240 21 2 7.5  250 85   2 .39  56 4.7  2 .43  56 5.0  2 2.9 280 27 -16 5.9 310 47 2 .18  11 1.6  0 12   350 110 2 13   300 120 2 12   340 130 2 8.6 290 83 2
floats-cbmc-regression/float4_true-unreach-call.i 11     45 130    2 14    49 170   2 3.8 270 34 2 3.2 270 27 2 27   330 340 2 310    590 3400   2 7.4   110 87    2 7.4   110 100    2 3.9 280 30 2 3.9 270 35 0 .17  11 1.9  0 74   490 960 2 64   410 770 0 73   480 880 2 250   480 3000 2
floats-cbmc-regression/float5_true-unreach-call_true-termination.i .12  23 .77 2 .42 33 4.8 2 2.7 270 23 2 2.7 270 25 2 2.4 260 20 2 16    260 240   2 .24  31 2.2  2 .22  31 2.9  2 2.9 280 28 2 6.8 330 63 2 .17  11 1.9  0 21   320 230 2 28   280 300 2 21   320 220 2 8.7 280 78 2
floats-cbmc-regression/float6_true-unreach-call_true-termination.i .099 23 1.1  2 .43 33 4.2 2 3.0 280 29 2 3.0 270 30 2 2.5 250 22 2 3.5  260 34   2 .16  29 2.1  2 .19  29 2.0  2 3.1 260 30 2 6.1 300 50 0 .16  11 2.1  0 9.5 300 79 2 14   470 140 2 10   300 85 2 8.6 280 69 2
floats-cbmc-regression/float8_true-unreach-call.i .55  30 5.7  2 1.4  37 14   2 3.9 300 37 2 2.8 270 26 2 14   300 150 2 7.5  340 81   2 .64  38 7.9  2 .66  38 7.6  2 3.7 280 31 2 4.7 280 38 0 .17  11 2.1  0 10   310 82 2 8.4 260 72 2 10   310 90 2 170   300 2200 2
floats-cbmc-regression/float_lib1_true-unreach-call.i 6.6   34 72    2 1.1  39 9.5 2 1.7 140 15 0 1.6 130 14 0 1.7 130 16 0 3.9  150 47   0 .70  27 6.6  2 .72  27 7.4  2 1.8 130 17 0 3.2 210 32 0 .18  11 1.6  0 8.1 250 68 0 9.1 260 70 0 8.1 260 68 0 12   190 110 2
floats-cbmc-regression/float_lib2_true-unreach-call.i .24  29 2.0  2 1.0  38 11   2 4.2 310 36 2 3.2 270 30 2 2.9 250 24 2 4.4  260 43   2 .11  27 .99 2 .095 27 .91 2 3.8 280 34 -16 4.1 250 37 0 .16  11 2.2  0 13   490 120 2 19   570 190 2 13   500 110 2 16   310 130 2
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c .095 22 .72 0 .25 33 2.3 1 3.6 280 28 1 3.5 280 32 1 2.8 260 26 1 .41 48 4.8 0 .66  42 5.6  1 .61  42 5.6  1 2.4 260 24 0 5.0 290 44 0 .15  11 1.6  1 9.1 270 77 1 11   290 100 1 12   350 110 1 11   290 100 1
float-benchs/cast_union_loose_false-unreach-call_true-termination.c .13  26 1.2  1 .26 33 2.7 1 4.0 310 33 1 3.6 300 32 0 3.4 270 30 1 .51 49 5.5 1 1.2   51 8.5  1 1.2   51 9.9  1 2.9 260 28 1 5.6 320 44 0 .18  11 1.8  1 9.2 280 87 1 11   270 97 1 9.6 290 85 1 11   290 92 1
float-benchs/cast_union_tight_false-unreach-call_true-termination.c .15  24 1.1  1 .29 34 2.2 1 3.5 290 31 1 3.2 290 29 0 3.1 280 29 1 1.2  48 14   1 1.2   51 12    1 1.2   51 12    1 2.7 270 22 1 5.1 310 41 0 .15  11 1.8  0 9.4 290 87 1 15   290 140 1 9.7 290 79 1 12   290 94 1
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c .17  27 1.2  1 .28 34 2.4 1 3.4 280 31 1 3.4 300 27 1 2.6 260 25 1 17    66 220   1 .35  42 3.9  1 .33  42 3.7  1 2.9 270 24 1 6.0 320 48 0 .20  14 1.8  1 8.6 310 67 1 11   300 110 1 8.7 300 80 1 7.4 290 70 1
float-benchs/inv_Newton_false-unreach-call.c 900     820 6800    0 870    250 6800   0 4.2 320 37 0 4.3 370 41 0 3.8 350 38 1 890    340 7300   0 900     1300 6000    0 900     1100 6300    0 900   4200 11000 0 5.7 310 57 0 .17  11 2.2  0 900   1800 5800 0 64   420 580 0 900   1700 6300 0 110   220 1400 0
float-benchs/inv_square_false-unreach-call_true-termination.c .17  27 1.1  1 .26 35 2.2 1 3.5 290 32 1 3.4 300 33 1 2.6 260 23 1 .46 40 5.6 1 .32  38 3.3  1 .30  39 3.0  1 2.9 260 25 1 5.4 310 51 0 .16  11 2.0  0 8.5 310 70 1 9.0 280 86 1 8.6 310 75 1 7.5 290 61 1
float-benchs/nan_double_false-unreach-call_true-termination.c .10  22 1.0  1 .23 33 2.2 1 2.9 270 26 -32 2.8 270 24 -32 2.5 250 20 1 .36 48 4.8 0 .20  31 2.4  1 .20  32 2.0  1 2.8 270 26 -32 4.9 290 42 0 .18  11 1.6  1 4.1 240 34 1 8.1 250 68 1 4.1 240 34 1 7.3 270 70 1
float-benchs/nan_float_false-unreach-call_true-termination.c .11  22 .88 1 .25 33 2.2 1 2.8 270 24 -32 2.7 270 24 -32 2.6 250 22 1 .35 48 5.0 0 .21  31 1.9  1 .20  31 1.8  1 2.8 280 25 -32 4.6 290 46 0 .15  11 1.7  1 4.0 240 31 1 8.0 250 70 1 4.1 240 35 1 7.4 280 65 1
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c 3.2   260 34    1 2.7  240 30   1 4.0 300 39 1 3.3 280 30 0 7.4 380 76 1 110    410 1100   1 5.5   320 63    0 5.7   320 51    0 3.3 270 30 1 8.4 480 75 0 .20  11 1.9  0 370   2100 4100 1 32   2500 230 0 640   2500 6300 1 32   350 400 1
float-benchs/sqrt_poly2_false-unreach-call.c .64  46 6.6  1 .72 50 7.5 1 4.0 290 34 1 6.3 470 58 1 5.4 390 55 1 290    340 2800   1 5.4   280 46    1 5.4   280 55    1 3.0 270 26 1 6.4 330 51 0 .16  11 1.9  0 15   600 120 1 92   700 730 0 15   610 130 1 22   450 220 1
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c 900     610 6500    0 3.0  33 36   2 110   3700 1200 0 630   15000 8500 0 3.3 260 31 2 890    1200 6700   0 .66  26 7.3  2 4.2   260 42    2 81   3700 880 -16 5.6 310 51 0 .16  11 1.4  2 900   3400 10000 0 900   1900 9800 0 900   7300 11000 0 79   1000 880 2
float-benchs/Rump_double_true-unreach-call_true-termination.c .15  27 1.1  2 .41 33 3.8 2 2.7 270 26 2 2.8 270 26 2 2.3 250 18 2 3.3  300 30   2 .077 26 .84 2 .11  26 .67 2 2.8 280 22 -16 4.0 250 38 2 .14  11 1.4  2 19   1000 200 2 22   1500 220 0 20   990 190 2 8.1 280 58 2
float-benchs/Rump_float_true-unreach-call_true-termination.c .12  24 .88 2 .43 33 3.6 2 2.7 270 24 2 2.8 270 27 2 2.4 250 21 2 3.1  270 29   2 .085 26 .78 2 .11  26 .64 2 2.8 280 26 -16 4.0 250 35 2 .14  11 1.6  2 11   440 100 2 21   570 130 0 11   440 110 2 8.4 280 75 2
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c .096 22 .82 2 .39 33 4.4 2 2.7 280 29 2 2.7 270 27 2 2.4 250 18 2 3.1  270 28   2 .073 26 .98 2 .11  26 .75 2 3.0 280 24 2 3.9 240 38 2 .16  11 1.5  2 8.9 290 81 2 11   280 96 2 8.7 290 76 2 8.0 270 70 2
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c .11  22 .77 2 .40 33 5.1 2 2.8 270 25 2 2.8 270 23 2 2.3 240 21 2 3.1  260 29   2 .070 26 .72 2 .077 26 .79 2 3.0 270 23 2 4.0 250 35 2 .14  11 1.8  2 8.9 290 69 2 8.9 250 81 2 8.8 290 80 2 8.0 270 75 2
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c .10  22 .73 2 .41 33 4.6 2 2.8 270 25 2 2.7 270 24 2 2.4 240 20 2 3.0  260 27   2 .074 26 .75 2 .078 26 .72 2 2.7 270 24 -16 3.9 240 41 2 .14  11 1.7  2 8.7 290 69 2 8.8 260 79 2 8.8 290 78 2 8.0 270 77 2
float-benchs/arctan_Pade_true-unreach-call_true-termination.c 55     260 670    2 94    240 940   2 4.1 290 35 -16 8.0 460 65 0 87   560 810 2 890    1100 11000   0 130     1200 910    2 120     1200 1000    2 3.4 280 31 -16 6.4 330 55 0 .17  11 2.1  0 140   2700 1200 0 51   840 340 0 410   2700 4500 0 160   540 1900 2
float-benchs/bary_diverge_true-unreach-call_true-termination.c 900     460 11000    0 870    1200 9100   0 900   7500 9700 0 900   1800 10000 0 900   4700 9200 0 890    260 10000   0 900     1000 7800    0 900     1000 8500    0 900   2100 10000 0 6.7 330 56 0 900     69 11000    0 900   3100 9600 0 15   280 140 0 900   3000 12000 0 84   820 850 2
float-benchs/cast_float_union_true-unreach-call.c .13  23 .72 2 .44 33 3.6 2 3.1 300 27 2 2.7 260 27 2 2.4 250 24 2 3.1  250 32   2 .075 26 1.0  2 .11  26 .67 2 2.6 270 24 2 4.1 250 36 2 .15  11 1.3  2 4.1 240 37 2 4.8 270 35 2 4.4 260 37 2 7.3 260 59 2
float-benchs/cos_polynomial_true-unreach-call_true-termination.c 7.0   110 60    2 11    110 94   2 4.1 290 33 -16 330   830 1800 0 900   1600 5900 0 890    610 8200   0 17     540 170    2 17     540 180    2 3.2 280 29 -16 6.5 320 59 0 .19  11 1.9  0 900   2900 6600 0 130   960 1000 0 900   2900 6500 0 100   590 1000 2
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c .70  32 8.0  2 870    3200 5700   0 900   4200 10000 0 900   3900 11000 0 900   2800 8400 0 890    270 9500   0 900     1800 11000    0 900     1800 11000    0 6.8 370 59 2 6.2 320 53 0 900     1800 8000    0 900   5400 11000 0 900   4700 11000 0 900   4900 11000 0 790   6700 9400 2
float-benchs/divmul_diverge_true-unreach-call_true-termination.c 900     400 10000    0 870    3100 6100   0 900   4200 12000 0 900   4000 11000 0 900   2700 9200 0 890    270 13000   0 900     2400 11000    0 900     2400 11000    0 5.5 310 43 2 5.4 310 49 0 900     1800 8500    0 900   5400 12000 0 900   4800 12000 0 900   4900 11000 0 780   6500 11000 2
float-benchs/drift_tenth_true-unreach-call_true-termination.c .42  35 5.4  2 1.2  33 10   2 3.5 270 30 2 4.0 280 34 2 2.4 250 21 2 890    490 7700   0 .10  26 .93 2 .26  37 2.9  2 9.3 460 82 2 4.0 240 37 2 .14  11 1.6  2 770   850 7900 0 900   660 9500 0 760   840 9000 0 18   530 150 -16
float-benchs/exp_loop_true-unreach-call.c 19     210 220    2 3.4  42 39   2 4.7 300 36 -16 4.0 330 41 0 790   8500 8000 2 890    410 8100   0 17     110 190    2 17     110 190    2 4.7 300 41 -16 6.4 310 53 0 .20  11 1.8  0 900   1300 8600 0 430   990 4400 0 900   1400 13000 0 680   220 7600 0
float-benchs/feedback_diverge_true-unreach-call_true-termination.c 900     1600 12000    0 870    1100 8500   0 900   7100 8600 0 900   3900 11000 0 900   1900 8800 0 890    330 8200   0 900     2600 10000    0 900     2600 10000    0 910   4100 11000 0 6.2 340 59 0 900     1800 8700    0 900   5300 13000 0 900   4900 11000 0 900   4700 11000 0 900   6100 10000 0
float-benchs/filter1_true-unreach-call_true-termination.c 900     630 8900    0 870    1600 11000   0 3.5 280 32 2 3.5 270 32 2 18   790 130 2 890    280 8400   0 900     1400 7800    0 3.4   140 45    2 7.4 420 60 2 6.1 320 56 0 900     2000 11000    0 530   1400 4200 0 37   380 410 0 570   1100 5400 0 31   660 260 2
float-benchs/filter2_alt_true-unreach-call.c 900     180 12000    0 870    180 11000   0 4.3 320 38 0 6.1 340 71 0 900   1200 7000 0 890    230 9700   0 900     560 6800    0 900     670 9000    0 900   1600 12000 0 6.8 330 55 0 900     70 10000    0 900   1300 9600 0 16   320 170 0 900   1300 7600 0 900   380 13000 0
float-benchs/filter2_iterated_true-unreach-call.c 900     620 8000    0 870    1300 4900   0 4.1 300 39 0 6.1 510 59 0 900   2400 8200 0 900    6500 8200   0 900     3400 7200    0 900     4000 7900    0 900   2000 11000 0 6.7 350 58 0 900     9600 11000    0 35   2200 370 0 18   2200 180 0 39   2200 530 0 400   540 5100 0
float-benchs/filter2_reinit_true-unreach-call_true-termination.c 900     530 8400    0 870    490 8400   0 900   3400 14000 0 900   3900 12000 0 900   3000 8100 0 890    250 9500   0 900     1400 6300    0 900     1600 6500    0 200   2300 2400 2 5.8 300 54 0 900     69 11000    0 900   2000 7400 0 49   430 390 0 900   2100 7900 0 900   1000 11000 0
float-benchs/filter2_set_true-unreach-call_true-termination.c 900     380 7200    0 870    450 13000   0 5.1 310 40 -16 8.6 470 84 0 910   3800 8300 0 890    450 7500   0 900     1900 7300    0 900     1200 9000    0 5.3 290 48 -16 7.2 350 58 0 .18  12 2.0  0 400   3400 4200 0 30   530 250 0 460   3400 4300 0 900   540 11000 0
float-benchs/filter2_true-unreach-call_true-termination.c 900     640 7600    0 870    480 8600   0 34   1400 300 2 35   1400 290 2 900   3900 9700 0 890    550 8500   0 900     1700 9000    0 900     1400 6000    0 210   3200 2600 2 5.6 300 47 0 900     68 11000    0 900   2100 12000 0 29   400 240 0 900   2100 9100 0 900   530 11000 0
float-benchs/filter_iir_true-unreach-call.c 900     310 9900    0 870    750 8600   0 3.3 280 28 2 3.3 280 30 2 2.7 260 23 2 890    750 8400   0 900     2300 7500    0 900     1800 10000    0 3.7 280 32 -16 7.3 360 56 0 900     64 11000    0 900   1500 8200 0 900   2000 6900 0 900   1800 8500 0 810   410 12000 0
float-benchs/float_double_true-unreach-call_true-termination.c .12  22 .83 2 .44 33 4.0 2 2.8 270 25 2 2.7 270 23 2 2.3 240 21 2 3.1  250 30   2 .10  26 .62 2 .098 26 .80 2 2.9 280 23 -16 3.8 230 41 2 .17  11 1.4  2 8.6 280 73 2 8.6 270 71 2 9.3 290 73 2 8.3 270 75 2
float-benchs/image_filter_true-unreach-call.c 900     1100 9200    0 850    2800 6000   2 900   4700 10000 0 900   4700 11000 0 690   15000 7800 0 890    3100 7200   0 660     3000 4200    2 750     5700 5000    2 910   4300 11000 0 10   640 86 0 .25  12 3.0  0 900   6900 8400 0 900   6800 10000 0 910   13000 3500 0 870   2300 9900 0
float-benchs/interpolation2_true-unreach-call_true-termination.c .42  30 4.3  2 1.2  36 13   2 4.1 310 35 -16 6.3 340 68 0 900   660 9800 0 630    320 7200   0 3.1   92 45    2 5.5   93 65    2 3.7 290 31 -16 5.8 320 53 0 .20  11 2.0  0 900   760 10000 0 64   380 660 0 900   770 10000 0 820   220 10000 0
float-benchs/interpolation_true-unreach-call_true-termination.c .28  27 2.4  2 1.1  36 11   2 4.2 310 33 -16 8.2 330 92 0 11   410 140 2 130    310 1400   0 1.3   71 16    2 2.3   73 34    2 3.5 270 30 -16 5.9 320 45 0 .17  11 1.7  0 900   930 8500 0 650   760 6900 0 900   990 11000 0 900   220 11000 0
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c .28  30 2.9  2 .71 36 6.9 2 3.8 290 37 -16 3.6 310 36 -16 5.5 300 64 2 320    270 3100   -16 .75  67 8.6  2 .73  67 9.4  2 2.9 280 24 -16 5.9 320 50 0 .18  11 1.9  0 150   2400 1400 0 69   340 900 0 100   2400 880 0 13   300 120 2
float-benchs/inv_square_int_true-unreach-call_true-termination.c .13  27 1.3  2 .46 35 4.0 2 3.5 290 36 -16 3.1 290 30 0 3.3 280 32 2 27    300 360   2 .26  38 3.0  2 .23  38 3.4  2 2.9 270 23 -16 5.6 300 45 0 .16  12 1.9  2 33   390 380 2 12   300 100 2 32   390 360 2 8.7 280 73 2
float-benchs/inv_square_true-unreach-call_true-termination.c .15  26 1.0  2 .48 35 4.4 2 3.5 280 28 -16 3.1 300 30 0 3.4 280 34 2 5.2  280 56   2 .23  34 2.6  2 .24  34 2.2  2 2.8 270 25 -16 5.8 310 48 2 .18  11 1.8  0 61   400 710 2 12   290 110 2 62   410 700 2 8.6 280 73 2
float-benchs/loop_true-unreach-call.c 900     330 7400    0 480    15000 6200   0 900   4400 8100 0 900   4400 7300 0 900   3500 10000 0 890    320 10000   0 900     1300 11000    0 900     1400 13000    0 900   5300 14000 0 5.3 300 44 0 11     290 150    2 900   1100 10000 0 70   560 820 0 900   1000 8900 0 43   600 440 2
float-benchs/mea8000_true-unreach-call.c 900     2900 9700    0 230    13000 2500   0 900   4000 12000 0 900   4100 9900 0 900   4900 9800 0 890    1900 11000   0 900     1400 12000    0 900     1700 11000    0 910   4900 11000 0 15   730 120 0 900     67 11000    0 900   5600 12000 0 780   5100 9800 0 900   5300 11000 0 780   670 11000 0
float-benchs/nan_double_range_true-unreach-call_true-termination.c .11  22 .68 2 .42 33 3.6 2 2.7 270 25 2 2.8 270 28 2 3.0 270 24 2 3.6  280 37   2 .17  28 1.4  2 .13  28 1.7  2 2.8 270 24 2 5.5 300 47 0 .18  11 2.0  0 8.9 290 68 2 8.2 250 65 2 8.6 290 68 2 8.0 270 70 2
float-benchs/nan_float_range_true-unreach-call_true-termination.c .12  22 .81 2 .43 33 4.4 2 2.8 270 25 2 2.8 270 28 2 3.0 270 28 2 3.6  270 35   2 .16  28 1.7  2 .15  28 1.5  2 2.8 260 26 2 5.0 300 42 0 .18  11 1.9  0 10   300 91 2 8.7 260 80 2 10   300 93 2 8.4 270 75 2
float-benchs/rlim_exit_true-unreach-call_true-termination.c 900     1800 10000    0 180    14000 2600   0 900   4300 9300 0 900   3900 11000 0 900   3000 11000 0 890    200 9900   0 900     2300 11000    0 900     2300 9100    0 8.4 470 72 2 5.7 320 51 0 900     61 12000    0 900   5200 12000 0 900   5700 14000 0 900   3000 13000 0 780   3400 10000 2
float-benchs/rlim_invariant_true-unreach-call_true-termination.c 900     1800 11000    0 870    1300 7900   0 3.7 280 33 2 3.7 280 37 2 8.8 500 70 2 890    440 8600   0 900     870 7800    0 1.2   61 16    2 10   490 78 2 5.8 310 48 0 900     61 11000    0 770   910 8400 0 60   440 700 0 900   930 12000 0 22   470 170 2
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call_true-termination.c 820     310 8000    2 870    310 8900   0 3.2 290 26 0 2.7 270 22 0 900   1200 8500 0 890    1700 5600   0 900     4200 6400    0 900     4200 6700    0 4.7 320 37 -16 8.0 470 69 0 .19  11 2.4  0 900   2400 5300 0 33   2500 230 0 900   2000 6700 0 900   240 10000 0
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call_true-termination.c 900     320 9200    0 870    300 9900   0 2.7 270 24 0 2.6 270 25 0 900   1400 8300 0 890    1700 6900   0 900     3400 6400    0 900     3400 8600    0 4.9 310 39 -16 8.2 480 74 0 .17  11 2.0  0 900   2200 6000 0 33   2500 250 0 900   2100 6300 0 900   240 12000 0
float-benchs/sin_interpolated_index_true-unreach-call_true-termination.c 770     310 10000    2 870    290 10000   0 4.2 320 40 -16 3.2 280 29 0 900   720 11000 0 890    490 6100   0 900     740 8700    0 900     740 9200    0 3.4 270 31 -16 8.5 470 76 0 .17  11 2.1  0 900   2200 10000 0 38   2500 290 0 900   2100 10000 0 900   250 12000 0
float-benchs/sin_interpolated_negation_true-unreach-call.c 900     540 7000    0 870    4300 5900   0 2.7 270 25 0 2.8 270 25 0 900   2700 7200 0 890    2100 6800   0 900     13000 10000    0 900     3100 6200    0 35   1500 310 0 11   520 90 0 .20  11 2.2  0 900   2600 5500 0 22   2500 170 0 900   2400 5600 0 900   1700 9700 0
float-benchs/sin_interpolated_smallrange_true-unreach-call.c 900     360 7100    0 870    3000 6200   0 2.8 270 22 0 2.7 260 25 0 900   4000 9000 0 890    1800 6100   0 900     13000 8300    0 900     2700 6900    0 900   4500 11000 0 8.4 470 69 0 .17  11 2.0  0 900   2300 5500 0 33   2500 230 0 900   2700 5500 0 900   900 11000 0
float-benchs/sqrt_Householder_constant_true-unreach-call.c 900     310 6800    0 3.4  33 36   2 3.8 290 35 0 7.5 440 58 2 3.9 260 29 2 890    1000 12000   0 .49  27 5.5  2 240     1800 1900    2 5.2 290 44 -16 6.3 330 59 0 .14  11 2.0  2 250   3100 2100 0 94   1500 830 0 250   3000 2600 0 200   1400 2500 2
float-benchs/sqrt_Householder_interval_true-unreach-call.c 900     330 9400    0 870    590 9700   0 3.9 290 36 -16 6.0 520 50 0 900   1300 13000 0 890    620 7700   0 900     1900 6500    0 900     1500 6100    0 3.2 260 32 -16 6.2 330 59 0 .19  11 1.9  0 150   2800 1500 0 78   1600 690 0 160   2800 1300 0 900   230 11000 0
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c 900     330 6600    0 870    3000 12000   0 4.2 290 41 -16 5.5 540 53 0 900   2600 11000 0 890    1200 7200   0 900     3100 7900    0 900     1500 7800    0 3.1 260 31 -16 6.2 320 59 0 .17  11 1.8  0 90   2600 760 0 78   1700 550 0 87   2600 910 0 900   440 13000 0
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c 900     390 7100    0 870    2000 8100   0 4.1 290 38 -16 5.6 540 58 0 900   1800 11000 0 890    1100 7200   0 900     2500 9100    0 900     1200 6000    0 3.4 270 28 -16 6.4 320 63 0 .18  11 2.0  0 87   2600 910 0 99   1800 1000 0 110   2700 1000 0 900   340 12000 0
float-benchs/sqrt_biNewton_pseudoconstant_true-unreach-call.c 900     340 5800    0 870    3300 10000   0 4.2 290 35 -16 5.5 540 54 0 900   1900 10000 0 890    1400 7000   0 900     3600 8300    0 900     6400 7000    0 3.3 270 28 -16 6.0 300 54 0 .18  11 2.1  0 84   2600 870 0 100   1800 1100 0 110   2700 990 0 900   460 11000 0
float-benchs/sqrt_poly_true-unreach-call_true-termination.c 1.2   58 12    2 3.5  64 38   2 3.7 290 33 -16 35   490 300 0 45   510 440 2 890    500 6900   0 5.9   310 61    2 5.8   310 56    2 3.0 280 25 -16 5.7 330 57 0 .17  11 1.9  0 240   1800 1700 2 94   820 670 0 200   1900 1300 2 49   510 530 2
float-benchs/water_pid_true-unreach-call_true-termination.c 900     900 8400    0 3.8  36 39   2 9.5 490 74 0 900   1300 10000 0 4.4 270 35 2 890    580 7600   0 2.6   27 32    2 4.8   210 57    2 4.8 300 42 -16 5.5 300 45 0 .16  11 1.8  2 160   3000 1400 0 71   1500 540 0 130   3000 1200 0 56   1100 540 2
float-benchs/zonotope_2_true-unreach-call_true-termination.c 900     340 8400    0 400    5500 4100   2 4.2 290 35 2 3.8 270 36 2 900   2300 6900 0 45    76 610   0 900     4000 12000    0 900     4100 9600    0 900   4800 11000 0 5.6 300 46 0 1.0   34 14    2 900   2800 7700 0 200   580 1900 0 900   1800 8900 0 210   1800 2300 2
float-benchs/zonotope_3_true-unreach-call_true-termination.c 900     1700 12000    0 230    15000 3300   0 900   4200 11000 0 900   4100 8600 0 160   2300 1900 2 200    2300 2000   2 900     2700 10000    0 1.8   96 22    2 900   4900 12000 0 5.5 320 52 0 900     73 12000    0 900   5400 14000 0 900   5200 12000 0 900   5300 13000 0 23   520 210 2
float-benchs/zonotope_loose_true-unreach-call_true-termination.c .20  34 2.6  2 .65 40 6.4 2 3.5 280 32 -16 3.6 340 40 0 5.4 330 54 2 90    350 890   2 1.2   120 12    2 1.2   120 13    2 2.9 270 29 -16 5.7 320 51 0 .19  11 1.8  0 190   1500 1800 2 74   760 760 0 150   1200 1300 0 11   330 95 2
float-benchs/zonotope_tight_true-unreach-call_true-termination.c .22  34 2.1  2 .67 40 7.1 2 3.6 290 36 -16 3.9 340 39 0 5.5 330 63 2 110    350 960   2 1.2   120 13    2 1.2   120 14    2 3.0 270 27 -16 5.5 320 51 0 .18  11 1.9  0 170   1300 1300 2 72   740 660 0 190   1300 1600 2 11   340 100 2
floats-esbmc-regression/Double_div_true-unreach-call.i 1.6   49 19    2 5.6  34 66   2 900   4200 10000 0 900   4100 9400 0 5.8 460 43 2 890    260 8000   0 130     100 1600    2 130     81 1600    2 900   4000 14000 0 5.2 300 46 0 .17  11 1.5  2 290   2700 2200 0 51   890 560 0 340   2800 2800 0 12   340 99 2
floats-esbmc-regression/Float_div_true-unreach-call.i .43  32 4.4  2 2.8  33 27   2 900   4100 10000 0 900   4100 9100 0 3.4 260 28 2 890    610 12000   0 .47  26 6.1  2 .63  33 7.7  2 900   4000 12000 0 5.2 290 44 0 .17  11 1.7  2 190   600 1600 0 84   530 800 0 320   730 2700 0 12   300 88 2
floats-esbmc-regression/ceil_nondet_true-unreach-call.i 3.6   89 46    2 6.9  57 81   2 3.6 290 34 0 3.6 290 35 -16 5.9 410 47 0 17    460 170   0 .32  38 3.9  2 .29  38 3.5  2 3.2 280 30 0 4.2 290 43 0 .095 11 .81 0 7.5 230 64 0 7.5 230 56 0 7.7 230 62 0 190   330 2100 2
floats-esbmc-regression/ceil_true-unreach-call.i .45  32 3.9  2 1.9  39 20   2 4.1 280 40 2 3.6 300 33 -16 3.1 250 25 2 4.3  270 48   2 .15  27 1.8  2 .15  27 2.1  2 4.2 290 36 -16 3.8 250 38 0 .13  11 1.6  0 3.8 220 29 0 3.9 230 29 0 4.0 220 31 0 18   290 150 2
floats-esbmc-regression/copysign_true-unreach-call.i .36  30 2.4  2 1.4  38 11   2 4.9 290 39 2 3.5 270 28 2 3.0 250 28 2 4.5  270 48   2 .088 27 .98 2 .12  27 .94 2 4.5 290 39 -16 4.0 270 37 0 .14  11 1.4  0 3.7 220 31 0 3.6 230 31 0 3.7 230 31 0 17   280 130 2
floats-esbmc-regression/digits_for_true-unreach-call.i 620     760 7500    2 2.9  33 30   2 2.4 270 22 0 1.5 130 12 0 1.9 180 17 0 19    76 280   -16 .37  26 4.0  2 2.4   190 23    2 2.5 270 23 0 2.9 200 32 0 .17  11 1.6  2 900   3200 7000 0 86   540 640 0 900   2700 7500 0 16   270 120 2
floats-esbmc-regression/digits_while_true-unreach-call.i 630     770 5600    2 2.9  33 29   2 2.5 270 23 0 1.5 130 15 0 1.9 180 18 0 19    76 230   -16 .37  26 3.9  2 2.3   190 24    2 2.5 270 23 0 2.9 200 27 0 .17  11 1.4  2 900   3100 7000 0 89   520 930 0 900   2600 6800 0 16   270 150 2
floats-esbmc-regression/fabs_true-unreach-call.i .23  29 2.2  2 .90 37 8.8 2 4.4 310 41 2 3.3 270 31 2 4.8 290 40 2 5.8  300 59   2 .083 27 .87 2 .085 27 1.0  2 3.8 280 37 -16 3.9 240 38 0 .12  11 1.2  0 9.5 310 72 2 8.6 270 77 2 9.6 310 72 2 17   280 140 2
floats-esbmc-regression/fdim_true-unreach-call.i .21  29 2.5  2 1.0  39 11   2 4.2 280 37 2 3.0 270 32 2 3.0 250 26 2 4.2  260 45   2 .12  27 .82 2 .12  27 .91 2 3.9 290 32 -16 3.9 260 39 0 .12  11 1.3  0 3.6 220 27 0 3.7 230 29 0 3.9 230 33 0 17   280 140 2
floats-esbmc-regression/floor_nondet_true-unreach-call.i 3.7   90 46    2 7.1  59 74   2 3.5 300 27 0 3.7 290 32 -16 5.8 420 52 0 14    440 160   0 .32  38 4.0  2 .29  38 3.3  2 3.3 280 29 0 4.2 280 39 0 .096 11 .98 0 7.5 230 63 0 7.4 230 61 0 7.2 220 62 0 190   320 2300 2
floats-esbmc-regression/floor_true-unreach-call.i .45  32 4.2  2 1.9  39 22   2 4.0 280 35 2 3.4 290 29 -16 3.1 250 29 2 4.3  270 44   2 .19  27 1.9  2 .15  27 1.7  2 4.0 290 39 -16 4.0 260 34 0 .12  11 1.2  0 3.7 220 32 0 3.5 220 32 0 3.6 230 31 0 18   280 140 2
floats-esbmc-regression/fmax_true-unreach-call.i .35  30 2.6  2 1.4  38 15   2 4.1 280 37 2 3.0 270 26 2 3.1 260 29 2 4.2  260 44   2 .079 27 .87 2 .080 27 .90 2 3.8 280 31 -16 3.9 250 34 0 .14  11 1.3  0 8.5 290 66 2 8.4 260 69 2 8.5 290 68 2 18   280 130 2
floats-esbmc-regression/fmin_true-unreach-call.i .37  33 2.8  2 1.4  38 12   2 4.3 310 36 2 3.0 270 26 2 2.9 250 25 2 4.1  270 39   2 .080 27 1.1  2 .083 27 1.1  2 3.7 280 37 -16 3.8 250 38 0 .14  11 1.3  0 8.6 290 72 2 8.4 260 69 2 8.6 290 70 2 17   290 140 2
floats-esbmc-regression/fmod2_true-unreach-call.i .92  96 9.9  2 2.3  39 21   2 5.1 300 45 -16 3.5 290 35 -16 11   500 120 2 5.0  280 46   -16 .18  29 1.7  2 .17  29 1.8  2 4.1 280 33 -16 3.9 270 36 0 .12  11 1.3  0 7.5 230 62 0 7.2 230 59 0 7.3 230 61 0 22   530 190 2
floats-esbmc-regression/fmod3_true-unreach-call.i .93  95 12    2 2.2  39 26   2 4.9 300 45 -16 3.5 290 34 -16 11   500 110 2 5.1  280 52   -16 .16  29 1.7  2 .18  32 1.9  2 4.1 290 34 -16 3.9 260 36 0 .13  11 1.2  0 7.3 230 64 0 7.4 230 70 0 7.2 230 64 0 22   520 190 2
floats-esbmc-regression/fmod_true-unreach-call.i .88  82 9.3  2 2.2  39 23   2 4.4 280 34 2 3.1 270 32 2 2.9 250 25 2 4.3  260 40   2 .088 27 .92 2 .12  27 .88 2 3.9 280 33 -16 3.8 240 34 2 .16  11 1.6  2 3.7 220 28 0 3.8 230 29 0 3.6 230 30 0 18   280 170 2
floats-esbmc-regression/isgreater_true-unreach-call.i .21  28 1.8  2 .91 37 8.6 2 3.9 280 35 2 3.0 270 30 2 3.2 250 28 2 4.2  270 37   2 .10  27 .86 2 .11  27 1.0  2 3.8 290 32 -16 4.2 240 37 2 .16  11 1.6  2 8.6 290 67 2 8.2 260 73 2 8.4 290 76 2 15   280 130 2
floats-esbmc-regression/isgreaterequal_true-unreach-call.i .19  30 1.7  2 .85 37 10   2 4.1 280 35 2 3.2 280 25 2 2.9 250 25 2 4.3  270 49   2 .080 27 .88 2 .12  27 .85 2 3.9 280 36 -16 4.0 240 38 2 .17  11 1.5  2 8.5 290 65 2 8.4 260 66 2 8.5 290 71 2 15   280 130 2
floats-esbmc-regression/isless_true-unreach-call.i .23  30 1.8  2 .90 37 8.1 2 4.0 280 35 2 3.2 270 28 2 3.0 260 23 2 4.2  260 41   2 .091 27 1.1  2 .079 27 1.0  2 3.9 280 33 -16 4.1 240 34 2 .14  11 1.5  2 8.5 290 63 2 8.1 260 64 2 8.7 300 82 2 15   280 120 2
floats-esbmc-regression/islessequal_true-unreach-call.i .23  28 1.3  2 .92 37 7.6 2 4.2 280 33 2 3.1 270 26 2 3.0 260 28 2 4.1  260 39   2 .082 27 .94 2 .11  27 .68 2 3.8 280 36 -16 3.8 250 39 2 .16  11 1.7  2 8.7 290 66 2 8.3 270 69 2 8.9 290 74 2 15   290 140 2
floats-esbmc-regression/islessgreater_true-unreach-call.i .19  28 1.9  2 .89 37 8.9 2 4.2 280 35 2 3.1 270 28 2 2.9 250 25 2 4.3  280 45   2 .11  27 .87 2 .083 27 .91 2 3.8 290 31 -16 4.1 240 40 2 .14  11 1.4  2 8.8 290 79 2 8.4 260 77 2 8.9 290 69 2 15   290 130 2
floats-esbmc-regression/isunordered_true-unreach-call.i .28  28 2.5  2 .88 37 9.6 2 4.0 280 37 2 3.0 270 26 2 3.1 260 27 2 4.2  270 44   2 .079 27 1.0  2 .084 27 1.1  2 4.0 280 36 -16 4.0 240 35 2 .17  11 1.7  2 8.6 290 71 2 8.4 260 78 2 8.9 300 76 2 16   310 140 2
floats-esbmc-regression/lrint_true-unreach-call.i .47  31 5.2  2 1.9  41 25   2 3.5 280 33 0 3.2 280 28 -16 6.3 440 46 0 8.8  430 84   0 .18  27 2.0  2 .19  27 2.2  2 3.0 270 28 0 4.5 300 38 0 .080 11 .89 0 3.7 230 30 0 3.6 220 30 0 3.7 220 30 0 19   370 150 2
floats-esbmc-regression/modf_true-unreach-call.i .41  30 3.0  2 1.8  43 22   2 4.6 300 43 -16 3.3 290 28 -16 2.9 250 26 2 4.4  270 44   2 .16  27 1.7  2 .18  27 1.6  2 3.9 280 35 -16 3.9 250 36 0 .12  11 1.2  0 3.6 230 28 0 3.6 230 30 0 3.7 220 32 0 18   280 160 2
floats-esbmc-regression/nan_true-unreach-call.i .27  31 3.0  2 .90 38 8.5 2 4.2 300 34 2 2.9 270 30 2 3.0 250 29 2 4.2  270 44   2 .11  27 .69 2 .11  27 .75 2 3.9 290 35 -16 4.2 260 40 0 .13  11 1.2  0 11   340 77 2 9.5 320 75 2 9.2 310 69 2 18   290 130 2
floats-esbmc-regression/nearbyint2_true-unreach-call.i .51  33 4.2  2 2.0  39 14   2 3.2 260 28 0 3.3 280 28 -16 6.8 440 57 0 9.2  450 91   0 .21  27 1.8  2 .18  27 1.9  2 3.1 270 29 0 3.7 240 33 0 .079 11 .91 0 3.7 220 30 0 5.8 320 51 0 3.7 220 30 0 19   380 170 2
floats-esbmc-regression/nearbyint_true-unreach-call.i .52  33 4.3  2 3.9  39 38   2 3.4 260 29 0 3.7 290 30 -16 8.6 460 68 0 11    470 100   0 .19  27 2.3  2 .23  32 2.2  2 3.4 280 30 0 3.8 240 33 0 .097 11 .85 0 3.8 230 33 0 3.8 230 32 0 5.8 320 47 0 260   230 2900 2
floats-esbmc-regression/remainder_true-unreach-call.i 1.1   110 12    2 2.2  39 24   2 4.8 310 38 2 3.8 280 33 2 3.0 260 23 2 4.5  270 48   2 .21  27 1.9  2 .19  27 2.3  2 4.4 290 38 -16 4.5 300 38 0 .13  11 1.3  0 3.7 220 33 0 3.8 220 31 0 3.6 220 31 0 2.3 140 20 0
floats-esbmc-regression/rint2_true-unreach-call.i .51  33 4.7  2 2.0  39 20   2 3.2 260 30 0 3.2 290 28 -16 6.9 440 59 0 9.4  450 83   0 .18  28 2.1  2 .17  28 2.1  2 3.1 280 28 0 4.0 240 33 0 .11  11 .80 0 3.6 230 31 0 3.8 220 34 0 3.5 220 28 0 19   390 160 2
floats-esbmc-regression/rint_true-unreach-call.i .51  32 4.6  2 3.8  39 49   2 3.3 260 30 0 3.6 300 30 -16 7.6 440 63 0 12    470 98   0 .18  28 2.0  2 .20  34 2.6  2 3.3 280 30 0 3.9 240 33 0 .097 11 .94 0 3.9 230 29 0 5.9 340 38 0 3.9 230 32 0 260   240 3000 2
floats-esbmc-regression/round_nondet_true-unreach-call.i 3.8   120 44    2 7.5  68 94   2 3.5 300 30 0 3.8 290 37 -16 6.7 430 56 0 17    450 180   0 .72  81 8.1  2 .70  81 8.5  2 3.2 280 29 0 3.9 290 36 0 .080 11 .99 0 7.5 230 60 0 7.6 230 62 0 7.5 220 59 0 190   350 2300 2
floats-esbmc-regression/round_true-unreach-call.i .54  39 5.2  2 2.1  39 20   2 5.0 290 38 2 3.8 290 39 -16 3.1 260 27 2 4.8  260 47   2 .21  27 2.5  2 .21  27 2.5  2 4.6 290 38 -16 4.2 300 41 0 .14  11 1.4  0 3.8 230 29 0 3.7 220 31 0 3.9 220 32 0 19   290 140 2
floats-esbmc-regression/rounding_functions_true-unreach-call.i .52  34 4.9  2 2.1  39 19   2 6.3 430 56 2 4.4 290 41 2 3.3 260 25 2 5.1  260 52   2 .27  28 2.6  2 .24  27 2.8  2 4.6 290 45 -16 4.0 240 37 2 .14  11 1.5  0 3.8 220 31 0 3.7 230 31 0 3.7 220 34 0 19   290 150 2
floats-esbmc-regression/trunc_nondet_2_true-unreach-call.i 2.1   38 25    2 4.9  40 51   2 5.1 310 46 -16 3.7 290 31 -16 10   310 110 2 890    97 12000   0 1.2   44 18    2 1.2   44 14    2 4.0 290 31 -16 4.0 260 39 0 .11  11 1.3  0 7.8 230 64 0 9.2 320 62 0 7.6 230 64 0 180   310 2200 2
floats-esbmc-regression/trunc_nondet_true-unreach-call.i 2.2   91 26    2 4.9  55 49   2 3.5 290 28 0 3.4 280 33 -16 6.0 400 44 0 12    450 100   0 .31  38 3.9  2 .30  38 3.6  2 3.2 280 28 0 4.2 270 41 0 .082 11 .99 0 10   330 89 0 7.5 230 66 0 7.4 230 65 0 180   340 2600 2
floats-esbmc-regression/trunc_true-unreach-call.i .45  34 3.6  2 1.8  39 24   2 4.2 280 36 2 3.6 290 34 -16 2.9 260 26 2 4.4  270 38   2 .16  27 1.6  2 .18  27 1.8  2 4.1 280 35 -16 3.9 250 40 0 .13  11 1.2  0 3.9 220 30 0 3.7 230 27 0 3.8 230 34 0 18   300 150 2
floats-esbmc-regression/Double_div_bad_false-unreach-call.i 900     400 8000    0 11    41 120   1 900   4100 9700 0 900   4100 10000 0 88   2000 1100 1 890    630 8100   0 480     250 5900    1 480     260 4700    1 900   3900 11000 0 5.4 300 45 0 .17  11 1.6  1 310   2900 2900 0 65   1000 680 0 370   4100 4600 0 250   3600 2700 1
floats-esbmc-regression/Float_div_bad_false-unreach-call.i 900     350 10000    0 3.5  33 37   1 900   910 12000 0 900   1000 10000 0 10   460 80 1 890    690 8800   0 1.4   30 16    1 1.6   35 23    1 900   1100 11000 0 5.3 300 44 0 .16  11 1.6  1 900   2000 7900 0 85   510 910 0 900   1900 7800 0 230   1000 2900 1
floats-esbmc-regression/digits_bad_for_false-unreach-call.i 710     770 8400    0 2.7  33 27   0 2.4 260 23 0 1.5 130 14 0 1.9 210 16 0 19    76 280   0 .34  28 3.9  0 2.3   190 25    0 2.4 260 20 0 3.0 200 33 0 .17  11 1.5  0 900   3000 6400 0 83   510 620 0 900   2700 7600 0 15   220 120 0
floats-esbmc-regression/digits_bad_while_false-unreach-call.i 750     780 6200    0 2.7  33 27   0 2.5 270 23 0 1.4 120 12 0 1.8 180 18 0 19    76 240   0 .35  28 4.2  0 2.3   190 26    0 2.5 260 21 0 2.9 200 28 0 .14  11 1.6  0 900   2900 7900 0 85   500 810 0 900   2600 6800 0 15   220 140 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
total 172 34000 35000 340000 251 172 23000   110000 230000 259 172 13000   110000 150000 -714 172 34000   130000 310000 -235 172 45000   140000 400000 181 172 71000 87000 680000 54 172 29000   100000 280000 257 172 27000 81000 240000 263 172 16000   120000 190000 -1425 172 1100   53000 11000 91 172 13000    20000 150000   83 172 56000 200000 500000 131 172 17000 160000 180000 93 172 57000 200000 500000 131 172 50000 89000 630000 202
    correct results 138 4800 10000 54000 251 143 3100   17000 30000 259 78 310   23000 2700 134 62 420   19000 3600 117 113 6000   50000 51000 197 72 2800 23000 27000 134 142 5100   21000 43000 257 145 5500 26000 43000 263 38 550   16000 6200 63 59 370   17000 3500 107 45 18    790 230   83 74 4100 37000 38000 131 50 610 15000 5700 93 75 4200 37000 36000 131 120 9200 65000 110000 218
        correct true 113 4600 8400 52000 226 116 2900   14000 28000 232 56 230   17000 2000 112 55 200   16000 1800 110 84 4200   37000 38000 168 62 1400 21000 15000 124 115 4300   16000 35000 230 118 4700 21000 36000 236 25 520   13000 5900 50 48 280   13000 2600 96 38 17    710 220   76 57 3400 27000 30000 114 43 540 13000 5000 86 56 3000 25000 25000 112 98 7600 53000 91000 196
        correct false 25 210 1900 2300 25 27 220   2100 2200 27 22 82   6400 710 22 7 210   2500 1800 7 29 1800   13000 14000 29 10 1300 1800 12000 10 27 790   5200 8400 27 27 790 5200 7200 27 13 39   3500 350 13 11 89   3900 860 11 7 1.2  81 12   7 17 750 10000 7500 17 7 73 1900 670 7 19 1200 12000 12000 19 22 1600 12000 16000 22
    correct-unconfimed results 2 1500 1500 15000 0 3 6.7 110 71 0 3 13   950 120 0 16 940   7100 7800 0 0 5 40 300 540 0 3 6.2 370 71 0 3 10 700 100 0 10 33   2800 280 0 2 22   710 230 0 2 .31 22 3.2 0 6 1600 4600 12000 0 0 4 1400 3400 11000 0 2 31 440 260 0
        correct-unconfirmed true 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
        correct-unconfirmed false 2 1500 1500 15000 0 3 6.7 110 71 0 3 13   950 120 0 16 940   7100 7800 0 0 5 40 300 540 0 3 6.2 370 71 0 3 10 700 100 0 10 33   2800 280 0 2 22   710 230 0 2 .31 22 3.2 0 6 1600 4600 12000 0 0 4 1400 3400 11000 0 2 31 440 260 0
    incorrect results 0 0 51 210   15000 1800 -848 20 69   5800 630 -352 1 4.7 300 39 -16 5 370 980 3700 -80 0 0 91 390   29000 3600 -1488 1 6.2 330 57 -16 0 0 0 0 1 18 530 150 -16
        incorrect true 0 0 2 5.6 540 50 -64 2 5.5 540 48 -64 0 0 0 0 2 5.5 550 51 -64 0 0 0 0 0 0
        incorrect false 0 0 49 200   15000 1800 -784 18 63   5300 580 -288 1 4.7 300 39 -16 5 370 980 3700 -80 0 0 89 390   28000 3600 -1424 1 6.2 330 57 -16 0 0 0 0 1 18 530 150 -16
score (172 tasks, max score: 313) 251 259 -714 -235 181 54 257 263 -1425 91 83 131 93 131 202
Run set 2ls.sv-comp18.ReachSafety-Floats cbmc.sv-comp18.ReachSafety-Floats cpa-bam-bnb.sv-comp18.ReachSafety-Floats cpa-bam-slicing.sv-comp18.ReachSafety-Floats cpa-seq.sv-comp18.ReachSafety-Floats depthk.sv-comp18.ReachSafety-Floats esbmc-incr.sv-comp18.ReachSafety-Floats esbmc-kind.sv-comp18.ReachSafety-Floats interpchecker.sv-comp18.ReachSafety-Floats skink.sv-comp18.ReachSafety-Floats symbiotic.sv-comp18.ReachSafety-Floats uautomizer.sv-comp18.ReachSafety-Floats ukojak.sv-comp18.ReachSafety-Floats utaipan.sv-comp18.ReachSafety-Floats veriabs.sv-comp18.ReachSafety-Floats