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-branches.ReachSafety-ControlFlow cpa-tiger.test-comp19_prop-coverage-branches.ReachSafety-ControlFlow esbmc-kind.test-comp19_prop-coverage-branches.ReachSafety-ControlFlow esbmc-falsi.test-comp19_prop-coverage-branches.ReachSafety-ControlFlow fairfuzz.test-comp19_prop-coverage-branches.ReachSafety-ControlFlow klee.test-comp19_prop-coverage-branches.ReachSafety-ControlFlow prtest.test-comp19_prop-coverage-branches.ReachSafety-ControlFlow symbiotic.test-comp19_prop-coverage-branches.ReachSafety-ControlFlow verifuzz.test-comp19_prop-coverage-branches.ReachSafety-ControlFlow
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)
ntdrivers-simplified/cdaudio_simpl1.cil-1.yml done .738 52 1300 510 true .738 29   510 310 unknown .0  .024 5.7 .11  unknown .0  .051 5.7 .12  done .0324 19 16 62 false(unreach-call) .738 .35 26 5.2 timeout .0294 900 31 12000 done .688 2.4  25 31   error .691 880 240 10000
ntdrivers-simplified/cdaudio_simpl1.cil-2.yml done .737 48 1200 410 true .737 29   510 290 unknown .0  .021 5.7 .097 unknown .0  .026 5.7 .094 timeout .530  900 21 3200 done .737 .35 26 5.4 timeout .0296 900 31 13000 done .686 2.4  24 31   error .349 880 240 11000
ntdrivers-simplified/diskperf_simpl1.cil.yml done .660 38 1400 330 true .660 20   430 230 unknown .0  .029 5.7 .13  unknown .0  .031 5.6 .12  timeout .593  900 19 2000 timeout .679 900    520 15000   timeout .154  900 31 13000 done .630 1.5  22 19   error .586 880 180 10000
ntdrivers-simplified/floppy_simpl3.cil-1.yml done .784 35 1100 310 true .784 17   480 160 unknown .0  .025 5.7 .11  unknown .0  .022 5.8 .12  false(unreach-call) .765  490 19 1600 false(unreach-call) .784 .30 23 3.6 timeout .0247 900 31 12000 done .716 1.4  21 19   error .784 880 180 11000
ntdrivers-simplified/floppy_simpl3.cil-2.yml done .784 37 1100 320 true .784 17   390 200 unknown .0  .026 5.6 .11  unknown .0  .021 5.7 .087 done .765  360 19 1500 done .784 .30 23 3.5 timeout .0247 900 30 13000 done .716 1.4  21 19   error .784 890 180 12000
ntdrivers-simplified/floppy_simpl4.cil-1.yml done .839 45 1200 410 true .839 23   480 250 unknown .0  .025 5.7 .12  unknown .0  .023 5.6 .092 false(unreach-call) .806  860 20 2600 false(unreach-call) .847 .47 28 6.4 timeout .0289 900 31 13000 done .740 2.1  23 27   error .847 880 200 8700
ntdrivers-simplified/floppy_simpl4.cil-2.yml done .839 41 1100 420 true .839 21   520 200 unknown .0  .023 5.7 .35  unknown .0  .040 5.8 .13  done .802  740 20 4200 done .847 .44 28 7.1 timeout .0289 900 31 16000 done .744 2.1  23 29   error .843 880 200 12000
ntdrivers-simplified/kbfiltr_simpl1.cil.yml done .467 24 890 190 true .467 7.4 310 64 unknown .0  .024 5.7 .046 unknown .0  .036 5.7 .14  done .05   27 16 80 done .742 .15 21 1.9 timeout .0417 900 31 12000 done .55  .70 19 9.7 error .733 880 170 10000
ntdrivers-simplified/kbfiltr_simpl2.cil-1.yml done .553 34 1100 290 true .553 12   490 100 unknown .0  .025 5.8 .11  unknown .0  .022 5.7 .14  done .595  220 18 770 done .784 .22 23 2.1 timeout .0421 900 30 14000 done .563 1.1  20 15   error .784 890 180 11000
ntdrivers-simplified/kbfiltr_simpl2.cil-2.yml done .557 34 1100 300 true .557 11   370 110 unknown .0  .025 5.7 .068 unknown .0  .026 5.7 .13  false(unreach-call) .609  290 18 890 false(unreach-call) .787 .22 23 2.4 timeout .0417 900 31 12000 done .568 1.1  20 13   error .781 890 190 12000
ssh-simplified/s3_clnt_1.cil-1.yml done .784 70 1000 1100 true .784 220   530 3000 unknown .0  .029 5.7 .22  unknown .0  .025 5.8 .066 done .0309 35 13 120 done .790 1.7  31 21   timeout .0247 900 31 13000 done .704 1.7  20 22   error .790 890 200 10000
ssh-simplified/s3_clnt_1.cil-2.yml done .784 65 1100 760 true .784 160   490 1900 unknown .0  .030 5.7 .14  unknown .0  .041 5.7 .11  done .0309 26 14 130 false(unreach-call) .790 .92 25 12   timeout .0247 900 31 14000 done .710 1.7  20 22   error .790 890 200 11000
ssh-simplified/s3_clnt_2.cil-1.yml done .784 65 1100 690 true .784 170   530 2300 unknown .0  .029 5.7 .16  unknown .0  .050 5.7 .15  done .0309 26 13 130 false(unreach-call) .778 .93 26 11   timeout .0247 900 31 13000 done .710 1.6  20 21   error .796 890 200 12000
ssh-simplified/s3_clnt_2.cil-2.yml done .778 58 1200 660 true .778 170   530 2200 unknown .0  .029 5.7 .16  unknown .0  .024 5.7 .15  done .0309 36 14 130 done .772 1.6  31 21   timeout .0247 900 31 13000 done .704 1.7  20 25   error .790 890 200 9700
ssh-simplified/s3_clnt_3.cil-1.yml done .55  57 1100 610 true .556 75   720 1000 unknown .0  .022 5.6 .13  unknown .0  .033 5.7 .14  done .025  32 18 110 done .356 .14 21 1.5 timeout .0188 900 31 12000 done .025 .56 16 7.1 error .119 890 200 12000
ssh-simplified/s3_clnt_3.cil-2.yml done .833 80 1100 950 true .833 130   890 1600 unknown .0  .029 5.6 .17  unknown .0  .017 5.7 .25  done .0309 42 15 130 false(unreach-call) .840 3.4  42 49   timeout .0370 900 31 13000 done .759 2.1  21 30   error .840 890 200 13000
ssh-simplified/s3_clnt_3.cil-3.yml done .778 66 1100 720 true .778 210   570 3100 unknown .0  .027 5.6 .079 unknown .0  .047 5.7 .080 done .0309 26 12 100 done .772 1.7  31 23   timeout .0247 900 31 13000 done .704 1.7  20 25   error .790 890 200 13000
ssh-simplified/s3_clnt_4.cil-1.yml done .778 61 1100 610 true .778 120   590 1600 unknown .0  .027 5.7 .20  unknown .0  .021 5.6 .13  done .0309 39 14 98 done .772 1.7  31 28   timeout .0247 900 31 11000 done .704 1.6  20 20   error .790 890 200 12000
ssh-simplified/s3_clnt_4.cil-2.yml done .833 81 1200 920 true .833 140   530 2000 unknown .0  .023 5.7 .090 unknown .0  .027 5.7 .085 done .0309 40 14 140 false(unreach-call) .840 3.3  40 41   timeout .0247 900 31 16000 done .759 2.0  20 29   error .840 890 200 12000
../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 19 13.9 990 21000 10000 19 13.9 1600 9900 21000 19 .0  .49 110 2.6 19 .0  .58 110 2.3 19 5.82 5100 310 18000 19 14.4  920   1000 15000 19 .675 17000 580 250000 19 12.4 31 400 410 19 13.7 17000 3800 210000
Run set coveritest.test-comp19_prop-coverage-branches.ReachSafety-ControlFlow cpa-tiger.test-comp19_prop-coverage-branches.ReachSafety-ControlFlow esbmc-kind.test-comp19_prop-coverage-branches.ReachSafety-ControlFlow esbmc-falsi.test-comp19_prop-coverage-branches.ReachSafety-ControlFlow fairfuzz.test-comp19_prop-coverage-branches.ReachSafety-ControlFlow klee.test-comp19_prop-coverage-branches.ReachSafety-ControlFlow prtest.test-comp19_prop-coverage-branches.ReachSafety-ControlFlow symbiotic.test-comp19_prop-coverage-branches.ReachSafety-ControlFlow verifuzz.test-comp19_prop-coverage-branches.ReachSafety-ControlFlow