Tool CBMC CPAchecker 1.4-svn 18912M
Limits timelimit: 60 s, memlimit: 4000 MB, CPU core limit: 2
Host tortuga
OS Linux 3.13.0-71-generic x86_64
System CPU: Intel Core i7-2600 CPU @ 3.40GHz, cores: 8, frequency: 3401 MHz, Turbo Boost: enabled; RAM: 16783 MB
Date of execution 2015-12-11 12:11:02 CET 2015-12-11 10:59:27 CET
Run set cbmc predicateAnalysis.ABEl
Options -heap 13000M -noout -disable-java-assertions -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -predicateAnalysis-PredAbsRefiner-ABEl
test/programs/benchmarks/ status cputime (s) walltime (s) memUsage (MB) status cputime (s) walltime (s) memUsage (MB)
ntdrivers/cdaudio_false-unreach-call.i.cil.c 60.1  60.1  987 60.7  38.8  3070
ntdrivers/diskperf_false-unreach-call.i.cil.c 1.24 1.26 104 15.8  9.00 256
ntdrivers/floppy_false-unreach-call.i.cil.c 3.10 3.11 140 22.0  11.9  439
ntdrivers/kbfiltr_false-unreach-call.i.cil.c 60.1  60.1  573 10.8  6.08 219
ntdrivers/parport_false-unreach-call.i.cil.c 13.0  13.3  676 10.2  5.94 249
ntdrivers/cdaudio_true-unreach-call.i.cil.c 60.1  60.4  993 17.0  9.18 295
ntdrivers/diskperf_true-unreach-call.i.cil.c 60.2  60.1  3500 15.7  8.89 273
ntdrivers/floppy2_true-unreach-call.i.cil.c 60.1  60.0  989 60.9  39.7  3010
ntdrivers/floppy_true-unreach-call.i.cil.c 60.0  60.4  391 35.6  20.2  1260
ntdrivers/parport_true-unreach-call.i.cil.c 61.1  61.7  2180 9.85 6.13 251
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c 11.6  12.0  411 15.2  8.35 268
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c 3.79 4.15 182 17.1  9.61 270
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c 3.78 3.82 182 16.7  9.32 269
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c 3.77 3.79 180 15.8  8.98 269
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c 4.91 4.94 242 10.5  6.20 197
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c 4.87 4.90 229 10.6  5.98 253
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c 4.89 4.90 229 9.79 5.56 249
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c 4.91 4.96 228 10.6  6.24 256
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c 5.25 5.27 231 16.7  9.38 275
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c 5.11 5.14 234 17.0  9.30 272
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c 15.4  15.4  461 29.3  16.4  939
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c 5.14 5.17 233 15.8  8.87 263
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c 14.9  15.0  459 25.0  13.6  419
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c 5.24 5.26 234 21.2  11.3  302
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c 4.96 4.99 229 14.0  7.67 255
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c 5.25 5.28 232 18.9  10.5  399
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c 4.98 5.02 230 17.1  9.42 290
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c 15.5  15.5  463 21.5  11.9  400
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c 5.22 5.26 229 18.8  10.1  275
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c 60.1  60.1  703 20.6  12.1  676
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c 60.0  60.5  654 21.0  11.8  665
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c 60.1  60.4  654 18.4  10.2  407
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c 60.0  60.4  656 16.8  9.56 396
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c 60.0  60.4  843 37.1  21.5  1240
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c 60.0  60.4  796 34.3  18.4  705
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c 60.1  60.4  784 23.6  13.6  674
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c 60.0  60.5  811 32.9  18.1  702
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c 60.1  60.2  799 48.1  31.1  2900
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c 60.0  60.4  817 27.6  15.7  722
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c 60.0  60.4  797 30.3  16.4  688
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c 60.1  60.2  814 61.2  45.0  2910
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c 60.1  60.1  803 38.0  23.0  1740
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c 60.1  60.1  816 51.2  37.9  4000
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c 60.1  60.1  804 54.7  38.0  2910
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c 60.8  61.5  801 34.5  19.9  1230
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c 60.0  60.1  808 27.0  14.8  700
test/programs/benchmarks/ status cputime (s) walltime (s) memUsage (MB) status cputime (s) walltime (s) memUsage (MB)
total 46 1590 1600 28800 46 1160 691 38700
local summary 148 1620 1160 697
    correct results 22 147 148 6040 40 903 518 25200
        correct true 0 18 533 312 18200
        correct false 22 147 148 6040 22 370 206 7030
    incorrect results 0 0
        incorrect true 0 0
        incorrect false 0 0
score (46 tasks, max score: 68) 22 58
Run set cbmc predicateAnalysis.ABEl