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 timeout 890   930   1900 wit - -
ntdrivers/diskperf_false-unreach-call.i.cil.c witness timeout 7.8 7.6 170 wit timeout 90 72 2100 true 21 14   470
ntdrivers/floppy_false-unreach-call.i.cil.c witness unconfirmed 14   14   230 wit true 86 59 2100 true 37 21   560
ntdrivers/kbfiltr_false-unreach-call.i.cil.c witness unconfirmed 6.0 5.9 130 wit true 34 17 910 true 19 12   370
ntdrivers/parport_false-unreach-call.i.cil.c witness timeout 15   15   340 wit timeout 90 62 2500 true 42 24   760
ntdrivers/cdaudio_true-unreach-call.i.cil.c true 23   22   250 wit - -
ntdrivers/diskperf_true-unreach-call.i.cil.c true 21   21   220 wit - -
ntdrivers/floppy2_true-unreach-call.i.cil.c true 31   31   320 wit - -
ntdrivers/floppy_true-unreach-call.i.cil.c true 240   240   420 wit - -
ntdrivers/parport_true-unreach-call.i.cil.c true 29   29   370 wit - -
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c witness unconfirmed 17   16   210 wit true 23 12 630 true 18 15   350
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c witness timeout 10   10   190 wit timeout 91 65 3400 true 18 10   340
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c witness timeout 9.9 9.7 190 wit timeout 91 65 3800 true 15 8.4 350
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c witness timeout 10   10   200 wit timeout 91 67 3800 true 17 9.4 340
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c witness unconfirmed 10   9.8 200 wit true 21 11 560 true 16 8.5 340
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c witness unconfirmed 9.9 9.8 190 wit true 76 53 2900 true 17 9.8 370
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c witness unconfirmed 9.9 9.8 200 wit true 77 53 3200 true 18 10   350
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c witness unconfirmed 10   10   190 wit true 78 53 3000 true 17 12   350
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c witness unconfirmed 20   20   240 wit true 82 57 2900 true 17 9.5 340
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c witness unconfirmed 19   18   230 wit true 72 49 3000 true 17 9.7 340
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c witness unconfirmed 250   250   330 wit true 75 51 2800 true 20 12   370
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c witness unconfirmed 19   19   230 wit true 76 50 3100 true 17 9.6 350
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c witness unconfirmed 300   300   350 wit true 75 51 3000 true 18 10   370
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c witness unconfirmed 14   14   230 wit true 80 54 2900 true 16 9.0 370
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c witness unconfirmed 19   19   230 wit true 73 48 3100 true 17 12   350
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c witness unconfirmed 19   18   230 wit true 78 53 3100 true 17 9.3 350
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c witness unconfirmed 20   19   240 wit true 75 52 2900 true 18 12   360
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c witness unconfirmed 250   250   350 wit true 71 50 2800 true 17 9.9 370
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c witness unconfirmed 20   19   240 wit true 74 50 3100 true 17 10   340
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c true 880   880   390 wit - -
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c true 880   880   330 wit - -
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c true 880   880   390 wit - -
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c true 880   880   350 wit - -
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c true 880   880   400 wit - -
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c true 880   880   420 wit - -
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c true 880   880   450 wit - -
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c true 880   880   410 wit - -
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c true 880   880   430 wit - -
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c true 880   880   410 wit - -
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c true 880   880   410 wit - -
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c true 880   880   390 wit - -
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c true 880   880   410 wit - -
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c true 880   880   390 wit - -
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c true 880   880   430 wit - -
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c true 880   880   420 wit - -
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c true 880   880   400 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 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