Tool CBMC
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host [zeus01; zeus02; zeus03; zeus04; zeus05; zeus06; zeus07; zeus08; zeus09; zeus10; zeus11; zeus12; zeus13; zeus14; zeus15; zeus16; zeus17; zeus18; zeus19; zeus20; zeus21; zeus22; zeus23; zeus24]
OS Linux 4.2.0-22-generic
System CPU: Intel Xeon E5-2650 v2 @ 2.60 GHz, cores: 32, frequency: 3.4 GHz; RAM: 135149 MB
Date of execution 2016-01-03 00:42:25 CET [[ 2016-01-15 08:22:02 CET ]] [[ 2016-01-15 21:54:19 CET ]]
Run set sv-comp16.Simple
Options --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cbmc.2016-01-03_0042.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cbmc.2016-01-03_0042.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]
../../sv-benchmarks/c/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime (s) wit1_walltime (s) wit1_memUsage (MB) wit2_status wit2_cputime (s) wit2_walltime (s) wit2_memUsage (MB)
ntdrivers/cdaudio_false-unreach-call.i.cil.c 210   210   4800
ntdrivers/diskperf_false-unreach-call.i.cil.c 1.5 1.5 100 91   71   2000 37 23 550
ntdrivers/floppy_false-unreach-call.i.cil.c 3.2 3.2 140 20   10   740 91 64 2600
ntdrivers/kbfiltr_false-unreach-call.i.cil.c 850   850   2200
ntdrivers/parport_false-unreach-call.i.cil.c 14   14   670 91   59   2400 90 54 1100
ntdrivers/cdaudio_true-unreach-call.i.cil.c 330   330   3600
ntdrivers/diskperf_true-unreach-call.i.cil.c 250   250   8300
ntdrivers/floppy2_true-unreach-call.i.cil.c 850   850   4200
ntdrivers/floppy_true-unreach-call.i.cil.c 850   850   1700
ntdrivers/parport_true-unreach-call.i.cil.c 850   850   4900
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c 13   13   410 11   5.6 320 91 82 470
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c 4.6 4.6 180 9.3 5.0 330 91 82 460
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c 4.3 4.3 180 9.5 5.1 330 91 80 480
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c 4.4 4.4 180 9.2 4.9 320 91 81 470
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c 5.5 5.5 240 8.8 4.7 330 82 64 520
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c 5.5 5.5 230 10   5.6 350 65 47 540
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c 5.7 5.7 230 9.4 5.1 340 72 53 520
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c 5.5 5.5 230 11   6.0 340 67 50 530
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c 5.7 5.7 230 12   6.5 360 91 80 530
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c 5.8 5.8 230 12   6.5 370 91 79 560
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c 16   16   460 13   7.0 420 91 78 580
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c 5.9 5.9 230 11   6.1 360 91 82 540
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c 15   15   460 13   7.0 430 91 80 590
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c 6.0 6.0 230 12   6.4 360 91 81 540
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c 5.6 5.6 230 12   6.1 370 91 81 560
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c 5.7 5.7 230 11   5.9 360 91 81 540
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c 5.3 5.3 230 11   5.8 350 90 76 580
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c 17   17   460 12   6.8 400 91 78 540
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c 5.4 5.4 230 12   6.5 370 91 81 530
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c 850   850   1300
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c 850   850   1300
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c 850   850   1300
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c 850   850   1300
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c 850   850   1600
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c 850   850   1500
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c 850   850   1600
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c 850   850   1600
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c 850   850   1600
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c 850   850   1600
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c 850   850   1500
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c 850   850   1600
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c 850   850   1600
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c 850   850   1600
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c 850   850   1600
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c 850   850   1600
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c 850   850   1600
../../sv-benchmarks/c/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime (s) wit1_walltime (s) wit1_memUsage (MB) wit2_status wit2_cputime (s) wit2_walltime (s) wit2_memUsage (MB)
total tasks 46 19000 19000 61000 46 410   250   12000   46 1900   1600   14000  
    correct results 22 18000 18000 48000 0 0   0   0   0 0   0   0  
        correct true 22 18000 18000 48000 0 0   0   0   0 0   0   0  
        correct false 0
    incorrect results 1 210 210 4800 0 0   0   0   0 0   0   0  
        incorrect true 1 210 210 4800 0 0   0   0   0 0   0   0  
        incorrect false 0
score (46 tasks, max score: 68) 12
Run set sv-comp16.Simple