Tool VVT prerelease
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-17 23:14:00 CET [[ 2016-01-18 06:54:01 CET ]] [[ 2016-01-18 07:05:55 CET ]]
Run set sv-comp16.ControlFlow
Options [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/vvt.2016-01-17_2314.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/vvt.2016-01-17_2314.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 witness unconfirmed 2.7  2.2  69 wit unknown 6.8 3.8 270 error (1) .030 .033 5.1
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-termination.cil.c witness unconfirmed 1.4  1.1  39 wit unknown 5.7 3.2 230 error (1) .030 .034 5.0
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-termination.cil.c witness unconfirmed 2.0  1.6  39 wit unknown 6.4 3.5 260 error (1) .028 .042 5.0
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-termination.cil.c witness unconfirmed .97 .69 34 wit unknown 5.0 2.8 230 error (1) .027 .031 5.0
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c unknown 3.0  2.6  64 wit - -
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-termination.cil.c true 6.8  3.9  120 wit - -
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-termination.cil.c unknown 1.3  1.1  44 wit - -
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-termination.cil.c unknown 2.0  1.6  37 wit - -
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-termination.cil.c unknown .52 .36 23 wit - -
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-termination.cil.c unknown .78 .58 28 wit - -
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c witness unconfirmed 4.2  2.0  69 wit unknown 4.9 2.8 200 error (1) .029 .032 5.1
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c witness unconfirmed 4.6  2.2  78 wit unknown 4.8 2.7 200 error (1) .048 .052 5.1
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c witness unconfirmed 5.1  2.4  68 wit unknown 4.7 2.7 200 error (1) .029 .032 5.1
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c witness unconfirmed 3.7  1.8  67 wit unknown 4.9 2.7 200 error (1) .026 .032 5.1
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c witness unconfirmed .39 .26 20 wit unknown 5.2 3.1 220 error (1) .040 .045 5.0
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c witness unconfirmed 5.6  2.8  72 wit unknown 5.2 2.9 200 error (1) .031 .033 5.0
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c witness unconfirmed 3.7  1.9  77 wit unknown 5.0 2.8 190 error (1) .037 .044 5.0
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c witness unconfirmed 1.3  .76 33 wit unknown 5.1 2.9 210 error (1) .027 .032 5.0
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c witness unconfirmed .64 .43 25 wit unknown 5.0 2.8 210 error (1) .029 .032 5.1
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c witness unconfirmed 1.2  .63 37 wit unknown 4.7 2.7 190 error (1) .029 .034 5.0
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c witness unconfirmed 1.4  .76 25 wit unknown 4.8 2.6 190 error (1) .030 .034 5.1
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c witness unconfirmed .59 .42 25 wit unknown 5.0 2.8 200 error (1) .033 .034 5.0
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c unknown 150    68    110 wit - -
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c unknown 150    73    100 wit - -
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c unknown 130    61    100 wit - -
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c unknown 95    44    110 wit - -
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c true 510    240    130 wit - -
ssh-simplified/s3_srvr_1a_true-unreach-call.cil.c true 5.6  2.6  52 wit - -
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c true 1.3  .57 44 wit - -
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c true 310    150    120 wit - -
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c true 550    260    130 wit - -
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c true 570    270    140 wit - -
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c true 880    420    180 wit - -
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c timeout 900    430    140 wit - -
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c true 160    75    160 wit - -
locks/test_locks_14_false-unreach-call.c witness unconfirmed .24 .15 18 wit unknown 3.7 2.2 170 error (1) .029 .033 5.0
locks/test_locks_15_false-unreach-call.c witness unconfirmed .23 .15 14 wit unknown 3.8 2.2 170 error (1) .031 .033 5.2
locks/test_locks_10_true-unreach-call.c true .51 .25 30 wit - -
locks/test_locks_11_true-unreach-call_false-termination.c true .61 .30 25 wit - -
locks/test_locks_12_true-unreach-call_false-termination.c true .62 .30 29 wit - -
locks/test_locks_13_true-unreach-call.c true .74 .37 32 wit - -
locks/test_locks_14_true-unreach-call.c true .94 .45 31 wit - -
locks/test_locks_15_true-unreach-call_false-termination.c true .93 .45 37 wit - -
locks/test_locks_5_true-unreach-call_false-termination.c true .26 .13 23 wit - -
locks/test_locks_6_true-unreach-call_false-termination.c true .33 .16 27 wit - -
locks/test_locks_7_true-unreach-call_false-termination.c true .34 .17 25 wit - -
locks/test_locks_8_true-unreach-call_false-termination.c true .39 .19 32 wit - -
locks/test_locks_9_true-unreach-call.c true .54 .26 25 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 4500 2100 3000 48 91   51   3700   48 .56 .64 91  
    correct results 20 3000 1400 1400 0 0   0   0   0 0    0    0  
        correct true 20 3000 1400 1400 0 0   0   0   0 0    0    0  
        correct false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (48 tasks, max score: 78) 40
Run set sv-comp16.ControlFlow