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 13:17:38 CET [[ 2016-01-15 08:48:20 CET ]] [[ 2016-01-15 22:10:37 CET ]]
Run set sv-comp16.Sequentialized
Options -sv-comp16 -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-seq.2016-01-04_1317.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-seq.2016-01-04_1317.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) 8.5 2.7 330 wit false(reach) 15   7.9 530 false(reach) 31 16   520
systemc/kundu2_false-unreach-call_false-termination.cil.c false(reach) 8.9 2.7 320 wit false(reach) 14   7.4 470 false(reach) 35 19   560
systemc/pc_sfifo_1_false-unreach-call_false-termination.cil.c false(reach) 4.5 1.9 220 wit false(reach) 8.0 4.5 360 false(reach) 15 7.9 350
systemc/pc_sfifo_2_false-unreach-call_false-termination.cil.c false(reach) 4.9 2.0 220 wit false(reach) 8.9 4.8 390 false(reach) 24 14   520
systemc/pipeline_false-unreach-call_false-termination.cil.c false(reach) 39   22   1600 wit false(reach) 38   20   910 timeout 92 53   3900
systemc/token_ring.01_false-unreach-call_false-termination.cil.c false(reach) 42   8.1 970 wit false(reach) 11   6.1 450 false(reach) 29 20   540
systemc/token_ring.02_false-unreach-call_false-termination.cil.c false(reach) 54   10   1000 wit false(reach) 13   6.9 500 false(reach) 36 20   690
systemc/token_ring.03_false-unreach-call_false-termination.cil.c false(reach) 65   14   1000 wit false(reach) 14   7.8 500 false(reach) 44 25   760
systemc/token_ring.04_false-unreach-call_false-termination.cil.c false(reach) 80   25   2500 wit false(reach) 17   9.1 550 false(reach) 64 36   1100
systemc/token_ring.05_false-unreach-call_false-termination.cil.c false(reach) 140   62   3600 wit false(reach) 21   11   610 false(reach) 76 44   1100
systemc/token_ring.06_false-unreach-call_false-termination.cil.c false(reach) 150   65   4600 wit false(reach) 24   13   690 timeout 92 52   1300
systemc/token_ring.07_false-unreach-call_false-termination.cil.c false(reach) 170   77   4500 wit false(reach) 24   13   790 timeout 91 53   1500
systemc/token_ring.08_false-unreach-call_false-termination.cil.c false(reach) 200   100   4800 wit false(reach) 29   15   830 timeout 91 53   1700
systemc/token_ring.09_false-unreach-call_false-termination.cil.c false(reach) 250   150   5000 wit false(reach) 30   16   860 timeout 92 56   1700
systemc/token_ring.10_false-unreach-call_false-termination.cil.c false(reach) 270   150   4500 wit false(reach) 37   20   910 timeout 91 54   1600
systemc/token_ring.11_false-unreach-call_false-termination.cil.c false(reach) 260   150   5100 wit false(reach) 40   21   1100 timeout 91 54   1800
systemc/token_ring.12_false-unreach-call_false-termination.cil.c false(reach) 280   150   4300 wit false(reach) 47   25   1500 timeout 92 54   1300
systemc/token_ring.13_false-unreach-call_false-termination.cil.c false(reach) 290   150   3900 wit false(reach) 49   26   1500 timeout 92 55   1900
systemc/token_ring.14_false-unreach-call_false-termination.cil.c false(reach) 320   160   4800 wit false(reach) 44   23   1000 timeout 92 54   1700
systemc/token_ring.15_false-unreach-call_false-termination.cil.c false(reach) 290   160   4100 wit false(reach) 49   27   1500 timeout 92 54   1500
systemc/toy1_false-unreach-call_false-termination.cil.c false(reach) 8.8 2.8 320 wit false(reach) 15   8.0 500 false(reach) 50 28   820
systemc/toy2_false-unreach-call_false-termination.cil.c false(reach) 9.2 2.9 320 wit false(reach) 13   6.9 500 false(reach) 48 25   810
systemc/transmitter.01_false-unreach-call_false-termination.cil.c false(reach) 6.1 2.2 240 wit false(reach) 9.6 5.2 400 false(reach) 25 14   520
systemc/transmitter.02_false-unreach-call_false-termination.cil.c false(reach) 7.3 2.5 260 wit false(reach) 12   6.3 460 false(reach) 32 18   540
systemc/transmitter.03_false-unreach-call_false-termination.cil.c false(reach) 9.4 2.9 310 wit false(reach) 13   7.1 490 false(reach) 43 24   720
systemc/transmitter.04_false-unreach-call_false-termination.cil.c false(reach) 11   3.1 400 wit false(reach) 16   8.3 510 false(reach) 46 25   810
systemc/transmitter.05_false-unreach-call_false-termination.cil.c false(reach) 16   4.5 540 wit false(reach) 18   9.4 570 false(reach) 73 42   1100
systemc/transmitter.06_false-unreach-call_false-termination.cil.c false(reach) 20   6.8 700 wit false(reach) 20   11   570 false(reach) 80 50   1200
systemc/transmitter.07_false-unreach-call_false-termination.cil.c false(reach) 29   14   1300 wit false(reach) 24   13   690 timeout 92 53   1600
systemc/transmitter.08_false-unreach-call_false-termination.cil.c false(reach) 66   46   2600 wit false(reach) 26   14   800 timeout 92 52   1500
systemc/transmitter.09_false-unreach-call_false-termination.cil.c false(reach) 220   140   4700 wit false(reach) 29   15   880 timeout 91 53   1400
systemc/transmitter.10_false-unreach-call_false-termination.cil.c false(reach) 220   140   4300 wit false(reach) 34   18   910 timeout 91 52   1700
systemc/transmitter.11_false-unreach-call_false-termination.cil.c false(reach) 220   140   3200 wit false(reach) 41   22   1100 timeout 91 53   1500
systemc/transmitter.12_false-unreach-call_false-termination.cil.c false(reach) 250   140   3200 wit false(reach) 43   23   1000 timeout 92 57   1900
systemc/transmitter.13_false-unreach-call_false-termination.cil.c false(reach) 240   150   3600 wit false(reach) 46   24   1500 timeout 90 52   1700
systemc/transmitter.15_false-unreach-call_false-termination.cil.c false(reach) 8.9 2.8 320 wit false(reach) 16   8.7 570 false(reach) 79 49   1500
systemc/transmitter.16_false-unreach-call_false-termination.cil.c false(reach) 7.5 2.4 320 wit false(reach) 16   8.6 550 false(reach) 89 54   1400
systemc/bist_cell_true-unreach-call_false-termination.cil.c true 4.1 1.7 200 wit - -
systemc/kundu_true-unreach-call_false-termination.cil.c true 14   5.5 660 wit - -
systemc/mem_slave_tlm.1_true-unreach-call_false-termination.cil.c true 5.5 2.0 220 wit - -
systemc/mem_slave_tlm.2_true-unreach-call_false-termination.cil.c true 4.9 1.8 230 wit - -
systemc/mem_slave_tlm.3_true-unreach-call_false-termination.cil.c true 5.2 1.9 240 wit - -
systemc/mem_slave_tlm.4_true-unreach-call_false-termination.cil.c true 6.5 2.3 240 wit - -
systemc/mem_slave_tlm.5_true-unreach-call_false-termination.cil.c true 7.3 2.5 260 wit - -
systemc/pc_sfifo_1_true-unreach-call_false-termination.cil.c true 310   130   4900 wit - -
systemc/pc_sfifo_2_true-unreach-call_false-termination.cil.c true 320   130   5000 wit - -
systemc/pc_sfifo_3_true-unreach-call_false-termination.cil.c true 4.8 1.9 200 wit - -
systemc/pipeline_true-unreach-call_false-termination.cil.c timeout 900   690   5500 wit - -
systemc/token_ring.01_true-unreach-call_false-termination.cil.c true 33   6.5 860 wit - -
systemc/token_ring.02_true-unreach-call_false-termination.cil.c true 120   38   3500 wit - -
systemc/token_ring.03_true-unreach-call_false-termination.cil.c true 330   140   4300 wit - -
systemc/token_ring.04_true-unreach-call_false-termination.cil.c true 400   200   4500 wit - -
systemc/token_ring.05_true-unreach-call_false-termination.cil.c true 600   390   4700 wit - -
systemc/token_ring.06_true-unreach-call_false-termination.cil.c timeout 900   680   5100 wit - -
systemc/token_ring.07_true-unreach-call_false-termination.cil.c timeout 900   680   5500 wit - -
systemc/token_ring.08_true-unreach-call_false-termination.cil.c timeout 900   670   5700 wit - -
systemc/token_ring.09_true-unreach-call_false-termination.cil.c timeout 900   670   6100 wit - -
systemc/token_ring.10_true-unreach-call_false-termination.cil.c timeout 900   670   6000 wit - -
systemc/token_ring.11_true-unreach-call_false-termination.cil.c timeout 900   650   5300 wit - -
systemc/token_ring.12_true-unreach-call_false-termination.cil.c timeout 900   670   6000 wit - -
systemc/token_ring.13_true-unreach-call_false-termination.cil.c timeout 900   660   5800 wit - -
systemc/toy_true-unreach-call_false-termination.cil.c true 520   310   5500 wit - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c false(reach) 9.6 3.0 320 wit false(reach) 17   9.4 560 false(reach) 30 16   530
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 10   3.0 320 wit false(reach) 16   8.8 580 false(reach) 25 14   500
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.BOUNDED-10.pals.c false(reach) 130   100   1700 wit false(reach) 18   9.9 620 false(reach) 35 20   550
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.UNBOUNDED.pals.c false(reach) 130   100   1600 wit false(reach) 19   9.9 590 false(reach) 33 18   580
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_2.ufo.BOUNDED-10.pals.c false(reach) 130   100   1600 wit false(reach) 20   11   650 false(reach) 28 15   560
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_2.ufo.UNBOUNDED.pals.c false(reach) 130   110   1700 wit false(reach) 20   11   640 false(reach) 31 17   520
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.5.ufo.BOUNDED-10.pals.c timeout 900   850   2400 wit - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.5.ufo.UNBOUNDED.pals.c timeout 900   850   2800 wit - -
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.1.ufo.BOUNDED-10.pals.c witness unconfirmed 540   400   5000 wit true 18   9.8 580 true 41 21   920
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.1.ufo.UNBOUNDED.pals.c timeout 900   720   5100 wit - -
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.BOUNDED-10.pals.c witness unconfirmed 530   390   4900 wit true 17   8.9 570 true 37 23   950
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.UNBOUNDED.pals.c timeout 900   740   5100 wit - -
seq-mthreaded/pals_floodmax.3_false-unreach-call.1.ufo.BOUNDED-6.pals.c false(reach) 130   80   3800 wit false(reach) 18   9.4 560 false(reach) 40 23   730
seq-mthreaded/pals_floodmax.3_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 130   79   3800 wit false(reach) 17   8.7 520 false(reach) 39 22   740
seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.BOUNDED-6.pals.c false(reach) 63   23   2500 wit false(reach) 17   9.2 550 false(reach) 44 28   720
seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 65   23   1800 wit false(reach) 17   8.7 530 false(reach) 43 30   790
seq-mthreaded/pals_floodmax.3_false-unreach-call.3.ufo.BOUNDED-6.pals.c false(reach) 140   88   3800 wit false(reach) 17   9.4 540 timeout 92 65   1300
seq-mthreaded/pals_floodmax.3_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(reach) 140   88   3900 wit false(reach) 19   10   580 error 66 45   1100
seq-mthreaded/pals_floodmax.3_false-unreach-call.4.ufo.BOUNDED-6.pals.c false(reach) 140   88   3800 wit false(reach) 19   10   590 false(reach) 55 37   750
seq-mthreaded/pals_floodmax.3_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(reach) 140   88   3800 wit false(reach) 19   10   600 timeout 91 65   1200
seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals.c false(reach) 170   100   3900 wit false(reach) 30   16   910 timeout 90 56   1400
seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 180   100   3800 wit false(reach) 26   14   850 timeout 91 57   1700
seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.BOUNDED-8.pals.c false(reach) 200   150   3700 wit false(reach) 26   14   780 true 21 14   400
seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 200   150   3800 wit false(reach) 27   14   810 true 23 15   530
seq-mthreaded/pals_floodmax.4_false-unreach-call.3.ufo.BOUNDED-8.pals.c false(reach) 220   150   3600 wit false(reach) 29   15   900 true 22 12   520
seq-mthreaded/pals_floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(reach) 220   150   3700 wit false(reach) 29   16   940 true 22 13   520
seq-mthreaded/pals_floodmax.4_false-unreach-call.4.ufo.BOUNDED-8.pals.c false(reach) 230   150   3700 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) 220   150   3700 wit false(reach) 27   14   850 true 21 12   520
seq-mthreaded/pals_floodmax.5_false-unreach-call.1.ufo.BOUNDED-10.pals.c false(reach) 310   210   4500 wit false(reach) 40   21   1400 timeout 91 53   2000
seq-mthreaded/pals_floodmax.5_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 320   210   4500 wit false(reach) 43   23   1500 timeout 92 51   1800
seq-mthreaded/pals_floodmax.5_false-unreach-call.2.ufo.BOUNDED-10.pals.c false(reach) 280   190   4000 wit false(reach) 37   19   1400 true 28 15   560
seq-mthreaded/pals_floodmax.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 280   190   4100 wit false(reach) 34   18   1400 true 28 15   570
seq-mthreaded/pals_floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals.c false(reach) 320   210   4400 wit false(reach) 42   22   1500 true 29 17   570
seq-mthreaded/pals_floodmax.5_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(reach) 320   210   4400 wit false(reach) 43   22   1500 true 27 15   550
seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.BOUNDED-10.pals.c false(reach) 340   220   4400 wit false(reach) 40   21   1500 true 29 17   560
seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(reach) 350   220   4400 wit false(reach) 43   22   1500 true 26 14   540
seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.1.ufo.BOUNDED-6.pals.c false(reach) 49   9.1 950 wit false(reach) 14   7.7 520 false(reach) 63 43   1000
seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 44   8.7 920 wit false(reach) 18   9.5 580 false(reach) 47 29   750
seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals.c false(reach) 51   9.8 920 wit false(reach) 16   8.3 510 false(reach) 29 17   540
seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 54   10   1100 wit false(reach) 16   8.6 510 false(reach) 29 16   520
seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.1.ufo.BOUNDED-8.pals.c false(reach) 74   15   1500 wit false(reach) 21   11   590 false(reach) 35 23   510
seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 72   15   1400 wit false(reach) 20   10   580 false(reach) 75 58   770
seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.2.ufo.BOUNDED-8.pals.c false(reach) 83   18   1500 wit false(reach) 19   10   600 false(reach) 30 16   530
seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 67   14   1200 wit false(reach) 19   10   580 false(reach) 34 19   570
seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.1.ufo.BOUNDED-10.pals.c false(reach) 110   35   3800 wit false(reach) 23   12   660 false(reach) 48 31   740
seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 110   34   3700 wit false(reach) 23   12   660 false(reach) 68 49   600
seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.BOUNDED-10.pals.c false(reach) 99   30   3200 wit false(reach) 23   12   630 false(reach) 42 24   580
seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 100   30   3800 wit false(reach) 23   12   640 false(reach) 41 23   600
seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.1.ufo.BOUNDED-12.pals.c false(reach) 220   130   3700 wit false(reach) 27   14   850 timeout 91 79   670
seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 230   130   3700 wit false(reach) 29   15   870 timeout 91 77   630
seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.2.ufo.BOUNDED-12.pals.c false(reach) 220   120   3800 wit false(reach) 27   14   850 timeout 92 76   840
seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 230   130   3800 wit false(reach) 28   15   840 timeout 91 80   590
seq-mthreaded/pals_lcr.3_false-unreach-call.1.ufo.BOUNDED-6.pals.c false(reach) 41   7.7 890 wit false(reach) 17   8.9 520 false(reach) 31 18   530
seq-mthreaded/pals_lcr.3_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 34   6.8 880 wit false(reach) 16   8.7 510 false(reach) 27 18   510
seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.BOUNDED-8.pals.c false(reach) 49   10   1100 wit false(reach) 18   9.8 580 false(reach) 49 32   590
seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 51   10   1000 wit false(reach) 20   10   590 false(reach) 48 33   570
seq-mthreaded/pals_lcr.5_false-unreach-call.1.ufo.BOUNDED-10.pals.c false(reach) 67   16   1500 wit false(reach) 23   12   650 timeout 91 69   930
seq-mthreaded/pals_lcr.5_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 71   17   1500 wit false(reach) 22   12   620 timeout 91 63   1100
seq-mthreaded/pals_lcr.6_false-unreach-call.1.ufo.BOUNDED-12.pals.c false(reach) 95   27   1900 wit false(reach) 27   15   840 timeout 90 75   790
seq-mthreaded/pals_lcr.6_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 87   25   2300 wit false(reach) 27   14   850 timeout 91 78   600
seq-mthreaded/pals_lcr.7_false-unreach-call.1.ufo.BOUNDED-14.pals.c false(reach) 130   45   3600 wit false(reach) 34   18   900 timeout 90 69   880
seq-mthreaded/pals_lcr.7_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 130   46   3200 wit false(reach) 35   18   900 timeout 91 65   1000
seq-mthreaded/pals_lcr.8_false-unreach-call.1.ufo.BOUNDED-16.pals.c false(reach) 200   80   4200 wit false(reach) 45   23   990 timeout 90 59   1200
seq-mthreaded/pals_lcr.8_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 200   79   4100 wit false(reach) 43   22   980 timeout 91 68   900
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.1.ufo.BOUNDED-6.pals.c false(reach) 130   80   3800 wit false(reach) 18   9.9 620 false(reach) 65 41   1100
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 130   81   3900 wit false(reach) 18   9.5 580 false(reach) 45 26   700
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.2.ufo.BOUNDED-6.pals.c false(reach) 120   58   3900 wit false(reach) 19   9.9 580 false(reach) 53 34   650
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 120   54   3900 wit false(reach) 18   9.6 570 false(reach) 57 38   690
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.3.ufo.BOUNDED-6.pals.c false(reach) 140   87   3900 wit false(reach) 18   9.5 610 false(reach) 50 29   730
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(reach) 140   88   3900 wit false(reach) 19   10   610 timeout 90 64   1100
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.4.ufo.BOUNDED-6.pals.c false(reach) 150   90   3900 wit false(reach) 19   10   620 false(reach) 70 44   1100
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(reach) 140   91   3900 wit false(reach) 19   10   600 false(reach) 69 42   990
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals.c false(reach) 170   100   3800 wit false(reach) 32   17   930 timeout 91 58   1600
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 180   110   3800 wit false(reach) 28   15   890 timeout 92 56   1300
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.2.ufo.BOUNDED-8.pals.c false(reach) 210   150   3700 wit false(reach) 27   14   800 true 21 12   520
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 210   150   3600 wit false(reach) 27   14   810 true 21 11   510
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.3.ufo.BOUNDED-8.pals.c false(reach) 230   150   3700 wit false(reach) 32   16   910 true 21 15   500
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(reach) 230   150   3400 wit false(reach) 28   15   900 true 21 15   510
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.4.ufo.BOUNDED-8.pals.c false(reach) 230   160   3800 wit false(reach) 29   15   890 true 22 13   520
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(reach) 240   160   3700 wit false(reach) 29   15   890 true 22 12   530
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.1.ufo.BOUNDED-10.pals.c false(reach) 340   230   4500 wit false(reach) 46   24   1500 timeout 90 52   1800
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 340   230   4500 wit false(reach) 42   22   1500 timeout 91 50   1800
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.2.ufo.BOUNDED-10.pals.c false(reach) 290   200   4100 wit false(reach) 38   20   1400 true 29 16   570
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 290   200   3900 wit false(reach) 42   22   1500 true 28 18   580
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals.c false(reach) 340   230   4500 wit false(reach) 49   26   1500 true 29 16   570
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(reach) 340   230   4400 wit false(reach) 42   22   1500 true 27 16   570
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.4.ufo.BOUNDED-10.pals.c false(reach) 430   270   4600 wit false(reach) 41   21   1400 true 26 15   550
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(reach) 350   230   4500 wit false(reach) 40   21   1400 true 29 16   590
seq-mthreaded/rekcba_aso_false-unreach-call.1.M1.c segmentation fault 180   90   5400 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.1.M4.c segmentation fault 390   170   8700 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.2.M1.c segmentation fault 180   90   5500 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.2.M4.c segmentation fault 390   170   8800 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.3.M1.c segmentation fault 230   110   7100 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.3.M4.c timeout 900   510   11000 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.4.M1.c segmentation fault 230   110   7000 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.4.M4.c timeout 900   550   10000 wit - -
seq-mthreaded/rekcba_ctm_false-unreach-call.2.c out of memory 260   200   15000 wit - -
seq-mthreaded/rekcba_ctm_false-unreach-call.3.c out of memory 290   220   15000 wit - -
seq-mthreaded/rekcba_nxt_false-unreach-call.1.M1.c segmentation fault 160   83   5100 wit - -
seq-mthreaded/rekcba_nxt_false-unreach-call.1.M4.c segmentation fault 320   140   6700 wit - -
seq-mthreaded/rekcba_nxt_false-unreach-call.2.M1.c segmentation fault 170   87   5400 wit - -
seq-mthreaded/rekcba_nxt_false-unreach-call.2.M4.c segmentation fault 360   160   8200 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.1.M1.c segmentation fault 14   7.7 1400 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.1.M4.c segmentation fault 17   8.6 1400 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.2.M1.c segmentation fault 16   8.6 1400 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.2.M4.c segmentation fault 16   8.3 1400 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.4.M1.c segmentation fault 26   16   2600 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.4.M4.c segmentation fault 24   15   2600 wit - -
seq-mthreaded/rekh_ctm_false-unreach-call.2.c timeout 900   850   6300 wit - -
seq-mthreaded/rekh_ctm_false-unreach-call.3.c timeout 900   850   9100 wit - -
seq-mthreaded/rekh_nxt_false-unreach-call.1.M1.c segmentation fault 180   92   5300 wit - -
seq-mthreaded/rekh_nxt_false-unreach-call.1.M4.c segmentation fault 280   140   6400 wit - -
seq-mthreaded/rekh_nxt_false-unreach-call.2.M1.c segmentation fault 16   8.0 1300 wit - -
seq-mthreaded/rekh_nxt_false-unreach-call.2.M4.c segmentation fault 16   7.8 1300 wit - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_true-unreach-call.ufo.BOUNDED-10.pals.c true 98   29   2600 wit - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_true-unreach-call.ufo.UNBOUNDED.pals.c true 350   150   4500 wit - -
seq-mthreaded/pals_STARTPALS_Triplicated_true-unreach-call.ufo.BOUNDED-10.pals.c true 240   92   4700 wit - -
seq-mthreaded/pals_STARTPALS_Triplicated_true-unreach-call.ufo.UNBOUNDED.pals.c true 350   150   4800 wit - -
seq-mthreaded/pals_floodmax.3_true-unreach-call.ufo.BOUNDED-6.pals.c true 150   91   3800 wit - -
seq-mthreaded/pals_floodmax.3_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   670   6800 wit - -
seq-mthreaded/pals_floodmax.4_true-unreach-call.ufo.BOUNDED-8.pals.c timeout 900   700   4300 wit - -
seq-mthreaded/pals_floodmax.4_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   700   3900 wit - -
seq-mthreaded/pals_floodmax.5_true-unreach-call.ufo.BOUNDED-10.pals.c timeout 900   690   4700 wit - -
seq-mthreaded/pals_floodmax.5_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   690   4900 wit - -
seq-mthreaded/pals_lcr-var-start-time.3_true-unreach-call.ufo.BOUNDED-6.pals.c true 53   9.9 930 wit - -
seq-mthreaded/pals_lcr-var-start-time.3_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   710   5200 wit - -
seq-mthreaded/pals_lcr-var-start-time.4_true-unreach-call.ufo.BOUNDED-8.pals.c true 93   23   2800 wit - -
seq-mthreaded/pals_lcr-var-start-time.4_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   710   4300 wit - -
seq-mthreaded/pals_lcr-var-start-time.5_true-unreach-call.ufo.BOUNDED-10.pals.c true 270   110   4000 wit - -
seq-mthreaded/pals_lcr-var-start-time.5_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   710   4100 wit - -
seq-mthreaded/pals_lcr-var-start-time.6_true-unreach-call.ufo.BOUNDED-12.pals.c timeout 900   700   4000 wit - -
seq-mthreaded/pals_lcr-var-start-time.6_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   700   3900 wit - -
seq-mthreaded/pals_lcr.3_true-unreach-call.ufo.BOUNDED-6.pals.c true 41   7.6 880 wit - -
seq-mthreaded/pals_lcr.3_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   710   4800 wit - -
seq-mthreaded/pals_lcr.4_true-unreach-call.ufo.BOUNDED-8.pals.c true 54   12   1100 wit - -
seq-mthreaded/pals_lcr.4_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   710   4800 wit - -
seq-mthreaded/pals_lcr.5_true-unreach-call.ufo.BOUNDED-10.pals.c true 91   27   1900 wit - -
seq-mthreaded/pals_lcr.5_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   710   4400 wit - -
seq-mthreaded/pals_lcr.6_true-unreach-call.ufo.BOUNDED-12.pals.c true 160   57   4000 wit - -
seq-mthreaded/pals_lcr.6_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   700   4200 wit - -
seq-mthreaded/pals_lcr.7_true-unreach-call.ufo.BOUNDED-14.pals.c timeout 900   710   4100 wit - -
seq-mthreaded/pals_lcr.7_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   710   4100 wit - -
seq-mthreaded/pals_lcr.8_true-unreach-call.ufo.BOUNDED-16.pals.c timeout 900   700   4300 wit - -
seq-mthreaded/pals_lcr.8_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   700   4200 wit - -
seq-mthreaded/pals_opt-floodmax.3_true-unreach-call.ufo.BOUNDED-6.pals.c true 160   91   3800 wit - -
seq-mthreaded/pals_opt-floodmax.3_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   690   5200 wit - -
seq-mthreaded/pals_opt-floodmax.4_true-unreach-call.ufo.BOUNDED-8.pals.c timeout 900   700   3700 wit - -
seq-mthreaded/pals_opt-floodmax.4_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   700   4300 wit - -
seq-mthreaded/pals_opt-floodmax.5_true-unreach-call.ufo.BOUNDED-10.pals.c timeout 900   690   4700 wit - -
seq-mthreaded/pals_opt-floodmax.5_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900   690   4800 wit - -
seq-mthreaded/rekcba_aso_true-unreach-call.1.M1.c segmentation fault 180   88   5500 wit - -
seq-mthreaded/rekcba_aso_true-unreach-call.1.M4.c segmentation fault 370   160   8600 wit - -
seq-mthreaded/rekcba_aso_true-unreach-call.2.M1.c segmentation fault 220   110   7000 wit - -
seq-mthreaded/rekcba_aso_true-unreach-call.2.M4.c timeout 900   500   11000 wit - -
seq-mthreaded/rekcba_ctm_true-unreach-call.1.c out of memory 270   210   15000 wit - -
seq-mthreaded/rekcba_ctm_true-unreach-call.2.c out of memory 270   210   15000 wit - -
seq-mthreaded/rekcba_ctm_true-unreach-call.3.c out of memory 280   210   15000 wit - -
seq-mthreaded/rekcba_ctm_true-unreach-call.4.c out of memory 320   240   15000 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.1.M1.c segmentation fault 170   84   5100 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.1.M4.c segmentation fault 310   130   6700 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.2.M1.c segmentation fault 170   82   5200 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.2.M4.c segmentation fault 330   140   7200 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.3.M1.c segmentation fault 180   87   5400 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.3.M4.c segmentation fault 360   160   8300 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.1.M1.c segmentation fault 14   7.6 1400 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.1.M4.c segmentation fault 17   8.6 1400 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.2.M1.c segmentation fault 26   15   2600 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.2.M4.c segmentation fault 24   15   2600 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.3.M1.c segmentation fault 27   17   3100 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.3.M4.c segmentation fault 25   17   3100 wit - -
seq-mthreaded/rekh_ctm_true-unreach-call.1.c timeout 900   860   6500 wit - -
seq-mthreaded/rekh_ctm_true-unreach-call.2.c timeout 900   860   6400 wit - -
seq-mthreaded/rekh_ctm_true-unreach-call.3.c timeout 900   860   8900 wit - -
seq-mthreaded/rekh_ctm_true-unreach-call.4.c timeout 900   850   13000 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.1.M1.c segmentation fault 170   92   5200 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.1.M4.c segmentation fault 280   150   6400 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.2.M1.c segmentation fault 76   22   2200 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.2.M4.c segmentation fault 140   50   4700 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.3.M1.c segmentation fault 16   8.0 1300 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.3.M4.c segmentation fault 16   8.1 1300 wit - -
seq-pthread/cs_fib_false-unreach-call.i timeout 900   690   4500 wit - -
seq-pthread/cs_fib_longer_false-unreach-call.i timeout 900   700   4400 wit - -
seq-pthread/cs_lazy_false-unreach-call.i timeout 900   700   4700 wit - -
seq-pthread/cs_queue_false-unreach-call.i timeout 900   690   6100 wit - -
seq-pthread/cs_read_write_lock_false-unreach-call.i timeout 900   700   5100 wit - -
seq-pthread/cs_stack_false-unreach-call.i timeout 900   690   4300 wit - -
seq-pthread/cs_stateful_false-unreach-call.i timeout 900   710   4400 wit - -
seq-pthread/cs_dekker_true-unreach-call.i timeout 900   710   4600 wit - -
seq-pthread/cs_fib_longer_true-unreach-call.i timeout 900   700   6400 wit - -
seq-pthread/cs_fib_true-unreach-call.i timeout 900   700   5700 wit - -
seq-pthread/cs_lamport_true-unreach-call.i timeout 900   710   4600 wit - -
seq-pthread/cs_peterson_true-unreach-call.i timeout 900   710   4500 wit - -
seq-pthread/cs_queue_true-unreach-call.i timeout 900   630   5600 wit - -
seq-pthread/cs_read_write_lock_true-unreach-call.i timeout 900   690   5100 wit - -
seq-pthread/cs_stack_true-unreach-call.i timeout 900   690   5100 wit - -
seq-pthread/cs_stateful_true-unreach-call.i timeout 900   710   4700 wit - -
seq-pthread/cs_sync_true-unreach-call.i timeout 900   700   4600 wit - -
seq-pthread/cs_szymanski_true-unreach-call.i timeout 900   700   5200 wit - -
seq-pthread/cs_time_var_mutex_true-unreach-call.i timeout 900   710   5000 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 90000 63000 1100000 261 3200   1700   99000   261 6900   4400   110000  
    correct results 148 23000 13000 420000 119 3100   1600   97000   77 6800   4300   110000  
        correct true 29 4800 2200 76000 0 0   0   0   24 0   0   0  
        correct false 119 18000 11000 340000 119 3100   1600   97000   53 6800   4300   110000  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (261 tasks, max score: 364) 177
Run set sv-comp16.Sequentialized