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 01:42:53 CET [[ 2016-01-15 08:36:34 CET ]] [[ 2016-01-15 22:02:40 CET ]]
Run set sv-comp16.Simple
Options -sv-comp16--k-induction -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-kind.2016-01-04_0142.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-kind.2016-01-04_0142.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 400   5400 wit - -
ntdrivers/diskperf_false-unreach-call.i.cil.c witness timeout 63 19   1400 wit timeout 90 79 1500 true 26 15 510
ntdrivers/floppy_false-unreach-call.i.cil.c witness unconfirmed 130 52   3100 wit true 64 40 3000 timeout 90 72 2600
ntdrivers/kbfiltr_false-unreach-call.i.cil.c timeout 900 890   4100 wit - -
ntdrivers/parport_false-unreach-call.i.cil.c witness timeout 140 64   2100 wit timeout 91 58 2400 true 52 29 750
ntdrivers/cdaudio_true-unreach-call.i.cil.c true 270 100   4400 wit - -
ntdrivers/diskperf_true-unreach-call.i.cil.c true 46 8.6 1400 wit - -
ntdrivers/floppy2_true-unreach-call.i.cil.c timeout 900 360   8100 wit - -
ntdrivers/floppy_true-unreach-call.i.cil.c timeout 900 370   7100 wit - -
ntdrivers/parport_true-unreach-call.i.cil.c timeout 900 340   7800 wit - -
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c out of memory 110 62   15000 wit - -
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c out of memory 100 60   15000 wit - -
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c out of memory 100 60   15000 wit - -
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c out of memory 100 61   15000 wit - -
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c out of memory 89 58   15000 wit - -
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c out of memory 87 56   15000 wit - -
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c out of memory 89 58   15000 wit - -
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c out of memory 88 57   15000 wit - -
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c out of memory 110 61   15000 wit - -
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c out of memory 100 61   15000 wit - -
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c out of memory 140 80   15000 wit - -
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c out of memory 100 60   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 99 60   15000 wit - -
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c out of memory 100 60   15000 wit - -
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c out of memory 100 63   15000 wit - -
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c out of memory 100 63   15000 wit - -
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c out of memory 140 80   15000 wit - -
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c out of memory 100 63   15000 wit - -
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c true 48 9.5 1200 wit - -
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c true 52 10   1300 wit - -
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c true 51 10   1200 wit - -
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c true 48 9.5 1200 wit - -
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c true 68 14   1200 wit - -
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c true 41 7.3 950 wit - -
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c true 160 55   3800 wit - -
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c true 150 57   3800 wit - -
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c true 57 12   1200 wit - -
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c true 150 54   3400 wit - -
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c true 57 11   1200 wit - -
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c true 140 50   3400 wit - -
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c true 130 46   3100 wit - -
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c true 64 14   1500 wit - -
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c true 140 50   3600 wit - -
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c true 100 32   2200 wit - -
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c true 150 52   3800 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 8800 4300 370000 46 240   180   6900   46 170   120   3800  
    correct results 19 1900 610 44000 0 0   0   0   0 0   0   0  
        correct true 19 1900 610 44000 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) 38
Run set sv-comp16.Simple