Tool CPAchecker 1.4-svn 18356M
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-10 22:01:17 CET [[ 2016-01-15 09:16:15 CET ]] [[ 2016-01-15 22:26:01 CET ]]
Run set sv-comp16.Sequentialized
Options -lpi-svcomp16 -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/lpi.2016-01-10_2201.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/lpi.2016-01-10_2201.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 unknown 65   20   1100 wit - -
systemc/kundu2_false-unreach-call_false-termination.cil.c false(reach) 29   6.7 730 wit false(reach) 13   7.3 500 false(reach) 36 20   560
systemc/pc_sfifo_1_false-unreach-call_false-termination.cil.c false(reach) 6.6 2.3 330 wit false(reach) 8.1 4.4 350 false(reach) 16 9.3 360
systemc/pc_sfifo_2_false-unreach-call_false-termination.cil.c false(reach) 7.1 2.4 350 wit false(reach) 8.0 4.4 370 false(reach) 24 15   510
systemc/pipeline_false-unreach-call_false-termination.cil.c timeout 900   350   7800 wit - -
systemc/token_ring.01_false-unreach-call_false-termination.cil.c false(reach) 22   5.3 570 wit false(reach) 9.4 5.2 420 false(reach) 29 16   530
systemc/token_ring.02_false-unreach-call_false-termination.cil.c false(reach) 26   5.9 660 wit false(reach) 13   7.1 490 false(reach) 40 23   670
systemc/token_ring.03_false-unreach-call_false-termination.cil.c false(reach) 32   6.9 730 wit false(reach) 16   8.8 530 false(reach) 52 31   790
systemc/token_ring.04_false-unreach-call_false-termination.cil.c false(reach) 38   7.9 930 wit false(reach) 18   9.9 580 false(reach) 64 39   1100
systemc/token_ring.05_false-unreach-call_false-termination.cil.c false(reach) 42   9.0 970 wit false(reach) 20   10   610 false(reach) 73 41   1200
systemc/token_ring.06_false-unreach-call_false-termination.cil.c false(reach) 48   10   950 wit false(reach) 22   12   650 false(reach) 86 49   1600
systemc/token_ring.07_false-unreach-call_false-termination.cil.c false(reach) 47   10   980 wit false(reach) 27   14   810 timeout 92 51   1400
systemc/token_ring.08_false-unreach-call_false-termination.cil.c false(reach) 55   13   1100 wit false(reach) 29   15   840 timeout 91 55   1500
systemc/token_ring.09_false-unreach-call_false-termination.cil.c false(reach) 60   14   1200 wit false(reach) 31   16   850 timeout 91 54   1500
systemc/token_ring.10_false-unreach-call_false-termination.cil.c false(reach) 61   15   1200 wit false(reach) 33   18   870 timeout 91 53   1500
systemc/token_ring.11_false-unreach-call_false-termination.cil.c timeout (false(reach)) 900   840   4800 wit - -
systemc/token_ring.12_false-unreach-call_false-termination.cil.c false(reach) 76   20   1500 wit false(reach) 46   24   1500 timeout 91 54   1600
systemc/token_ring.13_false-unreach-call_false-termination.cil.c false(reach) 84   24   1600 wit false(reach) 46   25   1500 timeout 92 56   2000
systemc/token_ring.14_false-unreach-call_false-termination.cil.c false(reach) 74   19   1500 wit false(reach) 36   19   1500 timeout 90 52   1600
systemc/token_ring.15_false-unreach-call_false-termination.cil.c false(reach) 89   26   1600 wit false(reach) 44   24   1500 timeout 90 53   1700
systemc/toy1_false-unreach-call_false-termination.cil.c unknown 71   21   1200 wit - -
systemc/toy2_false-unreach-call_false-termination.cil.c unknown 67   20   1100 wit - -
systemc/transmitter.01_false-unreach-call_false-termination.cil.c segmentation fault 9.8 2.6 350 wit - -
systemc/transmitter.02_false-unreach-call_false-termination.cil.c false(reach) 15   3.7 410 wit false(reach) 9.9 5.4 460 false(reach) 30 17   530
systemc/transmitter.03_false-unreach-call_false-termination.cil.c false(reach) 22   4.9 510 wit false(reach) 13   6.9 490 false(reach) 45 28   750
systemc/transmitter.04_false-unreach-call_false-termination.cil.c false(reach) 25   5.4 630 wit false(reach) 17   8.8 520 false(reach) 46 26   780
systemc/transmitter.05_false-unreach-call_false-termination.cil.c false(reach) 26   5.8 690 wit false(reach) 16   8.4 560 false(reach) 72 41   1100
systemc/transmitter.06_false-unreach-call_false-termination.cil.c false(reach) 32   6.5 780 wit false(reach) 22   11   610 false(reach) 76 44   1300
systemc/transmitter.07_false-unreach-call_false-termination.cil.c false(reach) 36   7.4 910 wit false(reach) 23   12   710 timeout 91 52   1400
systemc/transmitter.08_false-unreach-call_false-termination.cil.c false(reach) 42   8.5 900 wit false(reach) 25   13   810 timeout 92 53   1700
systemc/transmitter.09_false-unreach-call_false-termination.cil.c false(reach) 45   9.2 950 wit false(reach) 30   16   860 timeout 91 53   1600
systemc/transmitter.10_false-unreach-call_false-termination.cil.c false(reach) 50   10   980 wit false(reach) 33   17   860 timeout 91 53   1500
systemc/transmitter.11_false-unreach-call_false-termination.cil.c false(reach) 53   12   1000 wit false(reach) 41   21   1000 timeout 92 52   1700
systemc/transmitter.12_false-unreach-call_false-termination.cil.c false(reach) 57   13   1100 wit false(reach) 38   20   1500 timeout 92 54   1500
systemc/transmitter.13_false-unreach-call_false-termination.cil.c false(reach) 61   15   1300 wit false(reach) 45   24   1100 timeout 92 55   1700
systemc/transmitter.15_false-unreach-call_false-termination.cil.c false(reach) 14   3.7 490 wit false(reach) 20   10   620 timeout 92 54   1400
systemc/transmitter.16_false-unreach-call_false-termination.cil.c false(reach) 16   4.3 510 wit false(reach) 20   10   620 timeout 92 55   1400
systemc/bist_cell_true-unreach-call_false-termination.cil.c true 21   4.7 510 wit - -
systemc/kundu_true-unreach-call_false-termination.cil.c timeout 900   380   6100 wit - -
systemc/mem_slave_tlm.1_true-unreach-call_false-termination.cil.c timeout 900   330   9200 wit - -
systemc/mem_slave_tlm.2_true-unreach-call_false-termination.cil.c timeout 900   340   8800 wit - -
systemc/mem_slave_tlm.3_true-unreach-call_false-termination.cil.c timeout 900   330   8700 wit - -
systemc/mem_slave_tlm.4_true-unreach-call_false-termination.cil.c timeout 900   320   9000 wit - -
systemc/mem_slave_tlm.5_true-unreach-call_false-termination.cil.c timeout 910   310   9200 wit - -
systemc/pc_sfifo_1_true-unreach-call_false-termination.cil.c timeout 900   390   6500 wit - -
systemc/pc_sfifo_2_true-unreach-call_false-termination.cil.c timeout 900   370   7100 wit - -
systemc/pc_sfifo_3_true-unreach-call_false-termination.cil.c timeout 900   400   5800 wit - -
systemc/pipeline_true-unreach-call_false-termination.cil.c timeout 900   370   7900 wit - -
systemc/token_ring.01_true-unreach-call_false-termination.cil.c timeout 900   380   6400 wit - -
systemc/token_ring.02_true-unreach-call_false-termination.cil.c timeout 900   410   4400 wit - -
systemc/token_ring.03_true-unreach-call_false-termination.cil.c timeout 900   400   4900 wit - -
systemc/token_ring.04_true-unreach-call_false-termination.cil.c timeout 900   390   5900 wit - -
systemc/token_ring.05_true-unreach-call_false-termination.cil.c timeout 900   380   6000 wit - -
systemc/token_ring.06_true-unreach-call_false-termination.cil.c timeout 900   400   5200 wit - -
systemc/token_ring.07_true-unreach-call_false-termination.cil.c timeout 900   400   5500 wit - -
systemc/token_ring.08_true-unreach-call_false-termination.cil.c timeout 900   420   4700 wit - -
systemc/token_ring.09_true-unreach-call_false-termination.cil.c timeout 900   400   7300 wit - -
systemc/token_ring.10_true-unreach-call_false-termination.cil.c timeout 900   410   7400 wit - -
systemc/token_ring.11_true-unreach-call_false-termination.cil.c timeout 900   400   6900 wit - -
systemc/token_ring.12_true-unreach-call_false-termination.cil.c timeout 900   410   7100 wit - -
systemc/token_ring.13_true-unreach-call_false-termination.cil.c timeout 900   410   7100 wit - -
systemc/toy_true-unreach-call_false-termination.cil.c timeout 900   390   6000 wit - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c false(reach) 17   7.2 550 wit false(reach) 14   7.5 550 false(reach) 28 18   520
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 17   7.4 560 wit false(reach) 17   9.2 570 false(reach) 25 13   510
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.BOUNDED-10.pals.c false(reach) 110   94   1200 wit false(reach) 16   8.7 620 false(reach) 36 20   550
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.UNBOUNDED.pals.c false(reach) 110   93   1100 wit false(reach) 20   10   650 false(reach) 36 20   580
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_2.ufo.BOUNDED-10.pals.c false(reach) 120   100   1200 wit false(reach) 21   11   630 false(reach) 35 20   570
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_2.ufo.UNBOUNDED.pals.c false(reach) 120   99   1200 wit false(reach) 17   9.2 620 false(reach) 31 17   530
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.5.ufo.BOUNDED-10.pals.c timeout 900   870   2300 wit - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.5.ufo.UNBOUNDED.pals.c timeout 900   870   2300 wit - -
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.1.ufo.BOUNDED-10.pals.c witness unconfirmed 450   360   3100 wit true 17   8.9 580 true 34 19   840
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.1.ufo.UNBOUNDED.pals.c timeout 900   750   4400 wit - -
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.BOUNDED-10.pals.c witness unconfirmed 460   370   3100 wit true 14   7.2 550 true 32 17   660
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.UNBOUNDED.pals.c segmentation fault 230   92   3800 wit - -
seq-mthreaded/pals_floodmax.3_false-unreach-call.1.ufo.BOUNDED-6.pals.c false(reach) 32   6.7 760 wit false(reach) 16   8.8 530 false(reach) 47 33   740
seq-mthreaded/pals_floodmax.3_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 30   6.4 670 wit false(reach) 17   8.9 520 false(reach) 38 22   670
seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.BOUNDED-6.pals.c false(reach) 19   4.5 520 wit false(reach) 16   8.6 530 timeout 90 76   630
seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 18   4.5 520 wit false(reach) 15   8.2 490 false(reach) 57 40   720
seq-mthreaded/pals_floodmax.3_false-unreach-call.3.ufo.BOUNDED-6.pals.c false(reach) 31   6.7 710 wit false(reach) 18   9.5 550 timeout 92 65   1500
seq-mthreaded/pals_floodmax.3_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(reach) 31   6.6 680 wit false(reach) 14   7.7 530 false(reach) 47 29   770
seq-mthreaded/pals_floodmax.3_false-unreach-call.4.ufo.BOUNDED-6.pals.c false(reach) 32   6.7 820 wit false(reach) 15   8.0 540 false(reach) 58 37   970
seq-mthreaded/pals_floodmax.3_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(reach) 31   6.7 820 wit false(reach) 16   8.6 530 false(reach) 50 32   770
seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals.c false(reach) 67   18   1500 wit false(reach) 27   14   870 timeout 92 59   1500
seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 60   17   1400 wit false(reach) 28   15   860 timeout 90 61   1500
seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.BOUNDED-8.pals.c false(reach) 51   12   920 wit false(reach) 26   14   770 true 20 11   530
seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 46   11   940 wit false(reach) 23   12   760 true 21 12   520
seq-mthreaded/pals_floodmax.4_false-unreach-call.3.ufo.BOUNDED-8.pals.c false(reach) 67   18   1400 wit false(reach) 27   14   870 true 21 12   510
seq-mthreaded/pals_floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(reach) 57   17   1300 wit false(reach) 29   15   910 true 23 12   520
seq-mthreaded/pals_floodmax.4_false-unreach-call.4.ufo.BOUNDED-8.pals.c false(reach) 76   24   2000 wit false(reach) 29   15   890 true 22 13   510
seq-mthreaded/pals_floodmax.4_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(reach) 72   19   1500 wit false(reach) 29   15   900 true 22 12   510
seq-mthreaded/pals_floodmax.5_false-unreach-call.1.ufo.BOUNDED-10.pals.c false(reach) 160   83   3100 wit false(reach) 40   21   1500 timeout 92 53   2000
seq-mthreaded/pals_floodmax.5_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 160   84   3000 wit false(reach) 42   22   1400 timeout 90 51   1900
seq-mthreaded/pals_floodmax.5_false-unreach-call.2.ufo.BOUNDED-10.pals.c false(reach) 120   57   2200 wit false(reach) 36   19   930 true 28 18   560
seq-mthreaded/pals_floodmax.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 120   60   1900 wit false(reach) 34   18   1500 true 28 15   560
seq-mthreaded/pals_floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals.c false(reach) 180   92   3500 wit false(reach) 41   21   1500 true 27 15   570
seq-mthreaded/pals_floodmax.5_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(reach) 170   87   3400 wit false(reach) 35   18   1500 true 29 16   570
seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.BOUNDED-10.pals.c false(reach) 220   110   4100 wit false(reach) 35   18   1400 true 27 15   560
seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(reach) 260   130   4100 wit false(reach) 39   20   1400 true 28 16   590
seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.1.ufo.BOUNDED-6.pals.c false(reach) 28   5.8 620 wit false(reach) 13   7.1 510 false(reach) 26 14   500
seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 30   6.1 630 wit false(reach) 16   8.7 510 false(reach) 31 17   530
seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals.c false(reach) 29   5.9 620 wit false(reach) 15   8.0 530 false(reach) 35 22   540
seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 26   5.4 610 wit false(reach) 17   8.7 500 false(reach) 28 15   510
seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.1.ufo.BOUNDED-8.pals.c false(reach) 42   8.8 870 wit false(reach) 20   10   570 false(reach) 43 31   530
seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 38   8.2 900 wit false(reach) 19   10   580 false(reach) 87 62   850
seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.2.ufo.BOUNDED-8.pals.c false(reach) 36   8.1 870 wit false(reach) 18   9.5 570 false(reach) 29 18   410
seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 42   8.6 880 wit false(reach) 18   9.7 580 false(reach) 35 22   570
seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.1.ufo.BOUNDED-10.pals.c false(reach) 51   12   1200 wit false(reach) 24   13   700 timeout 91 70   1100
seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 55   13   1200 wit false(reach) 24   13   660 false(reach) 61 41   780
seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.BOUNDED-10.pals.c false(reach) 56   14   1200 wit false(reach) 23   12   650 false(reach) 41 27   620
seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 53   13   1200 wit false(reach) 23   12   620 false(reach) 35 19   580
seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.1.ufo.BOUNDED-12.pals.c false(reach) 89   28   1600 wit false(reach) 27   14   880 timeout 91 81   590
seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 82   25   1600 wit false(reach) 26   14   860 timeout 90 72   790
seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.2.ufo.BOUNDED-12.pals.c false(reach) 88   28   1800 wit false(reach) 29   15   860 false(reach) 56 39   600
seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 74   23   1600 wit false(reach) 24   13   840 timeout 90 75   700
seq-mthreaded/pals_lcr.3_false-unreach-call.1.ufo.BOUNDED-6.pals.c false(reach) 27   5.6 550 wit false(reach) 16   8.3 500 false(reach) 33 19   540
seq-mthreaded/pals_lcr.3_false-unreach-call.1.ufo.UNBOUNDED.pals.c segmentation fault 21   4.2 510 wit - -
seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.BOUNDED-8.pals.c false(reach) 36   7.9 830 wit false(reach) 17   9.2 560 false(reach) 51 35   730
seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 34   7.6 850 wit false(reach) 18   9.6 590 false(reach) 45 29   570
seq-mthreaded/pals_lcr.5_false-unreach-call.1.ufo.BOUNDED-10.pals.c false(reach) 48   11   1000 wit false(reach) 21   11   650 timeout 90 74   810
seq-mthreaded/pals_lcr.5_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 48   12   970 wit false(reach) 23   12   640 timeout 91 68   820
seq-mthreaded/pals_lcr.6_false-unreach-call.1.ufo.BOUNDED-12.pals.c false(reach) 72   19   1300 wit false(reach) 28   15   850 timeout 90 69   830
seq-mthreaded/pals_lcr.6_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 69   19   1500 wit false(reach) 27   14   830 timeout 90 71   780
seq-mthreaded/pals_lcr.7_false-unreach-call.1.ufo.BOUNDED-14.pals.c false(reach) 98   33   2400 wit false(reach) 33   17   890 timeout 91 67   1000
seq-mthreaded/pals_lcr.7_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 110   37   2300 wit false(reach) 27   14   890 timeout 91 62   1200
seq-mthreaded/pals_lcr.8_false-unreach-call.1.ufo.BOUNDED-16.pals.c false(reach) 160   70   4100 wit false(reach) 39   21   1000 timeout 91 56   1600
seq-mthreaded/pals_lcr.8_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 160   62   4000 wit false(reach) 47   24   990 timeout 90 59   1200
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.1.ufo.BOUNDED-6.pals.c false(reach) 31   7.2 740 wit false(reach) 17   9.0 620 false(reach) 57 34   990
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 33   7.3 730 wit false(reach) 19   10   610 false(reach) 45 26   740
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.2.ufo.BOUNDED-6.pals.c false(reach) 20   4.9 540 wit false(reach) 19   9.9 580 false(reach) 69 51   950
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 21   4.7 520 wit false(reach) 18   9.7 590 false(reach) 79 58   1000
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.3.ufo.BOUNDED-6.pals.c false(reach) 33   7.1 740 wit false(reach) 20   11   610 false(reach) 44 27   750
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(reach) 32   7.0 710 wit false(reach) 19   10   630 false(reach) 58 36   910
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.4.ufo.BOUNDED-6.pals.c false(reach) 32   7.0 740 wit false(reach) 19   10   600 false(reach) 80 53   1100
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(reach) 35   7.6 880 wit false(reach) 19   10   620 timeout 91 62   1300
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals.c segmentation fault 55   12   1400 wit - -
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c segmentation fault 56   11   1300 wit - -
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.2.ufo.BOUNDED-8.pals.c false(reach) 45   13   930 wit false(reach) 27   14   810 true 20 12   500
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 52   13   930 wit false(reach) 27   14   870 true 19 11   500
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.3.ufo.BOUNDED-8.pals.c false(reach) 63   20   1300 wit false(reach) 29   15   900 true 19 10   490
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(reach) 67   20   1500 wit false(reach) 28   15   880 true 23 13   520
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.4.ufo.BOUNDED-8.pals.c false(reach) 77   23   1600 wit false(reach) 31   16   920 true 20 15   390
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(reach) 69   21   1500 wit false(reach) 25   13   890 true 22 12   510
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.1.ufo.BOUNDED-10.pals.c false(reach) 220   120   4000 wit false(reach) 38   20   1500 timeout 91 54   1400
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 190   100   3200 wit false(reach) 43   22   1400 timeout 92 50   2000
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.2.ufo.BOUNDED-10.pals.c false(reach) 130   68   1800 wit false(reach) 39   21   1400 true 25 14   560
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 140   71   2200 wit false(reach) 39   20   1400 true 27 17   550
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals.c false(reach) 210   110   3900 wit false(reach) 40   21   1500 true 28 16   580
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(reach) 190   100   3100 wit false(reach) 39   20   1400 true 28 15   570
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.4.ufo.BOUNDED-10.pals.c timeout (false(reach)) 900   570   10000 wit - -
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(reach) 320   170   4300 wit false(reach) 38   20   1400 true 28 16   570
seq-mthreaded/rekcba_aso_false-unreach-call.1.M1.c timeout 900   390   4800 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.1.M4.c timeout 900   410   4400 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.2.M1.c timeout 900   390   5000 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.2.M4.c timeout 900   420   3200 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.3.M1.c timeout 900   430   2600 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.3.M4.c timeout 900   420   5000 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.4.M1.c timeout 900   430   2600 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.4.M4.c timeout 900   420   4900 wit - -
seq-mthreaded/rekcba_ctm_false-unreach-call.2.c timeout 900   840   5000 wit - -
seq-mthreaded/rekcba_ctm_false-unreach-call.3.c timeout 900   840   5500 wit - -
seq-mthreaded/rekcba_nxt_false-unreach-call.1.M1.c unknown 770   320   7500 wit - -
seq-mthreaded/rekcba_nxt_false-unreach-call.1.M4.c timeout 900   400   5400 wit - -
seq-mthreaded/rekcba_nxt_false-unreach-call.2.M1.c timeout 900   650   6500 wit - -
seq-mthreaded/rekcba_nxt_false-unreach-call.2.M4.c timeout 900   420   4300 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.1.M1.c timeout 900   390   4700 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.1.M4.c timeout 900   430   2900 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.2.M1.c timeout 900   580   6100 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.2.M4.c timeout 900   430   3000 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.4.M1.c timeout 900   430   2000 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.4.M4.c timeout 900   410   5000 wit - -
seq-mthreaded/rekh_ctm_false-unreach-call.2.c timeout 900   860   3000 wit - -
seq-mthreaded/rekh_ctm_false-unreach-call.3.c timeout 900   860   3000 wit - -
seq-mthreaded/rekh_nxt_false-unreach-call.1.M1.c timeout 900   390   4300 wit - -
seq-mthreaded/rekh_nxt_false-unreach-call.1.M4.c timeout 900   430   2700 wit - -
seq-mthreaded/rekh_nxt_false-unreach-call.2.M1.c timeout 900   400   4200 wit - -
seq-mthreaded/rekh_nxt_false-unreach-call.2.M4.c timeout 900   430   3100 wit - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_true-unreach-call.ufo.BOUNDED-10.pals.c true 78   27   1400 wit - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   420   3600 wit - -
seq-mthreaded/pals_STARTPALS_Triplicated_true-unreach-call.ufo.BOUNDED-10.pals.c true 120   37   2300 wit - -
seq-mthreaded/pals_STARTPALS_Triplicated_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   410   5300 wit - -
seq-mthreaded/pals_floodmax.3_true-unreach-call.ufo.BOUNDED-6.pals.c segmentation fault 35   7.4 820 wit - -
seq-mthreaded/pals_floodmax.3_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   410   4700 wit - -
seq-mthreaded/pals_floodmax.4_true-unreach-call.ufo.BOUNDED-8.pals.c true 340   170   5800 wit - -
seq-mthreaded/pals_floodmax.4_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   410   4600 wit - -
seq-mthreaded/pals_floodmax.5_true-unreach-call.ufo.BOUNDED-10.pals.c timeout 900   380   11000 wit - -
seq-mthreaded/pals_floodmax.5_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   370   11000 wit - -
seq-mthreaded/pals_lcr-var-start-time.3_true-unreach-call.ufo.BOUNDED-6.pals.c true 29   5.4 660 wit - -
seq-mthreaded/pals_lcr-var-start-time.3_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   420   5100 wit - -
seq-mthreaded/pals_lcr-var-start-time.4_true-unreach-call.ufo.BOUNDED-8.pals.c true 37   7.8 820 wit - -
seq-mthreaded/pals_lcr-var-start-time.4_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   420   4000 wit - -
seq-mthreaded/pals_lcr-var-start-time.5_true-unreach-call.ufo.BOUNDED-10.pals.c true 56   14   1400 wit - -
seq-mthreaded/pals_lcr-var-start-time.5_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   410   4200 wit - -
seq-mthreaded/pals_lcr-var-start-time.6_true-unreach-call.ufo.BOUNDED-12.pals.c true 100   33   2200 wit - -
seq-mthreaded/pals_lcr-var-start-time.6_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   410   4700 wit - -
seq-mthreaded/pals_lcr.3_true-unreach-call.ufo.BOUNDED-6.pals.c true 25   5.1 600 wit - -
seq-mthreaded/pals_lcr.3_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   420   4100 wit - -
seq-mthreaded/pals_lcr.4_true-unreach-call.ufo.BOUNDED-8.pals.c true 35   7.0 810 wit - -
seq-mthreaded/pals_lcr.4_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   420   4000 wit - -
seq-mthreaded/pals_lcr.5_true-unreach-call.ufo.BOUNDED-10.pals.c true 49   11   1200 wit - -
seq-mthreaded/pals_lcr.5_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   420   4000 wit - -
seq-mthreaded/pals_lcr.6_true-unreach-call.ufo.BOUNDED-12.pals.c true 65   18   1600 wit - -
seq-mthreaded/pals_lcr.6_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   420   4400 wit - -
seq-mthreaded/pals_lcr.7_true-unreach-call.ufo.BOUNDED-14.pals.c true 100   34   2600 wit - -
seq-mthreaded/pals_lcr.7_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   420   4300 wit - -
seq-mthreaded/pals_lcr.8_true-unreach-call.ufo.BOUNDED-16.pals.c true 180   73   3500 wit - -
seq-mthreaded/pals_lcr.8_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   410   4500 wit - -
seq-mthreaded/pals_opt-floodmax.3_true-unreach-call.ufo.BOUNDED-6.pals.c true 38   7.9 1000 wit - -
seq-mthreaded/pals_opt-floodmax.3_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   400   4900 wit - -
seq-mthreaded/pals_opt-floodmax.4_true-unreach-call.ufo.BOUNDED-8.pals.c true 210   82   4600 wit - -
seq-mthreaded/pals_opt-floodmax.4_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   410   4600 wit - -
seq-mthreaded/pals_opt-floodmax.5_true-unreach-call.ufo.BOUNDED-10.pals.c timeout 900   380   10000 wit - -
seq-mthreaded/pals_opt-floodmax.5_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   370   9900 wit - -
seq-mthreaded/rekcba_aso_true-unreach-call.1.M1.c timeout 900   670   6500 wit - -
seq-mthreaded/rekcba_aso_true-unreach-call.1.M4.c timeout 900   410   4700 wit - -
seq-mthreaded/rekcba_aso_true-unreach-call.2.M1.c timeout 900   430   2700 wit - -
seq-mthreaded/rekcba_aso_true-unreach-call.2.M4.c timeout 900   420   5100 wit - -
seq-mthreaded/rekcba_ctm_true-unreach-call.1.c timeout 900   840   4900 wit - -
seq-mthreaded/rekcba_ctm_true-unreach-call.2.c timeout 900   840   4900 wit - -
seq-mthreaded/rekcba_ctm_true-unreach-call.3.c timeout 900   820   5500 wit - -
seq-mthreaded/rekcba_ctm_true-unreach-call.4.c timeout 900   740   7500 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.1.M1.c timeout 900   390   4700 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.1.M4.c timeout 900   400   5100 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.2.M1.c exception 310   110   4100 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.2.M4.c timeout 900   410   4400 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.3.M1.c timeout 900   550   6800 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.3.M4.c timeout 900   420   4200 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.1.M1.c unknown 850   510   7400 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.1.M4.c timeout 900   430   2800 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.2.M1.c timeout 900   430   2000 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.2.M4.c timeout 900   420   4700 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.3.M1.c timeout 900   430   2600 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.3.M4.c timeout 900   420   4800 wit - -
seq-mthreaded/rekh_ctm_true-unreach-call.1.c timeout 900   860   2900 wit - -
seq-mthreaded/rekh_ctm_true-unreach-call.2.c timeout 900   860   3000 wit - -
seq-mthreaded/rekh_ctm_true-unreach-call.3.c timeout 900   860   3000 wit - -
seq-mthreaded/rekh_ctm_true-unreach-call.4.c timeout 900   840   4600 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.1.M1.c timeout 900   390   4400 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.1.M4.c timeout 900   420   2700 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.2.M1.c timeout 900   450   6200 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.2.M4.c timeout 900   420   3000 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.3.M1.c timeout 900   400   4300 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.3.M4.c timeout 900   430   3000 wit - -
seq-pthread/cs_fib_false-unreach-call.i unknown 61   30   850 wit - -
seq-pthread/cs_fib_longer_false-unreach-call.i unknown 37   11   850 wit - -
seq-pthread/cs_lazy_false-unreach-call.i witness unconfirmed 53   21   860 wit true 12   6.5 430 error 58 41   760
seq-pthread/cs_queue_false-unreach-call.i timeout 900   840   2200 wit - -
seq-pthread/cs_read_write_lock_false-unreach-call.i witness unconfirmed 87   44   960 wit true 12   6.5 460 error 11 6.0 320
seq-pthread/cs_stack_false-unreach-call.i unknown 140   110   920 wit - -
seq-pthread/cs_stateful_false-unreach-call.i witness timeout 38   15   800 wit timeout 90   66   2100 true 33 20   550
seq-pthread/cs_dekker_true-unreach-call.i unknown 70   17   1400 wit - -
seq-pthread/cs_fib_longer_true-unreach-call.i timeout 900   370   6300 wit - -
seq-pthread/cs_fib_true-unreach-call.i timeout 900   370   6100 wit - -
seq-pthread/cs_lamport_true-unreach-call.i unknown 91   23   1700 wit - -
seq-pthread/cs_peterson_true-unreach-call.i unknown 69   15   1500 wit - -
seq-pthread/cs_queue_true-unreach-call.i timeout 900   380   6300 wit - -
seq-pthread/cs_read_write_lock_true-unreach-call.i unknown 140   62   2900 wit - -
seq-pthread/cs_stack_true-unreach-call.i timeout 900   370   6300 wit - -
seq-pthread/cs_stateful_true-unreach-call.i unknown 77   24   1500 wit - -
seq-pthread/cs_sync_true-unreach-call.i timeout 900   370   7200 wit - -
seq-pthread/cs_szymanski_true-unreach-call.i timeout 900   370   7100 wit - -
seq-pthread/cs_time_var_mutex_true-unreach-call.i unknown 85   22   1700 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 110000 58000 810000 261 2900   1500   93000   261 6400   4100   100000  
    correct results 125 9000 3500 180000 109 2700   1500   89000   71 6300   4000   99000  
        correct true 16 1500 540 31000 0 0   0   0   23 0   0   0  
        correct false 109 7600 3000 150000 109 2700   1500   89000   48 6300   4000   99000  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (261 tasks, max score: 364) 141
Run set sv-comp16.Sequentialized