Tool SeaHorn-F16 0.1.0
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-23-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-11 21:35:00 [[ 2016-01-15 18:20:27 CET ]] [[ 2016-01-15 22:30:28 CET ]]
Run set sv-comp16.ControlFlow
Options --cex=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/seahorn.2016-01-11_2135.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/seahorn.2016-01-11_2135.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 1.2  .65 88 21   12   800 16 8.9 380
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-termination.cil.c .54 .29 45 19   10   600 15 9.7 360
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-termination.cil.c .73 .39 53 21   12   630 16 9.8 350
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-termination.cil.c .49 .27 44 18   9.8 580 14 7.7 360
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c 1.3  .66 91
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-termination.cil.c .71 .39 56
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-termination.cil.c .51 .29 41
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-termination.cil.c .68 .38 52
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-termination.cil.c .32 .18 34
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-termination.cil.c .44 .24 37
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c 2.3  1.2  77 19   10   610 11 6.6 330
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c 2.6  1.3  76 13   7.2 490 14 9.4 330
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c 2.4  1.2  76 13   6.9 480 13 7.4 340
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c 2.4  1.2  75 17   8.9 570 13 7.8 340
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c .69 .37 78 14   7.3 500 13 7.4 340
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c 5.0  2.5  79 90   70   1900 12 7.4 330
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c 7.5  3.8  140 91   73   3100 14 8.2 330
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c 6.2  3.2  150 19   10   600 14 10   340
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c .72 .39 65 91   75   1400 13 8.4 340
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c .90 .48 63 14   7.5 480 13 7.1 330
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c .80 .42 62 15   7.9 480 15 8.2 360
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c .43 .25 34 90   73   3800 14 9.1 360
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c 23    12    82
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c 92    46    110
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c 82    41    110
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c 18    8.9  76
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c 7.5  3.8  70
ssh-simplified/s3_srvr_1a_true-unreach-call.cil.c 1.4  .74 57
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c .69 .37 52
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c 73    37    84
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c 160    81    91
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c 10    5.0  61
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c 900    450    170
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c 130    64    87
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c 4.8  2.4  65
locks/test_locks_14_false-unreach-call.c .30 .18 37 8.6 4.8 360 12 9.3 330
locks/test_locks_15_false-unreach-call.c .40 .24 37 8.9 4.9 400 11 6.5 330
locks/test_locks_10_true-unreach-call.c .23 .14 24
locks/test_locks_11_true-unreach-call_false-termination.c .21 .13 24
locks/test_locks_12_true-unreach-call_false-termination.c .23 .13 25
locks/test_locks_13_true-unreach-call.c .18 .11 24
locks/test_locks_14_true-unreach-call.c .21 .12 25
locks/test_locks_15_true-unreach-call_false-termination.c .22 .14 25
locks/test_locks_5_true-unreach-call_false-termination.c .22 .13 25
locks/test_locks_6_true-unreach-call_false-termination.c .26 .16 24
locks/test_locks_7_true-unreach-call_false-termination.c .21 .13 25
locks/test_locks_8_true-unreach-call_false-termination.c .21 .13 24
locks/test_locks_9_true-unreach-call.c .23 .13 25
../../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 1500 770 3000 48 580   410   18000   48 240   150   6200  
    correct results 43 630 320 2500 14 220   120   7600   14 190   120   4800  
        correct true 29 610 300 1500 0 0   0   0   14 0   0   0  
        correct false 14 22 11 960 14 220   120   7600   0 190   120   4800  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (48 tasks, max score: 78) 72
Run set sv-comp16.ControlFlow