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 13:17:38 CET [[ 2016-01-15 08:48:20 CET ]] [[ 2016-01-15 22:10:37 CET ]]
Run set sv-comp16.Simple
Options -sv-comp16 -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-seq.2016-01-04_1317.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-seq.2016-01-04_1317.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 670   5000 wit - -
ntdrivers/diskperf_false-unreach-call.i.cil.c false(reach) 120 97   3900 wit false(reach) 85 71   4000 true 27 15 530
ntdrivers/floppy_false-unreach-call.i.cil.c false(reach) 25 9.7 860 wit false(reach) 37 24   890 timeout 90 72 2600
ntdrivers/kbfiltr_false-unreach-call.i.cil.c false(reach) 15 4.5 540 wit false(reach) 18 9.8 590 true 19 14 400
ntdrivers/parport_false-unreach-call.i.cil.c false(reach) 130 92   4600 wit false(reach) 26 14   800 timeout 91 68 790
ntdrivers/cdaudio_true-unreach-call.i.cil.c true 14 3.9 490 wit - -
ntdrivers/diskperf_true-unreach-call.i.cil.c true 110 86   3600 wit - -
ntdrivers/floppy2_true-unreach-call.i.cil.c true 440 200   5800 wit - -
ntdrivers/floppy_true-unreach-call.i.cil.c true 460 250   5500 wit - -
ntdrivers/parport_true-unreach-call.i.cil.c true 820 580   5600 wit - -
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c out of memory 200 130   15000 wit - -
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c out of memory 200 130   15000 wit - -
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c out of memory 210 130   15000 wit - -
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c out of memory 200 140   15000 wit - -
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c out of memory 190 130   15000 wit - -
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c out of memory 190 130   15000 wit - -
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c out of memory 190 130   15000 wit - -
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c out of memory 190 130   15000 wit - -
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c out of memory 100 62   15000 wit - -
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c out of memory 210 140   15000 wit - -
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c out of memory 130 81   15000 wit - -
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c out of memory 210 140   15000 wit - -
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c out of memory 140 80   15000 wit - -
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c out of memory 190 130   15000 wit - -
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c out of memory 110 64   15000 wit - -
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c out of memory 200 130   15000 wit - -
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c out of memory 100 61   15000 wit - -
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c out of memory 130 80   15000 wit - -
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c out of memory 100 62   15000 wit - -
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c true 150 82   1300 wit - -
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c true 150 81   970 wit - -
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c true 150 81   990 wit - -
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c true 150 80   1200 wit - -
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c true 160 86   970 wit - -
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c true 140 82   780 wit - -
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c true 400 200   4800 wit - -
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c true 250 130   2900 wit - -
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c true 160 85   1200 wit - -
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c true 250 120   2300 wit - -
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c true 160 80   1500 wit - -
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c true 240 120   2800 wit - -
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c true 390 190   4700 wit - -
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c true 170 87   1700 wit - -
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c true 250 120   4300 wit - -
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c true 200 100   2000 wit - -
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c true 250 120   4400 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 9900 5900 360000 46 170   120   6200   46 230   170   4300  
    correct results 26 5800 3200 70000 4 170   120   6200   2 230   170   4300  
        correct true 22 5500 3000 60000 0 0   0   0   2 0   0   0  
        correct false 4 300 200 9900 4 170   120   6200   0 230   170   4300  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (46 tasks, max score: 68) 48
Run set sv-comp16.Simple