Tool SMACK+Corral 1.5.2
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-07 09:05:16 CET [[ 2016-01-15 09:34:34 CET ]] [[ 2016-01-15 22:36:10 CET ]]
Run set sv-comp16.Simple
Options -w error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/smack.2016-01-07_0905.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/smack.2016-01-07_0905.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 890   930   1900
ntdrivers/diskperf_false-unreach-call.i.cil.c 7.8 7.6 170 90 72 2100 21 14   470
ntdrivers/floppy_false-unreach-call.i.cil.c 14   14   230 86 59 2100 37 21   560
ntdrivers/kbfiltr_false-unreach-call.i.cil.c 6.0 5.9 130 34 17 910 19 12   370
ntdrivers/parport_false-unreach-call.i.cil.c 15   15   340 90 62 2500 42 24   760
ntdrivers/cdaudio_true-unreach-call.i.cil.c 23   22   250
ntdrivers/diskperf_true-unreach-call.i.cil.c 21   21   220
ntdrivers/floppy2_true-unreach-call.i.cil.c 31   31   320
ntdrivers/floppy_true-unreach-call.i.cil.c 240   240   420
ntdrivers/parport_true-unreach-call.i.cil.c 29   29   370
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c 17   16   210 23 12 630 18 15   350
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c 10   10   190 91 65 3400 18 10   340
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c 9.9 9.7 190 91 65 3800 15 8.4 350
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c 10   10   200 91 67 3800 17 9.4 340
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c 10   9.8 200 21 11 560 16 8.5 340
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c 9.9 9.8 190 76 53 2900 17 9.8 370
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c 9.9 9.8 200 77 53 3200 18 10   350
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c 10   10   190 78 53 3000 17 12   350
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c 20   20   240 82 57 2900 17 9.5 340
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c 19   18   230 72 49 3000 17 9.7 340
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c 250   250   330 75 51 2800 20 12   370
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c 19   19   230 76 50 3100 17 9.6 350
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c 300   300   350 75 51 3000 18 10   370
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c 14   14   230 80 54 2900 16 9.0 370
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c 19   19   230 73 48 3100 17 12   350
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c 19   18   230 78 53 3100 17 9.3 350
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c 20   19   240 75 52 2900 18 12   360
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c 250   250   350 71 50 2800 17 9.9 370
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c 20   19   240 74 50 3100 17 10   340
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c 880   880   390
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c 880   880   330
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c 880   880   390
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c 880   880   350
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c 880   880   400
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c 880   880   420
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c 880   880   450
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c 880   880   410
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c 880   880   430
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c 880   880   410
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c 880   880   410
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c 880   880   390
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c 880   880   410
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c 880   880   390
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c 880   880   430
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c 880   880   420
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c 880   880   400
../../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 17000 17000 16000 46 1700   1200   62000   46 450   270   8800  
    correct results 22 15000 15000 8400 0 0   0   0   0 0   0   0  
        correct true 22 15000 15000 8400 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) 44
Run set sv-comp16.Simple