Benchmark CPA/CoVeriTest
Tool CPAchecker 1.8-svn 30375
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
Run set [test-comp19_prop-coverage-error-call.ReachSafety-Arrays; test-comp19_prop-coverage-error-call.ReachSafety-BitVectors; test-comp19_prop-coverage-error-call.ReachSafety-ControlFlow; test-comp19_prop-coverage-error-call.ReachSafety-ECA; test-comp19_prop-coverage-error-call.ReachSafety-Floats; test-comp19_prop-coverage-error-call.ReachSafety-Heap; test-comp19_prop-coverage-error-call.ReachSafety-Loops; test-comp19_prop-coverage-error-call.ReachSafety-Recursive; test-comp19_prop-coverage-error-call.ReachSafety-Sequentialized]
Options -benchmark -heap 10000M -testcomp19
../sv-benchmarks/c/ status cov cpu (s) mem (MB) energy (J)
array-examples/standard_copy1_ground-2.yml 900   2200 11000
array-examples/standard_copy2_ground-1.yml 900   2400 12000
array-examples/standard_copy3_ground-2.yml 900   2700 12000
array-examples/standard_copy4_ground-2.yml 900   2800 11000
array-examples/standard_copy5_ground-2.yml 900   2800 10000
array-examples/standard_copy6_ground-1.yml 900   2700 11000
array-examples/standard_copy7_ground-1.yml 900   2700 13000
array-examples/standard_copy8_ground-2.yml 900   3100 12000
array-examples/standard_copy9_ground-1.yml 900   3300 11000
array-examples/standard_partition_ground-1.yml 900   2200 11000
array-industry-pattern/array_ptr_single_elem_init-2.yml 900   1800 12000
array-industry-pattern/array_single_elem_init.yml 900   2000 12000
reducercommutativity/rangesum.yml 48   940 460
reducercommutativity/rangesum05.yml 99   2400 980
reducercommutativity/rangesum10.yml 900   3600 8200
reducercommutativity/rangesum20.yml 900   4400 9800
reducercommutativity/rangesum40.yml 900   4700 10000
reducercommutativity/rangesum60.yml 900   5200 12000
array-tiling/mlceu.yml 900   910 10000
array-tiling/skippedu.yml 1 23   780 190
array-programs/copysome1-2.yml 900   2900 10000
array-programs/copysome2-2.yml 900   2900 10000
bitvector/byte_add-1.yml 1 33   1100 380
bitvector/s3_clnt_1.BV.c.cil-2.yml 1 9.3 320 82
bitvector/s3_clnt_2.BV.c.cil-2.yml 1 35   1000 330
bitvector/s3_clnt_3.BV.c.cil-2.yml 1 7.2 350 58
bitvector/soft_float_1-3.c.cil.yml 1 23   790 200
bitvector/soft_float_4-3.c.cil.yml 1 16   600 130
bitvector/sum02-1.yml 900   5500 9000
bitvector-regression/recHanoi03-1.yml 140   15000 1400
bitvector-loops/diamond_2-1.yml 1 25   1100 230
bitvector-loops/verisec_sendmail_tTflag_arr_one_loop.yml 900   1600 12000
ntdrivers-simplified/cdaudio_simpl1.cil-1.yml 1 7.6 330 69
ntdrivers-simplified/floppy_simpl3.cil-1.yml 1 7.2 290 64
ntdrivers-simplified/floppy_simpl4.cil-1.yml 1 8.4 320 71
ntdrivers-simplified/kbfiltr_simpl2.cil-2.yml 1 6.4 290 57
ssh-simplified/s3_clnt_1.cil-2.yml 1 7.1 330 68
ssh-simplified/s3_clnt_2.cil-1.yml 1 7.2 340 66
ssh-simplified/s3_clnt_3.cil-2.yml 1 7.1 290 68
ssh-simplified/s3_clnt_4.cil-2.yml 1 6.9 330 64
eca-rers2012/Problem03_label09.yml 1 21   760 170
eca-rers2012/Problem03_label13.yml 1 19   760 170
eca-rers2012/Problem03_label26.yml 1 16   610 150
eca-rers2012/Problem03_label27.yml 1 18   590 160
eca-rers2012/Problem03_label28.yml 1 18   620 160
eca-rers2012/Problem03_label31.yml 1 20   700 160
eca-rers2012/Problem03_label35.yml 1 21   810 160
eca-rers2012/Problem03_label37.yml 1 15   530 130
eca-rers2012/Problem03_label39.yml 1 20   750 160
eca-rers2012/Problem03_label43.yml 1 16   530 150
eca-rers2012/Problem03_label45.yml 1 20   880 170
eca-rers2012/Problem03_label50.yml 1 19   710 150
eca-rers2012/Problem03_label52.yml 1 20   890 180
eca-rers2012/Problem04_label04.yml 1 140   4800 1200
eca-rers2012/Problem04_label06.yml 1 130   4700 1400
eca-rers2012/Problem04_label09.yml 1 99   4100 1000
eca-rers2012/Problem04_label13.yml 1 110   4500 970
eca-rers2012/Problem04_label15.yml 1 100   4200 950
eca-rers2012/Problem04_label18.yml 1 230   5600 2300
eca-rers2012/Problem04_label19.yml 1 240   6300 2600
eca-rers2012/Problem04_label26.yml 1 110   4500 1100
eca-rers2012/Problem04_label31.yml 1 210   5800 2000
eca-rers2012/Problem04_label32.yml 1 200   5500 2000
eca-rers2012/Problem04_label35.yml 1 230   5600 2600
eca-rers2012/Problem04_label38.yml 1 220   5700 2200
eca-rers2012/Problem04_label39.yml 1 120   4500 1400
eca-rers2012/Problem04_label45.yml 1 120   4700 1100
eca-rers2012/Problem04_label52.yml 1 120   4800 1100
eca-rers2012/Problem04_label55.yml 1 110   4500 970
eca-rers2012/Problem05_label00.yml 1 180   5000 2000
eca-rers2012/Problem05_label01.yml 1 140   4800 1400
eca-rers2012/Problem05_label11.yml 1 130   4700 1100
eca-rers2012/Problem05_label13.yml 1 250   5600 2400
eca-rers2012/Problem05_label15.yml 1 120   4800 1200
eca-rers2012/Problem05_label18.yml 1 120   4700 1100
eca-rers2012/Problem05_label24.yml 1 130   4800 1300
eca-rers2012/Problem05_label26.yml 1 190   5000 2000
eca-rers2012/Problem05_label30.yml 1 110   3900 1200
eca-rers2012/Problem05_label32.yml 1 130   4900 1400
eca-rers2012/Problem05_label33.yml 1 200   5000 2300
eca-rers2012/Problem05_label36.yml 1 130   4500 1200
eca-rers2012/Problem05_label37.yml 1 130   4800 1300
eca-rers2012/Problem05_label38.yml 1 300   5900 3600
eca-rers2012/Problem05_label39.yml 1 180   5100 1800
eca-rers2012/Problem05_label40.yml 1 140   4900 1400
eca-rers2012/Problem05_label41.yml 1 260   5200 2500
eca-rers2012/Problem05_label44.yml 1 240   5300 2600
eca-rers2012/Problem05_label47.yml 1 120   4200 1300
eca-rers2012/Problem05_label48.yml 1 200   5000 2200
eca-rers2012/Problem05_label51.yml 1 130   4800 1400
eca-rers2012/Problem05_label55.yml 1 150   4900 1400
eca-rers2012/Problem05_label57.yml 1 130   4800 1400
eca-rers2012/Problem05_label58.yml 1 180   5000 1800
eca-rers2012/Problem06_label00.yml 1 99   3900 960
eca-rers2012/Problem06_label01.yml 1 98   3600 930
eca-rers2012/Problem06_label02.yml 1 180   4700 2000
eca-rers2012/Problem06_label04.yml 1 120   4000 1000
eca-rers2012/Problem06_label05.yml 1 94   3500 890
eca-rers2012/Problem06_label09.yml 1 110   4000 920
eca-rers2012/Problem06_label10.yml 1 90   3700 880
eca-rers2012/Problem06_label11.yml 1 95   3800 920
eca-rers2012/Problem06_label12.yml 1 90   3500 830
eca-rers2012/Problem06_label15.yml 1 95   3900 830
eca-rers2012/Problem06_label20.yml 1 120   4200 1100
eca-rers2012/Problem06_label21.yml 1 120   4200 1100
eca-rers2012/Problem06_label24.yml 1 120   4500 1100
eca-rers2012/Problem06_label27.yml 1 99   4000 970
eca-rers2012/Problem06_label29.yml 1 110   4000 1100
eca-rers2012/Problem06_label33.yml 1 110   3900 1100
eca-rers2012/Problem06_label36.yml 1 110   3900 1100
eca-rers2012/Problem06_label37.yml 1 130   4100 1300
eca-rers2012/Problem06_label38.yml 1 110   3900 990
eca-rers2012/Problem06_label44.yml 1 100   3800 1100
eca-rers2012/Problem06_label47.yml 1 83   3400 760
eca-rers2012/Problem06_label48.yml 1 100   3700 910
eca-rers2012/Problem06_label56.yml 1 120   4100 1000
eca-rers2012/Problem06_label58.yml 1 110   3800 1100
eca-rers2012/Problem06_label59.yml 1 110   4100 1000
eca-rers2012/Problem07_label03.yml 900   8300 9700
eca-rers2012/Problem07_label05.yml 900   7500 8100
eca-rers2012/Problem07_label06.yml 900   12000 7600
eca-rers2012/Problem07_label07.yml 900   8500 8500
eca-rers2012/Problem07_label09.yml 900   12000 6100
eca-rers2012/Problem07_label11.yml 900   12000 6300
eca-rers2012/Problem07_label15.yml 900   11000 7800
eca-rers2012/Problem07_label18.yml 900   10000 7500
eca-rers2012/Problem07_label19.yml 900   9300 8000
eca-rers2012/Problem07_label20.yml 900   11000 8100
eca-rers2012/Problem07_label23.yml 900   8400 7600
eca-rers2012/Problem07_label30.yml 900   8400 8800
eca-rers2012/Problem07_label31.yml 900   11000 7100
eca-rers2012/Problem07_label35.yml 900   8500 10000
eca-rers2012/Problem07_label36.yml 900   9100 7400
eca-rers2012/Problem07_label37.yml 900   8300 8000
eca-rers2012/Problem07_label39.yml 900   7300 7400
eca-rers2012/Problem07_label40.yml 900   11000 8700
eca-rers2012/Problem07_label42.yml 900   11000 8700
eca-rers2012/Problem07_label44.yml 900   9200 8200
eca-rers2012/Problem07_label46.yml 900   10000 7300
eca-rers2012/Problem07_label47.yml 900   8100 8100
eca-rers2012/Problem07_label48.yml 910   7300 8800
eca-rers2012/Problem07_label58.yml 900   8600 8500
eca-rers2012/Problem08_label01.yml 910   12000 5700
eca-rers2012/Problem08_label02.yml 900   12000 5300
eca-rers2012/Problem08_label04.yml 910   12000 5000
eca-rers2012/Problem08_label05.yml 900   12000 5300
eca-rers2012/Problem08_label06.yml 910   12000 5000
eca-rers2012/Problem08_label07.yml 910   12000 4500
eca-rers2012/Problem08_label10.yml 910   12000 5400
eca-rers2012/Problem08_label13.yml 910   12000 5900
eca-rers2012/Problem08_label15.yml 900   12000 5400
eca-rers2012/Problem08_label24.yml 910   11000 4700
eca-rers2012/Problem08_label25.yml 910   11000 4700
eca-rers2012/Problem08_label26.yml 910   11000 5200
eca-rers2012/Problem08_label28.yml 910   11000 6000
eca-rers2012/Problem08_label29.yml 910   11000 5700
eca-rers2012/Problem08_label34.yml 910   11000 4800
eca-rers2012/Problem08_label37.yml 910   11000 5300
eca-rers2012/Problem08_label43.yml 910   12000 5400
eca-rers2012/Problem08_label46.yml 910   12000 5000
eca-rers2012/Problem08_label48.yml 910   12000 5500
eca-rers2012/Problem08_label49.yml 910   12000 5200
eca-rers2012/Problem08_label50.yml 910   12000 5100
eca-rers2012/Problem08_label51.yml 910   12000 4800
eca-rers2012/Problem08_label55.yml 910   12000 5800
eca-rers2012/Problem08_label59.yml 910   11000 5900
eca-rers2012/Problem09_label02.yml 910   11000 5100
eca-rers2012/Problem09_label03.yml 910   11000 4700
eca-rers2012/Problem09_label06.yml 900   11000 5100
eca-rers2012/Problem09_label08.yml 930   11000 5400
eca-rers2012/Problem09_label10.yml 910   11000 4900
eca-rers2012/Problem09_label11.yml 910   11000 4800
eca-rers2012/Problem09_label15.yml 900   11000 5000
eca-rers2012/Problem09_label19.yml 900   11000 5100
eca-rers2012/Problem09_label20.yml 900   11000 4500
eca-rers2012/Problem09_label32.yml 910   11000 4800
eca-rers2012/Problem09_label34.yml 910   11000 4800
eca-rers2012/Problem09_label35.yml 910   11000 5000
eca-rers2012/Problem09_label36.yml 910   11000 4300
eca-rers2012/Problem09_label38.yml 910   11000 5000
eca-rers2012/Problem09_label41.yml 910   11000 5100
eca-rers2012/Problem09_label44.yml 900   11000 4600
eca-rers2012/Problem09_label46.yml 910   11000 5200
eca-rers2012/Problem09_label47.yml 910   11000 4900
eca-rers2012/Problem09_label51.yml 910   11000 4500
eca-rers2012/Problem09_label53.yml 910   11000 5000
eca-rers2012/Problem09_label54.yml 910   11000 4700
eca-rers2012/Problem09_label56.yml 910   11000 4800
eca-rers2012/Problem09_label57.yml 910   11000 4400
eca-rers2012/Problem09_label59.yml 910   11000 5300
eca-rers2012/Problem10_label12.yml 1 13   630 120
eca-rers2012/Problem10_label15.yml 1 12   490 110
eca-rers2012/Problem10_label24.yml 1 13   600 110
eca-rers2012/Problem10_label26.yml 1 13   550 110
eca-rers2012/Problem10_label28.yml 1 13   430 110
eca-rers2012/Problem10_label29.yml 1 13   450 110
eca-rers2012/Problem10_label41.yml 1 12   530 98
eca-rers2012/Problem10_label42.yml 1 9.4 330 74
eca-rers2012/Problem10_label46.yml 1 6.8 300 67
eca-rers2012/Problem10_label47.yml 1 12   430 100
eca-rers2012/Problem10_label48.yml 1 12   450 94
eca-rers2012/Problem10_label50.yml 1 14   560 110
eca-rers2012/Problem10_label55.yml 1 12   400 99
eca-rers2012/Problem10_label57.yml 1 13   510 110
eca-rers2012/Problem10_label58.yml 1 13   580 130
eca-rers2012/Problem11_label00.yml 1 15   570 120
eca-rers2012/Problem11_label08.yml 1 13   490 110
eca-rers2012/Problem11_label14.yml 1 13   520 110
eca-rers2012/Problem11_label15.yml 1 12   490 92
eca-rers2012/Problem11_label20.yml 1 15   640 130
eca-rers2012/Problem11_label29.yml 1 14   540 100
eca-rers2012/Problem11_label31.yml 1 15   680 130
eca-rers2012/Problem11_label34.yml 1 15   590 120
eca-rers2012/Problem11_label36.yml 1 11   490 87
eca-rers2012/Problem11_label39.yml 1 15   550 120
eca-rers2012/Problem11_label42.yml 1 13   460 110
eca-rers2012/Problem11_label43.yml 1 12   390 100
eca-rers2012/Problem11_label49.yml 1 12   400 96
eca-rers2012/Problem11_label51.yml 1 14   520 130
eca-rers2012/Problem11_label58.yml 1 12   500 110
eca-rers2012/Problem12_label00.yml 900   8400 7000
eca-rers2012/Problem12_label03.yml 900   8700 7100
eca-rers2012/Problem12_label06.yml 900   8300 5800
eca-rers2012/Problem12_label07.yml 1 140   5000 1100
eca-rers2012/Problem12_label08.yml 1 200   4800 1400
eca-rers2012/Problem12_label10.yml 1 370   7400 3900
eca-rers2012/Problem12_label13.yml 900   8400 6100
eca-rers2012/Problem12_label19.yml 900   8200 6800
eca-rers2012/Problem12_label20.yml 1 870   8400 6100
eca-rers2012/Problem12_label21.yml 900   8700 6900
eca-rers2012/Problem12_label25.yml 900   8500 5500
eca-rers2012/Problem12_label28.yml 1 890   11000 6500
eca-rers2012/Problem12_label30.yml 1 140   4800 1300
eca-rers2012/Problem12_label34.yml 900   11000 7500
eca-rers2012/Problem12_label35.yml 1 120   4200 960
eca-rers2012/Problem12_label37.yml 900   8400 6500
eca-rers2012/Problem12_label38.yml 1 140   6200 1300
eca-rers2012/Problem12_label39.yml 900   4900 5100
eca-rers2012/Problem12_label40.yml 1 19   950 180
eca-rers2012/Problem12_label42.yml 1 130   4800 1300
eca-rers2012/Problem12_label48.yml 1 120   4200 1100
eca-rers2012/Problem12_label50.yml 900   8700 7500
eca-rers2012/Problem12_label51.yml 900   8400 6100
eca-rers2012/Problem12_label52.yml 900   8300 5700
eca-rers2012/Problem12_label55.yml 900   5100 8200
eca-rers2012/Problem13_label04.yml 1 200   6700 2100
eca-rers2012/Problem13_label06.yml 1 430   6500 2700
eca-rers2012/Problem13_label07.yml 1 410   10000 3300
eca-rers2012/Problem13_label11.yml 900   11000 6100
eca-rers2012/Problem13_label12.yml 1 280   9600 2600
eca-rers2012/Problem13_label16.yml 900   11000 6500
eca-rers2012/Problem13_label19.yml 900   11000 7600
eca-rers2012/Problem13_label21.yml 1 310   9900 2700
eca-rers2012/Problem13_label23.yml 900   7000 6200
eca-rers2012/Problem13_label24.yml 1 460   6100 2800
eca-rers2012/Problem13_label25.yml 900   7900 8200
eca-rers2012/Problem13_label28.yml 1 24   990 200
eca-rers2012/Problem13_label29.yml 1 740   6800 5000
eca-rers2012/Problem13_label30.yml 900   11000 7200
eca-rers2012/Problem13_label32.yml 900   7800 6400
eca-rers2012/Problem13_label35.yml 1 140   6200 1200
eca-rers2012/Problem13_label36.yml 1 180   6800 1800
eca-rers2012/Problem13_label40.yml 1 26   1300 250
eca-rers2012/Problem13_label43.yml 900   9500 6300
eca-rers2012/Problem13_label44.yml 1 220   6100 1900
eca-rers2012/Problem13_label45.yml 1 23   990 210
eca-rers2012/Problem13_label48.yml 1 160   7000 1400
eca-rers2012/Problem13_label51.yml 900   11000 6300
eca-rers2012/Problem13_label54.yml 900   11000 7000
eca-rers2012/Problem13_label58.yml 900   11000 6800
eca-rers2012/Problem15_label00.yml 1 16   520 120
eca-rers2012/Problem15_label02.yml 1 17   580 140
eca-rers2012/Problem15_label03.yml 1 18   660 140
eca-rers2012/Problem15_label07.yml 1 21   900 200
eca-rers2012/Problem15_label09.yml 1 19   720 150
eca-rers2012/Problem15_label14.yml 1 18   660 160
eca-rers2012/Problem15_label15.yml 1 17   690 140
eca-rers2012/Problem15_label22.yml 1 18   630 150
eca-rers2012/Problem15_label23.yml 1 18   810 170
eca-rers2012/Problem15_label25.yml 1 21   1000 200
eca-rers2012/Problem15_label29.yml 1 18   700 160
eca-rers2012/Problem15_label30.yml 1 16   600 130
eca-rers2012/Problem15_label33.yml 1 17   640 150
eca-rers2012/Problem15_label34.yml 1 19   670 160
eca-rers2012/Problem15_label37.yml 1 21   930 170
eca-rers2012/Problem15_label38.yml 1 20   930 180
eca-rers2012/Problem15_label39.yml 1 20   940 180
eca-rers2012/Problem15_label40.yml 1 18   660 170
eca-rers2012/Problem15_label41.yml 1 17   710 150
eca-rers2012/Problem15_label45.yml 1 18   690 160
eca-rers2012/Problem15_label47.yml 1 17   690 140
eca-rers2012/Problem15_label48.yml 1 17   700 150
eca-rers2012/Problem15_label50.yml 1 18   770 170
eca-rers2012/Problem15_label51.yml 1 18   640 150
eca-rers2012/Problem16_label00.yml 900   6100 7300
eca-rers2012/Problem16_label01.yml 900   8100 6900
eca-rers2012/Problem16_label03.yml 900   8000 7400
eca-rers2012/Problem16_label04.yml 900   8000 8500
eca-rers2012/Problem16_label05.yml 900   9900 7600
eca-rers2012/Problem16_label06.yml 900   10000 7100
eca-rers2012/Problem16_label08.yml 900   9700 6500
eca-rers2012/Problem16_label14.yml 900   9400 8000
eca-rers2012/Problem16_label15.yml 900   8100 6800
eca-rers2012/Problem16_label18.yml 900   12000 7600
eca-rers2012/Problem16_label20.yml 900   11000 7000
eca-rers2012/Problem16_label22.yml 900   11000 6800
eca-rers2012/Problem16_label27.yml 900   8400 7600
eca-rers2012/Problem16_label30.yml 900   11000 7400
eca-rers2012/Problem16_label31.yml 900   8400 7400
eca-rers2012/Problem16_label33.yml 900   8400 9100
eca-rers2012/Problem16_label37.yml 900   11000 6800
eca-rers2012/Problem16_label38.yml 900   8800 8000
eca-rers2012/Problem16_label41.yml 900   8600 7700
eca-rers2012/Problem16_label43.yml 900   8000 7400
eca-rers2012/Problem16_label44.yml 900   9700 6700
eca-rers2012/Problem16_label46.yml 900   9900 7800
eca-rers2012/Problem16_label51.yml 900   11000 7300
eca-rers2012/Problem16_label52.yml 900   10000 7200
eca-rers2012/Problem16_label54.yml 900   8300 6600
eca-rers2012/Problem17_label04.yml 1 18   550 170
eca-rers2012/Problem17_label07.yml 900   8000 6300
eca-rers2012/Problem17_label09.yml 1 18   600 140
eca-rers2012/Problem17_label13.yml 1 21   870 180
eca-rers2012/Problem17_label16.yml 1 20   760 180
eca-rers2012/Problem17_label20.yml 910   4600 6800
eca-rers2012/Problem17_label23.yml 1 18   730 140
eca-rers2012/Problem17_label25.yml 1 23   990 230
eca-rers2012/Problem17_label26.yml 1 21   870 180
eca-rers2012/Problem17_label30.yml 1 16   560 130
eca-rers2012/Problem17_label31.yml 900   4400 4400
eca-rers2012/Problem17_label33.yml 1 22   1000 180
eca-rers2012/Problem17_label34.yml 1 18   710 160
eca-rers2012/Problem17_label35.yml 900   4700 5900
eca-rers2012/Problem17_label37.yml 1 21   950 170
eca-rers2012/Problem17_label40.yml 1 21   950 190
eca-rers2012/Problem17_label46.yml 900   4700 7900
eca-rers2012/Problem17_label49.yml 1 20   770 160
eca-rers2012/Problem17_label50.yml 1 840   4900 5600
eca-rers2012/Problem17_label52.yml 900   4700 6500
eca-rers2012/Problem17_label53.yml 1 16   540 130
eca-rers2012/Problem17_label54.yml 1 20   880 170
eca-rers2012/Problem17_label55.yml 1 19   770 160
eca-rers2012/Problem17_label57.yml 1 25   1200 220
eca-rers2012/Problem18_label00.yml 1 320   4500 3000
eca-rers2012/Problem18_label01.yml 1 300   3700 2100
eca-rers2012/Problem18_label03.yml 1 280   3700 2300
eca-rers2012/Problem18_label06.yml 1 270   5200 2700
eca-rers2012/Problem18_label08.yml 1 130   3500 1000
eca-rers2012/Problem18_label09.yml 1 240   6000 2000
eca-rers2012/Problem18_label10.yml 1 550   4700 3800
eca-rers2012/Problem18_label12.yml 1 150   2900 1100
eca-rers2012/Problem18_label19.yml 1 160   3700 1500
eca-rers2012/Problem18_label20.yml 900   9900 7300
eca-rers2012/Problem18_label25.yml 900   7200 7300
eca-rers2012/Problem18_label27.yml 1 250   3600 1500
eca-rers2012/Problem18_label31.yml 1 250   7000 2100
eca-rers2012/Problem18_label32.yml 900   4300 5400
eca-rers2012/Problem18_label33.yml 900   6400 6700
eca-rers2012/Problem18_label34.yml 1 550   5800 3900
eca-rers2012/Problem18_label35.yml 1 480   4100 3800
eca-rers2012/Problem18_label36.yml 1 300   4700 2300
eca-rers2012/Problem18_label38.yml 1 140   2900 1100
eca-rers2012/Problem18_label39.yml 1 170   3400 1300
eca-rers2012/Problem18_label45.yml 1 250   4100 2200
eca-rers2012/Problem18_label49.yml 900   6200 7300
eca-rers2012/Problem18_label52.yml 1 120   4600 1100
eca-rers2012/Problem18_label55.yml 1 130   5100 1200
eca-rers2012/Problem18_label57.yml 1 300   7000 2200
eca-rers2012/Problem19_label10.yml 900   9200 7500
eca-rers2012/Problem19_label11.yml 900   8500 5600
eca-rers2012/Problem19_label14.yml 900   11000 6100
eca-rers2012/Problem19_label17.yml 900   14000 9700
eca-rers2012/Problem19_label18.yml 900   9600 7200
eca-rers2012/Problem19_label19.yml 530   15000 5000
eca-rers2012/Problem19_label21.yml 900   8500 6600
eca-rers2012/Problem19_label22.yml 900   8400 8000
eca-rers2012/Problem19_label26.yml 900   8200 5900
eca-rers2012/Problem19_label27.yml 900   8400 5100
eca-rers2012/Problem19_label28.yml 900   8400 7500
eca-rers2012/Problem19_label29.yml 530   15000 4100
eca-rers2012/Problem19_label31.yml 900   9300 6400
eca-rers2012/Problem19_label32.yml 910   7900 5800
eca-rers2012/Problem19_label41.yml 900   14000 7900
eca-rers2012/Problem19_label42.yml 900   9600 5800
eca-rers2012/Problem19_label43.yml 900   9300 5900
eca-rers2012/Problem19_label47.yml 900   8400 5000
eca-rers2012/Problem19_label50.yml 900   11000 6200
eca-rers2012/Problem19_label51.yml 910   9400 6900
eca-rers2012/Problem19_label53.yml 900   8400 5500
eca-rers2012/Problem19_label55.yml 900   11000 6800
eca-rers2012/Problem19_label58.yml 900   10000 6200
eca-rers2012/Problem19_label59.yml 900   8400 6300
eca-programs/Problem101_label00.yml 900   8300 7100
eca-programs/Problem101_label01.yml 900   8100 7100
eca-programs/Problem101_label02.yml 900   12000 6300
eca-programs/Problem101_label03.yml 900   10000 7200
eca-programs/Problem101_label04.yml 900   10000 6900
eca-programs/Problem101_label05.yml 900   9800 7000
eca-programs/Problem101_label06.yml 900   8900 7000
eca-programs/Problem101_label07.yml 900   11000 8300
eca-programs/Problem101_label08.yml 900   8400 8100
eca-programs/Problem101_label09.yml 900   8100 8100
eca-programs/Problem101_label10.yml 900   11000 8600
eca-programs/Problem101_label11.yml 900   10000 7800
eca-programs/Problem101_label12.yml 900   8900 8700
eca-programs/Problem101_label13.yml 900   11000 6800
eca-programs/Problem101_label14.yml 900   11000 7500
eca-programs/Problem101_label15.yml 900   12000 7100
eca-programs/Problem101_label16.yml 910   8600 7300
eca-programs/Problem101_label17.yml 900   9800 8700
eca-programs/Problem101_label18.yml 900   11000 8000
eca-programs/Problem101_label19.yml 900   8500 8100
eca-programs/Problem101_label20.yml 900   9600 7100
eca-programs/Problem101_label21.yml 900   8300 7200
eca-programs/Problem101_label22.yml 900   8400 8900
eca-programs/Problem101_label23.yml 900   9700 6900
eca-programs/Problem102_label01.yml 910   12000 5600
eca-programs/Problem102_label02.yml 910   12000 5400
eca-programs/Problem102_label04.yml 910   12000 6400
eca-programs/Problem102_label05.yml 900   12000 5300
eca-programs/Problem102_label06.yml 910   12000 5100
eca-programs/Problem102_label07.yml 900   12000 5300
eca-programs/Problem102_label10.yml 910   12000 5200
eca-programs/Problem102_label13.yml 910   12000 5000
eca-programs/Problem102_label15.yml 910   12000 5200
eca-programs/Problem102_label24.yml 900   11000 5200
eca-programs/Problem102_label25.yml 910   11000 4600
eca-programs/Problem102_label26.yml 910   11000 4900
eca-programs/Problem102_label28.yml 910   11000 5300
eca-programs/Problem102_label29.yml 910   11000 6100
eca-programs/Problem102_label34.yml 910   11000 5200
eca-programs/Problem102_label37.yml 900   11000 5000
eca-programs/Problem102_label43.yml 910   12000 5900
eca-programs/Problem102_label46.yml 910   12000 6200
eca-programs/Problem102_label48.yml 900   12000 5500
eca-programs/Problem102_label49.yml 910   12000 6000
eca-programs/Problem102_label50.yml 910   12000 5500
eca-programs/Problem102_label51.yml 910   12000 5200
eca-programs/Problem102_label55.yml 910   12000 5700
eca-programs/Problem102_label59.yml 910   11000 4500
eca-programs/Problem103_label32.yml 900   11000 5100
eca-programs/Problem103_label35.yml 910   11000 4800
eca-programs/Problem103_label41.yml 900   11000 4600
eca-programs/Problem103_label44.yml 910   11000 4900
eca-programs/Problem103_label46.yml 910   11000 5000
eca-programs/Problem103_label47.yml 900   11000 4600
eca-programs/Problem103_label51.yml 910   11000 4800
eca-programs/Problem103_label53.yml 900   11000 4600
eca-programs/Problem103_label54.yml 900   11000 4500
eca-programs/Problem103_label56.yml 900   11000 4700
eca-programs/Problem103_label57.yml 910   11000 4400
eca-programs/Problem103_label59.yml 910   11000 4800
floats-cdfpl/newton_1_4.yml 1 94   380 610
floats-cdfpl/newton_1_5.yml 1 77   370 540
floats-cdfpl/newton_1_6.yml 1 64   370 630
floats-cdfpl/newton_1_7.yml 1 41   370 330
floats-cdfpl/newton_1_8.yml 1 36   380 290
floats-cdfpl/newton_2_6.yml 1 160   480 1100
floats-cdfpl/newton_2_7.yml 1 100   480 760
floats-cdfpl/newton_2_8.yml 1 62   470 600
floats-cdfpl/newton_3_6.yml 1 310   600 2300
floats-cdfpl/newton_3_7.yml 1 220   600 1900
floats-cdfpl/newton_3_8.yml 1 190   600 1300
floats-cdfpl/sine_1.yml 1 29   340 290
floats-cdfpl/sine_2.yml 1 66   350 590
floats-cdfpl/sine_3.yml 1 300   450 2800
floats-cdfpl/square_1.yml 1 37   1500 400
floats-cdfpl/square_2.yml 1 200   1600 2100
floats-cdfpl/square_3.yml 1 82   1500 750
float-benchs/cast_float_ptr.yml 3.4 270 33
float-benchs/cast_union_loose.yml 3.7 280 40
float-benchs/cast_union_tight.yml 3.8 270 40
float-benchs/float_int_inv_square.yml 1 3.6 280 35
float-benchs/inv_Newton-2.yml 6.1 350 63
float-benchs/inv_Newton.c.p+cfa-reducer.yml 1 6.8 350 74
float-benchs/inv_square-1.yml 1 3.4 270 34
float-benchs/nan_double.yml 3.4 270 31
float-benchs/nan_float.yml 3.2 260 31
float-benchs/sin_interpolated_index-1.yml 1 25   570 220
float-benchs/sqrt_poly2.yml 1 15   440 120
float-newlib/double_req_bl_0870a.yml 6.9 460 63
float-newlib/float_req_bl_0870a.yml 1 350   2700 3200
loop-floats-scientific-comp/loop1-2.yml 1 4.2 300 40
loop-floats-scientific-comp/loop2-1.yml 1 4.6 300 51
ldv-regression/fo_test.yml 1 4.4 280 38
ldv-regression/rule60_list2.c_1.yml 1 4.8 280 41
ldv-regression/test21-2.yml 1 3.4 270 31
ldv-regression/test22-2.yml 1 23   1200 270
ldv-regression/test23-1.yml 1 31   1500 370
ldv-regression/test24-2.yml 1 5.2 290 51
ldv-regression/test25-1.yml 1 32   1800 370
ldv-regression/test28-1.yml 1 3.5 270 27
ldv-regression/test29-1.yml 1 23   720 200
loops/array-2.yml 1 23   1600 280
loops/compact.yml 900   2900 6200
loops/count_up_down-2.yml 1 3.3 260 30
loops/eureka_01-1.yml 900   5100 13000
loops/for_bounded_loop1.yml 1 3.9 270 40
loops/insertion_sort-1.yml 1 320   3900 4000
loops/invert_string-1.yml 900   5300 13000
loops/linear_search.yml 900   1500 11000
loops/matrix-2.yml 1 25   880 200
loops/nec20.yml 1 3.6 270 35
loops/string-2.yml 1 4.6 280 44
loops/sum01-1.yml 1 24   850 190
loops/sum01_bug02.yml 1 24   860 190
loops/sum01_bug02_sum01_bug02_base.case.yml 1 9.3 450 83
loops/sum03-1.yml 1 4.9 280 40
loops/sum_array-1.yml 1 23   820 220
loops/terminator_01.yml 1 3.4 260 29
loops/terminator_02-1.yml 1 3.4 260 31
loops/terminator_03-1.yml 1 23   1400 300
loops/trex01-1.yml 1 3.5 260 36
loops/trex02-2.yml 1 3.4 260 36
loops/trex03-1.yml 1 22   1500 240
loops/vogal-2.yml 1 72   900 700
loop-acceleration/array_3-2.yml 900   5700 12000
loop-acceleration/diamond_1-2.yml 1 10   500 90
loop-acceleration/multivar_1-2.yml 1 3.4 260 34
loop-invgen/id_trans.yml 1 3.8 270 40
recursive/Ackermann02.yml 100   15000 930
recursive/Addition02.yml 100   15000 970
recursive/BallRajamani-SPIN2000-Fig1.yml 120   15000 1100
recursive/EvenOdd03.yml 1 3.5 260 33
recursive/Fibonacci04.yml 200   15000 2200
recursive/Fibonacci05.yml 210   15000 2000
recursive/McCarthy91-1.yml 1 3.6 270 32
recursive-simple/id2_b3_o2.yml 34   15000 320
recursive-simple/id_b3_o2-2.yml 35   15000 350
recursive-simple/id_o10.yml 34   15000 360
recursive-simple/id_o100.yml 35   15000 370
recursive-simple/id_o1000.yml 35   15000 350
recursive-simple/id_o20.yml 34   15000 400
recursive-simple/id_o200.yml 34   15000 340
recursive-simple/id_o3.yml 34   15000 320
recursive-simple/sum_non_eq-3.yml 1 3.7 270 28
seq-mthreaded/pals_STARTPALS_ActiveStandby.1.ufo.BOUNDED-10.pals.yml 1 29   1100 220
seq-mthreaded/pals_STARTPALS_ActiveStandby.1.ufo.UNBOUNDED.pals.yml 1 25   870 190
seq-mthreaded/pals_STARTPALS_ActiveStandby.4_1.ufo.BOUNDED-10.pals.yml 1 26   870 230
seq-mthreaded/pals_STARTPALS_ActiveStandby.4_1.ufo.UNBOUNDED.pals.yml 1 25   890 200
seq-mthreaded/pals_STARTPALS_ActiveStandby.4_2.ufo.BOUNDED-10.pals.yml 1 26   890 210
seq-mthreaded/pals_STARTPALS_ActiveStandby.4_2.ufo.UNBOUNDED.pals.yml 1 31   1100 230
seq-mthreaded/pals_STARTPALS_ActiveStandby.5.ufo.BOUNDED-10.pals.yml 1 130   2200 1500
seq-mthreaded/pals_STARTPALS_ActiveStandby.5.ufo.UNBOUNDED.pals.yml 1 42   1100 410
seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.BOUNDED-10.pals.yml 1 39   1200 340
seq-mthreaded/pals_STARTPALS_Triplicated.1.ufo.UNBOUNDED.pals.yml 1 39   1300 350
seq-mthreaded/pals_STARTPALS_Triplicated.2.ufo.BOUNDED-10.pals.yml 1 43   1400 370
seq-mthreaded/pals_STARTPALS_Triplicated.2.ufo.UNBOUNDED.pals.yml 1 40   1400 420
seq-mthreaded/pals_floodmax.3.1.ufo.BOUNDED-6.pals.yml 1 27   1000 300
seq-mthreaded/pals_floodmax.3.1.ufo.UNBOUNDED.pals.yml 1 26   1000 290
seq-mthreaded/pals_floodmax.3.2.ufo.BOUNDED-6.pals.yml 1 25   810 240
seq-mthreaded/pals_floodmax.3.2.ufo.UNBOUNDED.pals.yml 1 26   790 230
seq-mthreaded/pals_floodmax.3.3.ufo.BOUNDED-6.pals.yml 1 27   1100 270
seq-mthreaded/pals_floodmax.3.3.ufo.UNBOUNDED.pals.yml 1 27   1300 250
seq-mthreaded/pals_floodmax.3.4.ufo.BOUNDED-6.pals.yml 1 28   920 300
seq-mthreaded/pals_floodmax.3.4.ufo.UNBOUNDED.pals.yml 1 26   1100 290
seq-mthreaded/pals_floodmax.3_overflow.ufo.UNBOUNDED.pals.yml 900   1500 8800
seq-mthreaded/pals_floodmax.4.1.ufo.BOUNDED-8.pals.yml 1 62   890 550
seq-mthreaded/pals_floodmax.4.1.ufo.UNBOUNDED.pals.yml 1 32   900 380
seq-mthreaded/pals_floodmax.4.2.ufo.BOUNDED-8.pals.yml 1 30   840 340
seq-mthreaded/pals_floodmax.4.2.ufo.UNBOUNDED.pals.yml 1 30   910 330
seq-mthreaded/pals_floodmax.4.3.ufo.BOUNDED-8.pals.yml 1 36   860 360
seq-mthreaded/pals_floodmax.4.3.ufo.UNBOUNDED.pals.yml 1 42   940 450
seq-mthreaded/pals_floodmax.4.4.ufo.BOUNDED-8.pals.yml 1 58   780 500
seq-mthreaded/pals_floodmax.4.4.ufo.UNBOUNDED.pals.yml 1 85   850 700
seq-mthreaded/pals_floodmax.4_overflow.ufo.UNBOUNDED.pals.yml 900   1600 8700
seq-mthreaded/pals_floodmax.5.1.ufo.BOUNDED-10.pals.yml 1 160   1300 1100
seq-mthreaded/pals_floodmax.5.1.ufo.UNBOUNDED.pals.yml 1 190   1200 1500
seq-mthreaded/pals_floodmax.5.2.ufo.BOUNDED-10.pals.yml 1 41   880 440
seq-mthreaded/pals_floodmax.5.2.ufo.UNBOUNDED.pals.yml 1 39   1100 400
seq-mthreaded/pals_floodmax.5.3.ufo.BOUNDED-10.pals.yml 1 70   1100 620
seq-mthreaded/pals_floodmax.5.3.ufo.UNBOUNDED.pals.yml 1 160   1200 1200
seq-mthreaded/pals_floodmax.5.4.ufo.BOUNDED-10.pals.yml 900   1500 5300
seq-mthreaded/pals_floodmax.5.4.ufo.UNBOUNDED.pals.yml 900   1500 5700
seq-mthreaded/pals_floodmax.5_overflow.ufo.UNBOUNDED.pals.yml 900   1700 5800
seq-mthreaded/pals_lcr-var-start-time.3.1.ufo.BOUNDED-6.pals.yml 1 35   1100 330
seq-mthreaded/pals_lcr-var-start-time.3.1.ufo.UNBOUNDED.pals.yml 1 30   850 250
seq-mthreaded/pals_lcr-var-start-time.3.2.ufo.BOUNDED-6.pals.yml 900   2000 14000
seq-mthreaded/pals_lcr-var-start-time.3.2.ufo.UNBOUNDED.pals.yml 1 41   1100 420
seq-mthreaded/pals_lcr-var-start-time.4.1.ufo.BOUNDED-8.pals.yml 900   4800 11000
seq-mthreaded/pals_lcr-var-start-time.4.1.ufo.UNBOUNDED.pals.yml 900   2000 11000
seq-mthreaded/pals_lcr-var-start-time.4.2.ufo.BOUNDED-8.pals.yml 900   2100 9800
seq-mthreaded/pals_lcr-var-start-time.4.2.ufo.UNBOUNDED.pals.yml 900   2000 12000
seq-mthreaded/pals_lcr-var-start-time.5.1.ufo.BOUNDED-10.pals.yml 900   4900 11000
seq-mthreaded/pals_lcr-var-start-time.5.1.ufo.UNBOUNDED.pals.yml 900   3200 14000
seq-mthreaded/pals_lcr-var-start-time.5.2.ufo.BOUNDED-10.pals.yml 900   4500 12000
seq-mthreaded/pals_lcr-var-start-time.5.2.ufo.UNBOUNDED.pals.yml 900   1600 14000
seq-mthreaded/pals_lcr-var-start-time.6.1.ufo.BOUNDED-12.pals.yml 900   1300 14000
seq-mthreaded/pals_lcr-var-start-time.6.1.ufo.UNBOUNDED.pals.yml 900   1200 12000
seq-mthreaded/pals_lcr-var-start-time.6.2.ufo.BOUNDED-12.pals.yml 900   2900 11000
seq-mthreaded/pals_lcr-var-start-time.6.2.ufo.UNBOUNDED.pals.yml 900   1400 12000
seq-mthreaded/pals_lcr.3.1.ufo.BOUNDED-6.pals.yml 1 26   850 230
seq-mthreaded/pals_lcr.3.1.ufo.UNBOUNDED.pals.yml 1 230   4000 2800
seq-mthreaded/pals_lcr.3_overflow.ufo.UNBOUNDED.pals.yml 900   1800 12000
seq-mthreaded/pals_lcr.4.1.ufo.BOUNDED-8.pals.yml 900   1800 9300
seq-mthreaded/pals_lcr.4.1.ufo.UNBOUNDED.pals.yml 900   2000 12000
seq-mthreaded/pals_lcr.4_overflow.ufo.UNBOUNDED.pals.yml 900   2900 6600
seq-mthreaded/pals_lcr.5.1.ufo.BOUNDED-10.pals.yml 900   3600 11000
seq-mthreaded/pals_lcr.5.1.ufo.UNBOUNDED.pals.yml 900   3900 10000
seq-mthreaded/pals_lcr.5_overflow.ufo.UNBOUNDED.pals.yml 900   4400 8500
seq-mthreaded/pals_lcr.6.1.ufo.BOUNDED-12.pals.yml 900   2500 11000
seq-mthreaded/pals_lcr.6.1.ufo.UNBOUNDED.pals.yml 900   1800 10000
seq-mthreaded/pals_lcr.6_overflow.ufo.UNBOUNDED.pals.yml 900   2400 10000
seq-mthreaded/pals_lcr.7.1.ufo.BOUNDED-14.pals.yml 900   1100 11000
seq-mthreaded/pals_lcr.7.1.ufo.UNBOUNDED.pals.yml 900   1200 13000
seq-mthreaded/pals_lcr.7_overflow.ufo.UNBOUNDED.pals.yml 900   1800 12000
seq-mthreaded/pals_lcr.8.1.ufo.BOUNDED-16.pals.yml 900   1300 11000
seq-mthreaded/pals_lcr.8.1.ufo.UNBOUNDED.pals.yml 900   1100 11000
seq-mthreaded/pals_lcr.8_overflow.ufo.UNBOUNDED.pals.yml 900   1100 14000
seq-mthreaded/pals_opt-floodmax.3.1.ufo.BOUNDED-6.pals.yml 1 26   890 270
seq-mthreaded/pals_opt-floodmax.3.1.ufo.UNBOUNDED.pals.yml 1 27   1000 280
seq-mthreaded/pals_opt-floodmax.3.2.ufo.BOUNDED-6.pals.yml 1 25   890 260
seq-mthreaded/pals_opt-floodmax.3.2.ufo.UNBOUNDED.pals.yml 1 26   1300 260
seq-mthreaded/pals_opt-floodmax.3.3.ufo.BOUNDED-6.pals.yml 1 27   1200 280
seq-mthreaded/pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.yml 1 27   1100 290
seq-mthreaded/pals_opt-floodmax.3.4.ufo.BOUNDED-6.pals.yml 1 29   1000 290
seq-mthreaded/pals_opt-floodmax.3.4.ufo.UNBOUNDED.pals.yml 1 28   990 300
seq-mthreaded/pals_opt-floodmax.3_overflow.ufo.UNBOUNDED.pals.yml 900   2000 9200
seq-mthreaded/pals_opt-floodmax.4.1.ufo.BOUNDED-8.pals.yml 1 33   810 350
seq-mthreaded/pals_opt-floodmax.4.1.ufo.UNBOUNDED.pals.yml 1 44   810 480
seq-mthreaded/pals_opt-floodmax.4.2.ufo.BOUNDED-8.pals.yml 1 30   740 320
seq-mthreaded/pals_opt-floodmax.4.2.ufo.UNBOUNDED.pals.yml 1 32   870 330
seq-mthreaded/pals_opt-floodmax.4.3.ufo.BOUNDED-8.pals.yml 1 40   970 440
seq-mthreaded/pals_opt-floodmax.4.3.ufo.UNBOUNDED.pals.yml 1 32   950 370
seq-mthreaded/pals_opt-floodmax.4.4.ufo.BOUNDED-8.pals.yml 1 99   970 730
seq-mthreaded/pals_opt-floodmax.4.4.ufo.UNBOUNDED.pals.yml 1 150   1100 1500
seq-mthreaded/pals_opt-floodmax.4_overflow.ufo.UNBOUNDED.pals.yml 900   1600 7100
seq-mthreaded/pals_opt-floodmax.5.1.ufo.BOUNDED-10.pals.yml 1 620   1600 4600
seq-mthreaded/pals_opt-floodmax.5.1.ufo.UNBOUNDED.pals.yml 1 380   1600 3200
seq-mthreaded/pals_opt-floodmax.5.2.ufo.BOUNDED-10.pals.yml 1 82   1100 670
seq-mthreaded/pals_opt-floodmax.5.2.ufo.UNBOUNDED.pals.yml 1 110   1100 930
seq-mthreaded/pals_opt-floodmax.5.3.ufo.BOUNDED-10.pals.yml 1 71   1400 630
seq-mthreaded/pals_opt-floodmax.5.3.ufo.UNBOUNDED.pals.yml 1 260   1500 2000
seq-mthreaded/pals_opt-floodmax.5.4.ufo.BOUNDED-10.pals.yml 900   1800 5800
seq-mthreaded/pals_opt-floodmax.5.4.ufo.UNBOUNDED.pals.yml 900   1500 5800
seq-mthreaded/pals_opt-floodmax.5_overflow.ufo.UNBOUNDED.pals.yml 900   1400 6000
../sv-benchmarks/c/ status cov cpu (s) mem (MB) energy (J)
total 636 331 290000 3300000 2300000
Run set [test-comp19_prop-coverage-error-call.ReachSafety-Arrays; test-comp19_prop-coverage-error-call.ReachSafety-BitVectors; test-comp19_prop-coverage-error-call.ReachSafety-ControlFlow; test-comp19_prop-coverage-error-call.ReachSafety-ECA; test-comp19_prop-coverage-error-call.ReachSafety-Floats; test-comp19_prop-coverage-error-call.ReachSafety-Heap; test-comp19_prop-coverage-error-call.ReachSafety-Loops; test-comp19_prop-coverage-error-call.ReachSafety-Recursive; test-comp19_prop-coverage-error-call.ReachSafety-Sequentialized]