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-Heap cpa-tiger.test-comp19_prop-coverage-error-call.ReachSafety-Heap esbmc-kind.test-comp19_prop-coverage-error-call.ReachSafety-Heap esbmc-falsi.test-comp19_prop-coverage-error-call.ReachSafety-Heap fairfuzz.test-comp19_prop-coverage-error-call.ReachSafety-Heap klee.test-comp19_prop-coverage-error-call.ReachSafety-Heap prtest.test-comp19_prop-coverage-error-call.ReachSafety-Heap symbiotic.test-comp19_prop-coverage-error-call.ReachSafety-Heap verifuzz.test-comp19_prop-coverage-error-call.ReachSafety-Heap
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/ldv-regression/ 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)
fo_test.yml done 1 4.4 280 38 unknown 1 3.4 270 33 false(unreach-call) .092 27 1.1 false(unreach-call) .12 27 .94 false(unreach-call) 1 2.8 17 56 false(unreach-call) 1 .12 21 1.2 unknown 1 .25 31 3.4 done 1 .59 19 6.5 done 1 4.9 170 46
rule60_list2.c_1.yml done 1 4.8 280 41 unknown 1 3.8 270 32 false(unreach-call) .14  27 1.4 false(unreach-call) .16 27 2.4  false(unreach-call) 1 16   15 62 false(unreach-call) 1 .13 21 1.3 timeout 900    31 12000   done 1 .67 18 10   done 1 4.8 170 53
test21-2.yml done 1 3.4 270 31 unknown 1 3.1 270 29 false(unreach-call) .10  26 1.2 false(unreach-call) .13 26 1.1  false(unreach-call) 1 25   17 79 false(unreach-call) 1 .11 21 1.3 unknown 1 .24 31 2.9 done 1 .79 19 11   done 1 3.5 150 33
test22-2.yml done 1 23   1200 270 unknown 1 3.2 270 33 false(unreach-call) .11  26 1.3 false(unreach-call) .11 26 1.2  false(unreach-call) 1 10   15 31 false(unreach-call) 1 .12 21 1.5 unknown 9.9  31 140   done .98 20 14   done 1 6.5 150 72
test23-1.yml done 1 31   1500 370 unknown 1 11   290 120 false(unreach-call) 2.3   32 33   false(unreach-call) 1.4  32 21    false(unreach-call) 1 26   17 120 false(unreach-call) 1 .25 23 2.9 unknown 1 580    31 7800   done 1 1.3  27 14   done 1 3.6 150 36
test24-2.yml done 1 5.2 290 51 unknown 1 6.4 300 58 error (1) .51  37 7.0 error (1) .33 33 3.9  false(unreach-call) 1 21   13 63 false(unreach-call) 1 .15 23 1.7 timeout 900    31 12000   done 1 .60 23 8.0 done 1 4.2 150 48
test25-1.yml done 1 32   1800 370 unknown 1 12   300 140 error (1) .36  32 4.7 error (1) .24 29 2.5  false(unreach-call) 1 21   14 60 false(unreach-call) 1 .28 23 2.8 timeout 900    31 10000   done 1 .62 23 7.2 done 1 4.0 150 40
test28-1.yml done 1 3.5 270 27 unknown 1 2.9 270 27 false(unreach-call) 1 .10  26 1.1 false(unreach-call) 1 .10 26 1.1  done 1 13   17 100 false(unreach-call) 1 .11 21 1.2 unknown 1 710    31 10000   done 1 .63 19 8.7 timeout 900   150 12000
test29-1.yml done 1 23   720 200 unknown 1 2.8 270 28 false(unreach-call) .11  26 1.2 false(unreach-call) .11 26 1.2  false(unreach-call) 1 7.9 14 35 false(unreach-call) 1 .11 21 1.3 unknown 1 690    31 9600   done 1 .50 19 7.5 done 1 3.7 150 36
../sv-benchmarks/c/ldv-regression/ 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 9 9 130 6700 1400 9 9 48 2500 500 9 1 3.9  260 52   9 1 2.7  250 35   9 9 140 140 610 9 9 1.4 200 15 9 5 4700 280 63000 9 8 6.6 190 87 9 8 940 1400 12000
Run set coveritest.test-comp19_prop-coverage-error-call.ReachSafety-Heap cpa-tiger.test-comp19_prop-coverage-error-call.ReachSafety-Heap esbmc-kind.test-comp19_prop-coverage-error-call.ReachSafety-Heap esbmc-falsi.test-comp19_prop-coverage-error-call.ReachSafety-Heap fairfuzz.test-comp19_prop-coverage-error-call.ReachSafety-Heap klee.test-comp19_prop-coverage-error-call.ReachSafety-Heap prtest.test-comp19_prop-coverage-error-call.ReachSafety-Heap symbiotic.test-comp19_prop-coverage-error-call.ReachSafety-Heap verifuzz.test-comp19_prop-coverage-error-call.ReachSafety-Heap