Tool SeaHorn-F16 0.1.0
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host [zeus01; zeus02; zeus03; zeus04; zeus05; zeus06; zeus07; zeus08; zeus09; zeus10; zeus11; zeus12; zeus13; zeus14; zeus15; zeus16; zeus17; zeus18; zeus19; zeus20; zeus21; zeus22; zeus23; zeus24]
OS Linux 4.2.0-23-generic
System CPU: Intel Xeon E5-2650 v2 @ 2.60 GHz, cores: 32, frequency: 3.4 GHz; RAM: 135149 MB
Date of execution 2016-01-11 21:35:00 [[ 2016-01-15 18:20:27 CET ]] [[ 2016-01-15 22:30:28 CET ]]
Run set sv-comp16.Sequentialized
Options --cex=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/seahorn.2016-01-11_2135.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/seahorn.2016-01-11_2135.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]
../../sv-benchmarks/c/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime (s) wit1_walltime (s) wit1_memUsage (MB) wit2_status wit2_cputime (s) wit2_walltime (s) wit2_memUsage (MB)
systemc/kundu1_false-unreach-call_false-termination.cil.c false(reach) 11    5.6  180 wit false(reach) 33   18   810 true 14   9.1 340
systemc/kundu2_false-unreach-call_false-termination.cil.c false(reach) 14    7.1  300 wit false(reach) 24   13   720 true 13   8.7 320
systemc/pc_sfifo_1_false-unreach-call_false-termination.cil.c false(reach) .77 .41 56 wit false(reach) 7.9 4.3 360 true 13   7.3 340
systemc/pc_sfifo_2_false-unreach-call_false-termination.cil.c false(reach) .68 .36 49 wit false(reach) 8.4 4.7 360 true 11   6.4 330
systemc/pipeline_false-unreach-call_false-termination.cil.c false(reach) 510    260    1600 wit false(reach) 62   38   2600 true 15   8.8 340
systemc/token_ring.01_false-unreach-call_false-termination.cil.c false(reach) 1.7  .85 110 wit false(reach) 13   7.3 490 true 13   9.2 330
systemc/token_ring.02_false-unreach-call_false-termination.cil.c false(reach) 2.6  1.3  140 wit false(reach) 14   7.8 490 true 12   6.7 340
systemc/token_ring.03_false-unreach-call_false-termination.cil.c false(reach) 6.5  3.3  230 wit false(reach) 13   7.0 510 true 13   9.4 340
systemc/token_ring.04_false-unreach-call_false-termination.cil.c false(reach) 8.4  4.2  220 wit false(reach) 20   11   580 true 14   9.7 330
systemc/token_ring.05_false-unreach-call_false-termination.cil.c false(reach) 21    11    320 wit false(reach) 19   10   600 true 14   8.4 320
systemc/token_ring.06_false-unreach-call_false-termination.cil.c false(reach) 38    19    470 wit false(reach) 20   10   620 true 15   10   330
systemc/token_ring.07_false-unreach-call_false-termination.cil.c false(reach) 98    49    910 wit false(reach) 25   14   740 true 13   8.8 330
systemc/token_ring.08_false-unreach-call_false-termination.cil.c false(reach) 180    89    1200 wit false(reach) 24   13   750 true 15   9.2 330
systemc/token_ring.09_false-unreach-call_false-termination.cil.c witness timeout 320    160    1700 wit timeout 91   78   740 true 17   9.4 360
systemc/token_ring.10_false-unreach-call_false-termination.cil.c false(reach) 560    280    2400 wit false(reach) 43   27   930 true 15   8.3 350
systemc/token_ring.11_false-unreach-call_false-termination.cil.c false(reach) 760    380    3100 wit false(reach) 31   17   890 true 18   12   360
systemc/token_ring.12_false-unreach-call_false-termination.cil.c witness timeout 720    360    3800 wit timeout 90   75   910 true 15   8.9 330
systemc/token_ring.13_false-unreach-call_false-termination.cil.c timeout 900    450    5000 wit - -
systemc/token_ring.14_false-unreach-call_false-termination.cil.c witness timeout 730    360    3800 wit timeout 90   75   900 true 15   7.9 330
systemc/token_ring.15_false-unreach-call_false-termination.cil.c timeout 900    450    5200 wit - -
systemc/toy1_false-unreach-call_false-termination.cil.c false(reach) 59    30    720 wit false(reach) 43   26   1200 true 14   9.7 330
systemc/toy2_false-unreach-call_false-termination.cil.c false(reach) 30    15    150 wit false(reach) 32   17   820 true 14   7.8 340
systemc/transmitter.01_false-unreach-call_false-termination.cil.c false(reach) .60 .32 53 wit false(reach) 12   6.8 410 true 12   6.6 350
systemc/transmitter.02_false-unreach-call_false-termination.cil.c false(reach) 2.1  1.1  110 wit false(reach) 12   6.5 440 true 12   7.4 330
systemc/transmitter.03_false-unreach-call_false-termination.cil.c false(reach) 4.3  2.2  190 wit false(reach) 12   6.7 470 true 13   7.5 330
systemc/transmitter.04_false-unreach-call_false-termination.cil.c false(reach) 7.7  3.9  280 wit false(reach) 14   7.8 490 true 12   6.4 350
systemc/transmitter.05_false-unreach-call_false-termination.cil.c false(reach) 7.9  4.0  260 wit false(reach) 16   8.5 550 true 13   7.3 340
systemc/transmitter.06_false-unreach-call_false-termination.cil.c false(reach) 12    6.1  380 wit false(reach) 18   9.7 600 true 15   8.4 360
systemc/transmitter.07_false-unreach-call_false-termination.cil.c false(reach) 51    25    750 wit false(reach) 24   14   700 true 13   8.9 340
systemc/transmitter.08_false-unreach-call_false-termination.cil.c false(reach) 67    33    1000 wit false(reach) 21   11   670 true 16   8.7 330
systemc/transmitter.09_false-unreach-call_false-termination.cil.c false(reach) 110    54    1400 wit false(reach) 20   11   670 true 16   9.1 340
systemc/transmitter.10_false-unreach-call_false-termination.cil.c false(reach) 140    69    1800 wit false(reach) 32   18   860 true 15   9.0 320
systemc/transmitter.11_false-unreach-call_false-termination.cil.c false(reach) 190    95    2500 wit false(reach) 26   14   850 true 16   10   360
systemc/transmitter.12_false-unreach-call_false-termination.cil.c witness timeout 250    130    3300 wit timeout 90   76   950 true 17   9.6 350
systemc/transmitter.13_false-unreach-call_false-termination.cil.c false(reach) 370    190    4200 wit false(reach) 42   26   1100 true 16   9.6 340
systemc/transmitter.15_false-unreach-call_false-termination.cil.c false(reach) 49    24    1500 wit false(reach) 16   8.5 610 true 16   9.0 330
systemc/transmitter.16_false-unreach-call_false-termination.cil.c false(reach) 21    10    1600 wit false(reach) 19   10   630 true 14   8.3 340
systemc/bist_cell_true-unreach-call_false-termination.cil.c true .34 .19 39 wit - -
systemc/kundu_true-unreach-call_false-termination.cil.c true 210    100    490 wit - -
systemc/mem_slave_tlm.1_true-unreach-call_false-termination.cil.c true 770    380    1900 wit - -
systemc/mem_slave_tlm.2_true-unreach-call_false-termination.cil.c true 610    310    1900 wit - -
systemc/mem_slave_tlm.3_true-unreach-call_false-termination.cil.c timeout 900    450    2000 wit - -
systemc/mem_slave_tlm.4_true-unreach-call_false-termination.cil.c timeout 900    450    1500 wit - -
systemc/mem_slave_tlm.5_true-unreach-call_false-termination.cil.c timeout 900    450    1800 wit - -
systemc/pc_sfifo_1_true-unreach-call_false-termination.cil.c true 4.1  2.1  77 wit - -
systemc/pc_sfifo_2_true-unreach-call_false-termination.cil.c true 25    13    310 wit - -
systemc/pc_sfifo_3_true-unreach-call_false-termination.cil.c true .63 .33 45 wit - -
systemc/pipeline_true-unreach-call_false-termination.cil.c true 540    270    1600 wit - -
systemc/token_ring.01_true-unreach-call_false-termination.cil.c true 3.2  1.6  100 wit - -
systemc/token_ring.02_true-unreach-call_false-termination.cil.c true 6.7  3.4  130 wit - -
systemc/token_ring.03_true-unreach-call_false-termination.cil.c true 18    9.2  220 wit - -
systemc/token_ring.04_true-unreach-call_false-termination.cil.c true 61    31    330 wit - -
systemc/token_ring.05_true-unreach-call_false-termination.cil.c true 83    41    310 wit - -
systemc/token_ring.06_true-unreach-call_false-termination.cil.c true 160    79    470 wit - -
systemc/token_ring.07_true-unreach-call_false-termination.cil.c timeout 900    450    1000 wit - -
systemc/token_ring.08_true-unreach-call_false-termination.cil.c timeout 900    450    1300 wit - -
systemc/token_ring.09_true-unreach-call_false-termination.cil.c timeout 900    450    1700 wit - -
systemc/token_ring.10_true-unreach-call_false-termination.cil.c timeout 900    450    2200 wit - -
systemc/token_ring.11_true-unreach-call_false-termination.cil.c timeout 900    450    2900 wit - -
systemc/token_ring.12_true-unreach-call_false-termination.cil.c timeout 900    450    3700 wit - -
systemc/token_ring.13_true-unreach-call_false-termination.cil.c timeout 900    450    4800 wit - -
systemc/toy_true-unreach-call_false-termination.cil.c true 230    110    840 wit - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c false(reach) .72 .39 69 wit false(reach) 15   8.3 530 true 14   9.3 330
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) .58 .31 67 wit false(reach) 15   8.2 520 true 13   8.4 350
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.BOUNDED-10.pals.c false(reach) 1.3  .67 71 wit false(reach) 24   13   600 true 14   9.0 330
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.UNBOUNDED.pals.c false(reach) 1.4  .72 69 wit false(reach) 25   14   610 true 15   11   340
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_2.ufo.BOUNDED-10.pals.c false(reach) 1.0  .55 72 wit false(reach) 23   12   660 true 14   7.8 340
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_2.ufo.UNBOUNDED.pals.c false(reach) 1.1  .59 71 wit false(reach) 23   12   650 true 12   6.6 330
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.5.ufo.BOUNDED-10.pals.c witness timeout 2.8  1.4  75 wit timeout 90   71   2100 true 15   11   330
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.5.ufo.UNBOUNDED.pals.c witness timeout 3.1  1.6  74 wit timeout 90   73   2000 true 16   12   340
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.1.ufo.BOUNDED-10.pals.c false(reach) .95 .49 81 wit false(reach) 20   11   580 true 14   8.4 350
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) .88 .48 77 wit false(reach) 21   11   600 true 14   7.8 330
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.BOUNDED-10.pals.c false(reach) .83 .43 78 wit false(reach) 20   11   550 true 13   7.6 330
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) .78 .41 72 wit false(reach) 21   11   560 true 14   9.6 330
seq-mthreaded/pals_floodmax.3_false-unreach-call.1.ufo.BOUNDED-6.pals.c witness timeout 6.0  3.0  77 wit timeout 90   67   4000 true 13   7.4 340
seq-mthreaded/pals_floodmax.3_false-unreach-call.1.ufo.UNBOUNDED.pals.c witness timeout 21    11    81 wit timeout 91   68   4000 true 12   7.4 330
seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.BOUNDED-6.pals.c witness timeout 2.5  1.2  76 wit timeout 91   71   4000 true 16   9.0 350
seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c witness timeout 3.4  1.7  77 wit timeout 91   72   4000 true 13   8.0 350
seq-mthreaded/pals_floodmax.3_false-unreach-call.3.ufo.BOUNDED-6.pals.c witness timeout 8.6  4.3  81 wit timeout 90   71   4000 true 14   8.4 330
seq-mthreaded/pals_floodmax.3_false-unreach-call.3.ufo.UNBOUNDED.pals.c witness timeout 14    6.9  83 wit timeout 91   71   4000 true 13   9.2 330
seq-mthreaded/pals_floodmax.3_false-unreach-call.4.ufo.BOUNDED-6.pals.c witness timeout 18    9.1  83 wit timeout 90   73   4000 true 12   6.8 350
seq-mthreaded/pals_floodmax.3_false-unreach-call.4.ufo.UNBOUNDED.pals.c witness timeout 22    11    83 wit timeout 91   70   4000 true 14   7.9 340
seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals.c witness timeout 170    87    130 wit timeout 91   70   3900 true 16   9.1 370
seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c witness timeout 150    73    120 wit timeout 91   69   3900 true 16   10   350
seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.BOUNDED-8.pals.c witness timeout 150    75    110 wit timeout 91   73   3900 true 17   11   350
seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c witness timeout 120    61    100 wit timeout 91   70   3900 true 15   8.6 360
seq-mthreaded/pals_floodmax.4_false-unreach-call.3.ufo.BOUNDED-8.pals.c witness timeout 690    350    140 wit timeout 91   70   3900 true 16   8.8 380
seq-mthreaded/pals_floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c witness timeout 320    160    120 wit timeout 91   70   3900 true 15   8.4 370
seq-mthreaded/pals_floodmax.4_false-unreach-call.4.ufo.BOUNDED-8.pals.c witness timeout 750    380    140 wit timeout 91   69   3900 true 17   9.4 380
seq-mthreaded/pals_floodmax.4_false-unreach-call.4.ufo.UNBOUNDED.pals.c timeout 900    450    130 wit - -
seq-mthreaded/pals_floodmax.5_false-unreach-call.1.ufo.BOUNDED-10.pals.c timeout 900    450    140 wit - -
seq-mthreaded/pals_floodmax.5_false-unreach-call.1.ufo.UNBOUNDED.pals.c timeout 900    450    140 wit - -
seq-mthreaded/pals_floodmax.5_false-unreach-call.2.ufo.BOUNDED-10.pals.c timeout 900    450    150 wit - -
seq-mthreaded/pals_floodmax.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c witness timeout 420    210    150 wit timeout 91   70   3800 true 21   14   480
seq-mthreaded/pals_floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals.c timeout 900    450    150 wit - -
seq-mthreaded/pals_floodmax.5_false-unreach-call.3.ufo.UNBOUNDED.pals.c timeout 900    450    150 wit - -
seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.BOUNDED-10.pals.c timeout 900    450    150 wit - -
seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.UNBOUNDED.pals.c timeout 900    450    160 wit - -
seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.1.ufo.BOUNDED-6.pals.c witness timeout 28    14    98 wit timeout 91   69   4200 true 13   9.9 330
seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.1.ufo.UNBOUNDED.pals.c witness timeout 24    12    88 wit timeout 91   71   4100 true 13   8.2 330
seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals.c witness timeout 31    16    87 wit timeout 91   72   4100 true 13   8.6 330
seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c witness timeout 11    5.6  78 wit timeout 91   72   4100 true 13   8.4 330
seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.1.ufo.BOUNDED-8.pals.c witness timeout 310    160    120 wit timeout 91   72   4100 true 13   7.7 330
seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c witness timeout 350    170    130 wit timeout 91   70   4100 true 14   8.0 340
seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.2.ufo.BOUNDED-8.pals.c witness timeout 130    64    120 wit timeout 91   70   4000 true 15   8.9 350
seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c witness timeout 250    130    160 wit timeout 91   69   4000 true 12   7.4 330
seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.1.ufo.BOUNDED-10.pals.c timeout 900    450    150 wit - -
seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.1.ufo.UNBOUNDED.pals.c timeout 900    450    150 wit - -
seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.BOUNDED-10.pals.c timeout 900    450    150 wit - -
seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c timeout 900    450    160 wit - -
seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.1.ufo.BOUNDED-12.pals.c timeout 900    450    150 wit - -
seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.1.ufo.UNBOUNDED.pals.c timeout 900    450    160 wit - -
seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.2.ufo.BOUNDED-12.pals.c timeout 900    450    150 wit - -
seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.2.ufo.UNBOUNDED.pals.c timeout 900    450    160 wit - -
seq-mthreaded/pals_lcr.3_false-unreach-call.1.ufo.BOUNDED-6.pals.c witness timeout 8.2  4.1  63 wit timeout 91   71   4000 true 13   7.2 350
seq-mthreaded/pals_lcr.3_false-unreach-call.1.ufo.UNBOUNDED.pals.c witness timeout 9.4  4.7  63 wit timeout 91   70   4200 true 13   8.5 340
seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.BOUNDED-8.pals.c witness timeout 39    19    84 wit timeout 91   71   4000 true 15   8.5 340
seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c witness timeout 29    15    77 wit timeout 90   73   4000 true 12   6.8 340
seq-mthreaded/pals_lcr.5_false-unreach-call.1.ufo.BOUNDED-10.pals.c witness timeout 180    89    110 wit timeout 91   70   4100 true 14   8.2 340
seq-mthreaded/pals_lcr.5_false-unreach-call.1.ufo.UNBOUNDED.pals.c witness timeout 210    100    120 wit timeout 91   68   4100 true 13   7.6 330
seq-mthreaded/pals_lcr.6_false-unreach-call.1.ufo.BOUNDED-12.pals.c timeout 900    450    150 wit - -
seq-mthreaded/pals_lcr.6_false-unreach-call.1.ufo.UNBOUNDED.pals.c timeout 900    450    160 wit - -
seq-mthreaded/pals_lcr.7_false-unreach-call.1.ufo.BOUNDED-14.pals.c timeout 900    450    150 wit - -
seq-mthreaded/pals_lcr.7_false-unreach-call.1.ufo.UNBOUNDED.pals.c timeout 900    450    150 wit - -
seq-mthreaded/pals_lcr.8_false-unreach-call.1.ufo.BOUNDED-16.pals.c timeout 900    450    200 wit - -
seq-mthreaded/pals_lcr.8_false-unreach-call.1.ufo.UNBOUNDED.pals.c timeout 900    450    200 wit - -
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.1.ufo.BOUNDED-6.pals.c witness timeout 19    9.3  85 wit timeout 91   69   4000 true 15   9.7 350
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.1.ufo.UNBOUNDED.pals.c witness timeout 16    8.0  83 wit timeout 91   71   4100 true 14   7.8 340
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.2.ufo.BOUNDED-6.pals.c witness timeout 3.0  1.5  83 wit timeout 91   71   4000 true 13   7.5 350
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c witness timeout 3.3  1.7  80 wit timeout 91   69   4100 true 13   8.7 330
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.3.ufo.BOUNDED-6.pals.c witness timeout 18    8.8  89 wit timeout 91   70   4000 true 15   9.7 330
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.3.ufo.UNBOUNDED.pals.c witness timeout 19    9.6  87 wit timeout 91   70   4000 true 12   7.7 330
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.4.ufo.BOUNDED-6.pals.c witness timeout 18    9.2  88 wit timeout 91   71   4000 true 16   9.7 350
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.4.ufo.UNBOUNDED.pals.c witness timeout 21    10    86 wit timeout 91   71   4000 true 14   7.9 340
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals.c timeout 900    450    150 wit - -
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c witness timeout 150    74    130 wit timeout 91   69   3900 true 17   10   390
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.2.ufo.BOUNDED-8.pals.c witness timeout 54    27    95 wit timeout 91   71   3900 true 17   9.7 370
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c witness timeout 78    39    98 wit timeout 91   68   3900 true 17   9.8 380
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.3.ufo.BOUNDED-8.pals.c witness timeout 760    380    140 wit timeout 91   70   3900 true 15   9.1 390
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c timeout 900    450    130 wit - -
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.4.ufo.BOUNDED-8.pals.c timeout 900    450    130 wit - -
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.4.ufo.UNBOUNDED.pals.c timeout 900    450    130 wit - -
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.1.ufo.BOUNDED-10.pals.c timeout 900    450    140 wit - -
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.1.ufo.UNBOUNDED.pals.c timeout 900    450    130 wit - -
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.2.ufo.BOUNDED-10.pals.c timeout 900    450    150 wit - -
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c witness timeout 530    270    170 wit timeout 91   71   3900 true 21   12   480
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals.c timeout 900    450    150 wit - -
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.3.ufo.UNBOUNDED.pals.c timeout 900    450    160 wit - -
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.4.ufo.BOUNDED-10.pals.c timeout 900    450    160 wit - -
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.4.ufo.UNBOUNDED.pals.c timeout 900    450    160 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.1.M1.c killed by signal 9 630    310    15000 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.1.M4.c timeout 900    450    11000 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.2.M1.c killed by signal 9 260    130    15000 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.2.M4.c timeout 900    450    12000 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.3.M1.c timeout 900    450    14000 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.3.M4.c timeout 900    450    13000 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.4.M1.c timeout 900    450    590 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.4.M4.c timeout 900    450    12000 wit - -
seq-mthreaded/rekcba_ctm_false-unreach-call.2.c timeout 900    450    6000 wit - -
seq-mthreaded/rekcba_ctm_false-unreach-call.3.c timeout 900    450    8900 wit - -
seq-mthreaded/rekcba_nxt_false-unreach-call.1.M1.c witness timeout 440    220    8600 wit timeout 91   63   2200 true 20   11   480
seq-mthreaded/rekcba_nxt_false-unreach-call.1.M4.c timeout 900    450    12000 wit - -
seq-mthreaded/rekcba_nxt_false-unreach-call.2.M1.c timeout 900    450    6900 wit - -
seq-mthreaded/rekcba_nxt_false-unreach-call.2.M4.c timeout 900    450    11000 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.1.M1.c timeout 900    450    7100 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.1.M4.c timeout 900    450    13000 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.2.M1.c timeout 900    450    5800 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.2.M4.c timeout 900    450    13000 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.4.M1.c timeout 900    450    5000 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.4.M4.c timeout 900    450    13000 wit - -
seq-mthreaded/rekh_ctm_false-unreach-call.2.c witness timeout 770    380    3500 wit timeout 90   64   3900 error 28   17   550
seq-mthreaded/rekh_ctm_false-unreach-call.3.c timeout 900    450    4900 wit - -
seq-mthreaded/rekh_nxt_false-unreach-call.1.M1.c witness timeout 140    70    520 wit timeout 91   68   3900 error 25   15   490
seq-mthreaded/rekh_nxt_false-unreach-call.1.M4.c timeout 900    450    4000 wit - -
seq-mthreaded/rekh_nxt_false-unreach-call.2.M1.c timeout 900    450    2800 wit - -
seq-mthreaded/rekh_nxt_false-unreach-call.2.M4.c timeout 900    450    11000 wit - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_true-unreach-call.ufo.BOUNDED-10.pals.c true 2.5  1.3  73 wit - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_true-unreach-call.ufo.UNBOUNDED.pals.c true 2.9  1.5  72 wit - -
seq-mthreaded/pals_STARTPALS_Triplicated_true-unreach-call.ufo.BOUNDED-10.pals.c true 1.2  .62 81 wit - -
seq-mthreaded/pals_STARTPALS_Triplicated_true-unreach-call.ufo.UNBOUNDED.pals.c true .98 .51 79 wit - -
seq-mthreaded/pals_floodmax.3_true-unreach-call.ufo.BOUNDED-6.pals.c true 100    51    100 wit - -
seq-mthreaded/pals_floodmax.3_true-unreach-call.ufo.UNBOUNDED.pals.c true 140    71    120 wit - -
seq-mthreaded/pals_floodmax.4_true-unreach-call.ufo.BOUNDED-8.pals.c timeout 900    450    130 wit - -
seq-mthreaded/pals_floodmax.4_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900    450    130 wit - -
seq-mthreaded/pals_floodmax.5_true-unreach-call.ufo.BOUNDED-10.pals.c timeout 900    450    150 wit - -
seq-mthreaded/pals_floodmax.5_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900    450    160 wit - -
seq-mthreaded/pals_lcr-var-start-time.3_true-unreach-call.ufo.BOUNDED-6.pals.c true 230    120    170 wit - -
seq-mthreaded/pals_lcr-var-start-time.3_true-unreach-call.ufo.UNBOUNDED.pals.c true 600    300    320 wit - -
seq-mthreaded/pals_lcr-var-start-time.4_true-unreach-call.ufo.BOUNDED-8.pals.c timeout 900    450    170 wit - -
seq-mthreaded/pals_lcr-var-start-time.4_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900    450    190 wit - -
seq-mthreaded/pals_lcr-var-start-time.5_true-unreach-call.ufo.BOUNDED-10.pals.c timeout 900    450    150 wit - -
seq-mthreaded/pals_lcr-var-start-time.5_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900    450    150 wit - -
seq-mthreaded/pals_lcr-var-start-time.6_true-unreach-call.ufo.BOUNDED-12.pals.c timeout 900    450    150 wit - -
seq-mthreaded/pals_lcr-var-start-time.6_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900    450    160 wit - -
seq-mthreaded/pals_lcr.3_true-unreach-call.ufo.BOUNDED-6.pals.c true 24    12    75 wit - -
seq-mthreaded/pals_lcr.3_true-unreach-call.ufo.UNBOUNDED.pals.c true 22    11    74 wit - -
seq-mthreaded/pals_lcr.4_true-unreach-call.ufo.BOUNDED-8.pals.c true 200    99    170 wit - -
seq-mthreaded/pals_lcr.4_true-unreach-call.ufo.UNBOUNDED.pals.c true 280    140    180 wit - -
seq-mthreaded/pals_lcr.5_true-unreach-call.ufo.BOUNDED-10.pals.c timeout 900    450    230 wit - -
seq-mthreaded/pals_lcr.5_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900    450    290 wit - -
seq-mthreaded/pals_lcr.6_true-unreach-call.ufo.BOUNDED-12.pals.c timeout 900    450    160 wit - -
seq-mthreaded/pals_lcr.6_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900    450    150 wit - -
seq-mthreaded/pals_lcr.7_true-unreach-call.ufo.BOUNDED-14.pals.c timeout 900    450    150 wit - -
seq-mthreaded/pals_lcr.7_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900    450    160 wit - -
seq-mthreaded/pals_lcr.8_true-unreach-call.ufo.BOUNDED-16.pals.c timeout 900    450    200 wit - -
seq-mthreaded/pals_lcr.8_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900    450    170 wit - -
seq-mthreaded/pals_opt-floodmax.3_true-unreach-call.ufo.BOUNDED-6.pals.c true 150    73    120 wit - -
seq-mthreaded/pals_opt-floodmax.3_true-unreach-call.ufo.UNBOUNDED.pals.c true 140    69    120 wit - -
seq-mthreaded/pals_opt-floodmax.4_true-unreach-call.ufo.BOUNDED-8.pals.c timeout 900    450    130 wit - -
seq-mthreaded/pals_opt-floodmax.4_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900    450    130 wit - -
seq-mthreaded/pals_opt-floodmax.5_true-unreach-call.ufo.BOUNDED-10.pals.c timeout 900    450    170 wit - -
seq-mthreaded/pals_opt-floodmax.5_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900    450    150 wit - -
seq-mthreaded/rekcba_aso_true-unreach-call.1.M1.c killed by signal 9 580    290    15000 wit - -
seq-mthreaded/rekcba_aso_true-unreach-call.1.M4.c timeout 900    450    11000 wit - -
seq-mthreaded/rekcba_aso_true-unreach-call.2.M1.c timeout 900    450    550 wit - -
seq-mthreaded/rekcba_aso_true-unreach-call.2.M4.c timeout 900    450    12000 wit - -
seq-mthreaded/rekcba_ctm_true-unreach-call.1.c timeout 900    450    6000 wit - -
seq-mthreaded/rekcba_ctm_true-unreach-call.2.c timeout 900    450    8600 wit - -
seq-mthreaded/rekcba_ctm_true-unreach-call.3.c timeout 900    450    9000 wit - -
seq-mthreaded/rekcba_ctm_true-unreach-call.4.c timeout 900    450    15000 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.1.M1.c false(reach) 660    330    8600 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.1.M4.c timeout 900    450    9400 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.2.M1.c false(reach) 640    320    12000 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.2.M4.c timeout 900    450    9900 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.3.M1.c timeout 900    450    6800 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.3.M4.c timeout 900    450    10000 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.1.M1.c timeout 900    450    7900 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.1.M4.c timeout 900    450    12000 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.2.M1.c timeout 900    450    7700 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.2.M4.c timeout 900    450    13000 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.3.M1.c timeout 900    450    7800 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.3.M4.c killed by signal 9 630    310    15000 wit - -
seq-mthreaded/rekh_ctm_true-unreach-call.1.c timeout 900    450    3800 wit - -
seq-mthreaded/rekh_ctm_true-unreach-call.2.c timeout 900    450    3400 wit - -
seq-mthreaded/rekh_ctm_true-unreach-call.3.c timeout 900    450    4800 wit - -
seq-mthreaded/rekh_ctm_true-unreach-call.4.c timeout 900    450    6800 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.1.M1.c true 290    140    2000 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.1.M4.c timeout 900    450    4000 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.2.M1.c true 560    280    950 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.2.M4.c timeout 900    450    10000 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.3.M1.c timeout 900    450    2700 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.3.M4.c timeout 900    450    10000 wit - -
seq-pthread/cs_fib_false-unreach-call.i witness timeout 4.3  2.2  120 wit timeout 91   70   1400 error 9.4 5.2 310
seq-pthread/cs_fib_longer_false-unreach-call.i witness timeout 5.1  2.6  110 wit timeout 90   71   1900 error 10   6.7 300
seq-pthread/cs_lazy_false-unreach-call.i witness timeout 1.0  .55 65 wit timeout 91   83   900 true 23   12   680
seq-pthread/cs_queue_false-unreach-call.i witness timeout 29    15    170 wit timeout 91   66   1800 error 52   41   5800
seq-pthread/cs_read_write_lock_false-unreach-call.i witness timeout 1.8  .93 84 wit timeout 91   83   1100 error 11   6.5 320
seq-pthread/cs_stack_false-unreach-call.i witness timeout 2.8  1.5  110 wit timeout 91   66   1800 error 10   6.7 320
seq-pthread/cs_stateful_false-unreach-call.i witness timeout 1.1  .60 63 wit timeout 91   83   770 true 20   11   500
seq-pthread/cs_dekker_true-unreach-call.i false(reach) 2.9  1.5  140 wit - -
seq-pthread/cs_fib_longer_true-unreach-call.i false(reach) 68    34    160 wit - -
seq-pthread/cs_fib_true-unreach-call.i false(reach) 31    15    110 wit - -
seq-pthread/cs_lamport_true-unreach-call.i false(reach) 2.0  1.0  120 wit - -
seq-pthread/cs_peterson_true-unreach-call.i false(reach) 2.1  1.1  110 wit - -
seq-pthread/cs_queue_true-unreach-call.i false(reach) 880    440    510 wit - -
seq-pthread/cs_read_write_lock_true-unreach-call.i false(reach) 3.0  1.5  100 wit - -
seq-pthread/cs_stack_true-unreach-call.i false(reach) 2.9  1.5  110 wit - -
seq-pthread/cs_stateful_true-unreach-call.i false(reach) 1.0  .52 64 wit - -
seq-pthread/cs_sync_true-unreach-call.i false(reach) 5.0  2.5  130 wit - -
seq-pthread/cs_szymanski_true-unreach-call.i false(reach) 1.8  .93 110 wit - -
seq-pthread/cs_time_var_mutex_true-unreach-call.i false(reach) 3.6  1.8  230 wit - -
../../sv-benchmarks/c/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime (s) wit1_walltime (s) wit1_memUsage (MB) wit2_status wit2_cputime (s) wit2_walltime (s) wit2_memUsage (MB)
total tasks 261 120000 62000 580000 261 6300   4700   230000   261 1500   920   41000  
    correct results 72 8800 4400 42000 41 930   520   28000   41 570   350   14000  
        correct true 31 5400 2700 13000 0 0   0   0   41 0   0   0  
        correct false 41 3300 1700 29000 41 930   520   28000   0 570   350   14000  
    incorrect results 14 2300 1100 22000 0 0   0   0   0 0   0   0  
        incorrect true 0
        incorrect false 14 2300 1100 22000 0 0   0   0   0 0   0   0  
score (261 tasks, max score: 364) -121
Run set sv-comp16.Sequentialized