Tool SymDIVINE
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-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-13 11:13:29 CET [[ 2017-01-15 02:06:46 CET ]] [[ 2017-01-15 03:46:01 CET ]] [[ 2017-01-15 02:24:39 CET ]] [[ 2017-01-15 04:02:29 CET ]]
Run set sv-comp17.ReachSafety-ControlFlow
Options --fix_volatile --fix_inline --silent -Os [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symdivine.2017-01-13_1113.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symdivine.2017-01-13_1113.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symdivine.2017-01-13_1113.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symdivine.2017-01-13_1113.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 4.6   4.6   54    150   .074  .090 false(unreach-call) 18    9.9  150   540 true 12   6.7 170 400 - -
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect 3.1   3.2   39    190   .053  11     false(unreach-call) 14    7.6  140   480 true 11   5.7 89 330 - -
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect 22     22     290    790   .070  9.8   false(unreach-call) 14    7.9  290   500 true 11   6.2 210 370 - -
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c false(unreach-call) 1 wit inspect 1.2   1.2   16    75   .041  0     false(unreach-call) 9.4  5.0  110   380 true 12   6.1 120 330 - -
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 4.8   4.8   57    170   .074  0     - - true 15    8.1  290   680 true 92   51   760 1100
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 13     13     160    480   .053  0     - - out of memory 520    500    7400   7000 true 91   49   1200 970
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 5.6   5.6   60    360   .053  0     - - true 11    5.7  72   480 true 70   38   620 920
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 25     25     350    1500   .070  .098 - - true 14    7.6  160   500 true 79   43   1000 980
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect .46  .49  4.7  41   .029  9.4   - - true 6.6  3.5  130   300 true 23   12   380 580
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 1.4   1.4   18    130   .041  0     - - true 8.3  4.4  170   340 true 21   11   210 570
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 120     120     1700    410   .025  0     false(unreach-call) 12    6.2  160   450 true 9.8 5.2 97 310 - -
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 120     120     1600    440   .025  0     false(unreach-call) 13    6.9  100   460 true 8.0 4.3 140 320 - -
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 280     280     3700    1000   .025  0     false(unreach-call) 11    6.0  220   450 true 8.2 4.4 170 320 - -
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 280     270     3300    960   .025  16     false(unreach-call) 10    5.4  190   450 true 10   5.5 130 320 - -
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 1.1   1.1   16    10   .020  0     false(unreach-call) 10    5.4  110   360 true 8.9 4.8 150 320 - -
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c timeout 0 wit inspect 900     890     10000    4200   .029  0     error (invalid witness file) .59 .37 9.9 40 error (invalid witness file) 6.3 3.3 120 300 - -
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c timeout 0 wit inspect 900     890     12000    3100   .033  0     error (invalid witness file) .54 .34 10   39 error (invalid witness file) 7.9 4.2 76 300 - -
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 290     280     3900    2000   .029  0     false(unreach-call) 13    6.6  130   470 true 11   5.8 140 330 - -
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 670     670     8300    3400   .025  0     false(unreach-call) 10    5.4  110   310 true 8.1 4.5 160 320 - -
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 420     420     5000    1800   .025  0     false(unreach-call) 9.0  4.8  120   320 true 10   5.5 120 320 - -
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 410     410     5900    2000   .025  0     false(unreach-call) 8.4  4.5  78   310 true 8.9 4.7 150 330 - -
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c false(unreach-call) 1 wit inspect 340     340     4400    1000   .029  0     false(unreach-call) 5.3  2.9  110   290 true 8.2 4.4 140 310 - -
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c true 2 wit inspect 160     160     2100    540   .025  0     - - true 14    7.8  220   530 true 50   27   720 1400
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c true 2 wit inspect 160     160     2300    860   .025  0     - - true 16    9.1  190   540 true 60   32   670 1500
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c true 2 wit inspect 160     160     2000    860   .025  .098 - - true 17    9.6  230   560 true 54   29   530 1400
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c true 2 wit inspect 160     160     2200    550   .025  0     - - true 15    8.4  220   550 true 61   33   610 1400
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c timeout 0 wit inspect 900     900     11000    4200   .025  4.0   - - error (invalid witness file) .71 .44 9.3 44 error (invalid witness file) 5.7 3.0 110 310
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c true 2 wit inspect .57  .57  7.3  15   .012  0     - - true 7.8  4.1  120   320 true 12   6.5 170 380
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c true 2 wit inspect .090 .090 .62 9.7 .0082 0     - - true 4.9  2.7  87   300 true 8.4 4.5 130 330
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c timeout 0 wit inspect 900     900     13000    4500   .025  0     - - error (invalid witness file) .50 .31 4.1 39 error (invalid witness file) 5.9 3.2 100 300
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c timeout 0 wit inspect 900     900     12000    4500   .025  0     - - error (invalid witness file) .46 .30 5.7 39 error (invalid witness file) 6.2 3.3 110 300
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c timeout 0 wit inspect 900     900     13000    4500   .025  0     - - error (invalid witness file) .61 .39 11   43 error (invalid witness file) 6.2 3.2 120 300
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c timeout 0 wit inspect 900     900     13000    5000   .029  .061 - - error (invalid witness file) .53 .34 12   40 error (invalid witness file) 6.1 3.2 86 310
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c timeout 0 wit inspect 900     900     12000    4500   .025  4.5   - - error (invalid witness file) .65 .42 8.4 41 error (invalid witness file) 6.4 3.3 92 300
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c timeout 0 wit inspect 900     900     13000    4500   .025  0     - - error (invalid witness file) .49 .32 9.1 40 error (invalid witness file) 7.0 3.7 83 300
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect .088 .087 .72 9.9 .0082 0     false(unreach-call) 6.0  3.2  64   280 true 7.2 3.8 130 310 - -
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c false(unreach-call) 1 wit inspect .099 .099 .76 10   .0082 0     false(unreach-call) 5.4  2.9  91   290 true 7.8 4.2 150 330 - -
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .059 .059 .55 10   .0082 0     - - true 5.8  3.1  99   290 true 22   12   290 760
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .081 .081 .57 9.8 .0082 0     - - true 7.6  4.1  84   300 true 27   14   460 1300
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .072 .072 .60 9.9 .0082 0     - - true 7.8  4.2  89   300 true 34   19   760 2500
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .096 .097 .52 9.8 .0082 0     - - true 7.6  4.1  92   300 true 39   24   640 3600
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .093 .093 .55 10   .0082 0     - - true 7.0  3.8  120   300 true 77   49   610 6300
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .088 .087 .52 9.9 .0082 0     - - true 8.1  4.4  73   300 out of memory 100   65   1100 7000
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .076 .076 .50 9.6 .0082 0     - - true 5.9  3.3  65   290 true 9.4 5.1 180 350
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .061 .061 .62 10   .0082 0     - - true 5.9  3.2  76   290 true 12   6.5 190 440
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .059 .058 .58 9.9 .0082 0     - - true 4.9  2.7  65   280 true 14   7.4 240 490
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .060 .060 .54 9.6 .0082 0     - - true 5.5  3.0  60   290 true 16   8.5 260 490
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c true 2 wit inspect .074 .11  .80 17   .0082 11     - - true 7.4  4.0  72   290 true 18   9.4 250 590
ntdrivers/cdaudio_false-unreach-call.i.cil.c unknown 0 wit inspect .17  .17  1.5  16   .26   0     error (invalid witness file) .66 .43 7.2 41 error (invalid witness file) 6.8 3.6 120 300 - -
ntdrivers/diskperf_false-unreach-call.i.cil.c error (1) 0 wit inspect 1.0   1.0   14    64   .18   .41  error (invalid witness file) .50 .32 8.6 39 error (invalid witness file) 7.3 3.8 110 300 - -
ntdrivers/floppy_false-unreach-call.i.cil.c unknown 0 wit inspect .32  .32  3.6  26   .34   0     error (invalid witness file) .56 .37 9.0 39 error (invalid witness file) 8.3 4.4 63 300 - -
ntdrivers/kbfiltr_false-unreach-call.i.cil.c error (1) 0 wit inspect .093 .094 1.0  12   .11   .41  error (invalid witness file) .51 .34 9.1 40 error (invalid witness file) 6.5 3.4 120 300 - -
ntdrivers/parport_false-unreach-call.i.cil.c error (1) 0 wit inspect .66  .67  6.7  41   .41   .64  error (invalid witness file) .57 .37 9.2 39 error (invalid witness file) 7.4 3.8 120 310 - -
ntdrivers/cdaudio_true-unreach-call.i.cil.c unknown 0 wit inspect .14  .14  1.5  16   .26   0     - - error (invalid witness file) .52 .35 9.3 40 error (invalid witness file) 7.2 3.8 110 320
ntdrivers/diskperf_true-unreach-call.i.cil.c error (1) 0 wit inspect 1.1   1.1   15    65   .18   .41  - - error (invalid witness file) .49 .31 10   39 error (invalid witness file) 6.4 3.4 110 300
ntdrivers/floppy2_true-unreach-call.i.cil.c unknown 0 wit inspect .31  .31  3.4  22   .52   0     - - error (invalid witness file) .53 .34 10   42 error (invalid witness file) 7.7 4.1 120 310
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c unknown 0 wit inspect .27  .27  2.4  14   .34   0     - - error (invalid witness file) .58 .37 5.4 42 error (invalid witness file) 6.7 3.5 100 300
ntdrivers/parport_true-unreach-call.i.cil.c error (1) 0 wit inspect .64  .66  8.1  46   .41   4.7   - - error (invalid witness file) .54 .35 11   41 error (invalid witness file) 7.4 3.9 150 310
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c unknown 0 wit inspect .071 .071 .67 11   .049  0     error (invalid witness file) .56 .35 9.9 40 error (invalid witness file) 6.6 3.5 140 300 - -
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c unknown 0 wit inspect .064 .064 .66 11   .049  0     error (invalid witness file) .51 .33 11   39 error (invalid witness file) 6.2 3.3 130 310 - -
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c unknown 0 wit inspect .063 .062 .79 11   .049  0     error (invalid witness file) .63 .41 8.1 40 error (invalid witness file) 5.7 3.1 120 300 - -
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c unknown 0 wit inspect .069 .069 .62 11   .049  0     error (invalid witness file) .59 .37 10   41 error (invalid witness file) 6.6 3.4 96 300 - -
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c unknown 0 wit inspect .066 .067 .76 11   .053  0     error (invalid witness file) .51 .32 11   40 error (invalid witness file) 5.6 3.0 120 290 - -
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c unknown 0 wit inspect .087 .087 .61 11   .057  0     error (invalid witness file) .50 .31 8.2 39 error (invalid witness file) 7.6 4.0 78 300 - -
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c unknown 0 wit inspect .073 .073 .73 11   .057  0     error (invalid witness file) .60 .39 9.3 40 error (invalid witness file) 6.1 3.3 120 310 - -
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c unknown 0 wit inspect .089 .089 .68 11   .057  0     error (invalid witness file) .49 .31 6.6 39 error (invalid witness file) 5.8 3.1 93 300 - -
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c unknown 0 wit inspect .081 .095 .74 12   .057  5.1   error (invalid witness file) .51 .33 10   40 error (invalid witness file) 5.6 3.0 110 290 - -
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c unknown 0 wit inspect .075 .075 .70 11   .057  0     error (invalid witness file) .64 .40 5.6 40 error (invalid witness file) 6.6 3.5 95 310 - -
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c unknown 0 wit inspect .066 .066 .87 11   .057  0     error (invalid witness file) .56 .37 10   39 error (invalid witness file) 6.5 3.4 100 300 - -
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c unknown 0 wit inspect .093 .093 .66 11   .057  0     error (invalid witness file) .50 .32 7.7 41 error (invalid witness file) 5.8 3.1 120 290 - -
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c unknown 0 wit inspect .070 .070 .66 11   .057  0     error (invalid witness file) .52 .33 9.2 40 error (invalid witness file) 7.0 3.7 89 310 - -
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c unknown 0 wit inspect .071 .072 .61 11   .057  0     error (invalid witness file) .57 .37 11   42 error (invalid witness file) 7.5 3.9 82 300 - -
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c unknown 0 wit inspect .10  .10  .60 11   .057  0     error (invalid witness file) .60 .37 7.8 39 error (invalid witness file) 6.1 3.2 120 300 - -
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c unknown 0 wit inspect .10  .10  .56 11   .057  0     error (invalid witness file) .50 .33 6.7 40 error (invalid witness file) 6.1 3.2 120 300 - -
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c unknown 0 wit inspect .10  .10  .56 11   .057  0     error (invalid witness file) .51 .34 10   41 error (invalid witness file) 6.2 3.3 120 300 - -
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c unknown 0 wit inspect .066 .067 .72 11   .057  0     error (invalid witness file) .65 .41 7.4 39 error (invalid witness file) 7.7 4.0 90 290 - -
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c unknown 0 wit inspect .084 .084 .73 11   .057  0     error (invalid witness file) .53 .35 11   40 error (invalid witness file) 6.5 3.4 90 300 - -
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c unknown 0 wit inspect .064 .064 .73 11   .049  0     - - error (invalid witness file) .50 .31 14   40 error (invalid witness file) 6.6 3.5 120 300
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c unknown 0 wit inspect .070 .070 .60 11   .049  .13  - - error (invalid witness file) .52 .34 13   40 error (invalid witness file) 6.3 3.3 120 300
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c unknown 0 wit inspect .073 .073 .69 11   .049  0     - - error (invalid witness file) .51 .32 9.1 39 error (invalid witness file) 6.4 3.4 120 300
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c unknown 0 wit inspect .065 .065 .76 11   .049  0     - - error (invalid witness file) .57 .37 11   41 error (invalid witness file) 7.2 3.8 120 310
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c unknown 0 wit inspect .085 .085 .63 11   .057  0     - - error (invalid witness file) .50 .33 13   40 error (invalid witness file) 6.7 3.5 140 300
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c unknown 0 wit inspect .094 .094 .64 11   .057  0     - - error (invalid witness file) .62 .40 8.8 41 error (invalid witness file) 6.9 3.6 120 320
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c unknown 0 wit inspect .083 .083 .77 11   .057  0     - - error (invalid witness file) .56 .36 9.8 39 error (invalid witness file) 6.4 3.4 130 300
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c unknown 0 wit inspect .069 .069 .71 11   .057  0     - - error (invalid witness file) .62 .39 9.5 40 error (invalid witness file) 6.1 3.3 130 290
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c unknown 0 wit inspect .088 .088 .64 11   .057  0     - - error (invalid witness file) .58 .36 11   40 error (invalid witness file) 6.2 3.2 100 300
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c unknown 0 wit inspect .067 .067 .69 11   .057  0     - - error (invalid witness file) .62 .40 7.0 39 error (invalid witness file) 6.9 3.6 100 320
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c unknown 0 wit inspect .087 .087 .70 11   .057  0     - - error (invalid witness file) .66 .40 9.0 41 error (invalid witness file) 6.1 3.3 100 310
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c unknown 0 wit inspect .067 .067 .60 11   .057  0     - - error (invalid witness file) .64 .41 7.8 40 error (invalid witness file) 6.2 3.3 95 310
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c unknown 0 wit inspect .091 .093 .67 11   .057  0     - - error (invalid witness file) .63 .40 7.7 42 error (invalid witness file) 6.5 3.5 100 310
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c unknown 0 wit inspect .087 .088 .66 11   .057  0     - - error (invalid witness file) .55 .35 5.7 41 error (invalid witness file) 7.7 4.0 120 310
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c unknown 0 wit inspect .081 .081 .56 11   .057  0     - - error (invalid witness file) .61 .40 9.1 40 error (invalid witness file) 5.6 3.1 110 300
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c unknown 0 wit inspect .076 .090 .80 12   .057  4.4   - - error (invalid witness file) .51 .34 7.1 40 error (invalid witness file) 6.3 3.3 120 300
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c unknown 0 wit inspect .067 .067 .87 11   .057  0     - - error (invalid witness file) .53 .34 12   40 error (invalid witness file) 6.8 3.6 99 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 62 12000 12000 160000 60000 6.2  82 94 180 100 2400 7400   94 320 170 5000 13000   94 740 620 10000 17000   94 1200 660 15000 44000  
    correct results 39 62 3700 3600 47000 20000 1.0  58 16 170 91 2200 6300   16 150 82 2300 5300   22 720 610 10000 15000   22 990 560 12000 35000  
        correct true 23 46 700 700 9200 5600 .53 21 0 0 0 0 0   16 0 0 0 0   22 720 610 10000 15000   22 990 560 12000 35000  
        correct false 16 16 3000 2900 38000 14000 .50 37 16 170 91 2200 6300   0 150 82 2300 5300   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (94 tasks, max score: 146) 62
Run set sv-comp17.ReachSafety-ControlFlow