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-Arrays cpa-tiger.test-comp19_prop-coverage-error-call.ReachSafety-Arrays esbmc-kind.test-comp19_prop-coverage-error-call.ReachSafety-Arrays esbmc-falsi.test-comp19_prop-coverage-error-call.ReachSafety-Arrays fairfuzz.test-comp19_prop-coverage-error-call.ReachSafety-Arrays klee.test-comp19_prop-coverage-error-call.ReachSafety-Arrays prtest.test-comp19_prop-coverage-error-call.ReachSafety-Arrays symbiotic.test-comp19_prop-coverage-error-call.ReachSafety-Arrays verifuzz.test-comp19_prop-coverage-error-call.ReachSafety-Arrays
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)
array-examples/standard_copy1_ground-2.yml timeout 900 2200 11000 timeout 900   7300 11000 timeout 900    11000 11000   timeout 940    8200 14000   timeout 1 900   59 13000 false(unreach-call) 1 1.9  180 28   timeout 900    31 15000   done 1 6.9  420 100 done 1 3.4 150 36
array-examples/standard_copy2_ground-1.yml timeout 900 2400 12000 timeout 900   7200 11000 timeout 900    11000 10000   timeout 900    10000 10000   timeout 1 900   71 11000 false(unreach-call) 1 2.2  190 35   timeout 900    31 13000   done 1 9.3  530 120 done 1 3.4 150 39
array-examples/standard_copy3_ground-2.yml timeout 900 2700 12000 timeout 900   7700 11000 timeout 900    11000 9900   timeout 940    3600 10000   timeout 1 900   72 11000 false(unreach-call) 1 2.6  190 34   timeout 900    31 14000   done 1 10    580 150 done 1 3.7 150 36
array-examples/standard_copy4_ground-2.yml timeout 900 2800 11000 timeout 900   8100 12000 timeout 900    11000 9600   timeout 900    11000 9900   timeout 1 900   79 13000 false(unreach-call) 1 3.1  200 44   timeout 900    31 12000   done 1 11    640 160 done 1 3.6 150 44
array-examples/standard_copy5_ground-2.yml timeout 900 2800 10000 timeout 900   7700 11000 timeout 900    11000 9900   timeout 900    11000 9400   timeout 1 900   63 13000 false(unreach-call) 1 3.5  200 46   timeout 900    30 14000   done 1 13    700 170 done 1 3.6 150 39
array-examples/standard_copy6_ground-1.yml timeout 900 2700 11000 timeout 900   8200 11000 timeout 900    11000 12000   timeout 900    10000 9700   timeout 1 900   74 11000 false(unreach-call) 1 3.9  200 52   timeout 900    31 12000   done 1 13    770 220 done 1 3.6 150 39
array-examples/standard_copy7_ground-1.yml timeout 900 2700 13000 timeout 900   8500 11000 timeout 900    11000 11000   timeout 900    11000 12000   timeout 1 900   62 11000 false(unreach-call) 1 4.4  210 66   timeout 900    31 13000   done 1 15    850 190 done 1 3.7 150 39
array-examples/standard_copy8_ground-2.yml timeout 900 3100 12000 timeout 900   9100 11000 timeout 900    11000 10000   timeout 900    11000 12000   timeout 1 900   65 9900 false(unreach-call) 1 4.8  210 68   timeout 900    31 14000   done 1 16    930 200 done 1 3.4 150 35
array-examples/standard_copy9_ground-1.yml timeout 900 3300 11000 timeout 900   9500 11000 timeout 900    11000 11000   timeout 900    11000 9600   timeout 1 900   79 11000 false(unreach-call) 1 5.4  210 86   timeout 900    31 14000   done 1 17    1000 210 done 1 3.8 160 40
array-examples/standard_partition_ground-1.yml timeout 900 2200 11000 timeout 900   6700 13000 timeout 900    4300 12000   timeout 900    3500 12000   couldn't run: all seeds time out or crash 1.4 14 17 out of memory 8.3  15000 99   timeout 900    31 14000   out of memory (killed (signal 9, verification)) 45    15000 540 done 1 3.4 150 38
array-industry-pattern/array_ptr_single_elem_init-2.yml timeout 900 1800 12000 timeout 930   4900 12000 timeout 900    5000 11000   timeout 900    4000 11000   couldn't run: all seeds time out or crash 1.4 15 15 timeout 900    11000 9400   timeout 900    35 13000   done 1 2.0  190 21 done 1 3.4 150 37
array-industry-pattern/array_single_elem_init.yml timeout 900 2000 12000 timeout 900   6800 11000 timeout 900    5000 11000   timeout 900    3900 11000   timeout 900   69 12000 timeout 900    11000 8700   timeout 900    35 13000   out of memory (killed (signal 9, verification)) 15    15000 220 timeout 900   150 11000
reducercommutativity/rangesum.yml done 48 940 460 unknown 29   540 340 false(unreach-call) 1 1.1  62 15   false(unreach-call) 1 .29 29 3.1 false(unreach-call) 1 730   57 8800 false(valid-deref) 1 .26 41 2.9 error (0) .26 31 3.4 done 1 1.3  23 21 done 1 4.0 150 37
reducercommutativity/rangesum05.yml done 99 2400 980 unknown 79   670 830 false(unreach-call) 1 .89 58 11   false(unreach-call) 1 .11 26 1.4 false(unreach-call) 1 11   15 32 false(unreach-call) 1 .14 21 1.2 unknown 1 .28 31 2.9 done 1 .88 64 10 done 1 3.5 150 33
reducercommutativity/rangesum10.yml timeout 900 3600 8200 timeout 900   2200 10000 false(unreach-call) 1 .90 58 11   false(unreach-call) 1 .13 26 1.3 false(unreach-call) 1 8.4 13 27 false(unreach-call) 1 .14 22 2.7 unknown 1 .28 31 3.1 done 1 .91 63 11 done 1 3.5 150 40
reducercommutativity/rangesum20.yml timeout 900 4400 9800 timeout 900   1800 8100 false(unreach-call) 1 1.4  58 15   false(unreach-call) 1 .63 29 7.0 false(unreach-call) 1 8.6 13 37 false(unreach-call) 1 .18 36 3.1 unknown 1 .26 31 3.4 done 1 1.8  65 21 done 1 3.5 150 39
reducercommutativity/rangesum40.yml timeout 900 4700 10000 timeout 900   2300 8900 false(unreach-call) 1 9.3  59 120   false(unreach-call) 1 8.5  45 98   false(unreach-call) 1 14   12 42 false(unreach-call) 1 .21 41 2.2 unknown 1 .26 31 3.2 done 1 7.3  70 100 done 1 3.5 150 36
reducercommutativity/rangesum60.yml timeout 900 5200 12000 timeout 900   4600 8200 false(unreach-call) 1 180    170 2400   false(unreach-call) 1 180    170 2300   false(unreach-call) 1 14   12 52 false(unreach-call) 1 .23 48 2.7 unknown 1 .27 31 3.2 done 1 50    86 620 done 1 3.5 150 37
array-tiling/mlceu.yml timeout 900 910 10000 timeout 900   610 12000 done .13 27 1.8 timeout 900    160 12000   done 28   14 120 done .16 21 1.2 error (0) .20 31 2.8 timeout (verification) 900    2200 12000 timeout 900   150 12000
array-tiling/skippedu.yml done 1 23 780 190 unknown 1 3.3 280 30 false(unreach-call) .17 27 1.9 false(unreach-call) .14 27 1.6 timeout 1 900   34 13000 false(unreach-call) 1 .17 21 1.5 error (0) .19 31 2.8 done 1.0  24 14 done 1 11   150 140
array-programs/copysome1-2.yml timeout 900 2900 10000 timeout 900   8200 9800 timeout 900    10000 9100   timeout 900    9900 9900   couldn't run: all seeds time out or crash 3.1 17 45 false(unreach-call) 1 5.1  350 74   timeout 900    31 14000   done 1 25    1200 220 done 1 3.6 150 33
array-programs/copysome2-2.yml timeout 900 2900 10000 timeout 900   8900 11000 timeout 900    10000 9600   timeout 900    10000 9200   couldn't run: all seeds time out or crash 3.1 15 44 false(unreach-call) 1 7.2  530 110   timeout 900    31 14000   done 1 44    1500 360 done 1 440   4200 6300
../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 22 1 17000 59000 210000 22 1 17000 120000 210000 22 6 13000 130000 150000 22 6 14000 120000 160000 22 16 11000 920 140000 22 18 1900 41000 19000 22 5 13000 680 190000 22 18 1200 42000 16000 22 20 2300 7400 30000
Run set coveritest.test-comp19_prop-coverage-error-call.ReachSafety-Arrays cpa-tiger.test-comp19_prop-coverage-error-call.ReachSafety-Arrays esbmc-kind.test-comp19_prop-coverage-error-call.ReachSafety-Arrays esbmc-falsi.test-comp19_prop-coverage-error-call.ReachSafety-Arrays fairfuzz.test-comp19_prop-coverage-error-call.ReachSafety-Arrays klee.test-comp19_prop-coverage-error-call.ReachSafety-Arrays prtest.test-comp19_prop-coverage-error-call.ReachSafety-Arrays symbiotic.test-comp19_prop-coverage-error-call.ReachSafety-Arrays verifuzz.test-comp19_prop-coverage-error-call.ReachSafety-Arrays