Tool SeaHorn-F16 0.1.0
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-11 21:35:00 [[ 2016-01-15 18:20:27 CET ]] [[ 2016-01-15 22:30:28 CET ]]
Run set sv-comp16.Simple
Options --cex=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/seahorn.2016-01-11_2135.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/seahorn.2016-01-11_2135.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 900   450    320 wit - -
ntdrivers/diskperf_false-unreach-call.i.cil.c witness timeout 1.8 .93 120 wit timeout 91 69   1700 true 19 11   450
ntdrivers/floppy_false-unreach-call.i.cil.c witness timeout 2.3 1.2  140 wit timeout 90 74   1600 true 30 18   540
ntdrivers/kbfiltr_false-unreach-call.i.cil.c false(reach) 1.1 .58 66 wit false(reach) 20 11   610 true 17 9.8 390
ntdrivers/parport_false-unreach-call.i.cil.c witness timeout 7.6 3.9  700 wit timeout 90 61   2200 true 43 24   750
ntdrivers/cdaudio_true-unreach-call.i.cil.c true 1.2 .63 75 wit - -
ntdrivers/diskperf_true-unreach-call.i.cil.c true 2.1 1.1  140 wit - -
ntdrivers/floppy2_true-unreach-call.i.cil.c true 5.7 3.0  300 wit - -
ntdrivers/floppy_true-unreach-call.i.cil.c true 3.1 1.6  150 wit - -
ntdrivers/parport_true-unreach-call.i.cil.c true 110   56    1200 wit - -
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c false(reach) 2.3 1.1  67 wit false(reach) 27 16   660 true 17 11   340
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c false(reach) 2.3 1.2  75 wit false(reach) 27 16   670 true 16 9.2 330
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c false(reach) 2.3 1.2  79 wit false(reach) 27 17   650 true 15 9.0 330
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c false(reach) 2.6 1.3  79 wit false(reach) 27 16   660 true 15 9.4 320
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c false(reach) 1.3 .67 72 wit false(reach) 23 13   590 true 16 8.9 360
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c false(reach) 1.3 .68 78 wit false(reach) 24 13   570 true 17 11   340
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c false(reach) 1.2 .62 77 wit false(reach) 24 13   580 true 16 8.7 350
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c false(reach) 1.3 .66 76 wit false(reach) 22 13   570 true 16 9.2 330
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c false(reach) 3.1 1.6  83 wit false(reach) 12 6.5 450 true 14 7.7 340
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c false(reach) 2.9 1.5  85 wit false(reach) 27 16   680 true 16 10   350
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c false(reach) 13   6.3  100 wit false(reach) 12 6.4 440 true 17 11   380
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c false(reach) 2.6 1.3  84 wit false(reach) 27 16   680 true 18 11   350
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c false(reach) 8.4 4.2  82 wit false(reach) 13 7.0 470 true 17 10   340
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c false(reach) 2.1 1.1  79 wit false(reach) 29 17   720 true 15 8.4 340
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c false(reach) 2.7 1.4  71 wit false(reach) 13 7.1 440 true 16 10   330
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c false(reach) 3.0 1.5  84 wit false(reach) 31 18   680 true 14 8.2 330
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c false(reach) 3.4 1.7  86 wit false(reach) 12 6.7 450 true 16 9.0 320
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c false(reach) 14   6.8  110 wit false(reach) 12 6.4 460 true 16 11   340
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c false(reach) 2.8 1.4  79 wit false(reach) 13 7.0 450 true 17 9.9 340
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c true 9.3 4.7  70 wit - -
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c true 91   46    140 wit - -
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c true 58   29    100 wit - -
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c true 15   7.8  81 wit - -
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c true 12   6.0  67 wit - -
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c true 64   32    81 wit - -
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c timeout 900   450    220 wit - -
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c true 93   47    92 wit - -
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c true 11   5.5  78 wit - -
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c true 77   39    87 wit - -
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c true 6.8 3.4  73 wit - -
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c true 43   21    78 wit - -
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c true 240   120    120 wit - -
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c true 35   18    77 wit - -
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c timeout 900   450    200 wit - -
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c true 10   5.3  80 wit - -
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c timeout 900   450    180 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 4600 2300 6600 46 690   450   17000   46 410   250   8600  
    correct results 39 970 480 4700 20 420   240   11000   20 320   190   6900  
        correct true 19 890 450 3100 0 0   0   0   20 0   0   0  
        correct false 20 73 37 1600 20 420   240   11000   0 320   190   6900  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (46 tasks, max score: 68) 58
Run set sv-comp16.Simple