Tool 2LS 0.3.4
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-02 22:42:27 CET [[ 2016-01-15 08:01:51 CET ]] [[ 2016-01-15 21:37:22 CET ]]
Run set sv-comp16.Simple
Options --k-induction --competition-mode --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/2ls.2016-01-02_2242.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/2ls.2016-01-02_2242.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    900    2800 wit - -
ntdrivers/diskperf_false-unreach-call.i.cil.c witness timeout 3.3  3.3  780 wit timeout 90 72   1900 unknown 25 14   530
ntdrivers/floppy_false-unreach-call.i.cil.c witness unconfirmed 12    12    2100 wit true 40 23   910 true 33 19   540
ntdrivers/kbfiltr_false-unreach-call.i.cil.c true 110    110    630 wit - -
ntdrivers/parport_false-unreach-call.i.cil.c error (6) .84 .84 66 wit - -
ntdrivers/cdaudio_true-unreach-call.i.cil.c true 63    63    1400 wit - -
ntdrivers/diskperf_true-unreach-call.i.cil.c true 3.4  3.4  780 wit - -
ntdrivers/floppy2_true-unreach-call.i.cil.c error (6) 4.7  4.6  470 wit - -
ntdrivers/floppy_true-unreach-call.i.cil.c error (8) 7.7  7.7  1900 wit - -
ntdrivers/parport_true-unreach-call.i.cil.c error (6) .84 .84 66 wit - -
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c witness unconfirmed 590    590    1200 wit true 16 8.3 470 true 21 12   500
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c witness unconfirmed 410    410    910 wit true 15 8.1 460 true 21 12   450
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c witness unconfirmed 320    320    910 wit true 16 8.7 510 true 14 8.0 340
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c witness unconfirmed 420    420    910 wit true 16 8.3 480 true 17 10   350
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c witness unconfirmed 540    540    1100 wit true 12 6.7 440 unknown 79 61   530
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c witness unconfirmed 450    450    1000 wit true 12 6.6 440 unknown 53 34   520
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c witness unconfirmed 450    450    1000 wit true 11 6.2 430 unknown 62 41   550
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c witness unconfirmed 450    450    1000 wit true 12 6.5 440 unknown 60 41   530
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c timeout 900    900    1300 wit - -
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c timeout 900    900    1300 wit - -
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c timeout 900    900    1300 wit - -
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c timeout 900    900    1300 wit - -
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c timeout 900    900    1300 wit - -
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c witness unconfirmed 810    810    1300 wit true 12 6.7 440 true 21 12   480
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c timeout 900    900    1300 wit - -
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c timeout 900    900    1400 wit - -
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c timeout 900    900    1300 wit - -
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c timeout 900    900    1300 wit - -
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c timeout 900    900    1400 wit - -
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c true 880    880    1400 wit - -
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c true 740    740    1300 wit - -
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c true 700    710    1300 wit - -
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c true 700    700    1300 wit - -
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c timeout 900    900    1400 wit - -
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c timeout 900    900    1300 wit - -
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c timeout 900    900    1200 wit - -
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c timeout 900    900    1400 wit - -
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c timeout 900    900    1300 wit - -
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c timeout 900    900    1300 wit - -
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c timeout 900    900    1400 wit - -
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c timeout 900    900    1300 wit - -
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c timeout 900    900    1300 wit - -
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c timeout 900    900    1300 wit - -
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c timeout 900    900    1300 wit - -
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c timeout 900    900    1300 wit - -
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c timeout 900    900    1200 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 29000 29000 56000 46 250   160   7000   46 410   260   5300  
    correct results 6 3100 3100 7600 0 0   0   0   0 0   0   0  
        correct true 6 3100 3100 7600 0 0   0   0   0 0   0   0  
        correct false 0
    incorrect results 1 110 110 630 0 0   0   0   0 0   0   0  
        incorrect true 1 110 110 630 0 0   0   0   0 0   0   0  
        incorrect false 0
score (46 tasks, max score: 68) -20
Run set sv-comp16.Simple