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-05 07:52:24 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 false(unreach-call) 4.3   56 42    1 false(unreach-call) 3.1  59 31   1 false(unreach-call) 3.5 290 31 1 false(unreach-call) 33   390 240 0 false(unreach-call) 51   350 370 1 unknown 890    400 7500   0 false(unreach-call) 8.6   190 74    1 false(unreach-call) 8.4   190 89    1 false(unreach-call) 3.0 280 28 1 false(unreach-call) 7.4 350 71 1 unknown .16  11 1.9  0 false(unreach-call) 43   690 390 1 error (7) 100   1200 750 0 false(unreach-call) 43   700 320 1 false(unreach-call) 120   380 1100 1
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i false(unreach-call) 5.2   56 57    1 false(unreach-call) 1.9  58 28   1 false(unreach-call) 3.8 290 36 1 false(unreach-call) 49   390 350 0 false(unreach-call) 21   350 160 1 unknown 890    480 8000   0 false(unreach-call) 6.8   190 81    1 false(unreach-call) 6.8   190 55    1 false(unreach-call) 3.0 280 25 0 false(unreach-call) 7.1 360 62 1 unknown .18  11 1.9  0 false(unreach-call) 120   740 1100 1 error (7) 94   1100 700 0 false(unreach-call) 120   720 1100 1 false(unreach-call) 75   380 650 1
floats-cdfpl/newton_1_6_false-unreach-call_true-termination.i false(unreach-call) 2.8   55 29    1 false(unreach-call) 4.9  61 54   1 false(unreach-call) 3.7 290 35 1 false(unreach-call) 12   390 120 0 false(unreach-call) 18   360 130 1 unknown 890    400 7900   0 false(unreach-call) 2.9   180 29    1 false(unreach-call) 2.9   180 28    1 false(unreach-call) 3.0 270 25 1 false(unreach-call) 7.1 340 73 1 unknown .16  11 2.0  0 false(unreach-call) 20   680 180 1 error (7) 96   1100 830 0 false(unreach-call) 20   680 170 1 false(unreach-call) 87   380 850 1
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i false(unreach-call) 1.1   53 14    1 false(unreach-call) 3.5  60 29   1 false(unreach-call) 3.7 290 33 1 false(unreach-call) 12   390 98 0 false(unreach-call) 48   360 340 1 unknown 890    400 8700   0 false(unreach-call) 10     190 100    1 false(unreach-call) 10     190 91    1 false(unreach-call) 2.9 260 26 1 false(unreach-call) 10   350 97 1 unknown .18  11 1.8  0 false(unreach-call) 40   690 280 1 error (7) 99   1100 780 0 false(unreach-call) 40   700 400 1 false(unreach-call) 64   380 650 1
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i false(unreach-call) 3.8   54 38    1 false(unreach-call) 3.5  60 37   1 false(unreach-call) 3.6 290 29 1 false(unreach-call) 13   380 110 0 false(unreach-call) 11   350 83 1 unknown 890    460 7500   0 false(unreach-call) 7.5   190 66    1 false(unreach-call) 7.4   190 64    1 false(unreach-call) 3.0 270 30 1 false(unreach-call) 6.8 360 59 1 unknown .16  11 2.0  0 false(unreach-call) 27   680 230 1 error (7) 96   1200 660 0 false(unreach-call) 26   690 270 1 false(unreach-call) 41   380 400 1
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i false(unreach-call) 7.6   110 84    1 false(unreach-call) 22    130 190   1 false(unreach-call) 4.1 310 34 1 false(unreach-call) 40   490 350 0 false(unreach-call) 14   450 120 1 unknown 890    710 8400   0 false(unreach-call) 16     340 130    1 false(unreach-call) 16     340 140    1 false(unreach-call) 3.3 280 30 0 false(unreach-call) 15   350 170 0 unknown .19  11 2.1  0 timeout 900   1100 7200 0 error (7) 55   1500 460 0 timeout 900   1100 6400 0 timeout 900   230 13000 0
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i false(unreach-call) 4.1   92 47    1 false(unreach-call) 28    140 260   1 false(unreach-call) 3.9 310 37 1 false(unreach-call) 40   490 340 0 false(unreach-call) 70   460 470 1 unknown 890    700 9200   0 false(unreach-call) 16     350 130    1 false(unreach-call) 16     350 170    1 false(unreach-call) 3.3 270 31 0 false(unreach-call) 13   370 120 1 unknown .16  11 1.8  0 false(unreach-call) 130   860 1000 0 error (7) 48   1400 550 0 false(unreach-call) 130   860 1000 1 timeout 900   230 13000 0
floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i false(unreach-call) 12     100 120    1 false(unreach-call) 4.7  91 36   1 false(unreach-call) 3.8 290 32 1 false(unreach-call) 14   480 140 0 false(unreach-call) 15   450 120 1 unknown 890    760 8100   0 false(unreach-call) 12     350 110    1 false(unreach-call) 12     350 95    1 false(unreach-call) 3.2 270 31 1 false(unreach-call) 12   340 140 1 unknown .16  11 1.8  0 false(unreach-call) 27   840 240 1 error (7) 69   1600 550 0 false(unreach-call) 28   830 240 1 timeout 900   230 11000 0
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i false(unreach-call) 83     220 1100    1 false(unreach-call) 50    220 600   1 false(unreach-call) 4.4 320 35 0 false(unreach-call) 120   600 1100 0 false(unreach-call) 630   1100 4700 1 unknown 890    1000 9100   0 false(unreach-call) 18     510 150    1 false(unreach-call) 18     510 180    1 false(unreach-call) 3.7 310 30 0 unknown 18   360 190 0 unknown .18  11 1.9  0 timeout 900   1000 8700 0 error (7) 71   2000 650 0 timeout 900   1000 6000 0 timeout 900   230 11000 0
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i false(unreach-call) 50     220 440    1 false(unreach-call) 43    220 420   1 false(unreach-call) 4.5 320 44 0 false(unreach-call) 43   590 300 0 false(unreach-call) 340   570 2400 1 unknown 890    1000 8100   0 false(unreach-call) 170     520 1200    1 false(unreach-call) 160     520 1200    1 false(unreach-call) 3.6 300 29 0 unknown 18   370 200 0 unknown .18  11 1.7  0 false(unreach-call) 160   920 1200 0 error (7) 58   2000 560 0 false(unreach-call) 160   930 1200 0 timeout 900   230 12000 0
floats-cdfpl/newton_3_8_false-unreach-call_true-termination.i false(unreach-call) 29     190 250    1 false(unreach-call) 29    180 260   1 false(unreach-call) 4.4 310 34 1 false(unreach-call) 18   590 150 0 false(unreach-call) 17   560 140 1 unknown 890    1100 6900   0 false(unreach-call) 11     510 100    1 false(unreach-call) 11     510 100    1 false(unreach-call) 3.5 270 32 0 unknown 17   370 190 0 unknown .17  11 1.9  0 false(unreach-call) 260   990 1700 0 error (7) 57   2000 480 0 false(unreach-call) 260   1000 1800 0 timeout 900   230 12000 0
floats-cdfpl/sine_1_false-unreach-call_true-termination.i false(unreach-call) .49  38 5.2  1 false(unreach-call) 1.3  43 17   1 false(unreach-call) 3.6 280 32 1 false(unreach-call) 24   360 190 1 false(unreach-call) 7.4 300 61 1 false(unreach-call) 190    240 1600   1 false(unreach-call) 5.2   130 67    1 false(unreach-call) 5.7   130 48    1 false(unreach-call) 3.1 280 28 1 unknown 5.7 330 52 0 unknown .19  11 1.8  0 false(unreach-call) 19   570 170 1 error (7) 49   660 370 0 false(unreach-call) 19   580 170 1 false(unreach-call) 19   340 230 1
floats-cdfpl/sine_2_false-unreach-call_true-termination.i false(unreach-call) .64  38 9.0  1 false(unreach-call) .75 42 8.1 1 false(unreach-call) 3.4 280 30 1 false(unreach-call) 4.0 350 36 1 false(unreach-call) 37   330 320 1 false(unreach-call) 97    200 970   1 false(unreach-call) 2.9   130 27    1 false(unreach-call) 2.8   130 27    1 false(unreach-call) 2.8 280 28 1 false(unreach-call) 7.2 340 71 1 unknown .16  11 2.0  0 false(unreach-call) 23   570 240 1 error (7) 51   620 460 0 false(unreach-call) 23   570 230 1 false(unreach-call) 51   370 460 1
floats-cdfpl/sine_3_false-unreach-call_true-termination.i false(unreach-call) .30  38 3.0  1 false(unreach-call) 1.8  49 22   1 false(unreach-call) 3.4 280 31 1 false(unreach-call) 480   570 3900 0 false(unreach-call) 6.0 300 48 1 false(unreach-call) 65    180 620   1 false(unreach-call) 5.6   130 57    1 false(unreach-call) 5.9   130 58    1 false(unreach-call) 2.8 270 25 0 false(unreach-call) 7.0 360 61 0 unknown .16  11 2.0  0 timeout 900   870 6300 0 error (7) 51   620 430 0 timeout 900   900 7100 0 false(unreach-call) 220   450 1800 1
floats-cdfpl/square_1_false-unreach-call_true-termination.i false(unreach-call) 1.3   38 16    1 false(unreach-call) 1.0  42 14   1 false(unreach-call) 3.6 290 29 1 false(unreach-call) 12   360 110 0 false(unreach-call) 44   360 390 1 false(unreach-call) 570    210 4500   1 false(unreach-call) 3.1   130 31    1 false(unreach-call) 3.1   130 35    1 false(unreach-call) 2.9 280 28 0 false(unreach-call) 6.3 400 53 1 unknown .18  11 1.6  0 false(unreach-call) 160   500 1300 0 error (7) 32   380 250 0 false(unreach-call) 160   500 1400 0 false(unreach-call) 32   350 400 1
floats-cdfpl/square_2_false-unreach-call_true-termination.i false(unreach-call) 1.1   37 13    1 false(unreach-call) 1.2  43 15   1 false(unreach-call) 3.6 290 31 1 false(unreach-call) 170   490 1400 1 false(unreach-call) 210   510 1600 1 unknown 890    250 9000   0 false(unreach-call) 2.9   130 40    1 false(unreach-call) 2.9   130 30    1 false(unreach-call) 2.9 280 25 1 false(unreach-call) 6.4 400 64 1 unknown .16  11 1.5  0 false(unreach-call) 81   430 620 0 error (7) 28   380 210 0 false(unreach-call) 77   440 890 1 false(unreach-call) 200   510 1600 1
floats-cdfpl/square_3_false-unreach-call_true-termination.i false(unreach-call) .95  38 11    1 false(unreach-call) 1.2  42 17   0 false(unreach-call) 3.6 290 29 1 false(unreach-call) 46   400 400 0 false(unreach-call) 90   390 710 1 unknown 890    350 6400   0 false(unreach-call) 3.3   130 37    1 false(unreach-call) 3.5   130 32    1 false(unreach-call) 3.0 280 22 0 false(unreach-call) 5.6 310 51 1 unknown .18  11 2.0  0 false(unreach-call) 820   930 5800 0 error (7) 35   380 360 0 false(unreach-call) 830   930 6600 0 false(unreach-call) 71   360 590 1
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i true 8.3   73 78    2 true 18    65 180   2 false(unreach-call) 3.6 290 32 -16 timeout 900   620 6500 0 timeout 900   720 6000 0 unknown 890    410 8900   0 true 23     200 180    2 true 23     200 190    2 false(unreach-call) 3.0 270 27 -16 true 7.9 350 77 2 unknown .19  11 2.1  0 timeout 900   1100 5700 0 error (7) 110   1200 760 0 timeout 900   1100 5600 0 timeout 900   230 12000 0
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i true 10     70 95    2 true 14    72 200   2 false(unreach-call) 3.8 290 30 -16 timeout 900   820 6100 0 timeout 900   810 7500 0 unknown 890    400 8300   0 true 48     210 420    2 true 46     210 470    2 false(unreach-call) 3.1 280 26 -16 true 7.6 330 67 2 unknown .18  11 1.7  0 timeout 900   1000 6600 0 error (7) 100   1100 750 0 timeout 900   1000 6100 0 true 190   380 2700 2
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i true 10     73 120    2 true 22    66 240   2 false(unreach-call) 3.6 290 36 -16 timeout 900   760 6300 0 timeout 900   620 6400 0 unknown 890    400 8800   0 true 46     210 380    2 true 45     210 370    2 false(unreach-call) 3.0 270 26 -16 true 8.3 360 78 2 unknown .18  11 1.7  0 timeout 900   930 5500 0 error (7) 93   1200 760 0 timeout 900   920 6000 0 timeout 900   230 12000 0
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i true 33     150 400    2 true 48    130 470   2 false(unreach-call) 3.8 300 38 -16 timeout 900   700 6800 0 timeout 900   550 6200 0 unknown 890    680 8600   0 true 74     380 610    2 true 75     390 610    2 false(unreach-call) 3.4 290 31 -16 true 21   350 230 2 unknown .18  11 2.3  0 timeout 900   1000 8000 0 error (7) 66   1400 750 0 timeout 900   1000 7500 0 timeout 900   230 13000 0
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i true 28     140 230    2 true 55    140 600   2 false(unreach-call) 3.9 290 32 -16 timeout 900   640 8200 0 timeout 900   1000 6200 0 unknown 890    700 9100   0 true 90     390 1000    2 true 91     390 610    2 false(unreach-call) 3.2 280 32 -16 true 20   380 200 2 unknown .19  11 1.7  0 timeout 900   1000 6400 0 error (7) 67   1500 560 0 timeout 900   1000 5300 0 timeout 900   230 14000 0
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i true 23     130 170    2 true 68    150 740   2 false(unreach-call) 3.9 280 33 -16 timeout 900   750 6400 0 timeout 900   560 5700 0 unknown 890    710 9300   0 true 79     390 580    2 true 81     380 470    2 false(unreach-call) 3.3 290 28 -16 true 15   350 170 2 unknown .19  11 1.8  0 timeout 900   950 5800 0 error (7) 62   1400 510 0 timeout 900   980 6100 0 timeout 900   230 9900 0
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i true 44     140 480    2 true 47    130 700   2 false(unreach-call) 4.1 310 36 -16 timeout 900   630 6800 0 timeout 900   650 6700 0 unknown 890    710 9500   0 true 88     380 840    2 true 91     380 700    2 false(unreach-call) 3.3 280 29 -16 unknown 18   400 180 0 unknown .17  11 2.4  0 timeout 900   1000 6100 0 error (7) 59   1500 560 0 timeout 900   1000 7000 0 timeout 900   230 10000 0
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i true 60     140 580    2 true 75    140 790   2 false(unreach-call) 3.9 290 32 -16 timeout 900   630 6300 0 timeout 900   640 6900 0 unknown 890    760 8400   0 true 410     430 3200    2 true 400     430 2800    2 false(unreach-call) 3.2 270 30 -16 unknown 18   400 220 0 unknown .16  11 2.1  0 timeout 900   1000 6700 0 error (7) 61   1500 520 0 timeout 900   1000 7900 0 timeout 900   230 12000 0
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i true 69     200 680    2 true 120    190 1000   2 false(unreach-call) 4.6 330 35 -16 timeout 900   630 5600 0 timeout 900   910 7700 0 unknown 890    1000 10000   0 true 190     610 2000    2 true 190     610 1500    2 false(unreach-call) 3.6 270 34 -16 unknown 23   370 280 0 unknown .18  11 2.0  0 timeout 900   1100 6000 0 error (7) 66   2000 520 0 timeout 900   1100 6800 0 timeout 900   230 11000 0
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i true 69     220 600    2 true 140    220 1400   2 false(unreach-call) 4.6 330 40 -16 timeout 900   720 6200 0 timeout 900   670 5700 0 unknown 890    1000 9000   0 true 650     680 4400    2 true 670     680 4700    2 false(unreach-call) 3.5 280 29 -16 unknown 19   380 190 0 unknown .19  11 1.8  0 timeout 900   1100 7800 0 error (7) 70   2000 590 0 timeout 900   1100 5600 0 timeout 900   230 10000 0
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i true 98     220 850    2 true 160    220 1500   2 false(unreach-call) 4.4 330 40 -16 timeout 900   720 6500 0 timeout 900   790 6300 0 unknown 890    930 8900   0 true 240     620 1600    2 true 250     610 2200    2 false(unreach-call) 3.4 270 32 -16 unknown 21   380 250 0 unknown .16  11 1.7  0 timeout 900   1200 6000 0 error (7) 72   1900 790 0 timeout 900   1200 6800 0 timeout 900   230 12000 0
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i true 81     220 790    2 true 120    220 1000   2 false(unreach-call) 4.6 320 31 -16 timeout 900   820 6500 0 timeout 900   810 6100 0 unknown 890    990 9900   0 true 470     680 4700    2 true 450     670 3300    2 false(unreach-call) 3.7 300 29 -16 unknown 17   370 190 0 unknown .18  11 2.1  0 timeout 900   1100 5800 0 error (7) 58   2000 450 0 timeout 900   1100 5800 0 timeout 900   230 11000 0
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i true 90     220 890    2 true 110    220 1400   2 false(unreach-call) 4.5 320 39 -16 timeout 900   680 6000 0 timeout 900   700 6500 0 unknown 890    1200 7700   0 true 500     640 3300    2 true 470     640 3500    2 false(unreach-call) 3.5 280 26 -16 unknown 18   370 190 0 unknown .18  11 1.8  0 timeout 900   1100 6600 0 error (7) 60   2000 530 0 timeout 900   1100 6200 0 timeout 900   230 12000 0
floats-cdfpl/sine_4_true-unreach-call_true-termination.i true 25     55 330    2 true 69    55 870   2 false(unreach-call) 3.5 290 34 -16 timeout 900   590 8500 0 timeout 900   660 7500 0 unknown 890    310 10000   0 true 130     180 970    2 true 130     180 1000    2 false(unreach-call) 3.0 280 28 -16 true 6.9 350 68 2 unknown .16  11 2.1  0 timeout 900   860 6700 0 error (7) 51   630 460 0 timeout 900   870 5600 0 timeout 900   160 11000 0
floats-cdfpl/sine_5_true-unreach-call_true-termination.i true 2.0   41 24    2 true 5.6  48 69   2 false(unreach-call) 3.6 280 30 -16 timeout 900   540 5900 0 timeout 900   750 9200 0 unknown 890    310 9900   0 true 19     140 170    2 true 18     140 200    2 false(unreach-call) 2.9 270 25 -16 true 6.7 310 57 2 unknown .16  11 1.9  0 timeout 900   930 6200 0 error (7) 49   650 360 0 timeout 900   980 8600 0 timeout 900   160 11000 0
floats-cdfpl/sine_6_true-unreach-call_true-termination.i true 1.7   38 23    2 true 3.2  44 41   2 false(unreach-call) 3.5 280 29 -16 unknown 290   490 2900 0 timeout 900   900 7100 0 unknown 890    320 7000   0 true 6.7   130 85    2 true 7.0   130 68    2 false(unreach-call) 2.9 270 25 -16 true 7.2 350 69 2 unknown .19  11 1.8  0 timeout 900   840 6200 0 error (7) 51   640 430 0 timeout 900   840 6100 0 true 200   370 2700 2
floats-cdfpl/sine_7_true-unreach-call_true-termination.i true 1.4   40 17    2 true 3.5  49 40   2 false(unreach-call) 3.5 280 35 -16 unknown 750   600 5400 0 timeout (true) 900   820 7200 0 unknown 890    310 8100   0 true 6.7   130 76    2 true 6.7   130 90    2 false(unreach-call) 3.0 280 27 -16 true 7.5 340 63 2 unknown .16  11 1.8  0 timeout 900   810 6700 0 error (7) 48   640 360 0 timeout 900   800 7100 0 true 120   360 1500 2
floats-cdfpl/sine_8_true-unreach-call_true-termination.i true 1.3   39 16    2 true 3.0  46 34   2 false(unreach-call) 3.6 280 33 -16 timeout 900   560 6800 0 true 780   690 6800 2 unknown 890    310 8400   0 true 5.4   130 57    2 true 5.3   130 57    2 false(unreach-call) 3.1 270 24 -16 true 6.3 320 54 2 unknown .16  11 2.1  0 timeout 900   860 7500 0 error (7) 50   660 400 0 timeout 900   890 5500 0 timeout 900   160 11000 0
floats-cdfpl/square_4_true-unreach-call_true-termination.i true 200     68 2600    2 true 140    63 2100   2 false(unreach-call) 3.5 280 31 -16 timeout 900   680 6500 0 true 700   710 5300 2 unknown 890    250 7700   0 true 120     160 1100    2 true 130     160 980    2 false(unreach-call) 3.1 280 26 -16 true 6.4 350 58 2 unknown .18  11 1.8  0 true 610   820 5800 2 error (7) 39   370 300 0 true 620   840 4200 2 timeout 900   150 14000 0
floats-cdfpl/square_5_true-unreach-call_true-termination.i true 680     170 8900    2 true 120    63 1500   2 false(unreach-call) 3.6 290 30 -16 unknown 660   630 5000 0 true 620   610 5100 2 unknown 890    350 8900   0 true 110     150 870    2 true 110     150 780    2 false(unreach-call) 3.1 280 24 -16 true 6.1 330 56 2 unknown .16  11 1.7  0 true 450   780 3500 2 error (7) 31   380 270 0 true 450   770 4000 2 timeout 900   160 12000 0
floats-cdfpl/square_6_true-unreach-call_true-termination.i true 62     63 810    2 true 13    49 140   2 false(unreach-call) 3.4 280 34 -16 unknown 310   540 2500 0 true 440   610 3400 2 unknown 890    260 6600   0 true 21     130 240    2 true 22     130 180    2 false(unreach-call) 2.9 270 26 -16 true 6.0 320 54 2 unknown .16  11 2.1  0 true 330   840 2400 2 error (7) 34   380 240 0 true 330   830 2200 2 timeout 900   160 13000 0
floats-cdfpl/square_7_true-unreach-call_true-termination.i true 9.3   59 120    2 true 17    50 190   2 false(unreach-call) 3.7 290 28 -16 unknown 400   490 2800 0 timeout 900   610 6000 0 unknown 890    350 11000   0 true 27     130 320    2 true 30     130 300    2 false(unreach-call) 2.9 260 27 -16 true 6.6 330 54 2 unknown .16  11 1.6  0 true 150   720 1300 2 error (7) 32   370 250 0 true 160   740 1200 2 timeout 900   160 13000 0
floats-cdfpl/square_8_true-unreach-call_true-termination.i true .72  38 10    2 true 1.6  43 19   2 false(unreach-call) 3.5 280 28 -16 unknown 9.5 350 85 0 true 280   500 2800 2 unknown 890    200 9900   0 true 2.7   120 30    2 true 2.7   120 30    2 false(unreach-call) 3.0 280 26 -16 true 6.3 340 49 2 unknown .17  11 2.0  0 true 110   630 820 2 error (7) 42   380 320 0 true 110   650 830 2 true 52   370 480 2
floats-cbmc-regression/float-div1_true-unreach-call.i true .30  38 3.0  2 true 1.2  43 11   2 false(unreach-call) 5.1 310 42 -16 unknown 3.6 320 36 0 true 10   550 86 2 true 37    370 370   2 true 1.2   110 12    2 true 1.2   110 13    2 false(unreach-call) 4.0 290 35 -16 unknown 5.0 290 49 0 error .17  11 2.1  0 true 31   670 310 2 error (7) 110   560 1100 0 true 31   680 280 2 true 170   450 2100 2
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i true .94  130 11    2 true 1.3  47 13   2 false(unreach-call) 6.3 330 51 -16 assertion 1.8 130 18 0 true 7.4 410 58 2 true 25    2000 220   2 true .13  29 1.4  2 true .12  29 1.3  2 false(unreach-call) 4.0 290 37 -16 unknown 4.9 300 45 0 error .18  12 1.9  0 true 27   700 260 2 true 17   530 150 2 true 28   720 240 2 unknown 610   260 6700 0
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i true .094 22 .85 2 true .40 33 3.6 2 true 2.8 270 25 2 true 2.7 270 27 2 true 2.6 270 22 2 true 3.1  270 33   2 true .10  26 .69 2 true .070 26 .79 2 false(unreach-call) 2.8 270 25 -16 true 3.7 230 32 2 true .12  11 1.3  2 true 8.5 280 63 2 true 8.7 260 76 2 true 8.7 290 77 2 true 8.1 270 66 2
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true .72  33 9.3  2 true 3.0  39 34   2 true 3.6 280 32 2 true 3.1 270 27 2 true 11   310 140 2 true 300    330 3000   2 true 2.2   71 27    2 true 2.2   71 26    2 true 3.8 280 35 2 unknown 3.5 260 32 0 error .17  11 1.7  0 true 40   440 460 2 error (7) 31   360 420 0 true 40   450 550 2 true 180   450 2600 2
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i true .096 23 .92 2 true .41 33 3.5 2 true 2.7 270 23 2 true 2.8 270 26 2 true 2.6 270 23 2 true 3.2  260 30   2 true .087 26 .80 2 true .093 26 .80 2 false(unreach-call) 2.7 280 24 -16 true 3.8 230 34 2 true .14  11 1.4  2 true 8.4 270 73 2 true 8.9 260 73 2 true 8.4 270 76 2 true 8.0 270 67 2
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true .31  36 3.8  2 true 1.1  39 9.7 2 false(unreach-call) 5.0 320 45 -16 unknown 3.6 290 34 0 true 5.0 300 42 2 true 6.3  310 66   2 true .21  30 2.1  2 true .18  30 2.1  2 timeout 900   8100 11000 0 unknown 4.7 310 43 0 error .20  11 1.8  0 true 31   550 340 2 true 17   500 160 2 true 39   560 480 2 true 17   370 150 2
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i true .089 23 .71 2 true .39 33 4.3 2 true 2.9 270 28 2 true 2.9 270 26 2 true 2.4 240 19 2 true 3.2  250 28   2 true .10  26 .83 2 true .11  26 .63 2 false(unreach-call) 2.7 270 22 -16 true 3.7 240 33 2 true .15  11 1.3  2 true 9.3 300 85 2 true 11   340 96 2 true 9.2 310 84 2 true 7.8 280 64 2
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i true .080 22 .99 2 true .43 33 3.7 2 true 2.9 270 27 2 true 2.8 270 26 2 true 2.3 250 20 2 true 3.1  260 33   2 true .095 26 .84 2 true .10  26 .63 2 false(unreach-call) 2.8 260 23 -16 true 3.6 230 33 2 true .14  11 1.5  2 true 8.5 290 68 2 true 9.2 250 77 2 true 8.6 290 73 2 true 7.9 270 68 2
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true .19  28 1.5  2 true .90 37 8.6 2 true 3.5 280 31 2 true 2.8 270 26 2 true 2.9 260 27 2 true 4.3  260 39   2 true .12  27 .69 2 true .085 27 .74 2 true 3.7 280 33 2 true 3.9 240 38 2 true .19  11 2.2  2 true 9.1 310 70 2 true 9.7 290 78 2 true 9.6 320 79 2 true 15   280 140 2
floats-cbmc-regression/float-rounding1_true-unreach-call.i true .21  28 1.5  2 true .90 39 8.4 2 error 3.3 280 33 0 true 2.8 270 23 2 unknown 6.3 440 57 0 unknown 9.1  450 82   0 true .21  32 2.3  2 true .20  32 2.6  2 error 3.0 270 28 0 unknown 4.1 270 41 0 unknown .13  11 1.5  0 unknown 3.7 220 30 0 unknown 3.7 230 27 0 unknown 3.8 230 33 0 true 170   370 2500 2
floats-cbmc-regression/float-to-double1_true-unreach-call.i true .24  28 1.9  2 true .95 37 10   2 true 3.7 280 27 2 true 2.8 270 26 2 true 4.9 300 40 2 true 29    320 350   2 true .22  31 2.6  2 true .24  31 2.4  2 true 3.4 280 30 2 unknown 3.8 240 37 0 error .17  11 1.8  0 true 100   510 1200 2 true 17   280 200 2 true 82   490 910 2 true 170   300 2000 2
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i true .089 22 .64 2 true .39 33 3.8 2 true 2.7 270 25 2 true 2.9 270 24 2 true 2.3 230 21 2 true 3.1  260 32   2 true .079 26 .67 2 true .11  26 .68 2 true 2.7 260 24 2 true 3.7 230 38 2 true .14  10 1.5  2 true 8.2 280 63 2 true 8.7 260 79 2 true 8.5 280 69 2 true 8.3 280 82 2
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i true .11  22 .73 2 true .38 33 5.1 2 true 3.0 270 27 2 true 2.8 270 27 2 true 2.5 250 24 2 true 3.1  260 30   2 true .13  28 1.6  2 true .14  28 1.5  2 false(unreach-call) 2.8 280 25 -16 true 3.8 240 35 2 true .15  11 1.4  2 true 9.8 300 76 2 true 9.1 250 69 2 true 9.3 290 78 2 true 9.1 270 80 2
floats-cbmc-regression/float11_true-unreach-call_true-termination.i true .11  22 .82 2 true .40 33 3.8 2 true 2.8 270 22 2 true 2.7 270 25 2 true 2.3 250 19 2 true 3.4  250 33   2 true .12  27 1.0  2 true .090 27 .94 2 true 2.7 270 23 2 true 3.4 320 40 2 true .12  11 1.3  2 true 8.8 280 72 2 true 9.7 310 72 2 true 8.8 290 81 2 true 8.3 280 70 2
floats-cbmc-regression/float12_true-unreach-call_true-termination.i true .10  22 .66 2 true .43 33 3.5 2 true 2.8 270 26 2 true 2.8 270 24 2 true 2.9 270 28 2 true 7.7  290 85   2 true .21  31 2.4  2 true .18  32 2.4  2 true 2.7 270 27 2 unknown 5.7 310 48 0 unknown .18  11 1.8  0 true 13   310 150 2 true 14   280 140 2 true 13   310 140 2 true 8.0 270 69 2
floats-cbmc-regression/float13_true-unreach-call_true-termination.i true .12  24 1.0  2 true .44 33 3.9 2 true 2.8 270 26 2 true 2.8 270 25 2 true 2.4 250 23 2 true 3.2  250 27   2 true .077 26 .74 2 true .10  26 .90 2 false(unreach-call) 2.7 270 22 -16 true 3.8 240 38 2 true .12  11 1.6  2 true 9.2 290 82 2 true 11   350 100 2 true 9.3 290 74 2 true 8.5 280 81 2
floats-cbmc-regression/float14_true-unreach-call.i true .17  28 1.9  2 true .90 37 7.8 2 true 3.7 280 36 2 true 2.8 270 27 2 true 3.1 260 25 2 true 4.3  270 40   2 true .12  27 .88 2 true .079 27 1.0  2 false(unreach-call) 4.1 290 37 -16 unknown 3.6 240 32 0 error .19  11 1.9  0 true 9.3 300 84 2 true 9.9 300 79 2 true 9.1 310 83 2 true 15   280 120 2
floats-cbmc-regression/float18_true-unreach-call.i timeout 900     1700 10000    0 true 2.6  38 27   2 true 4.1 280 33 2 true 3.1 270 26 2 true 3.0 250 28 2 true 18    270 270   2 true .23  27 2.1  2 true .12  27 .98 2 true 7.7 460 64 2 true 3.8 240 33 2 true .18  11 2.0  2 unknown 3.7 220 29 0 unknown 3.8 230 32 0 unknown 3.8 220 31 0 true 39   710 360 2
floats-cbmc-regression/float19_true-unreach-call.i true .19  28 1.4  2 true .91 37 9.0 2 false(unreach-call) 5.3 320 40 -16 unknown 3.0 280 27 0 true 4.6 300 43 2 true 7.3  300 78   2 true .15  29 2.3  2 true .15  28 1.9  2 false(unreach-call) 3.8 280 33 -16 unknown 3.7 250 34 0 error .18  11 1.8  0 true 10   290 97 2 true 9.8 270 84 2 true 10   290 96 2 true 20   290 150 2
floats-cbmc-regression/float1_true-unreach-call_true-termination.i true .11  22 .52 2 true .39 33 4.2 2 true 2.7 270 27 2 true 2.8 270 27 2 true 2.5 260 19 2 true 3.1  260 30   2 true .10  26 .75 2 true .099 26 .78 2 false(unreach-call) 2.7 260 24 -16 true 3.6 230 32 2 true .12  11 1.3  2 true 8.6 280 78 2 true 8.4 260 77 2 true 8.5 280 77 2 true 7.8 270 70 2
floats-cbmc-regression/float20_true-unreach-call_true-termination.i true .14  26 1.2  2 true .42 35 5.6 2 true 2.9 270 28 2 true 2.9 270 29 2 true 2.4 250 24 2 true 24    250 270   2 true .36  52 4.7  2 true .36  52 4.4  2 false(unreach-call) 2.8 270 24 -16 false(unreach-call) 6.2 330 57 -16 unknown .19  11 2.1  0 true 14   390 120 2 true 39   490 370 2 true 13   390 140 2 true 10   270 90 2
floats-cbmc-regression/float21_true-unreach-call.i true .27  30 2.6  2 true 1.1  39 12   2 false(unreach-call) 4.9 300 39 -16 unknown 3.2 280 26 0 true 5.1 300 49 2 true 30    310 370   2 true .29  35 3.5  2 true .28  35 2.9  2 false(unreach-call) 3.7 280 35 -16 unknown 4.1 270 39 0 error .18  11 1.8  0 true 68   580 740 2 true 63   630 730 2 true 62   600 660 2 true 170   570 2100 2
floats-cbmc-regression/float22_true-unreach-call_true-termination.i true .11  23 .86 2 true .44 33 4.0 2 error 3.5 290 29 0 unknown 3.0 290 28 0 false(unreach-call) 4.7 300 39 -16 unknown 18    51 260   0 true .60  58 7.2  2 true .56  58 7.3  2 false(unreach-call) 2.9 270 27 -16 true 3.8 250 37 2 true .15  11 1.4  2 true 280   1100 2900 2 timeout 900   1000 9800 0 true 65   690 690 2 true 12   320 100 2
floats-cbmc-regression/float2_true-unreach-call_true-termination.i true .095 22 .93 2 true .40 33 4.8 2 true 2.7 270 25 2 true 2.7 270 22 2 true 2.3 250 23 2 true 3.2  240 28   2 true .16  26 1.3  2 true .12  26 1.3  2 true 2.9 270 24 2 true 3.6 230 32 2 true .15  11 1.3  2 true 8.8 300 67 2 true 8.9 260 75 2 true 9.1 310 74 2 true 7.9 270 74 2
floats-cbmc-regression/float3_true-unreach-call_true-termination.i true .11  24 1.1  2 true .44 33 4.0 2 error 3.3 280 34 0 true 2.8 270 24 2 true 2.3 240 21 2 true 7.5  250 85   2 true .39  56 4.7  2 true .43  56 5.0  2 false(unreach-call) 2.9 270 24 -16 true 5.9 310 47 2 unknown .18  11 1.6  0 true 12   350 110 2 true 13   300 120 2 true 12   340 130 2 true 8.6 290 83 2
floats-cbmc-regression/float4_true-unreach-call.i true 11     45 130    2 true 14    49 170   2 true 3.8 270 34 2 true 3.2 270 27 2 true 27   330 340 2 true 310    590 3400   2 true 7.4   110 87    2 true 7.4   110 100    2 true 4.0 280 33 2 unknown 3.9 270 35 0 error .17  11 1.9  0 true 74   490 960 2 error (7) 64   410 770 0 true 73   480 880 2 true 250   480 3000 2
floats-cbmc-regression/float5_true-unreach-call_true-termination.i true .12  23 .77 2 true .42 33 4.8 2 true 2.7 270 23 2 true 2.7 270 25 2 true 2.4 260 20 2 true 16    260 240   2 true .24  31 2.2  2 true .22  31 2.9  2 true 3.0 280 26 2 true 6.8 330 63 2 unknown .17  11 1.9  0 true 21   320 230 2 true 28   280 300 2 true 21   320 220 2 true 8.7 280 78 2
floats-cbmc-regression/float6_true-unreach-call_true-termination.i true .099 23 1.1  2 true .43 33 4.2 2 true 3.0 280 29 2 true 3.0 270 30 2 true 2.5 250 22 2 true 3.5  260 34   2 true .16  29 2.1  2 true .19  29 2.0  2 true 3.2 260 27 2 unknown 6.1 300 50 0 unknown .16  11 2.1  0 true 9.5 300 79 2 true 14   470 140 2 true 10   300 85 2 true 8.6 280 69 2
floats-cbmc-regression/float8_true-unreach-call.i true .55  30 5.7  2 true 1.4  37 14   2 true 3.9 300 37 2 true 2.8 270 26 2 true 14   300 150 2 true 7.5  340 81   2 true .64  38 7.9  2 true .66  38 7.6  2 true 3.7 280 32 2 unknown 4.7 280 38 0 error .17  11 2.1  0 true 10   310 82 2 true 8.4 260 72 2 true 10   310 90 2 true 170   300 2200 2
floats-cbmc-regression/float_lib1_true-unreach-call.i true 6.6   34 72    2 true 1.1  39 9.5 2 error (parsing failed) 1.7 140 15 0 assertion 1.6 130 14 0 error (parsing failed) 1.7 130 16 0 unknown 3.9  150 47   0 true .70  27 6.6  2 true .72  27 7.4  2 error (parsing failed) 1.7 130 15 0 unknown 3.2 210 32 0 error .18  11 1.6  0 error (7) 8.1 250 68 0 error (7) 9.1 260 70 0 error (7) 8.1 260 68 0 true 12   190 110 2
floats-cbmc-regression/float_lib2_true-unreach-call.i true .24  29 2.0  2 true 1.0  38 11   2 true 4.2 310 36 2 true 3.2 270 30 2 true 2.9 250 24 2 true 4.4  260 43   2 true .11  27 .99 2 true .095 27 .91 2 false(unreach-call) 3.9 290 34 -16 unknown 4.1 250 37 0 error .16  11 2.2  0 true 13   490 120 2 true 19   570 190 2 true 13   500 110 2 true 16   310 130 2
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c error (134) .095 22 .72 0 false(unreach-call) .25 33 2.3 1 false(unreach-call) 3.6 280 28 1 false(unreach-call) 3.5 280 32 1 false(unreach-call) 2.8 260 26 1 false(unreach-call) .41 48 4.8 0 false(unreach-call) .66  42 5.6  1 false(unreach-call) .61  42 5.6  1 exception 2.4 260 21 0 unknown 5.0 290 44 0 false(unreach-call) .15  11 1.6  1 false(unreach-call) 9.1 270 77 1 false(unreach-call) 11   290 100 1 false(unreach-call) 12   350 110 1 false(unreach-call) 11   290 100 1
float-benchs/cast_union_loose_false-unreach-call_true-termination.c false(unreach-call) .13  26 1.2  1 false(unreach-call) .26 33 2.7 1 false(unreach-call) 4.0 310 33 1 false(unreach-call) 3.6 300 32 0 false(unreach-call) 3.4 270 30 1 false(unreach-call) .51 49 5.5 1 false(unreach-call) 1.2   51 8.5  1 false(unreach-call) 1.2   51 9.9  1 false(unreach-call) 2.9 260 28 1 unknown 5.6 320 44 0 false(unreach-call) .18  11 1.8  1 false(unreach-call) 9.2 280 87 1 false(unreach-call) 11   270 97 1 false(unreach-call) 9.6 290 85 1 false(unreach-call) 11   290 92 1
float-benchs/cast_union_tight_false-unreach-call_true-termination.c false(unreach-call) .15  24 1.1  1 false(unreach-call) .29 34 2.2 1 false(unreach-call) 3.5 290 31 1 false(unreach-call) 3.2 290 29 0 false(unreach-call) 3.1 280 29 1 false(unreach-call) 1.2  48 14   1 false(unreach-call) 1.2   51 12    1 false(unreach-call) 1.2   51 12    1 false(unreach-call) 2.8 270 27 1 unknown 5.1 310 41 0 unknown .15  11 1.8  0 false(unreach-call) 9.4 290 87 1 false(unreach-call) 15   290 140 1 false(unreach-call) 9.7 290 79 1 false(unreach-call) 12   290 94 1
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c false(unreach-call) .17  27 1.2  1 false(unreach-call) .28 34 2.4 1 false(unreach-call) 3.4 280 31 1 false(unreach-call) 3.4 300 27 1 false(unreach-call) 2.6 260 25 1 false(unreach-call) 17    66 220   1 false(unreach-call) .35  42 3.9  1 false(unreach-call) .33  42 3.7  1 false(unreach-call) 3.0 280 27 1 unknown 6.0 320 48 0 false(unreach-call) .20  14 1.8  1 false(unreach-call) 8.6 310 67 1 false(unreach-call) 11   300 110 1 false(unreach-call) 8.7 300 80 1 false(unreach-call) 7.4 290 70 1
float-benchs/inv_Newton_false-unreach-call.c timeout 900     820 6800    0 error (42) 870    250 6800   0 false(unreach-call) 4.2 320 37 0 unknown 4.3 370 41 0 false(unreach-call) 3.8 350 38 1 unknown 890    340 7300   0 timeout 900     1300 6000    0 timeout 900     1100 6300    0 timeout 900   4200 11000 0 unknown 5.7 310 57 0 unknown .17  11 2.2  0 timeout 900   1800 5800 0 error (7) 64   420 580 0 timeout 900   1700 6300 0 unknown 110   220 1400 0
float-benchs/inv_square_false-unreach-call_true-termination.c false(unreach-call) .17  27 1.1  1 false(unreach-call) .26 35 2.2 1 false(unreach-call) 3.5 290 32 1 false(unreach-call) 3.4 300 33 1 false(unreach-call) 2.6 260 23 1 false(unreach-call) .46 40 5.6 1 false(unreach-call) .32  38 3.3  1 false(unreach-call) .30  39 3.0  1 false(unreach-call) 3.1 280 30 1 unknown 5.4 310 51 0 unknown .16  11 2.0  0 false(unreach-call) 8.5 310 70 1 false(unreach-call) 9.0 280 86 1 false(unreach-call) 8.6 310 75 1 false(unreach-call) 7.5 290 61 1
float-benchs/nan_double_false-unreach-call_true-termination.c false(unreach-call) .10  22 1.0  1 false(unreach-call) .23 33 2.2 1 true 2.9 270 26 -32 true 2.8 270 24 -32 false(unreach-call) 2.5 250 20 1 false(unreach-call) .36 48 4.8 0 false(unreach-call) .20  31 2.4  1 false(unreach-call) .20  32 2.0  1 true 2.8 280 23 -32 unknown 4.9 290 42 0 false(unreach-call) .18  11 1.6  1 false(unreach-call) 4.1 240 34 1 false(unreach-call) 8.1 250 68 1 false(unreach-call) 4.1 240 34 1 false(unreach-call) 7.3 270 70 1
float-benchs/nan_float_false-unreach-call_true-termination.c false(unreach-call) .11  22 .88 1 false(unreach-call) .25 33 2.2 1 true 2.8 270 24 -32 true 2.7 270 24 -32 false(unreach-call) 2.6 250 22 1 false(unreach-call) .35 48 5.0 0 false(unreach-call) .21  31 1.9  1 false(unreach-call) .20  31 1.8  1 true 2.8 260 24 -32 unknown 4.6 290 46 0 false(unreach-call) .15  11 1.7  1 false(unreach-call) 4.0 240 31 1 false(unreach-call) 8.0 250 70 1 false(unreach-call) 4.1 240 35 1 false(unreach-call) 7.4 280 65 1
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c false(unreach-call) 3.2   260 34    1 false(unreach-call) 2.7  240 30   1 false(unreach-call) 4.0 300 39 1 unknown 3.3 280 30 0 false(unreach-call) 7.4 380 76 1 false(unreach-call) 110    410 1100   1 false(unreach-call) 5.5   320 63    0 false(unreach-call) 5.7   320 51    0 false(unreach-call) 3.1 270 29 1 unknown 8.4 480 75 0 unknown .20  11 1.9  0 false(unreach-call) 370   2100 4100 1 error (7) 32   2500 230 0 false(unreach-call) 640   2500 6300 1 false(unreach-call) 32   350 400 1
float-benchs/sqrt_poly2_false-unreach-call.c false(unreach-call) .64  46 6.6  1 false(unreach-call) .72 50 7.5 1 false(unreach-call) 4.0 290 34 1 false(unreach-call) 6.3 470 58 1 false(unreach-call) 5.4 390 55 1 false(unreach-call) 290    340 2800   1 false(unreach-call) 5.4   280 46    1 false(unreach-call) 5.4   280 55    1 false(unreach-call) 3.1 270 27 1 unknown 6.4 330 51 0 unknown .16  11 1.9  0 false(unreach-call) 15   600 120 1 error (7) 92   700 730 0 false(unreach-call) 15   610 130 1 false(unreach-call) 22   450 220 1
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c timeout 900     610 6500    0 true 3.0  33 36   2 error 110   3700 1200 0 out of memory 630   15000 8500 0 true 3.3 260 31 2 unknown 890    1200 6700   0 true .66  26 7.3  2 true 4.2   260 42    2 false(unreach-call) 81   3700 880 -16 unknown 5.6 310 51 0 true .16  11 1.4  2 timeout 900   3400 10000 0 timeout 900   1900 9800 0 timeout 900   7300 11000 0 true 79   1000 880 2
float-benchs/Rump_double_true-unreach-call_true-termination.c true .15  27 1.1  2 true .41 33 3.8 2 true 2.7 270 26 2 true 2.8 270 26 2 true 2.3 250 18 2 true 3.3  300 30   2 true .077 26 .84 2 true .11  26 .67 2 false(unreach-call) 2.9 280 27 -16 true 4.0 250 38 2 true .14  11 1.4  2 true 19   1000 200 2 error (7) 22   1500 220 0 true 20   990 190 2 true 8.1 280 58 2
float-benchs/Rump_float_true-unreach-call_true-termination.c true .12  24 .88 2 true .43 33 3.6 2 true 2.7 270 24 2 true 2.8 270 27 2 true 2.4 250 21 2 true 3.1  270 29   2 true .085 26 .78 2 true .11  26 .64 2 false(unreach-call) 2.9 280 24 -16 true 4.0 250 35 2 true .14  11 1.6  2 true 11   440 100 2 error (7) 21   570 130 0 true 11   440 110 2 true 8.4 280 75 2
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c true .096 22 .82 2 true .39 33 4.4 2 true 2.7 280 29 2 true 2.7 270 27 2 true 2.4 250 18 2 true 3.1  270 28   2 true .073 26 .98 2 true .11  26 .75 2 true 2.9 280 26 2 true 3.9 240 38 2 true .16  11 1.5  2 true 8.9 290 81 2 true 11   280 96 2 true 8.7 290 76 2 true 8.0 270 70 2
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c true .11  22 .77 2 true .40 33 5.1 2 true 2.8 270 25 2 true 2.8 270 23 2 true 2.3 240 21 2 true 3.1  260 29   2 true .070 26 .72 2 true .077 26 .79 2 true 2.9 280 28 2 true 4.0 250 35 2 true .14  11 1.8  2 true 8.9 290 69 2 true 8.9 250 81 2 true 8.8 290 80 2 true 8.0 270 75 2
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c true .10  22 .73 2 true .41 33 4.6 2 true 2.8 270 25 2 true 2.7 270 24 2 true 2.4 240 20 2 true 3.0  260 27   2 true .074 26 .75 2 true .078 26 .72 2 false(unreach-call) 2.8 280 26 -16 true 3.9 240 41 2 true .14  11 1.7  2 true 8.7 290 69 2 true 8.8 260 79 2 true 8.8 290 78 2 true 8.0 270 77 2
float-benchs/arctan_Pade_true-unreach-call_true-termination.c true 55     260 670    2 true 94    240 940   2 false(unreach-call) 4.1 290 35 -16 unknown 8.0 460 65 0 true 87   560 810 2 unknown 890    1100 11000   0 true 130     1200 910    2 true 120     1200 1000    2 false(unreach-call) 3.2 270 25 -16 unknown 6.4 330 55 0 unknown .17  11 2.1  0 error (7) 140   2700 1200 0 error (7) 51   840 340 0 error (7) 410   2700 4500 0 true 160   540 1900 2
float-benchs/bary_diverge_true-unreach-call_true-termination.c timeout 900     460 11000    0 error (42) 870    1200 9100   0 timeout 900   7500 9700 0 timeout 900   1800 10000 0 timeout 900   4700 9200 0 unknown 890    260 10000   0 timeout 900     1000 7800    0 timeout 900     1000 8500    0 timeout 900   2100 14000 0 unknown 6.7 330 56 0 timeout (timeout) 900     69 11000    0 timeout 900   3100 9600 0 error (7) 15   280 140 0 timeout 900   3000 12000 0 true 84   820 850 2
float-benchs/cast_float_union_true-unreach-call.c true .13  23 .72 2 true .44 33 3.6 2 true 3.1 300 27 2 true 2.7 260 27 2 true 2.4 250 24 2 true 3.1  250 32   2 true .075 26 1.0  2 true .11  26 .67 2 true 2.6 270 22 2 true 4.1 250 36 2 true .15  11 1.3  2 true 4.1 240 37 2 true 4.8 270 35 2 true 4.4 260 37 2 true 7.3 260 59 2
float-benchs/cos_polynomial_true-unreach-call_true-termination.c true 7.0   110 60    2 true 11    110 94   2 false(unreach-call) 4.1 290 33 -16 unknown 330   830 1800 0 timeout 900   1600 5900 0 unknown 890    610 8200   0 true 17     540 170    2 true 17     540 180    2 false(unreach-call) 3.3 260 27 -16 unknown 6.5 320 59 0 unknown .19  11 1.9  0 timeout 900   2900 6600 0 error (7) 130   960 1000 0 timeout 900   2900 6500 0 true 100   590 1000 2
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c true .70  32 8.0  2 error (42) 870    3200 5700   0 timeout 900   4200 10000 0 timeout 900   3900 11000 0 timeout 900   2800 8400 0 unknown 890    270 9500   0 timeout 900     1800 11000    0 timeout 900     1800 11000    0 true 6.2 370 53 2 unknown 6.2 320 53 0 timeout (timeout) 900     1800 8000    0 timeout 900   5400 11000 0 timeout 900   4700 11000 0 timeout 900   4900 11000 0 true 790   6700 9400 2
float-benchs/divmul_diverge_true-unreach-call_true-termination.c timeout 900     400 10000    0 error (42) 870    3100 6100   0 timeout 900   4200 12000 0 timeout 900   4000 11000 0 timeout 900   2700 9200 0 unknown 890    270 13000   0 timeout 900     2400 11000    0 timeout 900     2400 11000    0 true 5.7 310 46 2 unknown 5.4 310 49 0 timeout (timeout) 900     1800 8500    0 timeout 900   5400 12000 0 timeout 900   4800 12000 0 timeout 900   4900 11000 0 true 780   6500 11000 2
float-benchs/drift_tenth_true-unreach-call_true-termination.c true .42  35 5.4  2 true 1.2  33 10   2 true 3.5 270 30 2 true 4.0 280 34 2 true 2.4 250 21 2 unknown 890    490 7700   0 true .10  26 .93 2 true .26  37 2.9  2 true 8.1 460 62 2 true 4.0 240 37 2 true .14  11 1.6  2 error (7) 770   850 7900 0 timeout 900   660 9500 0 error (7) 760   840 9000 0 false(unreach-call) 18   530 150 -16
float-benchs/exp_loop_true-unreach-call.c true 19     210 220    2 true 3.4  42 39   2 false(unreach-call) 4.7 300 36 -16 unknown 4.0 330 41 0 true 790   8500 8000 2 unknown 890    410 8100   0 true 17     110 190    2 true 17     110 190    2 false(unreach-call) 4.5 290 40 -16 unknown 6.4 310 53 0 unknown .20  11 1.8  0 timeout 900   1300 8600 0 error (7) 430   990 4400 0 timeout 900   1400 13000 0 unknown 680   220 7600 0
float-benchs/feedback_diverge_true-unreach-call_true-termination.c timeout 900     1600 12000    0 error (42) 870    1100 8500   0 timeout 900   7100 8600 0 timeout 900   3900 11000 0 timeout 900   1900 8800 0 unknown 890    330 8200   0 timeout 900     2600 10000    0 timeout 900     2600 10000    0 timeout 910   4000 9900 0 unknown 6.2 340 59 0 timeout (timeout) 900     1800 8700    0 timeout 900   5300 13000 0 timeout 900   4900 11000 0 timeout 900   4700 11000 0 timeout 900   6100 10000 0
float-benchs/filter1_true-unreach-call_true-termination.c timeout 900     630 8900    0 error (42) 870    1600 11000   0 true 3.5 280 32 2 true 3.5 270 32 2 true 18   790 130 2 unknown 890    280 8400   0 timeout 900     1400 7800    0 true 3.4   140 45    2 true 6.5 410 47 2 unknown 6.1 320 56 0 timeout (timeout) 900     2000 11000    0 error (7) 530   1400 4200 0 error (7) 37   380 410 0 error (7) 570   1100 5400 0 true 31   660 260 2
float-benchs/filter2_alt_true-unreach-call.c timeout 900     180 12000    0 error (42) 870    180 11000   0 error 4.3 320 38 0 unknown 6.1 340 71 0 timeout 900   1200 7000 0 unknown 890    230 9700   0 timeout 900     560 6800    0 timeout 900     670 9000    0 timeout 900   1500 12000 0 unknown 6.8 330 55 0 timeout (timeout) 900     70 10000    0 timeout 900   1300 9600 0 error (7) 16   320 170 0 timeout 900   1300 7600 0 timeout 900   380 13000 0
float-benchs/filter2_iterated_true-unreach-call.c timeout 900     620 8000    0 error (42) 870    1300 4900   0 error 4.1 300 39 0 unknown 6.1 510 59 0 timeout 900   2400 8200 0 unknown 900    6500 8200   0 timeout 900     3400 7200    0 timeout 900     4000 7900    0 timeout 900   1800 11000 0 unknown 6.7 350 58 0 timeout (timeout) 900     9600 11000    0 error (7) 35   2200 370 0 error (7) 18   2200 180 0 error (7) 39   2200 530 0 unknown 400   540 5100 0
float-benchs/filter2_reinit_true-unreach-call_true-termination.c timeout 900     530 8400    0 error (42) 870    490 8400   0 timeout 900   3400 14000 0 timeout 900   3900 12000 0 timeout 900   3000 8100 0 unknown 890    250 9500   0 timeout 900     1400 6300    0 timeout 900     1600 6500    0 true 200   2400 2100 2 unknown 5.8 300 54 0 timeout (timeout) 900     69 11000    0 timeout 900   2000 7400 0 error (7) 49   430 390 0 timeout 900   2100 7900 0 timeout 900   1000 11000 0
float-benchs/filter2_set_true-unreach-call_true-termination.c timeout 900     380 7200    0 error (42) 870    450 13000   0 false(unreach-call) 5.1 310 40 -16 unknown 8.6 470 84 0 timeout 910   3800 8300 0 unknown 890    450 7500   0 timeout 900     1900 7300    0 timeout 900     1200 9000    0 false(unreach-call) 5.4 290 41 -16 unknown 7.2 350 58 0 unknown .18  12 2.0  0 error (7) 400   3400 4200 0 error (7) 30   530 250 0 error (7) 460   3400 4300 0 timeout 900   540 11000 0
float-benchs/filter2_true-unreach-call_true-termination.c timeout 900     640 7600    0 error (42) 870    480 8600   0 true 34   1400 300 2 true 35   1400 290 2 timeout 900   3900 9700 0 unknown 890    550 8500   0 timeout 900     1700 9000    0 timeout 900     1400 6000    0 true 210   2800 2300 2 unknown 5.6 300 47 0 timeout (timeout) 900     68 11000    0 timeout 900   2100 12000 0 error (7) 29   400 240 0 timeout 900   2100 9100 0 timeout 900   530 11000 0
float-benchs/filter_iir_true-unreach-call.c timeout 900     310 9900    0 error (42) 870    750 8600   0 true 3.3 280 28 2 true 3.3 280 30 2 true 2.7 260 23 2 unknown 890    750 8400   0 timeout 900     2300 7500    0 timeout 900     1800 10000    0 false(unreach-call) 3.7 280 33 -16 unknown 7.3 360 56 0 timeout (timeout) 900     64 11000    0 timeout 900   1500 8200 0 timeout 900   2000 6900 0 timeout 900   1800 8500 0 unknown 810   410 12000 0
float-benchs/float_double_true-unreach-call_true-termination.c true .12  22 .83 2 true .44 33 4.0 2 true 2.8 270 25 2 true 2.7 270 23 2 true 2.3 240 21 2 true 3.1  250 30   2 true .10  26 .62 2 true .098 26 .80 2 false(unreach-call) 2.8 270 25 -16 true 3.8 230 41 2 true .17  11 1.4  2 true 8.6 280 73 2 true 8.6 270 71 2 true 9.3 290 73 2 true 8.3 270 75 2
float-benchs/image_filter_true-unreach-call.c timeout 900     1100 9200    0 true 850    2800 6000   2 timeout 900   4700 10000 0 timeout 900   4700 11000 0 out of memory 690   15000 7800 0 unknown 890    3100 7200   0 true 660     3000 4200    2 true 750     5700 5000    2 timeout 910   4300 10000 0 unknown 10   640 86 0 unknown .25  12 3.0  0 timeout 900   6900 8400 0 timeout 900   6800 10000 0 timeout 910   13000 3500 0 unknown 870   2300 9900 0
float-benchs/interpolation2_true-unreach-call_true-termination.c true .42  30 4.3  2 true 1.2  36 13   2 false(unreach-call) 4.1 310 35 -16 unknown 6.3 340 68 0 timeout 900   660 9800 0 unknown 630    320 7200   0 true 3.1   92 45    2 true 5.5   93 65    2 false(unreach-call) 3.7 270 32 -16 unknown 5.8 320 53 0 unknown .20  11 2.0  0 timeout 900   760 10000 0 error (7) 64   380 660 0 timeout 900   770 10000 0 unknown 820   220 10000 0
float-benchs/interpolation_true-unreach-call_true-termination.c true .28  27 2.4  2 true 1.1  36 11   2 false(unreach-call) 4.2 310 33 -16 unknown 8.2 330 92 0 true 11   410 140 2 unknown 130    310 1400   0 true 1.3   71 16    2 true 2.3   73 34    2 false(unreach-call) 3.8 270 27 -16 unknown 5.9 320 45 0 unknown .17  11 1.7  0 timeout 900   930 8500 0 error (7) 650   760 6900 0 timeout 900   990 11000 0 timeout 900   220 11000 0
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c true .28  30 2.9  2 true .71 36 6.9 2 false(unreach-call) 3.8 290 37 -16 false(unreach-call) 3.6 310 36 -16 true 5.5 300 64 2 false(unreach-call) 320    270 3100   -16 true .75  67 8.6  2 true .73  67 9.4  2 false(unreach-call) 2.9 260 27 -16 unknown 5.9 320 50 0 unknown .18  11 1.9  0 error (7) 150   2400 1400 0 error (7) 69   340 900 0 error (7) 100   2400 880 0 true 13   300 120 2
float-benchs/inv_square_int_true-unreach-call_true-termination.c true .13  27 1.3  2 true .46 35 4.0 2 false(unreach-call) 3.5 290 36 -16 unknown 3.1 290 30 0 true 3.3 280 32 2 true 27    300 360   2 true .26  38 3.0  2 true .23  38 3.4  2 false(unreach-call) 3.0 270 28 -16 unknown 5.6 300 45 0 true .16  12 1.9  2 true 33   390 380 2 true 12   300 100 2 true 32   390 360 2 true 8.7 280 73 2
float-benchs/inv_square_true-unreach-call_true-termination.c true .15  26 1.0  2 true .48 35 4.4 2 false(unreach-call) 3.5 280 28 -16 unknown 3.1 300 30 0 true 3.4 280 34 2 true 5.2  280 56   2 true .23  34 2.6  2 true .24  34 2.2  2 false(unreach-call) 3.0 280 30 -16 true 5.8 310 48 2 unknown .18  11 1.8  0 true 61   400 710 2 true 12   290 110 2 true 62   410 700 2 true 8.6 280 73 2
float-benchs/loop_true-unreach-call.c timeout 900     330 7400    0 out of memory 480    15000 6200   0 timeout 900   4400 8100 0 timeout 900   4400 7300 0 timeout 900   3500 10000 0 unknown 890    320 10000   0 timeout 900     1300 11000    0 timeout 900     1400 13000    0 timeout 900   5400 12000 0 unknown 5.3 300 44 0 true 11     290 150    2 timeout 900   1100 10000 0 error (7) 70   560 820 0 timeout 900   1000 8900 0 true 43   600 440 2
float-benchs/mea8000_true-unreach-call.c timeout 900     2900 9700    0 error (134) 230    13000 2500   0 timeout 900   4000 12000 0 timeout 900   4100 9900 0 timeout 900   4900 9800 0 unknown 890    1900 11000   0 timeout 900     1400 12000    0 timeout 900     1700 11000    0 timeout 910   4900 13000 0 unknown 15   730 120 0 timeout (timeout) 900     67 11000    0 timeout 900   5600 12000 0 error (7) 780   5100 9800 0 timeout 900   5300 11000 0 unknown 780   670 11000 0
float-benchs/nan_double_range_true-unreach-call_true-termination.c true .11  22 .68 2 true .42 33 3.6 2 true 2.7 270 25 2 true 2.8 270 28 2 true 3.0 270 24 2 true 3.6  280 37   2 true .17  28 1.4  2 true .13  28 1.7  2 true 2.9 260 26 2 unknown 5.5 300 47 0 unknown .18  11 2.0  0 true 8.9 290 68 2 true 8.2 250 65 2 true 8.6 290 68 2 true 8.0 270 70 2
float-benchs/nan_float_range_true-unreach-call_true-termination.c true .12  22 .81 2 true .43 33 4.4 2 true 2.8 270 25 2 true 2.8 270 28 2 true 3.0 270 28 2 true 3.6  270 35   2 true .16  28 1.7  2 true .15  28 1.5  2 true 2.8 260 24 2 unknown 5.0 300 42 0 unknown .18  11 1.9  0 true 10   300 91 2 true 8.7 260 80 2 true 10   300 93 2 true 8.4 270 75 2
float-benchs/rlim_exit_true-unreach-call_true-termination.c timeout 900     1800 10000    0 error (134) 180    14000 2600   0 timeout 900   4300 9300 0 timeout 900   3900 11000 0 timeout 900   3000 11000 0 unknown 890    200 9900   0 timeout 900     2300 11000    0 timeout 900     2300 9100    0 true 8.9 470 75 2 unknown 5.7 320 51 0 timeout (timeout) 900     61 12000    0 timeout 900   5200 12000 0 timeout 900   5700 14000 0 timeout 900   3000 13000 0 true 780   3400 10000 2
float-benchs/rlim_invariant_true-unreach-call_true-termination.c timeout 900     1800 11000    0 error (42) 870    1300 7900   0 true 3.7 280 33 2 true 3.7 280 37 2 true 8.8 500 70 2 unknown 890    440 8600   0 timeout 900     870 7800    0 true 1.2   61 16    2 true 11   480 81 2 unknown 5.8 310 48 0 timeout (timeout) 900     61 11000    0 error (7) 770   910 8400 0 error (7) 60   440 700 0 timeout 900   930 12000 0 true 22   470 170 2
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call_true-termination.c true 820     310 8000    2 error (1) 870    310 8900   0 error 3.2 290 26 0 error 2.7 270 22 0 timeout 900   1200 8500 0 unknown 890    1700 5600   0 timeout 900     4200 6400    0 timeout 900     4200 6700    0 false(unreach-call) 5.0 310 42 -16 unknown 8.0 470 69 0 unknown .19  11 2.4  0 timeout 900   2400 5300 0 error (7) 33   2500 230 0 timeout 900   2000 6700 0 timeout 900   240 10000 0
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call_true-termination.c timeout 900     320 9200    0 error (1) 870    300 9900   0 error 2.7 270 24 0 error 2.6 270 25 0 timeout 900   1400 8300 0 unknown 890    1700 6900   0 timeout 900     3400 6400    0 timeout 900     3400 8600    0 false(unreach-call) 4.6 320 37 -16 unknown 8.2 480 74 0 unknown .17  11 2.0  0 timeout 900   2200 6000 0 error (7) 33   2500 250 0 timeout 900   2100 6300 0 timeout 900   240 12000 0
float-benchs/sin_interpolated_index_true-unreach-call_true-termination.c true 770     310 10000    2 error (1) 870    290 10000   0 false(unreach-call) 4.2 320 40 -16 unknown 3.2 280 29 0 timeout 900   720 11000 0 unknown 890    490 6100   0 timeout 900     740 8700    0 timeout 900     740 9200    0 false(unreach-call) 3.3 270 31 -16 unknown 8.5 470 76 0 unknown .17  11 2.1  0 timeout 900   2200 10000 0 error (7) 38   2500 290 0 timeout 900   2100 10000 0 timeout 900   250 12000 0
float-benchs/sin_interpolated_negation_true-unreach-call.c timeout 900     540 7000    0 error (42) 870    4300 5900   0 error 2.7 270 25 0 error 2.8 270 25 0 timeout 900   2700 7200 0 unknown 890    2100 6800   0 timeout 900     13000 10000    0 timeout 900     3100 6200    0 exception 34   1600 280 0 unknown 11   520 90 0 unknown .20  11 2.2  0 timeout 900   2600 5500 0 error (7) 22   2500 170 0 timeout 900   2400 5600 0 timeout 900   1700 9700 0
float-benchs/sin_interpolated_smallrange_true-unreach-call.c timeout 900     360 7100    0 error (42) 870    3000 6200   0 error 2.8 270 22 0 error 2.7 260 25 0 timeout 900   4000 9000 0 unknown 890    1800 6100   0 timeout 900     13000 8300    0 timeout 900     2700 6900    0 timeout 900   4600 11000 0 unknown 8.4 470 69 0 unknown .17  11 2.0  0 timeout 900   2300 5500 0 error (7) 33   2500 230 0 timeout 900   2700 5500 0 timeout 900   900 11000 0
float-benchs/sqrt_Householder_constant_true-unreach-call.c timeout 900     310 6800    0 true 3.4  33 36   2 error 3.8 290 35 0 true 7.5 440 58 2 true 3.9 260 29 2 unknown 890    1000 12000   0 true .49  27 5.5  2 true 240     1800 1900    2 false(unreach-call) 4.9 280 42 -16 unknown 6.3 330 59 0 true .14  11 2.0  2 error (7) 250   3100 2100 0 error (7) 94   1500 830 0 error (7) 250   3000 2600 0 true 200   1400 2500 2
float-benchs/sqrt_Householder_interval_true-unreach-call.c timeout 900     330 9400    0 error (42) 870    590 9700   0 false(unreach-call) 3.9 290 36 -16 unknown 6.0 520 50 0 timeout 900   1300 13000 0 unknown 890    620 7700   0 timeout 900     1900 6500    0 timeout 900     1500 6100    0 false(unreach-call) 3.1 260 28 -16 unknown 6.2 330 59 0 unknown .19  11 1.9  0 error (7) 150   2800 1500 0 error (7) 78   1600 690 0 error (7) 160   2800 1300 0 timeout 900   230 11000 0
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c timeout 900     330 6600    0 error (42) 870    3000 12000   0 false(unreach-call) 4.2 290 41 -16 unknown 5.5 540 53 0 timeout 900   2600 11000 0 unknown 890    1200 7200   0 timeout 900     3100 7900    0 timeout 900     1500 7800    0 false(unreach-call) 3.1 270 27 -16 unknown 6.2 320 59 0 unknown .17  11 1.8  0 error (7) 90   2600 760 0 error (7) 78   1700 550 0 error (7) 87   2600 910 0 timeout 900   440 13000 0
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c timeout 900     390 7100    0 error (42) 870    2000 8100   0 false(unreach-call) 4.1 290 38 -16 unknown 5.6 540 58 0 timeout 900   1800 11000 0 unknown 890    1100 7200   0 timeout 900     2500 9100    0 timeout 900     1200 6000    0 false(unreach-call) 3.1 260 26 -16 unknown 6.4 320 63 0 unknown .18  11 2.0  0 error (7) 87   2600 910 0 error (7) 99   1800 1000 0 error (7) 110   2700 1000 0 timeout 900   340 12000 0
float-benchs/sqrt_biNewton_pseudoconstant_true-unreach-call.c timeout 900     340 5800    0 error (42) 870    3300 10000   0 false(unreach-call) 4.2 290 35 -16 unknown 5.5 540 54 0 timeout 900   1900 10000 0 unknown 890    1400 7000   0 timeout 900     3600 8300    0 timeout 900     6400 7000    0 false(unreach-call) 3.2 270 26 -16 unknown 6.0 300 54 0 unknown .18  11 2.1  0 error (7) 84   2600 870 0 error (7) 100   1800 1100 0 error (7) 110   2700 990 0 timeout 900   460 11000 0
float-benchs/sqrt_poly_true-unreach-call_true-termination.c true 1.2   58 12    2 true 3.5  64 38   2 false(unreach-call) 3.7 290 33 -16 unknown 35   490 300 0 true 45   510 440 2 unknown 890    500 6900   0 true 5.9   310 61    2 true 5.8   310 56    2 false(unreach-call) 3.1 280 25 -16 unknown 5.7 330 57 0 unknown .17  11 1.9  0 true 240   1800 1700 2 error (7) 94   820 670 0 true 200   1900 1300 2 true 49   510 530 2
float-benchs/water_pid_true-unreach-call_true-termination.c timeout 900     900 8400    0 true 3.8  36 39   2 error 9.5 490 74 0 timeout 900   1300 10000 0 true 4.4 270 35 2 unknown 890    580 7600   0 true 2.6   27 32    2 true 4.8   210 57    2 false(unreach-call) 4.7 290 42 -16 unknown 5.5 300 45 0 true .16  11 1.8  2 error (7) 160   3000 1400 0 error (7) 71   1500 540 0 error (7) 130   3000 1200 0 true 56   1100 540 2
float-benchs/zonotope_2_true-unreach-call_true-termination.c timeout 900     340 8400    0 true 400    5500 4100   2 true 4.2 290 35 2 true 3.8 270 36 2 timeout 900   2300 6900 0 unknown 45    76 610   0 timeout 900     4000 12000    0 timeout 900     4100 9600    0 timeout 910   5000 11000 0 unknown 5.6 300 46 0 true 1.0   34 14    2 timeout 900   2800 7700 0 error (7) 200   580 1900 0 timeout 900   1800 8900 0 true 210   1800 2300 2
float-benchs/zonotope_3_true-unreach-call_true-termination.c timeout 900     1700 12000    0 error (134) 230    15000 3300   0 timeout 900   4200 11000 0 timeout 900   4100 8600 0 true 160   2300 1900 2 true 200    2300 2000   2 timeout 900     2700 10000    0 true 1.8   96 22    2 timeout 900   4900 12000 0 unknown 5.5 320 52 0 timeout (timeout) 900     73 12000    0 timeout 900   5400 14000 0 timeout 900   5200 12000 0 timeout 900   5300 13000 0 true 23   520 210 2
float-benchs/zonotope_loose_true-unreach-call_true-termination.c true .20  34 2.6  2 true .65 40 6.4 2 false(unreach-call) 3.5 280 32 -16 unknown 3.6 340 40 0 true 5.4 330 54 2 true 90    350 890   2 true 1.2   120 12    2 true 1.2   120 13    2 false(unreach-call) 3.1 280 29 -16 unknown 5.7 320 51 0 unknown .19  11 1.8  0 true 190   1500 1800 2 error (7) 74   760 760 0 error (7) 150   1200 1300 0 true 11   330 95 2
float-benchs/zonotope_tight_true-unreach-call_true-termination.c true .22  34 2.1  2 true .67 40 7.1 2 false(unreach-call) 3.6 290 36 -16 unknown 3.9 340 39 0 true 5.5 330 63 2 true 110    350 960   2 true 1.2   120 13    2 true 1.2   120 14    2 false(unreach-call) 3.3 280 28 -16 unknown 5.5 320 51 0 unknown .18  11 1.9  0 true 170   1300 1300 2 error (7) 72   740 660 0 true 190   1300 1600 2 true 11   340 100 2
floats-esbmc-regression/Double_div_true-unreach-call.i true 1.6   49 19    2 true 5.6  34 66   2 timeout 900   4200 10000 0 timeout 900   4100 9400 0 true 5.8 460 43 2 unknown 890    260 8000   0 true 130     100 1600    2 true 130     81 1600    2 timeout 900   4000 11000 0 unknown 5.2 300 46 0 true .17  11 1.5  2 error (7) 290   2700 2200 0 error (7) 51   890 560 0 error (7) 340   2800 2800 0 true 12   340 99 2
floats-esbmc-regression/Float_div_true-unreach-call.i true .43  32 4.4  2 true 2.8  33 27   2 timeout 900   4100 10000 0 timeout 900   4100 9100 0 true 3.4 260 28 2 unknown 890    610 12000   0 true .47  26 6.1  2 true .63  33 7.7  2 timeout 900   4000 13000 0 unknown 5.2 290 44 0 true .17  11 1.7  2 error (7) 190   600 1600 0 error (7) 84   530 800 0 error (7) 320   730 2700 0 true 12   300 88 2
floats-esbmc-regression/ceil_nondet_true-unreach-call.i true 3.6   89 46    2 true 6.9  57 81   2 error 3.6 290 34 0 false(unreach-call) 3.6 290 35 -16 unknown 5.9 410 47 0 unknown 17    460 170   0 true .32  38 3.9  2 true .29  38 3.5  2 error 3.1 280 27 0 unknown 4.2 290 43 0 unknown .095 11 .81 0 unknown 7.5 230 64 0 unknown 7.5 230 56 0 unknown 7.7 230 62 0 true 190   330 2100 2
floats-esbmc-regression/ceil_true-unreach-call.i true .45  32 3.9  2 true 1.9  39 20   2 true 4.1 280 40 2 false(unreach-call) 3.6 300 33 -16 true 3.1 250 25 2 true 4.3  270 48   2 true .15  27 1.8  2 true .15  27 2.1  2 false(unreach-call) 4.0 280 35 -16 unknown 3.8 250 38 0 error .13  11 1.6  0 unknown 3.8 220 29 0 unknown 3.9 230 29 0 unknown 4.0 220 31 0 true 18   290 150 2
floats-esbmc-regression/copysign_true-unreach-call.i true .36  30 2.4  2 true 1.4  38 11   2 true 4.9 290 39 2 true 3.5 270 28 2 true 3.0 250 28 2 true 4.5  270 48   2 true .088 27 .98 2 true .12  27 .94 2 false(unreach-call) 4.8 300 41 -16 unknown 4.0 270 37 0 error .14  11 1.4  0 unknown 3.7 220 31 0 unknown 3.6 230 31 0 unknown 3.7 230 31 0 true 17   280 130 2
floats-esbmc-regression/digits_for_true-unreach-call.i true 620     760 7500    2 true 2.9  33 30   2 assertion 2.4 270 22 0 assertion 1.5 130 12 0 assertion 1.9 180 17 0 false(unreach-call) 19    76 280   -16 true .37  26 4.0  2 true 2.4   190 23    2 assertion 2.4 270 20 0 unknown 2.9 200 32 0 true .17  11 1.6  2 timeout 900   3200 7000 0 error (7) 86   540 640 0 timeout 900   2700 7500 0 true 16   270 120 2
floats-esbmc-regression/digits_while_true-unreach-call.i true 630     770 5600    2 true 2.9  33 29   2 assertion 2.5 270 23 0 assertion 1.5 130 15 0 assertion 1.9 180 18 0 false(unreach-call) 19    76 230   -16 true .37  26 3.9  2 true 2.3   190 24    2 assertion 2.3 270 21 0 unknown 2.9 200 27 0 true .17  11 1.4  2 timeout 900   3100 7000 0 error (7) 89   520 930 0 timeout 900   2600 6800 0 true 16   270 150 2
floats-esbmc-regression/fabs_true-unreach-call.i true .23  29 2.2  2 true .90 37 8.8 2 true 4.4 310 41 2 true 3.3 270 31 2 true 4.8 290 40 2 true 5.8  300 59   2 true .083 27 .87 2 true .085 27 1.0  2 false(unreach-call) 3.8 280 33 -16 unknown 3.9 240 38 0 error .12  11 1.2  0 true 9.5 310 72 2 true 8.6 270 77 2 true 9.6 310 72 2 true 17   280 140 2
floats-esbmc-regression/fdim_true-unreach-call.i true .21  29 2.5  2 true 1.0  39 11   2 true 4.2 280 37 2 true 3.0 270 32 2 true 3.0 250 26 2 true 4.2  260 45   2 true .12  27 .82 2 true .12  27 .91 2 false(unreach-call) 3.8 280 36 -16 unknown 3.9 260 39 0 error .12  11 1.3  0 unknown 3.6 220 27 0 unknown 3.7 230 29 0 unknown 3.9 230 33 0 true 17   280 140 2
floats-esbmc-regression/floor_nondet_true-unreach-call.i true 3.7   90 46    2 true 7.1  59 74   2 error 3.5 300 27 0 false(unreach-call) 3.7 290 32 -16 unknown 5.8 420 52 0 unknown 14    440 160   0 true .32  38 4.0  2 true .29  38 3.3  2 error 3.1 280 27 0 unknown 4.2 280 39 0 unknown .096 11 .98 0 unknown 7.5 230 63 0 unknown 7.4 230 61 0 unknown 7.2 220 62 0 true 190   320 2300 2
floats-esbmc-regression/floor_true-unreach-call.i true .45  32 4.2  2 true 1.9  39 22   2 true 4.0 280 35 2 false(unreach-call) 3.4 290 29 -16 true 3.1 250 29 2 true 4.3  270 44   2 true .19  27 1.9  2 true .15  27 1.7  2 false(unreach-call) 4.1 290 35 -16 unknown 4.0 260 34 0 error .12  11 1.2  0 unknown 3.7 220 32 0 unknown 3.5 220 32 0 unknown 3.6 230 31 0 true 18   280 140 2
floats-esbmc-regression/fmax_true-unreach-call.i true .35  30 2.6  2 true 1.4  38 15   2 true 4.1 280 37 2 true 3.0 270 26 2 true 3.1 260 29 2 true 4.2  260 44   2 true .079 27 .87 2 true .080 27 .90 2 false(unreach-call) 3.8 280 35 -16 unknown 3.9 250 34 0 error .14  11 1.3  0 true 8.5 290 66 2 true 8.4 260 69 2 true 8.5 290 68 2 true 18   280 130 2
floats-esbmc-regression/fmin_true-unreach-call.i true .37  33 2.8  2 true 1.4  38 12   2 true 4.3 310 36 2 true 3.0 270 26 2 true 2.9 250 25 2 true 4.1  270 39   2 true .080 27 1.1  2 true .083 27 1.1  2 false(unreach-call) 3.9 280 36 -16 unknown 3.8 250 38 0 error .14  11 1.3  0 true 8.6 290 72 2 true 8.4 260 69 2 true 8.6 290 70 2 true 17   290 140 2
floats-esbmc-regression/fmod2_true-unreach-call.i true .92  96 9.9  2 true 2.3  39 21   2 false(unreach-call) 5.1 300 45 -16 false(unreach-call) 3.5 290 35 -16 true 11   500 120 2 false(unreach-call) 5.0  280 46   -16 true .18  29 1.7  2 true .17  29 1.8  2 false(unreach-call) 4.0 290 35 -16 unknown 3.9 270 36 0 error .12  11 1.3  0 unknown 7.5 230 62 0 unknown 7.2 230 59 0 unknown 7.3 230 61 0 true 22   530 190 2
floats-esbmc-regression/fmod3_true-unreach-call.i true .93  95 12    2 true 2.2  39 26   2 false(unreach-call) 4.9 300 45 -16 false(unreach-call) 3.5 290 34 -16 true 11   500 110 2 false(unreach-call) 5.1  280 52   -16 true .16  29 1.7  2 true .18  32 1.9  2 false(unreach-call) 3.9 290 37 -16 unknown 3.9 260 36 0 error .13  11 1.2  0 unknown 7.3 230 64 0 unknown 7.4 230 70 0 unknown 7.2 230 64 0 true 22   520 190 2
floats-esbmc-regression/fmod_true-unreach-call.i true .88  82 9.3  2 true 2.2  39 23   2 true 4.4 280 34 2 true 3.1 270 32 2 true 2.9 250 25 2 true 4.3  260 40   2 true .088 27 .92 2 true .12  27 .88 2 false(unreach-call) 4.0 280 33 -16 true 3.8 240 34 2 true .16  11 1.6  2 unknown 3.7 220 28 0 unknown 3.8 230 29 0 unknown 3.6 230 30 0 true 18   280 170 2
floats-esbmc-regression/isgreater_true-unreach-call.i true .21  28 1.8  2 true .91 37 8.6 2 true 3.9 280 35 2 true 3.0 270 30 2 true 3.2 250 28 2 true 4.2  270 37   2 true .10  27 .86 2 true .11  27 1.0  2 false(unreach-call) 3.8 280 36 -16 true 4.2 240 37 2 true .16  11 1.6  2 true 8.6 290 67 2 true 8.2 260 73 2 true 8.4 290 76 2 true 15   280 130 2
floats-esbmc-regression/isgreaterequal_true-unreach-call.i true .19  30 1.7  2 true .85 37 10   2 true 4.1 280 35 2 true 3.2 280 25 2 true 2.9 250 25 2 true 4.3  270 49   2 true .080 27 .88 2 true .12  27 .85 2 false(unreach-call) 3.8 280 30 -16 true 4.0 240 38 2 true .17  11 1.5  2 true 8.5 290 65 2 true 8.4 260 66 2 true 8.5 290 71 2 true 15   280 130 2
floats-esbmc-regression/isless_true-unreach-call.i true .23  30 1.8  2 true .90 37 8.1 2 true 4.0 280 35 2 true 3.2 270 28 2 true 3.0 260 23 2 true 4.2  260 41   2 true .091 27 1.1  2 true .079 27 1.0  2 false(unreach-call) 3.8 280 35 -16 true 4.1 240 34 2 true .14  11 1.5  2 true 8.5 290 63 2 true 8.1 260 64 2 true 8.7 300 82 2 true 15   280 120 2
floats-esbmc-regression/islessequal_true-unreach-call.i true .23  28 1.3  2 true .92 37 7.6 2 true 4.2 280 33 2 true 3.1 270 26 2 true 3.0 260 28 2 true 4.1  260 39   2 true .082 27 .94 2 true .11  27 .68 2 false(unreach-call) 3.8 280 34 -16 true 3.8 250 39 2 true .16  11 1.7  2 true 8.7 290 66 2 true 8.3 270 69 2 true 8.9 290 74 2 true 15   290 140 2
floats-esbmc-regression/islessgreater_true-unreach-call.i true .19  28 1.9  2 true .89 37 8.9 2 true 4.2 280 35 2 true 3.1 270 28 2 true 2.9 250 25 2 true 4.3  280 45   2 true .11  27 .87 2 true .083 27 .91 2 false(unreach-call) 3.8 280 32 -16 true 4.1 240 40 2 true .14  11 1.4  2 true 8.8 290 79 2 true 8.4 260 77 2 true 8.9 290 69 2 true 15   290 130 2
floats-esbmc-regression/isunordered_true-unreach-call.i true .28  28 2.5  2 true .88 37 9.6 2 true 4.0 280 37 2 true 3.0 270 26 2 true 3.1 260 27 2 true 4.2  270 44   2 true .079 27 1.0  2 true .084 27 1.1  2 false(unreach-call) 3.8 280 33 -16 true 4.0 240 35 2 true .17  11 1.7  2 true 8.6 290 71 2 true 8.4 260 78 2 true 8.9 300 76 2 true 16   310 140 2
floats-esbmc-regression/lrint_true-unreach-call.i true .47  31 5.2  2 true 1.9  41 25   2 error 3.5 280 33 0 false(unreach-call) 3.2 280 28 -16 unknown 6.3 440 46 0 unknown 8.8  430 84   0 true .18  27 2.0  2 true .19  27 2.2  2 error 3.1 280 29 0 unknown 4.5 300 38 0 unknown .080 11 .89 0 unknown 3.7 230 30 0 unknown 3.6 220 30 0 unknown 3.7 220 30 0 true 19   370 150 2
floats-esbmc-regression/modf_true-unreach-call.i true .41  30 3.0  2 true 1.8  43 22   2 false(unreach-call) 4.6 300 43 -16 false(unreach-call) 3.3 290 28 -16 true 2.9 250 26 2 true 4.4  270 44   2 true .16  27 1.7  2 true .18  27 1.6  2 false(unreach-call) 3.9 280 31 -16 unknown 3.9 250 36 0 error .12  11 1.2  0 unknown 3.6 230 28 0 unknown 3.6 230 30 0 unknown 3.7 220 32 0 true 18   280 160 2
floats-esbmc-regression/nan_true-unreach-call.i true .27  31 3.0  2 true .90 38 8.5 2 true 4.2 300 34 2 true 2.9 270 30 2 true 3.0 250 29 2 true 4.2  270 44   2 true .11  27 .69 2 true .11  27 .75 2 false(unreach-call) 4.0 290 37 -16 unknown 4.2 260 40 0 error .13  11 1.2  0 true 11   340 77 2 true 9.5 320 75 2 true 9.2 310 69 2 true 18   290 130 2
floats-esbmc-regression/nearbyint2_true-unreach-call.i true .51  33 4.2  2 true 2.0  39 14   2 error 3.2 260 28 0 false(unreach-call) 3.3 280 28 -16 unknown 6.8 440 57 0 unknown 9.2  450 91   0 true .21  27 1.8  2 true .18  27 1.9  2 error 3.1 270 25 0 unknown 3.7 240 33 0 unknown .079 11 .91 0 unknown 3.7 220 30 0 unknown 5.8 320 51 0 unknown 3.7 220 30 0 true 19   380 170 2
floats-esbmc-regression/nearbyint_true-unreach-call.i true .52  33 4.3  2 true 3.9  39 38   2 error 3.4 260 29 0 false(unreach-call) 3.7 290 30 -16 unknown 8.6 460 68 0 unknown 11    470 100   0 true .19  27 2.3  2 true .23  32 2.2  2 error 3.3 270 29 0 unknown 3.8 240 33 0 unknown .097 11 .85 0 unknown 3.8 230 33 0 unknown 3.8 230 32 0 unknown 5.8 320 47 0 true 260   230 2900 2
floats-esbmc-regression/remainder_true-unreach-call.i true 1.1   110 12    2 true 2.2  39 24   2 true 4.8 310 38 2 true 3.8 280 33 2 true 3.0 260 23 2 true 4.5  270 48   2 true .21  27 1.9  2 true .19  27 2.3  2 false(unreach-call) 4.3 290 34 -16 unknown 4.5 300 38 0 error .13  11 1.3  0 unknown 3.7 220 33 0 unknown 3.8 220 31 0 unknown 3.6 220 31 0 error 2.3 140 20 0
floats-esbmc-regression/rint2_true-unreach-call.i true .51  33 4.7  2 true 2.0  39 20   2 error 3.2 260 30 0 false(unreach-call) 3.2 290 28 -16 unknown 6.9 440 59 0 unknown 9.4  450 83   0 true .18  28 2.1  2 true .17  28 2.1  2 error 3.4 270 29 0 unknown 4.0 240 33 0 unknown .11  11 .80 0 unknown 3.6 230 31 0 unknown 3.8 220 34 0 unknown 3.5 220 28 0 true 19   390 160 2
floats-esbmc-regression/rint_true-unreach-call.i true .51  32 4.6  2 true 3.8  39 49   2 error 3.3 260 30 0 false(unreach-call) 3.6 300 30 -16 unknown 7.6 440 63 0 unknown 12    470 98   0 true .18  28 2.0  2 true .20  34 2.6  2 error 3.3 280 26 0 unknown 3.9 240 33 0 unknown .097 11 .94 0 unknown 3.9 230 29 0 unknown 5.9 340 38 0 unknown 3.9 230 32 0 true 260   240 3000 2
floats-esbmc-regression/round_nondet_true-unreach-call.i true 3.8   120 44    2 true 7.5  68 94   2 error 3.5 300 30 0 false(unreach-call) 3.8 290 37 -16 unknown 6.7 430 56 0 unknown 17    450 180   0 true .72  81 8.1  2 true .70  81 8.5  2 error 3.4 280 27 0 unknown 3.9 290 36 0 unknown .080 11 .99 0 unknown 7.5 230 60 0 unknown 7.6 230 62 0 unknown 7.5 220 59 0 true 190   350 2300 2
floats-esbmc-regression/round_true-unreach-call.i true .54  39 5.2  2 true 2.1  39 20   2 true 5.0 290 38 2 false(unreach-call) 3.8 290 39 -16 true 3.1 260 27 2 true 4.8  260 47   2 true .21  27 2.5  2 true .21  27 2.5  2 false(unreach-call) 4.6 290 39 -16 unknown 4.2 300 41 0 error .14  11 1.4  0 unknown 3.8 230 29 0 unknown 3.7 220 31 0 unknown 3.9 220 32 0 true 19   290 140 2
floats-esbmc-regression/rounding_functions_true-unreach-call.i true .52  34 4.9  2 true 2.1  39 19   2 true 6.3 430 56 2 true 4.4 290 41 2 true 3.3 260 25 2 true 5.1  260 52   2 true .27  28 2.6  2 true .24  27 2.8  2 false(unreach-call) 4.4 290 43 -16 true 4.0 240 37 2 error .14  11 1.5  0 unknown 3.8 220 31 0 unknown 3.7 230 31 0 unknown 3.7 220 34 0 true 19   290 150 2
floats-esbmc-regression/trunc_nondet_2_true-unreach-call.i true 2.1   38 25    2 true 4.9  40 51   2 false(unreach-call) 5.1 310 46 -16 false(unreach-call) 3.7 290 31 -16 true 10   310 110 2 unknown 890    97 12000   0 true 1.2   44 18    2 true 1.2   44 14    2 false(unreach-call) 4.0 290 31 -16 unknown 4.0 260 39 0 error .11  11 1.3  0 unknown 7.8 230 64 0 unknown 9.2 320 62 0 unknown 7.6 230 64 0 true 180   310 2200 2
floats-esbmc-regression/trunc_nondet_true-unreach-call.i true 2.2   91 26    2 true 4.9  55 49   2 error 3.5 290 28 0 false(unreach-call) 3.4 280 33 -16 unknown 6.0 400 44 0 unknown 12    450 100   0 true .31  38 3.9  2 true .30  38 3.6  2 error 3.3 280 25 0 unknown 4.2 270 41 0 unknown .082 11 .99 0 unknown 10   330 89 0 unknown 7.5 230 66 0 unknown 7.4 230 65 0 true 180   340 2600 2
floats-esbmc-regression/trunc_true-unreach-call.i true .45  34 3.6  2 true 1.8  39 24   2 true 4.2 280 36 2 false(unreach-call) 3.6 290 34 -16 true 2.9 260 26 2 true 4.4  270 38   2 true .16  27 1.6  2 true .18  27 1.8  2 false(unreach-call) 3.9 290 39 -16 unknown 3.9 250 40 0 error .13  11 1.2  0 unknown 3.9 220 30 0 unknown 3.7 230 27 0 unknown 3.8 230 34 0 true 18   300 150 2
floats-esbmc-regression/Double_div_bad_false-unreach-call.i timeout 900     400 8000    0 false(unreach-call) 11    41 120   1 timeout 900   4100 9700 0 timeout 900   4100 10000 0 false(unreach-call) 88   2000 1100 1 unknown 890    630 8100   0 false(unreach-call) 480     250 5900    1 false(unreach-call) 480     260 4700    1 timeout 900   3900 13000 0 unknown 5.4 300 45 0 false(unreach-call) .17  11 1.6  1 error (7) 310   2900 2900 0 error (7) 65   1000 680 0 error (7) 370   4100 4600 0 false(unreach-call) 250   3600 2700 1
floats-esbmc-regression/Float_div_bad_false-unreach-call.i timeout 900     350 10000    0 false(unreach-call) 3.5  33 37   1 timeout 900   910 12000 0 timeout 900   1000 10000 0 false(unreach-call) 10   460 80 1 unknown 890    690 8800   0 false(unreach-call) 1.4   30 16    1 false(unreach-call) 1.6   35 23    1 timeout 900   1500 14000 0 unknown 5.3 300 44 0 false(unreach-call) .16  11 1.6  1 timeout 900   2000 7900 0 error (7) 85   510 910 0 timeout 900   1900 7800 0 false(unreach-call) 230   1000 2900 1
floats-esbmc-regression/digits_bad_for_false-unreach-call.i false(unreach-call) 710     770 8400    0 false(unreach-call) 2.7  33 27   0 assertion 2.4 260 23 0 assertion 1.5 130 14 0 assertion 1.9 210 16 0 false(unreach-call) 19    76 280   0 false(unreach-call) .34  28 3.9  0 false(unreach-call) 2.3   190 25    0 assertion 2.4 260 22 0 unknown 3.0 200 33 0 false(unreach-call) .17  11 1.5  0 timeout 900   3000 6400 0 error (7) 83   510 620 0 timeout 900   2700 7600 0 false(unreach-call) 15   220 120 0
floats-esbmc-regression/digits_bad_while_false-unreach-call.i false(unreach-call) 750     780 6200    0 false(unreach-call) 2.7  33 27   0 assertion 2.5 270 23 0 assertion 1.4 120 12 0 assertion 1.8 180 18 0 false(unreach-call) 19    76 240   0 false(unreach-call) .35  28 4.2  0 false(unreach-call) 2.3   190 26    0 assertion 2.3 270 22 0 unknown 2.9 200 28 0 false(unreach-call) .14  11 1.6  0 timeout 900   2900 7900 0 error (7) 85   500 810 0 timeout 900   2600 6800 0 false(unreach-call) 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 200000 -1424 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 39 560   16000 5700 64 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 5300 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 14 42   3800 390 14 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 9 29   2500 250 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 9 29   2500 250 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 400   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.6 540 47 -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 -1424 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