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