Tool DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017
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-11 11:24:16 CET [[ 2017-01-14 21:58:42 CET ]] [[ 2017-01-14 22:27:33 CET ]] [[ 2017-01-14 22:07:52 CET ]] [[ 2017-01-14 22:42:14 CET ]]
Run set sv-comp17.ReachSafety-Sequentialized
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-11_1124.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-11_1124.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)
systemc/kundu1_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect 480    480    5100   260 6.0  0      true 18    9.2  380   640 true 7.5 4.1 88 320 - -
systemc/kundu2_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect 480    480    6700   170 3.5  0      true 32    19    680   1700 true 8.2 4.4 150 320 - -
systemc/pc_sfifo_1_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .50 .50 5.8 110 .87 0      false(unreach-call) 8.1  4.4  88   290 true 7.8 4.2 72 310 - -
systemc/pc_sfifo_2_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .53 .53 7.0 110 .87 0      false(unreach-call) 7.5  4.0  90   290 true 9.1 4.8 130 330 - -
systemc/pipeline_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 550    550    6700   15000 11    0      false(unreach-call) 23    12    270   760 true 11   6.0 140 330 - -
systemc/token_ring.01_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 2.3  2.3  31   110 4.3  0      false(unreach-call) 8.3  4.5  110   300 true 9.8 5.3 110 310 - -
systemc/token_ring.02_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 5.7  5.7  74   130 4.4  0      false(unreach-call) 8.7  4.6  150   330 true 8.1 4.4 130 320 - -
systemc/token_ring.03_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 79    79    1100   1200 4.4  0      false(unreach-call) 11    5.9  170   460 true 9.0 4.9 150 310 - -
systemc/token_ring.04_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 490    490    7000   14000 6.1  0      false(unreach-call) 15    7.6  180   490 true 11   6.0 130 320 - -
systemc/token_ring.05_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 490    490    6100   11000 6.1  0      false(unreach-call) 16    8.2  240   520 true 8.7 4.7 140 330 - -
systemc/token_ring.06_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 490    490    6000   8700 6.1  0      false(unreach-call) 20    10    230   720 true 11   6.0 110 330 - -
systemc/token_ring.07_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 490    490    6500   5900 6.2  0      false(unreach-call) 23    12    270   800 true 9.5 5.1 170 320 - -
systemc/token_ring.08_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 500    500    6000   6800 6.2  0      false(unreach-call) 23    12    310   860 true 9.6 5.2 150 320 - -
systemc/token_ring.09_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 500    500    6800   6800 6.3  0      false(unreach-call) 29    16    450   830 true 10   5.5 150 330 - -
systemc/token_ring.10_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 510    510    7100   7300 6.3  0      false(unreach-call) 31    16    470   870 true 9.9 5.3 170 340 - -
systemc/token_ring.11_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 520    520    6200   13000 6.4  0      false(unreach-call) 34    20    520   1000 true 11   5.9 160 340 - -
systemc/token_ring.12_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 520    520    6800   13000 6.4  0      false(unreach-call) 41    24    460   2200 true 11   5.7 180 380 - -
systemc/token_ring.13_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 530    530    6400   12000 6.5  0      false(unreach-call) 34    20    760   2100 true 12   6.7 150 360 - -
systemc/token_ring.14_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 520    520    6600   13000 6.4  0      false(unreach-call) 34    20    580   1100 true 9.9 5.4 210 360 - -
systemc/token_ring.15_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 530    530    6300   12000 6.5  0      false(unreach-call) 35    21    590   2100 true 13   7.0 120 360 - -
systemc/toy1_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect 480    480    4900   210 6.0  0      true 7.2  3.9  130   310 true 9.7 5.2 150 320 - -
systemc/toy2_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect 480    480    4900   250 6.0  0      true 6.8  3.6  130   290 true 10   5.4 100 320 - -
systemc/transmitter.01_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect 1.2  1.2  15   110 2.6  0      true 4.8  2.6  80   280 true 9.7 5.1 130 320 - -
systemc/transmitter.02_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect 2.4  2.4  30   110 2.6  0      true 5.6  3.0  74   290 true 8.2 4.4 160 310 - -
systemc/transmitter.03_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect 23    23    320   370 2.7  0      true 8.0  4.3  85   290 true 9.6 5.2 130 310 - -
systemc/transmitter.04_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect 480    480    5500   15000 3.5  0      true 7.5  4.0  140   310 true 8.2 4.4 130 300 - -
systemc/transmitter.05_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect 480    480    6100   14000 3.5  0      true 9.2  4.9  100   310 true 12   6.1 95 330 - -
systemc/transmitter.06_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect 480    480    6000   8900 3.6  0      true 10    5.3  110   320 true 12   6.5 140 340 - -
systemc/transmitter.07_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect 480    480    5700   3700 3.6  0      true 10    5.5  140   390 true 9.4 5.1 190 310 - -
systemc/transmitter.08_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect 480    480    6400   6700 3.6  0      true 11    6.0  100   460 true 9.6 5.2 160 330 - -
systemc/transmitter.09_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5500   7200 3.7  0      true 12    6.5  130   490 true 12   6.6 130 340 - -
systemc/transmitter.10_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5600   8200 3.9  0      true 12    6.4  230   530 true 9.9 5.3 140 330 - -
systemc/transmitter.11_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6200   9100 3.8  0      true 16    8.2  150   520 true 13   6.8 130 340 - -
systemc/transmitter.12_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect 490    490    5400   12000 3.8  0      true 16    8.4  180   550 true 12   6.4 160 350 - -
systemc/transmitter.13_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect 490    490    6100   13000 3.9  0      true 14    7.3  210   660 true 11   5.7 130 360 - -
systemc/transmitter.15_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 480    480    6700   13000 .91 0      false(unreach-call) 11    5.8  120   350 true 10   5.6 180 350 - -
systemc/transmitter.16_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 480    480    6500   12000 .91 0      false(unreach-call) 11    5.9  120   390 true 13   6.9 130 370 - -
systemc/bist_cell_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 900    900    12000   760 84    .041  - - error (invalid witness file) .55 .35 10   41 error (invalid witness file) 5.6 2.9 84 300
systemc/kundu_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 890    900    11000   320 19    0      - - error (invalid witness file) .66 .43 7.2 41 error (invalid witness file) 6.8 3.6 95 310
systemc/mem_slave_tlm.1_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 890    900    7900   1300 22    0      - - error (invalid witness file) .64 .41 7.4 39 error (invalid witness file) 5.7 3.0 73 310
systemc/mem_slave_tlm.2_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 900    900    10000   1500 22    0      - - error (invalid witness file) .51 .33 13   43 error (invalid witness file) 5.4 2.9 120 280
systemc/mem_slave_tlm.3_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 900    900    8700   1500 23    .21   - - error (invalid witness file) .66 .41 8.3 40 error (invalid witness file) 5.7 3.0 98 300
systemc/mem_slave_tlm.4_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 900    900    10000   1300 22    0      - - error (invalid witness file) .62 .39 9.3 40 error (invalid witness file) 5.7 3.1 94 300
systemc/mem_slave_tlm.5_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 900    900    9600   1200 19    0      - - error (invalid witness file) .48 .32 11   39 error (invalid witness file) 5.5 2.9 72 300
systemc/pc_sfifo_1_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 900    900    8600   480 39    0      - - error (invalid witness file) .53 .34 9.8 40 error (invalid witness file) 6.2 3.3 73 320
systemc/pc_sfifo_2_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 900    900    9400   470 38    0      - - error (invalid witness file) .57 .35 9.7 40 error (invalid witness file) 6.1 3.2 94 310
systemc/pc_sfifo_3_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 900    900    9400   940 49    0      - - error (invalid witness file) .61 .39 9.2 41 error (invalid witness file) 5.3 2.9 89 290
systemc/pipeline_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 900    900    9900   15000 18    0      - - error (invalid witness file) .52 .34 14   41 error (invalid witness file) 5.9 3.1 86 300
systemc/token_ring.01_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 900    900    9600   800 32    0      - - error (invalid witness file) .58 .38 9.2 40 error (invalid witness file) 5.5 2.9 63 300
systemc/token_ring.02_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 900    900    11000   590 22    0      - - error (invalid witness file) .63 .41 7.9 39 error (invalid witness file) 6.3 3.3 77 310
systemc/token_ring.03_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 890    900    14000   1200 17    0      - - error (invalid witness file) .58 .36 7.6 39 error (invalid witness file) 5.7 3.1 71 300
systemc/token_ring.04_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 900    900    10000   14000 19    0      - - error (invalid witness file) .53 .33 14   40 error (invalid witness file) 6.8 3.6 73 330
systemc/token_ring.05_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 890    900    11000   12000 16    0      - - error (invalid witness file) .55 .36 14   41 error (invalid witness file) 5.9 3.1 72 290
systemc/token_ring.06_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 890    900    11000   8700 14    0      - - error (invalid witness file) .52 .33 12   40 error (invalid witness file) 5.7 3.0 67 300
systemc/token_ring.07_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 890    900    11000   7200 14    0      - - error (invalid witness file) .59 .39 9.4 45 error (invalid witness file) 6.0 3.2 96 290
systemc/token_ring.08_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 890    900    10000   7200 14    0      - - error (invalid witness file) .51 .33 13   40 error (invalid witness file) 6.0 3.2 120 300
systemc/token_ring.09_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 890    900    10000   7800 13    33      - - error (invalid witness file) .49 .33 12   39 error (invalid witness file) 5.7 3.1 77 300
systemc/token_ring.10_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 890    900    11000   7300 12    0      - - error (invalid witness file) .61 .39 6.0 40 error (invalid witness file) 5.6 3.0 76 300
systemc/token_ring.11_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 890    900    10000   12000 11    0      - - error (invalid witness file) .59 .37 8.5 40 error (invalid witness file) 5.9 3.2 80 300
systemc/token_ring.12_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 890    900    9900   14000 11    0      - - error (invalid witness file) .50 .32 12   39 error (invalid witness file) 7.0 3.7 76 300
systemc/token_ring.13_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 890    900    12000   12000 11    0      - - error (invalid witness file) .51 .32 10   40 error (invalid witness file) 5.8 3.1 47 300
systemc/toy_true-unreach-call_false-termination.cil.c unknown 0 wit inspect 890    900    10000   250 19    0      - - error (invalid witness file) .66 .42 8.1 40 error (invalid witness file) 5.5 3.0 93 290
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c false(unreach-call) 1 wit inspect 1.3  1.3  15   86 .91 0      false(unreach-call) 9.6  5.1  140   340 true 12   6.3 130 340 - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect .90 .90 10   85 .89 0      false(unreach-call) 9.3  4.9  130   340 true 9.9 5.3 160 330 - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.BOUNDED-10.pals.c false(unreach-call) 0 wit inspect 2.7  2.6  39   86 3.5  0      timeout 98    73    2100   4300 true 12   6.4 120 340 - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 2.2  2.2  25   85 3.5  .13   timeout 93    75    2600   2800 true 10   5.5 160 330 - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_2.ufo.BOUNDED-10.pals.c false(unreach-call) 0 wit inspect 2.6  2.6  35   86 3.5  0      timeout 97    74    1300   4200 true 9.8 5.3 190 330 - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_2.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 2.2  2.2  25   85 3.5  .13   timeout 96    74    1300   2300 true 11   6.1 120 340 - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.5.ufo.BOUNDED-10.pals.c false(unreach-call) 0 wit inspect 5.4  5.4  80   87 7.9  0      timeout 96    73    1700   4300 true 11   5.6 140 340 - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.5.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 7.3  7.3  110   85 11    0      timeout 96    73    1400   2300 true 13   7.0 110 350 - -
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c false(unreach-call) 0 wit inspect 4.1  4.1  49   200 6.3  0      true 44    26    840   2500 timeout 97   64   1300 6900 - -
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 3.9  3.8  42   190 6.1  0      true 29    16    580   1600 true 12   6.1 200 460 - -
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.BOUNDED-10.pals_true-termination.c false(unreach-call) 0 wit inspect 4.1  4.1  58   190 6.1  0      true 47    28    860   2800 true 20   10   280 830 - -
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 3.9  3.9  55   200 6.1  0      true 38    21    400   1500 true 10   5.5 180 440 - -
seq-mthreaded/pals_floodmax.3_false-unreach-call.1.ufo.BOUNDED-6.pals_true-termination.c false(unreach-call) 0 wit inspect 6.4  6.3  86   86 8.6  0      true 17    8.9  150   460 true 9.7 5.2 170 330 - -
seq-mthreaded/pals_floodmax.3_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 5.5  5.5  78   85 8.6  0      true 47    29    620   2500 true 9.8 5.2 120 350 - -
seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.BOUNDED-6.pals_true-termination.c false(unreach-call) 0 wit inspect 2.3  2.3  32   85 2.6  0      true 17    8.9  180   510 true 13   6.8 120 350 - -
seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 2.3  2.3  26   85 3.5  0      timeout 97    74    1300   3100 true 10   5.5 160 330 - -
seq-mthreaded/pals_floodmax.3_false-unreach-call.3.ufo.BOUNDED-6.pals_true-termination.c false(unreach-call) 0 wit inspect 4.3  4.3  64   85 6.1  0      true 14    7.2  260   490 true 11   6.0 140 350 - -
seq-mthreaded/pals_floodmax.3_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 5.1  5.1  64   85 8.5  0      true 46    29    540   2400 true 8.6 4.7 160 330 - -
seq-mthreaded/pals_floodmax.3_false-unreach-call.4.ufo.BOUNDED-6.pals_true-termination.c false(unreach-call) 0 wit inspect 4.3  4.3  59   85 6.0  .045  true 18    9.1  220   510 true 11   5.9 130 350 - -
seq-mthreaded/pals_floodmax.3_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 5.0  5.0  55   85 8.5  .14   true 11    5.9  220   460 true 13   6.9 110 330 - -
seq-mthreaded/pals_floodmax.3_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c unknown 0 wit inspect 900    900    12000   230 90    0      error (invalid witness file) .51 .32 9.8 39 error (invalid witness file) 7.1 3.8 92 300 - -
seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c false(unreach-call) 0 wit inspect 14    14    210   99 9.6  0      true 39    21    440   1600 true 13   6.7 140 450 - -
seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 22    22    310   98 14    .27   timeout 97    67    1300   4500 true 15   7.9 150 440 - -
seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.BOUNDED-8.pals_true-termination.c false(unreach-call) 0 wit inspect 11    11    140   98 6.2  0      true 35    19    450   1600 true 12   6.6 180 480 - -
seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 13    13    170   100 8.6  0      true 57    35    630   3200 true 14   7.4 160 450 - -
seq-mthreaded/pals_floodmax.4_false-unreach-call.3.ufo.BOUNDED-8.pals_true-termination.c false(unreach-call) 0 wit inspect 17    17    200   98 9.7  0      true 34    18    300   1600 true 15   7.7 170 460 - -
seq-mthreaded/pals_floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 23    23    290   98 14    .090  true 49    30    770   3200 true 12   6.4 210 460 - -
seq-mthreaded/pals_floodmax.4_false-unreach-call.4.ufo.BOUNDED-8.pals_true-termination.c false(unreach-call) 0 wit inspect 19    19    220   98 9.6  0      true 32    17    650   1700 true 12   6.5 190 450 - -
seq-mthreaded/pals_floodmax.4_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 27    27    330   98 14    0      timeout 96    69    1800   4800 true 14   7.4 170 470 - -
seq-mthreaded/pals_floodmax.4_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c unknown 0 wit inspect 890    900    12000   150 26    0      error (invalid witness file) .48 .32 10   40 error (invalid witness file) 8.0 4.2 91 300 - -
seq-mthreaded/pals_floodmax.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c false(unreach-call) 0 wit inspect 61    61    730   150 13    0      true 78    56    2000   4100 true 14   7.6 210 500 - -
seq-mthreaded/pals_floodmax.5_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 96    96    1200   150 19    0      timeout (true) 91    65    1200   3500 true 13   7.2 160 490 - -
seq-mthreaded/pals_floodmax.5_false-unreach-call.2.ufo.BOUNDED-10.pals_true-termination.c false(unreach-call) 0 wit inspect 49    49    610   140 9.8  0      true 80    55    1100   2800 true 15   8.0 190 480 - -
seq-mthreaded/pals_floodmax.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 74    73    920   130 14    0      timeout 98    71    1600   3800 true 15   8.0 230 500 - -
seq-mthreaded/pals_floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals_true-termination.c false(unreach-call) 0 wit inspect 63    63    900   140 14    0      true 68    48    1500   4100 true 14   7.5 230 490 - -
seq-mthreaded/pals_floodmax.5_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 110    110    1300   150 19    .13   timeout 97    66    1400   3900 true 18   9.4 170 510 - -
seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.BOUNDED-10.pals_true-termination.c false(unreach-call) 0 wit inspect 92    92    1200   170 13    0      true 75    52    1400   4000 true 19   10   170 490 - -
seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 160    160    1900   190 19    0      timeout 97    67    1200   3800 true 14   7.4 230 490 - -
seq-mthreaded/pals_floodmax.5_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c unknown 0 wit inspect 890    900    10000   230 19    .098  error (invalid witness file) .65 .41 8.8 40 error (invalid witness file) 7.6 4.0 100 310 - -
seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.1.ufo.BOUNDED-6.pals_true-termination.c false(unreach-call) 0 wit inspect 4.2  4.2  59   81 9.4  0      true 9.7  5.1  130   330 true 9.6 5.1 150 330 - -
seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 5.9  5.9  82   81 14    .045  true 40    23    710   2000 true 8.1 4.4 140 320 - -
seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals_true-termination.c false(unreach-call) 0 wit inspect 4.2  4.2  55   81 9.4  0      true 7.7  4.1  140   330 true 8.4 4.5 160 320 - -
seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 5.8  5.8  90   80 14    0      true 36    19    410   1100 true 11   6.1 100 330 - -
seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c false(unreach-call) 0 wit inspect 7.4  7.4  100   83 13    0      true 12    6.3  140   400 true 9.2 4.9 160 330 - -
seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 11    11    140   85 19    0      true 58    35    740   2600 true 9.3 4.9 140 330 - -
seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.2.ufo.BOUNDED-8.pals_true-termination.c false(unreach-call) 0 wit inspect 11    11    140   83 19    0      true 10    5.4  150   340 true 8.2 4.4 150 320 - -
seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 11    11    130   82 19    0      true 36    20    550   1300 true 9.0 4.8 170 320 - -
seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c false(unreach-call) 0 wit inspect 22    22    270   86 24    0      true 12    6.3  190   480 true 11   5.7 140 320 - -
seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 22    22    260   86 24    0      true 69    42    830   3100 true 11   5.9 170 330 - -
seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.BOUNDED-10.pals_true-termination.c false(unreach-call) 0 wit inspect 22    22    290   86 24    0      true 11    5.8  140   380 true 10   5.3 190 330 - -
seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 23    23    300   85 24    0      true 46    27    430   1900 true 9.8 5.3 150 330 - -
seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.1.ufo.BOUNDED-12.pals_true-termination.c false(unreach-call) 0 wit inspect 47    47    630   89 29    .22   true 14    7.1  250   530 true 9.4 5.1 160 340 - -
seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 51    51    730   88 29    0      true 59    38    1200   3700 true 9.7 5.2 150 330 - -
seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.2.ufo.BOUNDED-12.pals_true-termination.c false(unreach-call) 0 wit inspect 27    27    330   88 20    0      true 12    6.1  200   490 true 9.4 5.0 160 330 - -
seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 48    48    720   87 29    0      true 72    50    1700   4400 true 8.4 4.6 93 320 - -
seq-mthreaded/pals_lcr.3_false-unreach-call.1.ufo.BOUNDED-6.pals_true-termination.c false(unreach-call) 0 wit inspect 3.9  3.9  61   79 9.4  0      true 6.3  3.4  130   300 true 9.0 4.8 120 330 - -
seq-mthreaded/pals_lcr.3_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 6.1  6.1  78   80 14    0      true 6.5  3.5  120   290 true 8.8 4.7 110 320 - -
seq-mthreaded/pals_lcr.3_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c unknown 0 wit inspect 900    900    11000   200 150    0      error (invalid witness file) .53 .34 11   39 error (invalid witness file) 6.3 3.3 130 310 - -
seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c false(unreach-call) 0 wit inspect 46    46    120   81 19    0      true 8.0  4.3  88   340 true 11   5.6 94 330 - -
seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 12    12    150   81 19    0      true 8.2  4.4  96   310 true 8.8 4.7 180 320 - -
seq-mthreaded/pals_lcr.4_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c unknown 0 wit inspect 890    900    13000   220 110    0      error (invalid witness file) .62 .39 11   42 error (invalid witness file) 5.7 3.1 79 300 - -
seq-mthreaded/pals_lcr.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c false(unreach-call) 0 wit inspect 21    21    310   86 24    0      true 7.7  4.1  150   360 true 8.8 4.7 170 330 - -
seq-mthreaded/pals_lcr.5_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 24    24    300   83 24    0      true 9.5  5.1  130   400 true 9.4 5.0 120 320 - -
seq-mthreaded/pals_lcr.5_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c unknown 0 wit inspect 890    900    9800   180 76    0      error (invalid witness file) .52 .32 12   41 error (invalid witness file) 6.0 3.2 120 300 - -
seq-mthreaded/pals_lcr.6_false-unreach-call.1.ufo.BOUNDED-12.pals_true-termination.c false(unreach-call) 0 wit inspect 45    44    620   86 29    0      true 8.7  4.7  180   380 true 8.7 4.6 110 320 - -
seq-mthreaded/pals_lcr.6_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 50    50    620   85 29    0      true 11    5.7  140   400 true 12   6.2 120 330 - -
seq-mthreaded/pals_lcr.6_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c unknown 0 wit inspect 890    900    13000   140 57    0      error (invalid witness file) .51 .33 12   39 error (invalid witness file) 7.7 4.1 77 300 - -
seq-mthreaded/pals_lcr.7_false-unreach-call.1.ufo.BOUNDED-14.pals_true-termination.c false(unreach-call) 0 wit inspect 100    100    1300   110 34    0      true 16    8.1  190   440 true 12   6.4 130 330 - -
seq-mthreaded/pals_lcr.7_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 110    110    1200   110 34    0      true 12    6.2  150   440 true 12   6.2 120 340 - -
seq-mthreaded/pals_lcr.7_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c unknown 0 wit inspect 890    900    11000   150 47    0      error (invalid witness file) .69 .44 8.0 43 error (invalid witness file) 8.4 4.4 97 320 - -
seq-mthreaded/pals_lcr.8_false-unreach-call.1.ufo.BOUNDED-16.pals_true-termination.c false(unreach-call) 0 wit inspect 54    54    700   100 27    0      true 14    7.2  220   560 true 10   5.3 200 360 - -
seq-mthreaded/pals_lcr.8_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 180    180    2400   130 39    0      true 14    7.5  130   550 true 11   5.6 190 350 - -
seq-mthreaded/pals_lcr.8_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c unknown 0 wit inspect 890    900    10000   150 44    0      error (invalid witness file) .54 .34 9.5 40 error (invalid witness file) 9.3 4.9 99 310 - -
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.1.ufo.BOUNDED-6.pals_true-termination.c false(unreach-call) 0 wit inspect 4.7  4.6  66   86 6.1  0      true 22    11    190   630 true 11   5.7 120 340 - -
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 6.0  6.0  69   86 8.7  0      true 35    20    620   1500 true 12   6.6 120 350 - -
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.2.ufo.BOUNDED-6.pals_true-termination.c false(unreach-call) 0 wit inspect 3.4  3.4  38   87 2.7  0      true 21    11    400   690 true 9.4 5.1 170 340 - -
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 2.4  2.4  33   86 3.5  0      true 66    44    1100   3100 true 9.7 5.2 180 350 - -
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.3.ufo.BOUNDED-6.pals_true-termination.c false(unreach-call) 0 wit inspect 5.1  5.1  69   87 6.1  .30   true 20    10    220   610 true 11   5.9 160 340 - -
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 5.9  5.9  77   86 8.6  0      true 72    47    1100   3100 true 11   5.8 98 360 - -
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.4.ufo.BOUNDED-6.pals_true-termination.c false(unreach-call) 0 wit inspect 5.5  5.4  74   87 6.1  0      true 19    9.7  210   550 true 11   6.1 140 350 - -
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 5.8  6.0  71   120 8.6  34      true 73    51    1700   3900 true 9.3 5.0 110 340 - -
seq-mthreaded/pals_opt-floodmax.3_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c unknown 0 wit inspect 900    900    10000   250 85    .17   error (invalid witness file) .63 .41 7.7 40 error (invalid witness file) 6.1 3.2 92 310 - -
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c false(unreach-call) 0 wit inspect 18    18    230   100 9.6  0      true 37    20    400   1600 true 11   5.9 180 470 - -
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 25    25    320   99 14    0      true 67    45    1300   3900 true 12   6.3 240 460 - -
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.2.ufo.BOUNDED-8.pals_true-termination.c false(unreach-call) 0 wit inspect 16    16    180   100 6.2  0      true 34    20    670   2000 true 12   6.3 220 460 - -
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 14    14    180   100 8.7  0      timeout 98    71    1300   3600 true 12   6.2 190 450 - -
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.3.ufo.BOUNDED-8.pals_true-termination.c false(unreach-call) 0 wit inspect 21    21    290   100 9.6  0      true 38    22    760   2100 true 12   6.3 210 480 - -
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 23    23    270   100 14    0      timeout 97    70    1700   4100 true 12   6.4 150 470 - -
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.4.ufo.BOUNDED-8.pals_true-termination.c false(unreach-call) 0 wit inspect 25    25    350   100 9.6  0      true 34    19    610   1700 true 13   6.9 120 480 - -
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 25    25    310   100 14    0      timeout 97    69    2000   3700 true 12   6.3 210 450 - -
seq-mthreaded/pals_opt-floodmax.4_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c unknown 0 wit inspect 890    900    11000   150 26    0      error (invalid witness file) .52 .33 12   42 error (invalid witness file) 6.6 3.5 75 300 - -
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c false(unreach-call) 0 wit inspect 64    64    940   140 13    0      true 76    57    2200   4300 true 17   9.0 240 500 - -
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 89    89    1100   160 19    0      timeout 98    67    1500   3100 true 14   7.8 270 500 - -
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.2.ufo.BOUNDED-10.pals_true-termination.c false(unreach-call) 0 wit inspect 46    46    590   130 9.8  0      timeout (true) 91    68    2200   3900 true 18   9.8 180 480 - -
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 68    68    830   130 14    0      timeout 98    70    1800   3100 true 17   9.4 190 490 - -
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals_true-termination.c false(unreach-call) 0 wit inspect 62    62    770   140 13    0      timeout 97    73    1600   4400 true 17   9.1 190 480 - -
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 98    98    1300   160 19    0      timeout 97    72    2200   3400 true 14   7.6 180 490 - -
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.4.ufo.BOUNDED-10.pals_true-termination.c false(unreach-call) 0 wit inspect 120    120    1500   220 13    34      timeout 96    71    1600   4200 true 17   9.1 150 490 - -
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(unreach-call) 0 wit inspect 140    140    1800   180 19    0      timeout 97    71    1500   4200 true 19   10   200 480 - -
seq-mthreaded/pals_opt-floodmax.5_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c unknown 0 wit inspect 890    900    12000   230 19    0      error (invalid witness file) .65 .41 7.9 43 error (invalid witness file) 6.3 3.4 130 310 - -
seq-mthreaded/rekcba_aso_false-unreach-call.1.M1.c unknown 0 wit inspect 890    900    9300   520 .95 0      error (invalid witness file) .71 .46 8.6 46 error (invalid witness file) 6.9 3.6 87 320 - -
seq-mthreaded/rekcba_aso_false-unreach-call.1.M4.c unknown 0 wit inspect 890    900    4900   5900 1.0  0      error (invalid witness file) .69 .44 6.7 39 error (invalid witness file) 6.9 3.6 140 310 - -
seq-mthreaded/rekcba_aso_false-unreach-call.2.M1.c unknown 0 wit inspect 890    900    9400   540 .95 0      error (invalid witness file) .65 .41 6.1 42 error (invalid witness file) 6.9 3.6 120 300 - -
seq-mthreaded/rekcba_aso_false-unreach-call.2.M4.c unknown 0 wit inspect 890    900    8400   6100 1.0  0      error (invalid witness file) .53 .33 11   42 error (invalid witness file) 7.1 3.7 150 310 - -
seq-mthreaded/rekcba_aso_false-unreach-call.3.M1.c unknown 0 wit inspect 890    900    11000   680 .97 .086  error (invalid witness file) .52 .34 9.8 40 error (invalid witness file) 6.0 3.2 110 300 - -
seq-mthreaded/rekcba_aso_false-unreach-call.3.M4.c unknown 0 wit inspect 890    900    8400   7200 1.1  0      error (invalid witness file) .66 .42 8.2 41 error (invalid witness file) 7.9 4.1 95 300 - -
seq-mthreaded/rekcba_aso_false-unreach-call.4.M1.c unknown 0 wit inspect 890    900    12000   680 .97 0      error (invalid witness file) .61 .39 7.4 39 error (invalid witness file) 6.3 3.4 110 300 - -
seq-mthreaded/rekcba_aso_false-unreach-call.4.M4.c unknown 0 wit inspect 890    900    8300   7100 1.1  0      error (invalid witness file) .52 .33 10   40 error (invalid witness file) 8.3 4.3 110 300 - -
seq-mthreaded/rekcba_ctm_false-unreach-call.2_true-termination.c unknown 0 wit inspect 890    900    6300   3700 1.0  0      error (invalid witness file) .52 .34 11   39 error (invalid witness file) 6.4 3.3 64 310 - -
seq-mthreaded/rekcba_ctm_false-unreach-call.3_true-termination.c unknown 0 wit inspect 890    900    7200   7500 1.1  0      error (invalid witness file) .58 .37 11   41 error (invalid witness file) 7.5 4.0 110 300 - -
seq-mthreaded/rekcba_nxt_false-unreach-call.1.M1.c unknown 0 wit inspect 890    900    9300   1500 2.6  0      error (invalid witness file) .50 .32 9.5 39 error (invalid witness file) 7.3 3.9 100 310 - -
seq-mthreaded/rekcba_nxt_false-unreach-call.1.M4.c unknown 0 wit inspect 900    900    7800   12000 1.0  0      error (invalid witness file) .64 .42 8.3 40 error (invalid witness file) 6.1 3.2 84 300 - -
seq-mthreaded/rekcba_nxt_false-unreach-call.2.M1.c unknown 0 wit inspect 890    900    8900   1900 2.6  .42   error (invalid witness file) .66 .43 8.0 41 error (invalid witness file) 8.1 4.3 76 300 - -
seq-mthreaded/rekcba_nxt_false-unreach-call.2.M4.c out of memory 0 wit inspect 17    17    140   15000 .19 .30   error (invalid witness file) .50 .32 11   40 error (invalid witness file) 7.2 3.8 99 310 - -
seq-mthreaded/rekh_aso_false-unreach-call.1.M1.c false(unreach-call) 0 wit inspect 600    600    7800   2000 1.5  0      timeout 97    76    2100   3900 true 42   26   480 820 - -
seq-mthreaded/rekh_aso_false-unreach-call.1.M4.c unknown 0 wit inspect 900    900    9000   5700 1.5  .086  error (invalid witness file) .61 .38 8.9 40 error (invalid witness file) 6.8 3.6 120 310 - -
seq-mthreaded/rekh_aso_false-unreach-call.2.M1.c false(unreach-call) 0 wit inspect 590    590    6500   1900 1.5  0      timeout 97    73    1200   3800 true 40   26   510 810 - -
seq-mthreaded/rekh_aso_false-unreach-call.2.M4.c unknown 0 wit inspect 890    900    8800   5900 1.5  0      error (invalid witness file) .59 .38 9.9 42 error (invalid witness file) 8.8 4.6 84 320 - -
seq-mthreaded/rekh_aso_false-unreach-call.4.M1.c false(unreach-call) 0 wit inspect 560    560    6600   2900 1.9  0      timeout 97    78    2800   3500 true 47   31   400 880 - -
seq-mthreaded/rekh_aso_false-unreach-call.4.M4.c unknown 0 wit inspect 900    900    9700   13000 2.0  0      error (invalid witness file) .56 .36 10   40 error (invalid witness file) 5.9 3.2 110 290 - -
seq-mthreaded/rekh_ctm_false-unreach-call.2_true-termination.c unknown 0 wit inspect 890    900    8900   2600 1.6  0      error (invalid witness file) .55 .35 11   40 error (invalid witness file) 6.2 3.3 92 300 - -
seq-mthreaded/rekh_ctm_false-unreach-call.3_true-termination.c unknown 0 wit inspect 890    900    8000   4000 1.7  0      error (invalid witness file) .54 .34 10   40 error (invalid witness file) 6.4 3.4 110 300 - -
seq-mthreaded/rekh_nxt_false-unreach-call.1.M1.c false(unreach-call) 0 wit inspect 660    660    8400   4200 7.5  0      timeout 97    69    2100   3900 true 32   22   490 840 - -
seq-mthreaded/rekh_nxt_false-unreach-call.1.M4.c out of memory 0 wit inspect 24    23    220   15000 .39 0      error (invalid witness file) .62 .40 8.1 40 error (invalid witness file) 6.4 3.4 130 300 - -
seq-mthreaded/rekh_nxt_false-unreach-call.2.M1.c false(unreach-call) 0 wit inspect 820    820    8100   4800 7.4  .21   timeout 97    70    2300   4400 true 39   25   480 810 - -
seq-mthreaded/rekh_nxt_false-unreach-call.2.M4.c out of memory 0 wit inspect 30    30    220   15000 .55 0      error (invalid witness file) .67 .43 7.8 40 error (invalid witness file) 7.9 4.1 93 310 - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_true-unreach-call.ufo.BOUNDED-10.pals.c true 2 wit inspect 170    160    2000   870 26    0      - - true 280    270    3800   950 out of memory 440   320   5400 7000
seq-mthreaded/pals_STARTPALS_ActiveStandby_true-unreach-call.ufo.UNBOUNDED.pals.c unknown 0 wit inspect 900    900    11000   410 160    0      - - error (invalid witness file) .54 .35 13   43 error (invalid witness file) 5.8 3.1 110 310
seq-mthreaded/pals_STARTPALS_Triplicated_true-unreach-call.ufo.BOUNDED-10.pals_true-termination.c true 2 wit inspect 48    31    520   1100 18    .0041 - - true 180    160    2600   2500 true 270   200   3700 4000
seq-mthreaded/pals_STARTPALS_Triplicated_true-unreach-call.ufo.UNBOUNDED.pals.c unknown 0 wit inspect 900    900    11000   530 130    0      - - error (invalid witness file) .53 .33 13   41 error (invalid witness file) 5.4 2.9 84 290
seq-mthreaded/pals_floodmax.3_true-unreach-call.ufo.BOUNDED-6.pals_true-termination.c true 2 wit inspect 310    260    2700   4100 11    0      - - true 25    18    360   560 out of memory 190   120   2200 7000
seq-mthreaded/pals_floodmax.3_true-unreach-call.ufo.UNBOUNDED.pals.c true 2 wit inspect 450    410    5000   4000 11    0      - - true 38    25    390   700 out of memory 160   100   1400 7000
seq-mthreaded/pals_floodmax.4_true-unreach-call.ufo.BOUNDED-8.pals_true-termination.c timeout 0 wit inspect 900    880    11000   2300 15    0      - - timeout 910    890    13000   810 out of memory 150   98   1200 7000
seq-mthreaded/pals_floodmax.4_true-unreach-call.ufo.UNBOUNDED.pals.c unknown 0 wit inspect 890    900    11000   99 15    .13   - - error (invalid witness file) .52 .33 10   40 error (invalid witness file) 5.8 3.1 92 300
seq-mthreaded/pals_floodmax.5_true-unreach-call.ufo.BOUNDED-10.pals_true-termination.c unknown 0 wit inspect 890    900    11000   230 13    0      - - error (invalid witness file) .66 .42 7.7 43 error (invalid witness file) 5.2 2.9 92 290
seq-mthreaded/pals_floodmax.5_true-unreach-call.ufo.UNBOUNDED.pals.c unknown 0 wit inspect 890    900    11000   230 19    0      - - error (invalid witness file) .62 .41 8.6 39 error (invalid witness file) 7.2 3.8 130 320
seq-mthreaded/pals_lcr-var-start-time.3_true-unreach-call.ufo.BOUNDED-6.pals_true-termination.c true 2 wit inspect 230    210    2800   850 16    0      - - true 16    9.8  180   430 out of memory 180   120   2300 7000
seq-mthreaded/pals_lcr-var-start-time.3_true-unreach-call.ufo.UNBOUNDED.pals.c true 2 wit inspect 260    230    2400   960 21    0      - - true 24    15    300   550 out of memory 180   120   1800 7000
seq-mthreaded/pals_lcr-var-start-time.4_true-unreach-call.ufo.BOUNDED-8.pals_true-termination.c true 2 wit inspect 270    230    3000   1300 21    .0041 - - true 40    33    760   570 out of memory 160   96   1300 7000
seq-mthreaded/pals_lcr-var-start-time.4_true-unreach-call.ufo.UNBOUNDED.pals.c true 2 wit inspect 370    320    4300   1500 26    0      - - true 53    42    790   770 out of memory 130   80   1600 7000
seq-mthreaded/pals_lcr-var-start-time.5_true-unreach-call.ufo.BOUNDED-10.pals_true-termination.c true 2 wit inspect 410    310    3900   4100 18    0      - - true 120    110    2300   690 out of memory 160   100   2300 7000
seq-mthreaded/pals_lcr-var-start-time.5_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 0 wit inspect 900    840    10000   3400 31    0      - - true 140    130    2400   710 out of memory 89   54   880 7000
seq-mthreaded/pals_lcr-var-start-time.6_true-unreach-call.ufo.BOUNDED-12.pals_true-termination.c timeout 0 wit inspect 900    630    9100   4500 32    .0041 - - timeout 900    890    12000   960 out of memory 190   120   1900 7000
seq-mthreaded/pals_lcr-var-start-time.6_true-unreach-call.ufo.UNBOUNDED.pals.c unknown 0 wit inspect 890    900    12000   150 36    0      - - error (invalid witness file) .62 .40 11   42 error (invalid witness file) 5.9 3.1 100 300
seq-mthreaded/pals_lcr.3_true-unreach-call.ufo.BOUNDED-6.pals_true-termination.c true 2 wit inspect 220    210    2200   840 11    0      - - true 12    6.9  180   410 timeout 960   870   15000 5400
seq-mthreaded/pals_lcr.3_true-unreach-call.ufo.UNBOUNDED.pals.c true 2 wit inspect 190    190    2300   890 21    0      - - true 13    8.1  300   390 timeout 960   890   14000 2000
seq-mthreaded/pals_lcr.4_true-unreach-call.ufo.BOUNDED-8.pals_true-termination.c true 2 wit inspect 240    220    2700   790 15    0      - - true 20    14    530   500 out of memory 180   120   1700 7000
seq-mthreaded/pals_lcr.4_true-unreach-call.ufo.UNBOUNDED.pals.c true 2 wit inspect 310    280    4300   1100 26    34      - - true 58    44    1300   1700 out of memory 190   130   2500 7000
seq-mthreaded/pals_lcr.5_true-unreach-call.ufo.BOUNDED-10.pals_true-termination.c true 2 wit inspect 290    250    3300   1600 18    0      - - true 47    40    1100   600 out of memory 190   130   2900 7000
seq-mthreaded/pals_lcr.5_true-unreach-call.ufo.UNBOUNDED.pals.c true 2 wit inspect 650    590    7300   2400 32    0      - - true 320    300    5100   4200 out of memory 150   94   2700 7000
seq-mthreaded/pals_lcr.6_true-unreach-call.ufo.BOUNDED-12.pals_true-termination.c true 2 wit inspect 460    360    5500   2200 31    .0041 - - true 120    110    1900   720 out of memory 200   130   3900 7000
seq-mthreaded/pals_lcr.6_true-unreach-call.ufo.UNBOUNDED.pals.c unknown 0 wit inspect 890    900    11000   150 36    0      - - true 210    200    3000   800 out of memory 200   130   3600 7000
seq-mthreaded/pals_lcr.7_true-unreach-call.ufo.BOUNDED-14.pals_true-termination.c true 2 wit inspect 870    620    10000   2800 25    0      - - true 580    560    9200   910 out of memory 220   150   4400 7000
seq-mthreaded/pals_lcr.7_true-unreach-call.ufo.UNBOUNDED.pals.c unknown 0 wit inspect 890    900    10000   170 41    0      - - error (invalid witness file) .52 .34 9.7 39 error (invalid witness file) 5.2 2.8 42 290
seq-mthreaded/pals_lcr.8_true-unreach-call.ufo.BOUNDED-16.pals_true-termination.c timeout 0 wit inspect 900    760    10000   3200 28    .34   - - timeout 900    890    17000   1200 out of memory 180   120   1300 7000
seq-mthreaded/pals_lcr.8_true-unreach-call.ufo.UNBOUNDED.pals.c unknown 0 wit inspect 890    900    9600   180 43    0      - - error (invalid witness file) .61 .38 12   42 error (invalid witness file) 6.0 3.2 79 310
seq-mthreaded/pals_opt-floodmax.3_true-unreach-call.ufo.BOUNDED-6.pals_true-termination.c true 2 wit inspect 340    310    4300   3800 11    0      - - true 28    20    440   570 out of memory 190   120   1400 7000
seq-mthreaded/pals_opt-floodmax.3_true-unreach-call.ufo.UNBOUNDED.pals.c true 2 wit inspect 380    350    3600   3800 11    .0041 - - true 28    18    550   550 out of memory 160   98   1400 7000
seq-mthreaded/pals_opt-floodmax.4_true-unreach-call.ufo.BOUNDED-8.pals_true-termination.c timeout 0 wit inspect 900    830    10000   2800 15    0      - - timeout 910    890    12000   770 out of memory 160   100   2100 7000
seq-mthreaded/pals_opt-floodmax.4_true-unreach-call.ufo.UNBOUNDED.pals.c unknown 0 wit inspect 890    900    12000   100 15    0      - - error (invalid witness file) .61 .40 7.3 39 error (invalid witness file) 6.0 3.2 100 300
seq-mthreaded/pals_opt-floodmax.5_true-unreach-call.ufo.BOUNDED-10.pals_true-termination.c unknown 0 wit inspect 890    900    10000   230 13    0      - - error (invalid witness file) .53 .32 11   39 error (invalid witness file) 5.8 3.1 90 300
seq-mthreaded/pals_opt-floodmax.5_true-unreach-call.ufo.UNBOUNDED.pals.c unknown 0 wit inspect 890    900    10000   230 19    0      - - error (invalid witness file) .63 .40 10   43 error (invalid witness file) 6.1 3.2 100 300
seq-mthreaded/rekcba_aso_true-unreach-call.1.M1.c unknown 0 wit inspect 890    900    12000   530 .95 0      - - error (invalid witness file) .59 .38 8.4 39 error (invalid witness file) 8.7 4.5 93 300
seq-mthreaded/rekcba_aso_true-unreach-call.1.M4.c unknown 0 wit inspect 890    900    8500   5900 1.0  0      - - error (invalid witness file) .55 .35 14   40 error (invalid witness file) 7.2 3.8 110 310
seq-mthreaded/rekcba_aso_true-unreach-call.2.M1.c unknown 0 wit inspect 890    900    11000   670 .97 0      - - error (invalid witness file) .58 .36 9.8 40 error (invalid witness file) 6.0 3.2 110 300
seq-mthreaded/rekcba_aso_true-unreach-call.2.M4.c unknown 0 wit inspect 890    900    11000   7200 1.1  0      - - error (invalid witness file) .57 .37 7.3 40 error (invalid witness file) 6.7 3.5 70 300
seq-mthreaded/rekcba_ctm_true-unreach-call.1_true-termination.c unknown 0 wit inspect 890    900    8500   3900 1.0  0      - - error (invalid witness file) .57 .36 9.1 40 error (invalid witness file) 6.4 3.4 87 300
seq-mthreaded/rekcba_ctm_true-unreach-call.2_true-termination.c unknown 0 wit inspect 890    900    6800   3900 1.0  0      - - error (invalid witness file) .64 .41 8.1 39 error (invalid witness file) 7.1 3.7 120 320
seq-mthreaded/rekcba_ctm_true-unreach-call.3_true-termination.c unknown 0 wit inspect 890    900    6100   7500 1.1  0      - - error (invalid witness file) .52 .34 13   40 error (invalid witness file) 6.1 3.3 77 290
seq-mthreaded/rekcba_ctm_true-unreach-call.4_true-termination.c unknown 0 wit inspect 890    900    8700   12000 1.1  0      - - error (invalid witness file) .62 .39 11   43 error (invalid witness file) 7.0 3.7 110 310
seq-mthreaded/rekcba_nxt_true-unreach-call.1.M1.c unknown 0 wit inspect 890    900    9500   1500 2.6  0      - - error (invalid witness file) .66 .42 8.9 41 error (invalid witness file) 6.3 3.4 55 290
seq-mthreaded/rekcba_nxt_true-unreach-call.1.M4.c unknown 0 wit inspect 890    900    11000   12000 1.0  0      - - error (invalid witness file) .64 .41 7.5 40 error (invalid witness file) 6.6 3.5 110 300
seq-mthreaded/rekcba_nxt_true-unreach-call.2.M1.c unknown 0 wit inspect 890    900    8700   1600 2.6  0      - - error (invalid witness file) .60 .39 7.8 41 error (invalid witness file) 6.1 3.2 75 310
seq-mthreaded/rekcba_nxt_true-unreach-call.2.M4.c unknown 0 wit inspect 890    900    9400   13000 1.0  0      - - error (invalid witness file) .51 .33 11   40 error (invalid witness file) 6.2 3.3 98 290
seq-mthreaded/rekcba_nxt_true-unreach-call.3.M1.c unknown 0 wit inspect 890    900    9700   1900 2.8  0      - - error (invalid witness file) .52 .33 11   42 error (invalid witness file) 5.8 3.1 67 300
seq-mthreaded/rekcba_nxt_true-unreach-call.3.M4.c out of memory 0 wit inspect 17    17    140   15000 .19 .39   - - error (invalid witness file) .65 .42 7.9 41 error (invalid witness file) 6.3 3.3 73 300
seq-mthreaded/rekh_aso_true-unreach-call.1.M1.c timeout 0 wit inspect 900    810    8700   11000 4.2  0      - - out of memory 180    110    2400   7000 error 220   190   2900 1800
seq-mthreaded/rekh_aso_true-unreach-call.1.M4.c unknown 0 wit inspect 890    900    9800   5700 1.5  .086  - - error (invalid witness file) .49 .31 12   40 error (invalid witness file) 8.4 4.4 78 300
seq-mthreaded/rekh_aso_true-unreach-call.2.M1.c false(unreach-call) -16 wit inspect 610    610    6100   2900 1.9  0      - - timeout 960    890    20000   7000 true 41   27   520 900
seq-mthreaded/rekh_aso_true-unreach-call.2.M4.c unknown 0 wit inspect 900    900    7700   13000 2.0  0      - - error (invalid witness file) .55 .35 9.2 40 error (invalid witness file) 7.5 3.9 160 300
seq-mthreaded/rekh_aso_true-unreach-call.3.M1.c false(unreach-call) -16 wit inspect 700    700    8000   2900 1.9  0      - - timeout 920    840    15000   5400 true 44   29   580 860
seq-mthreaded/rekh_aso_true-unreach-call.3.M4.c unknown 0 wit inspect 900    900    9300   13000 1.9  0      - - error (invalid witness file) .47 .31 11   40 error (invalid witness file) 6.2 3.3 110 300
seq-mthreaded/rekh_ctm_true-unreach-call.1_true-termination.c unknown 0 wit inspect 890    900    7000   2700 1.6  35      - - error (invalid witness file) .68 .43 8.8 39 error (invalid witness file) 6.3 3.3 90 300
seq-mthreaded/rekh_ctm_true-unreach-call.2_true-termination.c unknown 0 wit inspect 900    900    8200   2600 1.6  0      - - error (invalid witness file) .63 .41 8.9 40 error (invalid witness file) 6.1 3.2 100 300
seq-mthreaded/rekh_ctm_true-unreach-call.3_true-termination.c unknown 0 wit inspect 890    900    6100   4100 1.7  0      - - error (invalid witness file) .60 .39 9.3 41 error (invalid witness file) 6.3 3.3 100 300
seq-mthreaded/rekh_ctm_true-unreach-call.4_true-termination.c unknown 0 wit inspect 890    900    5100   5100 1.7  .086  - - error (invalid witness file) .62 .39 6.3 40 error (invalid witness file) 6.0 3.2 78 300
seq-mthreaded/rekh_nxt_true-unreach-call.1.M1.c timeout 0 wit inspect 900    810    9300   6200 4.0  .34   - - out of memory 100    72    1300   7000 out of memory 730   690   8200 7000
seq-mthreaded/rekh_nxt_true-unreach-call.1.M4.c out of memory 0 wit inspect 24    23    200   15000 .39 .21   - - error (invalid witness file) .55 .35 12   42 error (invalid witness file) 6.4 3.4 96 300
seq-mthreaded/rekh_nxt_true-unreach-call.2.M1.c timeout 0 wit inspect 900    750    10000   12000 3.9  0      - - out of memory 79    56    1000   7000 timeout 960   930   18000 1400
seq-mthreaded/rekh_nxt_true-unreach-call.2.M4.c out of memory 0 wit inspect 24    23    180   15000 .40 0      - - error (invalid witness file) .50 .32 12   39 error (invalid witness file) 6.0 3.2 47 310
seq-mthreaded/rekh_nxt_true-unreach-call.3.M1.c timeout 0 wit inspect 900    810    9300   11000 4.1  0      - - out of memory 110    70    2000   7000 timeout 960   940   15000 1500
seq-mthreaded/rekh_nxt_true-unreach-call.3.M4.c out of memory 0 wit inspect 28    28    200   15000 .55 0      - - error (invalid witness file) .64 .40 5.8 39 error (invalid witness file) 5.9 3.1 62 300
seq-pthread/cs_fib_false-unreach-call.i unknown 0 wit inspect 890    900    9700   120 12    0      error (invalid witness file) .68 .43 8.7 41 error (invalid witness file) 6.6 3.5 94 300 - -
seq-pthread/cs_fib_longer_false-unreach-call.i unknown 0 wit inspect 890    900    12000   160 11    0      error (invalid witness file) .56 .36 10   40 error (invalid witness file) 6.2 3.3 120 300 - -
seq-pthread/cs_lazy_false-unreach-call.i unknown 0 wit inspect 47    47    630   65 84    0      error (invalid witness file) .66 .43 8.8 40 error (invalid witness file) 5.8 3.1 130 300 - -
seq-pthread/cs_queue_false-unreach-call.i unknown 0 wit inspect 890    900    11000   640 25    .41   error (invalid witness file) .48 .31 11   39 error (invalid witness file) 6.6 3.5 110 300 - -
seq-pthread/cs_read_write_lock_false-unreach-call.i false(unreach-call) 0 wit inspect 17    17    180   150 .93 0      timeout 96    78    1500   2800 error 13   6.7 220 320 - -
seq-pthread/cs_stack_false-unreach-call.i unknown 0 wit inspect 140    140    2000   89 84    0      error (invalid witness file) .64 .40 7.7 39 error (invalid witness file) 6.4 3.3 96 300 - -
seq-pthread/cs_stateful_false-unreach-call.i unknown 0 wit inspect 44    44    560   66 84    0      error (invalid witness file) .64 .40 8.2 44 error (invalid witness file) 5.6 3.0 110 290 - -
seq-pthread/cs_dekker_true-unreach-call.i unknown 0 wit inspect 890    900    8900   2800 4.3  0      - - true 460    440    4500   1800 timeout 960   930   18000 2700
seq-pthread/cs_fib_longer_true-unreach-call.i unknown 0 wit inspect 890    900    10000   390 16    0      - - error (invalid witness file) .58 .36 9.8 41 error (invalid witness file) 6.3 3.3 130 300
seq-pthread/cs_fib_true-unreach-call.i unknown 0 wit inspect 890    900    9700   450 15    .13   - - error (invalid witness file) .67 .41 7.6 39 error (invalid witness file) 5.7 3.1 74 300
seq-pthread/cs_lamport_true-unreach-call.i unknown 0 wit inspect 890    900    9000   420 7.8  0      - - error (invalid witness file) .49 .32 11   41 error (invalid witness file) 6.2 3.2 84 300
seq-pthread/cs_peterson_true-unreach-call.i true 2 wit inspect 120    120    1500   220 4.4  .13   - - true 320    310    2700   1600 timeout 960   930   11000 2600
seq-pthread/cs_queue_true-unreach-call.i unknown 0 wit inspect 900    900    11000   610 68    .87   - - error (invalid witness file) .56 .36 13   44 error (invalid witness file) 5.5 3.0 100 290
seq-pthread/cs_read_write_lock_true-unreach-call.i true 1 wit inspect 28    28    340   130 4.4  0      - - timeout 900    880    12000   2900 error 12   6.2 120 310
seq-pthread/cs_stack_true-unreach-call.i unknown 0 wit inspect 150    150    1800   150 94    0      - - error (invalid witness file) .51 .31 12   39 error (invalid witness file) 6.1 3.2 65 310
seq-pthread/cs_stateful_true-unreach-call.i unknown 0 wit inspect 48    48    610   120 90    0      - - error (invalid witness file) .63 .41 7.1 39 error (invalid witness file) 5.9 3.2 100 300
seq-pthread/cs_sync_true-unreach-call.i true 1 wit inspect 210    210    1700   780 9.5  0      - - timeout 910    870    15000   6500 timeout 960   920   15000 3000
seq-pthread/cs_szymanski_true-unreach-call.i unknown 0 wit inspect 890    900    7600   570 4.4  0      - - true 370    350    6800   1500 timeout 960   930   20000 2700
seq-pthread/cs_time_var_mutex_true-unreach-call.i true 1 wit inspect 24    24    320   130 4.4  0      - - timeout 900    890    15000   2000 timeout 960   930   11000 2800
../../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 273 33 120000 120000 1400000 840000 4400   180   273 5600 3700 95000 240000   273 2000 1100 27000 70000   273 12000 12000 190000 83000   273 14000 12000 210000 210000  
    correct results 42 62 14000 13000 170000 200000 480   34   22 440 240 6400 18000   22 230 120 3200 7400   20 2300 2100 35000 20000   1 6200 4900 83000 130000  
        correct true 20 40 6600 5600 74000 39000 380   34   0 0 0 0 0   22 0 0 0 0   20 2300 2100 35000 20000   1 6200 4900 83000 130000  
        correct false 22 22 7700 7700 99000 170000 110   0   22 440 240 6400 18000   0 230 120 3200 7400   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 112 3 13000 13000 160000 130000 1300   69   80 5100 3500 88000 220000   107 1500 830 20000 51000   0 2700 2600 43000 11000   0 1900 1900 26000 6100  
        correct-unconfirmed true 3 3 260 260 2400 1000 18   0   80 0 0 0 0   107 0 0 0 0   0 2700 2600 43000 11000   0 1900 1900 26000 6100  
        correct-unconfirmed false 109 0 13000 13000 150000 120000 1300   69   0 5100 3500 88000 220000   0 1500 830 20000 51000   0 0 0 0 0   0 0 0 0 0  
    incorrect results 2 -32 1300 1300 14000 5800 3.9 0   0 0 0 0 0   0 0 0 0 0   0 1900 1700 35000 12000   2 85 56 1100 1800  
        incorrect true 0
        incorrect false 2 -32 1300 1300 14000 5800 3.9 0   0 0 0 0 0   0 0 0 0 0   0 1900 1700 35000 12000   0 85 56 1100 1800  
score (273 tasks, max score: 376) 33
Run set sv-comp17.ReachSafety-Sequentialized