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-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-11 11:18:39 CET [[ 2017-01-14 21:32:33 CET ]] [[ 2017-01-14 22:21:46 CET ]] [[ 2017-01-14 21:35:07 CET ]] [[ 2017-01-14 22:35:09 CET ]]
Run set sv-comp17.ReachSafety-Sequentialized
Options -sv-comp17 -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-11_1118.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 4.9 1.7 41 280 .053  0      false(unreach-call) 8.1  4.3  130   320 false(unreach-call) 19   9.8 320 710 - -
systemc/kundu2_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 5.0 1.6 42 290 .045  0      false(unreach-call) 8.1  4.3  160   350 false(unreach-call) 32   17   580 800 - -
systemc/pc_sfifo_1_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 2.8 1.1 27 260 .0082 0      false(unreach-call) 4.8  2.6  97   280 false(unreach-call) 8.9 4.7 180 320 - -
systemc/pc_sfifo_2_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 3.0 1.2 27 260 .016  0      false(unreach-call) 5.3  2.9  100   280 false(unreach-call) 18   9.8 200 460 - -
systemc/pipeline_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 30   17   280 1700 .25   0      false(unreach-call) 17    9.1  320   720 timeout 97   56   1500 5400 - -
systemc/token_ring.01_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 7.9 2.5 56 360 .086  0      false(unreach-call) 6.5  3.5  130   290 false(unreach-call) 27   14   330 580 - -
systemc/token_ring.02_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 11   3.4 95 470 .13   0      false(unreach-call) 7.7  4.1  120   310 false(unreach-call) 45   24   430 840 - -
systemc/token_ring.03_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 14   4.5 120 580 .18   0      false(unreach-call) 9.3  4.9  140   340 false(unreach-call) 53   28   620 1100 - -
systemc/token_ring.04_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 24   11   230 1100 .24   0      false(unreach-call) 10    5.2  150   430 false(unreach-call) 78   41   770 1600 - -
systemc/token_ring.05_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 68   44   650 3500 .31   0      false(unreach-call) 11    5.7  210   440 timeout (false(unreach-call)) 92   50   1400 2400 - -
systemc/token_ring.06_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 83   55   750 4200 .25   0      false(unreach-call) 13    7.1  260   480 timeout 97   53   1100 3000 - -
systemc/token_ring.07_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 100   67   990 4500 .32   0      false(unreach-call) 16    8.5  250   560 timeout 97   53   1300 3200 - -
systemc/token_ring.08_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 150   110   1500 4600 .38   0      false(unreach-call) 16    8.4  330   700 timeout 98   55   1200 4200 - -
systemc/token_ring.09_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 270   230   2900 3500 .23   0      false(unreach-call) 19    10    370   710 timeout 98   55   1100 4200 - -
systemc/token_ring.10_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect 420   330   4200 4200 .97   .0041 timeout 96    75    1500   4500 true 64   34   870 1100 - -
systemc/token_ring.11_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect 420   330   4800 3900 1.1    .0041 timeout 96    75    2800   4500 true 88   49   1400 1700 - -
systemc/token_ring.12_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect 420   340   4000 3600 1.2    .0041 timeout 97    75    1700   4500 timeout 96   54   1400 1600 - -
systemc/token_ring.13_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect 430   340   4800 3700 1.4    .0041 timeout 97    75    2400   4400 true 80   45   1800 1800 - -
systemc/token_ring.14_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect 430   340   4100 4000 1.2    0      timeout 97    76    1900   4700 timeout 97   53   1100 1400 - -
systemc/token_ring.15_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect 430   340   4100 3900 1.4    .0041 timeout 96    75    2400   4500 timeout 96   54   940 1700 - -
systemc/toy1_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 5.3 1.7 42 280 .049  0      false(unreach-call) 7.9  4.2  130   310 false(unreach-call) 36   18   410 840 - -
systemc/toy2_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 5.2 1.7 45 280 .049  0      false(unreach-call) 8.1  4.3  120   320 false(unreach-call) 35   19   510 850 - -
systemc/transmitter.01_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 3.6 1.3 29 270 .025  0      false(unreach-call) 5.5  2.9  80   290 false(unreach-call) 26   14   280 550 - -
systemc/transmitter.02_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.3 1.5 33 270 .033  0      false(unreach-call) 6.8  3.7  140   290 false(unreach-call) 35   19   370 700 - -
systemc/transmitter.03_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 5.5 1.7 42 290 .049  0      false(unreach-call) 7.9  4.2  140   300 false(unreach-call) 46   25   480 1300 - -
systemc/transmitter.04_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 7.2 2.1 52 290 .066  0      false(unreach-call) 9.2  4.8  170   370 false(unreach-call) 58   31   860 1200 - -
systemc/transmitter.05_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 9.4 2.7 81 360 .090  0      false(unreach-call) 11    5.7  180   450 false(unreach-call) 72   39   1100 2400 - -
systemc/transmitter.06_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 12   4.4 96 520 .11   0      false(unreach-call) 12    6.5  240   460 false(unreach-call) 83   46   1300 2900 - -
systemc/transmitter.07_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 19   10   190 850 .14   0      false(unreach-call) 14    7.2  230   480 timeout 97   53   1700 3800 - -
systemc/transmitter.08_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 48   36   480 2400 .17   0      false(unreach-call) 15    8.0  230   490 timeout 97   53   1700 3900 - -
systemc/transmitter.09_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 160   120   1600 2600 .20   0      false(unreach-call) 15    8.2  300   670 timeout 97   53   1100 3400 - -
systemc/transmitter.10_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 160   130   1900 2300 .25   .0041 false(unreach-call) 17    9.1  330   730 timeout 97   57   1800 4600 - -
systemc/transmitter.11_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 170   130   1600 2700 .29   0      false(unreach-call) 19    10    400   800 timeout 97   55   990 4600 - -
systemc/transmitter.12_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 170   130   1700 2800 .34   .0041 false(unreach-call) 25    13    360   950 timeout 97   58   2000 4600 - -
systemc/transmitter.13_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 180   140   1900 2900 .39   0      false(unreach-call) 25    13    490   860 timeout 96   54   930 4600 - -
systemc/transmitter.15_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.7 1.6 38 280 .045  0      false(unreach-call) 9.1  4.8  170   360 timeout (false(unreach-call)) 97   54   930 1400 - -
systemc/transmitter.16_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.9 1.6 40 280 .049  0      false(unreach-call) 8.7  4.6  170   380 timeout (false(unreach-call)) 95   53   1100 1600 - -
systemc/bist_cell_true-unreach-call_false-termination.cil.c true 2 wit inspect 2.9 1.1 25 260 0      0      - - out of memory 420    370    6300   7000 true 68   38   580 1400
systemc/kundu_true-unreach-call_false-termination.cil.c true 1 wit inspect 10   3.5 75 520 0      0      - - timeout 910    890    18000   4600 out of memory 160   100   2500 7000
systemc/mem_slave_tlm.1_true-unreach-call_false-termination.cil.c true 2 wit inspect 3.7 1.3 30 270 0      0      - - timeout 910    870    16000   5100 true 200   140   1800 6900
systemc/mem_slave_tlm.2_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.1 1.4 31 260 0      0      - - timeout 910    880    30000   5100 true 230   160   2200 6900
systemc/mem_slave_tlm.3_true-unreach-call_false-termination.cil.c true 1 wit inspect 4.0 1.3 35 260 0      0      - - timeout 910    870    21000   5100 out of memory 170   120   2500 7000
systemc/mem_slave_tlm.4_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.3 1.4 33 270 0      0      - - timeout 910    870    19000   5100 true 310   220   4600 6900
systemc/mem_slave_tlm.5_true-unreach-call_false-termination.cil.c true 1 wit inspect 4.4 1.4 35 270 0      0      - - timeout 910    870    16000   5200 out of memory 150   100   1800 7000
systemc/pc_sfifo_1_true-unreach-call_false-termination.cil.c true 2 wit inspect 8.5 2.9 70 440 .041  0      - - out of memory 770    710    18000   7000 true 31   17   440 660
systemc/pc_sfifo_2_true-unreach-call_false-termination.cil.c true 2 wit inspect 11   4.0 110 450 .041  0      - - out of memory 720    650    18000   7000 true 59   32   520 1300
systemc/pc_sfifo_3_true-unreach-call_false-termination.cil.c true 2 wit inspect 3.1 1.2 25 250 0      0      - - timeout 900    880    17000   5600 true 25   14   510 550
systemc/pipeline_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 960   610   12000 4400 .25   0      - - out of memory 700    660    17000   7000 false(unreach-call) 44   24   350 1100
systemc/token_ring.01_true-unreach-call_false-termination.cil.c true 2 wit inspect 7.8 2.5 65 380 .061  0      - - out of memory 770    730    16000   7000 true 34   18   540 730
systemc/token_ring.02_true-unreach-call_false-termination.cil.c true 2 wit inspect 15   5.5 120 480 .090  0      - - timeout 900    880    18000   4600 true 73   39   590 1000
systemc/token_ring.03_true-unreach-call_false-termination.cil.c true 2 wit inspect 19   8.1 160 610 .12   0      - - timeout 900    880    15000   2800 true 75   41   590 1600
systemc/token_ring.04_true-unreach-call_false-termination.cil.c true 2 wit inspect 31   18   300 1200 .16   0      - - timeout 900    890    17000   2600 true 100   57   1100 2800
systemc/token_ring.05_true-unreach-call_false-termination.cil.c true 1 wit inspect 130   110   1500 3700 .21   0      - - timeout 900    880    14000   3200 out of memory 170   110   2400 7000
systemc/token_ring.06_true-unreach-call_false-termination.cil.c true 2 wit inspect 180   140   1900 4400 .13   0      - - timeout 900    890    17000   2800 true 160   99   2000 6500
systemc/token_ring.07_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 920   540   8000 5800 .15   0      - - timeout 910    880    17000   6200 false(unreach-call) 110   69   1600 4700
systemc/token_ring.08_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 920   540   7300 5900 .18   0      - - timeout 910    880    21000   6200 false(unreach-call) 110   64   1100 3400
systemc/token_ring.09_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 940   570   8300 6100 0      0      - - out of memory 880    860    15000   7000 out of memory 240   150   2900 7000
systemc/token_ring.10_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 960   570   7600 6100 0      0      - - out of memory 570    550    13000   7000 out of memory 290   190   3700 7000
systemc/token_ring.11_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 960   580   8600 6500 0      0      - - error (invalid witness file) .69 .43 9.7 44 error (invalid witness file) 5.6 3.0 120 290
systemc/token_ring.12_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 960   570   9100 6800 0      0      - - error (invalid witness file) .54 .35 12   41 error (invalid witness file) 6.0 3.2 140 300
systemc/token_ring.13_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 920   520   8900 7500 0      0      - - out of memory 570    550    14000   7000 out of memory 190   120   4500 7000
systemc/toy_true-unreach-call_false-termination.cil.c true 2 wit inspect 190   160   2000 4300 0      0      - - out of memory 460    420    8600   7000 true 120   77   1100 3300
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c false(unreach-call) 1 wit inspect 5.6 1.7 42 300 .037  0      false(unreach-call) 7.8  4.2  150   340 false(unreach-call) 15   8.0 160 430 - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 5.7 1.7 44 300 .037  0      false(unreach-call) 7.9  4.2  150   330 false(unreach-call) 16   8.6 160 420 - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.BOUNDED-10.pals.c false(unreach-call) 1 wit inspect 270   260   2700 1800 .19   0      false(unreach-call) 10    5.4  230   440 false(unreach-call) 20   11   240 540 - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 260   250   2900 1800 .19   0      false(unreach-call) 10    5.5  180   430 false(unreach-call) 20   10   210 550 - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_2.ufo.BOUNDED-10.pals.c false(unreach-call) 1 wit inspect 270   260   3000 1800 .19   0      false(unreach-call) 10    5.4  210   440 false(unreach-call) 19   9.7 260 580 - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_2.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 270   260   3300 1800 .19   0      false(unreach-call) 11    5.7  130   390 false(unreach-call) 21   11   240 600 - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.5.ufo.BOUNDED-10.pals.c timeout 0 wit inspect 960   950   7400 1700 .35   0      error (invalid witness file) .51 .33 14   39 error (invalid witness file) 7.7 4.0 86 300 - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.5.ufo.UNBOUNDED.pals.c timeout 0 wit inspect 960   950   5400 1700 .35   0      error (invalid witness file) .56 .37 4.4 43 error (invalid witness file) 7.1 3.8 81 300 - -
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c false(unreach-call) 1 wit inspect 35   18   310 1300 .38   0      false(unreach-call) 12    6.1  240   490 false(unreach-call) 24   12   260 840 - -
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 35   18   330 1200 .38   0      false(unreach-call) 10    5.5  140   460 false(unreach-call) 22   11   320 850 - -
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.BOUNDED-10.pals_true-termination.c false(unreach-call) 1 wit inspect 35   18   320 1200 .38   0      false(unreach-call) 12    6.2  230   490 false(unreach-call) 35   19   360 940 - -
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 32   18   310 1200 .38   0      false(unreach-call) 11    5.9  210   460 false(unreach-call) 32   17   370 830 - -
seq-mthreaded/pals_floodmax.3_false-unreach-call.1.ufo.BOUNDED-6.pals_true-termination.c false(unreach-call) 1 wit inspect 65   45   670 3800 .19   0      false(unreach-call) 10    5.3  170   370 true 9.6 5.1 99 320 - -
seq-mthreaded/pals_floodmax.3_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 59   41   590 3800 .20   0      false(unreach-call) 9.8  5.2  140   410 true 11   5.7 140 320 - -
seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.BOUNDED-6.pals_true-termination.c false(unreach-call) 1 wit inspect 27   12   230 1700 .14   0      false(unreach-call) 8.6  4.6  170   320 false(unreach-call) 76   54   1200 990 - -
seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 28   13   250 1800 .14   0      false(unreach-call) 9.8  5.2  150   350 false(unreach-call) 86   71   1300 810 - -
seq-mthreaded/pals_floodmax.3_false-unreach-call.3.ufo.BOUNDED-6.pals_true-termination.c false(unreach-call) 1 wit inspect 68   47   640 3800 .21   0      false(unreach-call) 9.7  5.1  200   400 false(unreach-call) 53   36   1000 920 - -
seq-mthreaded/pals_floodmax.3_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 62   42   630 3800 .21   0      false(unreach-call) 11    5.8  200   420 timeout 96   71   1700 1300 - -
seq-mthreaded/pals_floodmax.3_false-unreach-call.4.ufo.BOUNDED-6.pals_true-termination.c false(unreach-call) 1 wit inspect 59   39   580 3800 .21   0      false(unreach-call) 10    5.5  200   410 timeout 96   74   1600 860 - -
seq-mthreaded/pals_floodmax.3_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 55   36   530 3800 .21   0      false(unreach-call) 11    5.6  200   430 timeout 97   72   1300 950 - -
seq-mthreaded/pals_floodmax.3_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c timeout 0 wit inspect 910   550   10000 6400 .12   0      timeout 97    88    1400   3600 timeout 97   57   1000 2400 - -
seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c false(unreach-call) 1 wit inspect 130   110   1400 2300 .34   0      false(unreach-call) 14    7.4  240   510 true 14   7.3 130 390 - -
seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 150   130   1600 2200 .34   0      false(unreach-call) 14    7.5  250   510 true 13   7.0 150 390 - -
seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.BOUNDED-8.pals_true-termination.c false(unreach-call) 1 wit inspect 170   150   1900 2500 .18   0      false(unreach-call) 14    7.3  300   500 true 13   7.2 130 440 - -
seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 170   150   2200 2300 .18   0      false(unreach-call) 14    7.2  300   480 true 15   7.9 130 430 - -
seq-mthreaded/pals_floodmax.4_false-unreach-call.3.ufo.BOUNDED-8.pals_true-termination.c false(unreach-call) 1 wit inspect 180   160   2100 2300 .23   0      false(unreach-call) 15    7.9  260   510 true 13   7.0 130 430 - -
seq-mthreaded/pals_floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 170   160   2300 2600 .24   0      false(unreach-call) 14    7.6  300   490 true 13   7.0 130 440 - -
seq-mthreaded/pals_floodmax.4_false-unreach-call.4.ufo.BOUNDED-8.pals_true-termination.c false(unreach-call) 1 wit inspect 290   280   2500 2800 .23   0      false(unreach-call) 14    7.2  250   480 true 13   6.8 150 430 - -
seq-mthreaded/pals_floodmax.4_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 280   270   2700 2300 .24   0      false(unreach-call) 16    8.4  200   500 true 11   5.7 170 430 - -
seq-mthreaded/pals_floodmax.4_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c timeout 0 wit inspect 910   600   7900 2500 0      0      timeout 98    82    2500   2100 timeout 97   61   1500 3800 - -
seq-mthreaded/pals_floodmax.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c false(unreach-call) 1 wit inspect 350   320   3400 3200 .73   0      false(unreach-call) 23    12    410   800 true 14   7.7 290 490 - -
seq-mthreaded/pals_floodmax.5_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 380   350   4200 3200 .73   0      false(unreach-call) 22    12    400   780 true 15   8.3 160 500 - -
seq-mthreaded/pals_floodmax.5_false-unreach-call.2.ufo.BOUNDED-10.pals_true-termination.c false(unreach-call) 1 wit inspect 280   260   2600 2300 .43   0      false(unreach-call) 20    10    390   790 true 16   8.5 210 480 - -
seq-mthreaded/pals_floodmax.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 280   260   2600 2300 .43   0      false(unreach-call) 19    10    340   820 true 17   9.2 230 510 - -
seq-mthreaded/pals_floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals_true-termination.c false(unreach-call) 1 wit inspect 440   420   3900 3100 .51   0      false(unreach-call) 21    11    400   830 true 19   10   200 490 - -
seq-mthreaded/pals_floodmax.5_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 480   450   4600 2800 .52   .0041 false(unreach-call) 21    11    390   820 true 18   9.9 230 490 - -
seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.BOUNDED-10.pals_true-termination.c false(unreach-call) 1 wit inspect 700   490   5100 5000 .48   .0041 false(unreach-call) 26    14    460   1000 true 18   9.5 220 530 - -
seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 740   520   6600 3900 .48   0      false(unreach-call) 22    12    400   910 true 18   9.8 210 580 - -
seq-mthreaded/pals_floodmax.5_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c timeout 0 wit inspect 910   600   7200 3300 0      0      timeout 97    80    2100   1600 timeout 97   60   1300 3000 - -
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 20   11   190 530 .13   0      false(unreach-call) 12    6.2  130   340 false(unreach-call) 17   9.0 190 460 - -
seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 20   11   230 520 .13   0      false(unreach-call) 11    5.9  230   380 false(unreach-call) 85   62   1300 1000 - -
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 21   11   190 540 .12   0      false(unreach-call) 9.6  5.1  180   340 false(unreach-call) 17   8.6 170 440 - -
seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 230   200   3100 890 .11   0      false(unreach-call) 10    5.4  210   370 false(unreach-call) 33   19   400 710 - -
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 240   210   2400 1100 .18   0      false(unreach-call) 13    6.7  240   520 false(unreach-call) 48   30   640 910 - -
seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 240   210   3100 1200 .18   0      false(unreach-call) 12    6.3  220   500 false(unreach-call) 28   15   250 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 240   210   2700 1100 .17   0      false(unreach-call) 12    6.3  210   500 false(unreach-call) 26   14   410 770 - -
seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 240   210   2600 1200 .17   0      false(unreach-call) 12    6.2  250   480 false(unreach-call) 26   14   280 740 - -
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 260   220   3000 3700 .25   0      false(unreach-call) 14    7.1  240   530 timeout 97   73   1600 1200 - -
seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 260   220   3000 2700 .25   0      false(unreach-call) 14    7.3  240   540 timeout 97   73   1400 1500 - -
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 260   220   2800 2000 .24   0      false(unreach-call) 14    7.5  260   570 false(unreach-call) 24   13   260 600 - -
seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 260   220   3200 1900 .24   0      false(unreach-call) 15    7.7  260   550 false(unreach-call) 39   22   410 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 370   290   4700 4200 .34   0      false(unreach-call) 20    10    290   650 timeout 96   66   1400 1700 - -
seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 370   290   4200 4300 .34   0      false(unreach-call) 16    8.4  320   640 false(unreach-call) 36   20   480 950 - -
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 350   270   4000 4200 .33   0      false(unreach-call) 18    9.7  320   670 false(unreach-call) 64   39   800 2000 - -
seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 340   260   3800 4200 .33   0      false(unreach-call) 16    8.4  300   670 false(unreach-call) 42   24   550 1200 - -
seq-mthreaded/pals_lcr.3_false-unreach-call.1.ufo.BOUNDED-6.pals_true-termination.c false(unreach-call) 1 wit inspect 12   4.1 90 500 .10   0      false(unreach-call) 8.9  4.7  150   330 false(unreach-call) 17   8.7 160 440 - -
seq-mthreaded/pals_lcr.3_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 12   4.5 98 500 .10   0      false(unreach-call) 8.7  4.6  170   320 false(unreach-call) 35   19   320 680 - -
seq-mthreaded/pals_lcr.3_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c timeout 0 wit inspect 910   530   8200 3400 .049  0      timeout 93    79    1700   1300 timeout 97   58   1200 1500 - -
seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c false(unreach-call) 1 wit inspect 230   200   2400 980 .14   0      false(unreach-call) 12    6.6  240   480 false(unreach-call) 36   20   520 850 - -
seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 27   18   310 630 .15   0      false(unreach-call) 11    5.8  150   440 false(unreach-call) 30   16   280 870 - -
seq-mthreaded/pals_lcr.4_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c timeout 0 wit inspect 910   530   7600 4500 .057  0      timeout 94    79    2400   2400 timeout 97   57   1200 1900 - -
seq-mthreaded/pals_lcr.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c false(unreach-call) 1 wit inspect 240   210   2600 1200 .19   0      false(unreach-call) 13    7.0  260   530 false(unreach-call) 47   28   690 1300 - -
seq-mthreaded/pals_lcr.5_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 240   210   3300 1400 .19   0      false(unreach-call) 16    8.6  180   530 false(unreach-call) 35   19   570 1000 - -
seq-mthreaded/pals_lcr.5_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c timeout 0 wit inspect 910   540   8400 5100 .070  0      timeout 97    79    1800   2700 timeout 97   58   1200 3100 - -
seq-mthreaded/pals_lcr.6_false-unreach-call.1.ufo.BOUNDED-12.pals_true-termination.c false(unreach-call) 1 wit inspect 260   220   3400 1800 .25   0      false(unreach-call) 16    8.2  300   640 false(unreach-call) 53   30   640 1400 - -
seq-mthreaded/pals_lcr.6_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 260   220   3200 1700 .25   0      false(unreach-call) 16    8.5  270   620 false(unreach-call) 51   27   580 1400 - -
seq-mthreaded/pals_lcr.6_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c timeout 0 wit inspect 920   540   8200 2800 .082  0      timeout 98    85    2100   3400 timeout 97   57   970 1500 - -
seq-mthreaded/pals_lcr.7_false-unreach-call.1.ufo.BOUNDED-14.pals_true-termination.c false(unreach-call) 1 wit inspect 290   240   3300 2600 .32   0      false(unreach-call) 20    11    330   700 false(unreach-call) 54   30   590 1400 - -
seq-mthreaded/pals_lcr.7_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 290   230   3500 3200 .32   0      false(unreach-call) 19    9.7  310   790 timeout 97   58   1100 2500 - -
seq-mthreaded/pals_lcr.7_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c timeout 0 wit inspect 920   550   9200 3100 .094  0      timeout 96    83    2500   2500 timeout 97   58   1300 5000 - -
seq-mthreaded/pals_lcr.8_false-unreach-call.1.ufo.BOUNDED-16.pals_true-termination.c false(unreach-call) 1 wit inspect 370   270   3900 2500 .41   0      false(unreach-call) 30    16    340   960 timeout 97   62   1000 3000 - -
seq-mthreaded/pals_lcr.8_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 360   270   4500 2200 .41   0      false(unreach-call) 23    12    440   960 timeout 97   63   1300 2900 - -
seq-mthreaded/pals_lcr.8_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c timeout 0 wit inspect 910   540   10000 2800 .10   0      timeout 97    85    2100   2100 timeout 98   57   1200 3100 - -
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.1.ufo.BOUNDED-6.pals_true-termination.c false(unreach-call) 1 wit inspect 100   87   1400 2600 .16   0      false(unreach-call) 9.7  5.1  160   390 true 12   6.6 130 340 - -
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 100   87   1000 3700 .16   0      false(unreach-call) 10    5.3  190   420 true 11   6.0 110 320 - -
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.2.ufo.BOUNDED-6.pals_true-termination.c false(unreach-call) 1 wit inspect 39   23   340 3700 .15   0      false(unreach-call) 9.0  4.8  180   330 false(unreach-call) 71   50   900 890 - -
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 38   21   330 2500 .15   0      false(unreach-call) 8.7  4.6  160   330 false(unreach-call) 25   14   260 590 - -
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.3.ufo.BOUNDED-6.pals_true-termination.c false(unreach-call) 1 wit inspect 110   92   1200 3800 .16   0      false(unreach-call) 11    5.7  190   440 timeout 96   65   1100 1300 - -
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 110   92   1400 3800 .16   0      false(unreach-call) 10    5.4  210   460 timeout 97   67   1900 1200 - -
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.4.ufo.BOUNDED-6.pals_true-termination.c false(unreach-call) 1 wit inspect 110   92   1200 3700 .16   0      false(unreach-call) 11    5.5  180   400 false(unreach-call) 62   36   800 1100 - -
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 110   91   1200 3800 .16   0      false(unreach-call) 10    5.3  170   400 false(unreach-call) 61   36   860 1100 - -
seq-mthreaded/pals_opt-floodmax.3_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c timeout 0 wit inspect 910   570   8400 4600 .061  0      timeout 96    80    2100   2500 timeout 98   63   2100 5600 - -
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals_true-termination.c false(unreach-call) 1 wit inspect 140   120   1500 2300 .37   0      false(unreach-call) 17    9.2  230   510 true 14   7.5 120 400 - -
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 140   120   1500 2200 .38   0      false(unreach-call) 15    7.6  290   500 true 13   7.1 150 410 - -
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.2.ufo.BOUNDED-8.pals_true-termination.c false(unreach-call) 1 wit inspect 170   150   2400 2600 .20   0      false(unreach-call) 14    7.1  250   490 true 13   7.2 140 430 - -
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 170   150   2500 2600 .20   0      false(unreach-call) 14    7.1  280   480 true 14   7.6 120 430 - -
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.3.ufo.BOUNDED-8.pals_true-termination.c false(unreach-call) 1 wit inspect 190   170   2600 2700 .26   0      false(unreach-call) 15    8.0  300   670 true 14   7.6 140 450 - -
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 180   160   1900 2200 .27   0      false(unreach-call) 16    8.5  290   520 true 13   7.0 140 450 - -
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.4.ufo.BOUNDED-8.pals_true-termination.c false(unreach-call) 1 wit inspect 260   240   2700 2300 .26   0      false(unreach-call) 15    8.0  290   620 true 15   8.1 120 430 - -
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 200   190   2800 2700 .27   0      false(unreach-call) 15    7.9  290   480 true 12   6.3 170 440 - -
seq-mthreaded/pals_opt-floodmax.4_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c timeout 0 wit inspect 910   600   7100 3500 0      0      timeout 95    77    1200   1100 timeout 97   59   1200 3600 - -
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.1.ufo.BOUNDED-10.pals_true-termination.c false(unreach-call) 1 wit inspect 470   440   4200 3600 .80   0      false(unreach-call) 24    12    490   800 true 17   9.3 200 480 - -
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 500   470   3500 3200 .80   0      false(unreach-call) 26    14    440   790 true 17   9.5 190 480 - -
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.2.ufo.BOUNDED-10.pals_true-termination.c false(unreach-call) 1 wit inspect 380   360   3300 3200 .48   0      false(unreach-call) 22    12    420   690 true 19   10   190 500 - -
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 320   300   3400 2300 .48   0      false(unreach-call) 19    9.9  310   790 true 19   10   210 490 - -
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals_true-termination.c false(unreach-call) 1 wit inspect 470   450   3900 2600 .57   0      false(unreach-call) 23    12    440   770 true 16   8.8 230 510 - -
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 410   390   3800 2400 .58   0      false(unreach-call) 24    13    410   830 true 17   9.1 240 510 - -
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.4.ufo.BOUNDED-10.pals_true-termination.c false(unreach-call) 1 wit inspect 880   580   8700 5000 .53   0      false(unreach-call) 26    14    510   1100 true 19   10   210 530 - -
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(unreach-call) 1 wit inspect 800   540   6500 4800 .54   0      false(unreach-call) 27    14    520   1100 true 18   9.8 230 560 - -
seq-mthreaded/pals_opt-floodmax.5_overflow_false-unreach-call.ufo.UNBOUNDED.pals.c timeout 0 wit inspect 910   600   6900 3700 0      0      timeout 97    74    1200   1000 timeout 97   60   1700 3100 - -
seq-mthreaded/rekcba_aso_false-unreach-call.1.M1.c out of memory 0 wit inspect 580   380   4200 15000 .094  0      error (invalid witness file) .55 .35 14   42 error (invalid witness file) 6.1 3.3 110 300 - -
seq-mthreaded/rekcba_aso_false-unreach-call.1.M4.c out of memory 0 wit inspect 650   380   6100 15000 .45   0      error (invalid witness file) .50 .32 11   41 error (invalid witness file) 6.6 3.5 89 290 - -
seq-mthreaded/rekcba_aso_false-unreach-call.2.M1.c out of memory 0 wit inspect 600   380   4700 15000 .094  0      error (invalid witness file) .51 .32 12   39 error (invalid witness file) 6.3 3.3 130 300 - -
seq-mthreaded/rekcba_aso_false-unreach-call.2.M4.c out of memory 0 wit inspect 590   350   5500 15000 .45   0      error (invalid witness file) .53 .34 11   40 error (invalid witness file) 7.0 3.7 110 300 - -
seq-mthreaded/rekcba_aso_false-unreach-call.3.M1.c out of memory 0 wit inspect 420   310   3500 15000 .14   0      error (invalid witness file) .57 .36 10   41 error (invalid witness file) 8.0 4.2 68 290 - -
seq-mthreaded/rekcba_aso_false-unreach-call.3.M4.c out of memory 0 wit inspect 730   400   7900 15000 .64   0      error (invalid witness file) .53 .35 12   41 error (invalid witness file) 8.2 4.3 110 310 - -
seq-mthreaded/rekcba_aso_false-unreach-call.4.M1.c out of memory 0 wit inspect 430   310   3700 15000 .14   0      error (invalid witness file) .57 .37 9.2 43 error (invalid witness file) 6.6 3.5 81 290 - -
seq-mthreaded/rekcba_aso_false-unreach-call.4.M4.c out of memory 0 wit inspect 720   400   6500 15000 .64   0      error (invalid witness file) .51 .33 10   42 error (invalid witness file) 8.8 4.6 69 310 - -
seq-mthreaded/rekcba_ctm_false-unreach-call.2_true-termination.c out of memory 0 wit inspect 270   220   2800 15000 .33   0      error (invalid witness file) .50 .33 14   40 error (invalid witness file) 6.7 3.5 120 300 - -
seq-mthreaded/rekcba_ctm_false-unreach-call.3_true-termination.c out of memory 0 wit inspect 320   260   3400 15000 .52   0      error (invalid witness file) .53 .34 14   39 error (invalid witness file) 8.5 4.5 76 310 - -
seq-mthreaded/rekcba_nxt_false-unreach-call.1.M1.c timeout 0 wit inspect 910   490   8500 12000 .14   0      timeout 98    85    1500   6800 timeout 97   77   2600 1100 - -
seq-mthreaded/rekcba_nxt_false-unreach-call.1.M4.c out of memory 0 wit inspect 560   320   5200 15000 .36   0      error (invalid witness file) .49 .31 8.9 39 error (invalid witness file) 8.1 4.3 90 300 - -
seq-mthreaded/rekcba_nxt_false-unreach-call.2.M1.c timeout 0 wit inspect 910   470   8300 12000 .086  0      timeout 97    81    1700   6800 timeout 96   71   1500 1100 - -
seq-mthreaded/rekcba_nxt_false-unreach-call.2.M4.c out of memory 0 wit inspect 590   340   6200 15000 .41   0      error (invalid witness file) .51 .32 13   39 error (invalid witness file) 7.7 4.0 88 300 - -
seq-mthreaded/rekh_aso_false-unreach-call.1.M1.c timeout 0 wit inspect 910   420   6400 12000 .21   0      out of memory 73    57    1900   7000 timeout 97   80   2300 1100 - -
seq-mthreaded/rekh_aso_false-unreach-call.1.M4.c out of memory 0 wit inspect 280   130   2400 15000 .21   0      error (invalid witness file) .48 .33 3.9 40 error (invalid witness file) 8.1 4.2 83 300 - -
seq-mthreaded/rekh_aso_false-unreach-call.2.M1.c timeout 0 wit inspect 910   410   6500 12000 .21   0      out of memory 77    62    1400   7000 timeout 97   77   1200 1200 - -
seq-mthreaded/rekh_aso_false-unreach-call.2.M4.c out of memory 0 wit inspect 290   130   2600 15000 .21   0      error (invalid witness file) .54 .34 8.2 44 error (invalid witness file) 6.8 3.6 110 310 - -
seq-mthreaded/rekh_aso_false-unreach-call.4.M1.c out of memory 0 wit inspect 570   310   4300 15000 .30   0      error (invalid witness file) .50 .33 5.9 42 error (invalid witness file) 8.5 4.5 74 300 - -
seq-mthreaded/rekh_aso_false-unreach-call.4.M4.c out of memory 0 wit inspect 400   230   4100 15000 .30   0      error (invalid witness file) .54 .34 9.7 40 error (invalid witness file) 7.0 3.7 96 300 - -
seq-mthreaded/rekh_ctm_false-unreach-call.2_true-termination.c timeout 0 wit inspect 920   500   6600 12000 .31   0      timeout 97    81    2000   6700 timeout 96   54   880 1200 - -
seq-mthreaded/rekh_ctm_false-unreach-call.3_true-termination.c timeout 0 wit inspect 920   490   7000 14000 .23   0      out of memory 67    51    1500   7000 timeout 97   70   1500 2000 - -
seq-mthreaded/rekh_nxt_false-unreach-call.1.M1.c timeout 0 wit inspect 910   490   9200 13000 .27   0      timeout 96    83    1100   6900 timeout 97   76   1700 2000 - -
seq-mthreaded/rekh_nxt_false-unreach-call.1.M4.c out of memory 0 wit inspect 490   300   4600 15000 1.0    0      error (invalid witness file) .50 .33 9.1 41 error (invalid witness file) 6.2 3.3 120 300 - -
seq-mthreaded/rekh_nxt_false-unreach-call.2.M1.c timeout 0 wit inspect 920   440   6900 12000 .19   0      out of memory 78    60    1400   7000 timeout 98   75   1400 1100 - -
seq-mthreaded/rekh_nxt_false-unreach-call.2.M4.c out of memory 0 wit inspect 290   150   2900 15000 .19   0      error (invalid witness file) .49 .32 8.3 40 error (invalid witness file) 7.4 3.9 76 290 - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_true-unreach-call.ufo.BOUNDED-10.pals.c true 2 wit inspect 140   130   1900 820 .074  0      - - true 300    290    6200   960 out of memory 350   260   3400 7000
seq-mthreaded/pals_STARTPALS_ActiveStandby_true-unreach-call.ufo.UNBOUNDED.pals.c true 1 wit inspect 180   170   2100 970 .074  0      - - timeout 900    890    17000   1200 out of memory 350   250   7000 7000
seq-mthreaded/pals_STARTPALS_Triplicated_true-unreach-call.ufo.BOUNDED-10.pals_true-termination.c true 2 wit inspect 35   17   320 1100 .11   0      - - true 170    150    4100   2600 true 260   190   3400 4100
seq-mthreaded/pals_STARTPALS_Triplicated_true-unreach-call.ufo.UNBOUNDED.pals.c true 2 wit inspect 33   17   340 1100 .11   0      - - timeout 900    890    18000   3500 true 250   180   3800 4100
seq-mthreaded/pals_floodmax.3_true-unreach-call.ufo.BOUNDED-6.pals_true-termination.c true 2 wit inspect 290   250   3100 4100 .18   0      - - true 30    21    310   580 out of memory 180   110   1400 7000
seq-mthreaded/pals_floodmax.3_true-unreach-call.ufo.UNBOUNDED.pals.c true 2 wit inspect 280   240   3500 3900 .23   0      - - true 27    18    710   550 out of memory 130   87   1600 7000
seq-mthreaded/pals_floodmax.4_true-unreach-call.ufo.BOUNDED-8.pals_true-termination.c true 2 wit inspect 890   590   7000 2300 .14   0      - - true 820    810    16000   840 out of memory 160   100   2300 7000
seq-mthreaded/pals_floodmax.4_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 0 wit inspect 910   600   8400 3100 0      0      - - timeout 910    880    19000   4300 out of memory 170   110   2400 7000
seq-mthreaded/pals_floodmax.5_true-unreach-call.ufo.BOUNDED-10.pals_true-termination.c timeout 0 wit inspect 900   600   8000 3600 0      0      - - timeout 910    890    14000   1200 out of memory 210   140   2900 7000
seq-mthreaded/pals_floodmax.5_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 0 wit inspect 910   600   7900 4400 0      0      - - timeout 910    880    15000   3900 out of memory 130   79   1100 7000
seq-mthreaded/pals_lcr-var-start-time.3_true-unreach-call.ufo.BOUNDED-6.pals_true-termination.c true 2 wit inspect 220   200   2300 820 .090  0      - - true 16    9.5  220   460 out of memory 200   130   2900 7000
seq-mthreaded/pals_lcr-var-start-time.3_true-unreach-call.ufo.UNBOUNDED.pals.c true 2 wit inspect 230   210   2400 1000 .11   0      - - true 21    13    330   520 timeout 960   830   11000 6700
seq-mthreaded/pals_lcr-var-start-time.4_true-unreach-call.ufo.BOUNDED-8.pals_true-termination.c true 2 wit inspect 250   220   2600 1400 .11   0      - - true 32    25    640   560 out of memory 120   76   1500 7000
seq-mthreaded/pals_lcr-var-start-time.4_true-unreach-call.ufo.UNBOUNDED.pals.c true 2 wit inspect 270   220   2500 1500 .15   0      - - true 63    50    780   610 out of memory 130   81   1200 7000
seq-mthreaded/pals_lcr-var-start-time.5_true-unreach-call.ufo.BOUNDED-10.pals_true-termination.c true 2 wit inspect 370   270   3600 3900 .14   0      - - true 120    110    2700   710 out of memory 190   110   1500 7000
seq-mthreaded/pals_lcr-var-start-time.5_true-unreach-call.ufo.UNBOUNDED.pals.c true 2 wit inspect 410   290   4800 4000 .27   0      - - true 180    160    3800   1900 out of memory 110   66   820 7000
seq-mthreaded/pals_lcr-var-start-time.6_true-unreach-call.ufo.BOUNDED-12.pals_true-termination.c timeout 0 wit inspect 900   550   10000 4500 .082  0      - - true 700    690    11000   1000 out of memory 180   120   2500 7000
seq-mthreaded/pals_lcr-var-start-time.6_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 0 wit inspect 910   550   7700 4400 .082  0      - - true 660    640    12000   2200 out of memory 140   87   3300 7000
seq-mthreaded/pals_lcr.3_true-unreach-call.ufo.BOUNDED-6.pals_true-termination.c true 2 wit inspect 220   200   2400 890 .086  0      - - true 13    7.7  200   420 timeout 960   870   18000 5600
seq-mthreaded/pals_lcr.3_true-unreach-call.ufo.UNBOUNDED.pals.c true 2 wit inspect 170   170   2100 910 .049  0      - - true 13    8.6  250   390 timeout 960   890   13000 2200
seq-mthreaded/pals_lcr.4_true-unreach-call.ufo.BOUNDED-8.pals_true-termination.c true 2 wit inspect 230   200   3200 910 .10   0      - - true 21    15    460   500 out of memory 200   130   1700 7000
seq-mthreaded/pals_lcr.4_true-unreach-call.ufo.UNBOUNDED.pals.c true 2 wit inspect 240   210   3200 1000 .26   0      - - true 64    51    1400   1700 out of memory 190   120   1700 7000
seq-mthreaded/pals_lcr.5_true-unreach-call.ufo.BOUNDED-10.pals_true-termination.c true 2 wit inspect 270   220   3100 1800 .12   0      - - true 47    39    1000   610 out of memory 170   110   2800 7000
seq-mthreaded/pals_lcr.5_true-unreach-call.ufo.UNBOUNDED.pals.c true 2 wit inspect 290   230   3400 2200 .38   0      - - true 200    180    3800   3900 out of memory 170   110   1500 7000
seq-mthreaded/pals_lcr.6_true-unreach-call.ufo.BOUNDED-12.pals_true-termination.c true 2 wit inspect 350   260   4500 1800 .14   0      - - true 170    160    4000   750 out of memory 190   130   1700 7000
seq-mthreaded/pals_lcr.6_true-unreach-call.ufo.UNBOUNDED.pals.c true 2 wit inspect 410   290   4200 2500 .42   0      - - true 760    720    20000   4600 out of memory 180   120   1800 7000
seq-mthreaded/pals_lcr.7_true-unreach-call.ufo.BOUNDED-14.pals_true-termination.c true 2 wit inspect 680   420   7500 3500 .16   0      - - true 600    590    12000   890 out of memory 260   180   3800 7000
seq-mthreaded/pals_lcr.7_true-unreach-call.ufo.UNBOUNDED.pals.c true 1 wit inspect 720   450   6900 3000 1.1    0      - - timeout 910    840    20000   5300 out of memory 250   160   3500 7000
seq-mthreaded/pals_lcr.8_true-unreach-call.ufo.BOUNDED-16.pals_true-termination.c timeout 0 wit inspect 900   530   8800 3500 .11   0      - - timeout 900    890    14000   1100 out of memory 180   120   2300 7000
seq-mthreaded/pals_lcr.8_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 0 wit inspect 910   540   9200 3200 .10   0      - - timeout 910    860    24000   4800 out of memory 190   120   2900 7000
seq-mthreaded/pals_opt-floodmax.3_true-unreach-call.ufo.BOUNDED-6.pals_true-termination.c true 2 wit inspect 330   290   3400 3800 .14   0      - - true 31    22    420   570 out of memory 180   110   3200 7000
seq-mthreaded/pals_opt-floodmax.3_true-unreach-call.ufo.UNBOUNDED.pals.c true 2 wit inspect 330   290   2900 4000 .18   0      - - true 37    24    450   560 out of memory 160   98   2100 7000
seq-mthreaded/pals_opt-floodmax.4_true-unreach-call.ufo.BOUNDED-8.pals_true-termination.c timeout 0 wit inspect 900   600   8100 2500 0      0      - - true 690    680    14000   850 out of memory 160   110   1800 7000
seq-mthreaded/pals_opt-floodmax.4_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 0 wit inspect 910   600   8600 2300 0      0      - - timeout 910    890    16000   1100 out of memory 140   91   1900 7000
seq-mthreaded/pals_opt-floodmax.5_true-unreach-call.ufo.BOUNDED-10.pals_true-termination.c timeout 0 wit inspect 900   590   7400 4800 0      0      - - timeout 910    890    16000   1200 out of memory 200   140   2100 7000
seq-mthreaded/pals_opt-floodmax.5_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 0 wit inspect 910   590   7200 4100 0      0      - - timeout 910    880    17000   3600 out of memory 150   94   1800 7000
seq-mthreaded/rekcba_aso_true-unreach-call.1.M1.c out of memory 0 wit inspect 580   370   4400 15000 .094  0      - - error (invalid witness file) .66 .42 8.6 41 error (invalid witness file) 6.2 3.3 110 310
seq-mthreaded/rekcba_aso_true-unreach-call.1.M4.c out of memory 0 wit inspect 620   370   5500 15000 .45   0      - - error (invalid witness file) .55 .36 14   41 error (invalid witness file) 7.2 3.8 110 300
seq-mthreaded/rekcba_aso_true-unreach-call.2.M1.c out of memory 0 wit inspect 420   310   4000 15000 .14   0      - - error (invalid witness file) .64 .42 8.0 40 error (invalid witness file) 6.6 3.4 110 300
seq-mthreaded/rekcba_aso_true-unreach-call.2.M4.c out of memory 0 wit inspect 740   410   6800 15000 .64   0      - - error (invalid witness file) .52 .33 10   40 error (invalid witness file) 6.4 3.4 130 300
seq-mthreaded/rekcba_ctm_true-unreach-call.1_true-termination.c out of memory 0 wit inspect 270   230   2600 15000 .33   0      - - error (invalid witness file) .65 .42 8.1 40 error (invalid witness file) 6.5 3.5 110 300
seq-mthreaded/rekcba_ctm_true-unreach-call.2_true-termination.c out of memory 0 wit inspect 270   230   3200 15000 .33   0      - - error (invalid witness file) .59 .38 9.5 39 error (invalid witness file) 7.0 3.7 150 310
seq-mthreaded/rekcba_ctm_true-unreach-call.3_true-termination.c out of memory 0 wit inspect 320   260   3600 15000 .52   0      - - error (invalid witness file) .55 .35 9.1 40 error (invalid witness file) 6.7 3.6 110 310
seq-mthreaded/rekcba_ctm_true-unreach-call.4_true-termination.c out of memory 0 wit inspect 740   400   6100 15000 .72   0      - - error (invalid witness file) .52 .33 11   39 error (invalid witness file) 7.6 3.9 130 310
seq-mthreaded/rekcba_nxt_true-unreach-call.1.M1.c timeout 0 wit inspect 910   480   7500 12000 .14   0      - - out of memory 120    110    3600   7000 timeout 960   940   16000 1100
seq-mthreaded/rekcba_nxt_true-unreach-call.1.M4.c out of memory 0 wit inspect 570   330   5700 15000 .36   0      - - error (invalid witness file) .63 .41 8.3 40 error (invalid witness file) 7.1 3.7 110 310
seq-mthreaded/rekcba_nxt_true-unreach-call.2.M1.c timeout 0 wit inspect 910   480   8200 12000 .074  0      - - out of memory 220    210    5200   7000 timeout 960   930   19000 1500
seq-mthreaded/rekcba_nxt_true-unreach-call.2.M4.c out of memory 0 wit inspect 570   330   5500 15000 .36   0      - - error (invalid witness file) .46 .29 8.6 39 error (invalid witness file) 6.5 3.4 140 290
seq-mthreaded/rekcba_nxt_true-unreach-call.3.M1.c timeout 0 wit inspect 910   470   8400 12000 .086  0      - - out of memory 160    150    3000   7000 error 210   180   2500 1700
seq-mthreaded/rekcba_nxt_true-unreach-call.3.M4.c out of memory 0 wit inspect 550   320   5000 15000 .41   0      - - error (invalid witness file) .65 .41 8.5 39 error (invalid witness file) 7.0 3.7 110 310
seq-mthreaded/rekh_aso_true-unreach-call.1.M1.c timeout 0 wit inspect 910   410   7900 12000 .21   0      - - out of memory 76    58    2200   7000 error 240   200   2700 1600
seq-mthreaded/rekh_aso_true-unreach-call.1.M4.c out of memory 0 wit inspect 290   130   2900 15000 .21   0      - - error (invalid witness file) .60 .38 9.0 40 error (invalid witness file) 6.2 3.3 99 300
seq-mthreaded/rekh_aso_true-unreach-call.2.M1.c out of memory 0 wit inspect 580   320   4500 15000 .30   0      - - error (invalid witness file) .61 .40 9.7 42 error (invalid witness file) 6.2 3.2 77 290
seq-mthreaded/rekh_aso_true-unreach-call.2.M4.c out of memory 0 wit inspect 400   230   3500 15000 .30   0      - - error (invalid witness file) .59 .38 9.1 40 error (invalid witness file) 6.1 3.2 78 300
seq-mthreaded/rekh_aso_true-unreach-call.3.M1.c out of memory 0 wit inspect 440   260   3600 15000 .30   0      - - error (invalid witness file) .66 .43 8.5 41 error (invalid witness file) 7.8 4.1 110 320
seq-mthreaded/rekh_aso_true-unreach-call.3.M4.c out of memory 0 wit inspect 410   240   4400 15000 .30   0      - - error (invalid witness file) .63 .39 8.9 40 error (invalid witness file) 8.0 4.2 100 300
seq-mthreaded/rekh_ctm_true-unreach-call.1_true-termination.c timeout 0 wit inspect 920   480   7700 13000 .32   0      - - out of memory 340    330    6700   7000 timeout 960   890   18000 5900
seq-mthreaded/rekh_ctm_true-unreach-call.2_true-termination.c timeout 0 wit inspect 910   490   8300 12000 .32   0      - - timeout 930    910    18000   7000 timeout 960   850   14000 6600
seq-mthreaded/rekh_ctm_true-unreach-call.3_true-termination.c timeout 0 wit inspect 920   500   6800 15000 .23   0      - - out of memory 67    51    1800   7000 timeout 960   890   17000 4600
seq-mthreaded/rekh_ctm_true-unreach-call.4_true-termination.c out of memory 0 wit inspect 440   290   3400 15000 .41   0      - - error (invalid witness file) .59 .37 10   42 error (invalid witness file) 5.8 3.1 99 300
seq-mthreaded/rekh_nxt_true-unreach-call.1.M1.c timeout 0 wit inspect 910   500   7500 14000 .27   0      - - out of memory 100    90    2600   7000 out of memory 720   680   9200 7000
seq-mthreaded/rekh_nxt_true-unreach-call.1.M4.c out of memory 0 wit inspect 500   300   4900 15000 1.0    0      - - error (invalid witness file) .67 .43 9.3 44 error (invalid witness file) 5.9 3.2 80 290
seq-mthreaded/rekh_nxt_true-unreach-call.2.M1.c timeout 0 wit inspect 920   450   5900 12000 .15   0      - - out of memory 90    70    1500   7000 timeout 960   930   16000 1200
seq-mthreaded/rekh_nxt_true-unreach-call.2.M4.c out of memory 0 wit inspect 280   140   2400 15000 .15   0      - - error (invalid witness file) .50 .32 12   40 error (invalid witness file) 6.0 3.2 90 300
seq-mthreaded/rekh_nxt_true-unreach-call.3.M1.c timeout 0 wit inspect 920   440   7300 11000 .19   0      - - out of memory 88    67    1600   7000 timeout 960   930   17000 1300
seq-mthreaded/rekh_nxt_true-unreach-call.3.M4.c out of memory 0 wit inspect 290   150   2600 15000 .19   0      - - error (invalid witness file) .51 .32 7.7 39 error (invalid witness file) 6.2 3.3 120 300
seq-pthread/cs_fib_false-unreach-call.i timeout 0 wit inspect 910   810   7400 4600 .22   0      timeout 93    79    2200   1200 error 14   7.7 150 300 - -
seq-pthread/cs_fib_longer_false-unreach-call.i timeout 0 wit inspect 900   790   6300 4300 .23   0      timeout 93    80    1200   1200 error 16   8.2 150 310 - -
seq-pthread/cs_lazy_false-unreach-call.i false(unreach-call) 1 wit inspect 430   300   2900 4800 .30   0      false(unreach-call) 18    12    430   510 false(unreach-call) 41   21   370 770 - -
seq-pthread/cs_queue_false-unreach-call.i timeout 0 wit inspect 900   580   8300 6900 .30   0      timeout 97    82    1800   2500 out of memory 46   36   630 7000 - -
seq-pthread/cs_read_write_lock_false-unreach-call.i timeout 0 wit inspect 900   530   6200 5400 .14   0      timeout 94    87    1400   1000 error 12   6.4 160 290 - -
seq-pthread/cs_stack_false-unreach-call.i timeout 0 wit inspect 900   520   7600 5000 .24   0      timeout 94    86    1900   780 unknown 17   9.0 150 300 - -
seq-pthread/cs_stateful_false-unreach-call.i false(unreach-call) 0 wit inspect 440   300   3000 3600 .30   0      true 9.2  4.8  150   300 timeout 96   77   2200 1100 - -
seq-pthread/cs_dekker_true-unreach-call.i true 2 wit inspect 480   380   4100 4700 .27   0      - - true 610    590    10000   1700 timeout 960   920   18000 2400
seq-pthread/cs_fib_longer_true-unreach-call.i timeout 0 wit inspect 940   820   11000 4400 .27   0      - - timeout 910    870    22000   6400 error 14   7.3 160 300
seq-pthread/cs_fib_true-unreach-call.i timeout 0 wit inspect 960   830   11000 4500 .25   0      - - timeout 900    870    18000   6200 error 12   6.4 180 320
seq-pthread/cs_lamport_true-unreach-call.i true 2 wit inspect 450   370   3600 3500 .29   0      - - true 540    520    10000   1700 timeout 960   930   17000 2100
seq-pthread/cs_peterson_true-unreach-call.i true 2 wit inspect 410   360   3900 3000 .24   0      - - true 490    470    5500   1600 timeout 960   930   13000 1600
seq-pthread/cs_queue_true-unreach-call.i timeout 0 wit inspect 930   590   8900 6500 .37   0      - - timeout 910    870    15000   5200 out of memory 34   27   750 7000
seq-pthread/cs_read_write_lock_true-unreach-call.i timeout 0 wit inspect 900   530   8900 5600 .17   0      - - timeout 900    890    20000   2900 error 12   6.4 120 300
seq-pthread/cs_stack_true-unreach-call.i timeout 0 wit inspect 960   580   9800 5000 .26   0      - - timeout 910    880    15000   4600 unknown 13   6.9 150 320
seq-pthread/cs_stateful_true-unreach-call.i true 2 wit inspect 690   440   5000 4800 .26   0      - - true 670    650    13000   1600 timeout 960   920   15000 2300
seq-pthread/cs_sync_true-unreach-call.i timeout 0 wit inspect 960   790   10000 4600 .23   0      - - timeout 900    870    21000   6600 timeout 960   920   15000 3000
seq-pthread/cs_szymanski_true-unreach-call.i true 2 wit inspect 400   350   2700 3400 .26   0      - - true 370    350    8700   1600 timeout 960   930   20000 2700
seq-pthread/cs_time_var_mutex_true-unreach-call.i timeout 0 wit inspect 900   670   7400 5600 .24   0      - - timeout 900    890    28000   1900 timeout 960   930   13000 2800
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
total 273 206 110000 76000 1000000 1400000 67   .037 273 4600 3300 87000 180000   273 8100 4900 110000 210000   273 46000 44000 920000 300000   273 27000 23000 410000 400000  
    correct results 159 200 32000 26000 320000 340000 36   .016 118 1700 880 30000 63000   92 5300 3100 70000 140000   27 18000 17000 360000 110000   15 13000 11000 190000 200000  
        correct true 41 82 9800 7700 98000 82000 5.7 0     0 0 0 0 0   36 0 0 0 0   27 18000 17000 360000 110000   15 13000 11000 190000 200000  
        correct false 118 118 22000 18000 220000 260000 30   .016 118 1700 880 30000 63000   56 5300 3100 70000 140000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 13 6 4000 3100 40000 36000 8.9 .020 1 590 460 13000 27000   3 620 370 9600 11000   0 5500 5200 110000 25000   0 1300 840 20000 42000  
        correct-unconfirmed true 6 6 1100 740 11000 8700 1.4 0     1 0 0 0 0   3 0 0 0 0   0 5500 5200 110000 25000   0 1300 840 20000 42000  
        correct-unconfirmed false 7 0 3000 2300 29000 27000 7.5 .020 0 590 460 13000 27000   0 620 370 9600 11000   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) 206
Run set sv-comp17.ReachSafety-Sequentialized