Tool CPAchecker 1.4-svn 18356M
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-10 22:01:17 CET [[ 2016-01-15 09:16:15 CET ]] [[ 2016-01-15 22:26:01 CET ]]
Run set sv-comp16.Simple
Options -lpi-svcomp16 -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/lpi.2016-01-10_2201.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/lpi.2016-01-10_2201.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 360   7000
ntdrivers/diskperf_false-unreach-call.i.cil.c 31 13   580 91 71 2100 23 13 380
ntdrivers/floppy_false-unreach-call.i.cil.c 58 25   1000 49 30 1200 91 64 2500
ntdrivers/kbfiltr_false-unreach-call.i.cil.c 900 890   4000
ntdrivers/parport_false-unreach-call.i.cil.c 100 56   1200 90 60 2500 53 29 800
ntdrivers/cdaudio_true-unreach-call.i.cil.c 87 19   1400
ntdrivers/diskperf_true-unreach-call.i.cil.c 65 13   1500
ntdrivers/floppy2_true-unreach-call.i.cil.c 530 170   7500
ntdrivers/floppy_true-unreach-call.i.cil.c 170 60   3700
ntdrivers/parport_true-unreach-call.i.cil.c 52 9.5 910
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c 93 58   15000
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c 28 5.4 570
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c 82 56   15000
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c 83 57   15000
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c 72 55   15000
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c 73 56   15000
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c 72 55   15000
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c 75 56   15000
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c 86 60   15000
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c 86 60   15000
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c 110 75   15000
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c 88 60   15000
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c 120 75   15000
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c 81 58   15000
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c 88 60   15000
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c 87 60   15000
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c 31 6.2 700
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c 120 76   15000
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c 86 61   15000
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c 47 8.1 880
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c 39 7.0 840
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c 39 7.1 810
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c 36 6.6 810
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c 900 410   4100
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c 900 410   5000
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c 900 410   4400
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c 900 390   5500
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c 900 390   5400
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c 900 400   5100
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c 900 400   5100
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c 900 400   5200
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c 900 400   5200
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c 900 400   5000
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c 900 400   4800
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c 900 400   5100
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c 900 410   4400
../../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 16000 7900 350000 46 230   160   5800   46 170   110   3700  
    correct results 7 970 280 17000 0 0   0   0   0 0   0   0  
        correct true 7 970 280 17000 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) 14
Run set sv-comp16.Simple