Tool ULTIMATE Automizer cfb9fd9e
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-14 23:51:13 CET [[ 2016-01-15 09:43:48 CET ]] [[ 2016-01-15 22:41:15 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/uautomizer.2016-01-14_2351.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/uautomizer.2016-01-14_2351.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) 77 26   1300 wit false(reach) 17   9.0 570 false(reach) 25 14   520
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-termination.cil.c false(reach) 54 17   970 wit false(reach) 15   7.9 510 false(reach) 25 13   500
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-termination.cil.c false(reach) 62 22   1100 wit false(reach) 16   8.5 550 false(reach) 23 13   390
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-termination.cil.c false(reach) 29 9.2 610 wit timeout 90   73   3800 false(reach) 21 12   440
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-termination.cil.c true 83 31   1300 wit - -
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-termination.cil.c true 66 25   1200 wit - -
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-termination.cil.c true 64 23   1500 wit - -
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-termination.cil.c true 73 28   1800 wit - -
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-termination.cil.c true 16 5.3 410 wit - -
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-termination.cil.c true 19 5.9 490 wit - -
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c false(reach) 17 4.9 370 wit timeout 90   72   3800 false(reach) 21 12   490
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(reach) 19 5.0 500 wit timeout 90   72   3800 false(reach) 21 12   500
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c unknown 17 5.4 490 wit - -
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c false(reach) 17 4.7 510 wit timeout 90   74   3900 false(reach) 21 11   490
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c false(reach) 13 3.6 340 wit false(reach) 12   6.3 430 false(reach) 19 11   390
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c false(reach) 27 8.1 610 wit false(reach) 29   15   810 false(reach) 26 15   540
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c false(reach) 25 7.3 630 wit timeout 91   68   3300 false(reach) 24 13   510
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c false(reach) 21 6.6 450 wit false(reach) 16   8.6 550 false(reach) 22 12   510
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c false(reach) 24 6.8 530 wit false(reach) 14   7.5 500 false(reach) 23 13   470
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c false(reach) 14 3.9 350 wit false(reach) 15   8.4 560 false(reach) 21 12   510
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c false(reach) 14 3.8 410 wit false(reach) 15   8.5 570 false(reach) 22 12   510
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c false(reach) 11 3.2 340 wit false(reach) 10   5.7 410 false(reach) 18 9.8 360
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c true 33 11   1100 wit - -
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true 33 11   810 wit - -
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c true 35 12   1000 wit - -
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c true 34 10   830 wit - -
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c true 32 8.5 670 wit - -
ssh-simplified/s3_srvr_1a_true-unreach-call.cil.c true 11 3.4 340 wit - -
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c true 11 4.4 320 wit - -
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c true 33 10   840 wit - -
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c true 27 8.2 550 wit - -
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c true 31 8.4 680 wit - -
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c true 36 11   940 wit - -
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c true 37 12   1300 wit - -
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c true 33 9.7 590 wit - -
locks/test_locks_14_false-unreach-call.c false(reach) 11 3.4 340 wit false(reach) 7.6 4.3 390 false(reach) 15 8.5 330
locks/test_locks_15_false-unreach-call.c false(reach) 11 3.4 330 wit timeout 90   73   3900 false(reach) 17 9.7 360
locks/test_locks_10_true-unreach-call.c true 24 8.3 650 wit - -
locks/test_locks_11_true-unreach-call_false-termination.c true 25 8.0 1000 wit - -
locks/test_locks_12_true-unreach-call_false-termination.c true 42 13   2100 wit - -
locks/test_locks_13_true-unreach-call.c true 64 22   3800 wit - -
locks/test_locks_14_true-unreach-call.c true 110 38   5400 wit - -
locks/test_locks_15_true-unreach-call_false-termination.c true 250 81   7200 wit - -
locks/test_locks_5_true-unreach-call_false-termination.c true 11 3.4 320 wit - -
locks/test_locks_6_true-unreach-call_false-termination.c true 13 3.7 430 wit - -
locks/test_locks_7_true-unreach-call_false-termination.c true 17 4.4 490 wit - -
locks/test_locks_8_true-unreach-call_false-termination.c true 17 5.0 480 wit - -
locks/test_locks_9_true-unreach-call.c true 23 6.0 540 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 1800 580 49000 48 710   520   28000   48 360   200   7800  
    correct results 47 1800 570 49000 11 710   520   28000   17 360   200   7800  
        correct true 30 1300 430 39000 0 0   0   0   0 0   0   0  
        correct false 17 450 140 9700 11 710   520   28000   17 360   200   7800  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (48 tasks, max score: 78) 77
Run set sv-comp16.ControlFlow