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