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