Tool CPAchecker 1.4-svcomp16c
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-04 06:25:51 CET [[ 2016-01-15 08:31:02 CET ]] [[ 2016-01-15 21:59:57 CET ]]
Run set sv-comp16.Simple
Options -sv-comp16-bam -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-bam.2016-01-04_0625.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-bam.2016-01-04_0625.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   750   4800 wit - -
ntdrivers/diskperf_false-unreach-call.i.cil.c timeout 900   790   4400 wit - -
ntdrivers/floppy_false-unreach-call.i.cil.c witness timeout 52   27   1400 wit timeout 91 72   1700 true 33 20   540
ntdrivers/kbfiltr_false-unreach-call.i.cil.c false(reach) 23   5.7 790 wit false(reach) 25 14   640 true 18 12   400
ntdrivers/parport_false-unreach-call.i.cil.c timeout 900   670   6100 wit - -
ntdrivers/cdaudio_true-unreach-call.i.cil.c timeout 900   730   5000 wit - -
ntdrivers/diskperf_true-unreach-call.i.cil.c timeout 900   790   4400 wit - -
ntdrivers/floppy2_true-unreach-call.i.cil.c timeout 900   790   4400 wit - -
ntdrivers/floppy_true-unreach-call.i.cil.c timeout 910   710   6000 wit - -
ntdrivers/parport_true-unreach-call.i.cil.c timeout 900   660   6000 wit - -
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c false(reach) 26   7.2 840 wit false(reach) 15 7.9 500 true 16 12   350
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c false(reach) 15   5.0 650 wit false(reach) 13 6.9 460 true 16 12   340
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c false(reach) 17   5.7 650 wit false(reach) 14 7.4 530 timeout 91 81   550
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c false(reach) 15   5.1 650 wit false(reach) 16 8.5 520 timeout 91 81   410
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c false(reach) 10   3.3 500 wit false(reach) 14 7.6 480 true 18 9.9 370
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c false(reach) 12   3.9 490 wit false(reach) 15 7.9 490 unknown 56 37   450
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c false(reach) 12   4.0 480 wit false(reach) 13 7.2 480 true 16 9.3 340
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c false(reach) 9.6 3.2 490 wit false(reach) 13 7.0 490 unknown 56 38   530
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c false(reach) 21   7.6 760 wit false(reach) 14 7.3 470 true 16 9.3 330
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c false(reach) 20   6.1 760 wit false(reach) 15 8.3 480 unknown 77 56   540
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c false(reach) 29   11   890 wit false(reach) 12 6.7 460 true 16 11   340
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c false(reach) 19   6.1 740 wit false(reach) 14 7.4 520 unknown 64 47   520
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c false(reach) 33   15   870 wit false(reach) 22 11   590 true 18 9.7 340
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c false(reach) 12   4.0 550 wit false(reach) 14 7.7 490 unknown 72 55   460
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c false(reach) 25   10   760 wit false(reach) 14 7.7 490 true 17 9.9 340
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c false(reach) 25   7.1 810 wit false(reach) 16 8.7 490 unknown 64 46   550
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c false(reach) 23   7.9 750 wit false(reach) 16 8.6 490 true 17 9.7 330
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c false(reach) 29   12   910 wit false(reach) 13 7.2 460 true 16 9.5 350
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c false(reach) 24   8.5 780 wit false(reach) 12 6.6 450 true 17 9.5 340
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c true 210   180   1100 wit - -
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c true 160   130   990 wit - -
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c true 89   59   1100 wit - -
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c true 90   66   970 wit - -
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c true 38   16   880 wit - -
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c true 64   34   1100 wit - -
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c true 140   91   1400 wit - -
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c true 150   100   1200 wit - -
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c true 120   75   1300 wit - -
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c true 120   71   1200 wit - -
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c true 70   32   1000 wit - -
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c true 100   71   1500 wit - -
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c true 120   75   1700 wit - -
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c true 110   66   1200 wit - -
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c true 95   60   1100 wit - -
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c true 200   150   1500 wit - -
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c true 190   140   1900 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 9700 7500 78000 46 390   230   12000   46 810   590   8700  
    correct results 37 2500 1500 35000 20 300   160   10000   12 770   570   8200  
        correct true 17 2100 1400 21000 0 0   0   0   12 0   0   0  
        correct false 20 400 140 14000 20 300   160   10000   0 770   570   8200  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (46 tasks, max score: 68) 54
Run set sv-comp16.Simple