Tool CPAchecker 1.4-svcomp16c
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-22-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-04 06:25:51 CET [[ 2016-01-15 08:31:02 CET ]] [[ 2016-01-15 21:59:57 CET ]]
Run set sv-comp16.ControlFlow
Options -sv-comp16-bam -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-bam.2016-01-04_0625.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-bam.2016-01-04_0625.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 false(reach) 15   4.3 660 wit false(reach) 15   7.8 560 false(reach) 26 17 530
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-termination.cil.c exception 6.7 2.5 290 wit - -
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-termination.cil.c exception 7.3 2.6 290 wit - -
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-termination.cil.c false(reach) 18   5.1 750 wit false(reach) 20   11   580 true 15 10 340
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c timeout 900   670   6600 wit - -
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-termination.cil.c true 41   12   1000 wit - -
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-termination.cil.c exception 5.7 2.2 280 wit - -
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-termination.cil.c exception 6.0 2.2 280 wit - -
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-termination.cil.c true 7.9 2.8 410 wit - -
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-termination.cil.c true 14   4.0 600 wit - -
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c timeout 900   830   1600 wit - -
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c timeout 900   830   1500 wit - -
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c timeout 900   840   860 wit - -
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c timeout 900   830   2400 wit - -
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c timeout 900   840   3600 wit - -
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c timeout 900   840   2300 wit - -
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c timeout 900   840   2900 wit - -
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c timeout 900   840   3700 wit - -
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c timeout 900   830   1500 wit - -
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c witness unconfirmed 8.8 3.0 440 wit true 27   15   890 true 21 12 510
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c false(reach) 10   3.5 460 wit false(reach) 13   6.9 480 false(reach) 20 12 510
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c false(reach) 6.9 2.5 350 wit false(reach) 8.4 4.7 420 false(reach) 17 10 380
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c timeout 900   830   1500 wit - -
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c timeout 900   830   3600 wit - -
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c timeout 900   830   3700 wit - -
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c timeout 900   840   2500 wit - -
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c timeout 900   830   2500 wit - -
ssh-simplified/s3_srvr_1a_true-unreach-call.cil.c true 5.6 2.4 260 wit - -
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c true 4.1 1.7 230 wit - -
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c timeout 900   830   1400 wit - -
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c timeout 900   830   2500 wit - -
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c timeout 900   830   950 wit - -
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c timeout 900   830   2600 wit - -
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c true 30   6.7 850 wit - -
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c timeout 900   830   2500 wit - -
locks/test_locks_14_false-unreach-call.c timeout 900   840   2600 wit - -
locks/test_locks_15_false-unreach-call.c timeout 900   840   3600 wit - -
locks/test_locks_10_true-unreach-call.c true 4.2 1.9 220 wit - -
locks/test_locks_11_true-unreach-call_false-termination.c true 4.0 1.7 220 wit - -
locks/test_locks_12_true-unreach-call_false-termination.c true 4.1 1.9 220 wit - -
locks/test_locks_13_true-unreach-call.c true 4.2 1.9 220 wit - -
locks/test_locks_14_true-unreach-call.c true 4.2 1.9 220 wit - -
locks/test_locks_15_true-unreach-call_false-termination.c true 3.6 1.7 220 wit - -
locks/test_locks_5_true-unreach-call_false-termination.c true 3.4 1.5 210 wit - -
locks/test_locks_6_true-unreach-call_false-termination.c true 4.0 1.8 210 wit - -
locks/test_locks_7_true-unreach-call_false-termination.c true 4.1 1.8 220 wit - -
locks/test_locks_8_true-unreach-call_false-termination.c true 4.0 1.8 220 wit - -
locks/test_locks_9_true-unreach-call.c true 3.4 1.6 220 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 20000 18000 66000 48 83   45   2900   48 99   61   2300  
    correct results 21 200 64 8000 4 56   30   2000   4 78   49   1800  
        correct true 17 150 49 5800 0 0   0   0   1 0   0   0  
        correct false 4 50 15 2200 4 56   30   2000   3 78   49   1800  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (48 tasks, max score: 78) 38
Run set sv-comp16.ControlFlow