Tool ESBMC ESBMC version 2.0.0 64-bit x86_64 linux
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-23-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-16 17:45:19 CET [[ 2016-01-17 00:36:28 CET ]] [[ 2016-01-17 00:39:38 CET ]]
Run set sv-comp16.Simple
Options [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/esbmc.2016-01-16_1745.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/esbmc.2016-01-16_1745.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 unknown 8.4 8.5 2200 wit - -
ntdrivers/diskperf_false-unreach-call.i.cil.c unknown 4.2 4.2 210 wit - -
ntdrivers/floppy_false-unreach-call.i.cil.c unknown 890   900   280 wit - -
ntdrivers/kbfiltr_false-unreach-call.i.cil.c witness timeout 810   660   5600 wit timeout 91   69   3700 true 18 10   420
ntdrivers/parport_false-unreach-call.i.cil.c unknown 900   900   8600 wit - -
ntdrivers/cdaudio_true-unreach-call.i.cil.c unknown 6.3 6.3 2100 wit - -
ntdrivers/diskperf_true-unreach-call.i.cil.c unknown 4.3 4.3 210 wit - -
ntdrivers/floppy2_true-unreach-call.i.cil.c unknown 890   900   510 wit - -
ntdrivers/floppy_true-unreach-call.i.cil.c unknown 890   900   280 wit - -
ntdrivers/parport_true-unreach-call.i.cil.c unknown 900   900   8500 wit - -
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c witness timeout 800   710   4600 wit timeout 90   65   1200 true 16 8.7 340
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c witness unconfirmed 680   610   6900 wit unknown 8.2 4.6 290 true 17 9.6 340
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c witness unconfirmed 710   650   7000 wit unknown 8.7 4.7 290 true 16 9.4 340
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c witness unconfirmed 680   610   6900 wit unknown 8.8 4.8 320 true 16 9.2 340
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c witness timeout 830   720   7700 wit timeout 90   75   860 true 16 8.8 340
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c witness timeout 800   790   11000 wit timeout 90   73   970 true 14 8.3 330
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c witness timeout 820   820   13000 wit timeout 90   75   870 true 18 11   350
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c witness timeout 820   820   13000 wit timeout 90   72   900 true 14 8.2 330
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c witness timeout 830   830   13000 wit timeout 90   75   930 true 17 10   340
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c witness timeout 840   840   13000 wit timeout 90   76   870 true 15 8.7 350
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c witness timeout 800   780   13000 wit timeout 91   69   1000 true 17 9.5 340
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c witness timeout 800   790   13000 wit timeout 90   75   910 true 16 11   340
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c witness timeout 800   790   13000 wit timeout 90   71   980 true 16 11   330
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c witness timeout 840   840   13000 wit timeout 91   71   960 true 17 10   330
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c witness timeout 840   840   13000 wit timeout 91   75   890 true 16 9.8 330
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c witness timeout 850   850   11000 wit timeout 90   75   890 true 17 9.8 340
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c witness timeout 800   790   11000 wit timeout 91   74   910 true 17 11   340
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c witness timeout 800   790   11000 wit timeout 91   69   950 true 17 12   340
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c witness timeout 850   850   13000 wit timeout 90   75   940 true 16 10   330
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c true 230   230   4500 wit - -
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c true 240   240   6800 wit - -
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c true 230   230   6800 wit - -
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c true 260   260   6900 wit - -
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c true 310   310   8100 wit - -
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c true 430   430   12000 wit - -
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c true 450   450   14000 wit - -
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c true 460   460   14000 wit - -
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c true 440   440   14000 wit - -
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c out of memory 500   500   15000 wit - -
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c true 450   450   13000 wit - -
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c true 460   460   14000 wit - -
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c true 460   460   14000 wit - -
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c true 470   470   14000 wit - -
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c true 460   460   14000 wit - -
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c true 450   450   13000 wit - -
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c true 440   440   13000 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 27000 27000 430000 46 1600   1300   20000   46 320   200   6800  
    correct results 16 6200 6200 180000 0 0   0   0   0 0   0   0  
        correct true 16 6200 6200 180000 0 0   0   0   0 0   0   0  
        correct false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (46 tasks, max score: 68) 32
Run set sv-comp16.Simple