Tool Forest svc_16_20151108
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]
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-09 23:49:59 CET [[ 2016-01-15 09:05:13 CET ]] [[ 2016-01-15 22:20:31 CET ]]
Run set sv-comp16.ControlFlow
Options -svcomp [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/forest.2016-01-09_2349.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/forest.2016-01-09_2349.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 true .54  .66 8.9 wit - -
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-termination.cil.c unknown .96  1.1  36   wit - -
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-termination.cil.c true .97  1.1  18   wit - -
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-termination.cil.c unknown .80  .89 39   wit - -
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c true 3.1   3.5  43   wit - -
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-termination.cil.c true 3.8   4.3  41   wit - -
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-termination.cil.c true .71  .81 13   wit - -
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-termination.cil.c unknown 1.1   1.2  41   wit - -
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-termination.cil.c unknown .73  .83 39   wit - -
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-termination.cil.c true .93  1.0  40   wit - -
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c unknown .22  .30 7.6 wit - -
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c true 1.0   1.2  39   wit - -
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c true .87  .98 39   wit - -
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c true 3.3   3.7  40   wit - -
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c true 1.4   1.7  40   wit - -
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c true .92  1.0  39   wit - -
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c unknown .90  .99 40   wit - -
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c error (139) 7.6   8.4  40   wit - -
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c true 1.6   1.8  40   wit - -
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c true .87  .98 39   wit - -
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c false(reach) 240     260    66   wit false(reach) 12   6.5 470 true 13 8.4 320
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c error (139) 4.4   4.9  40   wit - -
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c error (134) 5.3   5.8  39   wit - -
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true .85  .95 39   wit - -
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c true 3.4   3.9  39   wit - -
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c true .93  1.0  39   wit - -
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c true 2.9   3.3  40   wit - -
ssh-simplified/s3_srvr_1a_true-unreach-call.cil.c error (139) 18     20    39   wit - -
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c true .53  .62 39   wit - -
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c true .95  1.1  39   wit - -
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c true 2.7   3.1  40   wit - -
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c true .78  .87 39   wit - -
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c true 2.9   3.2  40   wit - -
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c true 56     60    40   wit - -
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c true 2.8   3.1  39   wit - -
locks/test_locks_14_false-unreach-call.c unknown .60  .68 39   wit - -
locks/test_locks_15_false-unreach-call.c false(reach) 3.0   3.5  39   wit false(reach) 7.3 4.2 290 true 11 6.6 330
locks/test_locks_10_true-unreach-call.c unknown .52  .61 39   wit - -
locks/test_locks_11_true-unreach-call_false-termination.c true .20  .28 7.5 wit - -
locks/test_locks_12_true-unreach-call_false-termination.c error (139) 4.4   5.1  39   wit - -
locks/test_locks_13_true-unreach-call.c true 3.7   4.3  39   wit - -
locks/test_locks_14_true-unreach-call.c error (139) 370     400    40   wit - -
locks/test_locks_15_true-unreach-call_false-termination.c true .68  .79 39   wit - -
locks/test_locks_5_true-unreach-call_false-termination.c true 2.9   3.5  38   wit - -
locks/test_locks_6_true-unreach-call_false-termination.c error (134) 7.8   9.2  38   wit - -
locks/test_locks_7_true-unreach-call_false-termination.c timeout .086 930    3.5 wit - -
locks/test_locks_8_true-unreach-call_false-termination.c error (134) 53     60    39   wit - -
locks/test_locks_9_true-unreach-call.c unknown .54  .61 38   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 820 1800 1700 48 20   11   770   48 23   15   660  
    correct results 21 330 360 800 2 20   11   770   2 23   15   660  
        correct true 19 90 99 690 0 0   0   0   2 0   0   0  
        correct false 2 240 260 100 2 20   11   770   0 23   15   660  
    incorrect results 9 12 13 300 0 0   0   0   0 0   0   0  
        incorrect true 9 12 13 300 0 0   0   0   0 0   0   0  
        incorrect false 0
score (48 tasks, max score: 78) -248
Run set sv-comp16.ControlFlow