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-ControlFlow cpa-tiger.test-comp19_prop-coverage-error-call.ReachSafety-ControlFlow esbmc-kind.test-comp19_prop-coverage-error-call.ReachSafety-ControlFlow esbmc-falsi.test-comp19_prop-coverage-error-call.ReachSafety-ControlFlow fairfuzz.test-comp19_prop-coverage-error-call.ReachSafety-ControlFlow klee.test-comp19_prop-coverage-error-call.ReachSafety-ControlFlow prtest.test-comp19_prop-coverage-error-call.ReachSafety-ControlFlow symbiotic.test-comp19_prop-coverage-error-call.ReachSafety-ControlFlow verifuzz.test-comp19_prop-coverage-error-call.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 1 7.6 330 69 unknown 1 9.6 400 79 false(unreach-call) .51 52 6.2 false(unreach-call) .52 52 11   timeout 900 20 3900 false(unreach-call) 1 .23 25 2.5 timeout 900 31 12000 done 3.7 31 46 error 860 250 11000
ntdrivers-simplified/floppy_simpl3.cil-1.yml done 1 7.2 290 64 unknown 1 5.8 320 57 false(unreach-call) .22 33 2.6 false(unreach-call) .22 32 2.6 false(unreach-call) 1 450 20 1500 false(unreach-call) 1 .15 21 1.8 timeout 900 31 12000 done 2.2 22 24 done 1 18 190 210
ntdrivers-simplified/floppy_simpl4.cil-1.yml done 1 8.4 320 71 unknown 1 7.5 350 68 false(unreach-call) .33 39 3.7 false(unreach-call) .34 39 5.5 false(unreach-call) 1 660 20 2000 false(unreach-call) 1 .23 25 2.9 timeout 900 31 13000 done 3.1 26 38 done 1 100 200 1100
ntdrivers-simplified/kbfiltr_simpl2.cil-2.yml done 1 6.4 290 57 unknown 1 4.9 300 45 false(unreach-call) .17 30 2.1 false(unreach-call) .17 30 2.2 false(unreach-call) 1 240 19 920 false(unreach-call) 1 .20 21 1.6 timeout 900 30 12000 done 1.8 20 22 done 1 20 190 230
ssh-simplified/s3_clnt_1.cil-2.yml done 1 7.1 330 68 unknown 1 6.9 330 59 false(unreach-call) 2.0  63 49   false(unreach-call) .92 56 12   done 26 14 120 false(unreach-call) 1 .16 21 2.4 timeout 900 31 12000 done 1.7 20 22 done 1 70 200 870
ssh-simplified/s3_clnt_2.cil-1.yml done 1 7.2 340 66 unknown 1 5.9 310 49 false(unreach-call) 1.8  64 24   false(unreach-call) .94 56 11   done 39 13 100 false(unreach-call) 1 .16 21 1.8 timeout 900 31 12000 done 1.7 19 23 done 1 63 200 610
ssh-simplified/s3_clnt_3.cil-2.yml done 1 7.1 290 68 unknown 1 7.2 340 64 false(unreach-call) 2.2  75 25   false(unreach-call) 1.1  66 14   done 38 14 110 false(unreach-call) 1 .19 21 1.9 timeout 900 31 13000 done 1.9 20 25 done 1 75 210 900
ssh-simplified/s3_clnt_4.cil-2.yml done 1 6.9 330 64 unknown 1 6.1 310 56 false(unreach-call) 1.9  65 22   false(unreach-call) .98 58 12   done 40 14 120 false(unreach-call) 1 .21 21 2.0 timeout 900 31 12000 done 1.8 20 23 done 1 85 200 1000
../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 8 8 58 2500 530 8 8 54 2700 480 8 9.2 420 140 8 5.2 390 69 8 3 2400 130 8700 8 8 1.5 180 17 8 7200 250 100000 8 18 180 220 8 7 1300 1600 16000
Run set coveritest.test-comp19_prop-coverage-error-call.ReachSafety-ControlFlow cpa-tiger.test-comp19_prop-coverage-error-call.ReachSafety-ControlFlow esbmc-kind.test-comp19_prop-coverage-error-call.ReachSafety-ControlFlow esbmc-falsi.test-comp19_prop-coverage-error-call.ReachSafety-ControlFlow fairfuzz.test-comp19_prop-coverage-error-call.ReachSafety-ControlFlow klee.test-comp19_prop-coverage-error-call.ReachSafety-ControlFlow prtest.test-comp19_prop-coverage-error-call.ReachSafety-ControlFlow symbiotic.test-comp19_prop-coverage-error-call.ReachSafety-ControlFlow verifuzz.test-comp19_prop-coverage-error-call.ReachSafety-ControlFlow