Benchmark CPA/CoVeriTest CPA/Tiger-MGP ESBMC-bkind ESBMC-falsif FairFuzz KLEE PRtest Symbiotic VeriFuzz
Tool CPAchecker 1.8-svn 30375 CPAchecker 1.8-svn 30541M ESBMC version 6.0.0 64-bit x86_64 linux FairFuzz TC-0.0.2 KLEE 2.0.0-pre-test-comp tbf v0.3.0-testcomp19 symbiotic 6.0.3-dev-fd3f777b VeriFuzz 1.0.1
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.15.0-45-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 2019-02-05 21:05:56 CET 2019-02-05 21:13:54 CET 2019-02-05 21:13:25 CET 2019-02-05 21:11:17 CET 2019-02-08 09:39:09 CET 2019-02-05 21:09:47 CET 2019-02-06 06:02:44 CET 2019-02-06 07:07:32 CET 2019-02-06 07:17:17 CET
Run set coveritest.test-comp19_prop-coverage-error-call.ReachSafety-Floats cpa-tiger.test-comp19_prop-coverage-error-call.ReachSafety-Floats esbmc-kind.test-comp19_prop-coverage-error-call.ReachSafety-Floats esbmc-falsi.test-comp19_prop-coverage-error-call.ReachSafety-Floats fairfuzz.test-comp19_prop-coverage-error-call.ReachSafety-Floats klee.test-comp19_prop-coverage-error-call.ReachSafety-Floats prtest.test-comp19_prop-coverage-error-call.ReachSafety-Floats symbiotic.test-comp19_prop-coverage-error-call.ReachSafety-Floats verifuzz.test-comp19_prop-coverage-error-call.ReachSafety-Floats
Options -benchmark -heap 10000M -testcomp19 -benchmark -heap 10000M -tigertestcomp19 -s kinduction -s falsi --stats -i random --write-xml --svcomp-nondets --test-comp --verifier klee-testcomp --testcomp
../sv-benchmarks/c/ status score cpu (s) mem (MB) energy (J) status score cpu (s) mem (MB) energy (J) status score cpu (s) mem (MB) energy (J) status score cpu (s) mem (MB) energy (J) status score cpu (s) mem (MB) energy (J) status score cpu (s) mem (MB) energy (J) status score cpu (s) mem (MB) energy (J) status score cpu (s) mem (MB) energy (J) status score cpu (s) mem (MB) energy (J)
floats-cdfpl/newton_1_4.yml 1 94   380 610 1 76   370 580 25     92 310    25     93 330    900   11 12000 .11 21 1.3  1 .27 31 2.7 .42 18 5.0 1 10   150 120
floats-cdfpl/newton_1_5.yml 1 77   370 540 1 56   370 560 33     92 400    33     93 420    900   10 12000 .11 21 1.4  1 .25 31 3.0 .44 18 4.6 1 7.3 150 71
floats-cdfpl/newton_1_6.yml 1 64   370 630 1 45   370 340 41     94 570    41     92 530    900   10 12000 .12 21 1.0  1 .24 31 3.5 .42 19 5.2 1 7.9 150 79
floats-cdfpl/newton_1_7.yml 1 41   370 330 1 22   380 180 8.8   93 120    8.9   92 110    900   10 10000 .13 21 1.4  1 .27 30 4.7 .44 18 5.2 1 6.9 150 89
floats-cdfpl/newton_1_8.yml 1 36   380 290 1 16   360 120 39     92 490    39     93 500    900   10 12000 .12 21 2.0  1 .26 31 3.0 .43 18 4.9 1 6.9 150 83
floats-cdfpl/newton_2_6.yml 1 160   480 1100 1 130   470 970 130     190 1700    130     190 1900    900   10 14000 .15 21 1.0  1 .24 30 3.2 .42 18 5.5 1 42   150 370
floats-cdfpl/newton_2_7.yml 1 100   480 760 1 84   460 600 130     190 1500    120     190 1400    900   10 13000 .12 21 1.2  1 .24 31 3.5 .45 19 5.2 1 26   150 270
floats-cdfpl/newton_2_8.yml 1 62   470 600 1 43   460 360 60     190 830    60     190 770    1 900   11 12000 .12 21 1.4  1 .26 31 2.8 .43 18 5.0 1 19   150 190
floats-cdfpl/newton_3_6.yml 1 310   600 2300 1 290   570 2500 100     290 1200    100     290 1200    900   10 14000 .12 21 1.2  1 .27 31 3.2 .43 19 5.3 1 320   220 3900
floats-cdfpl/newton_3_7.yml 1 220   600 1900 1 200   570 1300 120     280 1400    120     280 1400    900   10 14000 .13 21 1.1  1 .26 31 3.2 .44 18 6.3 1 74   230 940
floats-cdfpl/newton_3_8.yml 1 190   600 1300 1 160   570 1400 130     300 1600    130     300 1600    900   10 12000 .12 21 1.4  1 .26 31 5.0 .43 19 6.1 1 36   200 360
floats-cdfpl/sine_1.yml 1 29   340 290 1 8.7 330 91 20     65 230    20     65 240    1 900   10 12000 .14 21 1.1  1 .25 30 3.1 .42 19 5.0 1 5.2 150 51
floats-cdfpl/sine_2.yml 1 66   350 590 1 44   360 360 20     63 270    20     64 260    1 900   10 13000 .12 21 1.8  1 .28 31 3.1 .41 19 4.5 1 4.6 150 59
floats-cdfpl/sine_3.yml 1 300   450 2800 1 280   440 2700 19     64 260    19     64 250    900   10 11000 .14 21 1.2  1 .25 31 2.5 .41 19 5.1 1 5.6 150 63
floats-cdfpl/square_1.yml 1 37   1500 400 1 18   350 150 4.7   57 60    4.7   54 59    900   10 13000 .13 21 1.1  1 .31 31 3.3 .41 19 5.5 1 9.6 150 120
floats-cdfpl/square_2.yml 1 200   1600 2100 1 180   510 1500 6.8   55 85    6.8   60 81    900   11 11000 .12 21 1.1  1 1.3  31 15   .40 19 4.5 1 22   150 250
floats-cdfpl/square_3.yml 1 82   1500 750 1 61   360 440 7.5   55 99    7.5   54 92    900   10 13000 .14 21 .98 1 8.0  31 91   .39 18 4.9 1 12   150 170
float-benchs/cast_float_ptr.yml 3.4 270 33 2.8 270 27 1 .11  26 1.0  1 .10  26 1.2  1 13   15 60 .13 21 1.5  .25 31 3.6 .39 19 4.9 1 3.8 150 43
float-benchs/cast_union_loose.yml 3.7 280 40 3.2 280 29 1 .15  26 1.9  1 .15  26 1.8  1 900   11 14000 .13 21 1.4  1 3.3  31 40   .45 19 5.7 1 3.7 150 39
float-benchs/cast_union_tight.yml 3.8 270 40 3.2 290 30 1 .17  27 1.7  1 .16  27 1.5  1 9.4 16 27 .13 21 1.2  1 .25 30 3.1 .41 18 5.8 1 3.6 150 30
float-benchs/float_int_inv_square.yml 1 3.6 280 35 1 2.9 280 28 1 .36  28 4.4  1 .36  28 4.9  1 900   11 11000 .16 21 1.4  900    31 9900   1 .54 21 7.4 1 3.7 150 39
float-benchs/inv_Newton-2.yml 6.1 350 63 3.0 270 30 900     300 12000    900     300 10000    3.1 11 42 .11 21 2.3  .25 31 3.0 .44 19 5.7 1 5.0 150 55
float-benchs/inv_Newton.c.p+cfa-reducer.yml 1 6.8 350 74 4.4 350 47 470     530 4100    900     1300 8700    16   15 56 .11 21 1.3  .27 31 3.2 .41 18 5.1 1 4.5 150 47
float-benchs/inv_square-1.yml 1 3.4 270 34 1 3.0 280 31 .30  28 3.9  .33  28 4.4  740   11 9200 .13 21 1.3  1 .26 31 2.6 .41 18 5.8 900   150 11000
float-benchs/nan_double.yml 3.4 270 31 2.8 270 23 1 .085 26 1.1  1 .082 26 .95 1 20   16 120 .13 21 1.1  .25 31 3.5 .36 18 5.0 1 3.4 150 36
float-benchs/nan_float.yml 3.2 260 31 3.1 280 31 1 .088 26 .98 1 .085 26 1.0  1 19   16 89 .12 21 2.4  1 .26 31 2.9 .36 18 4.6 1 3.6 150 36
float-benchs/sin_interpolated_index-1.yml 1 25   570 220 1 4.8 360 44 9.1   100 110    9.1   100 110    890   10 11000 .12 21 1.4  900    31 12000   .51 18 5.5 1 6.9 280 82
float-benchs/sqrt_poly2.yml 1 15   440 120 1 11   430 100 58     150 580    58     150 800    3.1 11 48 .14 21 1.2  .24 31 3.6 .46 18 7.5 1 4.0 150 44
float-newlib/double_req_bl_0870a.yml 6.9 460 63 5.4 360 47 .24  40 2.6  .25  40 3.0  1 44   17 110 .15 21 1.6  900    31 13000   1.4  20 19   1 590   170 7600
float-newlib/float_req_bl_0870a.yml 1 350   2700 3200 4.9 300 42 .20  32 2.4  .20  32 2.1  11   15 41 .15 21 1.4  1 350    31 5300   1.3  19 18   1 130   170 1700
loop-floats-scientific-comp/loop1-2.yml 1 4.2 300 40 1 3.5 300 36 1.6   46 18    1.6   46 22    1 70   18 340 900    75 11000    1 680    47 9800   900    61 9500   1 3.4 150 40
loop-floats-scientific-comp/loop2-1.yml 1 4.6 300 51 1 3.7 300 37 1.3   42 17    1.3   42 16    3.1 10 42 .13 21 1.2  1 710    42 11000   .49 19 6.1 3.7 150 38
../sv-benchmarks/c/ status score cpu (s) mem (MB) energy (J) status score cpu (s) mem (MB) energy (J) status score cpu (s) mem (MB) energy (J) status score cpu (s) mem (MB) energy (J) status score cpu (s) mem (MB) energy (J) status score cpu (s) mem (MB) energy (J) status score cpu (s) mem (MB) energy (J) status score cpu (s) mem (MB) energy (J) status score cpu (s) mem (MB) energy (J)
total 32 25 2500 18000 21000 32 23 1800 12000 15000 32 6 2300    3700 28000 32 6 2800    4400 31000 32 11 19000 380 260000 32 900 730 11000 32 24 4500 1000 61000 32 1 920 640 9700 32 30 2300 5200 28000
Run set coveritest.test-comp19_prop-coverage-error-call.ReachSafety-Floats cpa-tiger.test-comp19_prop-coverage-error-call.ReachSafety-Floats esbmc-kind.test-comp19_prop-coverage-error-call.ReachSafety-Floats esbmc-falsi.test-comp19_prop-coverage-error-call.ReachSafety-Floats fairfuzz.test-comp19_prop-coverage-error-call.ReachSafety-Floats klee.test-comp19_prop-coverage-error-call.ReachSafety-Floats prtest.test-comp19_prop-coverage-error-call.ReachSafety-Floats symbiotic.test-comp19_prop-coverage-error-call.ReachSafety-Floats verifuzz.test-comp19_prop-coverage-error-call.ReachSafety-Floats