Tool CBMC
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-03 00:42:25 CET [[ 2016-01-15 08:22:02 CET ]] [[ 2016-01-15 21:54:19 CET ]]
Run set sv-comp16.Sequentialized
Options --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cbmc.2016-01-03_0042.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cbmc.2016-01-03_0042.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) 4.6  4.6  61 wit true 24   13   810 false(reach) 87 48   1400
systemc/kundu2_false-unreach-call_false-termination.cil.c witness unconfirmed .40 .41 29 wit true 14   7.3 590 timeout 92 54   1700
systemc/pc_sfifo_1_false-unreach-call_false-termination.cil.c false(reach) .18 .19 28 wit false(reach) 6.8 3.8 270 false(reach) 14 9.4 340
systemc/pc_sfifo_2_false-unreach-call_false-termination.cil.c false(reach) .17 .18 26 wit false(reach) 9.0 4.9 370 false(reach) 21 12   480
systemc/pipeline_false-unreach-call_false-termination.cil.c witness timeout 21    21    340 wit timeout 91   60   2400 true 30 17   650
systemc/token_ring.01_false-unreach-call_false-termination.cil.c false(reach) 2.5  2.5  53 wit true 16   8.8 550 false(reach) 29 18   550
systemc/token_ring.02_false-unreach-call_false-termination.cil.c false(reach) 4.5  4.5  83 wit true 20   11   610 false(reach) 40 22   790
systemc/token_ring.03_false-unreach-call_false-termination.cil.c false(reach) 7.6  7.6  120 wit true 23   12   720 false(reach) 51 28   840
systemc/token_ring.04_false-unreach-call_false-termination.cil.c false(reach) 12    12    170 wit true 31   16   800 false(reach) 60 35   990
systemc/token_ring.05_false-unreach-call_false-termination.cil.c false(reach) 18    18    220 wit true 31   16   730 false(reach) 70 40   1300
systemc/token_ring.06_false-unreach-call_false-termination.cil.c witness unconfirmed 27    27    280 wit true 36   19   960 timeout 92 53   1500
systemc/token_ring.07_false-unreach-call_false-termination.cil.c witness timeout 36    36    350 wit timeout 91   72   1000 timeout 92 56   1700
systemc/token_ring.08_false-unreach-call_false-termination.cil.c witness unconfirmed 49    49    430 wit true 41   23   1100 timeout 91 52   1500
systemc/token_ring.09_false-unreach-call_false-termination.cil.c witness unconfirmed 65    65    510 wit true 41   23   1000 timeout 91 53   1500
systemc/token_ring.10_false-unreach-call_false-termination.cil.c witness timeout 74    74    610 wit timeout (true) 90   69   1800 timeout 91 51   1700
systemc/token_ring.11_false-unreach-call_false-termination.cil.c witness timeout 110    110    700 wit timeout 90   70   1300 timeout 92 50   1500
systemc/token_ring.12_false-unreach-call_false-termination.cil.c witness timeout 140    140    800 wit timeout 90   72   1500 timeout 92 50   1500
systemc/token_ring.13_false-unreach-call_false-termination.cil.c witness unconfirmed 170    170    940 wit true 54   34   1500 timeout 90 51   1300
systemc/token_ring.14_false-unreach-call_false-termination.cil.c witness timeout 140    140    800 wit timeout 90   73   1500 timeout 92 49   1700
systemc/token_ring.15_false-unreach-call_false-termination.cil.c witness unconfirmed 170    170    930 wit true 56   36   1400 timeout 92 50   1500
systemc/toy1_false-unreach-call_false-termination.cil.c false(reach) 5.4  5.4  58 wit true 14   7.5 550 false(reach) 75 38   940
systemc/toy2_false-unreach-call_false-termination.cil.c false(reach) 5.2  5.2  56 wit true 13   7.3 530 false(reach) 65 35   920
systemc/transmitter.01_false-unreach-call_false-termination.cil.c false(reach) .17 .18 26 wit true 8.7 4.8 330 false(reach) 24 13   410
systemc/transmitter.02_false-unreach-call_false-termination.cil.c false(reach) .17 .18 27 wit true 16   8.8 540 false(reach) 32 18   530
systemc/transmitter.03_false-unreach-call_false-termination.cil.c false(reach) .24 .26 29 wit true 20   10   550 false(reach) 41 23   670
systemc/transmitter.04_false-unreach-call_false-termination.cil.c false(reach) .26 .27 31 wit true 16   8.5 570 false(reach) 47 27   770
systemc/transmitter.05_false-unreach-call_false-termination.cil.c false(reach) .32 .33 34 wit true 26   14   830 false(reach) 64 36   1000
systemc/transmitter.06_false-unreach-call_false-termination.cil.c false(reach) .54 .55 36 wit true 34   18   840 false(reach) 72 42   1200
systemc/transmitter.07_false-unreach-call_false-termination.cil.c witness unconfirmed .68 .69 39 wit true 31   17   1000 timeout 92 52   1400
systemc/transmitter.08_false-unreach-call_false-termination.cil.c witness unconfirmed .87 .87 43 wit true 36   20   1000 timeout 92 53   1500
systemc/transmitter.09_false-unreach-call_false-termination.cil.c witness unconfirmed 1.0  1.0  48 wit true 33   19   1200 timeout 91 53   1500
systemc/transmitter.10_false-unreach-call_false-termination.cil.c witness unconfirmed 1.1  1.1  51 wit true 41   24   1400 timeout 91 53   1400
systemc/transmitter.11_false-unreach-call_false-termination.cil.c witness unconfirmed 1.5  1.5  58 wit true 47   28   1500 timeout 91 53   1500
systemc/transmitter.12_false-unreach-call_false-termination.cil.c witness unconfirmed 1.6  1.6  70 wit true 55   34   1600 timeout 91 54   1700
systemc/transmitter.13_false-unreach-call_false-termination.cil.c witness unconfirmed 2.1  2.1  77 wit true 54   34   1600 timeout 91 53   1300
systemc/transmitter.15_false-unreach-call_false-termination.cil.c false(reach) 2.0  2.0  62 wit false(reach) 12   6.5 550 false(reach) 82 50   1400
systemc/transmitter.16_false-unreach-call_false-termination.cil.c false(reach) 2.2  2.2  67 wit false(reach) 15   7.9 570 false(reach) 88 56   1400
systemc/bist_cell_true-unreach-call_false-termination.cil.c true 850    850    1700 wit - -
systemc/kundu_true-unreach-call_false-termination.cil.c true 850    850    750 wit - -
systemc/mem_slave_tlm.1_true-unreach-call_false-termination.cil.c true 850    850    1600 wit - -
systemc/mem_slave_tlm.2_true-unreach-call_false-termination.cil.c true 850    850    530 wit - -
systemc/mem_slave_tlm.3_true-unreach-call_false-termination.cil.c true 850    850    530 wit - -
systemc/mem_slave_tlm.4_true-unreach-call_false-termination.cil.c true 850    850    550 wit - -
systemc/mem_slave_tlm.5_true-unreach-call_false-termination.cil.c true 850    850    560 wit - -
systemc/pc_sfifo_1_true-unreach-call_false-termination.cil.c true 850    850    750 wit - -
systemc/pc_sfifo_2_true-unreach-call_false-termination.cil.c true 850    850    610 wit - -
systemc/pc_sfifo_3_true-unreach-call_false-termination.cil.c true 850    850    490 wit - -
systemc/pipeline_true-unreach-call_false-termination.cil.c true 850    850    430 wit - -
systemc/token_ring.01_true-unreach-call_false-termination.cil.c true 850    850    650 wit - -
systemc/token_ring.02_true-unreach-call_false-termination.cil.c true 850    850    750 wit - -
systemc/token_ring.03_true-unreach-call_false-termination.cil.c true 850    850    1200 wit - -
systemc/token_ring.04_true-unreach-call_false-termination.cil.c true 850    850    950 wit - -
systemc/token_ring.05_true-unreach-call_false-termination.cil.c true 850    850    1300 wit - -
systemc/token_ring.06_true-unreach-call_false-termination.cil.c true 850    850    1400 wit - -
systemc/token_ring.07_true-unreach-call_false-termination.cil.c true 850    850    1700 wit - -
systemc/token_ring.08_true-unreach-call_false-termination.cil.c true 850    850    520 wit - -
systemc/token_ring.09_true-unreach-call_false-termination.cil.c true 850    850    670 wit - -
systemc/token_ring.10_true-unreach-call_false-termination.cil.c true 850    850    700 wit - -
systemc/token_ring.11_true-unreach-call_false-termination.cil.c true 850    850    880 wit - -
systemc/token_ring.12_true-unreach-call_false-termination.cil.c true 850    850    980 wit - -
systemc/token_ring.13_true-unreach-call_false-termination.cil.c true 850    850    1100 wit - -
systemc/toy_true-unreach-call_false-termination.cil.c true 850    850    770 wit - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c false(reach) .28 .29 29 wit false(reach) 16   8.7 550 false(reach) 28 15   520
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) .28 .29 29 wit false(reach) 16   8.4 550 false(reach) 29 15   530
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.BOUNDED-10.pals.c false(reach) .28 .29 29 wit false(reach) 18   9.8 590 false(reach) 46 25   760
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.UNBOUNDED.pals.c false(reach) .32 .33 29 wit false(reach) 16   8.5 600 false(reach) 43 24   590
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_2.ufo.BOUNDED-10.pals.c false(reach) .28 .30 31 wit false(reach) 19   10   610 false(reach) 38 21   640
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_2.ufo.UNBOUNDED.pals.c false(reach) .31 .32 30 wit false(reach) 18   9.7 610 false(reach) 35 19   560
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.5.ufo.BOUNDED-10.pals.c false(reach) 1.3  1.3  36 wit false(reach) 28   15   900 timeout 91 50   1200
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.5.ufo.UNBOUNDED.pals.c false(reach) 1.3  1.3  37 wit false(reach) 27   15   870 timeout 92 52   1300
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.1.ufo.BOUNDED-10.pals.c false(reach) .84 .86 34 wit false(reach) 24   13   770 timeout 90 55   1600
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) .85 .86 35 wit false(reach) 24   13   740 timeout 91 55   1200
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.BOUNDED-10.pals.c false(reach) .82 .84 35 wit false(reach) 23   12   670 timeout 90 54   1300
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) .80 .82 35 wit false(reach) 19   10   580 timeout 91 57   1500
seq-mthreaded/pals_floodmax.3_false-unreach-call.1.ufo.BOUNDED-6.pals.c false(reach) .51 .52 34 wit false(reach) 18   9.5 550 timeout 91 70   980
seq-mthreaded/pals_floodmax.3_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) .50 .52 34 wit false(reach) 17   9.3 580 timeout 91 66   1100
seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.BOUNDED-6.pals.c false(reach) .15 .16 28 wit false(reach) 12   6.8 500 false(reach) 57 39   720
seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) .22 .23 30 wit false(reach) 15   8.0 510 error 48 32   690
seq-mthreaded/pals_floodmax.3_false-unreach-call.3.ufo.BOUNDED-6.pals.c false(reach) .50 .52 32 wit false(reach) 17   9.1 520 timeout 90 65   1000
seq-mthreaded/pals_floodmax.3_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(reach) .52 .53 32 wit false(reach) 16   8.8 520 timeout 91 68   1000
seq-mthreaded/pals_floodmax.3_false-unreach-call.4.ufo.BOUNDED-6.pals.c false(reach) .38 .39 32 wit false(reach) 16   8.7 560 false(reach) 82 56   990
seq-mthreaded/pals_floodmax.3_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(reach) .53 .55 31 wit false(reach) 17   8.9 530 false(reach) 75 52   1200
seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals.c witness unconfirmed 1.1  1.1  38 wit unknown 12   6.3 410 timeout 91 62   1400
seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c witness unconfirmed 1.2  1.3  38 wit unknown 12   6.7 410 timeout 91 57   1400
seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.BOUNDED-8.pals.c false(reach) 1.3  1.3  39 wit false(reach) 26   13   840 true 19 11   430
seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 1.2  1.3  39 wit false(reach) 28   15   860 true 18 9.7 430
seq-mthreaded/pals_floodmax.4_false-unreach-call.3.ufo.BOUNDED-8.pals.c false(reach) 1.2  1.2  40 wit false(reach) 23   12   870 true 19 10   410
seq-mthreaded/pals_floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(reach) 1.3  1.3  40 wit false(reach) 27   14   870 true 18 10   420
seq-mthreaded/pals_floodmax.4_false-unreach-call.4.ufo.BOUNDED-8.pals.c false(reach) 1.3  1.4  39 wit false(reach) 27   14   860 true 19 11   420
seq-mthreaded/pals_floodmax.4_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(reach) 1.4  1.4  40 wit false(reach) 27   14   840 true 17 9.5 450
seq-mthreaded/pals_floodmax.5_false-unreach-call.1.ufo.BOUNDED-10.pals.c false(reach) 8.1  8.2  73 wit false(reach) 36   19   1400 timeout 90 52   1800
seq-mthreaded/pals_floodmax.5_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 9.1  9.1  81 wit false(reach) 45   24   1100 timeout 91 51   1600
seq-mthreaded/pals_floodmax.5_false-unreach-call.2.ufo.BOUNDED-10.pals.c false(reach) 4.6  4.6  53 wit false(reach) 43   23   1100 true 25 14   500
seq-mthreaded/pals_floodmax.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 4.7  4.7  53 wit false(reach) 40   21   1000 true 26 15   520
seq-mthreaded/pals_floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals.c false(reach) 8.9  8.9  74 wit false(reach) 41   22   1400 true 24 13   490
seq-mthreaded/pals_floodmax.5_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(reach) 9.5  9.6  84 wit false(reach) 48   25   1500 true 25 15   440
seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.BOUNDED-10.pals.c witness unconfirmed 8.9  8.9  73 wit unknown 14   7.6 440 true 26 17   520
seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(reach) 10    10    82 wit false(reach) 43   23   1000 true 26 17   420
seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.1.ufo.BOUNDED-6.pals.c false(reach) .39 .41 28 wit false(reach) 14   7.8 500 false(reach) 26 14   490
seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) .35 .37 30 wit false(reach) 14   7.6 510 false(reach) 28 17   460
seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals.c false(reach) .36 .38 28 wit unknown 5.1 2.8 220 false(reach) 31 17   470
seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) .28 .30 30 wit unknown 6.2 3.4 220 false(reach) 27 15   520
seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.1.ufo.BOUNDED-8.pals.c false(reach) .92 .94 33 wit false(reach) 17   9.2 520 false(reach) 30 19   520
seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 1.0  1.0  35 wit unknown 7.6 4.3 240 false(reach) 64 48   690
seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.2.ufo.BOUNDED-8.pals.c false(reach) .96 .99 31 wit unknown 5.9 3.3 240 false(reach) 28 16   510
seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 1.1  1.2  34 wit unknown 6.4 3.5 220 false(reach) 34 19   520
seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.1.ufo.BOUNDED-10.pals.c false(reach) 1.2  1.3  35 wit false(reach) 22   12   680 timeout 91 69   840
seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 1.3  1.4  35 wit false(reach) 21   11   640 timeout 90 72   970
seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.BOUNDED-10.pals.c false(reach) 1.2  1.2  34 wit false(reach) 21   11   610 false(reach) 69 46   770
seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 1.3  1.3  34 wit false(reach) 21   11   600 false(reach) 31 18   540
seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.1.ufo.BOUNDED-12.pals.c false(reach) 1.4  1.4  37 wit false(reach) 26   14   860 timeout 90 70   780
seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 1.4  1.4  38 wit false(reach) 28   15   850 timeout 91 67   820
seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.2.ufo.BOUNDED-12.pals.c false(reach) 1.4  1.4  37 wit false(reach) 26   14   830 timeout 91 79   570
seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 1.3  1.3  37 wit false(reach) 28   15   860 false(reach) 65 47   730
seq-mthreaded/pals_lcr.3_false-unreach-call.1.ufo.BOUNDED-6.pals.c false(reach) .34 .35 27 wit unknown 5.8 3.2 220 false(reach) 34 19   560
seq-mthreaded/pals_lcr.3_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) .37 .39 27 wit unknown 5.4 3.0 220 false(reach) 27 16   510
seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.BOUNDED-8.pals.c false(reach) .69 .70 32 wit false(reach) 15   8.0 560 false(reach) 44 28   560
seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) .67 .69 32 wit false(reach) 15   8.1 540 false(reach) 35 21   530
seq-mthreaded/pals_lcr.5_false-unreach-call.1.ufo.BOUNDED-10.pals.c false(reach) .85 .87 33 wit false(reach) 21   11   630 timeout 91 67   970
seq-mthreaded/pals_lcr.5_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) .93 .95 35 wit false(reach) 21   11   610 timeout 90 72   770
seq-mthreaded/pals_lcr.6_false-unreach-call.1.ufo.BOUNDED-12.pals.c false(reach) .79 .81 36 wit false(reach) 23   12   840 timeout 90 71   800
seq-mthreaded/pals_lcr.6_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 1.0  1.1  37 wit false(reach) 24   13   790 timeout 91 77   580
seq-mthreaded/pals_lcr.7_false-unreach-call.1.ufo.BOUNDED-14.pals.c false(reach) 20    20    40 wit false(reach) 34   18   870 timeout 90 74   780
seq-mthreaded/pals_lcr.7_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 20    20    41 wit false(reach) 29   15   840 timeout 90 72   810
seq-mthreaded/pals_lcr.8_false-unreach-call.1.ufo.BOUNDED-16.pals.c false(reach) 13    13    43 wit false(reach) 37   19   900 timeout 91 63   1000
seq-mthreaded/pals_lcr.8_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 13    13    44 wit false(reach) 36   19   950 timeout 91 56   1600
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.1.ufo.BOUNDED-6.pals.c false(reach) .56 .58 33 wit false(reach) 17   9.0 600 false(reach) 68 42   1000
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) .53 .55 34 wit false(reach) 15   8.1 550 false(reach) 70 44   1000
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.2.ufo.BOUNDED-6.pals.c false(reach) .21 .23 28 wit false(reach) 16   8.5 520 false(reach) 80 55   930
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) .24 .25 28 wit false(reach) 16   8.6 510 error 30 18   560
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.3.ufo.BOUNDED-6.pals.c false(reach) .52 .54 32 wit false(reach) 19   10   630 error 87 62   980
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(reach) .53 .55 31 wit false(reach) 18   9.6 640 false(reach) 45 27   700
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.4.ufo.BOUNDED-6.pals.c false(reach) .59 .60 34 wit false(reach) 18   9.5 590 false(reach) 79 52   1000
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(reach) .60 .62 34 wit false(reach) 19   10   590 false(reach) 69 42   990
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals.c false(reach) 1.1  1.1  39 wit false(reach) 25   13   900 timeout 90 58   1700
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 1.4  1.4  39 wit false(reach) 27   14   900 timeout 91 57   1500
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.2.ufo.BOUNDED-8.pals.c witness unconfirmed 1.4  1.4  39 wit unknown 11   5.9 400 true 19 11   440
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c witness unconfirmed 1.4  1.4  41 wit unknown 11   5.9 370 true 19 10   430
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.3.ufo.BOUNDED-8.pals.c false(reach) 1.4  1.4  41 wit false(reach) 26   14   860 true 18 9.7 430
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(reach) 1.3  1.3  41 wit false(reach) 29   15   900 true 18 11   440
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.4.ufo.BOUNDED-8.pals.c false(reach) 1.6  1.6  41 wit false(reach) 25   13   880 true 17 9.3 420
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(reach) 1.5  1.6  40 wit false(reach) 24   13   880 true 19 10   430
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.1.ufo.BOUNDED-10.pals.c false(reach) 9.3  9.3  78 wit false(reach) 39   20   1400 timeout 91 51   1600
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 10    10    88 wit false(reach) 43   22   1500 timeout 91 54   1500
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.2.ufo.BOUNDED-10.pals.c false(reach) 5.1  5.1  58 wit false(reach) 42   22   1400 true 22 13   480
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 5.2  5.2  58 wit false(reach) 40   21   1400 true 25 15   500
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals.c false(reach) 9.9  9.9  79 wit false(reach) 39   21   1400 true 24 13   500
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.3.ufo.UNBOUNDED.pals.c witness unconfirmed 11    11    90 wit unknown 15   8.1 460 true 27 16   510
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.4.ufo.BOUNDED-10.pals.c false(reach) 11    11    82 wit false(reach) 40   21   1400 true 23 13   490
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(reach) 11    11    89 wit false(reach) 48   25   1500 true 24 14   500
seq-mthreaded/rekcba_aso_false-unreach-call.1.M1.c error 850    850    1800 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.1.M4.c error 850    850    5400 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.2.M1.c error 850    850    1900 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.2.M4.c error 850    850    5400 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.3.M1.c error 850    850    2000 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.3.M4.c error 850    850    6400 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.4.M1.c error 850    850    2000 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.4.M4.c error 850    850    6200 wit - -
seq-mthreaded/rekcba_ctm_false-unreach-call.2.c witness timeout 110    110    1000 wit timeout 91   60   2600 timeout 91 56   1900
seq-mthreaded/rekcba_ctm_false-unreach-call.3.c error 850    850    2200 wit - -
seq-mthreaded/rekcba_nxt_false-unreach-call.1.M1.c true 850    850    2000 wit - -
seq-mthreaded/rekcba_nxt_false-unreach-call.1.M4.c true 850    850    4900 wit - -
seq-mthreaded/rekcba_nxt_false-unreach-call.2.M1.c true 850    850    1900 wit - -
seq-mthreaded/rekcba_nxt_false-unreach-call.2.M4.c true 850    850    5100 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.1.M1.c error 850    850    2100 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.1.M4.c error 850    850    4600 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.2.M1.c error 850    850    2100 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.2.M4.c error 850    850    4600 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.4.M1.c error 850    850    2300 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.4.M4.c error 850    850    4900 wit - -
seq-mthreaded/rekh_ctm_false-unreach-call.2.c witness timeout 17    17    470 wit timeout 91   66   3600 error 80 53   890
seq-mthreaded/rekh_ctm_false-unreach-call.3.c witness unconfirmed 36    36    690 wit unknown 29   15   980 error 65 38   830
seq-mthreaded/rekh_nxt_false-unreach-call.1.M1.c true 850    850    1900 wit - -
seq-mthreaded/rekh_nxt_false-unreach-call.1.M4.c true 850    850    4500 wit - -
seq-mthreaded/rekh_nxt_false-unreach-call.2.M1.c true 850    850    2000 wit - -
seq-mthreaded/rekh_nxt_false-unreach-call.2.M4.c true 850    850    4500 wit - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_true-unreach-call.ufo.BOUNDED-10.pals.c true 12    12    55 wit - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_true-unreach-call.ufo.UNBOUNDED.pals.c true 850    850    880 wit - -
seq-mthreaded/pals_STARTPALS_Triplicated_true-unreach-call.ufo.BOUNDED-10.pals.c true 6.2  6.2  45 wit - -
seq-mthreaded/pals_STARTPALS_Triplicated_true-unreach-call.ufo.UNBOUNDED.pals.c true 850    850    880 wit - -
seq-mthreaded/pals_floodmax.3_true-unreach-call.ufo.BOUNDED-6.pals.c true 3.6  3.6  33 wit - -
seq-mthreaded/pals_floodmax.3_true-unreach-call.ufo.UNBOUNDED.pals.c false(reach) 290    290    1200 wit - -
seq-mthreaded/pals_floodmax.4_true-unreach-call.ufo.BOUNDED-8.pals.c true 690    690    54 wit - -
seq-mthreaded/pals_floodmax.4_true-unreach-call.ufo.UNBOUNDED.pals.c true 850    850    820 wit - -
seq-mthreaded/pals_floodmax.5_true-unreach-call.ufo.BOUNDED-10.pals.c true 850    850    160 wit - -
seq-mthreaded/pals_floodmax.5_true-unreach-call.ufo.UNBOUNDED.pals.c true 850    850    160 wit - -
seq-mthreaded/pals_lcr-var-start-time.3_true-unreach-call.ufo.BOUNDED-6.pals.c true 3.4  3.4  30 wit - -
seq-mthreaded/pals_lcr-var-start-time.3_true-unreach-call.ufo.UNBOUNDED.pals.c true 520    520    800 wit - -
seq-mthreaded/pals_lcr-var-start-time.4_true-unreach-call.ufo.BOUNDED-8.pals.c true 30    30    33 wit - -
seq-mthreaded/pals_lcr-var-start-time.4_true-unreach-call.ufo.UNBOUNDED.pals.c true 850    850    790 wit - -
seq-mthreaded/pals_lcr-var-start-time.5_true-unreach-call.ufo.BOUNDED-10.pals.c true 410    410    47 wit - -
seq-mthreaded/pals_lcr-var-start-time.5_true-unreach-call.ufo.UNBOUNDED.pals.c true 850    850    470 wit - -
seq-mthreaded/pals_lcr-var-start-time.6_true-unreach-call.ufo.BOUNDED-12.pals.c true 850    850    75 wit - -
seq-mthreaded/pals_lcr-var-start-time.6_true-unreach-call.ufo.UNBOUNDED.pals.c true 850    850    88 wit - -
seq-mthreaded/pals_lcr.3_true-unreach-call.ufo.BOUNDED-6.pals.c true 1.9  2.0  28 wit - -
seq-mthreaded/pals_lcr.3_true-unreach-call.ufo.UNBOUNDED.pals.c false(reach) 130    130    580 wit - -
seq-mthreaded/pals_lcr.4_true-unreach-call.ufo.BOUNDED-8.pals.c true 6.7  6.7  32 wit - -
seq-mthreaded/pals_lcr.4_true-unreach-call.ufo.UNBOUNDED.pals.c false(reach) 210    210    710 wit - -
seq-mthreaded/pals_lcr.5_true-unreach-call.ufo.BOUNDED-10.pals.c true 43    43    34 wit - -
seq-mthreaded/pals_lcr.5_true-unreach-call.ufo.UNBOUNDED.pals.c false(reach) 700    700    980 wit - -
seq-mthreaded/pals_lcr.6_true-unreach-call.ufo.BOUNDED-12.pals.c true 210    210    42 wit - -
seq-mthreaded/pals_lcr.6_true-unreach-call.ufo.UNBOUNDED.pals.c true 850    850    810 wit - -
seq-mthreaded/pals_lcr.7_true-unreach-call.ufo.BOUNDED-14.pals.c true 650    650    56 wit - -
seq-mthreaded/pals_lcr.7_true-unreach-call.ufo.UNBOUNDED.pals.c true 850    850    330 wit - -
seq-mthreaded/pals_lcr.8_true-unreach-call.ufo.BOUNDED-16.pals.c true 850    850    82 wit - -
seq-mthreaded/pals_lcr.8_true-unreach-call.ufo.UNBOUNDED.pals.c true 850    850    160 wit - -
seq-mthreaded/pals_opt-floodmax.3_true-unreach-call.ufo.BOUNDED-6.pals.c true 3.7  3.8  33 wit - -
seq-mthreaded/pals_opt-floodmax.3_true-unreach-call.ufo.UNBOUNDED.pals.c false(reach) 300    300    1300 wit - -
seq-mthreaded/pals_opt-floodmax.4_true-unreach-call.ufo.BOUNDED-8.pals.c true 360    360    52 wit - -
seq-mthreaded/pals_opt-floodmax.4_true-unreach-call.ufo.UNBOUNDED.pals.c true 850    850    900 wit - -
seq-mthreaded/pals_opt-floodmax.5_true-unreach-call.ufo.BOUNDED-10.pals.c true 850    850    150 wit - -
seq-mthreaded/pals_opt-floodmax.5_true-unreach-call.ufo.UNBOUNDED.pals.c true 850    850    170 wit - -
seq-mthreaded/rekcba_aso_true-unreach-call.1.M1.c true 110    110    1200 wit - -
seq-mthreaded/rekcba_aso_true-unreach-call.1.M4.c error 850    850    5400 wit - -
seq-mthreaded/rekcba_aso_true-unreach-call.2.M1.c error 850    850    1800 wit - -
seq-mthreaded/rekcba_aso_true-unreach-call.2.M4.c error 850    850    6200 wit - -
seq-mthreaded/rekcba_ctm_true-unreach-call.1.c error 850    850    1400 wit - -
seq-mthreaded/rekcba_ctm_true-unreach-call.2.c true 850    850    1500 wit - -
seq-mthreaded/rekcba_ctm_true-unreach-call.3.c error 850    850    2200 wit - -
seq-mthreaded/rekcba_ctm_true-unreach-call.4.c error 850    850    3600 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.1.M1.c true 92    92    1100 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.1.M4.c true 850    850    4900 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.2.M1.c true 95    95    1100 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.2.M4.c true 850    850    5100 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.3.M1.c true 98    98    1200 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.3.M4.c true 850    850    5100 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.1.M1.c true 110    110    1200 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.1.M4.c true 630    630    4600 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.2.M1.c error 850    850    2200 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.2.M4.c error 850    850    4900 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.3.M1.c error 850    850    2200 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.3.M4.c error 850    850    5000 wit - -
seq-mthreaded/rekh_ctm_true-unreach-call.1.c true 140    140    480 wit - -
seq-mthreaded/rekh_ctm_true-unreach-call.2.c true 140    140    480 wit - -
seq-mthreaded/rekh_ctm_true-unreach-call.3.c true 300    300    710 wit - -
seq-mthreaded/rekh_ctm_true-unreach-call.4.c true 560    560    950 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.1.M1.c true 91    91    1100 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.1.M4.c true 460    460    4500 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.2.M1.c true 120    120    1100 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.2.M4.c true 680    680    4500 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.3.M1.c true 100    100    1100 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.3.M4.c true 580    580    4500 wit - -
seq-pthread/cs_fib_false-unreach-call.i witness unconfirmed 3.5  3.5  73 wit true 12   6.2 440 error 11 6.2 320
seq-pthread/cs_fib_longer_false-unreach-call.i witness unconfirmed 15    15    110 wit true 11   5.9 440 error 11 6.1 320
seq-pthread/cs_lazy_false-unreach-call.i witness unconfirmed .61 .62 40 wit true 9.4 5.1 320 timeout 91 60   1300
seq-pthread/cs_queue_false-unreach-call.i witness unconfirmed 68    68    650 wit true 15   7.8 590 error 53 42   5700
seq-pthread/cs_read_write_lock_false-unreach-call.i witness unconfirmed 1.0  1.1  53 wit true 12   6.4 430 error 11 6.0 310
seq-pthread/cs_stack_false-unreach-call.i witness unconfirmed 1.6  1.6  77 wit true 12   6.4 460 error 11 6.3 320
seq-pthread/cs_stateful_false-unreach-call.i witness unconfirmed .57 .58 39 wit true 9.5 5.2 330 timeout 91 63   1000
seq-pthread/cs_dekker_true-unreach-call.i true 850    850    150 wit - -
seq-pthread/cs_fib_longer_true-unreach-call.i true 100    100    130 wit - -
seq-pthread/cs_fib_true-unreach-call.i true 30    30    74 wit - -
seq-pthread/cs_lamport_true-unreach-call.i true 850    850    420 wit - -
seq-pthread/cs_peterson_true-unreach-call.i true 850    850    510 wit - -
seq-pthread/cs_queue_true-unreach-call.i true 850    850    1900 wit - -
seq-pthread/cs_read_write_lock_true-unreach-call.i true 7.2  7.2  53 wit - -
seq-pthread/cs_stack_true-unreach-call.i true 39    39    170 wit - -
seq-pthread/cs_stateful_true-unreach-call.i true 4.1  4.1  40 wit - -
seq-pthread/cs_sync_true-unreach-call.i true 850    850    380 wit - -
seq-pthread/cs_szymanski_true-unreach-call.i true 850    850    350 wit - -
seq-pthread/cs_time_var_mutex_true-unreach-call.i true 5.1  5.1  43 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 82000 82000 220000 261 3700   2200   110000   261 8100   5100   130000  
    correct results 188 51000 51000 86000 93 2300   1200   73000   68 5600   3600   81000  
        correct true 88 51000 51000 81000 14 0   0   0   20 0   0   0  
        correct false 100 300 300 4600 79 2300   1200   73000   48 5600   3600   81000  
    incorrect results 13 8400 8400 32000 0 0   0   0   0 0   0   0  
        incorrect true 8 6800 6800 27000 0 0   0   0   0 0   0   0  
        incorrect false 5 1600 1600 4800 0 0   0   0   0 0   0   0  
score (261 tasks, max score: 364) -60
Run set sv-comp16.Sequentialized