Tool CPAchecker 1.4-svn 18356M
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-10 22:01:17 CET [[ 2016-01-15 09:16:15 CET ]] [[ 2016-01-15 22:26:01 CET ]]
Run set sv-comp16.ControlFlow
Options -lpi-svcomp16 -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/lpi.2016-01-10_2201.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/lpi.2016-01-10_2201.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) 38   17   720 wit false(reach) 15   7.9 540 false(reach) 25 13 510
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-termination.cil.c false(reach) 20   6.7 540 wit false(reach) 14   7.4 490 false(reach) 26 14 520
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-termination.cil.c false(reach) 32   12   680 wit false(reach) 15   8.1 540 false(reach) 25 13 520
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-termination.cil.c false(reach) 9.6 3.3 410 wit false(reach) 15   8.0 540 false(reach) 24 15 490
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c true 19   4.2 520 wit - -
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-termination.cil.c true 46   8.5 1000 wit - -
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-termination.cil.c true 13   3.2 460 wit - -
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-termination.cil.c true 19   4.1 530 wit - -
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-termination.cil.c true 4.8 1.8 240 wit - -
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-termination.cil.c true 7.4 2.5 260 wit - -
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c false(reach) 24   5.4 520 wit false(reach) 11   5.8 480 false(reach) 21 14 500
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(reach) 26   5.7 570 wit false(reach) 15   7.8 500 false(reach) 22 14 500
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c false(reach) 25   5.3 560 wit false(reach) 14   7.6 500 unknown 20 11 490
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c false(reach) 28   6.1 530 wit false(reach) 12   6.6 480 false(reach) 22 14 490
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c false(reach) 8.6 2.7 360 wit false(reach) 8.4 4.6 420 false(reach) 19 10 400
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c false(reach) 43   12   990 wit false(reach) 16   8.3 500 false(reach) 28 15 560
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c false(reach) 40   11   940 wit false(reach) 15   7.8 490 false(reach) 24 13 520
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c false(reach) 24   5.9 510 wit false(reach) 14   7.3 510 false(reach) 23 12 510
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c exception 13   3.3 370 wit - -
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c false(reach) 21   4.9 450 wit false(reach) 12   6.6 480 false(reach) 21 11 500
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c false(reach) 20   4.5 480 wit false(reach) 11   6.1 470 false(reach) 22 14 510
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c false(reach) 8.6 2.7 360 wit false(reach) 9.8 5.4 400 false(reach) 20 11 370
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c true 30   5.7 730 wit - -
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true 35   6.3 840 wit - -
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c true 34   6.2 790 wit - -
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c true 33   6.0 780 wit - -
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c timeout 900   410   4500 wit - -
ssh-simplified/s3_srvr_1a_true-unreach-call.cil.c true 17   3.9 410 wit - -
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c true 5.6 1.9 310 wit - -
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c timeout 900   410   4700 wit - -
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c timeout 900   400   4800 wit - -
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c timeout 900   400   4800 wit - -
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c timeout 900   400   4900 wit - -
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c timeout 900   410   4700 wit - -
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c timeout 900   410   4700 wit - -
locks/test_locks_14_false-unreach-call.c timeout 900   900   950 wit - -
locks/test_locks_15_false-unreach-call.c exception 6.6 2.2 320 wit - -
locks/test_locks_10_true-unreach-call.c true 6.6 2.2 330 wit - -
locks/test_locks_11_true-unreach-call_false-termination.c true 6.9 2.2 320 wit - -
locks/test_locks_12_true-unreach-call_false-termination.c true 6.3 2.0 320 wit - -
locks/test_locks_13_true-unreach-call.c true 6.8 2.2 320 wit - -
locks/test_locks_14_true-unreach-call.c true 7.3 2.3 330 wit - -
locks/test_locks_15_true-unreach-call_false-termination.c true 7.5 2.3 330 wit - -
locks/test_locks_5_true-unreach-call_false-termination.c true 5.6 1.9 300 wit - -
locks/test_locks_6_true-unreach-call_false-termination.c true 5.9 2.0 300 wit - -
locks/test_locks_7_true-unreach-call_false-termination.c true 6.6 2.3 310 wit - -
locks/test_locks_8_true-unreach-call_false-termination.c true 5.7 1.9 320 wit - -
locks/test_locks_9_true-unreach-call.c true 5.9 2.1 310 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 7900 3900 54000 48 200   110   7300   48 340   200   7400  
    correct results 38 700 180 19000 15 200   110   7300   14 340   200   7400  
        correct true 23 340 78 10000 0 0   0   0   0 0   0   0  
        correct false 15 370 110 8600 15 200   110   7300   14 340   200   7400  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (48 tasks, max score: 78) 61
Run set sv-comp16.ControlFlow