Tool BLAST 2.7.3
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 17:36:26 CET [[ 2016-01-15 08:15:11 CET ]] [[ 2016-01-15 21:49:51 CET ]]
Run set sv-comp16.Simple
Options -alias empty -enable-recursion -noprofile -cref -sv-comp -lattice -include-lattice symb -nosserr -svcomp-witness error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/blast.2016-01-03_1736.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/blast.2016-01-03_1736.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 740    930    250 wit - -
ntdrivers/diskperf_false-unreach-call.i.cil.c witness timeout 14    14    180 wit timeout 90 72   1900 unknown 23 15 520
ntdrivers/floppy_false-unreach-call.i.cil.c false(reach) 9.7  9.7  130 wit false(reach) 49 32   1000 true 34 20 550
ntdrivers/kbfiltr_false-unreach-call.i.cil.c false(reach) 42    59    58 wit false(reach) 17 9.9 560 true 18 10 410
ntdrivers/parport_false-unreach-call.i.cil.c witness timeout 7.6  8.5  100 wit timeout 91 58   2300 timeout 90 71 810
ntdrivers/cdaudio_true-unreach-call.i.cil.c true 290    400    270 wit - -
ntdrivers/diskperf_true-unreach-call.i.cil.c true 190    210    410 wit - -
ntdrivers/floppy2_true-unreach-call.i.cil.c true .56 .56 44 wit - -
ntdrivers/floppy_true-unreach-call.i.cil.c exception (gremlins) 96    110    170 wit - -
ntdrivers/parport_true-unreach-call.i.cil.c timeout 670    930    310 wit - -
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c witness unconfirmed 19    26    53 wit true 16 8.4 490 timeout 91 82 480
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c witness unconfirmed 13    18    48 wit true 16 8.5 480 timeout 91 81 470
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c witness unconfirmed 14    19    46 wit true 16 8.3 460 timeout 91 83 470
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c witness unconfirmed 15    20    53 wit true 15 8.0 480 timeout 91 81 470
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c witness unconfirmed 8.3  11    46 wit true 11 6.0 440 unknown 55 35 540
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c witness unconfirmed 5.3  6.5  45 wit true 12 6.3 430 unknown 59 38 560
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c witness unconfirmed 5.1  6.3  47 wit true 12 6.6 430 unknown 52 34 500
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c witness unconfirmed 5.4  6.7  47 wit true 12 6.5 440 unknown 50 32 520
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c witness unconfirmed 330    450    250 wit true 11 5.9 430 unknown 76 55 520
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c witness unconfirmed 180    260    150 wit true 11 6.2 450 unknown 72 53 530
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c timeout 690    930    320 wit - -
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c witness unconfirmed 180    260    150 wit true 12 6.5 430 unknown 76 56 540
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c timeout 690    930    320 wit - -
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c witness unconfirmed 74    100    63 wit true 12 6.3 440 unknown 62 44 530
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c witness unconfirmed 270    370    170 wit true 10 5.5 420 unknown 71 52 540
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c witness unconfirmed 190    260    150 wit true 12 6.6 430 unknown 70 51 530
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c witness unconfirmed 270    370    170 wit true 12 6.5 440 unknown 72 52 560
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c timeout 690    930    450 wit - -
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c witness unconfirmed 330    450    250 wit true 12 6.7 430 unknown 70 51 550
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c timeout 660    930    280 wit - -
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c true 310    440    160 wit - -
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c timeout 670    930    290 wit - -
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c true 310    430    160 wit - -
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c timeout 670    930    380 wit - -
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c timeout 660    930    440 wit - -
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c timeout 700    930    300 wit - -
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c timeout 670    930    300 wit - -
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c timeout 670    930    300 wit - -
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c timeout 670    930    310 wit - -
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c timeout 670    930    430 wit - -
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c timeout 660    930    410 wit - -
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c timeout 690    930    310 wit - -
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c timeout 670    930    300 wit - -
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c timeout 670    930    300 wit - -
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c timeout 670    930    420 wit - -
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c timeout 690    930    310 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 23000 10000 46 450   280   13000   46 1300   1000   11000  
    correct results 7 1200 1600 1200 2 66   42   1600   2 52   30   960  
        correct true 5 1100 1500 1000 0 0   0   0   2 0   0   0  
        correct false 2 52 68 190 2 66   42   1600   0 52   30   960  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (46 tasks, max score: 68) 12
Run set sv-comp16.Simple