Tool CPAchecker 1.4-svn 18373
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 20:04:07 CET [[ 2016-01-15 08:41:31 CET ]] [[ 2016-01-15 22:05:37 CET ]]
Run set sv-comp16.Simple
Options -sv-comp16--refsel -disable-java-assertions -heap 12500m -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-refsel.2016-01-04_2004.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-refsel.2016-01-04_2004.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 900 860 3200
ntdrivers/diskperf_false-unreach-call.i.cil.c 170 150 1200 73 60   3800 28 17 530
ntdrivers/floppy_false-unreach-call.i.cil.c 900 890 930
ntdrivers/kbfiltr_false-unreach-call.i.cil.c 51 30 860 16 8.6 540 20 11 420
ntdrivers/parport_false-unreach-call.i.cil.c 520 480 1900 25 13   800 91 69 830
ntdrivers/cdaudio_true-unreach-call.i.cil.c 450 420 1200
ntdrivers/diskperf_true-unreach-call.i.cil.c 360 340 950
ntdrivers/floppy2_true-unreach-call.i.cil.c 200 160 2500
ntdrivers/floppy_true-unreach-call.i.cil.c 900 890 940
ntdrivers/parport_true-unreach-call.i.cil.c 900 850 1900
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c 900 850 1300
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c 900 850 1300
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c 900 860 1300
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c 900 860 1300
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c 270 240 870 14 7.5 480 49 32 520
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c 150 120 830 14 7.4 480 60 39 520
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c 150 120 870 11 6.2 480 57 40 420
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c 190 160 860 12 6.7 460 55 36 530
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c 100 79 820 15 7.9 490 86 63 540
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c 900 860 1300
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c 900 860 1500
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c 900 860 1100
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c 900 860 1300
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c 900 860 1200
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c 94 68 850 17 8.9 510 79 58 540
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c 900 860 1500
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c 110 79 850 15 8.1 510 72 54 530
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c 900 860 1300
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c 100 78 860 14 7.6 500 82 61 540
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c 900 870 1100
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c 900 860 920
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c 900 860 1100
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c 900 850 1400
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c 900 860 1200
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c 900 860 1000
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c 900 860 1300
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c 900 870 880
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c 900 870 1400
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c 900 860 1200
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c 900 870 1200
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c 900 860 1000
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c 900 870 1400
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c 900 860 1300
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c 900 860 1300
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c 900 870 1200
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c 900 860 1400
../../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 32000 30000 57000 46 230   140   9000   46 680   480   5900  
    correct results 14 2900 2500 15000 11 230   140   9000   2 680   480   5900  
        correct true 3 1000 920 4700 0 0   0   0   2 0   0   0  
        correct false 11 1900 1600 11000 11 230   140   9000   0 680   480   5900  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (46 tasks, max score: 68) 17
Run set sv-comp16.Simple