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