Tool 2LS 0.7.2-sv-comp19 CBMC CBMC Path 5.10 () CPAchecker 1.7-svn 29852 DepthK 3.1 DIVINE ESBMC version 6.0.0 64-bit x86_64 linux PeSCo 1.7-svn b8d6131600+ Pinaka 0.1 skink 2.0 SMACK 1.9.3 symbiotic 6.0.3-77d4af47 ULTIMATE Automizer 0.1.23-635dfa2a ULTIMATE Kojak 0.1.23-635dfa2a ULTIMATE Taipan 0.1.23-635dfa2a VeriAbs 1.3.10 VeriFuzz 1.0.0
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.15.0-42-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution 2018-12-04 22:44:17 CET 2018-12-04 22:48:40 CET 2018-12-04 22:45:10 CET 2018-12-05 05:46:16 CET 2018-12-05 09:36:33 CET 2018-12-10 10:00:20 CET 2018-12-06 11:06:04 CET 2018-12-06 11:03:31 CET 2018-12-06 12:44:04 CET 2018-12-06 20:14:43 CET 2018-12-07 12:00:55 CET 2018-12-07 19:13:55 CET 2018-12-07 21:42:05 CET 2018-12-08 07:42:40 CET 2018-12-08 11:04:44 CET 2018-12-08 14:19:36 CET 2018-12-10 16:50:17 CET 2018-12-09 02:47:33 CET
Run set 2ls.sv-comp19_prop-reachsafety.ReachSafety-Floats cbmc.sv-comp19_prop-reachsafety.ReachSafety-Floats cbmc-path.sv-comp19_prop-reachsafety.ReachSafety-Floats cpa-seq.sv-comp19_prop-reachsafety.ReachSafety-Floats depthk.sv-comp19_prop-reachsafety.ReachSafety-Floats divine-explicit.sv-comp19_prop-reachsafety.ReachSafety-Floats divine-smt.sv-comp19_prop-reachsafety.ReachSafety-Floats esbmc-kind.sv-comp19_prop-reachsafety.ReachSafety-Floats pesco.sv-comp19_prop-reachsafety.ReachSafety-Floats pinaka.sv-comp19_prop-reachsafety.ReachSafety-Floats skink.sv-comp19_prop-reachsafety.ReachSafety-Floats smack.sv-comp19_prop-reachsafety.ReachSafety-Floats symbiotic.sv-comp19_prop-reachsafety.ReachSafety-Floats uautomizer.sv-comp19_prop-reachsafety.ReachSafety-Floats ukojak.sv-comp19_prop-reachsafety.ReachSafety-Floats utaipan.sv-comp19_prop-reachsafety.ReachSafety-Floats veriabs.sv-comp19_prop-reachsafety.ReachSafety-Floats verifuzz.sv-comp19_prop-reachsafety.ReachSafety-Floats
Options --graphml-witness witness.graphml --graphml-witness witness.graphml --graphml-witness witness.graphml -svcomp19 -heap 10000M -benchmark -timelimit 900s --no-symbolic -s kinduction -svcomp19-pesco -heap 10000M -stack 2048k -benchmark -timelimit 900s --graphml-witness witness.graphml -w error-witness.graphml --witness witness.graphml --full-output --full-output --full-output
../sv-benchmarks/c/ status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score status cpu (s) mem (MB) energy (J) score
floats-cdfpl/newton_1_4_false-unreach-call_true-termination.i false(unreach-call) 6.8   61 84    1 false(unreach-call) 14     60   150    1 false(unreach-call) 9.2   54   96    1 false(unreach-call) 74   450 650 1 false(unreach-call) 26    99 360   1 unknown 8.3 430 110 0 unknown 8.3 430 110 0 false(unreach-call) 25     93 350    1 false(unreach-call) 46 1200 360 1 false(unreach-call) 3.9  72 46   1 unknown 34   2900 310 0 timeout 880    1100 7300   0 error(unknown, verification-finished) .19  17 1.8  0 false(unreach-call) 32   700 260 1 error (7) 84   1100 800 0 false(unreach-call) 32   700 270 1 false(unreach-call) 87   370 660 1 false(unreach-call) 15   150 170 1
floats-cdfpl/newton_1_5_false-unreach-call_true-termination.i false(unreach-call) 6.3   60 68    1 false(unreach-call) 6.6   47   72    1 false(unreach-call) 7.3   51   89    1 false(unreach-call) 57   440 410 1 false(unreach-call) 33    99 420   1 unknown 8.3 430 130 0 unknown 8.3 430 110 0 false(unreach-call) 33     93 440    1 false(unreach-call) 62 1200 450 1 false(unreach-call) 4.2  73 51   1 unknown 34   2900 280 0 timeout 880    1200 6000   0 error(unknown, verification-finished) .17  17 1.9  0 false(unreach-call) 94   730 640 1 error (7) 77   1100 690 0 false(unreach-call) 91   720 760 1 false(unreach-call) 67   370 520 1 false(unreach-call) 6.0 150 66 1
floats-cdfpl/newton_1_6_false-unreach-call_true-termination.i false(unreach-call) 2.6   51 32    1 false(unreach-call) 4.3   42   44    1 false(unreach-call) 5.5   44   72    1 false(unreach-call) 44   450 360 1 false(unreach-call) 42    100 580   1 unknown 8.1 430 99 0 unknown 8.3 430 95 0 false(unreach-call) 41     92 520    1 false(unreach-call) 27 1200 180 1 false(unreach-call) 1.8  72 25   1 unknown 34   2900 280 0 timeout 880    970 6900   0 error(unknown, verification-finished) .17  17 1.8  0 false(unreach-call) 64   710 480 1 error (7) 81   1100 640 0 false(unreach-call) 64   710 490 1 false(unreach-call) 56   380 460 1 false(unreach-call) 8.8 150 84 1
floats-cdfpl/newton_1_7_false-unreach-call_true-termination.i false(unreach-call) 2.4   50 25    1 false(unreach-call) 8.4   49   87    1 false(unreach-call) 2.4   41   31    1 false(unreach-call) 22   440 210 1 false(unreach-call) 9.0  100 130   1 unknown 8.2 430 110 0 unknown 8.2 430 91 0 false(unreach-call) 8.8   92 120    1 false(unreach-call) 26 1300 230 1 false(unreach-call) 3.1  73 43   1 unknown 37   2900 350 0 timeout 880    960 6500   0 error(unknown, verification-finished) .17  18 2.2  0 false(unreach-call) 250   760 1500 1 error (7) 80   1100 700 0 false(unreach-call) 250   760 1800 1 false(unreach-call) 29   370 270 1 false(unreach-call) 11   150 140 1
floats-cdfpl/newton_1_8_false-unreach-call_true-termination.i false(unreach-call) 3.9   53 41    1 false(unreach-call) 7.4   49   95    1 false(unreach-call) .92  38   11    1 false(unreach-call) 16   440 130 1 false(unreach-call) 39    99 520   1 unknown 8.3 430 95 0 unknown 8.5 430 110 0 false(unreach-call) 39     91 460    1 false(unreach-call) 22 1200 170 1 false(unreach-call) 1.9  72 28   1 unknown 33   2900 290 0 timeout 880    1400 5300   0 error(unknown, verification-finished) .20  18 2.1  0 false(unreach-call) 25   710 220 1 error (7) 83   1100 720 0 false(unreach-call) 24   700 220 1 false(unreach-call) 25   370 210 1 false(unreach-call) 6.9 150 83 1
floats-cdfpl/newton_2_6_false-unreach-call_true-termination.i false(unreach-call) 3.5   90 32    1 false(unreach-call) 77     160   660    1 false(unreach-call) 57     140   600    1 false(unreach-call) 140   610 1100 1 false(unreach-call) 130    200 1700   1 unknown 8.3 430 110 0 unknown 8.3 430 110 0 false(unreach-call) 130     190 1700    1 false(unreach-call) 35 1300 250 0 false(unreach-call) 22    96 260   1 unknown 35   2900 330 0 timeout 880    2100 6400   0 error(unknown, verification-finished) .18  17 2.1  0 false(unreach-call) 130   860 980 0 error (7) 73   1500 710 0 false(unreach-call) 120   860 850 0 false(unreach-call) 160   460 1400 0 false(unreach-call) 60   150 890 1
floats-cdfpl/newton_2_7_false-unreach-call_true-termination.i false(unreach-call) 6.7   94 63    1 false(unreach-call) 120     230   1200    1 false(unreach-call) 53     140   490    1 false(unreach-call) 84   600 590 1 false(unreach-call) 120    200 1400   1 unknown 8.2 430 100 0 unknown 8.4 430 100 0 false(unreach-call) 120     190 1400    1 false(unreach-call) 33 1300 240 0 false(unreach-call) 23    97 270   1 unknown 34   2900 330 0 timeout 880    1500 6800   0 error(unknown, verification-finished) .18  17 1.9  0 false(unreach-call) 330   910 2300 1 error (7) 65   1400 530 0 false(unreach-call) 330   920 2700 1 false(unreach-call) 98   460 750 0 false(unreach-call) 24   150 310 1
floats-cdfpl/newton_2_8_false-unreach-call_true-termination.i false(unreach-call) 17     120 170    1 false(unreach-call) 25     100   310    1 false(unreach-call) 21     99   270    1 false(unreach-call) 43   610 310 1 false(unreach-call) 61    200 740   1 unknown 8.1 430 130 0 unknown 8.5 430 100 0 false(unreach-call) 61     190 730    1 false(unreach-call) 42 1300 350 1 false(unreach-call) 20    95 290   1 unknown 33   2900 280 0 timeout 880    2100 6000   0 error(unknown, verification-finished) .19  18 2.1  0 false(unreach-call) 34   850 290 1 error (7) 54   1400 520 0 false(unreach-call) 34   840 290 1 false(unreach-call) 69   460 560 1 false(unreach-call) 19   200 200 1
floats-cdfpl/newton_3_6_false-unreach-call_true-termination.i false(unreach-call) 40     210 400    1 false(unreach-call) 430     480   4500    1 false(unreach-call) 340     460   3200    1 false(unreach-call) 300   780 1900 1 false(unreach-call) 100    300 980   1 unknown 8.2 430 100 0 unknown 8.2 430 120 0 false(unreach-call) 100     290 1400    1 false(unreach-call) 410 1900 2900 1 false(unreach-call) 73    150 770   1 unknown 35   2900 310 0 timeout 880    3200 6800   0 error(unknown, verification-finished) .21  17 1.6  0 timeout 900   1100 6800 0 error (7) 69   2000 640 0 timeout 900   1100 8200 0 false(unreach-call) 360   570 3400 1 false(unreach-call) 74   220 750 1
floats-cdfpl/newton_3_7_false-unreach-call_true-termination.i false(unreach-call) 64     220 680    1 false(unreach-call) 75     200   830    1 false(unreach-call) 38     150   360    1 false(unreach-call) 200   780 1300 1 false(unreach-call) 120    280 1400   1 unknown 8.4 430 120 0 unknown 8.4 430 100 0 false(unreach-call) 120     280 1500    1 false(unreach-call) 300 2000 2000 1 false(unreach-call) 42    120 460   1 unknown 35   2900 320 0 timeout 880    2100 6800   0 error(unknown, verification-finished) .20  17 1.7  0 false(unreach-call) 47   930 390 1 error (7) 71   1900 540 0 false(unreach-call) 49   940 470 1 false(unreach-call) 270   570 1900 1 false(unreach-call) 67   230 570 1
floats-cdfpl/newton_3_8_false-unreach-call_true-termination.i false(unreach-call) 35     190 440    1 false(unreach-call) 55     180   540    1 false(unreach-call) 84     220   820    1 false(unreach-call) 170   780 980 1 false(unreach-call) 130    310 1500   1 unknown 8.2 430 100 0 unknown 8.4 430 130 0 false(unreach-call) 130     300 1600    1 false(unreach-call) 29 1500 210 0 false(unreach-call) 32    130 360   1 unknown 35   2900 320 0 timeout 880    2800 5800   0 error(unknown, verification-finished) .17  17 1.6  0 false(unreach-call) 610   1100 5200 0 error (7) 63   2000 520 0 false(unreach-call) 610   1100 4500 0 false(unreach-call) 230   570 1800 0 false(unreach-call) 37   200 320 1
floats-cdfpl/sine_1_false-unreach-call_true-termination.i false(unreach-call) .74  24 8.4  1 false(unreach-call) .90  22   10    1 false(unreach-call) .91  21   11    1 false(unreach-call) 9.0 380 110 1 false(unreach-call) 20    71 320   1 unknown 8.2 430 120 0 unknown 8.3 430 110 0 false(unreach-call) 20     64 280    1 false(unreach-call) 110 1400 1000 1 false(unreach-call) 1.9  65 30   1 false(unreach-call) 31   2800 250 1 false(unreach-call) 750    700 6300   0 error(unknown, verification-finished) .18  18 2.1  0 false(unreach-call) 200   700 1700 0 error (7) 34   590 260 0 false(unreach-call) 200   700 1600 0 false(unreach-call) 17   340 170 0 false(unreach-call) 7.4 150 77 1
floats-cdfpl/sine_2_false-unreach-call_true-termination.i false(unreach-call) .58  24 7.1  1 false(unreach-call) 4.1   31   58    1 false(unreach-call) 1.4   23   18    1 false(unreach-call) 45   410 390 1 false(unreach-call) 20    71 240   1 unknown 8.2 430 110 0 unknown 8.3 430 110 0 false(unreach-call) 20     64 300    1 false(unreach-call) 21 1100 180 1 false(unreach-call) .47 61 4.3 1 false(unreach-call) 32   2800 260 1 timeout 880    610 6600   0 error(unknown, verification-finished) .19  17 2.2  0 false(unreach-call) 380   810 3600 1 error (7) 35   610 300 0 false(unreach-call) 380   810 3000 1 false(unreach-call) 50   360 520 1 false(unreach-call) 4.5 150 47 1
floats-cdfpl/sine_3_false-unreach-call_true-termination.i false(unreach-call) 1.6   31 19    1 false(unreach-call) .98  21   13    1 false(unreach-call) 1.3   23   17    1 false(unreach-call) 270   540 2700 1 false(unreach-call) 19    71 310   1 unknown 8.3 430 110 0 unknown 8.3 430 110 0 false(unreach-call) 19     64 240    1 false(unreach-call) 45 1200 450 1 false(unreach-call) 1.8  65 20   1 false(unreach-call) 28   2800 230 0 false(unreach-call) 680    530 5100   0 error(unknown, verification-finished) .17  18 2.3  0 false(unreach-call) 360   760 2900 1 error (7) 34   590 260 0 false(unreach-call) 360   740 3600 1 false(unreach-call) 210   440 1800 1 false(unreach-call) 6.3 150 67 1
floats-cdfpl/square_1_false-unreach-call_true-termination.i false(unreach-call) .90  26 11    1 false(unreach-call) 1.7   24   21    1 false(unreach-call) 1.6   23   21    1 false(unreach-call) 18   400 150 1 false(unreach-call) 4.8  64 73   1 unknown 8.1 430 110 0 unknown 8.2 430 110 0 false(unreach-call) 4.7   57 55    1 false(unreach-call) 29 1200 230 1 false(unreach-call) .80 61 8.8 1 unknown 33   1300 290 0 false(unreach-call) 390    200 2700   0 error(unknown, verification-finished) .17  17 2.2  0 false(unreach-call) 80   460 670 1 error (7) 29   370 210 0 false(unreach-call) 81   460 660 1 false(unreach-call) 25   350 210 1 false(unreach-call) 7.4 150 94 1
floats-cdfpl/square_2_false-unreach-call_true-termination.i false(unreach-call) .99  26 12    1 false(unreach-call) 1.8   24   21    0 false(unreach-call) 2.1   26   25    1 false(unreach-call) 180   590 1800 1 false(unreach-call) 6.9  62 85   1 unknown 8.3 430 98 0 unknown 8.4 430 100 0 false(unreach-call) 6.8   55 78    1 false(unreach-call) 200 1400 1500 1 false(unreach-call) 1.2  64 13   0 unknown 32   1300 320 0 false(unreach-call) 830    280 6700   0 error(unknown, verification-finished) .21  17 1.7  0 false(unreach-call) 88   460 700 1 error (7) 29   370 230 0 false(unreach-call) 86   460 780 1 false(unreach-call) 200   500 1400 1 false(unreach-call) 76   150 1000 1
floats-cdfpl/square_3_false-unreach-call_true-termination.i false(unreach-call) .71  24 8.2  1 false(unreach-call) 1.5   23   19    0 false(unreach-call) 1.5   26   18    1 false(unreach-call) 62   430 560 1 false(unreach-call) 7.6  63 110   1 unknown 8.1 430 93 0 unknown 8.3 430 120 0 false(unreach-call) 7.5   55 95    1 false(unreach-call) 71 1300 620 1 false(unreach-call) 1.3  65 19   0 unknown 33   1200 310 0 timeout 880    280 9500   0 error(unknown, verification-finished) .20  17 1.7  0 false(unreach-call) 180   570 1400 1 error (7) 29   370 240 0 false(unreach-call) 180   550 1400 1 false(unreach-call) 69   360 560 0 false(unreach-call) 9.2 150 120 1
floats-cdfpl/newton_1_1_true-unreach-call_true-termination.i true 8.6   63 90    2 true 230     150   2200    2 true 320     95   2200    2 timeout 900   620 5800 0 unknown 110    100 1400   0 unknown 8.2 430 93 0 unknown 8.6 430 110 0 true 36     93 480    2 timeout 900 1600 5800 0 true 4.9  78 62   2 unknown 34   2900 320 0 timeout 880    1600 6700   0 error(unknown, verification-finished) .17  17 2.0  0 timeout 900   1000 7600 0 error (7) 78   1100 570 0 timeout 900   1000 5500 0 true 93   770 680 2 error (1) 860   150 11000 0
floats-cdfpl/newton_1_2_true-unreach-call_true-termination.i true 7.8   63 110    2 true 140     110   1100    2 true 100     85   1100    2 timeout 900   600 6700 0 unknown 120    100 1700   0 unknown 8.2 430 98 0 unknown 8.3 430 100 0 true 39     94 570    2 timeout 900 1600 6100 0 true 5.7  78 85   2 unknown 33   2900 290 0 timeout 880    990 6600   0 error(unknown, verification-finished) .20  17 2.0  0 timeout 900   810 6200 0 error (7) 77   1100 600 0 timeout 900   820 6400 0 true 96   770 840 2 error (1) 860   150 12000 0
floats-cdfpl/newton_1_3_true-unreach-call_true-termination.i true 10     64 110    2 true 170     110   1600    2 true 410     140   4900    2 timeout 900   610 6100 0 unknown 130    100 1800   0 unknown 8.3 430 110 0 unknown 8.3 430 110 0 true 44     93 650    2 timeout 900 1600 6400 0 true 6.2  79 81   2 unknown 34   2900 310 0 timeout 880    1200 6400   0 error(unknown, verification-finished) .17  17 1.9  0 timeout 900   990 7200 0 error (7) 80   1100 620 0 timeout 900   980 5400 0 true 94   760 680 2 error (1) 860   150 10000 0
floats-cdfpl/newton_2_1_true-unreach-call_true-termination.i true 21     130 240    2 true 260     210   3100    2 true 300     240   2800    2 timeout 900   540 7300 0 unknown 480    200 6000   0 unknown 8.2 430 100 0 unknown 8.4 430 110 0 true 160     190 1900    2 timeout 900 1700 6600 0 true 15    120 200   2 unknown 44   2900 500 0 timeout 880    1500 7900   0 error(unknown, verification-finished) .18  17 1.7  0 timeout 900   920 5900 0 error (7) 73   1500 690 0 timeout 900   920 6300 0 true 130   880 1200 2 error (1) 860   150 10000 0
floats-cdfpl/newton_2_2_true-unreach-call_true-termination.i true 32     130 280    2 true 550     310   4600    2 true 320     240   3000    2 timeout 900   860 8000 0 unknown 510    200 5900   0 unknown 8.2 430 110 0 unknown 8.2 430 88 0 true 170     190 2000    2 timeout 900 2000 6500 0 true 16    110 200   2 unknown 35   2900 330 0 timeout 880    2500 5700   0 error(unknown, verification-finished) .17  18 2.0  0 timeout 900   1000 6100 0 error (7) 64   1500 500 0 timeout 900   1000 6600 0 true 140   890 1300 2 error (1) 860   150 10000 0
floats-cdfpl/newton_2_3_true-unreach-call_true-termination.i true 27     130 280    2 true 350     340   2900    2 true 430     440   4200    2 timeout 900   550 6300 0 unknown 480    200 5800   0 unknown 8.4 430 100 0 unknown 8.3 430 98 0 true 160     190 1800    2 timeout 900 1700 6100 0 true 17    100 180   2 unknown 41   2900 400 0 timeout 880    2600 5200   0 error(unknown, verification-finished) .17  18 1.9  0 timeout 900   1100 6800 0 error (7) 74   1600 610 0 timeout 900   1000 6500 0 true 130   880 1400 2 error (1) 860   150 12000 0
floats-cdfpl/newton_2_4_true-unreach-call_true-termination.i true 33     130 330    2 true 550     360   4800    2 true 510     280   4400    2 timeout 900   620 8600 0 unknown 470    200 6500   0 unknown 8.3 430 99 0 unknown 8.3 430 96 0 true 160     190 2100    2 timeout 900 1700 6400 0 true 15    100 180   2 unknown 35   2900 330 0 timeout 880    1500 5200   0 error(unknown, verification-finished) .20  18 1.9  0 timeout 900   1200 7800 0 error (7) 80   1500 630 0 timeout 900   1200 6400 0 true 140   890 1700 2 error (1) 860   150 11000 0
floats-cdfpl/newton_2_5_true-unreach-call_true-termination.i true 51     130 470    2 true 830     590   8000    2 true 700     660   6700    2 timeout 900   610 8500 0 unknown 540    200 6900   0 unknown 8.2 430 95 0 unknown 8.2 430 100 0 true 180     190 2100    2 timeout 900 1700 6800 0 true 21    110 250   2 unknown 34   2900 350 0 timeout 880    1800 7000   0 error(unknown, verification-finished) .19  18 1.7  0 timeout 900   920 8000 0 error (7) 64   1500 630 0 timeout 900   910 8600 0 true 170   890 1400 2 error (1) 860   150 11000 0
floats-cdfpl/newton_3_1_true-unreach-call_true-termination.i true 81     220 940    2 error (42) 870     550   9600    0 error (42) 880     520   9000    0 timeout 900   610 6000 0 unknown 890    300 12000   0 unknown 8.2 430 110 0 unknown 8.3 430 100 0 true 450     290 5100    2 timeout 900 1700 6700 0 true 43    150 440   2 unknown 35   2900 410 0 timeout 880    3300 5400   0 error(unknown, verification-finished) .17  18 1.8  0 timeout 900   1100 5900 0 error (7) 62   2000 570 0 timeout 900   1100 5400 0 true 190   980 1600 2 error (1) 860   230 12000 0
floats-cdfpl/newton_3_2_true-unreach-call_true-termination.i true 73     210 580    2 error (42) 880     480   6000    0 true 670     430   7200    2 timeout 900   570 6900 0 unknown 900    310 9600   0 unknown 8.3 430 110 0 unknown 8.3 430 100 0 true 700     300 11000    2 timeout 900 1700 6700 0 true 35    150 490   2 unknown 35   2900 310 0 timeout 880    2300 7100   0 error(unknown, verification-finished) .20  17 1.6  0 timeout 900   1100 6000 0 error (7) 70   2000 600 0 timeout 900   1100 6500 0 true 220   970 2000 2 error (1) 860   230 12000 0
floats-cdfpl/newton_3_3_true-unreach-call_true-termination.i true 74     190 740    2 error (42) 880     550   7900    0 true 720     450   6300    2 timeout 900   700 6500 0 unknown 900    300 13000   0 unknown 8.1 430 98 0 unknown 8.3 430 100 0 true 460     300 6500    2 timeout 900 1900 7200 0 true 50    130 510   2 unknown 35   2900 330 0 timeout 880    3500 6000   0 error(unknown, verification-finished) .18  18 1.8  0 timeout 900   1100 6100 0 error (7) 63   2000 560 0 timeout 900   1100 6700 0 true 220   980 2300 2 error (1) 860   270 10000 0
floats-cdfpl/newton_3_4_true-unreach-call_true-termination.i true 110     210 980    2 error (42) 880     540   8500    0 error (42) 880     600   7400    0 timeout 900   710 7200 0 unknown 900    310 10000   0 unknown 8.1 430 120 0 unknown 8.4 430 97 0 true 630     300 7000    2 timeout 900 1900 6100 0 true 46    140 580   2 unknown 35   2900 390 0 timeout 880    2800 11000   0 error(unknown, verification-finished) .20  18 2.1  0 timeout 900   1100 5700 0 error (7) 73   2000 630 0 timeout 900   1100 6000 0 true 210   990 1900 2 error (1) 860   240 9900 0
floats-cdfpl/newton_3_5_true-unreach-call_true-termination.i true 74     220 720    2 error (42) 880     850   8200    0 error (42) 880     480   8500    0 timeout 900   570 7400 0 unknown 900    310 9800   0 unknown 8.1 430 110 0 unknown 8.4 430 110 0 true 620     310 6000    2 timeout 900 1700 8000 0 true 54    130 680   2 unknown 35   2900 310 0 timeout 880    2400 5600   0 error(unknown, verification-finished) .17  19 2.0  0 timeout 900   1100 5900 0 error (7) 65   1900 540 0 timeout 900   1100 5200 0 true 250   980 2100 2 error (1) 870   230 10000 0
floats-cdfpl/sine_4_true-unreach-call_true-termination.i true 25     41 290    2 true 710     85   8100    2 error (42) 880     110   10000    0 timeout 900   500 5300 0 unknown 100    73 1500   0 unknown 8.3 430 100 0 unknown 8.4 430 120 0 true 34     64 450    2 timeout 900 1500 6600 0 true 39    74 520   2 unknown 32   2800 330 0 timeout 880    620 5300   0 error(unknown, verification-finished) .19  17 1.8  0 timeout 900   810 8000 0 error (7) 34   600 280 0 timeout 900   810 6100 0 true 110   670 1400 2 error (1) 860   150 12000 0
floats-cdfpl/sine_5_true-unreach-call_true-termination.i true 1.7   33 21    2 true 220     77   3100    2 true 250     86   3100    2 timeout 900   500 6700 0 unknown 53    72 570   0 unknown 8.2 430 110 0 unknown 8.6 430 99 0 true 17     64 220    2 timeout 900 1500 7600 0 true 2.6  70 36   2 unknown 33   2800 310 0 timeout 880    600 6500   0 error(unknown, verification-finished) .17  18 1.8  0 timeout 900   860 5900 0 error (7) 35   590 270 0 timeout 900   860 7300 0 true 79   680 700 2 error (1) 860   150 10000 0
floats-cdfpl/sine_6_true-unreach-call_true-termination.i true 1.9   31 23    2 true 19     44   280    2 true 220     100   2500    2 timeout 900   650 7600 0 unknown 62    72 760   0 unknown 8.3 430 98 0 unknown 8.5 430 120 0 true 20     64 300    2 timeout 900 1700 4900 0 true 2.5  70 35   2 unknown 32   2800 300 0 timeout 880    600 6500   0 error(unknown, verification-finished) .20  17 2.1  0 timeout 900   850 7700 0 error (7) 34   590 310 0 timeout 900   850 6300 0 true 79   680 910 2 error (1) 860   150 10000 0
floats-cdfpl/sine_7_true-unreach-call_true-termination.i true 1.2   27 17    2 true 5.9   29   81    2 true 220     87   3000    2 true 590   590 4800 2 unknown 44    72 570   0 unknown 8.3 430 92 0 unknown 8.2 430 94 0 true 14     64 150    2 true 690 1600 5500 2 true 2.0  71 25   2 unknown 32   2800 310 0 timeout 880    630 6000   0 error(unknown, verification-finished) .17  18 2.1  0 timeout 900   900 9200 0 error (7) 35   600 320 0 timeout 900   880 6500 0 true 79   670 750 2 error (1) 860   150 12000 0
floats-cdfpl/sine_8_true-unreach-call_true-termination.i true 1.7   31 24    2 true 62     60   680    2 true 40     60   570    2 true 460   550 4100 2 unknown 53    72 790   0 unknown 8.2 430 100 0 unknown 8.3 430 110 0 true 17     63 220    2 true 560 1600 4800 2 true 2.6  70 38   2 unknown 31   2800 270 0 timeout 880    720 6500   0 error(unknown, verification-finished) .18  17 2.0  0 timeout 900   840 6300 0 error (7) 34   600 280 0 timeout 900   840 7600 0 true 79   670 660 2 error (1) 860   150 11000 0
floats-cdfpl/square_4_true-unreach-call_true-termination.i true 55     50 800    2 true 270     110   3600    2 true 250     140   3900    2 true 540   570 3900 2 unknown 87    66 1100   0 unknown 8.1 430 98 0 unknown 8.3 430 90 0 true 29     57 330    2 true 540 1400 5000 2 true 190    86 2400   2 unknown 32   1300 390 0 timeout 880    370 7800   0 error(unknown, verification-finished) .17  17 1.8  0 true 840   760 5400 2 error (7) 28   360 210 0 true 810   780 6000 2 true 170   500 1900 2 error (1) 860   150 10000 0
floats-cdfpl/square_5_true-unreach-call_true-termination.i true 25     50 360    2 true 260     110   3100    2 true 250     110   2400    2 true 430   510 2900 2 unknown 41    67 580   0 unknown 8.3 430 100 0 unknown 8.4 430 120 0 true 13     59 180    2 true 450 1300 3100 2 true 130    89 1700   2 unknown 32   1600 300 0 timeout 880    370 9700   0 error(unknown, verification-finished) .17  17 1.8  0 true 880   860 6300 2 error (7) 27   360 270 0 true 880   830 6600 2 true 310   520 3800 2 error (1) 860   150 11000 0
floats-cdfpl/square_6_true-unreach-call_true-termination.i true 79     68 1100    2 true 93     62   1200    2 true 130     90   1500    2 true 220   500 1600 2 unknown 36    67 570   0 unknown 8.3 430 110 0 unknown 8.2 430 110 0 true 12     55 180    2 true 240 1300 1600 2 true 25    75 330   2 unknown 32   1300 270 0 timeout 880    560 7700   0 error(unknown, verification-finished) .17  17 1.8  0 timeout 900   790 6300 0 error (7) 28   370 210 0 timeout 900   790 6500 0 true 120   510 1400 2 error (1) 860   150 12000 0
floats-cdfpl/square_7_true-unreach-call_true-termination.i true 85     68 1000    2 true 66     56   860    2 true 30     42   390    2 true 760   490 6700 2 unknown 22    65 310   0 unknown 8.1 430 110 0 unknown 8.4 430 100 0 true 7.1   61 110    2 true 750 1300 5700 2 true 5.9  74 72   2 unknown 32   1300 270 0 timeout 880    370 9200   0 error(unknown, verification-finished) .16  18 2.3  0 true 530   850 4600 2 error (7) 28   360 260 0 true 510   800 4600 2 true 87   510 730 2 error (1) 860   150 12000 0
floats-cdfpl/square_8_true-unreach-call_true-termination.i true .79  25 10    2 true 1.8   21   26    2 true 2.0   21   24    2 true 56   370 500 2 unknown 17    65 270   0 unknown 8.3 430 97 0 unknown 8.2 430 110 0 true 5.5   62 71    2 true 65 1300 570 2 true 1.3  68 16   2 unknown 32   1300 350 0 timeout 880    370 7200   0 error(unknown, verification-finished) .17  17 2.0  0 true 74   640 580 2 error (7) 28   370 230 0 true 73   630 520 2 true 79   500 610 2 error (1) 860   150 10000 0
floats-cbmc-regression/float-div1_true-unreach-call.i true .30  38 3.3  2 true .34  15   5.2  2 true .35  17   4.8  2 true 4.9 350 41 2 unknown 10    77 140   0 unknown 8.2 430 95 0 unknown 8.2 430 120 0 true 3.2   68 42    2 true 17 1200 120 2 true .96 81 10   2 unknown 10   300 88 0 true 37    250 440   2 error(unknown, slicing-finished) .17  15 1.7  0 true 42   890 400 2 error (7) 18   480 160 0 true 43   940 360 2 true 50   770 460 2 timeout 900   180 11000 0
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i true .92  120 12    2 true .29  24   3.1  2 true .31  26   4.5  2 true 10   800 110 2 unknown 1.0  67 11   0 unknown 8.3 430 88 0 unknown 8.4 430 110 0 true .14  28 1.5  2 true 31 2100 270 2 true .95 85 11   2 true 19   580 170 2 true 290    590 1900   2 error(unknown, slicing-finished) .20  15 1.6  0 error (7) 13   340 100 0 error (7) 13   340 100 0 error (7) 13   330 95 0 true 45   810 400 2 timeout 900   180 13000 0
floats-cbmc-regression/float-no-simp1_true-unreach-call_true-termination.i true .097 23 .73 2 true .043 7.3 .33 2 true .065 6.0 .20 2 true 2.8 250 27 2 unknown .79 65 9.1 0 true 8.2 370 110 2 true 8.0 370 130 2 true .075 26 .90 2 true 13 1100 88 2 true .36 58 3.2 2 true 3.6 210 36 2 true 2.5  74 31   2 true .15  16 2.2  2 true 13   350 100 2 true 13   340 98 2 true 12   340 100 2 true 16   410 140 2 timeout 900   150 10000 0
floats-cbmc-regression/float-no-simp2_true-unreach-call.i true .69  29 10    2 true 1.7   10   19    2 true 1.6   11   22    2 true 13   330 120 2 unknown 6.0  66 68   0 error - divine failed with exitcode 1 1.6 200 22 0 error - divine failed with exitcode 1 1.7 200 21 0 true 1.8   36 27    2 true 25 1200 230 2 true 1.5  68 20   2 true 12   370 110 2 true 91    190 1100   2 error(unknown, slicing-finished) .17  17 1.7  0 true 48   480 510 2 error (7) 15   400 160 0 true 47   480 530 2 true 69   530 790 2 error (1) 870   180 12000 0
floats-cbmc-regression/float-no-simp3_true-unreach-call_true-termination.i true .10  23 1.1  2 true .050 7.7 .39 2 true .042 6.0 .31 2 true 2.9 250 30 2 unknown .77 67 8.6 0 true 8.0 370 110 2 true 8.1 370 120 2 true .080 26 1.1  2 true 12 1000 77 2 true .34 58 3.2 2 true 3.7 200 37 2 true 2.5  74 33   2 true .14  15 1.6  2 true 13   360 110 2 true 12   340 97 2 true 12   360 110 2 true 17   430 140 2 timeout 900   150 11000 0
floats-cbmc-regression/float-no-simp4_true-unreach-call.i true .31  37 3.4  2 true .17  9.3 2.6  2 true .19  12   2.7  2 true 4.4 300 42 2 unknown .93 67 9.5 0 error - divine failed with exitcode 1 1.6 200 22 0 error - divine failed with exitcode 1 1.7 200 24 0 true .14  27 1.4  2 true 15 1200 95 2 true .86 69 7.5 2 true 16   480 160 2 true 7.6  290 77   2 error(unknown, slicing-finished) .17  16 2.1  0 true 15   390 140 2 error (7) 14   370 110 0 true 15   370 130 2 true 63   670 640 2 timeout 900   180 11000 0
floats-cbmc-regression/float-no-simp6_true-unreach-call_true-termination.i true .090 24 .91 2 true .043 6.6 .40 2 true .080 5.6 .22 2 true 3.0 250 30 2 unknown .80 66 8.2 0 true 8.0 370 110 2 true 8.1 370 92 2 true .10  26 .79 2 true 11 1100 90 2 true .35 58 3.3 2 true 3.8 210 37 2 true 2.6  73 28   2 true .14  17 1.6  2 true 14   360 120 2 true 16   380 140 2 true 14   360 110 2 true 18   430 160 2 timeout 900   150 12000 0
floats-cbmc-regression/float-no-simp7_true-unreach-call_true-termination.i true .10  23 .87 2 true .11  5.6 .24 2 true .040 6.4 .22 2 true 2.9 250 26 2 unknown .79 66 8.2 0 true 8.1 370 91 2 true 8.0 370 86 2 true .085 26 .74 2 true 13 1000 84 2 true .35 58 3.5 2 true 3.7 210 33 2 true 2.6  72 34   2 true .15  15 1.5  2 true 12   330 100 2 true 13   360 110 2 true 13   370 110 2 true 16   420 140 2 timeout 900   150 12000 0
floats-cbmc-regression/float-no-simp8_true-unreach-call.i true .22  28 1.6  2 true .079 8.0 .80 2 true .12  8.5 .72 2 true 4.1 290 37 2 unknown .82 65 8.7 0 unknown 8.2 430 100 0 unknown 8.3 430 140 0 true .087 26 .88 2 true 14 1100 100 2 true .74 68 6.3 2 true 4.0 210 33 2 true 2.6  73 32   2 true .15  16 1.3  2 error (7) 13   350 110 0 error (7) 13   340 100 0 error (7) 14   330 110 0 true 25   410 200 2 timeout 900   170 13000 0
floats-cbmc-regression/float-rounding1_true-unreach-call.i true .21  28 1.7  2 true .087 7.2 .78 2 true .094 9.2 .78 2 error 4.0 270 33 0 unknown .98 66 13   0 unknown 8.2 430 120 0 unknown 8.3 430 100 0 true .14  27 1.6  2 unknown 18 1300 140 0 true .73 68 7.1 2 unknown 8.2 250 77 0 true 2.7  79 32   2 unknown .093 13 .68 0 unknown 7.3 330 61 0 unknown 7.3 340 54 0 unknown 7.2 330 59 0 true 21   420 170 2 timeout 900   180 12000 0
floats-cbmc-regression/float-to-double1_true-unreach-call.i true .22  28 2.1  2 true .14  6.8 1.2  2 true .13  9.6 1.5  2 true 4.0 290 39 2 unknown 1.4  66 16   0 unknown 8.2 430 100 0 unknown 8.2 430 100 0 true .28  27 3.1  2 true 15 1200 120 2 true .74 68 7.1 2 true 11   320 95 2 true 2.9  130 42   2 error(unknown, slicing-finished) .14  16 1.5  0 true 23   390 270 2 error (7) 14   370 120 0 true 25   400 280 2 true 56   450 650 2 timeout 900   180 11000 0
floats-cbmc-regression/float-to-double2_true-unreach-call_true-termination.i true .086 24 .90 2 true .049 6.2 .25 2 true .11  5.5 .21 2 true 2.7 250 25 2 unknown .81 67 8.2 0 true 7.9 370 94 2 true 8.1 370 96 2 true .094 26 .71 2 true 13 1000 89 2 true .34 58 3.3 2 true 3.7 200 29 2 true 2.5  73 31   2 true .13  15 1.6  2 true 13   360 100 2 true 12   330 100 2 true 13   360 110 2 true 16   420 160 2 timeout 900   150 10000 0
floats-cbmc-regression/float-zero-sum1_true-unreach-call_true-termination.i true .12  24 .85 2 true .052 6.5 .31 2 true .040 5.8 .29 2 true 3.0 250 27 2 unknown .82 66 8.4 0 true 8.4 370 100 2 true 8.0 370 93 2 true .085 26 .86 2 true 13 1200 100 2 true .36 58 3.2 2 true 4.0 220 36 2 true 2.5  74 36   2 true .14  15 1.7  2 true 13   350 97 2 true 14   350 110 2 true 12   340 110 2 true 18   410 170 2 timeout 900   150 12000 0
floats-cbmc-regression/float11_true-unreach-call_true-termination.i true .096 24 .88 2 true .047 6.6 .37 2 true .041 6.5 .29 2 true 2.9 260 28 2 unknown .82 66 9.1 0 true 8.2 370 97 2 true 8.1 370 120 2 true .095 26 .97 2 true 13 1000 90 2 true .36 58 3.7 2 true 3.6 210 36 2 true 2.5  72 31   2 true .13  15 1.5  2 true 13   340 110 2 true 15   360 110 2 true 13   370 120 2 true 17   410 150 2 timeout 900   200 11000 0
floats-cbmc-regression/float12_true-unreach-call_true-termination.i true .096 24 .96 2 true .085 6.4 .76 2 true .060 6.5 .42 2 true 2.8 260 27 2 unknown 1.2  66 13   0 unknown 8.2 430 99 0 error - divine failed with signal 11 1.7 200 21 0 true .20  26 2.6  2 true 13 1000 91 2 true .36 58 2.7 2 true 17   360 150 2 true 4.2  100 53   2 error(unknown, verification-finished) .18  17 1.6  0 true 17   360 170 2 true 18   350 160 2 true 18   350 180 2 true 26   440 320 2 timeout 900   150 11000 0
floats-cbmc-regression/float13_true-unreach-call_true-termination.i true .14  24 1.3  2 true .054 6.4 .32 2 true .051 6.6 .30 2 true 3.0 250 26 2 unknown .78 66 8.1 0 true 8.1 370 120 2 true 8.2 370 99 2 true .081 26 .80 2 true 13 1000 88 2 true .37 58 3.9 2 true 3.7 200 35 2 true 2.5  74 29   2 true .15  16 1.4  2 true 14   370 100 2 true 16   370 120 2 true 14   370 120 2 true 17   420 150 2 timeout 900   150 13000 0
floats-cbmc-regression/float14_true-unreach-call.i true .18  28 2.2  2 true .11  7.7 .84 2 true .075 9.7 .76 2 true 4.2 280 43 2 unknown .82 67 8.9 0 unknown 8.3 430 110 0 unknown 8.4 430 110 0 true .092 26 .96 2 true 14 1100 90 2 true .70 67 8.3 2 true 9.2 300 88 2 true 2.6  87 35   2 error(unknown, slicing-finished) .15  15 1.5  0 true 14   370 110 2 error (7) 14   360 110 0 true 14   370 110 2 true 26   430 200 2 timeout 900   190 12000 0
floats-cbmc-regression/float18_true-unreach-call.i timeout 900     2400 10000    0 true .19  7.8 2.3  2 true .18  9.5 2.2  2 error 4.0 280 33 0 unknown 900    2300 12000   0 unknown 8.2 430 100 0 unknown 8.4 430 110 0 true 270     1200 3100    2 true 12 1300 94 2 true .74 67 6.0 2 true 3.9 210 32 2 true 2.5  72 33   2 true .17  16 1.7  2 error (7) 12   340 98 0 error (7) 13   330 100 0 error (7) 12   320 110 0 true 45   810 370 2 timeout 900   180 13000 0
floats-cbmc-regression/float19_true-unreach-call.i true .21  28 1.8  2 true .097 7.1 .72 2 true .091 9.6 .89 2 true 4.2 290 40 2 unknown 1.0  66 11   0 unknown 8.3 430 99 0 unknown 8.4 430 120 0 true .16  26 1.8  2 true 15 1200 120 2 true .72 67 7.2 2 true 11   340 120 2 true 3.0  100 36   2 error(unknown, slicing-finished) .18  16 1.6  0 true 15   390 110 2 error (7) 14   360 120 0 true 15   370 120 2 true 28   430 220 2 timeout 900   180 12000 0
floats-cbmc-regression/float1_true-unreach-call_true-termination.i true .091 24 .70 2 true .078 6.1 .22 2 true .041 5.9 .27 2 true 2.9 250 28 2 unknown .81 66 9.2 0 true 8.1 370 110 2 true 8.0 370 89 2 true .081 26 .78 2 true 12 1000 89 2 true .36 58 3.0 2 true 3.8 200 40 2 true 2.6  80 32   2 true .13  15 1.8  2 true 13   360 110 2 true 13   360 94 2 true 13   360 110 2 true 17   480 160 2 timeout 900   150 11000 0
floats-cbmc-regression/float20_true-unreach-call_true-termination.i true .14  24 1.3  2 true .095 7.9 .85 2 true .097 8.1 .77 2 true 3.0 260 30 2 unknown .94 66 11   0 unknown 8.4 430 110 0 unknown 8.2 430 97 0 true .13  30 1.4  2 true 13 1000 85 2 true .36 59 4.2 2 false(unreach-call) 7.4 330 65 -16 true 8.0  140 93   2 error(unknown, verification-finished) .19  18 2.1  0 true 19   390 180 2 true 49   520 540 2 true 18   390 160 2 true 25   490 240 2 timeout 900   150 9300 0
floats-cbmc-regression/float21_true-unreach-call.i true .25  31 2.8  2 true .21  8.4 2.6  2 true .19  11   1.7  2 true 7.8 330 83 2 unknown 1.5  67 17   0 unknown 8.2 430 110 0 unknown 8.4 430 100 0 true .32  27 3.5  2 true 21 1200 160 2 true .84 69 9.4 2 true 15   390 150 2 true 120    450 940   2 error(unknown, slicing-finished) .16  16 1.7  0 true 59   500 620 2 error (7) 21   410 190 0 true 56   500 650 2 true 66   590 690 2 timeout 900   180 13000 0
floats-cbmc-regression/float22_true-unreach-call_true-termination.i true .12  24 .70 2 true .060 6.4 .55 2 true .059 6.1 .64 2 true 3.2 270 29 2 unknown .97 67 11   0 true 8.1 370 92 2 true 8.2 370 99 2 true .19  26 1.9  2 true 15 1200 130 2 true .39 59 2.9 2 true 4.1 220 41 2 true 5.1  110 71   2 true .15  16 1.8  2 true 170   780 2100 2 timeout 900   790 13000 0 true 200   750 2400 2 true 56   650 590 2 timeout 900   150 12000 0
floats-cbmc-regression/float2_true-unreach-call_true-termination.i true .091 24 1.3  2 true .072 5.9 .27 2 true .037 6.2 .35 2 true 2.9 260 30 2 unknown .89 67 10   0 true 8.1 370 110 2 true 8.1 370 96 2 true .10  26 1.1  2 true 12 1000 81 2 true .36 58 3.8 2 true 3.6 210 33 2 true 2.5  72 32   2 true .13  15 1.5  2 true 14   360 110 2 true 14   350 120 2 true 13   360 120 2 true 18   430 160 2 timeout 900   150 11000 0
floats-cbmc-regression/float3_true-unreach-call_true-termination.i true .15  24 .93 2 true .078 7.2 .76 2 true .073 7.2 .56 2 true 3.0 280 29 2 unknown .80 67 8.7 0 true 8.1 370 97 2 true 8.3 370 100 2 true .10  26 .81 2 true 13 1000 98 2 true .35 58 3.9 2 true 6.1 300 56 2 true 4.2  120 56   2 error(unknown, verification-finished) .15  17 1.8  0 true 16   350 160 2 true 17   340 140 2 true 17   360 160 2 true 25   440 230 2 timeout 900   150 11000 0
floats-cbmc-regression/float4_true-unreach-call.i true 9.5   46 120    2 true 9.7   25   130    2 true 10     26   120    2 true 51   360 670 2 unknown 3.1  67 38   0 unknown 8.1 430 100 0 unknown 8.4 430 110 0 true .83  31 10    2 true 63 1200 690 2 true 4.2  100 58   2 true 18   370 170 2 true 88    190 1100   2 error(unknown, slicing-finished) .15  16 1.9  0 true 86   510 1200 2 error (7) 16   410 150 0 true 87   510 1000 2 true 100   520 1400 2 error (1) 860   180 11000 0
floats-cbmc-regression/float5_true-unreach-call_true-termination.i true .11  24 .78 2 true .075 6.3 .60 2 true .075 7.4 .64 2 true 3.1 260 29 2 unknown 1.4  65 16   0 unknown 8.3 430 120 0 unknown 8.2 430 98 0 true .28  27 3.5  2 true 13 1000 88 2 true .36 58 3.1 2 true 6.1 300 57 2 true 5.5  97 67   2 error(unknown, verification-finished) .16  17 2.1  0 true 23   330 260 2 true 37   360 520 2 true 23   360 240 2 true 42   440 460 2 timeout 900   150 9800 0
floats-cbmc-regression/float6_true-unreach-call_true-termination.i true .11  24 .99 2 true .069 5.9 .49 2 true .099 6.1 .50 2 true 3.1 260 33 2 unknown .83 66 8.5 0 unknown 8.2 430 100 0 unknown 8.4 430 93 0 true .096 26 1.0  2 true 14 1100 90 2 true .37 59 3.4 2 true 16   390 140 2 true 2.7  78 33   2 error(unknown, verification-finished) .17  17 2.0  0 true 15   370 120 2 true 20   470 180 2 true 15   380 120 2 true 18   420 170 2 timeout 900   150 13000 0
floats-cbmc-regression/float8_true-unreach-call.i true .53  28 6.3  2 true .63  7.7 8.6  2 true .65  9.9 8.7  2 true 7.0 300 79 2 unknown .84 68 9.0 0 error - divine failed with exitcode 1 1.6 200 22 0 error - divine failed with exitcode 1 1.7 200 20 0 true .11  26 1.0  2 true 18 1200 160 2 true 1.1  67 12   2 true 12   320 110 2 true 2.6  73 34   2 error(unknown, verification-finished) .16  16 1.7  0 true 15   370 120 2 error (7) 14   360 100 0 true 15   390 120 2 true 26   430 210 2 timeout 900   180 12000 0
floats-cbmc-regression/float_lib1_true-unreach-call.i true 6.6   35 66    2 true .14  8.6 1.8  2 true .14  11   1.4  2 true 4.2 260 40 2 unknown 2.7  67 30   0 unknown 8.2 430 110 0 unknown 8.3 430 94 0 true .54  27 7.0  2 true 15 1300 120 2 true .81 69 9.0 2 true 13   380 120 2 true 2.8  80 32   2 error(unknown, slicing-finished) .14  16 1.7  0 error (7) 12   310 90 0 error (7) 13   340 100 0 error (7) 12   310 98 0 true 26   430 200 2 timeout 900   180 12000 0
floats-cbmc-regression/float_lib2_true-unreach-call.i true .23  29 2.1  2 true .13  8.3 1.1  2 true .14  11   1.4  2 true 4.2 290 43 2 unknown .84 67 9.1 0 unknown 8.3 430 100 0 unknown 8.2 430 110 0 true .097 27 1.1  2 true 14 1100 100 2 true .85 68 7.1 2 true 11   320 100 2 true 9.3  290 110   2 error(unknown, slicing-finished) .13  16 1.5  0 true 15   370 140 2 error (7) 14   370 100 0 true 15   380 120 2 true 31   610 270 2 timeout 900   180 11000 0
float-benchs/cast_float_ptr_false-unreach-call_true-termination.c error (134) .096 24 1.2  0 false(unreach-call) .068 9.2 .61 1 false(unreach-call) .082 8.9 .46 1 false(unreach-call) 3.1 270 29 1 false(unreach-call) .18 33 1.6 1 unknown 8.4 430 120 0 unknown 8.2 430 100 0 false(unreach-call) .094 26 1.0  1 false(unreach-call) 12 1200 89 1 false(unreach-call) .37 59 4.5 1 false(unreach-call) 11   320 100 1 false(unreach-call) 3.9  88 57   0 error(unknown, verification-finished) .17  17 2.1  0 false(unreach-call) 16   370 130 1 false(unreach-call) 13   330 110 1 false(unreach-call) 14   330 120 1 false(unreach-call) 9.4 270 84 1 false(unreach-call) 3.7 150 35 1
float-benchs/cast_union_loose_false-unreach-call_true-termination.c false(unreach-call) .12  24 1.5  1 false(unreach-call) .083 9.5 .57 1 false(unreach-call) .085 8.8 .54 1 false(unreach-call) 3.3 280 35 1 false(unreach-call) .21 33 2.4 1 unknown 8.2 430 110 0 error - unexpected error: memory error in userspace 8.5 430 110 0 false(unreach-call) .17  26 1.6  1 false(unreach-call) 14 1100 110 1 error (8) .38 59 3.0 0 false(unreach-call) 12   360 120 1 false(unreach-call) 4.7  94 59   0 error(unknown, verification-finished) .19  19 1.8  0 false(unreach-call) 13   350 99 1 false(unreach-call) 14   370 130 1 false(unreach-call) 14   370 110 1 false(unreach-call) 9.9 290 92 1 false(unreach-call) 3.8 150 38 1
float-benchs/cast_union_tight_false-unreach-call_true-termination.c false(unreach-call) .13  24 1.5  1 false(unreach-call) .085 9.6 .68 1 false(unreach-call) .076 9.1 .84 1 false(unreach-call) 3.2 290 29 1 false(unreach-call) .21 34 2.8 1 unknown 8.1 430 100 0 error - divine failed with signal 11 1.7 200 24 0 false(unreach-call) .15  27 1.7  1 false(unreach-call) 12 1200 94 1 error (8) .36 59 3.4 0 false(unreach-call) 14   390 110 1 false(unreach-call) 4.3  100 57   0 error(unknown, verification-finished) .16  17 1.8  0 false(unreach-call) 14   370 110 1 false(unreach-call) 15   360 130 1 false(unreach-call) 13   330 100 1 false(unreach-call) 9.6 280 87 1 false(unreach-call) 3.6 150 33 1
float-benchs/float_int_inv_square_false-unreach-call_true-termination.c false(unreach-call) .14  24 1.4  1 false(unreach-call) .091 9.0 .89 1 false(unreach-call) .13  9.2 .68 1 false(unreach-call) 3.1 280 32 1 false(unreach-call) .45 36 4.9 1 unknown 8.1 430 99 0 error - divine failed with signal 11 1.7 200 22 0 false(unreach-call) .36  28 5.4  1 false(unreach-call) 12 1200 82 1 false(unreach-call) .37 59 3.3 1 false(unreach-call) 22   470 190 1 false(unreach-call) 4.0  89 48   1 false(unreach-call) .22  20 2.8  1 false(unreach-call) 14   370 120 1 false(unreach-call) 15   350 130 1 false(unreach-call) 13   360 110 1 false(unreach-call) 7.5 280 68 1 false(unreach-call) 3.5 150 39 1
float-benchs/inv_Newton_false-unreach-call.c timeout 900     1300 9400    0 error (42) 880     780   5900    0 error (42) 880     540   6400    0 false(unreach-call) 5.4 350 60 1 unknown 890    300 13000   0 unknown 8.3 430 110 0 unknown 8.5 430 110 0 timeout 900     300 7600    0 false(unreach-call) 14 1300 110 1 timeout 900    270 6400   0 unknown 84   1000 670 0 timeout 880    810 8800   0 error(unknown, verification-finished) .17  18 2.3  0 timeout 900   2000 6400 0 error (7) 68   420 610 0 timeout 900   2000 7100 0 unknown 560   430 4100 0 false(unreach-call) 27   150 350 1
float-benchs/inv_Newton_false-unreach-call.c.p+cfa-reducer.c error (6) .083 24 .82 0 error (42) 880     12000   4900    0 error (42) 880     500   8000    0 false(unreach-call) 4.7 350 45 1 unknown 88    15000 960   0 unknown 8.1 430 100 0 unknown 8.2 430 100 0 true 450     530 4300    -32 false(unreach-call) 14 1300 110 1 timeout 900    480 8200   0 unknown 200   3100 2100 0 timeout 880    650 8900   0 error(unknown, verification-finished) .16  17 1.8  0 timeout 900   1800 6600 0 error (7) 48   430 400 0 timeout 900   1800 6100 0 out of memory 140   15000 1500 0 false(unreach-call) 11   150 140 1
float-benchs/inv_square_false-unreach-call_true-termination.c false(unreach-call) .14  24 1.3  1 false(unreach-call) .073 9.7 .70 1 false(unreach-call) .096 8.8 .48 1 false(unreach-call) 3.1 280 33 1 false(unreach-call) .37 36 5.2 1 unknown 8.3 430 100 0 unknown 8.3 430 110 0 false(unreach-call) .30  28 3.9  1 false(unreach-call) 14 1100 100 1 false(unreach-call) .37 59 3.7 1 false(unreach-call) 22   510 180 1 false(unreach-call) 3.5  81 45   0 error(unknown, verification-finished) .17  18 2.3  0 false(unreach-call) 13   330 110 1 false(unreach-call) 13   330 110 1 false(unreach-call) 13   370 120 1 false(unreach-call) 7.4 280 69 1 timeout 900   150 11000 0
float-benchs/nan_double_false-unreach-call_true-termination.c false(unreach-call) .11  24 1.0  1 false(unreach-call) .071 9.0 .40 1 false(unreach-call) .066 9.5 .42 1 false(unreach-call) 2.9 260 27 1 false(unreach-call) .14 33 1.6 1 unknown 8.2 430 99 0 unknown 8.3 430 100 0 false(unreach-call) .083 26 .97 1 false(unreach-call) 13 1100 92 1 false(unreach-call) .36 59 3.7 1 false(unreach-call) 9.7 300 90 1 false(unreach-call) 3.2  72 35   0 error(unknown, verification-finished) .15  17 1.8  0 false(unreach-call) 13   360 110 1 false(unreach-call) 13   370 92 1 false(unreach-call) 12   350 100 1 false(unreach-call) 7.2 270 65 1 false(unreach-call) 3.6 150 39 1
float-benchs/nan_float_false-unreach-call_true-termination.c false(unreach-call) .11  24 1.1  1 false(unreach-call) .054 9.3 .69 1 false(unreach-call) .061 9.9 .49 1 false(unreach-call) 2.8 270 26 1 false(unreach-call) .13 33 1.7 1 unknown 8.4 430 110 0 unknown 8.3 430 100 0 false(unreach-call) .076 26 .93 1 false(unreach-call) 13 1100 93 1 false(unreach-call) .36 59 3.0 1 false(unreach-call) 11   330 110 1 false(unreach-call) 3.2  72 39   0 error(unknown, verification-finished) .16  17 2.0  0 false(unreach-call) 13   370 100 1 false(unreach-call) 12   320 100 1 false(unreach-call) 12   350 110 1 false(unreach-call) 7.2 270 66 1 false(unreach-call) 3.7 200 35 1
float-benchs/sin_interpolated_index_false-unreach-call_true-termination.c false(unreach-call) 3.3   260 34    1 false(unreach-call) 2.6   190   29    1 false(unreach-call) .25  18   2.1  1 false(unreach-call) 5.5 420 51 1 false(unreach-call) 9.2  110 110   1 unknown 8.1 430 120 0 unknown 8.4 430 100 0 false(unreach-call) 9.2   100 120    1 false(unreach-call) 15 1200 120 1 false(unreach-call) .55 62 6.7 1 false(unreach-call) 31   670 340 1 timeout 880    3200 7100   0 error(unknown, verification-finished) .18  17 1.8  0 false(unreach-call) 410   2100 4100 1 error (7) 49   1200 490 0 false(unreach-call) 410   2100 4400 1 false(unreach-call) 15   340 130 1 false(unreach-call) 7.0 280 71 1
float-benchs/sqrt_poly2_false-unreach-call.c false(unreach-call) .56  41 6.2  1 false(unreach-call) .53  35   5.9  1 false(unreach-call) .33  32   4.1  1 false(unreach-call) 15   570 160 1 false(unreach-call) 58    150 840   1 unknown 8.1 430 99 0 unknown 8.4 430 96 0 false(unreach-call) 58     150 800    1 false(unreach-call) 30 1400 280 1 false(unreach-call) .66 69 7.0 1 false(unreach-call) 15   470 140 1 timeout 880    480 6000   0 error(unknown, verification-finished) .17  17 2.1  0 false(unreach-call) 19   600 170 0 error (7) 100   720 890 0 false(unreach-call) 19   600 160 0 false(unreach-call) 18   440 170 1 false(unreach-call) 4.1 150 38 1
float-benchs/Muller_Kahan_true-unreach-call.c.p+cfa-reducer.c error (6) .10  24 .92 0 true .34  7.0 3.0  2 true .31  6.3 2.4  2 true 3.7 260 31 2 unknown .99 67 13   0 true 8.1 370 110 2 true 8.1 370 130 2 true .10  26 .81 2 true 15 1200 99 2 true .47 59 4.0 2 unknown 37   1400 400 0 out of memory 35    15000 410   0 true .14  16 1.6  2 timeout 900   2800 9700 0 timeout 900   1800 11000 0 timeout 900   5600 12000 0 true 120   1200 1300 2 timeout 900   150 11000 0
float-benchs/Muller_Kahan_true-unreach-call_true-termination.c timeout 900     820 8100    0 true .31  6.5 3.4  2 true .25  6.2 3.3  2 true 3.8 260 39 2 unknown 900    1200 11000   0 true 8.1 370 100 2 true 8.2 370 110 2 true 21     260 280    2 true 16 1200 110 2 true .44 58 3.9 2 unknown 42   1400 470 0 out of memory 36    15000 390   0 true .14  16 1.8  2 timeout 900   4500 9100 0 timeout 900   1900 10000 0 timeout 900   7700 9700 0 true 110   1400 1100 2 timeout 900   150 13000 0
float-benchs/Rump_double_true-unreach-call_true-termination.c true .15  24 1.5  2 true .049 6.9 .39 2 true .045 6.4 .32 2 true 2.9 250 25 2 unknown .78 65 8.2 0 true 8.0 370 110 2 true 8.1 370 100 2 true .087 26 .90 2 true 13 1000 82 2 true .37 59 3.0 2 true 3.5 220 33 2 true 270    740 2400   2 true .14  15 1.9  2 true 24   1000 210 2 error (7) 27   1600 240 0 true 24   1000 210 2 true 28   1100 240 2 timeout 900   150 11000 0
float-benchs/Rump_float_true-unreach-call_true-termination.c true .12  24 .93 2 true .056 7.1 .31 2 true .11  6.3 .26 2 true 2.9 260 25 2 unknown .80 67 8.9 0 true 8.0 370 110 2 true 8.0 370 94 2 true .10  26 .83 2 true 11 1200 88 2 true .37 59 3.2 2 true 3.8 210 35 2 true 95    280 840   2 true .15  16 1.8  2 true 15   450 120 2 error (7) 24   580 180 0 true 16   450 130 2 true 18   520 160 2 timeout 900   150 10000 0
float-benchs/addsub_double_exact_true-unreach-call_true-termination.c true .15  24 .77 2 true .051 7.0 .46 2 true .042 6.4 .34 2 true 2.8 260 28 2 unknown .80 65 9.5 0 true 7.9 370 93 2 true 8.2 370 100 2 true .085 26 .98 2 true 13 1000 87 2 true .38 59 3.1 2 true 3.9 220 42 2 true 2.6  82 33   2 true .14  15 1.5  2 true 13   370 99 2 true 15   330 140 2 true 13   340 110 2 true 15   420 140 2 timeout 900   150 13000 0
float-benchs/addsub_float_exact_true-unreach-call_true-termination.c true .094 24 .96 2 true .050 7.0 .32 2 true .044 6.3 .30 2 true 2.8 250 24 2 unknown .78 65 8.5 0 true 8.1 370 100 2 true 8.1 370 97 2 true .098 26 1.5  2 true 13 1000 92 2 true .36 59 3.6 2 true 3.5 220 36 2 true 2.6  75 38   2 true .14  15 1.8  2 true 13   360 110 2 true 13   370 120 2 true 13   360 95 2 true 16   430 150 2 timeout 900   150 12000 0
float-benchs/addsub_float_inexact_true-unreach-call_true-termination.c true .11  24 .58 2 true .049 7.4 .41 2 true .041 6.3 .30 2 true 2.9 260 27 2 unknown .79 66 8.8 0 true 8.1 370 110 2 true 8.1 370 100 2 true .075 26 .75 2 true 13 1000 82 2 true .37 59 3.0 2 true 4.0 220 34 2 true 2.6  75 32   2 true .14  15 1.7  2 true 13   360 120 2 true 13   360 98 2 true 13   360 120 2 true 15   420 130 2 timeout 900   150 13000 0
float-benchs/arctan_Pade_true-unreach-call_true-termination.c true 59     260 660    2 true 97     300   1100    2 true 82     380   1100    2 true 22   500 260 2 unknown 780    510 8900   0 unknown 8.2 430 93 0 unknown 8.4 430 100 0 true 250     490 3100    2 true 32 1400 280 2 true 5.2  250 78   2 unknown 59   2300 540 0 timeout 880    4400 7100   0 error(unknown, verification-finished) .18  17 2.4  0 error (7) 120   2600 1100 0 error (7) 77   890 610 0 error (7) 120   2600 1200 0 true 220   1200 2000 2 error (1) 870   260 12000 0
float-benchs/bary_diverge_true-unreach-call_true-termination.c timeout 900     420 7800    0 error (42) 880     1400   9900    0 out of memory 720     15000   8800    0 timeout 910   3100 9000 0 unknown 890    200 11000   0 unknown 8.2 430 94 0 unknown 8.3 430 110 0 timeout 900     330 12000    0 timeout 920 2600 8100 0 out of memory 110    15000 1300   0 unknown 170   2900 2500 0 timeout 880    410 6900   0 timeout (verification) 900     48 11000    0 timeout 900   1100 8600 0 error (7) 22   360 210 0 timeout 900   1000 9500 0 true 120   990 1400 2 timeout 900   150 13000 0
float-benchs/cast_float_union_true-unreach-call.c true .11  24 .84 2 true .13  5.7 .29 2 true .047 6.3 .32 2 true 3.0 250 28 2 unknown .79 67 9.5 0 unknown 8.2 430 100 0 unknown 8.4 430 130 0 true .11  26 .78 2 true 13 1100 83 2 error (8) .39 59 3.3 0 true 3.7 230 34 2 true 2.6  74 32   2 true .15  16 1.6  2 true 7.6 350 58 2 true 7.9 340 63 2 true 7.7 350 58 2 true 13   450 120 2 timeout 900   150 12000 0
float-benchs/cos_polynomial_true-unreach-call_true-termination.c true 7.0   110 61    2 true 48     96   360    2 true 290     160   1900    2 timeout 900   1500 9000 0 unknown 350    240 4900   0 unknown 8.3 430 96 0 unknown 8.4 430 100 0 true 120     240 1400    2 timeout 900 2500 6100 0 true 18    520 200   2 unknown 23   570 220 0 timeout 880    640 5400   0 error(unknown, verification-finished) .18  17 2.3  0 timeout 900   3000 5900 0 error (7) 150   980 1000 0 timeout 900   3000 7100 0 true 88   930 780 2 error (1) 860   150 12000 0
float-benchs/divmul_buf_diverge_true-unreach-call_true-termination.c timeout 900     410 9100    0 error (42) 880     3100   5900    0 out of memory 510     15000   5700    0 timeout 960   4500 6900 0 unknown 900    330 12000   0 unknown 8.1 430 100 0 unknown 8.3 430 130 0 timeout 900     5200 10000    0 timeout 910 4400 8900 0 timeout 900    4700 6900   0 unknown 59   2200 810 0 timeout 880    640 7500   0 timeout (verification) 900     2800 8600    0 timeout 900   2600 12000 0 timeout 900   5400 8400 0 timeout 900   2600 8000 0 timeout 900   12000 7300 0 error (1) 860   150 12000 0
float-benchs/divmul_diverge_true-unreach-call_true-termination.c timeout 900     380 10000    0 error (42) 880     6200   6900    0 out of memory 510     15000   5900    0 timeout 970   4300 8200 0 unknown 900    330 11000   0 unknown 8.1 430 110 0 unknown 8.5 430 100 0 timeout 900     8300 11000    0 timeout 910 3000 8300 0 timeout 900    4800 6100   0 unknown 52   1700 660 0 timeout 880    490 8000   0 timeout (verification) 900     2800 10000    0 timeout 900   2600 13000 0 timeout 900   5100 9000 0 timeout 900   3600 11000 0 timeout 900   13000 8100 0 error (1) 860   150 11000 0
float-benchs/drift_tenth_true-unreach-call.c.p+cfa-reducer.c true .56  24 6.4  2 true .095 7.1 .71 2 true .073 6.6 .54 2 true 2.8 240 28 2 unknown 9.5  67 120   0 true 8.0 370 92 2 true 8.1 370 110 2 true .42  30 5.2  2 true 110 1600 1600 2 true .36 59 3.3 2 true 3.8 210 36 2 true 2.5  74 34   2 true .17  16 1.7  2 timeout 900   910 9000 0 error (7) 31   510 300 0 true 770   920 7600 2 true 53   520 600 2 timeout 900   150 14000 0
float-benchs/drift_tenth_true-unreach-call_true-termination.c true .60  24 7.5  2 true .080 7.2 .56 2 true .12  6.2 .40 2 true 2.7 250 28 2 unknown 9.4  67 130   0 true 8.0 370 110 2 true 8.1 370 110 2 true .43  29 4.9  2 true 22 1200 210 2 true .36 59 3.0 2 true 3.5 210 39 2 true 2.5  72 34   2 true .14  16 1.5  2 timeout 900   900 7400 0 timeout 900   700 8500 0 true 900   960 7000 2 true 59   530 620 2 timeout 900   150 11000 0
float-benchs/exp_loop_true-unreach-call.c true 20     240 240    2 true 1.0   20   15    2 true 7.6   22   110    2 true 840   8700 7900 2 unknown 670    300 8400   0 unknown 8.2 430 91 0 unknown 8.5 430 120 0 true 12     67 170    2 true 850 9700 8000 2 true 1.3  240 15   2 unknown 59   1700 680 0 timeout 880    640 7500   0 error(unknown, verification-finished) .18  17 2.1  0 timeout 900   1300 9000 0 error (7) 27   380 240 0 timeout 900   1400 8800 0 true 380   1000 3600 2 timeout 900   150 10000 0
float-benchs/feedback_diverge_true-unreach-call_true-termination.c timeout 900     2100 9400    0 error (42) 880     1800   9100    0 out of memory 620     15000   7000    0 timeout 970   4800 8100 0 unknown 900    250 11000   0 unknown 8.2 430 120 0 unknown 8.3 430 100 0 timeout 900     8400 8900    0 timeout 960 5300 10000 0 timeout 900    300 12000   0 unknown 65   1700 810 0 timeout 880    640 8100   0 timeout (verification) 900     2800 8400    0 timeout 900   2600 11000 0 timeout 900   5200 9000 0 timeout 900   2100 7500 0 timeout 900   8400 8500 0 error (1) 860   150 11000 0
float-benchs/filter1_true-unreach-call.c.p+cfa-reducer.c error (6) .086 24 .97 0 error (42) 880     2500   9400    0 error (134) .046 6.6 .28 0 true 20   890 170 2 unknown 900    580 10000   0 unknown 8.3 430 110 0 unknown 8.4 430 110 0 timeout 900     1100 10000    0 true 30 1700 210 2 timeout 900    860 9300   0 unknown 98   910 1200 0 timeout 880    500 8100   0 timeout (verification) 900     2800 11000    0 timeout 900   1100 11000 0 error (7) 49   460 540 0 timeout 900   1100 11000 0 unknown 840   830 5800 0 timeout 900   150 10000 0
float-benchs/filter1_true-unreach-call.c.v+lhb-reducer.c error (6) .10  24 .83 0 error (42) 880     2800   8700    0 error (134) .079 6.5 .28 0 true 31   1100 230 2 out of memory 320    15000 3800   0 unknown 8.2 430 110 0 unknown 8.4 430 100 0 true 56     140 780    2 true 49 2100 440 2 timeout 900    1000 12000   0 unknown 140   2000 2200 0 timeout 880    640 6800   0 timeout (verification) 900     2800 8400    0 timeout 900   1100 8700 0 error (7) 52   480 520 0 timeout 900   1200 10000 0 timeout 900   1200 7600 0 timeout 900   160 11000 0
float-benchs/filter1_true-unreach-call.c.v+nlh-reducer.c error (6) .11  25 .90 0 error (42) 880     2800   11000    0 error (134) .053 6.4 .36 0 true 28   900 220 2 out of memory 340    15000 4300   0 unknown 8.2 430 99 0 unknown 8.2 430 100 0 true 59     140 740    2 true 45 1700 410 2 timeout 900    980 11000   0 unknown 140   1800 1800 0 timeout 880    460 8100   0 timeout (verification) 900     2800 9900    0 true 870   1100 11000 2 error (7) 66   540 610 0 timeout 900   1100 8700 0 timeout 900   1200 8000 0 timeout 900   160 11000 0
float-benchs/filter1_true-unreach-call_true-termination.c timeout 900     1800 11000    0 error (42) 880     1600   9500    0 error (42) 880     4100   11000    0 true 20   880 170 2 unknown 900    680 12000   0 unknown 8.3 430 110 0 unknown 8.5 430 100 0 true 50     100 760    2 true 28 1400 200 2 timeout 900    900 6100   0 unknown 54   550 520 0 timeout 880    780 11000   0 timeout (verification) 900     2600 9200    0 true 220   720 2800 2 error (7) 43   400 400 0 true 220   780 1900 2 true 69   780 690 2 timeout 900   150 11000 0
float-benchs/filter2_alt_true-unreach-call.c timeout 900     210 10000    0 error (42) 880     340   9600    0 error (42) 880     220   11000    0 timeout 900   1100 10000 0 unknown 900    240 12000   0 unknown 8.3 430 120 0 unknown 8.3 430 93 0 timeout 900     250 10000    0 timeout 900 1900 7100 0 timeout 900    260 10000   0 unknown 120   2800 1500 0 timeout 880    360 8000   0 timeout (verification) 900     48 11000    0 timeout 900   1000 7800 0 error (7) 22   350 190 0 timeout 900   1000 8200 0 timeout 900   870 9400 0 timeout 900   160 11000 0
float-benchs/filter2_iterated_true-unreach-call.c timeout 900     610 7300    0 out of memory 560     15000   8100    0 out of memory 420     15000   5700    0 timeout 900   2200 10000 0 unknown 900    750 11000   0 true 8.0 370 90 2 true 8.1 370 97 2 timeout 900     1100 12000    0 timeout 900 3000 8800 0 timeout 900    10000 13000   0 unknown 100   2100 1600 0 timeout 880    8300 13000   0 timeout (verification) 900     14000 14000    0 error (7) 38   2200 430 0 error (7) 23   2200 200 0 error (7) 40   2200 480 0 unknown 290   920 2700 0 error (1) 7.5 150 96 0
float-benchs/filter2_reinit_true-unreach-call_true-termination.c timeout 900     780 7500    0 error (42) 880     740   8700    0 error (134) .98  33   15    0 timeout 960   3300 10000 0 unknown 890    390 11000   0 unknown 8.2 430 99 0 unknown 8.4 430 100 0 timeout 900     400 12000    0 timeout 960 4100 9600 0 out of memory 630    15000 8200   0 unknown 58   780 510 0 timeout 880    710 8000   0 timeout (verification) 900     65 9600    0 timeout 900   2500 8400 0 error (7) 53   450 510 0 timeout 900   2500 8900 0 unknown 820   1000 7100 0 error (1) 860   150 12000 0
float-benchs/filter2_set_true-unreach-call_true-termination.c timeout 900     560 5000    0 error (42) 880     1800   8100    0 error (42) 880     540   8500    0 timeout 960   3700 12000 0 unknown 900    310 10000   0 unknown 8.3 430 100 0 unknown 8.3 430 92 0 timeout 900     380 8800    0 timeout 960 3500 10000 0 timeout 900    810 10000   0 unknown 59   990 490 0 timeout 880    580 7700   0 error(unknown, verification-finished) .17  17 2.0  0 timeout 900   3800 8100 0 error (7) 35   540 270 0 error (7) 600   3900 4800 0 unknown 860   870 7100 0 error (1) 860   150 11000 0
float-benchs/filter2_true-unreach-call_true-termination.c timeout 900     680 8200    0 error (42) 870     710   9700    0 error (42) 880     290   8700    0 timeout 960   2900 11000 0 unknown 900    310 9400   0 unknown 8.3 430 110 0 unknown 8.4 430 110 0 timeout 900     350 12000    0 timeout 960 3100 11000 0 timeout 900    590 9500   0 unknown 54   810 570 0 timeout 880    600 7600   0 timeout (verification) 900     56 11000    0 timeout 900   2900 10000 0 error (7) 34   420 270 0 timeout 900   2700 9300 0 timeout 900   710 7300 0 error (1) 860   150 12000 0
float-benchs/filter_iir_true-unreach-call.c timeout 900     310 9000    0 error (42) 880     850   7300    0 error (42) 880     380   8900    0 true 3.7 300 29 2 unknown 900    480 9600   0 unknown 8.2 430 98 0 unknown 8.2 430 100 0 timeout 900     560 12000    0 true 13 1200 100 2 timeout 900    1100 11000   0 unknown 13   310 120 0 timeout 880    680 7200   0 timeout (verification) 900     54 10000    0 timeout 900   2700 8400 0 error (7) 220   1200 2100 0 timeout 900   2600 8400 0 true 93   1300 980 2 error (1) 860   210 9600 0
float-benchs/float_double_true-unreach-call_true-termination.c true .13  24 .72 2 true .050 7.8 .32 2 true .044 6.4 .27 2 true 2.8 250 27 2 unknown .80 66 8.9 0 true 8.1 370 98 2 true 8.1 370 110 2 true .076 26 .68 2 true 11 1200 86 2 true .37 59 3.4 2 true 3.8 210 41 2 true 2.5  77 30   2 true .14  16 1.5  2 true 13   370 130 2 true 12   330 93 2 true 14   360 110 2 true 15   400 140 2 timeout 900   150 11000 0
float-benchs/image_filter_true-unreach-call.c timeout 900     1000 9300    0 error (42) 880     3000   6600    0 error (42) 880     5500   10000    0 out of memory 330   15000 3900 0 unknown 900    510 10000   0 unknown 8.3 430 97 0 unknown 8.4 430 120 0 timeout 900     1900 9300    0 out of memory 260 15000 2700 0 timeout 900    12000 6700   0 unknown 46   3900 470 0 out of memory 68    15000 500   0 error(unknown, verification-finished) .24  21 2.8  0 timeout 900   620 12000 0 timeout 900   520 12000 0 timeout 900   630 13000 0 unknown 92   3000 990 0 error (1) 870   400 9600 0
float-benchs/interpolation2_true-unreach-call.c.p+cfa-reducer.c error (6) .093 24 .86 0 true .91  29   11    2 true .98  29   13    2 true 24   660 260 2 unknown 2.5  67 30   0 unknown 8.0 430 110 0 unknown 8.1 430 110 0 true 3.0   49 39    2 true 46 1500 560 2 true .59 75 6.8 2 true 70   1800 540 2 true 190    240 2200   2 error(unknown, verification-finished) .17  18 1.9  0 timeout 900   1600 6700 0 error (7) 28   380 320 0 timeout 900   1600 7300 0 true 66   520 620 2 timeout 900   160 12000 0
float-benchs/interpolation2_true-unreach-call.c.v+cfa-reducer.c error (6) .082 24 .91 0 true .94  29   13    2 true .97  29   11    2 true 270   790 3500 2 unknown 9.2  100 100   0 unknown 8.1 430 98 0 unknown 8.3 430 100 0 true 3.1   50 48    2 true 290 1500 3900 2 true .61 76 5.6 2 true 70   1800 580 2 true 190    210 2000   2 error(unknown, verification-finished) .16  18 1.7  0 timeout 900   1600 6000 0 timeout 900   1500 7300 0 timeout 900   1600 7300 0 true 84   520 900 2 timeout 900   160 14000 0
float-benchs/interpolation2_true-unreach-call.c.v+nlh-reducer.c error (6) .092 25 .78 0 true 1.1   29   13    2 true 1.3   30   16    2 true 25   490 280 2 unknown 2.6  67 33   0 unknown 8.1 430 110 0 unknown 8.2 430 100 0 true 2.6   59 32    2 true 32 1400 350 2 true .62 76 6.1 2 unknown 56   1900 630 0 true 230    220 2100   2 error(unknown, verification-finished) .20  22 2.0  0 timeout 900   1600 7900 0 timeout 900   1500 8900 0 timeout 900   1700 7400 0 true 71   520 680 2 timeout 900   160 11000 0
float-benchs/interpolation2_true-unreach-call_true-termination.c true .39  24 3.6  2 true .52  12   7.4  2 true .65  12   8.3  2 true 23   620 240 2 unknown 5.3  68 64   0 unknown 8.3 430 110 0 unknown 8.2 430 130 0 true 4.2   45 47    2 true 28 1400 260 2 true .57 66 6.3 2 true 79   1900 610 2 true 190    220 2500   2 error(unknown, verification-finished) .17  18 2.2  0 timeout 900   1600 7400 0 error (7) 27   380 230 0 timeout 900   1600 8000 0 true 78   510 740 2 timeout 900   150 11000 0
float-benchs/interpolation_true-unreach-call.c.p+cfa-reducer.c error (6) .11  24 .81 0 true .62  20   6.5  2 true .62  21   8.5  2 true 16   610 140 2 unknown 1.9  67 24   0 unknown 8.2 430 120 0 unknown 8.5 430 120 0 true 2.0   41 29    2 true 24 1400 180 2 true .47 66 3.9 2 true 66   1800 470 2 true 70    160 710   2 error(unknown, verification-finished) .17  17 1.7  0 timeout 900   1500 9800 0 error (7) 390   1100 3300 0 timeout 900   1500 6200 0 true 61   520 650 2 timeout 900   160 12000 0
float-benchs/interpolation_true-unreach-call.c.v+cfa-reducer.c error (6) .090 24 .65 0 true .58  20   8.0  2 true .57  21   7.2  2 true 23   580 250 2 unknown 4.2  79 55   0 unknown 8.3 430 110 0 unknown 8.5 430 110 0 true 2.0   41 29    2 true 32 1400 350 2 true .47 66 5.1 2 true 66   1800 470 2 true 84    210 790   2 error(unknown, verification-finished) .16  17 2.1  0 timeout 900   1500 7600 0 timeout 900   1500 6700 0 timeout 900   1500 7800 0 true 69   510 730 2 timeout 900   150 11000 0
float-benchs/interpolation_true-unreach-call.c.v+nlh-reducer.c error (6) .093 24 .88 0 true .67  21   8.3  2 true .75  21   10    2 true 19   460 250 2 unknown 2.0  67 24   0 unknown 8.2 430 99 0 unknown 8.4 430 90 0 true 1.7   48 26    2 true 27 1400 250 2 true .48 67 5.1 2 unknown 54   1700 560 0 true 100    200 1200   2 error(unknown, verification-finished) .16  17 2.2  0 timeout 900   1500 8100 0 timeout 900   1300 7700 0 timeout 900   1500 6400 0 true 66   490 710 2 timeout 900   160 11000 0
float-benchs/interpolation_true-unreach-call_true-termination.c true .20  24 2.9  2 true .25  8.7 3.0  2 true .36  9.6 5.0  2 true 14   550 140 2 unknown 2.1  67 26   0 unknown 8.2 430 110 0 unknown 8.4 430 94 0 true 2.2   39 33    2 true 21 1300 170 2 true .45 61 4.3 2 true 78   1700 530 2 true 77    150 1200   2 error(unknown, verification-finished) .19  17 2.0  0 timeout 900   1700 7600 0 error (7) 190   790 2200 0 timeout 900   1600 7000 0 true 170   510 2000 2 timeout 900   200 11000 0
float-benchs/inv_Newton_true-unreach-call.c timeout 900     1000 8500    0 error (42) 880     440   7200    0 error (42) 880     390   7700    0 timeout 900   2500 8600 0 unknown 900    280 13000   0 unknown 8.1 430 120 0 unknown 8.4 430 100 0 timeout 900     300 10000    0 timeout 900 3500 8800 0 timeout 900    220 5500   0 unknown 76   1000 640 0 timeout 880    800 7800   0 error(unknown, verification-finished) .17  18 2.4  0 error (7) 500   1600 4900 0 true 25   380 220 2 error (7) 550   1900 3900 0 unknown 580   410 4500 0 timeout 900   150 11000 0
float-benchs/inv_sqrt_Quake_true-unreach-call.c.v+cfa-reducer.c error (6) .088 24 .72 0 true .39  18   5.2  2 true .94  20   10    2 true 4.6 310 43 2 unknown 9.7  65 110   0 unknown 8.2 430 94 0 unknown 8.3 430 120 0 true 4.5   48 58    2 true 16 1200 120 2 true .73 71 7.8 2 true 13   410 130 2 true 720    340 5300   2 error(unknown, verification-finished) .16  17 1.8  0 error (7) 120   1700 950 0 error (7) 34   440 290 0 error (7) 120   1700 890 0 true 52   550 570 2 timeout 900   150 14000 0
float-benchs/inv_sqrt_Quake_true-unreach-call_true-termination.c true .28  24 3.7  2 true .46  12   5.7  2 true .24  12   3.1  2 true 3.4 280 33 2 unknown 3.9  66 43   0 unknown 8.1 430 110 0 unknown 8.4 430 100 0 true 1.1   40 14    2 true 14 1100 110 2 true .76 61 9.0 2 true 38   840 290 2 true 150    170 1600   2 error(unknown, verification-finished) .17  18 2.4  0 true 110   1800 1000 2 error (7) 55   370 620 0 true 110   1800 930 2 true 48   670 480 2 error (1) 860   150 11000 0
float-benchs/inv_square_int_true-unreach-call_true-termination.c true .13  24 1.2  2 true .14  6.9 .92 2 true .11  7.2 1.0  2 true 3.1 260 29 2 unknown 1.6  66 21   0 unknown 8.3 430 120 0 error - divine failed with signal 11 1.8 200 22 0 true .36  29 4.4  2 true 15 1200 100 2 true .40 59 3.3 2 true 27   470 230 2 true 4.1  89 52   2 true .18  19 2.4  2 true 20   340 190 2 true 18   360 140 2 true 21   370 230 2 true 24   440 260 2 timeout 900   150 11000 0
float-benchs/inv_square_true-unreach-call_true-termination.c true .12  24 1.3  2 true .14  6.3 .59 2 true .084 6.9 .78 2 true 2.9 270 27 2 unknown 1.5  66 16   0 unknown 8.1 430 120 0 unknown 8.3 430 110 0 true .30  28 4.3  2 true 14 1100 100 2 true .38 59 3.1 2 true 6.2 310 50 2 true 3.9  81 51   2 error(unknown, verification-finished) .19  18 1.8  0 true 66   370 870 2 true 17   350 170 2 true 67   370 790 2 true 47   440 470 2 timeout 900   150 11000 0
float-benchs/loop_true-unreach-call.c timeout 900     330 7300    0 out of memory 360     15000   5500    0 out of memory 260     15000   3400    0 timeout 960   1200 13000 0 unknown 900    300 13000   0 true 440   2300 4400 2 true 450   2300 4300 2 timeout 900     1800 13000    0 timeout 900 3700 8700 0 timeout 900    14000 11000   0 unknown 37   1300 400 0 true 880    480 7800   2 true 13     740 180    2 true 180   450 2300 2 error (7) 110   660 1300 0 true 220   540 2500 2 true 78   680 900 2 timeout 900   150 11000 0
float-benchs/mea8000_true-unreach-call.c timeout 900     2800 9400    0 out of memory 250     14000   2900    0 out of memory 100     15000   1200    0 error 5.5 320 51 0 unknown 900    1500 11000   0 error - divine failed with exitcode 1 1.2 170 13 0 error - divine failed with exitcode 1 1.3 170 17 0 timeout 900     1900 8200    0 timeout 920 8100 8700 0 out of memory 51    15000 680   0 unknown 27   830 230 0 error (1) 1.3  49 17   0 timeout (verification) 900     51 9200    0 timeout 900   6200 6800 0 timeout 900   5500 11000 0 timeout 900   6700 9300 0 out of memory 540   15000 4300 0 error (1) 4.5 160 45 0
float-benchs/nan_double_range_true-unreach-call_true-termination.c true .10  24 .78 2 true .050 6.1 .36 2 true .049 6.8 .43 2 true 2.8 250 25 2 unknown .80 65 8.4 0 unknown 8.2 430 100 0 unknown 8.4 430 110 0 true .075 26 .92 2 true 12 1200 88 2 true .36 59 3.4 2 true 10   300 110 2 true 2.5  72 31   2 error(unknown, verification-finished) .16  18 1.8  0 true 12   330 110 2 true 14   370 100 2 true 13   350 98 2 true 16   410 140 2 timeout 900   150 12000 0
float-benchs/nan_float_range_true-unreach-call_true-termination.c true .13  24 .72 2 true .067 6.6 .33 2 true .053 6.5 .35 2 true 3.0 260 25 2 unknown .80 66 8.4 0 unknown 8.1 430 120 0 unknown 8.3 430 100 0 true .11  26 .82 2 true 11 1200 88 2 true .36 58 3.0 2 true 10   300 110 2 true 2.6  74 41   2 error(unknown, verification-finished) .17  17 2.3  0 true 13   340 120 2 true 13   330 100 2 true 14   370 130 2 true 18   440 200 2 timeout 900   150 12000 0
float-benchs/rlim_exit_true-unreach-call_true-termination.c timeout 900     2400 12000    0 error (42) 880     5300   6600    0 out of memory 170     15000   2500    0 timeout 960   4200 8500 0 unknown 900    230 12000   0 unknown 8.2 430 120 0 unknown 8.4 430 98 0 timeout 900     12000 10000    0 timeout 960 4800 9100 0 timeout 900    2000 9700   0 unknown 110   1700 1500 0 timeout 880    660 8100   0 timeout (verification) 900     51 12000    0 timeout 900   1700 12000 0 timeout 900   5200 12000 0 timeout 900   1300 7900 0 out of memory 100   15000 1300 0 timeout 900   150 11000 0
float-benchs/rlim_invariant_true-unreach-call.c.p+cfa-reducer.c error (6) .12  24 .73 0 error (42) 880     1500   7900    0 error (42) 880     2300   12000    0 true 13   460 98 2 unknown 900    1300 12000   0 unknown 8.2 430 98 0 unknown 8.4 430 95 0 timeout 900     1400 8900    0 true 22 1300 160 2 timeout 900    1200 8300   0 unknown 570   4100 5500 0 timeout 880    440 9100   0 timeout (verification) 900     54 12000    0 timeout 900   1100 10000 0 error (7) 110   530 1600 0 timeout 900   1100 11000 0 timeout 900   1800 6900 0 timeout 900   150 12000 0
float-benchs/rlim_invariant_true-unreach-call.c.v+lhb-reducer.c error (6) .16  25 1.7  0 error (42) 880     2500   6700    0 error (42) 880     2500   11000    0 true 17   660 130 2 out of memory 270    15000 3100   0 unknown 8.3 430 100 0 unknown 8.1 430 99 0 true 590     680 6400    2 true 26 1600 200 2 timeout 900    1300 9800   0 unknown 170   2100 2100 0 timeout 880    410 9200   0 timeout (verification) 900     54 9900    0 timeout 900   1000 6800 0 error (7) 170   570 2500 0 timeout 900   1000 9900 0 timeout 900   3000 11000 0 timeout 900   170 11000 0
float-benchs/rlim_invariant_true-unreach-call.c.v+nlh-reducer.c error (6) .47  84 5.3  0 error (42) 880     2500   6500    0 error (42) 880     2600   10000    0 true 17   670 120 2 out of memory 280    15000 3100   0 unknown 8.1 430 120 0 unknown 8.5 430 110 0 true 620     700 7200    2 true 25 1600 160 2 timeout 900    1200 5800   0 unknown 170   2000 2500 0 timeout 880    450 6600   0 timeout (verification) 900     54 12000    0 timeout 900   1000 8000 0 error (7) 72   480 860 0 timeout 900   990 7600 0 timeout 900   1400 8400 0 error (1) 860   170 11000 0
float-benchs/rlim_invariant_true-unreach-call_true-termination.c timeout 900     2300 9700    0 error (42) 880     1100   6300    0 error (42) 880     3200   11000    0 true 9.5 400 74 2 unknown 61    170 860   0 unknown 8.2 430 110 0 unknown 8.3 430 130 0 true 4.1   39 53    2 true 20 1300 130 2 out of memory 130    15000 1800   0 unknown 860   4300 9300 0 timeout 880    420 9000   0 timeout (verification) 900     51 9800    0 true 830   1000 9300 2 error (7) 57   460 840 0 timeout 900   1000 14000 0 true 60   600 610 2 timeout 900   190 10000 0
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call_true-termination.c timeout 900     300 9700    0 error (42) 880     630   7100    0 error (42) 870     530   12000    0 timeout 900   880 10000 0 unknown 900    500 10000   0 unknown 8.2 430 92 0 unknown 8.4 430 120 0 timeout 900     480 12000    0 timeout 900 2000 10000 0 true 13    420 140   2 unknown 28   670 290 0 timeout 880    3100 6800   0 error(unknown, verification-finished) .18  17 2.2  0 timeout 900   1800 6800 0 error (7) 78   1400 620 0 timeout 900   1800 7000 0 timeout 900   290 11000 0 error (1) 870   280 11000 0
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call_true-termination.c timeout 900     310 7800    0 error (42) 880     630   7700    0 error (42) 880     510   11000    0 timeout 900   1000 10000 0 unknown 900    480 11000   0 unknown 8.2 430 130 0 unknown 8.4 430 100 0 timeout 900     490 9800    0 timeout 900 1900 7900 0 true 21    420 210   2 unknown 28   690 290 0 timeout 880    3700 11000   0 error(unknown, verification-finished) .20  18 2.1  0 timeout 900   1800 7000 0 error (7) 81   1400 660 0 timeout 900   1800 7500 0 timeout 900   290 11000 0 error (1) 860   290 11000 0
float-benchs/sin_interpolated_index_true-unreach-call_true-termination.c timeout 900     300 11000    0 error (42) 880     610   8100    0 error (42) 880     470   11000    0 timeout 900   600 10000 0 unknown 710    120 10000   0 unknown 8.4 430 97 0 unknown 8.5 430 110 0 true 230     110 2900    2 timeout 900 1600 11000 0 true 170    130 2200   2 unknown 29   730 320 0 timeout 880    3300 6800   0 error(unknown, verification-finished) .17  17 2.1  0 timeout 900   2300 10000 0 error (7) 46   1200 430 0 timeout 900   2400 9100 0 timeout 900   290 14000 0 error (1) 870   280 12000 0
float-benchs/sin_interpolated_negation_true-unreach-call.c timeout 900     540 7200    0 error (42) 880     4900   6900    0 error (42) 880     3000   11000    0 timeout 900   3400 8700 0 unknown 900    920 9100   0 unknown 8.2 430 100 0 unknown 8.3 430 100 0 timeout 900     1700 9200    0 timeout 900 4400 8600 0 out of memory 83    15000 920   0 unknown 680   6500 9300 0 timeout 880    4600 8600   0 error(unknown, verification-finished) .18  19 2.0  0 timeout 900   2400 9300 0 error (7) 580   2200 4500 0 timeout 900   2100 6700 0 true 340   1500 2900 2 error (1) 860   500 12000 0
float-benchs/sin_interpolated_smallrange_true-unreach-call.c timeout 900     450 6500    0 error (42) 870     3500   6800    0 error (42) 880     1400   12000    0 timeout 900   5600 12000 0 unknown 900    870 11000   0 unknown 8.3 430 120 0 unknown 8.4 430 110 0 timeout 900     1200 11000    0 timeout 900 6100 11000 0 out of memory 200    15000 1800   0 unknown 28   670 290 0 timeout 880    3100 7800   0 error(unknown, verification-finished) .20  19 2.0  0 error (7) 570   3200 4500 0 error (7) 73   1300 600 0 error (7) 570   3300 4200 0 true 230   1500 2100 2 error (1) 860   300 11000 0
float-benchs/sqrt_Householder_constant_true-unreach-call.c timeout 900     340 7700    0 true .85  10   13    2 true .79  10   13    2 true 4.6 270 40 2 unknown 900    1100 8600   0 true 8.2 370 100 2 true 8.3 370 96 2 timeout 900     1400 11000    0 true 16 1200 110 2 true .57 59 5.3 2 unknown 470   3500 4100 0 timeout 880    2400 6400   0 true .15  15 1.7  2 error (7) 230   3100 1700 0 error (7) 220   1800 1600 0 error (7) 250   3000 1800 0 true 110   1500 1000 2 timeout 900   150 13000 0
float-benchs/sqrt_Householder_constant_true-unreach-call.c.p+cfa-reducer.c error (6) .092 24 .82 0 true 1.1   13   14    2 true 1.1   14   15    2 true 4.9 270 45 2 unknown 900    6900 9200   0 true 8.1 370 100 2 true 8.2 370 110 2 out of memory 140     15000 1500    0 true 16 1400 120 2 true .66 59 6.8 2 unknown 470   3600 3200 0 timeout 880    8600 9300   0 true .16  15 1.9  2 error (7) 380   3400 3100 0 error (7) 190   1800 1600 0 error (7) 840   3900 7800 0 true 110   1500 1100 2 timeout 900   150 11000 0
float-benchs/sqrt_Householder_interval_true-unreach-call.c timeout 900     320 9500    0 error (42) 880     820   6700    0 error (42) 880     610   6900    0 timeout 900   1600 10000 0 unknown 900    500 8400   0 unknown 8.1 430 97 0 unknown 8.3 430 100 0 timeout 900     490 9700    0 timeout 900 1800 11000 0 timeout 900    370 8100   0 unknown 23   720 240 0 timeout 880    2600 6800   0 error(unknown, verification-finished) .17  18 1.8  0 error (7) 160   2700 1300 0 error (7) 100   1800 990 0 error (7) 160   2800 1400 0 timeout 900   1200 8800 0 error (1) 860   170 12000 0
float-benchs/sqrt_Householder_pseudoconstant_true-unreach-call.c timeout 900     430 6600    0 error (42) 880     2700   8900    0 error (42) 870     340   8500    0 timeout 900   3600 9700 0 unknown 900    1100 10000   0 unknown 8.2 430 94 0 unknown 8.4 430 110 0 timeout 900     1200 8600    0 timeout 900 2200 9800 0 timeout 900    700 7700   0 unknown 23   700 210 0 timeout 880    2500 7700   0 error(unknown, verification-finished) .18  17 2.1  0 error (7) 110   2600 970 0 error (7) 110   1800 1300 0 error (7) 93   2600 790 0 out of memory 220   15000 2100 0 error (1) 860   170 11000 0
float-benchs/sqrt_Newton_pseudoconstant_true-unreach-call.c timeout 900     490 6000    0 error (42) 880     2600   7900    0 error (42) 880     420   8300    0 timeout 900   2500 10000 0 unknown 900    850 11000   0 unknown 8.1 430 87 0 unknown 8.4 430 99 0 timeout 900     1200 9200    0 timeout 900 2000 9800 0 timeout 900    520 7900   0 unknown 23   650 210 0 timeout 880    2400 6500   0 error(unknown, verification-finished) .17  17 1.8  0 error (7) 120   2600 1000 0 error (7) 120   1800 1100 0 error (7) 120   2600 1200 0 out of memory 300   15000 3100 0 error (1) 860   150 11000 0
float-benchs/sqrt_biNewton_pseudoconstant_true-unreach-call.c timeout 900     370 6300    0 error (42) 880     3300   8900    0 error (42) 880     460   9200    0 timeout 900   3000 8700 0 unknown 900    530 8700   0 unknown 8.2 430 110 0 unknown 8.4 430 98 0 timeout 900     1300 10000    0 timeout 900 2300 11000 0 timeout 900    750 8300   0 unknown 23   730 240 0 timeout 880    4100 10000   0 error(unknown, verification-finished) .18  18 2.3  0 error (7) 100   2700 840 0 error (7) 84   1800 770 0 error (7) 110   2700 1200 0 out of memory 97   15000 1100 0 error (1) 860   180 12000 0
float-benchs/sqrt_poly_true-unreach-call_true-termination.c true 1.1   53 12    2 true 2.0   43   23    2 true .89  42   10    2 true 31   490 370 2 unknown 51    160 620   0 unknown 8.1 430 95 0 unknown 8.2 430 110 0 true 17     150 200    2 true 41 1400 370 2 true .88 88 10   2 true 36   700 370 2 timeout 880    690 6500   0 error(unknown, verification-finished) .17  18 1.8  0 true 150   1600 1200 2 error (7) 100   850 810 0 true 150   1600 1100 2 true 76   760 780 2 error (1) 860   150 10000 0
float-benchs/water_pid_true-unreach-call_true-termination.c timeout 900     800 6900    0 true .59  11   7.7  2 true .54  7.9 6.6  2 true 5.1 270 42 2 unknown 370    210 4500   0 true 8.2 370 99 2 true 8.1 370 96 2 true 19     120 310    2 true 15 1200 100 2 true .53 59 6.2 2 unknown 460   3800 3300 0 timeout 880    470 7800   0 true .14  16 1.7  2 error (7) 170   2900 1600 0 error (7) 110   1800 830 0 error (7) 150   3000 1500 0 true 100   1700 1000 2 timeout 900   150 11000 0
float-benchs/zonotope_2_true-unreach-call_true-termination.c timeout 900     330 8700    0 true 110     4500   1500    2 true 93     1900   1400    2 timeout 970   3600 6800 0 unknown 900    370 10000   0 true 22   410 240 2 true 22   410 250 2 timeout