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 true 210   210   4800 wit - -
ntdrivers/diskperf_false-unreach-call.i.cil.c witness timeout 1.5 1.5 100 wit timeout 91   71   2000 unknown 37 23 550
ntdrivers/floppy_false-unreach-call.i.cil.c witness invalid (assertion) 3.2 3.2 140 wit assertion 20   10   740 timeout 91 64 2600
ntdrivers/kbfiltr_false-unreach-call.i.cil.c error 850   850   2200 wit - -
ntdrivers/parport_false-unreach-call.i.cil.c witness timeout 14   14   670 wit timeout 91   59   2400 timeout 90 54 1100
ntdrivers/cdaudio_true-unreach-call.i.cil.c true 330   330   3600 wit - -
ntdrivers/diskperf_true-unreach-call.i.cil.c true 250   250   8300 wit - -
ntdrivers/floppy2_true-unreach-call.i.cil.c true 850   850   4200 wit - -
ntdrivers/floppy_true-unreach-call.i.cil.c true 850   850   1700 wit - -
ntdrivers/parport_true-unreach-call.i.cil.c true 850   850   4900 wit - -
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c witness invalid (assertion) 13   13   410 wit assertion 11   5.6 320 timeout 91 82 470
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c witness invalid (assertion) 4.6 4.6 180 wit assertion 9.3 5.0 330 timeout 91 82 460
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c witness invalid (assertion) 4.3 4.3 180 wit assertion 9.5 5.1 330 timeout 91 80 480
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c witness invalid (assertion) 4.4 4.4 180 wit assertion 9.2 4.9 320 timeout 91 81 470
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c witness invalid (assertion) 5.5 5.5 240 wit assertion 8.8 4.7 330 unknown 82 64 520
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c witness invalid (assertion) 5.5 5.5 230 wit assertion 10   5.6 350 unknown 65 47 540
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c witness invalid (assertion) 5.7 5.7 230 wit assertion 9.4 5.1 340 unknown 72 53 520
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c witness invalid (assertion) 5.5 5.5 230 wit assertion 11   6.0 340 unknown 67 50 530
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c witness invalid (assertion) 5.7 5.7 230 wit assertion 12   6.5 360 timeout 91 80 530
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c witness invalid (assertion) 5.8 5.8 230 wit assertion 12   6.5 370 timeout 91 79 560
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c witness invalid (assertion) 16   16   460 wit assertion 13   7.0 420 timeout 91 78 580
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c witness invalid (assertion) 5.9 5.9 230 wit assertion 11   6.1 360 timeout 91 82 540
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c witness invalid (assertion) 15   15   460 wit assertion 13   7.0 430 timeout 91 80 590
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c witness invalid (assertion) 6.0 6.0 230 wit assertion 12   6.4 360 timeout 91 81 540
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c witness invalid (assertion) 5.6 5.6 230 wit assertion 12   6.1 370 timeout 91 81 560
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c witness invalid (assertion) 5.7 5.7 230 wit assertion 11   5.9 360 timeout 91 81 540
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c witness invalid (assertion) 5.3 5.3 230 wit assertion 11   5.8 350 timeout 90 76 580
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c witness invalid (assertion) 17   17   460 wit assertion 12   6.8 400 timeout 91 78 540
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c witness invalid (assertion) 5.4 5.4 230 wit assertion 12   6.5 370 timeout 91 81 530
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c true 850   850   1300 wit - -
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c true 850   850   1300 wit - -
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c true 850   850   1300 wit - -
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c true 850   850   1300 wit - -
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c true 850   850   1600 wit - -
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c true 850   850   1500 wit - -
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c true 850   850   1600 wit - -
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c true 850   850   1600 wit - -
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c true 850   850   1600 wit - -
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c true 850   850   1600 wit - -
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c true 850   850   1500 wit - -
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c true 850   850   1600 wit - -
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c true 850   850   1600 wit - -
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c true 850   850   1600 wit - -
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c true 850   850   1600 wit - -
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c true 850   850   1600 wit - -
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c true 850   850   1600 wit - -
../../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