Tool CPAchecker 1.4-svcomp16c
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-22-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-04 01:42:53 CET [[ 2016-01-15 08:36:34 CET ]] [[ 2016-01-15 22:02:40 CET ]]
Run set sv-comp16.Sequentialized
Options -sv-comp16--k-induction -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/cpa-kind.2016-01-04_0142.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-kind.2016-01-04_0142.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 71   20   1500 wit - -
systemc/kundu2_false-unreach-call_false-termination.cil.c false(reach) 45   8.7 960 wit false(reach) 14   7.5 500 false(reach) 36 21   550
systemc/pc_sfifo_1_false-unreach-call_false-termination.cil.c false(reach) 6.1 2.1 340 wit false(reach) 8.0 4.5 350 false(reach) 15 8.2 370
systemc/pc_sfifo_2_false-unreach-call_false-termination.cil.c false(reach) 7.5 2.6 340 wit false(reach) 8.4 4.6 380 false(reach) 23 13   500
systemc/pipeline_false-unreach-call_false-termination.cil.c timeout 900   380   7600 wit - -
systemc/token_ring.01_false-unreach-call_false-termination.cil.c false(reach) 38   7.1 960 wit false(reach) 11   6.1 420 false(reach) 28 16   510
systemc/token_ring.02_false-unreach-call_false-termination.cil.c false(reach) 46   8.3 980 wit false(reach) 14   7.3 480 false(reach) 38 22   680
systemc/token_ring.03_false-unreach-call_false-termination.cil.c false(reach) 48   8.8 1200 wit false(reach) 15   8.2 520 false(reach) 51 29   750
systemc/token_ring.04_false-unreach-call_false-termination.cil.c false(reach) 54   11   1500 wit false(reach) 17   9.0 530 false(reach) 64 36   1100
systemc/token_ring.05_false-unreach-call_false-termination.cil.c false(reach) 61   12   1400 wit false(reach) 20   11   600 false(reach) 77 44   1100
systemc/token_ring.06_false-unreach-call_false-termination.cil.c false(reach) 70   14   1400 wit false(reach) 24   13   690 false(reach) 83 48   1600
systemc/token_ring.07_false-unreach-call_false-termination.cil.c false(reach) 80   16   1800 wit false(reach) 25   13   810 timeout 92 52   1400
systemc/token_ring.08_false-unreach-call_false-termination.cil.c false(reach) 91   18   2200 wit false(reach) 29   15   850 timeout 92 53   1300
systemc/token_ring.09_false-unreach-call_false-termination.cil.c false(reach) 93   20   2400 wit false(reach) 31   17   860 timeout 92 53   1500
systemc/token_ring.10_false-unreach-call_false-termination.cil.c false(reach) 100   25   3000 wit false(reach) 39   20   950 timeout 91 53   1700
systemc/token_ring.11_false-unreach-call_false-termination.cil.c false(reach) 100   24   3100 wit false(reach) 41   21   1100 timeout 91 54   1600
systemc/token_ring.12_false-unreach-call_false-termination.cil.c false(reach) 120   31   3700 wit false(reach) 46   24   1500 timeout 90 52   1500
systemc/token_ring.13_false-unreach-call_false-termination.cil.c false(reach) 130   33   4000 wit false(reach) 49   26   1500 timeout 92 53   1600
systemc/token_ring.14_false-unreach-call_false-termination.cil.c false(reach) 120   33   4100 wit false(reach) 41   21   1500 timeout 91 53   1700
systemc/token_ring.15_false-unreach-call_false-termination.cil.c false(reach) 130   36   4200 wit false(reach) 46   25   1500 timeout 91 52   1700
systemc/toy1_false-unreach-call_false-termination.cil.c unknown 77   23   2000 wit - -
systemc/toy2_false-unreach-call_false-termination.cil.c unknown 76   22   2200 wit - -
systemc/transmitter.01_false-unreach-call_false-termination.cil.c false(reach) 18   4.1 560 wit false(reach) 9.0 5.0 390 false(reach) 27 15   540
systemc/transmitter.02_false-unreach-call_false-termination.cil.c false(reach) 24   4.9 580 wit false(reach) 11   6.2 450 false(reach) 33 19   530
systemc/transmitter.03_false-unreach-call_false-termination.cil.c false(reach) 33   6.3 850 wit false(reach) 12   6.4 500 false(reach) 45 26   690
systemc/transmitter.04_false-unreach-call_false-termination.cil.c false(reach) 41   7.9 950 wit false(reach) 15   8.1 530 false(reach) 52 29   850
systemc/transmitter.05_false-unreach-call_false-termination.cil.c false(reach) 45   8.4 970 wit false(reach) 18   9.5 590 false(reach) 63 35   1000
systemc/transmitter.06_false-unreach-call_false-termination.cil.c false(reach) 48   8.9 1200 wit false(reach) 21   11   600 false(reach) 77 45   1200
systemc/transmitter.07_false-unreach-call_false-termination.cil.c false(reach) 58   11   1500 wit false(reach) 25   13   730 timeout 92 53   1400
systemc/transmitter.08_false-unreach-call_false-termination.cil.c false(reach) 58   11   1500 wit false(reach) 23   12   830 timeout 92 53   1500
systemc/transmitter.09_false-unreach-call_false-termination.cil.c false(reach) 66   13   1700 wit false(reach) 29   15   830 timeout 91 53   1500
systemc/transmitter.10_false-unreach-call_false-termination.cil.c false(reach) 71   15   1800 wit false(reach) 34   18   850 timeout 91 52   1600
systemc/transmitter.11_false-unreach-call_false-termination.cil.c false(reach) 70   16   1900 wit false(reach) 34   18   1000 timeout 90 52   1500
systemc/transmitter.12_false-unreach-call_false-termination.cil.c false(reach) 79   19   2400 wit false(reach) 42   22   1000 timeout 91 53   1700
systemc/transmitter.13_false-unreach-call_false-termination.cil.c false(reach) 88   23   2900 wit false(reach) 46   25   1100 timeout 91 52   1700
systemc/transmitter.15_false-unreach-call_false-termination.cil.c false(reach) 17   4.2 570 wit false(reach) 16   8.4 570 false(reach) 88 52   1400
systemc/transmitter.16_false-unreach-call_false-termination.cil.c false(reach) 19   4.5 590 wit false(reach) 16   8.3 570 false(reach) 89 54   1400
systemc/bist_cell_true-unreach-call_false-termination.cil.c timeout 900   380   6400 wit - -
systemc/kundu_true-unreach-call_false-termination.cil.c timeout 900   400   5400 wit - -
systemc/mem_slave_tlm.1_true-unreach-call_false-termination.cil.c true 120   34   4000 wit - -
systemc/mem_slave_tlm.2_true-unreach-call_false-termination.cil.c true 110   30   3900 wit - -
systemc/mem_slave_tlm.3_true-unreach-call_false-termination.cil.c true 120   34   4000 wit - -
systemc/mem_slave_tlm.4_true-unreach-call_false-termination.cil.c true 170   56   4600 wit - -
systemc/mem_slave_tlm.5_true-unreach-call_false-termination.cil.c true 170   54   4400 wit - -
systemc/pc_sfifo_1_true-unreach-call_false-termination.cil.c timeout 900   370   7200 wit - -
systemc/pc_sfifo_2_true-unreach-call_false-termination.cil.c timeout 900   380   7900 wit - -
systemc/pc_sfifo_3_true-unreach-call_false-termination.cil.c true 14   3.5 540 wit - -
systemc/pipeline_true-unreach-call_false-termination.cil.c timeout 900   380   7600 wit - -
systemc/token_ring.01_true-unreach-call_false-termination.cil.c true 30   5.7 780 wit - -
systemc/token_ring.02_true-unreach-call_false-termination.cil.c true 110   31   3100 wit - -
systemc/token_ring.03_true-unreach-call_false-termination.cil.c true 460   200   4200 wit - -
systemc/token_ring.04_true-unreach-call_false-termination.cil.c timeout 900   410   4600 wit - -
systemc/token_ring.05_true-unreach-call_false-termination.cil.c timeout 900   410   5200 wit - -
systemc/token_ring.06_true-unreach-call_false-termination.cil.c timeout 900   410   5100 wit - -
systemc/token_ring.07_true-unreach-call_false-termination.cil.c timeout 900   400   5400 wit - -
systemc/token_ring.08_true-unreach-call_false-termination.cil.c timeout 900   400   5600 wit - -
systemc/token_ring.09_true-unreach-call_false-termination.cil.c timeout 900   400   5600 wit - -
systemc/token_ring.10_true-unreach-call_false-termination.cil.c timeout 900   400   6000 wit - -
systemc/token_ring.11_true-unreach-call_false-termination.cil.c timeout 900   400   6300 wit - -
systemc/token_ring.12_true-unreach-call_false-termination.cil.c timeout 900   400   6400 wit - -
systemc/token_ring.13_true-unreach-call_false-termination.cil.c timeout 900   400   6500 wit - -
systemc/toy_true-unreach-call_false-termination.cil.c timeout 900   390   7100 wit - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c false(reach) 23   7.9 640 wit false(reach) 16   8.8 570 false(reach) 28 15   520
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 23   7.9 670 wit false(reach) 16   8.7 570 false(reach) 25 13   500
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.BOUNDED-10.pals.c false(reach) 120   97   1400 wit false(reach) 19   10   630 false(reach) 36 20   550
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.UNBOUNDED.pals.c false(reach) 120   97   1600 wit false(reach) 16   8.8 610 false(reach) 35 20   560
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_2.ufo.BOUNDED-10.pals.c false(reach) 120   100   1600 wit false(reach) 20   11   610 false(reach) 33 18   560
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_2.ufo.UNBOUNDED.pals.c false(reach) 130   100   1600 wit false(reach) 19   10   630 false(reach) 30 16   530
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.5.ufo.BOUNDED-10.pals.c timeout 900   860   2500 wit - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.5.ufo.UNBOUNDED.pals.c timeout 900   860   2500 wit - -
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.1.ufo.BOUNDED-10.pals.c witness unconfirmed 530   400   4900 wit true 13   7.3 570 true 35 19   810
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.1.ufo.UNBOUNDED.pals.c timeout 900   740   5200 wit - -
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.BOUNDED-10.pals.c false(reach) 520   390   4900 wit false(reach) 34   18   950 false(reach) 77 42   1300
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.UNBOUNDED.pals.c timeout 900   710   5100 wit - -
seq-mthreaded/pals_floodmax.3_false-unreach-call.1.ufo.BOUNDED-6.pals.c false(reach) 31   6.7 880 wit false(reach) 15   8.1 560 false(reach) 38 22   690
seq-mthreaded/pals_floodmax.3_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 28   6.1 830 wit false(reach) 18   9.6 520 false(reach) 37 22   710
seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.BOUNDED-6.pals.c false(reach) 21   4.6 570 wit false(reach) 16   8.8 530 false(reach) 42 27   720
seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 20   4.4 550 wit false(reach) 16   8.5 510 false(reach) 42 27   700
seq-mthreaded/pals_floodmax.3_false-unreach-call.3.ufo.BOUNDED-6.pals.c false(reach) 31   6.8 880 wit false(reach) 17   9.3 560 timeout 91 63   1100
seq-mthreaded/pals_floodmax.3_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(reach) 31   6.7 880 wit false(reach) 17   9.0 520 error 62 42   1100
seq-mthreaded/pals_floodmax.3_false-unreach-call.4.ufo.BOUNDED-6.pals.c false(reach) 33   6.9 880 wit false(reach) 17   9.3 540 false(reach) 60 39   800
seq-mthreaded/pals_floodmax.3_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(reach) 36   7.4 900 wit false(reach) 14   7.6 530 timeout 91 67   1000
seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals.c false(reach) 69   18   1500 wit false(reach) 28   15   880 timeout 91 59   1300
seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 64   18   1400 wit false(reach) 25   13   860 timeout 91 55   1500
seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.BOUNDED-8.pals.c false(reach) 50   12   1200 wit false(reach) 24   13   790 true 21 12   510
seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 48   12   960 wit false(reach) 26   13   790 true 20 11   510
seq-mthreaded/pals_floodmax.4_false-unreach-call.3.ufo.BOUNDED-8.pals.c false(reach) 68   18   1500 wit false(reach) 30   16   870 true 21 12   510
seq-mthreaded/pals_floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(reach) 67   18   1600 wit false(reach) 25   13   870 true 22 13   390
seq-mthreaded/pals_floodmax.4_false-unreach-call.4.ufo.BOUNDED-8.pals.c false(reach) 75   21   1700 wit false(reach) 23   12   870 true 21 13   510
seq-mthreaded/pals_floodmax.4_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(reach) 72   20   1600 wit false(reach) 23   12   870 true 22 12   510
seq-mthreaded/pals_floodmax.5_false-unreach-call.1.ufo.BOUNDED-10.pals.c false(reach) 170   81   3200 wit false(reach) 36   19   1500 timeout 90 51   1900
seq-mthreaded/pals_floodmax.5_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 180   84   3500 wit false(reach) 32   17   1400 timeout 91 51   1800
seq-mthreaded/pals_floodmax.5_false-unreach-call.2.ufo.BOUNDED-10.pals.c false(reach) 130   59   2400 wit false(reach) 35   18   910 true 26 14   570
seq-mthreaded/pals_floodmax.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 130   58   2400 wit false(reach) 35   18   1400 true 27 15   560
seq-mthreaded/pals_floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals.c false(reach) 170   83   3800 wit false(reach) 35   18   1400 true 27 15   550
seq-mthreaded/pals_floodmax.5_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(reach) 170   82   3500 wit false(reach) 42   22   1400 true 26 14   540
seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.BOUNDED-10.pals.c false(reach) 190   93   4000 wit false(reach) 41   22   1500 true 27 15   560
seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(reach) 190   92   3800 wit false(reach) 42   22   1500 true 27 15   570
seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.1.ufo.BOUNDED-6.pals.c false(reach) 39   7.4 920 wit false(reach) 17   9.1 520 false(reach) 68 46   1000
seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 32   6.3 890 wit false(reach) 14   7.3 510 false(reach) 44 27   740
seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals.c false(reach) 40   7.6 910 wit false(reach) 13   7.1 520 false(reach) 28 16   520
seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 37   7.3 920 wit false(reach) 15   8.0 500 false(reach) 27 15   530
seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.1.ufo.BOUNDED-8.pals.c false(reach) 48   11   1200 wit false(reach) 17   8.9 600 false(reach) 35 21   460
seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 43   10   1300 wit false(reach) 18   9.8 570 false(reach) 68 51   740
seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.2.ufo.BOUNDED-8.pals.c false(reach) 54   14   1400 wit false(reach) 18   9.7 600 false(reach) 28 16   520
seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 48   11   1400 wit false(reach) 16   8.4 570 false(reach) 34 20   540
seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.1.ufo.BOUNDED-10.pals.c false(reach) 69   20   2100 wit false(reach) 24   12   670 false(reach) 47 29   810
seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 70   20   1900 wit false(reach) 23   12   650 false(reach) 67 47   770
seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.BOUNDED-10.pals.c false(reach) 70   20   1900 wit false(reach) 20   11   640 false(reach) 44 25   590
seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 70   20   2000 wit false(reach) 19   10   630 false(reach) 40 23   590
seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.1.ufo.BOUNDED-12.pals.c false(reach) 120   43   4000 wit false(reach) 23   12   850 timeout 91 78   660
seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 120   45   3700 wit false(reach) 26   14   840 timeout 91 77   640
seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.2.ufo.BOUNDED-12.pals.c false(reach) 120   40   2900 wit false(reach) 27   15   840 false(reach) 88 70   780
seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 130   47   4000 wit false(reach) 29   15   850 timeout 91 79   590
seq-mthreaded/pals_lcr.3_false-unreach-call.1.ufo.BOUNDED-6.pals.c false(reach) 27   5.5 780 wit false(reach) 17   8.7 510 false(reach) 35 20   530
seq-mthreaded/pals_lcr.3_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 28   5.8 760 wit false(reach) 17   8.8 510 false(reach) 28 15   520
seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.BOUNDED-8.pals.c false(reach) 40   8.7 920 wit false(reach) 18   9.8 550 false(reach) 49 33   570
seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 40   8.2 1100 wit false(reach) 18   9.7 570 false(reach) 50 34   540
seq-mthreaded/pals_lcr.5_false-unreach-call.1.ufo.BOUNDED-10.pals.c false(reach) 56   14   1400 wit false(reach) 22   11   660 timeout 91 68   990
seq-mthreaded/pals_lcr.5_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 51   13   1400 wit false(reach) 23   12   640 timeout 91 64   1100
seq-mthreaded/pals_lcr.6_false-unreach-call.1.ufo.BOUNDED-12.pals.c false(reach) 84   23   2200 wit false(reach) 29   15   840 timeout 90 76   750
seq-mthreaded/pals_lcr.6_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 74   22   2200 wit false(reach) 24   13   810 timeout 91 78   600
seq-mthreaded/pals_lcr.7_false-unreach-call.1.ufo.BOUNDED-14.pals.c false(reach) 110   39   3300 wit false(reach) 32   17   910 timeout 90 69   830
seq-mthreaded/pals_lcr.7_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 110   39   2900 wit false(reach) 35   18   920 timeout 91 63   1000
seq-mthreaded/pals_lcr.8_false-unreach-call.1.ufo.BOUNDED-16.pals.c false(reach) 170   70   4200 wit false(reach) 47   25   1000 timeout 91 61   1300
seq-mthreaded/pals_lcr.8_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 170   69   4200 wit false(reach) 46   24   990 timeout 91 68   870
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.1.ufo.BOUNDED-6.pals.c false(reach) 35   7.4 920 wit false(reach) 18   9.7 570 false(reach) 62 38   1100
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 31   6.9 880 wit false(reach) 20   11   600 false(reach) 44 26   720
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.2.ufo.BOUNDED-6.pals.c false(reach) 26   5.6 650 wit false(reach) 17   9.1 600 false(reach) 50 32   730
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 24   5.4 590 wit false(reach) 17   9.8 580 false(reach) 49 33   920
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.3.ufo.BOUNDED-6.pals.c false(reach) 31   7.2 870 wit false(reach) 20   11   610 false(reach) 48 28   730
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(reach) 34   7.4 910 wit false(reach) 21   11   640 timeout 91 65   1100
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.4.ufo.BOUNDED-6.pals.c false(reach) 40   8.6 1100 wit false(reach) 15   8.3 580 false(reach) 73 46   1000
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(reach) 42   8.7 1100 wit false(reach) 19   10   590 false(reach) 66 41   1000
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals.c false(reach) 69   21   1500 wit false(reach) 29   15   890 timeout 91 55   1400
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 70   22   1800 wit false(reach) 27   14   900 timeout 91 56   1400
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.2.ufo.BOUNDED-8.pals.c false(reach) 53   14   1200 wit false(reach) 27   14   830 true 22 12   510
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 53   14   1200 wit false(reach) 26   14   800 true 21 12   520
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.3.ufo.BOUNDED-8.pals.c false(reach) 71   21   1500 wit false(reach) 25   13   890 true 22 12   500
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(reach) 71   21   1500 wit false(reach) 28   15   890 true 23 13   520
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.4.ufo.BOUNDED-8.pals.c false(reach) 73   22   1500 wit false(reach) 24   13   900 true 22 13   530
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(reach) 91   28   2500 wit false(reach) 29   15   880 true 22 12   520
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.1.ufo.BOUNDED-10.pals.c false(reach) 190   98   3600 wit false(reach) 42   22   1400 timeout 91 52   1800
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 180   97   3800 wit false(reach) 38   20   1400 timeout 91 51   1900
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.2.ufo.BOUNDED-10.pals.c false(reach) 140   65   2400 wit false(reach) 37   19   1400 true 27 15   560
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 140   68   2800 wit false(reach) 38   20   1500 true 28 16   570
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals.c false(reach) 200   100   3800 wit false(reach) 47   24   1500 true 28 15   560
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(reach) 200   100   3500 wit false(reach) 34   18   1500 true 27 16   560
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.4.ufo.BOUNDED-10.pals.c false(reach) 280   150   4300 wit false(reach) 42   22   1500 true 28 16   560
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(reach) 200   100   3700 wit false(reach) 35   19   1500 true 29 16   590
seq-mthreaded/rekcba_aso_false-unreach-call.1.M1.c segmentation fault 83   18   3000 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.1.M4.c segmentation fault 290   81   8300 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.2.M1.c segmentation fault 84   19   3400 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.2.M4.c segmentation fault 270   81   8600 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.3.M1.c segmentation fault 120   31   6300 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.3.M4.c out of memory 490   140   15000 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.4.M1.c segmentation fault 120   30   6400 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.4.M4.c out of memory 500   140   15000 wit - -
seq-mthreaded/rekcba_ctm_false-unreach-call.2.c out of memory 130   110   15000 wit - -
seq-mthreaded/rekcba_ctm_false-unreach-call.3.c out of memory 150   120   15000 wit - -
seq-mthreaded/rekcba_nxt_false-unreach-call.1.M1.c segmentation fault 63   13   2200 wit - -
seq-mthreaded/rekcba_nxt_false-unreach-call.1.M4.c segmentation fault 210   57   6600 wit - -
seq-mthreaded/rekcba_nxt_false-unreach-call.2.M1.c segmentation fault 82   17   3000 wit - -
seq-mthreaded/rekcba_nxt_false-unreach-call.2.M4.c segmentation fault 250   71   8100 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.1.M1.c segmentation fault 74   17   3600 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.1.M4.c segmentation fault 160   55   5000 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.2.M1.c segmentation fault 69   17   3200 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.2.M4.c segmentation fault 150   53   4900 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.4.M1.c segmentation fault 110   30   6000 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.4.M4.c segmentation fault 220   84   6500 wit - -
seq-mthreaded/rekh_ctm_false-unreach-call.2.c timeout 900   880   6700 wit - -
seq-mthreaded/rekh_ctm_false-unreach-call.3.c timeout 900   880   9900 wit - -
seq-mthreaded/rekh_nxt_false-unreach-call.1.M1.c segmentation fault 68   14   3000 wit - -
seq-mthreaded/rekh_nxt_false-unreach-call.1.M4.c segmentation fault 140   43   4900 wit - -
seq-mthreaded/rekh_nxt_false-unreach-call.2.M1.c segmentation fault 77   16   2900 wit - -
seq-mthreaded/rekh_nxt_false-unreach-call.2.M4.c segmentation fault 140   46   5100 wit - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_true-unreach-call.ufo.BOUNDED-10.pals.c true 76   22   2400 wit - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   410   5300 wit - -
seq-mthreaded/pals_STARTPALS_Triplicated_true-unreach-call.ufo.BOUNDED-10.pals.c true 260   100   4700 wit - -
seq-mthreaded/pals_STARTPALS_Triplicated_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   410   6300 wit - -
seq-mthreaded/pals_floodmax.3_true-unreach-call.ufo.BOUNDED-6.pals.c true 42   9.4 1200 wit - -
seq-mthreaded/pals_floodmax.3_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   420   6000 wit - -
seq-mthreaded/pals_floodmax.4_true-unreach-call.ufo.BOUNDED-8.pals.c true 810   370   4400 wit - -
seq-mthreaded/pals_floodmax.4_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   410   4900 wit - -
seq-mthreaded/pals_floodmax.5_true-unreach-call.ufo.BOUNDED-10.pals.c timeout 900   410   4600 wit - -
seq-mthreaded/pals_floodmax.5_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   410   4400 wit - -
seq-mthreaded/pals_lcr-var-start-time.3_true-unreach-call.ufo.BOUNDED-6.pals.c true 38   7.2 940 wit - -
seq-mthreaded/pals_lcr-var-start-time.3_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   420   4900 wit - -
seq-mthreaded/pals_lcr-var-start-time.4_true-unreach-call.ufo.BOUNDED-8.pals.c true 64   18   1800 wit - -
seq-mthreaded/pals_lcr-var-start-time.4_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   420   5000 wit - -
seq-mthreaded/pals_lcr-var-start-time.5_true-unreach-call.ufo.BOUNDED-10.pals.c true 240   100   4000 wit - -
seq-mthreaded/pals_lcr-var-start-time.5_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   430   4300 wit - -
seq-mthreaded/pals_lcr-var-start-time.6_true-unreach-call.ufo.BOUNDED-12.pals.c timeout 900   420   4200 wit - -
seq-mthreaded/pals_lcr-var-start-time.6_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   420   4300 wit - -
seq-mthreaded/pals_lcr.3_true-unreach-call.ufo.BOUNDED-6.pals.c true 28   5.6 850 wit - -
seq-mthreaded/pals_lcr.3_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   420   6800 wit - -
seq-mthreaded/pals_lcr.4_true-unreach-call.ufo.BOUNDED-8.pals.c true 42   9.3 1200 wit - -
seq-mthreaded/pals_lcr.4_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   420   5500 wit - -
seq-mthreaded/pals_lcr.5_true-unreach-call.ufo.BOUNDED-10.pals.c true 78   24   2300 wit - -
seq-mthreaded/pals_lcr.5_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   420   5000 wit - -
seq-mthreaded/pals_lcr.6_true-unreach-call.ufo.BOUNDED-12.pals.c true 140   54   3600 wit - -
seq-mthreaded/pals_lcr.6_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   420   4700 wit - -
seq-mthreaded/pals_lcr.7_true-unreach-call.ufo.BOUNDED-14.pals.c true 750   350   4300 wit - -
seq-mthreaded/pals_lcr.7_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   420   4500 wit - -
seq-mthreaded/pals_lcr.8_true-unreach-call.ufo.BOUNDED-16.pals.c timeout 900   420   4500 wit - -
seq-mthreaded/pals_lcr.8_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   420   4400 wit - -
seq-mthreaded/pals_opt-floodmax.3_true-unreach-call.ufo.BOUNDED-6.pals.c true 46   11   1300 wit - -
seq-mthreaded/pals_opt-floodmax.3_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   420   6100 wit - -
seq-mthreaded/pals_opt-floodmax.4_true-unreach-call.ufo.BOUNDED-8.pals.c true 790   370   4100 wit - -
seq-mthreaded/pals_opt-floodmax.4_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   420   4800 wit - -
seq-mthreaded/pals_opt-floodmax.5_true-unreach-call.ufo.BOUNDED-10.pals.c timeout 900   410   4600 wit - -
seq-mthreaded/pals_opt-floodmax.5_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   410   4400 wit - -
seq-mthreaded/rekcba_aso_true-unreach-call.1.M1.c segmentation fault 85   18   3200 wit - -
seq-mthreaded/rekcba_aso_true-unreach-call.1.M4.c segmentation fault 280   80   8300 wit - -
seq-mthreaded/rekcba_aso_true-unreach-call.2.M1.c segmentation fault 120   30   6300 wit - -
seq-mthreaded/rekcba_aso_true-unreach-call.2.M4.c out of memory 510   150   15000 wit - -
seq-mthreaded/rekcba_ctm_true-unreach-call.1.c out of memory 130   100   15000 wit - -
seq-mthreaded/rekcba_ctm_true-unreach-call.2.c out of memory 130   100   15000 wit - -
seq-mthreaded/rekcba_ctm_true-unreach-call.3.c out of memory 160   120   15000 wit - -
seq-mthreaded/rekcba_ctm_true-unreach-call.4.c out of memory 180   140   15000 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.1.M1.c segmentation fault 65   13   2000 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.1.M4.c segmentation fault 210   57   6600 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.2.M1.c segmentation fault 67   14   2200 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.2.M4.c segmentation fault 220   61   7100 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.3.M1.c segmentation fault 79   16   3100 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.3.M4.c segmentation fault 240   71   8100 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.1.M1.c segmentation fault 73   17   3200 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.1.M4.c segmentation fault 150   53   5100 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.2.M1.c segmentation fault 110   30   6000 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.2.M4.c segmentation fault 220   82   6500 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.3.M1.c segmentation fault 110   31   6400 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.3.M4.c segmentation fault 230   84   6900 wit - -
seq-mthreaded/rekh_ctm_true-unreach-call.1.c timeout 900   880   6900 wit - -
seq-mthreaded/rekh_ctm_true-unreach-call.2.c timeout 900   880   6700 wit - -
seq-mthreaded/rekh_ctm_true-unreach-call.3.c timeout 900   880   9900 wit - -
seq-mthreaded/rekh_ctm_true-unreach-call.4.c timeout 900   880   13000 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.1.M1.c segmentation fault 67   15   3100 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.1.M4.c segmentation fault 120   38   4900 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.2.M1.c segmentation fault 73   15   2800 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.2.M4.c segmentation fault 130   42   4700 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.3.M1.c segmentation fault 72   16   3100 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.3.M4.c segmentation fault 150   47   5000 wit - -
seq-pthread/cs_fib_false-unreach-call.i timeout 900   410   4600 wit - -
seq-pthread/cs_fib_longer_false-unreach-call.i timeout 900   410   4600 wit - -
seq-pthread/cs_lazy_false-unreach-call.i false(reach) 860   400   4800 wit true 9.5 5.1 330 false(reach) 39 22   510
seq-pthread/cs_queue_false-unreach-call.i timeout 900   410   5800 wit - -
seq-pthread/cs_read_write_lock_false-unreach-call.i timeout 900   410   5000 wit - -
seq-pthread/cs_stack_false-unreach-call.i unknown 590   310   4300 wit - -
seq-pthread/cs_stateful_false-unreach-call.i witness unconfirmed 450   200   4300 wit true 13   6.8 450 timeout 90 73   790
seq-pthread/cs_dekker_true-unreach-call.i timeout 900   420   4600 wit - -
seq-pthread/cs_fib_longer_true-unreach-call.i timeout 900   410   5100 wit - -
seq-pthread/cs_fib_true-unreach-call.i timeout 900   410   5100 wit - -
seq-pthread/cs_lamport_true-unreach-call.i true 900   410   4800 wit - -
seq-pthread/cs_peterson_true-unreach-call.i true 810   370   4500 wit - -
seq-pthread/cs_queue_true-unreach-call.i timeout 900   400   5900 wit - -
seq-pthread/cs_read_write_lock_true-unreach-call.i timeout 900   400   4800 wit - -
seq-pthread/cs_stack_true-unreach-call.i timeout 900   410   5200 wit - -
seq-pthread/cs_stateful_true-unreach-call.i timeout 900   410   4700 wit - -
seq-pthread/cs_sync_true-unreach-call.i timeout 900   410   5300 wit - -
seq-pthread/cs_szymanski_true-unreach-call.i timeout 910   390   6200 wit - -
seq-pthread/cs_time_var_mutex_true-unreach-call.i timeout 900   410   4800 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 83000 41000 1000000 261 3000   1600   96000   261 6800   4300   110000  
    correct results 142 17000 6800 300000 117 2900   1600   95000   78 6700   4200   110000  
        correct true 25 6400 2700 76000 1 0   0   0   24 0   0   0  
        correct false 117 10000 4100 220000 116 2900   1600   95000   54 6700   4200   110000  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (261 tasks, max score: 364) 167
Run set sv-comp16.Sequentialized