Tool impara 0.45
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-13 07:41:14 CET [[ 2016-01-15 09:11:00 CET ]] [[ 2016-01-15 22:23:23 CET ]]
Run set sv-comp16.ControlFlow
Options --eager --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/impara.2016-01-13_0741.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/impara.2016-01-13_0741.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 .74 .74 33 wit true 16   8.5 680 true 21 12   470
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-termination.cil.c witness unconfirmed .46 .47 28 wit true 13   7.0 540 true 20 12   390
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-termination.cil.c witness unconfirmed .52 .52 32 wit true 16   8.3 560 true 19 11   460
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-termination.cil.c false(reach) .36 .37 27 wit true 12   6.7 410 false(reach) 21 12   460
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c true 2.9  2.9  40 wit - -
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-termination.cil.c true 3.3  3.3  32 wit - -
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-termination.cil.c true 1.5  1.6  30 wit - -
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-termination.cil.c true 2.4  2.4  30 wit - -
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-termination.cil.c true .48 .48 25 wit - -
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-termination.cil.c true .91 .91 27 wit - -
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c witness timeout .67 .68 26 wit timeout 90   72   3800 true 17 10   360
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c witness timeout .82 .82 26 wit timeout 90   71   3800 true 16 9.2 360
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c witness timeout .81 .81 26 wit timeout 91   71   3800 true 17 11   350
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c witness timeout .63 .63 26 wit timeout 91   69   3700 true 16 9.0 350
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c false(reach) .28 .29 26 wit false(reach) 9.0 5.0 420 false(reach) 18 10   380
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c witness timeout 2.9  2.9  27 wit timeout 91   68   3800 true 16 9.5 350
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c witness timeout 4.6  4.6  27 wit timeout 91   70   3800 true 16 9.3 360
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c witness timeout .66 .66 28 wit timeout 91   69   3800 true 15 8.6 350
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c witness timeout 1.1  1.1  26 wit timeout 91   70   3700 true 16 9.2 350
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c false(reach) 1.2  1.2  26 wit false(reach) 9.6 5.2 440 true 15 9.6 350
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c witness timeout 1.1  1.1  26 wit timeout 90   73   3800 true 17 9.2 360
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c false(reach) .20 .20 28 wit timeout 91   69   3800 false(reach) 18 11   360
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c true 42    42    30 wit - -
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true 34    34    29 wit - -
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c true 35    35    30 wit - -
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c true 34    34    29 wit - -
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c timeout 900    900    130 wit - -
ssh-simplified/s3_srvr_1a_true-unreach-call.cil.c true .33 .33 24 wit - -
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c true .13 .14 23 wit - -
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c timeout 900    900    120 wit - -
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c timeout 900    900    120 wit - -
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c timeout 900    900    130 wit - -
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c timeout 900    900    140 wit - -
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c timeout 900    900    130 wit - -
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c timeout 900    900    120 wit - -
locks/test_locks_14_false-unreach-call.c false(reach) .12 .12 24 wit false(reach) 9.2 5.0 420 true 14 8.1 360
locks/test_locks_15_false-unreach-call.c false(reach) .18 .18 24 wit false(reach) 12   6.3 430 true 13 7.2 340
locks/test_locks_10_true-unreach-call.c true 31    31    31 wit - -
locks/test_locks_11_true-unreach-call_false-termination.c true 84    84    51 wit - -
locks/test_locks_12_true-unreach-call_false-termination.c true 240    240    110 wit - -
locks/test_locks_13_true-unreach-call.c true 760    760    230 wit - -
locks/test_locks_14_true-unreach-call.c timeout 900    900    270 wit - -
locks/test_locks_15_true-unreach-call_false-termination.c timeout 900    900    240 wit - -
locks/test_locks_5_true-unreach-call_false-termination.c true .39 .39 23 wit - -
locks/test_locks_6_true-unreach-call_false-termination.c true .89 .89 23 wit - -
locks/test_locks_7_true-unreach-call_false-termination.c true 1.7  1.7  24 wit - -
locks/test_locks_8_true-unreach-call_false-termination.c true 4.8  4.8  27 wit - -
locks/test_locks_9_true-unreach-call.c true 11    11    27 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 9400   9400   2800 48 1000   750   42000   48 300   180   6800  
    correct results 27 1300   1300   1000 5 140   97   5900   6 98   58   2200  
        correct true 21 1300   1300   890 1 0   0   0   3 0   0   0  
        correct false 6 2.4 2.4 160 4 140   97   5900   3 98   58   2200  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (48 tasks, max score: 78) 48
Run set sv-comp16.ControlFlow