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