Tool SMACK+Corral 1.5.2
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-07 09:05:16 CET [[ 2016-01-15 09:34:34 CET ]] [[ 2016-01-15 22:36:10 CET ]]
Run set sv-comp16.ControlFlow
Options -w error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/smack.2016-01-07_0905.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/smack.2016-01-07_0905.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 timeout 13   13   140 wit timeout 90 66 4100 true 21 13   460
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-termination.cil.c witness unconfirmed 4.5 4.4 100 wit true 32 17 910 true 17 9.7 380
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-termination.cil.c witness unconfirmed 6.2 6.1 140 wit true 36 19 1000 true 19 10   410
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-termination.cil.c witness unconfirmed 4.1 4.0 88 wit true 33 17 910 true 16 8.7 370
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c true 11   11   150 wit - -
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-termination.cil.c true 5.6 5.5 100 wit - -
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-termination.cil.c true 5.1 5.0 95 wit - -
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-termination.cil.c true 6.4 6.3 110 wit - -
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-termination.cil.c true 3.4 3.4 73 wit - -
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-termination.cil.c true 3.8 3.8 84 wit - -
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c witness timeout 6.6 6.5 130 wit timeout 91 71 3700 true 14 12   330
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c witness timeout 6.5 6.4 140 wit timeout 90 73 3700 true 14 9.1 340
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c witness timeout 7.2 7.1 130 wit timeout 91 68 3000 true 14 7.9 330
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c witness timeout 5.5 5.4 130 wit timeout 91 66 2800 true 15 9.6 340
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c witness timeout 4.7 4.6 110 wit timeout 91 68 2900 true 13 7.4 360
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c witness timeout 14   14   160 wit timeout 91 71 3700 true 14 10   340
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c witness timeout 13   13   190 wit timeout 91 69 2900 true 14 7.5 340
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c witness timeout 6.2 6.2 140 wit timeout 91 68 2900 true 14 8.3 350
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c witness timeout 4.8 4.8 120 wit timeout 91 68 2900 true 14 8.4 340
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c witness timeout 5.0 4.9 130 wit timeout 91 69 2800 true 15 9.1 330
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c witness timeout 5.5 5.4 130 wit timeout 91 68 2700 true 15 9.7 340
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c false(reach) 4.8 4.7 130 wit timeout 91 70 3700 false(reach) 16 10   370
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c true 99   99   180 wit - -
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true 83   82   180 wit - -
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c true 89   89   180 wit - -
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c true 88   88   180 wit - -
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c true 880   880   360 wit - -
ssh-simplified/s3_srvr_1a_true-unreach-call.cil.c true 880   880   360 wit - -
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c true 880   880   280 wit - -
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c true 880   880   360 wit - -
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c true 880   880   360 wit - -
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c true 880   880   370 wit - -
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c true 880   880   330 wit - -
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c true 880   880   340 wit - -
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c true 880   880   340 wit - -
locks/test_locks_14_false-unreach-call.c witness timeout 3.7 3.6 84 wit timeout 90 75 3700 true 12 7.1 330
locks/test_locks_15_false-unreach-call.c witness timeout 3.6 3.6 85 wit timeout 90 76 3700 true 12 7.3 340
locks/test_locks_10_true-unreach-call.c true 2.9 2.9 77 wit - -
locks/test_locks_11_true-unreach-call_false-termination.c true 3.1 3.1 77 wit - -
locks/test_locks_12_true-unreach-call_false-termination.c true 3.0 3.0 79 wit - -
locks/test_locks_13_true-unreach-call.c true 3.1 3.1 81 wit - -
locks/test_locks_14_true-unreach-call.c true 3.2 3.2 82 wit - -
locks/test_locks_15_true-unreach-call_false-termination.c true 3.1 3.1 78 wit - -
locks/test_locks_5_true-unreach-call_false-termination.c true 3.1 3.0 81 wit - -
locks/test_locks_6_true-unreach-call_false-termination.c true 3.0 3.0 80 wit - -
locks/test_locks_7_true-unreach-call_false-termination.c true 3.0 3.0 68 wit - -
locks/test_locks_8_true-unreach-call_false-termination.c true 3.0 3.1 75 wit - -
locks/test_locks_9_true-unreach-call.c true 3.1 3.1 82 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 8500   8500   7600 48 1500   1100   52000   48 270   170   6400  
    correct results 31 8400   8400   5400 0 91   70   3700   1 16   10   370  
        correct true 30 8400   8400   5300 0 0   0   0   0 0   0   0  
        correct false 1 4.8 4.7 130 0 91   70   3700   1 16   10   370  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (48 tasks, max score: 78) 61
Run set sv-comp16.ControlFlow