Tool 2LS 0.3.4
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-02 22:42:27 CET [[ 2016-01-15 08:01:51 CET ]] [[ 2016-01-15 21:37:22 CET ]]
Run set sv-comp16.Sequentialized
Options --k-induction --competition-mode --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/2ls.2016-01-02_2242.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/2ls.2016-01-02_2242.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 witness unconfirmed 8.1  8.1  120 wit true 11   5.8 370 true 21   11   490
systemc/kundu2_false-unreach-call_false-termination.cil.c witness unconfirmed 27    27    200 wit true 13   7.0 440 true 29   17   540
systemc/pc_sfifo_1_false-unreach-call_false-termination.cil.c false(reach) .26 .27 33 wit timeout 91   72   4300 false(reach) 15   8.6 340
systemc/pc_sfifo_2_false-unreach-call_false-termination.cil.c false(reach) .23 .24 31 wit timeout 90   73   3000 false(reach) 18   10   490
systemc/pipeline_false-unreach-call_false-termination.cil.c timeout 900    900    760 wit - -
systemc/token_ring.01_false-unreach-call_false-termination.cil.c false(reach) 72    72    380 wit false(reach) 9.4 5.2 390 false(reach) 27   15   510
systemc/token_ring.02_false-unreach-call_false-termination.cil.c false(reach) 490    490    900 wit false(reach) 12   6.6 460 false(reach) 40   22   740
systemc/token_ring.03_false-unreach-call_false-termination.cil.c timeout 900    900    1100 wit - -
systemc/token_ring.04_false-unreach-call_false-termination.cil.c timeout 900    900    1100 wit - -
systemc/token_ring.05_false-unreach-call_false-termination.cil.c timeout 900    900    1200 wit - -
systemc/token_ring.06_false-unreach-call_false-termination.cil.c timeout 900    900    870 wit - -
systemc/token_ring.07_false-unreach-call_false-termination.cil.c timeout 900    900    760 wit - -
systemc/token_ring.08_false-unreach-call_false-termination.cil.c timeout 900    900    680 wit - -
systemc/token_ring.09_false-unreach-call_false-termination.cil.c timeout 900    900    750 wit - -
systemc/token_ring.10_false-unreach-call_false-termination.cil.c timeout 900    900    810 wit - -
systemc/token_ring.11_false-unreach-call_false-termination.cil.c timeout 900    900    890 wit - -
systemc/token_ring.12_false-unreach-call_false-termination.cil.c timeout 900    900    960 wit - -
systemc/token_ring.13_false-unreach-call_false-termination.cil.c timeout 900    900    1100 wit - -
systemc/token_ring.14_false-unreach-call_false-termination.cil.c timeout 900    900    960 wit - -
systemc/token_ring.15_false-unreach-call_false-termination.cil.c timeout 900    900    1100 wit - -
systemc/toy1_false-unreach-call_false-termination.cil.c witness unconfirmed 170    170    560 wit true 12   6.7 470 true 32   17   560
systemc/toy2_false-unreach-call_false-termination.cil.c witness unconfirmed 150    150    500 wit true 13   7.2 470 true 33   18   570
systemc/transmitter.01_false-unreach-call_false-termination.cil.c false(reach) 5.1  5.1  94 wit false(reach) 8.4 4.6 370 false(reach) 25   14   490
systemc/transmitter.02_false-unreach-call_false-termination.cil.c witness unconfirmed 14    14    170 wit true 28   15   910 true 26   15   500
systemc/transmitter.03_false-unreach-call_false-termination.cil.c error(signal 6) 45    45    320 wit - -
systemc/transmitter.04_false-unreach-call_false-termination.cil.c witness timeout 150    150    520 wit timeout 91   68   1500 true 34   18   750
systemc/transmitter.05_false-unreach-call_false-termination.cil.c error(signal 6) 490    490    820 wit - -
systemc/transmitter.06_false-unreach-call_false-termination.cil.c timeout 900    900    830 wit - -
systemc/transmitter.07_false-unreach-call_false-termination.cil.c timeout 900    900    780 wit - -
systemc/transmitter.08_false-unreach-call_false-termination.cil.c timeout 900    900    660 wit - -
systemc/transmitter.09_false-unreach-call_false-termination.cil.c timeout 900    900    730 wit - -
systemc/transmitter.10_false-unreach-call_false-termination.cil.c timeout 900    900    790 wit - -
systemc/transmitter.11_false-unreach-call_false-termination.cil.c timeout 900    900    860 wit - -
systemc/transmitter.12_false-unreach-call_false-termination.cil.c timeout 900    900    940 wit - -
systemc/transmitter.13_false-unreach-call_false-termination.cil.c timeout 900    900    1000 wit - -
systemc/transmitter.15_false-unreach-call_false-termination.cil.c false(reach) 2.4  2.4  350 wit false(reach) 17   8.8 570 false(reach) 80   47   1200
systemc/transmitter.16_false-unreach-call_false-termination.cil.c false(reach) 2.6  2.7  380 wit false(reach) 15   8.1 600 false(reach) 89   53   1500
systemc/bist_cell_true-unreach-call_false-termination.cil.c true 2.9  2.9  62 wit - -
systemc/kundu_true-unreach-call_false-termination.cil.c false(reach) 32    32    220 wit - -
systemc/mem_slave_tlm.1_true-unreach-call_false-termination.cil.c timeout 900    900    910 wit - -
systemc/mem_slave_tlm.2_true-unreach-call_false-termination.cil.c timeout 900    900    880 wit - -
systemc/mem_slave_tlm.3_true-unreach-call_false-termination.cil.c timeout 900    900    860 wit - -
systemc/mem_slave_tlm.4_true-unreach-call_false-termination.cil.c timeout 900    900    830 wit - -
systemc/mem_slave_tlm.5_true-unreach-call_false-termination.cil.c timeout 900    900    790 wit - -
systemc/pc_sfifo_1_true-unreach-call_false-termination.cil.c timeout 900    900    1500 wit - -
systemc/pc_sfifo_2_true-unreach-call_false-termination.cil.c false(reach) 13    13    140 wit - -
systemc/pc_sfifo_3_true-unreach-call_false-termination.cil.c timeout 900    900    1500 wit - -
systemc/pipeline_true-unreach-call_false-termination.cil.c timeout 900    900    750 wit - -
systemc/token_ring.01_true-unreach-call_false-termination.cil.c false(reach) 390    390    880 wit - -
systemc/token_ring.02_true-unreach-call_false-termination.cil.c timeout 900    900    1300 wit - -
systemc/token_ring.03_true-unreach-call_false-termination.cil.c timeout 900    900    1100 wit - -
systemc/token_ring.04_true-unreach-call_false-termination.cil.c timeout 900    900    1100 wit - -
systemc/token_ring.05_true-unreach-call_false-termination.cil.c timeout 900    900    840 wit - -
systemc/token_ring.06_true-unreach-call_false-termination.cil.c timeout 900    900    850 wit - -
systemc/token_ring.07_true-unreach-call_false-termination.cil.c timeout 900    900    750 wit - -
systemc/token_ring.08_true-unreach-call_false-termination.cil.c timeout 900    900    680 wit - -
systemc/token_ring.09_true-unreach-call_false-termination.cil.c timeout 900    900    740 wit - -
systemc/token_ring.10_true-unreach-call_false-termination.cil.c timeout 900    900    810 wit - -
systemc/token_ring.11_true-unreach-call_false-termination.cil.c timeout 900    900    890 wit - -
systemc/token_ring.12_true-unreach-call_false-termination.cil.c timeout 900    900    960 wit - -
systemc/token_ring.13_true-unreach-call_false-termination.cil.c timeout 900    900    1100 wit - -
systemc/toy_true-unreach-call_false-termination.cil.c false(reach) 190    190    530 wit - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.BOUNDED-10.pals.c false(reach) .31 .31 31 wit false(reach) 14   7.6 510 false(reach) 30   18   540
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) .30 .30 31 wit false(reach) 12   6.8 470 false(reach) 26   14   510
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.BOUNDED-10.pals.c false(reach) 2.9  2.9  100 wit false(reach) 15   8.0 520 false(reach) 43   24   740
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_1.ufo.UNBOUNDED.pals.c false(reach) 2.8  2.8  94 wit false(reach) 13   7.2 530 false(reach) 37   22   620
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_2.ufo.BOUNDED-10.pals.c false(reach) 3.3  3.3  99 wit false(reach) 15   8.2 530 false(reach) 40   23   670
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.4_2.ufo.UNBOUNDED.pals.c false(reach) 2.6  2.6  96 wit false(reach) 16   8.5 560 false(reach) 40   23   560
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.5.ufo.BOUNDED-10.pals.c false(reach) 18    18    290 wit false(reach) 21   11   770 timeout 91   53   1400
seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.5.ufo.UNBOUNDED.pals.c false(reach) 16    16    270 wit false(reach) 24   13   790 timeout 91   53   1400
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.1.ufo.BOUNDED-10.pals.c witness unconfirmed 16    16    200 wit true 59   36   2300 true 63   34   1200
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.1.ufo.UNBOUNDED.pals.c witness timeout 16    16    190 wit timeout 91   67   1600 true 58   33   1100
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.BOUNDED-10.pals.c witness unconfirmed 15    15    200 wit true 75   51   3200 true 58   31   1100
seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 16    16    190 wit false(reach) 55   34   1400 true 86   49   1200
seq-mthreaded/pals_floodmax.3_false-unreach-call.1.ufo.BOUNDED-6.pals.c false(reach) 3.2  3.2  85 wit false(reach) 12   6.7 500 true 17   9.2 350
seq-mthreaded/pals_floodmax.3_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 2.9  2.9  81 wit false(reach) 12   6.5 460 true 16   9.5 350
seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.BOUNDED-6.pals.c false(reach) 1.1  1.1  40 wit false(reach) 13   7.0 470 true 15   8.8 350
seq-mthreaded/pals_floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) .95 .95 39 wit false(reach) 12   6.3 420 true 14   7.6 350
seq-mthreaded/pals_floodmax.3_false-unreach-call.3.ufo.BOUNDED-6.pals.c false(reach) 3.3  3.3  85 wit false(reach) 13   7.1 490 true 15   8.1 360
seq-mthreaded/pals_floodmax.3_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(reach) 2.9  2.9  84 wit false(reach) 12   6.7 450 true 15   9.1 350
seq-mthreaded/pals_floodmax.3_false-unreach-call.4.ufo.BOUNDED-6.pals.c false(reach) 3.2  3.2  85 wit false(reach) 12   6.7 470 true 14   8.9 350
seq-mthreaded/pals_floodmax.3_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(reach) 2.8  2.8  87 wit false(reach) 14   7.5 480 true 17   10   360
seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals.c false(reach) 19    19    270 wit false(reach) 22   12   760 true 19   10   510
seq-mthreaded/pals_floodmax.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 16    16    250 wit false(reach) 24   13   770 true 20   15   510
seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.BOUNDED-8.pals.c false(reach) 8.3  8.3  170 wit false(reach) 21   11   680 true 21   13   520
seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 7.9  7.9  170 wit false(reach) 22   12   680 true 20   11   510
seq-mthreaded/pals_floodmax.4_false-unreach-call.3.ufo.BOUNDED-8.pals.c false(reach) 19    19    260 wit false(reach) 25   14   790 true 20   12   510
seq-mthreaded/pals_floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(reach) 17    17    250 wit false(reach) 24   13   800 true 20   12   500
seq-mthreaded/pals_floodmax.4_false-unreach-call.4.ufo.BOUNDED-8.pals.c false(reach) 19    19    260 wit false(reach) 21   11   760 true 20   11   500
seq-mthreaded/pals_floodmax.4_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(reach) 17    17    250 wit false(reach) 23   13   820 true 20   13   500
seq-mthreaded/pals_floodmax.5_false-unreach-call.1.ufo.BOUNDED-10.pals.c false(reach) 88    88    670 wit false(reach) 32   18   1000 true 25   14   560
seq-mthreaded/pals_floodmax.5_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 80    80    650 wit false(reach) 35   18   990 true 24   14   570
seq-mthreaded/pals_floodmax.5_false-unreach-call.2.ufo.BOUNDED-10.pals.c false(reach) 50    50    530 wit false(reach) 40   24   920 true 25   14   580
seq-mthreaded/pals_floodmax.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 48    48    490 wit false(reach) 31   17   870 true 25   14   550
seq-mthreaded/pals_floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals.c false(reach) 89    89    680 wit false(reach) 36   22   1000 true 24   13   560
seq-mthreaded/pals_floodmax.5_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(reach) 80    80    660 wit false(reach) 51   36   990 true 22   13   540
seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.BOUNDED-10.pals.c false(reach) 86    86    670 wit false(reach) 33   18   910 true 25   14   560
seq-mthreaded/pals_floodmax.5_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(reach) 83    83    680 wit false(reach) 36   20   990 true 26   14   570
seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.1.ufo.BOUNDED-6.pals.c witness unconfirmed 3.1  3.1  71 wit true 11   5.7 440 true 11   6.2 340
seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.1.ufo.UNBOUNDED.pals.c witness unconfirmed 2.5  2.5  67 wit true 8.3 4.6 300 true 14   9.0 330
seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.BOUNDED-6.pals.c witness unconfirmed 3.2  3.2  71 wit true 11   5.7 410 true 12   8.6 340
seq-mthreaded/pals_lcr-var-start-time.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c witness unconfirmed 2.9  2.9  69 wit true 8.4 4.6 300 true 14   8.6 340
seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.1.ufo.BOUNDED-8.pals.c witness unconfirmed 9.1  9.1  130 wit true 14   7.4 470 true 14   7.7 340
seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c witness unconfirmed 7.5  7.5  120 wit true 8.8 4.9 400 true 13   7.5 330
seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.2.ufo.BOUNDED-8.pals.c witness unconfirmed 8.2  8.2  130 wit true 13   7.2 470 true 12   6.7 330
seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c witness unconfirmed 7.9  8.0  120 wit true 9.4 5.2 310 true 13   8.7 330
seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.1.ufo.BOUNDED-10.pals.c false(reach) 18    18    220 wit false(reach) 17   8.9 540 true 15   8.9 330
seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 16    16    180 wit false(reach) 18   9.7 560 true 14   11   330
seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.BOUNDED-10.pals.c false(reach) 19    19    230 wit false(reach) 17   9.2 550 true 14   7.8 330
seq-mthreaded/pals_lcr-var-start-time.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 17    17    190 wit false(reach) 19   10   550 true 13   7.6 340
seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.1.ufo.BOUNDED-12.pals.c false(reach) 57    57    310 wit false(reach) 22   12   750 true 16   9.0 360
seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 47    47    280 wit false(reach) 20   11   750 true 15   8.1 330
seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.2.ufo.BOUNDED-12.pals.c false(reach) 53    53    300 wit false(reach) 23   12   750 true 13   7.2 340
seq-mthreaded/pals_lcr-var-start-time.6_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 57    57    290 wit false(reach) 25   13   750 true 16   9.3 360
seq-mthreaded/pals_lcr.3_false-unreach-call.1.ufo.BOUNDED-6.pals.c witness unconfirmed 3.0  3.0  71 wit true 8.9 4.9 390 true 14   7.9 350
seq-mthreaded/pals_lcr.3_false-unreach-call.1.ufo.UNBOUNDED.pals.c witness unconfirmed 2.5  2.5  68 wit true 8.1 4.5 280 true 11   6.1 340
seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.BOUNDED-8.pals.c witness unconfirmed 7.1  7.1  140 wit true 12   6.7 440 true 13   7.4 340
seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c witness unconfirmed 6.3  6.3  120 wit true 9.3 5.0 300 true 13   9.0 320
seq-mthreaded/pals_lcr.5_false-unreach-call.1.ufo.BOUNDED-10.pals.c witness unconfirmed 11    11    180 wit true 14   7.5 470 true 15   8.2 350
seq-mthreaded/pals_lcr.5_false-unreach-call.1.ufo.UNBOUNDED.pals.c witness unconfirmed 10    10    160 wit true 11   5.8 400 true 13   8.0 330
seq-mthreaded/pals_lcr.6_false-unreach-call.1.ufo.BOUNDED-12.pals.c false(reach) 17    17    240 wit false(reach) 23   12   690 true 14   7.8 330
seq-mthreaded/pals_lcr.6_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 14    14    210 wit false(reach) 21   11   670 true 13   7.4 340
seq-mthreaded/pals_lcr.7_false-unreach-call.1.ufo.BOUNDED-14.pals.c false(reach) 26    26    290 wit false(reach) 25   13   840 true 14   7.7 340
seq-mthreaded/pals_lcr.7_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 23    23    290 wit false(reach) 25   13   840 true 14   8.8 340
seq-mthreaded/pals_lcr.8_false-unreach-call.1.ufo.BOUNDED-16.pals.c false(reach) 41    41    400 wit false(reach) 30   16   860 true 14   7.8 330
seq-mthreaded/pals_lcr.8_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 45    45    390 wit false(reach) 27   14   870 true 15   8.8 330
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.1.ufo.BOUNDED-6.pals.c false(reach) 3.0  3.1  87 wit false(reach) 14   7.4 520 true 15   8.4 360
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 2.9  2.9  85 wit false(reach) 15   8.0 530 true 16   10   370
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.2.ufo.BOUNDED-6.pals.c false(reach) .90 .90 43 wit false(reach) 15   7.9 490 true 16   9.3 360
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 1.0  1.0  42 wit false(reach) 12   6.7 520 true 17   11   400
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.3.ufo.BOUNDED-6.pals.c false(reach) 3.3  3.3  87 wit false(reach) 16   8.6 550 true 17   10   370
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(reach) 2.9  2.9  83 wit false(reach) 16   8.4 530 true 17   11   360
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.4.ufo.BOUNDED-6.pals.c false(reach) 3.4  3.4  88 wit false(reach) 15   8.2 520 true 16   9.2 370
seq-mthreaded/pals_opt-floodmax.3_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(reach) 3.1  3.1  86 wit false(reach) 15   8.2 550 true 16   9.3 350
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.1.ufo.BOUNDED-8.pals.c false(reach) 18    19    260 wit false(reach) 24   13   830 true 20   11   500
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 16    16    250 wit false(reach) 24   13   800 true 18   10   510
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.2.ufo.BOUNDED-8.pals.c false(reach) 8.2  8.2  180 wit false(reach) 18   9.9 710 true 20   12   520
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 7.7  7.7  170 wit false(reach) 23   12   710 true 19   12   500
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.3.ufo.BOUNDED-8.pals.c false(reach) 18    18    260 wit false(reach) 24   13   830 true 19   11   510
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(reach) 16    16    250 wit false(reach) 25   13   820 true 21   12   530
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.4.ufo.BOUNDED-8.pals.c false(reach) 19    19    260 wit false(reach) 25   13   800 true 19   11   520
seq-mthreaded/pals_opt-floodmax.4_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(reach) 17    17    250 wit false(reach) 26   14   820 true 19   12   500
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.1.ufo.BOUNDED-10.pals.c false(reach) 84    84    670 wit false(reach) 33   18   1000 true 25   14   570
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.1.ufo.UNBOUNDED.pals.c false(reach) 78    78    650 wit false(reach) 29   16   1000 true 24   14   550
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.2.ufo.BOUNDED-10.pals.c false(reach) 49    49    510 wit false(reach) 32   18   870 true 25   14   560
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.2.ufo.UNBOUNDED.pals.c false(reach) 46    46    490 wit false(reach) 31   17   890 true 25   15   560
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.3.ufo.BOUNDED-10.pals.c false(reach) 85    85    670 wit false(reach) 51   36   990 true 22   13   540
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.3.ufo.UNBOUNDED.pals.c false(reach) 77    77    650 wit false(reach) 30   16   1000 true 25   14   560
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.4.ufo.BOUNDED-10.pals.c false(reach) 88    88    670 wit false(reach) 34   19   1000 true 24   14   550
seq-mthreaded/pals_opt-floodmax.5_false-unreach-call.4.ufo.UNBOUNDED.pals.c false(reach) 81    81    670 wit false(reach) 33   18   1000 true 24   13   550
seq-mthreaded/rekcba_aso_false-unreach-call.1.M1.c timeout 900    900    2100 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.1.M4.c timeout 900    900    8200 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.2.M1.c timeout 900    900    2100 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.2.M4.c timeout 900    900    8300 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.3.M1.c timeout 900    900    2500 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.3.M4.c timeout 900    900    11000 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.4.M1.c timeout 900    900    2500 wit - -
seq-mthreaded/rekcba_aso_false-unreach-call.4.M4.c timeout 900    900    10000 wit - -
seq-mthreaded/rekcba_ctm_false-unreach-call.2.c timeout 900    900    13000 wit - -
seq-mthreaded/rekcba_ctm_false-unreach-call.3.c killed by signal 9 59    59    15000 wit - -
seq-mthreaded/rekcba_nxt_false-unreach-call.1.M1.c timeout 900    900    1800 wit - -
seq-mthreaded/rekcba_nxt_false-unreach-call.1.M4.c timeout 900    900    6500 wit - -
seq-mthreaded/rekcba_nxt_false-unreach-call.2.M1.c timeout 900    900    2000 wit - -
seq-mthreaded/rekcba_nxt_false-unreach-call.2.M4.c timeout 900    900    7300 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.1.M1.c timeout 900    900    2900 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.1.M4.c timeout 900    900    9900 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.2.M1.c timeout 900    900    2900 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.2.M4.c timeout 900    900    10000 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.4.M1.c timeout 900    900    3900 wit - -
seq-mthreaded/rekh_aso_false-unreach-call.4.M4.c timeout 900    900    14000 wit - -
seq-mthreaded/rekh_ctm_false-unreach-call.2.c witness unconfirmed 460    460    9500 wit true 66   41   2200 true 30   18   530
seq-mthreaded/rekh_ctm_false-unreach-call.3.c timeout 900    900    15000 wit - -
seq-mthreaded/rekh_nxt_false-unreach-call.1.M1.c timeout 900    900    2200 wit - -
seq-mthreaded/rekh_nxt_false-unreach-call.1.M4.c timeout 900    900    7000 wit - -
seq-mthreaded/rekh_nxt_false-unreach-call.2.M1.c timeout 900    900    2500 wit - -
seq-mthreaded/rekh_nxt_false-unreach-call.2.M4.c timeout 900    900    8400 wit - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_true-unreach-call.ufo.BOUNDED-10.pals.c true 48    48    500 wit - -
seq-mthreaded/pals_STARTPALS_ActiveStandby_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900    900    4600 wit - -
seq-mthreaded/pals_STARTPALS_Triplicated_true-unreach-call.ufo.BOUNDED-10.pals.c true 38    38    330 wit - -
seq-mthreaded/pals_STARTPALS_Triplicated_true-unreach-call.ufo.UNBOUNDED.pals.c true 39    39    330 wit - -
seq-mthreaded/pals_floodmax.3_true-unreach-call.ufo.BOUNDED-6.pals.c true 11    11    170 wit - -
seq-mthreaded/pals_floodmax.3_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900    900    3100 wit - -
seq-mthreaded/pals_floodmax.4_true-unreach-call.ufo.BOUNDED-8.pals.c true 330    330    580 wit - -
seq-mthreaded/pals_floodmax.4_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900    900    2100 wit - -
seq-mthreaded/pals_floodmax.5_true-unreach-call.ufo.BOUNDED-10.pals.c timeout 900    900    1000 wit - -
seq-mthreaded/pals_floodmax.5_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900    900    1000 wit - -
seq-mthreaded/pals_lcr-var-start-time.3_true-unreach-call.ufo.BOUNDED-6.pals.c true 5.6  5.6  100 wit - -
seq-mthreaded/pals_lcr-var-start-time.3_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900    900    2200 wit - -
seq-mthreaded/pals_lcr-var-start-time.4_true-unreach-call.ufo.BOUNDED-8.pals.c true 16    16    170 wit - -
seq-mthreaded/pals_lcr-var-start-time.4_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900    900    510 wit - -
seq-mthreaded/pals_lcr-var-start-time.5_true-unreach-call.ufo.BOUNDED-10.pals.c true 63    63    260 wit - -
seq-mthreaded/pals_lcr-var-start-time.5_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900    900    460 wit - -
seq-mthreaded/pals_lcr-var-start-time.6_true-unreach-call.ufo.BOUNDED-12.pals.c true 360    360    470 wit - -
seq-mthreaded/pals_lcr-var-start-time.6_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900    900    530 wit - -
seq-mthreaded/pals_lcr.3_true-unreach-call.ufo.BOUNDED-6.pals.c true 4.2  4.2  88 wit - -
seq-mthreaded/pals_lcr.3_true-unreach-call.ufo.UNBOUNDED.pals.c false(reach) 560    560    2100 wit - -
seq-mthreaded/pals_lcr.4_true-unreach-call.ufo.BOUNDED-8.pals.c true 9.4  9.4  150 wit - -
seq-mthreaded/pals_lcr.4_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900    900    1800 wit - -
seq-mthreaded/pals_lcr.5_true-unreach-call.ufo.BOUNDED-10.pals.c true 22    22    220 wit - -
seq-mthreaded/pals_lcr.5_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900    900    450 wit - -
seq-mthreaded/pals_lcr.6_true-unreach-call.ufo.BOUNDED-12.pals.c true 63    63    330 wit - -
seq-mthreaded/pals_lcr.6_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900    900    500 wit - -
seq-mthreaded/pals_lcr.7_true-unreach-call.ufo.BOUNDED-14.pals.c true 230    230    490 wit - -
seq-mthreaded/pals_lcr.7_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900    900    550 wit - -
seq-mthreaded/pals_lcr.8_true-unreach-call.ufo.BOUNDED-16.pals.c true 680    680    620 wit - -
seq-mthreaded/pals_lcr.8_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900    900    560 wit - -
seq-mthreaded/pals_opt-floodmax.3_true-unreach-call.ufo.BOUNDED-6.pals.c true 11    11    160 wit - -
seq-mthreaded/pals_opt-floodmax.3_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900    900    3300 wit - -
seq-mthreaded/pals_opt-floodmax.4_true-unreach-call.ufo.BOUNDED-8.pals.c true 380    380    570 wit - -
seq-mthreaded/pals_opt-floodmax.4_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900    900    2600 wit - -
seq-mthreaded/pals_opt-floodmax.5_true-unreach-call.ufo.BOUNDED-10.pals.c timeout 900    900    990 wit - -
seq-mthreaded/pals_opt-floodmax.5_true-unreach-call.ufo.UNBOUNDED.pals.c timeout 900    900    940 wit - -
seq-mthreaded/rekcba_aso_true-unreach-call.1.M1.c timeout 900    900    2100 wit - -
seq-mthreaded/rekcba_aso_true-unreach-call.1.M4.c timeout 900    900    8200 wit - -
seq-mthreaded/rekcba_aso_true-unreach-call.2.M1.c timeout 900    900    2500 wit - -
seq-mthreaded/rekcba_aso_true-unreach-call.2.M4.c timeout 900    900    10000 wit - -
seq-mthreaded/rekcba_ctm_true-unreach-call.1.c timeout 900    900    13000 wit - -
seq-mthreaded/rekcba_ctm_true-unreach-call.2.c timeout 900    900    13000 wit - -
seq-mthreaded/rekcba_ctm_true-unreach-call.3.c killed by signal 9 60    60    15000 wit - -
seq-mthreaded/rekcba_ctm_true-unreach-call.4.c killed by signal 9 73    73    15000 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.1.M1.c timeout 900    900    1800 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.1.M4.c timeout 900    900    6600 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.2.M1.c timeout 900    900    1900 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.2.M4.c timeout 900    900    6600 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.3.M1.c timeout 900    900    2000 wit - -
seq-mthreaded/rekcba_nxt_true-unreach-call.3.M4.c timeout 900    900    7300 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.1.M1.c true 710    710    2900 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.1.M4.c timeout 900    900    9900 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.2.M1.c timeout 900    900    3900 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.2.M4.c timeout 900    900    14000 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.3.M1.c timeout 900    900    3900 wit - -
seq-mthreaded/rekh_aso_true-unreach-call.3.M4.c timeout 900    900    14000 wit - -
seq-mthreaded/rekh_ctm_true-unreach-call.1.c true 160    160    9700 wit - -
seq-mthreaded/rekh_ctm_true-unreach-call.2.c true 310    310    9600 wit - -
seq-mthreaded/rekh_ctm_true-unreach-call.3.c killed by signal 9 73    73    15000 wit - -
seq-mthreaded/rekh_ctm_true-unreach-call.4.c killed by signal 9 62    62    15000 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.1.M1.c timeout 900    900    2100 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.1.M4.c timeout 900    900    7100 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.2.M1.c timeout 900    900    2100 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.2.M4.c timeout 900    900    7100 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.3.M1.c timeout 900    900    2500 wit - -
seq-mthreaded/rekh_nxt_true-unreach-call.3.M4.c timeout 900    900    8400 wit - -
seq-pthread/cs_fib_false-unreach-call.i witness timeout 21    21    220 wit timeout 91   69   2500 error 10   7.6 320
seq-pthread/cs_fib_longer_false-unreach-call.i witness timeout 74    74    310 wit timeout 90   65   2300 error 9.3 5.6 310
seq-pthread/cs_lazy_false-unreach-call.i witness timeout .77 .77 80 wit timeout 91   71   2100 true 18   11   370
seq-pthread/cs_queue_false-unreach-call.i witness timeout 39    39    790 wit timeout 91   68   2000 error 47   37   5600
seq-pthread/cs_read_write_lock_false-unreach-call.i witness timeout 1.3  1.3  110 wit timeout 91   72   2100 error 11   5.9 340
seq-pthread/cs_stack_false-unreach-call.i witness timeout 1.3  1.3  150 wit timeout 92   65   3200 error 10   6.6 310
seq-pthread/cs_stateful_false-unreach-call.i witness timeout .59 .59 65 wit timeout 91   67   1800 true 18   11   380
seq-pthread/cs_dekker_true-unreach-call.i timeout 900    900    6700 wit - -
seq-pthread/cs_fib_longer_true-unreach-call.i true 420    420    740 wit - -
seq-pthread/cs_fib_true-unreach-call.i true 100    100    470 wit - -
seq-pthread/cs_lamport_true-unreach-call.i timeout 900    900    2800 wit - -
seq-pthread/cs_peterson_true-unreach-call.i timeout 900    900    10000 wit - -
seq-pthread/cs_queue_true-unreach-call.i timeout 900    900    1700 wit - -
seq-pthread/cs_read_write_lock_true-unreach-call.i true 1.4  1.4  110 wit - -
seq-pthread/cs_stack_true-unreach-call.i false(reach) 150    150    820 wit - -
seq-pthread/cs_stateful_true-unreach-call.i true .65 .66 69 wit - -
seq-pthread/cs_sync_true-unreach-call.i true 10    10    280 wit - -
seq-pthread/cs_szymanski_true-unreach-call.i timeout 900    900    6900 wit - -
seq-pthread/cs_time_var_mutex_true-unreach-call.i true 1.1  1.1  86 wit - -
../../sv-benchmarks/c/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime (s) wit1_walltime (s) wit1_memUsage (MB) wit2_status wit2_cputime (s) wit2_walltime (s) wit2_memUsage (MB)
total tasks 261 110000 110000 550000 261 3100   2000   97000   261 2600   1500   60000  
    correct results 105 6600 6600 52000 76 1900   1100   62000   76 1900   1100   40000  
        correct true 27 4000 4000 30000 0 0   0   0   63 0   0   0  
        correct false 78 2600 2600 22000 76 1900   1100   62000   13 1900   1100   40000  
    incorrect results 6 1300 1300 4700 0 0   0   0   0 0   0   0  
        incorrect true 0
        incorrect false 6 1300 1300 4700 0 0   0   0   0 0   0   0  
score (261 tasks, max score: 364) 36
Run set sv-comp16.Sequentialized