Tool 2LS 0.5.0
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-57-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-10 17:21:21 CET [[ 2017-01-14 18:00:17 CET ]] [[ 2017-01-14 20:02:31 CET ]] [[ 2017-01-14 18:18:08 CET ]] [[ 2017-01-14 20:29:39 CET ]]
Run set sv-comp17.ReachSafety-ControlFlow
Options --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect 1.3  1.3  13    370 .0041 0     false(unreach-call) 8.2  4.4  120   320 false(unreach-call) 17   9.1 320 520 - -
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect .35 .34 3.3  60 .0041 0     false(unreach-call) 8.1  4.3  170   310 false(unreach-call) 13   6.6 240 450 - -
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect .55 .53 4.9  120 .0041 0     false(unreach-call) 8.3  4.4  100   330 false(unreach-call) 12   6.6 210 500 - -
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect .29 .28 2.4  39 .0041 0     false(unreach-call) 7.8  4.2  80   380 false(unreach-call) 13   6.7 180 410 - -
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 1.4  1.4  14    410 .0041 12     - - true 18    9.5  340   640 true 100   56   1200 1100
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .53 .53 4.9  110 .0041 0     - - out of memory 480    470    8700   7000 true 73   40   1100 1000
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .36 .35 3.3  67 .0041 0     - - true 12    6.5  230   480 true 70   38   1100 920
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .59 .58 5.6  130 .0041 0     - - true 16    8.4  260   520 true 68   37   700 1400
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .19 .19 1.4  26 .0041 0     - - true 8.0  4.2  140   310 true 24   13   400 550
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .29 .29 2.3  45 .0041 0     - - true 12    6.3  120   360 true 25   13   450 580
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 21    21    200    200 .0041 0     false(unreach-call) 7.4  3.9  170   310 false(unreach-call) 12   6.8 210 460 - -
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 23    23    200    200 .0041 0     false(unreach-call) 7.4  3.9  130   310 false(unreach-call) 14   7.1 200 480 - -
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 43    43    370    260 .0041 0     false(unreach-call) 8.1  4.3  140   310 false(unreach-call) 12   6.1 130 470 - -
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 24    24    250    200 .0041 0     false(unreach-call) 8.1  4.3  150   310 false(unreach-call) 13   7.0 220 470 - -
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c false(unreach-call) 1 wit inspect .27 .26 3.1  37 .0041 .16  false(unreach-call) 6.2  3.3  130   290 false(unreach-call) 11   5.8 200 370 - -
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 30    30    260    250 .0041 0     true 11    5.7  91   400 false(unreach-call) 16   8.4 320 570 - -
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c false(unreach-call) 0 wit inspect 43    43    320    250 .0041 0     true 9.0  4.8  180   410 true 11   5.6 150 490 - -
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 20    20    170    170 .0041 0     true 8.4  4.4  110   420 false(unreach-call) 15   7.8 230 490 - -
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 5.1  5.1  50    77 .0041 0     false(unreach-call) 6.5  3.5  110   290 false(unreach-call) 14   7.2 270 410 - -
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 25    25    190    180 .0041 0     false(unreach-call) 7.2  3.8  94   300 false(unreach-call) 12   6.4 190 480 - -
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 17    17    180    160 .0041 0     false(unreach-call) 7.1  3.8  83   320 false(unreach-call) 13   6.6 240 490 - -
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c false(unreach-call) 1 wit inspect .29 .28 2.8  38 .0041 0     false(unreach-call) 5.5  2.9  100   290 false(unreach-call) 10   5.4 200 350 - -
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c true 2 wit inspect 23    23    270    260 .0041 0     - - true 16    9.0  290   540 true 51   28   640 1500
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true 2 wit inspect 25    25    200    270 .0041 0     - - true 15    8.4  230   550 true 64   34   1100 1500
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c true 2 wit inspect 42    42    330    340 .0041 0     - - true 23    12    230   570 true 61   33   1000 1400
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c true 2 wit inspect 21    21    220    270 .0041 0     - - true 18    10    260   540 true 78   41   800 1400
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c timeout 0 wit inspect 900    900    9900    9200 .0041 0     - - error (invalid witness file) .52 .34 11   40 error (invalid witness file) 7.4 3.9 84 300
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c true 2 wit inspect 1.0  1.0  11    39 .0041 0     - - true 8.7  4.7  130   320 true 11   5.9 210 370
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c true 2 wit inspect .54 .53 6.5  28 .0041 0     - - true 6.3  3.4  78   290 true 8.6 4.7 190 330
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c timeout 0 wit inspect 900    900    10000    9000 .0041 0     - - error (invalid witness file) .53 .33 10   41 error (invalid witness file) 7.7 4.0 89 310
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c timeout 0 wit inspect 900    900    10000    9000 .0041 0     - - error (invalid witness file) .62 .40 7.3 39 error (invalid witness file) 6.0 3.1 120 300
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c timeout 0 wit inspect 900    900    11000    9100 .0041 0     - - error (invalid witness file) .62 .38 8.9 40 error (invalid witness file) 7.3 3.8 77 300
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c timeout 0 wit inspect 900    900    9800    8900 .0041 0     - - error (invalid witness file) .51 .32 11   39 error (invalid witness file) 6.4 3.4 100 310
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c timeout 0 wit inspect 900    900    9900    8800 .0041 0     - - error (invalid witness file) .57 .37 8.3 39 error (invalid witness file) 6.4 3.3 120 300
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c timeout 0 wit inspect 900    900    9900    9000 .0041 0     - - error (invalid witness file) .66 .42 8.2 40 error (invalid witness file) 6.1 3.2 120 300
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect .15 .14 .97 25 .0041 0     false(unreach-call) 5.0  2.7  54   290 false(unreach-call) 13   6.9 170 430 - -
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect .15 .14 1.3  25 .0041 0     false(unreach-call) 5.1  2.8  79   290 false(unreach-call) 9.2 4.9 140 350 - -
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .11 .11 1.3  24 .0041 0     - - true 7.3  4.0  89   290 true 22   12   380 790
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .15 .14 .93 26 .0041 0     - - true 8.0  4.3  74   310 true 26   14   470 1100
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .13 .13 .90 26 .0041 0     - - true 6.5  3.5  100   300 true 36   21   570 2200
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .13 .13 1.2  25 .0041 0     - - true 7.3  3.9  140   310 true 46   28   760 3800
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .14 .14 .93 25 .0041 0     - - true 8.1  4.3  81   300 true 82   53   1500 6200
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .14 .13 1.3  25 .0041 0     - - true 8.8  4.8  94   300 out of memory 110   67   1800 7000
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .14 .13 .67 25 .0041 .16  - - true 5.3  2.9  97   290 true 13   6.8 140 380
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .13 .13 .78 23 .0041 0     - - true 6.4  3.5  73   290 true 12   6.2 180 380
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .14 .14 .86 25 .0041 0     - - true 6.3  3.4  88   290 true 13   6.9 230 450
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .14 .14 .90 23 .0041 0     - - true 6.4  3.5  84   290 true 16   8.4 230 580
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .13 .12 .90 23 .0041 0     - - true 7.2  3.9  94   290 true 18   9.5 300 590
ntdrivers/cdaudio_false-unreach-call.i.cil.c timeout 0 wit inspect 900    900    7400    14000 .012  0     error (invalid witness file) .52 .34 11   40 error (invalid witness file) 7.6 4.0 150 310 - -
ntdrivers/diskperf_false-unreach-call.i.cil.c false(unreach-call) 1 wit inspect 2.3  2.2  25    660 .012  0     false(unreach-call) 17    11    210   970 false(unreach-call) 16   8.8 290 510 - -
ntdrivers/floppy_false-unreach-call.i.cil.c error (134) 0 wit inspect 4.0  4.0  44    1000 .012  0     error (invalid witness file) .49 .33 12   40 error (invalid witness file) 6.9 3.6 120 310 - -
ntdrivers/kbfiltr_false-unreach-call.i.cil.c true -32 wit inspect 2.0  2.0  23    180 .012  .025 false(unreach-call) 18    10    360   610 timeout 97   52   810 1000 - -
ntdrivers/parport_false-unreach-call.i.cil.c error (5) 0 wit inspect 1.3  1.3  11    99 .012  0     error (invalid witness file) .47 .30 12   39 error (invalid witness file) 6.8 3.6 130 300 - -
ntdrivers/cdaudio_true-unreach-call.i.cil.c true 2 wit inspect 24    24    190    1200 .012  0     - - true 44    28    970   930 true 160   97   2300 2400
ntdrivers/diskperf_true-unreach-call.i.cil.c true 2 wit inspect 2.2  2.2  31    680 .012  0     - - out of memory 640    630    12000   7000 true 130   79   1900 1800
ntdrivers/floppy2_true-unreach-call.i.cil.c error (5) 0 wit inspect 830    830    4100    2800 .012  0     - - error (invalid witness file) .52 .34 13   42 error (invalid witness file) 8.6 4.4 160 320
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c out of memory 0 wit inspect 840    840    6200    15000 .012  0     - - error (invalid witness file) .66 .42 8.4 40 error (invalid witness file) 7.0 3.7 130 300
ntdrivers/parport_true-unreach-call.i.cil.c error (5) 0 wit inspect 1.3  1.3  11    99 .012  0     - - error (invalid witness file) .62 .39 9.7 40 error (invalid witness file) 6.6 3.5 130 300
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c error (134) 0 wit inspect 200    200    1800    890 .012  0     error (invalid witness file) .50 .33 12   41 error (invalid witness file) 7.0 3.7 120 310 - -
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c error (134) 0 wit inspect 200    200    1100    750 .012  0     error (invalid witness file) .53 .34 4.5 42 error (invalid witness file) 5.7 3.1 110 290 - -
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c error (134) 0 wit inspect 190    190    1700    750 .012  0     error (invalid witness file) .48 .31 12   39 error (invalid witness file) 9.1 4.7 79 310 - -
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c error (134) 0 wit inspect 210    210    1600    760 .012  0     error (invalid witness file) .50 .32 13   40 error (invalid witness file) 7.1 3.8 83 290 - -
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c error (134) 0 wit inspect 410    410    2300    1100 .012  0     error (invalid witness file) .53 .34 9.8 42 error (invalid witness file) 6.3 3.3 140 300 - -
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c error (134) 0 wit inspect 360    360    2600    1000 .012  0     error (invalid witness file) .50 .33 11   40 error (invalid witness file) 6.4 3.4 120 300 - -
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c error (134) 0 wit inspect 400    400    1800    1000 .012  0     error (invalid witness file) .54 .37 12   44 error (invalid witness file) 6.1 3.2 120 290 - -
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c error (134) 0 wit inspect 400    400    3300    1000 .012  0     error (invalid witness file) .51 .34 3.8 40 error (invalid witness file) 6.0 3.2 120 300 - -
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c error (134) 0 wit inspect 590    590    3000    1500 .012  0     error (invalid witness file) .53 .35 11   39 error (invalid witness file) 6.1 3.2 82 300 - -
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c error (134) 0 wit inspect 600    600    3500    1500 .012  0     error (invalid witness file) .52 .34 8.9 42 error (invalid witness file) 5.9 3.1 110 290 - -
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c error (134) 0 wit inspect 660    660    3400    2100 .012  .10  error (invalid witness file) .50 .32 10   39 error (invalid witness file) 7.2 3.8 130 320 - -
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c error (134) 0 wit inspect 600    600    3500    1400 .012  0     error (invalid witness file) .50 .33 11   39 error (invalid witness file) 6.0 3.2 120 290 - -
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c error (134) 0 wit inspect 560    560    3800    2100 .012  0     error (invalid witness file) .53 .34 12   39 error (invalid witness file) 7.3 3.8 140 320 - -
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c error (134) 0 wit inspect 620    620    2900    1300 .012  0     error (invalid witness file) .58 .37 9.6 40 error (invalid witness file) 6.5 3.4 120 290 - -
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c error (134) 0 wit inspect 570    570    3500    1400 .012  0     error (invalid witness file) .51 .32 12   39 error (invalid witness file) 6.4 3.4 130 310 - -
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c error (134) 0 wit inspect 580    580    2900    1400 .012  0     error (invalid witness file) .50 .31 9.7 39 error (invalid witness file) 6.4 3.4 110 310 - -
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c error (134) 0 wit inspect 580    580    3600    1500 .012  0     error (invalid witness file) .52 .33 8.5 39 error (invalid witness file) 6.4 3.4 87 300 - -
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c error (134) 0 wit inspect 580    580    3600    2100 .012  0     error (invalid witness file) .51 .33 9.0 39 error (invalid witness file) 6.2 3.3 130 300 - -
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c error (134) 0 wit inspect 630    630    3500    1400 .012  0     error (invalid witness file) .51 .34 9.5 40 error (invalid witness file) 6.0 3.2 110 300 - -
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c true 2 wit inspect 210    210    1400    1100 .012  0     - - true 220    210    3900   2100 timeout 960   890   14000 3000
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c true 2 wit inspect 200    200    1400    1000 .012  0     - - true 220    210    4400   2000 timeout 960   890   16000 3800
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c true 2 wit inspect 210    210    1000    1000 .012  0     - - true 220    200    4100   2100 timeout 960   910   26000 4100
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c true 2 wit inspect 210    210    1100    1000 .012  0     - - true 230    220    3900   2000 timeout 960   880   16000 3100
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c timeout 0 wit inspect 900    900    8500    9400 .012  0     - - error (invalid witness file) .62 .40 8.1 39 error (invalid witness file) 6.9 3.6 98 300
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c timeout 0 wit inspect 900    900    5300    9300 .012  0     - - error (invalid witness file) .63 .40 7.8 40 error (invalid witness file) 6.6 3.5 110 300
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c timeout 0 wit inspect 900    900    6300    9000 .012  0     - - error (invalid witness file) .53 .33 12   42 error (invalid witness file) 5.5 3.0 100 290
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c timeout 0 wit inspect 900    900    6700    9100 .012  0     - - error (invalid witness file) .49 .32 8.4 40 error (invalid witness file) 6.6 3.5 120 300
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c timeout 0 wit inspect 900    900    6000    9100 .012  0     - - error (invalid witness file) .54 .34 13   44 error (invalid witness file) 8.6 4.5 86 330
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c timeout 0 wit inspect 900    900    5700    7900 .012  0     - - error (invalid witness file) .60 .38 9.5 42 error (invalid witness file) 6.3 3.4 130 300
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c timeout 0 wit inspect 900    900    7000    9200 .012  0     - - error (invalid witness file) .49 .31 8.6 41 error (invalid witness file) 6.2 3.3 130 300
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c timeout 0 wit inspect 900    900    5600    8400 .012  0     - - error (invalid witness file) .58 .38 7.1 39 error (invalid witness file) 6.4 3.4 120 300
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c timeout 0 wit inspect 900    900    6300    8800 .012  0     - - error (invalid witness file) .63 .40 7.9 39 error (invalid witness file) 6.3 3.3 130 300
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c timeout 0 wit inspect 900    900    9500    10000 .012  .31  - - error (invalid witness file) .61 .38 6.9 42 error (invalid witness file) 6.6 3.5 140 320
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c timeout 0 wit inspect 900    900    6200    8500 .012  0     - - error (invalid witness file) .51 .33 12   41 error (invalid witness file) 6.4 3.4 130 290
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c timeout 0 wit inspect 900    900    6000    8700 .012  .082 - - error (invalid witness file) .51 .33 10   40 error (invalid witness file) 6.7 3.5 130 310
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c timeout 0 wit inspect 900    900    6000    9100 .012  0     - - error (invalid witness file) .48 .31 13   40 error (invalid witness file) 6.3 3.3 130 300
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
total 94 44 31000   31000   240000 250000 .76   13     94 180   100   2900 8300   94 490 260   7500 16000   94 2300 2100 42000 32000   94 5300 4400 95000 61000  
    correct results 47 76 1200   1200   8100 11000 .25   13     18 140   77   2100 6400   18 240 120   4000 8200   27 2300 2100 41000 32000   24 5200 4300 92000 54000  
        correct true 29 58 970   970   6200 8400 .17   13     2 0   0   0 0   0 0 0   0 0   27 2300 2100 41000 32000   24 5200 4300 92000 54000  
        correct false 18 18 210   210   1900 3100 .082  .16  16 140   77   2100 6400   18 240 120   4000 8200   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 1 0 43   43   320 250 .0041 0     1 9.0 4.8 180 410   1 11 5.6 150 490   0 0 0 0 0   0 0 0 0 0  
        correct-unconfirmed true 0
        correct-unconfirmed false 1 0 43   43   320 250 .0041 0     0 9.0 4.8 180 410   0 11 5.6 150 490   0 0 0 0 0   0 0 0 0 0  
    incorrect results 1 -32 2.0 2.0 23 180 .012  .025 1 18   10   360 610   0 97 52   810 1000   0 0 0 0 0   0 0 0 0 0  
        incorrect true 1 -32 2.0 2.0 23 180 .012  .025 0 18   10   360 610   0 97 52   810 1000   0 0 0 0 0   0 0 0 0 0  
        incorrect false 0
score (94 tasks, max score: 146) 44
Run set sv-comp17.ReachSafety-ControlFlow