Tool ESBMC ESBMC version 3.1 64-bit x86_64 linux
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-11 15:09:43 CET [[ 2017-01-14 22:26:56 CET ]] [[ 2017-01-14 23:59:25 CET ]] [[ 2017-01-14 22:42:14 CET ]] [[ 2017-01-15 00:15:34 CET ]]
Run set sv-comp17.ReachSafety-ControlFlow
Options -s falsi [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 .52  .52  6.2  49 .84 0   7.8  4.2  170 300 11   6.2 140 420
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 .20  .20  2.5  28 .84 0   7.6  4.0  92 320 9.4 5.0 160 330
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 .35  .35  3.5  32 .84 0   7.9  4.2  72 310 9.6 5.2 110 370
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 .18  .17  2.3  27 .84 0   8.6  4.6  93 350 10   5.4 210 330
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 0 900     900     10000    15000 .84 0   .53 .34 12   42 6.6 3.5 130 300
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 0 900     890     9300    8600 .84 0   .52 .33 12   41 5.5 3.0 100 290
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c 0 670     660     9100    15000 .84 0   .51 .33 9.5 42 5.9 3.1 120 290
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c 0 700     700     11000    15000 .84 0   .54 .36 6.7 41 6.2 3.3 130 300
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 0 370     370     4700    15000 .84 0   .49 .31 8.7 39 6.2 3.2 120 300
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c 0 490     490     6100    15000 .84 0   .50 .32 11   39 5.8 3.1 120 290
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c 1 1.6   1.6   18    73 .84 0   7.8  4.2  100 300 9.9 5.3 140 320
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c 1 1.7   1.6   20    74 .84 0   7.2  3.8  140 310 11   5.7 130 320
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c 1 2.0   2.0   22    85 .84 0   7.0  3.8  73 320 9.3 4.9 150 330
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c 1 1.6   1.6   20    74 .84 0   7.4  3.9  150 300 11   5.8 98 330
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c 1 .12  .12  1.1  26 .84 0   6.1  3.3  89 290 8.5 4.6 170 330
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c 1 3.0   3.0   45    110 .84 0   7.7  4.1  140 310 9.0 4.8 120 330
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c 1 2.5   2.5   29    94 .89 0   11    5.7  200 440 8.7 4.7 140 320
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c 1 .82  .81  11    50 .84 0   9.0  4.8  100 300 9.3 4.9 150 330
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c 1 .19  .19  2.3  26 .84 0   8.0  4.3  86 290 8.4 4.5 86 320
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c 1 .74  .74  9.1  48 .84 0   7.9  4.2  140 310 10   5.3 120 320
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c 1 .74  .73  9.9  46 .84 0   6.4  3.5  74 300 12   6.3 150 330
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c 1 .099 .099 1.1  26 .84 0   5.4  2.9  84 290 9.2 4.9 160 330
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c 0 900     900     12000    5100 .84 0   .50 .33 8.5 39 5.9 3.1 120 290
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c 0 900     900     11000    5300 .84 0   .54 .36 8.9 40 6.2 3.3 130 300
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c 0 900     900     11000    5200 .84 0   .51 .33 12   40 6.4 3.4 120 310
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c 0 900     900     11000    5200 .84 0   .47 .31 6.4 39 6.5 3.4 140 310
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c 0 900     900     11000    4400 .84 0   .51 .33 13   41 6.4 3.4 140 300
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c 0 900     900     12000    7800 .84 0   .52 .34 11   39 5.9 3.1 120 300
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c 0 620     610     7900    15000 .84 0   .51 .32 10   42 5.8 3.1 110 300
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c 0 900     900     12000    4100 .84 0   .50 .35 5.2 40 6.1 3.2 100 300
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c 0 900     900     9700    4200 .84 0   .51 .33 10   40 5.5 3.0 130 290
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c 0 900     900     10000    4200 .84 0   .54 .35 12   40 6.1 3.3 120 300
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c 0 900     900     11000    3900 .84 0   .48 .31 12   39 6.0 3.2 99 290
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c 0 900     900     10000    4000 .84 0   .53 .34 11   40 6.8 3.6 100 320
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c 0 900     900     8400    4000 .84 0   .52 .33 12   39 6.4 3.3 130 300
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c 1 .13  .13  .81 24 .84 0   5.2  2.8  100 280 11   5.7 130 330
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c 1 .090 .090 1.3  24 .84 0   5.2  2.8  110 290 9.5 5.0 110 310
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c 0 660     660     7200    15000 .84 0   .53 .33 7.7 40 6.1 3.2 110 310
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c 0 680     680     8100    15000 .84 0   .57 .36 10   41 6.0 3.2 85 300
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c 0 690     690     9200    15000 .84 0   .51 .32 9.5 39 5.8 3.0 97 300
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c 0 730     730     8400    15000 .84 0   .52 .33 9.6 40 5.5 2.9 82 300
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c 0 730     730     8700    15000 .84 0   .51 .33 12   41 6.0 3.2 130 290
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c 0 750     750     8200    15000 .84 0   .50 .34 4.5 42 5.4 2.9 120 290
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c 0 520     520     6100    15000 .84 0   .53 .35 4.1 41 5.9 3.1 110 300
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c 0 560     560     7100    15000 .84 0   .56 .37 13   42 5.5 3.0 80 300
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c 0 590     590     6900    15000 .84 0   .54 .36 5.6 39 6.1 3.2 120 290
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c 0 620     620     7900    15000 .84 0   .50 .33 10   40 6.6 3.5 130 300
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c 0 640     640     7500    15000 .84 0   .52 .34 12   41 6.1 3.2 110 310
ntdrivers/cdaudio_false-unreach-call.i.cil.c 0 900     900     12000    380 .84 0   .57 .37 11 41 8.7 4.6 100 330
ntdrivers/diskperf_false-unreach-call.i.cil.c 0 .94  .94  11    92 .84 0   97    82    1700 2900 12   6.6 180 440
ntdrivers/floppy_false-unreach-call.i.cil.c 0 5.7   5.7   70    360 .84 0   44    28    500 1400 21   12   290 550
ntdrivers/kbfiltr_false-unreach-call.i.cil.c 1 54     54     700    490 .84 0   14    7.7  200 480 12   6.5 170 420
ntdrivers/parport_false-unreach-call.i.cil.c 0 11     11     110    430 .84 0   97    66    1200 3800 24   14   300 610
ntdrivers/cdaudio_true-unreach-call.i.cil.c 0 20     20     260    380 .84 0   .48 .32 9.2 40 7.3 3.8 140 310
ntdrivers/diskperf_true-unreach-call.i.cil.c 0 900     900     7600    5000 .84 0   .49 .31 8.1 40 6.6 3.5 130 290
ntdrivers/floppy2_true-unreach-call.i.cil.c 0 900     900     8700    5600 .84 0   .52 .32 9.0 39 8.0 4.2 150 310
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c 0 900     900     12000    5400 .84 0   .51 .33 13   40 6.0 3.2 120 290
ntdrivers/parport_true-unreach-call.i.cil.c 0 900     900     9800    14000 .84 0   .50 .34 8.1 40 6.8 3.6 130 300
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c 1 600     610     6600    2600 .84 0   16    8.3  170 480 10   5.6 210 350
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c 1 360     360     3500    2100 .84 0   12    6.3  240 470 11   6.0 170 360
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c 1 400     400     4500    2100 .84 0   13    7.3  180 470 14   7.3 140 360
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c 1 460     460     4800    2200 .84 0   14    7.5  190 470 10   5.5 180 350
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c 1 190     190     1800    1200 .84 0   12    6.3  130 380 11   6.1 150 370
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c 1 120     120     1000    1200 .84 0   11    5.8  140 390 10   5.5 160 360
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c 1 210     210     2400    1200 .84 0   12    6.1  120 400 12   6.3 120 370
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c 1 120     120     1300    1200 .84 0   10    5.5  160 400 11   5.7 170 360
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c 1 450     450     4600    2600 .84 0   13    6.9  160 460 12   6.3 130 380
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c 1 350     350     3200    2300 .84 0   12    6.4  120 450 10   5.6 95 360
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c 0 900     900     10000    3800 .84 0   .53 .34 13 41 6.6 3.5 84 300
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c 1 270     270     2500    2400 .84 0   12    6.3  160 450 11   5.7 170 360
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c 0 900     900     9400    4300 .84 0   .51 .33 11 40 6.9 3.6 120 320
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c 1 180     180     2000    1700 .84 0   11    5.9  200 460 9.8 5.3 160 350
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c 1 390     390     3200    2600 .84 0   13    7.1  130 460 9.6 5.1 120 350
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c 1 290     290     2400    2400 .84 0   10    5.6  180 450 11   6.2 140 360
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c 1 420     420     3200    2600 .84 0   12    6.5  120 460 11   5.9 140 370
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c 0 900     900     7000    3800 .84 0   .51 .32 12 39 6.6 3.5 110 300
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c 1 410     410     3900    2600 .84 0   10    5.5  160 460 10   5.5 140 360
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c 0 900     900     8300    4800 .84 0   .55 .34 12   41 6.3 3.3 120 300
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c 0 900     900     7600    4100 .84 0   .53 .33 10   43 6.2 3.3 130 290
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c 0 900     900     10000    4100 .84 0   .51 .33 7.3 42 6.5 3.4 140 300
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c 0 900     900     8200    4100 .84 0   .52 .34 9.9 40 6.6 3.5 120 310
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c 0 900     900     8100    5700 .84 0   .51 .33 10   42 6.2 3.3 110 300
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c 0 900     900     7800    5800 .84 0   .59 .39 12   43 6.2 3.3 120 290
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c 0 900     900     8400    4600 .84 0   .52 .34 12   42 5.8 3.1 110 300
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c 0 900     900     6500    5000 .84 0   .50 .32 9.2 39 7.0 3.7 140 330
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c 0 900     900     8300    5400 .84 0   .54 .34 4.9 43 6.3 3.4 130 300
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c 0 900     900     10000    5200 .84 0   .52 .33 11   40 6.5 3.4 120 300
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c 0 900     900     7700    5600 .84 0   .53 .33 11   40 6.4 3.4 130 310
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c 0 900     900     8200    5000 .84 0   .51 .33 12   40 6.7 3.6 140 300
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c 0 900     900     7900    4700 .84 0   .52 .33 11   41 6.3 3.4 130 300
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c 0 900     900     8200    5000 .84 0   .50 .32 12   40 6.4 3.4 130 310
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c 0 900     900     7500    4500 .84 0   .65 .43 7.3 41 6.1 3.3 110 300
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c 0 900     900     7200    5500 .84 0   .50 .33 5.5 40 6.3 3.4 130 300
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c 0 900     900     7300    4600 .84 0   .48 .31 6.9 40 6.1 3.3 100 300
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
total 94 35 50000 50000 540000 480000 79   0   94 580 360 8200 21000 94 450 240 6300 15000 94 27 17 500 2100   94 320 170 6200 16000  
    correct results 35 35 5300 5300 52000 34000 29   0   35 340 180 4700 13000 35 360 190 5100 12000 0 0 0 0 0   0 0 0 0 0  
        correct true 0
        correct false 35 35 5300 5300 52000 34000 29   0   35 340 180 4700 13000 1 360 190 5100 12000 0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 3 0 17 17 190 880 2.5 0   1 240 180 3400 8100 3 57 32 770 1600 0 0 0 0 0   0 0 0 0 0  
        correct-unconfirmed true 0
        correct-unconfirmed false 3 0 17 17 190 880 2.5 0   0 240 180 3400 8100 0 57 32 770 1600 0 0 0 0 0   0 0 0 0 0  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (94 tasks, max score: 146) 35
Run set sv-comp17.ReachSafety-ControlFlow