Tool BLAST 2.7.3
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-03 17:36:26 CET [[ 2016-01-15 08:15:11 CET ]] [[ 2016-01-15 21:49:51 CET ]]
Run set sv-comp16.ControlFlow
Options -alias empty -enable-recursion -noprofile -cref -sv-comp -lattice -include-lattice symb -nosserr -svcomp-witness error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/blast.2016-01-03_1736.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/blast.2016-01-03_1736.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-simplified/cdaudio_simpl1_false-unreach-call_true-termination.cil.c false(reach) 120     160     86 wit false(reach) 12   6.6 540 false(reach) 26 14   520
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-termination.cil.c false(reach) 20     25     50 wit false(reach) 13   7.0 480 false(reach) 21 11   470
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-termination.cil.c false(reach) 19     24     55 wit false(reach) 13   7.3 520 false(reach) 25 14   550
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-termination.cil.c false(reach) 5.8   7.4   54 wit false(reach) 13   7.2 490 false(reach) 18 11   430
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c true 430     620     210 wit - -
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-termination.cil.c true 120     170     100 wit - -
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-termination.cil.c true 140     200     120 wit - -
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-termination.cil.c true 240     340     210 wit - -
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-termination.cil.c true 1.6   2.1   31 wit - -
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-termination.cil.c true 1.7   2.2   34 wit - -
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c false(reach) 12     16     45 wit true 26   14   960 false(reach) 20 11   470
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(reach) 15     20     43 wit true 25   14   950 false(reach) 20 12   490
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c witness unconfirmed 14     19     45 wit true 29   16   1100 unknown 18 10   430
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c false(reach) 14     19     45 wit true 26   14   940 false(reach) 19 11   470
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c false(reach) .19  .19  26 wit false(reach) 9.9 5.5 410 false(reach) 18 9.9 380
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c exception (gremlins) 1.6   2.2   29 wit - -
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c exception (gremlins) 1.8   2.4   29 wit - -
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c exception (gremlins) 1.7   2.2   28 wit - -
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c exception (gremlins) 2.8   3.7   29 wit - -
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c false(reach) 2.9   3.6   40 wit false(reach) 10   5.5 420 false(reach) 20 11   500
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c false(reach) 2.2   2.9   42 wit true 23   13   910 false(reach) 19 10   500
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c false(reach) .11  .12  26 wit true 29   16   940 false(reach) 17 9.9 350
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c true 79     110     64 wit - -
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c timeout 650     930     190 wit - -
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c true 180     260     68 wit - -
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c timeout 660     930     190 wit - -
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c timeout 650     930     250 wit - -
ssh-simplified/s3_srvr_1a_true-unreach-call.cil.c true .63  .79  27 wit - -
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c true .89  1.1   26 wit - -
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c true 210     300     81 wit - -
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c true 220     320     84 wit - -
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c true 220     320     90 wit - -
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c timeout 650     930     220 wit - -
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c timeout 650     930     180 wit - -
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c true 110     160     58 wit - -
locks/test_locks_14_false-unreach-call.c false(reach) .096 .097 24 wit false(reach) 8.7 4.8 370 false(reach) 14 7.7 350
locks/test_locks_15_false-unreach-call.c false(reach) .12  .13  26 wit false(reach) 9.2 5.0 390 false(reach) 17 9.1 350
locks/test_locks_10_true-unreach-call.c timeout 730     930     430 wit - -
locks/test_locks_11_true-unreach-call_false-termination.c timeout 760     930     440 wit - -
locks/test_locks_12_true-unreach-call_false-termination.c timeout 790     930     410 wit - -
locks/test_locks_13_true-unreach-call.c timeout 780     930     400 wit - -
locks/test_locks_14_true-unreach-call.c timeout 780     930     410 wit - -
locks/test_locks_15_true-unreach-call_false-termination.c timeout 810     930     410 wit - -
locks/test_locks_5_true-unreach-call_false-termination.c true 15     18     41 wit - -
locks/test_locks_6_true-unreach-call_false-termination.c true 30     37     47 wit - -
locks/test_locks_7_true-unreach-call_false-termination.c true 86     110     73 wit - -
locks/test_locks_8_true-unreach-call_false-termination.c true 170     220     190 wit - -
locks/test_locks_9_true-unreach-call.c true 410     520     230 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 48 11000 14000 6000 48 250   140   9400   48 270   150   6300  
    correct results 32 2900 4000 2300 13 220   120   8300   13 250   140   5800  
        correct true 19 2700 3700 1800 5 0   0   0   0 0   0   0  
        correct false 13 210 280 560 8 220   120   8300   13 250   140   5800  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (48 tasks, max score: 78) 51
Run set sv-comp16.ControlFlow