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.ProductLines
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/product-lines/ 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)
elevator_spec14_product20_false-unreach-call.cil.c false(reach) 9.6  9.6  1500 wit true 15   8.0 610 false(reach) 40 22   590
elevator_spec14_product24_false-unreach-call.cil.c false(reach) 15    15    2300 wit true 14   7.4 570 false(reach) 41 24   790
elevator_spec14_product28_false-unreach-call.cil.c false(reach) 10    10    1600 wit true 13   7.2 590 false(reach) 35 19   600
elevator_spec14_product32_false-unreach-call.cil.c false(reach) 16    16    2400 wit true 14   7.7 560 false(reach) 40 27   800
elevator_spec14_productSimulator_false-unreach-call.cil.c false(reach) 54    54    7900 wit timeout 92   67   4000 false(reach) 43 24   740
elevator_spec1_product18_false-unreach-call.cil.c witness unconfirmed 770    770    1800 wit true 14   7.4 590 true 40 24   790
elevator_spec1_product20_false-unreach-call.cil.c timeout 900    900    1900 wit - -
elevator_spec1_product22_false-unreach-call.cil.c timeout 900    900    2200 wit - -
elevator_spec1_product24_false-unreach-call.cil.c timeout 900    900    2200 wit - -
elevator_spec1_product26_false-unreach-call.cil.c witness unconfirmed 780    780    1900 wit true 15   7.9 600 true 40 23   770
elevator_spec1_product28_false-unreach-call.cil.c timeout 900    900    2000 wit - -
elevator_spec1_product30_false-unreach-call.cil.c timeout 900    900    2200 wit - -
elevator_spec1_product32_false-unreach-call.cil.c timeout 900    900    2300 wit - -
elevator_spec1_productSimulator_false-unreach-call.cil.c timeout 900    900    4200 wit - -
elevator_spec2_product18_false-unreach-call.cil.c witness unconfirmed 650    650    1800 wit true 13   6.9 580 true 39 22   740
elevator_spec2_product20_false-unreach-call.cil.c witness unconfirmed 900    900    2000 wit true 15   8.1 590 true 38 21   750
elevator_spec2_product22_false-unreach-call.cil.c timeout 900    900    2200 wit - -
elevator_spec2_product24_false-unreach-call.cil.c timeout 900    900    2200 wit - -
elevator_spec2_product26_false-unreach-call.cil.c witness unconfirmed 750    750    1900 wit true 14   7.6 570 true 41 23   770
elevator_spec2_product28_false-unreach-call.cil.c timeout 900    900    2000 wit - -
elevator_spec2_product30_false-unreach-call.cil.c timeout 900    900    2300 wit - -
elevator_spec2_product32_false-unreach-call.cil.c timeout 900    900    2300 wit - -
elevator_spec2_productSimulator_false-unreach-call.cil.c timeout 900    900    4200 wit - -
elevator_spec3_product03_false-unreach-call.cil.c false(reach) 5.0  5.0  760 wit true 18   9.3 630 false(reach) 52 30   900
elevator_spec3_product11_false-unreach-call.cil.c false(reach) 5.3  5.3  800 wit true 15   7.8 610 false(reach) 51 29   880
elevator_spec3_product19_false-unreach-call.cil.c false(reach) 5.5  5.5  840 wit true 16   8.6 620 false(reach) 51 29   870
elevator_spec3_product20_false-unreach-call.cil.c false(reach) 10    10    1600 wit true 16   8.4 630 false(reach) 54 32   890
elevator_spec3_product23_false-unreach-call.cil.c false(reach) 8.4  8.4  1300 wit true 15   7.7 610 false(reach) 63 36   1200
elevator_spec3_product24_false-unreach-call.cil.c false(reach) 16    16    2400 wit true 15   8.1 660 false(reach) 56 33   1200
elevator_spec3_product27_false-unreach-call.cil.c false(reach) 5.7  5.7  890 wit true 17   9.2 610 false(reach) 60 33   980
elevator_spec3_product28_false-unreach-call.cil.c false(reach) 11    11    1700 wit true 16   8.7 610 false(reach) 49 28   910
elevator_spec3_product31_false-unreach-call.cil.c false(reach) 8.6  8.6  1300 wit true 15   7.9 660 false(reach) 69 38   1100
elevator_spec3_product32_false-unreach-call.cil.c false(reach) 16    16    2600 wit true 17   9.1 650 false(reach) 54 32   820
elevator_spec3_productSimulator_false-unreach-call.cil.c witness timeout 60    60    8500 wit timeout 91   61   3800 true 26 15   600
elevator_spec9_product26_false-unreach-call.cil.c witness unconfirmed 700    700    1900 wit true 12   6.5 570 true 42 24   780
elevator_spec9_product28_false-unreach-call.cil.c timeout 900    900    2000 wit - -
elevator_spec9_product30_false-unreach-call.cil.c timeout 900    900    2200 wit - -
elevator_spec9_product32_false-unreach-call.cil.c timeout 900    900    2300 wit - -
elevator_spec9_productSimulator_false-unreach-call.cil.c timeout 900    900    4200 wit - -
elevator_spec13_product21_true-unreach-call.cil.c error(signal 6) 7.0  7.0  1200 wit - -
elevator_spec13_product22_true-unreach-call.cil.c error(signal 6) 13    13    2300 wit - -
elevator_spec13_product23_true-unreach-call.cil.c error(signal 6) 7.5  7.5  1300 wit - -
elevator_spec13_product24_true-unreach-call.cil.c error(signal 6) 15    15    2500 wit - -
elevator_spec13_product29_true-unreach-call.cil.c error(signal 6) 7.2  7.2  1300 wit - -
elevator_spec13_product30_true-unreach-call.cil.c error(signal 6) 14    14    2400 wit - -
elevator_spec13_product31_true-unreach-call.cil.c error(signal 6) 7.7  7.7  1400 wit - -
elevator_spec13_product32_true-unreach-call.cil.c error(signal 6) 15    15    2600 wit - -
elevator_spec13_productSimulator_true-unreach-call.cil.c error(signal 6) 56    56    8500 wit - -
elevator_spec14_product03_true-unreach-call.cil.c true 750    750    1800 wit - -
elevator_spec14_product11_true-unreach-call.cil.c true 820    820    1800 wit - -
elevator_spec14_product19_true-unreach-call.cil.c timeout 900    900    1900 wit - -
elevator_spec14_product23_true-unreach-call.cil.c true 350    350    1700 wit - -
elevator_spec14_product27_true-unreach-call.cil.c timeout 900    900    1900 wit - -
elevator_spec14_product31_true-unreach-call.cil.c true 450    450    1800 wit - -
elevator_spec1_product01_true-unreach-call.cil.c timeout 900    900    1800 wit - -
elevator_spec1_product03_true-unreach-call.cil.c timeout 900    900    1700 wit - -
elevator_spec1_product09_true-unreach-call.cil.c timeout 900    900    1800 wit - -
elevator_spec1_product11_true-unreach-call.cil.c timeout 900    900    1700 wit - -
elevator_spec1_product17_true-unreach-call.cil.c timeout 900    900    1700 wit - -
elevator_spec1_product19_true-unreach-call.cil.c timeout 900    900    1700 wit - -
elevator_spec1_product21_true-unreach-call.cil.c timeout 900    900    1800 wit - -
elevator_spec1_product23_true-unreach-call.cil.c timeout 900    900    1700 wit - -
elevator_spec1_product25_true-unreach-call.cil.c timeout 900    900    1800 wit - -
elevator_spec1_product27_true-unreach-call.cil.c timeout 900    900    1700 wit - -
elevator_spec1_product29_true-unreach-call.cil.c timeout 900    900    1700 wit - -
elevator_spec1_product31_true-unreach-call.cil.c timeout 900    900    1700 wit - -
elevator_spec2_product01_true-unreach-call.cil.c timeout 900    900    1800 wit - -
elevator_spec2_product03_true-unreach-call.cil.c timeout 900    900    1700 wit - -
elevator_spec2_product09_true-unreach-call.cil.c timeout 900    900    1700 wit - -
elevator_spec2_product11_true-unreach-call.cil.c timeout 900    900    1700 wit - -
elevator_spec2_product17_true-unreach-call.cil.c timeout 900    900    1700 wit - -
elevator_spec2_product19_true-unreach-call.cil.c timeout 900    900    1800 wit - -
elevator_spec2_product21_true-unreach-call.cil.c timeout 900    900    1800 wit - -
elevator_spec2_product23_true-unreach-call.cil.c timeout 900    900    1800 wit - -
elevator_spec2_product25_true-unreach-call.cil.c timeout 900    900    1700 wit - -
elevator_spec2_product27_true-unreach-call.cil.c timeout 900    900    1800 wit - -
elevator_spec2_product29_true-unreach-call.cil.c timeout 900    900    1700 wit - -
elevator_spec2_product31_true-unreach-call.cil.c timeout 900    900    1800 wit - -
elevator_spec3_product01_true-unreach-call.cil.c true 4.6  4.6  680 wit - -
elevator_spec3_product09_true-unreach-call.cil.c true 5.0  5.0  730 wit - -
elevator_spec3_product17_true-unreach-call.cil.c true 5.1  5.1  770 wit - -
elevator_spec3_product18_true-unreach-call.cil.c true 9.7  9.7  1400 wit - -
elevator_spec3_product21_true-unreach-call.cil.c true 7.7  7.7  1200 wit - -
elevator_spec3_product22_true-unreach-call.cil.c true 15    15    2200 wit - -
elevator_spec3_product25_true-unreach-call.cil.c true 5.2  5.2  810 wit - -
elevator_spec3_product26_true-unreach-call.cil.c true 10    10    1500 wit - -
elevator_spec3_product29_true-unreach-call.cil.c true 8.0  8.0  1200 wit - -
elevator_spec3_product30_true-unreach-call.cil.c true 16    16    2300 wit - -
elevator_spec9_product09_true-unreach-call.cil.c timeout 900    900    1800 wit - -
elevator_spec9_product11_true-unreach-call.cil.c timeout 900    900    1800 wit - -
elevator_spec9_product25_true-unreach-call.cil.c timeout 900    900    1700 wit - -
elevator_spec9_product27_true-unreach-call.cil.c timeout 900    900    1800 wit - -
elevator_spec9_product29_true-unreach-call.cil.c timeout 900    900    1700 wit - -
elevator_spec9_product31_true-unreach-call.cil.c timeout 900    900    1800 wit - -
email_spec0_product16_false-unreach-call.cil.c false(reach) 180    180    610 wit true 25   13   1000 false(reach) 30 19   560
email_spec0_product21_false-unreach-call.cil.c false(reach) 350    350    1000 wit true 36   19   1400 false(reach) 30 16   590
email_spec0_product22_false-unreach-call.cil.c false(reach) 210    210    670 wit true 30   16   1000 false(reach) 28 16   560
email_spec0_product26_false-unreach-call.cil.c false(reach) 420    420    1100 wit true 37   21   1500 false(reach) 32 18   570
email_spec0_product31_false-unreach-call.cil.c false(reach) 170    170    640 wit true 31   17   890 false(reach) 32 19   540
email_spec0_product33_false-unreach-call.cil.c false(reach) 190    190    690 wit true 34   18   1200 false(reach) 34 19   570
email_spec0_product34_false-unreach-call.cil.c false(reach) 370    370    1100 wit true 39   22   1500 false(reach) 27 14   570
email_spec0_product35_false-unreach-call.cil.c false(reach) 400    400    1200 wit true 41   23   1500 false(reach) 35 20   600
email_spec0_productSimulator_false-unreach-call.cil.c killed by signal 9 700    700    15000 wit - -
email_spec11_product15_false-unreach-call.cil.c false(reach) 160    160    600 wit true 25   13   950 false(reach) 31 17   540
email_spec11_product20_false-unreach-call.cil.c false(reach) 330    330    950 wit true 35   19   1400 false(reach) 32 18   590
email_spec11_product22_false-unreach-call.cil.c false(reach) 220    220    660 wit true 32   17   1000 false(reach) 28 18   530
email_spec11_product26_false-unreach-call.cil.c false(reach) 400    400    1100 wit true 36   20   1400 false(reach) 29 18   550
email_spec11_product30_false-unreach-call.cil.c false(reach) 190    190    620 wit true 33   17   1000 false(reach) 31 17   550
email_spec11_product32_false-unreach-call.cil.c false(reach) 350    350    1000 wit true 35   19   1500 false(reach) 33 18   570
email_spec11_product33_false-unreach-call.cil.c false(reach) 200    200    720 wit true 29   15   1100 false(reach) 30 17   580
email_spec11_product35_false-unreach-call.cil.c false(reach) 430    430    1200 wit true 36   21   1600 false(reach) 29 16   570
email_spec11_productSimulator_false-unreach-call.cil.c killed by signal 9 70    70    15000 wit - -
email_spec1_product14_false-unreach-call.cil.c witness unconfirmed 130    130    630 wit true 22   12   990 true 21 11   530
email_spec1_product15_false-unreach-call.cil.c witness unconfirmed 90    90    440 wit true 25   13   940 true 20 11   460
email_spec1_product16_false-unreach-call.cil.c witness unconfirmed 75    75    450 wit true 25   13   1000 true 19 11   480
email_spec1_product20_false-unreach-call.cil.c witness unconfirmed 170    170    720 wit true 35   19   1400 true 20 11   520
email_spec1_product21_false-unreach-call.cil.c witness unconfirmed 170    170    770 wit true 36   20   1400 true 21 12   540
email_spec1_product22_false-unreach-call.cil.c witness unconfirmed 98    98    490 wit true 25   14   970 true 20 11   520
email_spec1_product26_false-unreach-call.cil.c witness unconfirmed 210    210    840 wit true 38   21   1500 true 22 12   540
email_spec1_product29_false-unreach-call.cil.c witness unconfirmed 150    150    710 wit true 33   17   1100 true 23 13   530
email_spec1_product30_false-unreach-call.cil.c witness unconfirmed 90    90    470 wit true 29   15   1000 true 22 12   540
email_spec1_product31_false-unreach-call.cil.c witness unconfirmed 81    81    490 wit true 33   18   1100 true 20 12   530
email_spec1_product32_false-unreach-call.cil.c witness unconfirmed 190    190    800 wit true 37   20   1500 true 22 12   540
email_spec1_product33_false-unreach-call.cil.c witness unconfirmed 110    110    550 wit true 32   17   1100 true 22 13   530
email_spec1_product34_false-unreach-call.cil.c witness unconfirmed 190    190    880 wit true 37   21   1500 true 23 13   530
email_spec1_product35_false-unreach-call.cil.c witness unconfirmed 240    240    960 wit true 38   22   1500 true 20 11   520
email_spec1_productSimulator_false-unreach-call.cil.c timeout 900    900    14000 wit - -
email_spec27_product17_false-unreach-call.cil.c false(reach) 150    150    660 wit true 24   13   980 false(reach) 35 19   600
email_spec27_product18_false-unreach-call.cil.c witness unconfirmed 81    81    440 wit true 22   12   930 true 21 12   410
email_spec27_product19_false-unreach-call.cil.c witness unconfirmed 85    85    460 wit true 28   15   1000 true 21 12   520
email_spec27_product23_false-unreach-call.cil.c false(reach) 180    180    730 wit true 33   18   1300 false(reach) 35 19   590
email_spec27_product24_false-unreach-call.cil.c witness unconfirmed 99    99    500 wit true 29   15   1000 true 21 11   520
email_spec27_product25_false-unreach-call.cil.c witness unconfirmed 180    180    780 wit true 35   19   1400 true 21 12   530
email_spec27_product27_false-unreach-call.cil.c witness unconfirmed 220    220    850 wit true 36   20   1500 true 22 13   420
email_spec27_product29_false-unreach-call.cil.c witness unconfirmed 140    140    730 wit true 28   15   1100 true 24 13   520
email_spec27_product30_false-unreach-call.cil.c witness unconfirmed 83    83    470 wit true 33   17   1100 true 22 12   540
email_spec27_product31_false-unreach-call.cil.c witness unconfirmed 96    96    500 wit true 30   16   1100 true 21 11   520
email_spec27_product32_false-unreach-call.cil.c witness unconfirmed 200    200    820 wit true 34   19   1400 true 23 13   520
email_spec27_product33_false-unreach-call.cil.c witness unconfirmed 91    91    540 wit true 35   19   1200 true 22 12   520
email_spec27_product34_false-unreach-call.cil.c witness unconfirmed 210    210    900 wit true 41   23   1500 true 20 11   530
email_spec27_product35_false-unreach-call.cil.c witness unconfirmed 250    250    980 wit true 38   22   1500 true 20 11   520
email_spec27_productSimulator_false-unreach-call.cil.c killed by signal 9 65    65    15000 wit - -
email_spec3_product13_false-unreach-call.cil.c false(reach) 1.1  1.1  130 wit true 19   10   770 false(reach) 26 15   520
email_spec3_product17_false-unreach-call.cil.c false(reach) 1.8  1.8  250 wit true 31   16   1000 false(reach) 30 16   530
email_spec3_product18_false-unreach-call.cil.c false(reach) 1.2  1.2  150 wit true 23   12   970 false(reach) 26 13   510
email_spec3_product19_false-unreach-call.cil.c false(reach) 1.1  1.1  160 wit true 28   15   980 false(reach) 26 15   530
email_spec3_product23_false-unreach-call.cil.c false(reach) 2.0  2.0  290 wit true 35   19   1400 false(reach) 28 16   520
email_spec3_product24_false-unreach-call.cil.c false(reach) 1.4  1.4  180 wit true 30   16   1000 false(reach) 24 13   520
email_spec3_product25_false-unreach-call.cil.c false(reach) 2.1  2.1  340 wit true 37   21   1600 false(reach) 28 15   550
email_spec3_product27_false-unreach-call.cil.c false(reach) 2.4  2.4  380 wit true 37   21   1600 false(reach) 26 16   540
email_spec3_product28_false-unreach-call.cil.c false(reach) 1.3  1.3  160 wit true 19   10   810 false(reach) 28 15   550
email_spec3_product29_false-unreach-call.cil.c false(reach) 2.2  2.2  330 wit true 32   17   1300 false(reach) 29 17   540
email_spec3_product30_false-unreach-call.cil.c false(reach) 1.4  1.4  180 wit true 29   15   1000 false(reach) 28 16   510
email_spec3_product31_false-unreach-call.cil.c false(reach) 1.5  1.5  210 wit true 30   16   1100 false(reach) 28 16   510
email_spec3_product32_false-unreach-call.cil.c false(reach) 2.5  2.5  380 wit true 36   20   1500 false(reach) 26 14   540
email_spec3_product33_false-unreach-call.cil.c false(reach) 1.7  1.7  220 wit true 30   16   1200 false(reach) 28 15   540
email_spec3_product34_false-unreach-call.cil.c false(reach) 2.8  2.8  460 wit true 40   23   1500 false(reach) 30 17   550
email_spec3_product35_false-unreach-call.cil.c false(reach) 3.1  3.1  510 wit true 39   22   1500 false(reach) 30 16   550
email_spec3_productSimulator_false-unreach-call.cil.c false(reach) 86    86    14000 wit timeout 90   64   4600 false(reach) 39 22   740
email_spec4_product18_false-unreach-call.cil.c witness unconfirmed 89    89    440 wit true 23   12   970 true 17 9.0 460
email_spec4_product19_false-unreach-call.cil.c witness unconfirmed 80    80    450 wit true 31   16   1000 true 21 12   490
email_spec4_product23_false-unreach-call.cil.c witness unconfirmed 170    170    720 wit true 35   19   1400 true 20 12   480
email_spec4_product24_false-unreach-call.cil.c witness unconfirmed 92    92    490 wit true 32   17   1100 true 20 12   490
email_spec4_product25_false-unreach-call.cil.c witness unconfirmed 190    190    770 wit true 35   19   1400 true 24 13   550
email_spec4_product27_false-unreach-call.cil.c witness unconfirmed 200    200    830 wit true 34   19   1400 true 19 11   520
email_spec4_product30_false-unreach-call.cil.c witness unconfirmed 85    85    470 wit true 25   13   1000 true 21 11   480
email_spec4_product31_false-unreach-call.cil.c witness unconfirmed 87    87    490 wit true 32   17   1100 true 20 11   530
email_spec4_product32_false-unreach-call.cil.c witness unconfirmed 160    160    790 wit true 35   19   1500 true 21 12   530
email_spec4_product33_false-unreach-call.cil.c witness unconfirmed 100    100    550 wit true 34   18   1200 true 21 15   520
email_spec4_product34_false-unreach-call.cil.c witness unconfirmed 200    200    880 wit true 41   23   1500 true 19 10   510
email_spec4_product35_false-unreach-call.cil.c witness unconfirmed 230    230    950 wit true 42   24   1500 true 21 13   520
email_spec4_productSimulator_false-unreach-call.cil.c timeout 900    900    14000 wit - -
email_spec6_product12_false-unreach-call.cil.c false(reach) 65    65    400 wit true 20   11   770 false(reach) 31 17   550
email_spec6_product14_false-unreach-call.cil.c false(reach) 150    150    660 wit true 25   14   980 false(reach) 29 15   560
email_spec6_product15_false-unreach-call.cil.c false(reach) 78    78    440 wit true 24   13   980 false(reach) 27 14   530
email_spec6_product16_false-unreach-call.cil.c false(reach) 80    80    450 wit true 26   14   1100 false(reach) 29 17   540
email_spec6_product20_false-unreach-call.cil.c false(reach) 170    170    730 wit true 30   17   1400 false(reach) 29 17   550
email_spec6_product21_false-unreach-call.cil.c false(reach) 170    170    790 wit true 33   18   1500 false(reach) 31 17   560
email_spec6_product22_false-unreach-call.cil.c false(reach) 93    93    490 wit true 26   14   1000 false(reach) 27 15   530
email_spec6_product26_false-unreach-call.cil.c false(reach) 210    210    870 wit true 33   19   1400 false(reach) 30 18   540
email_spec6_product28_false-unreach-call.cil.c false(reach) 90    90    440 wit true 22   12   880 false(reach) 32 17   540
email_spec6_product29_false-unreach-call.cil.c false(reach) 160    160    740 wit true 31   17   1100 false(reach) 33 18   580
email_spec6_product30_false-unreach-call.cil.c false(reach) 80    80    470 wit true 29   15   1000 false(reach) 27 16   520
email_spec6_product31_false-unreach-call.cil.c false(reach) 91    91    500 wit true 28   15   1100 false(reach) 30 17   550
email_spec6_product32_false-unreach-call.cil.c false(reach) 190    190    820 wit true 33   19   1500 false(reach) 32 18   580
email_spec6_product33_false-unreach-call.cil.c false(reach) 110    110    560 wit true 31   16   1300 false(reach) 29 16   550
email_spec6_product34_false-unreach-call.cil.c false(reach) 210    210    910 wit true 40   23   1500 false(reach) 34 18   580
email_spec6_product35_false-unreach-call.cil.c false(reach) 200    200    970 wit true 40   23   1500 false(reach) 30 17   560
email_spec6_productSimulator_false-unreach-call.cil.c timeout 900    900    14000 wit - -
email_spec7_product28_false-unreach-call.cil.c false(reach) 68    68    410 wit true 17   9.1 780 false(reach) 29 17   540
email_spec7_product29_false-unreach-call.cil.c false(reach) 120    120    710 wit true 30   16   1100 false(reach) 29 17   560
email_spec7_product30_false-unreach-call.cil.c false(reach) 90    90    460 wit true 28   15   1100 false(reach) 30 16   490
email_spec7_product31_false-unreach-call.cil.c false(reach) 78    78    480 wit true 30   16   1100 false(reach) 34 18   580
email_spec7_product32_false-unreach-call.cil.c false(reach) 190    190    790 wit true 35   20   1400 false(reach) 30 16   560
email_spec7_product33_false-unreach-call.cil.c false(reach) 110    110    550 wit true 33   17   1100 false(reach) 27 14   530
email_spec7_product34_false-unreach-call.cil.c false(reach) 200    200    870 wit true 37   21   1500 false(reach) 33 18   570
email_spec7_product35_false-unreach-call.cil.c false(reach) 180    180    930 wit true 41   23   1500 false(reach) 30 16   560
email_spec7_productSimulator_false-unreach-call.cil.c timeout 900    900    14000 wit - -
email_spec8_product15_false-unreach-call.cil.c witness unconfirmed 91    91    440 wit true 24   13   960 true 20 11   480
email_spec8_product16_false-unreach-call.cil.c witness unconfirmed 95    95    460 wit true 26   14   970 true 21 12   390
email_spec8_product20_false-unreach-call.cil.c witness unconfirmed 150    150    720 wit true 30   16   1400 true 20 12   500
email_spec8_product21_false-unreach-call.cil.c witness unconfirmed 170    170    780 wit true 32   17   1400 true 20 11   530
email_spec8_product22_false-unreach-call.cil.c witness unconfirmed 110    110    500 wit true 29   15   1000 true 22 15   390
email_spec8_product26_false-unreach-call.cil.c witness unconfirmed 200    200    840 wit true 35   19   1500 true 21 14   540
email_spec8_product30_false-unreach-call.cil.c witness unconfirmed 98    98    480 wit true 28   15   1100 true 21 13   530
email_spec8_product31_false-unreach-call.cil.c witness unconfirmed 83    83    500 wit true 29   15   1000 true 22 13   530
email_spec8_product32_false-unreach-call.cil.c witness unconfirmed 220    220    810 wit true 38   21   1500 true 22 12   530
email_spec8_product33_false-unreach-call.cil.c witness unconfirmed 89    89    540 wit true 32   17   1200 true 21 12   530
email_spec8_product34_false-unreach-call.cil.c witness unconfirmed 200    200    890 wit true 36   21   1500 true 23 13   540
email_spec8_product35_false-unreach-call.cil.c witness unconfirmed 220    220    960 wit true 41   23   1500 true 22 13   530
email_spec8_productSimulator_false-unreach-call.cil.c timeout 900    900    14000 wit - -
email_spec9_product15_false-unreach-call.cil.c witness unconfirmed 79    79    430 wit true 24   13   970 true 18 11   460
email_spec9_product16_false-unreach-call.cil.c witness unconfirmed 78    78    450 wit true 27   14   990 true 21 13   520
email_spec9_product20_false-unreach-call.cil.c witness unconfirmed 170    170    720 wit true 36   19   1400 true 21 16   500
email_spec9_product21_false-unreach-call.cil.c witness unconfirmed 180    180    780 wit true 37   20   1500 true 22 12   520
email_spec9_product22_false-unreach-call.cil.c witness unconfirmed 80    80    480 wit true 33   17   1000 true 19 11   480
email_spec9_product26_false-unreach-call.cil.c witness unconfirmed 220    220    840 wit true 34   19   1400 true 19 10   530
email_spec9_product30_false-unreach-call.cil.c witness unconfirmed 77    77    460 wit true 29   15   1000 true 22 13   530
email_spec9_product31_false-unreach-call.cil.c witness unconfirmed 98    99    510 wit true 28   15   1000 true 22 12   530
email_spec9_product32_false-unreach-call.cil.c witness unconfirmed 190    190    810 wit true 35   19   1500 true 20 11   520
email_spec9_product33_false-unreach-call.cil.c witness unconfirmed 85    85    540 wit true 31   16   1100 true 23 12   530
email_spec9_product34_false-unreach-call.cil.c witness unconfirmed 200    200    890 wit true 40   22   1500 true 22 13   520
email_spec9_product35_false-unreach-call.cil.c witness unconfirmed 220    220    960 wit true 36   21   1500 true 20 11   540
email_spec9_productSimulator_false-unreach-call.cil.c timeout 900    900    14000 wit - -
email_spec0_product05_true-unreach-call.cil.c true .64 .64 56 wit - -
email_spec0_product09_true-unreach-call.cil.c true 1.1  1.1  130 wit - -
email_spec0_product10_true-unreach-call.cil.c true .65 .65 67 wit - -
email_spec0_product11_true-unreach-call.cil.c true .94 .95 110 wit - -
email_spec0_product19_true-unreach-call.cil.c true 1.1  1.1  150 wit - -
email_spec0_product24_true-unreach-call.cil.c true 1.3  1.3  160 wit - -
email_spec0_product25_true-unreach-call.cil.c true 2.0  2.0  290 wit - -
email_spec0_product27_true-unreach-call.cil.c true 2.2  2.2  320 wit - -
email_spec0_product36_true-unreach-call.cil.c true 1.3  1.3  160 wit - -
email_spec0_product37_true-unreach-call.cil.c true 1.0  1.0  120 wit - -
email_spec0_product38_true-unreach-call.cil.c true 1.2  1.2  190 wit - -
email_spec0_product40_true-unreach-call.cil.c true 1.6  1.6  220 wit - -
email_spec11_product03_true-unreach-call.cil.c true .56 .56 50 wit - -
email_spec11_product07_true-unreach-call.cil.c true .99 .99 110 wit - -
email_spec11_product08_true-unreach-call.cil.c true .93 .94 100 wit - -
email_spec11_product10_true-unreach-call.cil.c true .65 .66 67 wit - -
email_spec11_product18_true-unreach-call.cil.c true 1.1  1.1  130 wit - -
email_spec11_product23_true-unreach-call.cil.c true 1.5  1.5  240 wit - -
email_spec11_product24_true-unreach-call.cil.c true 1.0  1.0  160 wit - -
email_spec11_product27_true-unreach-call.cil.c true 1.9  1.9  330 wit - -
email_spec11_product36_true-unreach-call.cil.c true 1.3  1.3  160 wit - -
email_spec11_product37_true-unreach-call.cil.c true .95 .96 120 wit - -
email_spec11_product39_true-unreach-call.cil.c true 1.4  1.4  170 wit - -
email_spec11_product40_true-unreach-call.cil.c true 1.6  1.6  220 wit - -
email_spec1_product12_true-unreach-call.cil.c true .99 .99 110 wit - -
email_spec1_product28_true-unreach-call.cil.c true 1.2  1.2  140 wit - -
email_spec27_product13_true-unreach-call.cil.c true 1.1  1.1  120 wit - -
email_spec27_product28_true-unreach-call.cil.c true 1.2  1.2  150 wit - -
email_spec4_product13_true-unreach-call.cil.c true 1.1  1.1  120 wit - -
email_spec4_product17_true-unreach-call.cil.c true 1.5  1.5  210 wit - -
email_spec4_product28_true-unreach-call.cil.c true 1.2  1.2  140 wit - -
email_spec4_product29_true-unreach-call.cil.c true 2.0  2.0  290 wit - -
email_spec7_product13_true-unreach-call.cil.c true 1.0  1.0  110 wit - -
email_spec7_product17_true-unreach-call.cil.c true 1.5  1.5  200 wit - -
email_spec7_product18_true-unreach-call.cil.c true 1.1  1.1  130 wit - -
email_spec7_product19_true-unreach-call.cil.c true 1.2  1.2  140 wit - -
email_spec7_product23_true-unreach-call.cil.c true 1.7  1.7  240 wit - -
email_spec7_product24_true-unreach-call.cil.c true 1.3  1.3  160 wit - -
email_spec7_product25_true-unreach-call.cil.c true 1.9  1.9  280 wit - -
email_spec7_product27_true-unreach-call.cil.c true 2.1  2.1  320 wit - -
email_spec8_product12_true-unreach-call.cil.c true 1.0  1.1  110 wit - -
email_spec8_product14_true-unreach-call.cil.c true 410    410    1100 wit - -
email_spec8_product28_true-unreach-call.cil.c true 1.2  1.2  140 wit - -
email_spec8_product29_true-unreach-call.cil.c true 430    430    1200 wit - -
email_spec9_product12_true-unreach-call.cil.c true 1.0  1.0  110 wit - -
email_spec9_product14_true-unreach-call.cil.c true 450    450    1100 wit - -
email_spec9_product28_true-unreach-call.cil.c true 1.2  1.2  140 wit - -
email_spec9_product29_true-unreach-call.cil.c true 440    440    1200 wit - -
minepump_spec1_product33_false-unreach-call.cil.c false(reach) .19 .19 31 wit true 7.9 4.4 290 false(reach) 17 10   360
minepump_spec1_product34_false-unreach-call.cil.c false(reach) .21 .21 31 wit false(reach) 9.1 4.9 400 false(reach) 19 10   370
minepump_spec1_product35_false-unreach-call.cil.c false(reach) .20 .20 33 wit false(reach) 8.9 4.9 410 false(reach) 16 9.4 370
minepump_spec1_product36_false-unreach-call.cil.c false(reach) .19 .19 31 wit true 7.3 4.1 300 false(reach) 17 9.6 360
minepump_spec1_product37_false-unreach-call.cil.c false(reach) .23 .24 33 wit true 6.4 3.7 300 false(reach) 16 8.7 350
minepump_spec1_product38_false-unreach-call.cil.c false(reach) .24 .25 35 wit true 6.5 3.7 280 false(reach) 19 12   380
minepump_spec1_product39_false-unreach-call.cil.c false(reach) .18 .18 33 wit true 7.6 4.1 300 false(reach) 17 10   360
minepump_spec1_product40_false-unreach-call.cil.c false(reach) .22 .23 35 wit true 8.3 4.6 300 false(reach) 18 11   380
minepump_spec1_product41_false-unreach-call.cil.c false(reach) 2.1  2.1  56 wit false(reach) 11   6.0 430 false(reach) 19 10   420
minepump_spec1_product42_false-unreach-call.cil.c false(reach) 2.2  2.2  57 wit true 7.7 4.3 300 false(reach) 18 9.9 420
minepump_spec1_product43_false-unreach-call.cil.c false(reach) 2.3  2.3  59 wit false(reach) 11   6.0 430 false(reach) 19 11   420
minepump_spec1_product44_false-unreach-call.cil.c false(reach) 2.3  2.3  60 wit true 8.0 4.5 290 false(reach) 18 10   410
minepump_spec1_product49_false-unreach-call.cil.c false(reach) .27 .27 34 wit true 8.2 4.5 290 false(reach) 14 8.1 340
minepump_spec1_product50_false-unreach-call.cil.c false(reach) .24 .24 34 wit false(reach) 9.0 5.0 400 false(reach) 15 8.0 340
minepump_spec1_product51_false-unreach-call.cil.c false(reach) .24 .25 35 wit true 8.8 4.8 320 false(reach) 18 10   350
minepump_spec1_product52_false-unreach-call.cil.c false(reach) .19 .19 35 wit false(reach) 11   6.0 410 false(reach) 19 12   390
minepump_spec1_product53_false-unreach-call.cil.c false(reach) .39 .40 38 wit true 7.4 4.1 300 false(reach) 15 10   360
minepump_spec1_product54_false-unreach-call.cil.c false(reach) .35 .35 37 wit true 7.9 4.4 300 false(reach) 14 7.6 360
minepump_spec1_product55_false-unreach-call.cil.c false(reach) .36 .36 37 wit false(reach) 9.8 5.4 410 false(reach) 17 9.5 380
minepump_spec1_product56_false-unreach-call.cil.c false(reach) .33 .33 39 wit true 7.9 4.4 310 false(reach) 18 11   360
minepump_spec1_productSimulator_false-unreach-call.cil.c witness unconfirmed .72 .73 92 wit true 11   6.0 470 true 14 7.7 360
minepump_spec2_product33_false-unreach-call.cil.c false(reach) 1.5  1.6  53 wit true 7.3 4.1 290 false(reach) 18 9.4 400
minepump_spec2_product34_false-unreach-call.cil.c false(reach) 1.6  1.6  51 wit true 6.5 3.7 290 false(reach) 18 9.9 390
minepump_spec2_product35_false-unreach-call.cil.c false(reach) 1.8  1.8  52 wit true 7.9 4.5 290 false(reach) 19 12   430
minepump_spec2_product36_false-unreach-call.cil.c false(reach) 1.8  1.8  52 wit true 7.4 4.2 300 false(reach) 18 9.7 400
minepump_spec2_product41_false-unreach-call.cil.c false(reach) 3.7  3.7  88 wit true 7.4 4.1 290 false(reach) 18 10   460
minepump_spec2_product42_false-unreach-call.cil.c false(reach) 4.2  4.2  93 wit true 8.4 4.6 300 false(reach) 22 12   460
minepump_spec2_product43_false-unreach-call.cil.c false(reach) 4.5  4.5  96 wit true 8.1 4.4 310 false(reach) 18 10   380
minepump_spec2_product44_false-unreach-call.cil.c false(reach) 4.3  4.3  92 wit false(reach) 10   5.5 450 false(reach) 18 9.5 380
minepump_spec2_productSimulator_false-unreach-call.cil.c false(reach) 8.2  8.2  170 wit false(reach) 10   5.6 440 true 13 7.5 330
minepump_spec3_product01_false-unreach-call.cil.c false(reach) .17 .17 29 wit false(reach) 9.3 5.1 370 false(reach) 14 7.4 340
minepump_spec3_product02_false-unreach-call.cil.c false(reach) .19 .20 31 wit true 7.7 4.3 280 false(reach) 14 9.6 330
minepump_spec3_product03_false-unreach-call.cil.c false(reach) .16 .17 29 wit true 6.6 3.8 290 false(reach) 18 10   370
minepump_spec3_product04_false-unreach-call.cil.c false(reach) .22 .22 32 wit false(reach) 9.6 5.2 390 false(reach) 14 9.3 320
minepump_spec3_product05_false-unreach-call.cil.c false(reach) .23 .24 32 wit true 6.4 3.6 280 false(reach) 14 8.0 350
minepump_spec3_product06_false-unreach-call.cil.c false(reach) .18 .19 33 wit false(reach) 8.5 4.7 380 false(reach) 15 9.3 340
minepump_spec3_product07_false-unreach-call.cil.c false(reach) .23 .24 32 wit true 6.7 3.7 280 false(reach) 13 7.3 360
minepump_spec3_product08_false-unreach-call.cil.c false(reach) .21 .21 31 wit true 6.9 3.9 290 false(reach) 13 7.9 340
minepump_spec3_product09_false-unreach-call.cil.c false(reach) .16 .16 29 wit true 7.3 4.2 280 false(reach) 13 8.0 340
minepump_spec3_product10_false-unreach-call.cil.c false(reach) .19 .20 31 wit true 7.4 4.2 280 false(reach) 14 7.7 330
minepump_spec3_product11_false-unreach-call.cil.c false(reach) .18 .18 30 wit true 6.8 3.8 290 false(reach) 16 8.3 360
minepump_spec3_product12_false-unreach-call.cil.c false(reach) .20 .20 32 wit true 7.6 4.2 280 false(reach) 17 9.8 370
minepump_spec3_product13_false-unreach-call.cil.c false(reach) .15 .15 31 wit false(reach) 9.8 5.4 390 false(reach) 14 9.2 350
minepump_spec3_product14_false-unreach-call.cil.c false(reach) .23 .23 31 wit true 7.5 4.2 290 false(reach) 13 7.1 340
minepump_spec3_product15_false-unreach-call.cil.c false(reach) .21 .21 31 wit false(reach) 9.1 5.0 390 false(reach) 15 8.1 350
minepump_spec3_product16_false-unreach-call.cil.c false(reach) .19 .19 33 wit true 7.1 3.9 270 false(reach) 12 6.9 340
minepump_spec3_product17_false-unreach-call.cil.c false(reach) .24 .24 32 wit false(reach) 8.7 4.7 380 false(reach) 13 7.6 350
minepump_spec3_product18_false-unreach-call.cil.c false(reach) .16 .16 33 wit false(reach) 9.4 5.1 370 false(reach) 14 7.6 340
minepump_spec3_product19_false-unreach-call.cil.c false(reach) .20 .21 33 wit true 7.5 4.2 290 false(reach) 16 8.8 360
minepump_spec3_product20_false-unreach-call.cil.c false(reach) .16 .16 32 wit true 7.8 4.3 290 false(reach) 16 9.2 370
minepump_spec3_product21_false-unreach-call.cil.c false(reach) .24 .24 33 wit true 7.6 4.2 280 false(reach) 15 9.6 350
minepump_spec3_product22_false-unreach-call.cil.c false(reach) .23 .24 33 wit false(reach) 9.7 5.3 410 false(reach) 17 11   390
minepump_spec3_product23_false-unreach-call.cil.c false(reach) .23 .24 34 wit false(reach) 9.2 5.0 390 false(reach) 15 9.2 340
minepump_spec3_product24_false-unreach-call.cil.c false(reach) .24 .25 35 wit true 7.4 4.1 290 false(reach) 15 8.8 360
minepump_spec3_product25_false-unreach-call.cil.c false(reach) .21 .22 31 wit false(reach) 9.7 5.4 400 false(reach) 13 7.3 380
minepump_spec3_product26_false-unreach-call.cil.c false(reach) .19 .20 31 wit false(reach) 9.9 5.3 410 false(reach) 13 8.0 340
minepump_spec3_product27_false-unreach-call.cil.c false(reach) .16 .16 32 wit true 7.7 4.3 290 false(reach) 13 7.5 360
minepump_spec3_product28_false-unreach-call.cil.c false(reach) .20 .21 31 wit false(reach) 9.2 5.1 400 false(reach) 14 8.1 350
minepump_spec3_product29_false-unreach-call.cil.c false(reach) .23 .24 34 wit false(reach) 9.7 5.3 400 false(reach) 19 11   420
minepump_spec3_product30_false-unreach-call.cil.c false(reach) .23 .24 34 wit false(reach) 8.9 4.8 390 false(reach) 18 10   400
minepump_spec3_product31_false-unreach-call.cil.c false(reach) .23 .24 35 wit true 8.1 4.6 310 false(reach) 18 11   400
minepump_spec3_product32_false-unreach-call.cil.c false(reach) .24 .24 34 wit true 7.8 4.3 280 false(reach) 15 8.0 360
minepump_spec3_product35_false-unreach-call.cil.c false(reach) .20 .21 33 wit false(reach) 9.3 5.1 390 false(reach) 16 8.9 380
minepump_spec3_product36_false-unreach-call.cil.c false(reach) .21 .21 33 wit true 7.6 4.2 290 false(reach) 20 11   390
minepump_spec3_product39_false-unreach-call.cil.c false(reach) .25 .25 36 wit true 7.6 4.2 290 false(reach) 18 11   360
minepump_spec3_product40_false-unreach-call.cil.c false(reach) .25 .25 34 wit false(reach) 8.9 4.9 390 false(reach) 19 11   380
minepump_spec3_product43_false-unreach-call.cil.c false(reach) .24 .25 33 wit true 7.4 4.1 290 false(reach) 17 9.7 390
minepump_spec3_product44_false-unreach-call.cil.c false(reach) .22 .22 34 wit false(reach) 9.5 5.2 400 false(reach) 17 9.1 380
minepump_spec3_product47_false-unreach-call.cil.c false(reach) .26 .27 36 wit true 7.0 3.9 300 false(reach) 16 9.9 350
minepump_spec3_product48_false-unreach-call.cil.c false(reach) .26 .27 36 wit false(reach) 8.3 4.7 400 false(reach) 13 7.8 340
minepump_spec3_product51_false-unreach-call.cil.c false(reach) .25 .26 35 wit false(reach) 10   5.6 410 false(reach) 18 9.9 350
minepump_spec3_product52_false-unreach-call.cil.c false(reach) .26 .27 35 wit true 7.8 4.3 310 false(reach) 15 8.3 340
minepump_spec3_product55_false-unreach-call.cil.c false(reach) .37 .38 39 wit false(reach) 9.5 5.2 400 false(reach) 14 7.8 360
minepump_spec3_product56_false-unreach-call.cil.c false(reach) .26 .26 40 wit false(reach) 10   5.4 400 false(reach) 18 12   390
minepump_spec3_product59_false-unreach-call.cil.c false(reach) .32 .33 37 wit true 8.1 4.5 310 false(reach) 16 9.0 360
minepump_spec3_product60_false-unreach-call.cil.c false(reach) .29 .29 37 wit true 7.9 4.4 300 false(reach) 19 10   380
minepump_spec3_product63_false-unreach-call.cil.c false(reach) .39 .39 46 wit false(reach) 9.9 5.3 400 false(reach) 18 12   400
minepump_spec3_product64_false-unreach-call.cil.c false(reach) .40 .41 46 wit true 8.6 4.7 310 false(reach) 14 8.1 350
minepump_spec3_productSimulator_false-unreach-call.cil.c witness unconfirmed .73 .74 94 wit true 11   5.9 460 true 14 8.4 340
minepump_spec4_product33_false-unreach-call.cil.c false(reach) 2.3  2.3  68 wit false(reach) 10   5.6 410 false(reach) 19 12   470
minepump_spec4_product34_false-unreach-call.cil.c false(reach) 2.6  2.6  70 wit false(reach) 10   5.6 430 false(reach) 18 10   390
minepump_spec4_product35_false-unreach-call.cil.c false(reach) 3.0  3.0  75 wit true 7.5 4.2 290 false(reach) 22 13   440
minepump_spec4_product36_false-unreach-call.cil.c false(reach) 3.7  3.7  75 wit true 8.0 4.4 280 false(reach) 20 12   440
minepump_spec4_product37_false-unreach-call.cil.c false(reach) 4.8  4.9  98 wit false(reach) 10   5.7 420 false(reach) 19 11   440
minepump_spec4_product38_false-unreach-call.cil.c false(reach) 4.3  4.3  99 wit false(reach) 11   5.8 440 false(reach) 17 9.7 360
minepump_spec4_product39_false-unreach-call.cil.c false(reach) 4.4  4.4  100 wit true 8.2 4.5 300 false(reach) 21 11   380
minepump_spec4_product40_false-unreach-call.cil.c false(reach) 4.4  4.4  99 wit false(reach) 11   5.7 440 false(reach) 17 9.1 360
minepump_spec4_product41_false-unreach-call.cil.c false(reach) 4.4  4.4  92 wit true 7.4 4.1 300 false(reach) 19 11   410
minepump_spec4_product42_false-unreach-call.cil.c false(reach) 3.5  3.5  92 wit true 7.6 4.2 290 false(reach) 19 12   460
minepump_spec4_product43_false-unreach-call.cil.c false(reach) 5.2  5.2  96 wit false(reach) 11   6.0 430 false(reach) 16 8.6 380
minepump_spec4_product44_false-unreach-call.cil.c false(reach) 4.9  4.9  97 wit true 7.9 4.4 300 false(reach) 18 11   460
minepump_spec4_product45_false-unreach-call.cil.c false(reach) 4.6  4.6  100 wit true 8.7 4.7 310 false(reach) 20 11   480
minepump_spec4_product46_false-unreach-call.cil.c false(reach) 4.7  4.7  110 wit true 7.6 4.2 320 false(reach) 20 11   480
minepump_spec4_product47_false-unreach-call.cil.c false(reach) 5.5  5.6  110 wit true 9.0 5.0 310 false(reach) 19 11   400
minepump_spec4_product48_false-unreach-call.cil.c false(reach) 5.2  5.2  110 wit true 8.9 4.8 310 false(reach) 19 10   460
minepump_spec4_productSimulator_false-unreach-call.cil.c witness unconfirmed 18    18    260 wit true 10   5.6 460 true 14 7.8 340
minepump_spec1_product01_true-unreach-call.cil.c true .18 .19 31 wit - -
minepump_spec1_product02_true-unreach-call.cil.c true .20 .20 28 wit - -
minepump_spec1_product03_true-unreach-call.cil.c true .12 .13 29 wit - -
minepump_spec1_product04_true-unreach-call.cil.c true .12 .13 29 wit - -
minepump_spec1_product05_true-unreach-call.cil.c true .18 .18 32 wit - -
minepump_spec1_product06_true-unreach-call.cil.c true .14 .14 31 wit - -
minepump_spec1_product07_true-unreach-call.cil.c true .18 .19 30 wit - -
minepump_spec1_product08_true-unreach-call.cil.c true .17 .18 30 wit - -
minepump_spec1_product09_true-unreach-call.cil.c true .19 .20 29 wit - -
minepump_spec1_product10_true-unreach-call.cil.c true .20 .21 29 wit - -
minepump_spec1_product11_true-unreach-call.cil.c true .16 .16 29 wit - -
minepump_spec1_product12_true-unreach-call.cil.c true .15 .16 29 wit - -
minepump_spec1_product13_true-unreach-call.cil.c true .19 .20 31 wit - -
minepump_spec1_product14_true-unreach-call.cil.c true .14 .14 31 wit - -
minepump_spec1_product15_true-unreach-call.cil.c true .21 .22 31 wit - -
minepump_spec1_product16_true-unreach-call.cil.c true .17 .18 30 wit - -
minepump_spec1_product17_true-unreach-call.cil.c true .18 .19 32 wit - -
minepump_spec1_product18_true-unreach-call.cil.c true .15 .15 32 wit - -
minepump_spec1_product19_true-unreach-call.cil.c true .15 .16 31 wit - -
minepump_spec1_product20_true-unreach-call.cil.c true .19 .19 31 wit - -
minepump_spec1_product21_true-unreach-call.cil.c true .23 .23 34 wit - -
minepump_spec1_product22_true-unreach-call.cil.c true .26 .26 34 wit - -
minepump_spec1_product23_true-unreach-call.cil.c true .22 .23 34 wit - -
minepump_spec1_product24_true-unreach-call.cil.c true .25 .26 33 wit - -
minepump_spec1_product25_true-unreach-call.cil.c true .18 .19 31 wit - -
minepump_spec1_product26_true-unreach-call.cil.c true .21 .22 33 wit - -
minepump_spec1_product27_true-unreach-call.cil.c true .22 .23 32 wit - -
minepump_spec1_product28_true-unreach-call.cil.c true .19 .19 33 wit - -
minepump_spec1_product29_true-unreach-call.cil.c true .26 .27 33 wit - -
minepump_spec1_product30_true-unreach-call.cil.c true .23 .23 33 wit - -
minepump_spec1_product31_true-unreach-call.cil.c true .24 .24 32 wit - -
minepump_spec1_product32_true-unreach-call.cil.c true .22 .23 33 wit - -
minepump_spec1_product45_true-unreach-call.cil.c true .24 .25 35 wit - -
minepump_spec1_product46_true-unreach-call.cil.c true .29 .29 36 wit - -
minepump_spec1_product47_true-unreach-call.cil.c timeout 900    900    4500 wit - -
minepump_spec1_product48_true-unreach-call.cil.c timeout 900    900    4300 wit - -
minepump_spec1_product57_true-unreach-call.cil.c timeout 900    900    4700 wit - -
minepump_spec1_product58_true-unreach-call.cil.c timeout 900    900    4800 wit - -
minepump_spec1_product59_true-unreach-call.cil.c timeout 900    900    4700 wit - -
minepump_spec1_product60_true-unreach-call.cil.c timeout 900    900    4600 wit - -
minepump_spec1_product61_true-unreach-call.cil.c true .42 .43 44 wit - -
minepump_spec1_product62_true-unreach-call.cil.c true .36 .37 43 wit - -
minepump_spec1_product63_true-unreach-call.cil.c timeout 900    900    5000 wit - -
minepump_spec1_product64_true-unreach-call.cil.c timeout 900    900    4900 wit - -
minepump_spec2_product01_true-unreach-call.cil.c true .18 .19 29 wit - -
minepump_spec2_product02_true-unreach-call.cil.c true .19 .20 29 wit - -
minepump_spec2_product03_true-unreach-call.cil.c true .17 .18 29 wit - -
minepump_spec2_product04_true-unreach-call.cil.c true .20 .20 29 wit - -
minepump_spec2_product05_true-unreach-call.cil.c true .18 .19 29 wit - -
minepump_spec2_product06_true-unreach-call.cil.c true .22 .23 30 wit - -
minepump_spec2_product07_true-unreach-call.cil.c true .22 .22 30 wit - -
minepump_spec2_product08_true-unreach-call.cil.c true .17 .18 32 wit - -
minepump_spec2_product09_true-unreach-call.cil.c true .17 .17 29 wit - -
minepump_spec2_product10_true-unreach-call.cil.c true .16 .17 31 wit - -
minepump_spec2_product11_true-unreach-call.cil.c true .20 .21 29 wit - -
minepump_spec2_product12_true-unreach-call.cil.c true .21 .21 29 wit - -
minepump_spec2_product13_true-unreach-call.cil.c true .20 .20 32 wit - -
minepump_spec2_product14_true-unreach-call.cil.c true .20 .21 30 wit - -
minepump_spec2_product15_true-unreach-call.cil.c true .21 .22 30 wit - -
minepump_spec2_product16_true-unreach-call.cil.c true .19 .20 30 wit - -
minepump_spec2_product17_true-unreach-call.cil.c true .19 .19 33 wit - -
minepump_spec2_product18_true-unreach-call.cil.c true .21 .22 33 wit - -
minepump_spec2_product19_true-unreach-call.cil.c true .17 .17 32 wit - -
minepump_spec2_product20_true-unreach-call.cil.c true .21 .21 31 wit - -
minepump_spec2_product21_true-unreach-call.cil.c true .27 .28 32 wit - -
minepump_spec2_product22_true-unreach-call.cil.c true .22 .23 32 wit - -
minepump_spec2_product23_true-unreach-call.cil.c true .28 .29 34 wit - -
minepump_spec2_product24_true-unreach-call.cil.c true .28 .28 34 wit - -
minepump_spec2_product25_true-unreach-call.cil.c true .23 .23 31 wit - -
minepump_spec2_product26_true-unreach-call.cil.c true .21 .21 31 wit - -
minepump_spec2_product27_true-unreach-call.cil.c true .23 .23 32 wit - -
minepump_spec2_product28_true-unreach-call.cil.c true .19 .19 32 wit - -
minepump_spec2_product29_true-unreach-call.cil.c true .23 .23 33 wit - -
minepump_spec2_product30_true-unreach-call.cil.c true .25 .26 32 wit - -
minepump_spec2_product31_true-unreach-call.cil.c true .23 .23 34 wit - -
minepump_spec2_product32_true-unreach-call.cil.c true .23 .23 34 wit - -
minepump_spec2_product37_true-unreach-call.cil.c true 4.1  4.1  95 wit - -
minepump_spec2_product38_true-unreach-call.cil.c true 4.7  4.7  100 wit - -
minepump_spec2_product39_true-unreach-call.cil.c timeout 900    900    4500 wit - -
minepump_spec2_product40_true-unreach-call.cil.c timeout 900    900    4100 wit - -
minepump_spec2_product45_true-unreach-call.cil.c true .25 .26 35 wit - -
minepump_spec2_product46_true-unreach-call.cil.c true .25 .26 36 wit - -
minepump_spec2_product47_true-unreach-call.cil.c timeout 900    900    4300 wit - -
minepump_spec2_product48_true-unreach-call.cil.c timeout 900    900    3900 wit - -
minepump_spec2_product49_true-unreach-call.cil.c timeout 900    900    5000 wit - -
minepump_spec2_product50_true-unreach-call.cil.c timeout 900    900    4900 wit - -
minepump_spec2_product51_true-unreach-call.cil.c timeout 900    900    4600 wit - -
minepump_spec2_product52_true-unreach-call.cil.c timeout 900    900    4300 wit - -
minepump_spec2_product53_true-unreach-call.cil.c true 6.9  6.9  140 wit - -
minepump_spec2_product54_true-unreach-call.cil.c true 7.2  7.2  150 wit - -
minepump_spec2_product55_true-unreach-call.cil.c timeout 900    900    4900 wit - -
minepump_spec2_product56_true-unreach-call.cil.c timeout 900    900    4600 wit - -
minepump_spec2_product57_true-unreach-call.cil.c timeout 900    900    4400 wit - -
minepump_spec2_product58_true-unreach-call.cil.c timeout 900    900    4600 wit - -
minepump_spec2_product59_true-unreach-call.cil.c timeout 900    900    4500 wit - -
minepump_spec2_product60_true-unreach-call.cil.c timeout 900    900    4400 wit - -
minepump_spec2_product61_true-unreach-call.cil.c true .41 .41 45 wit - -
minepump_spec2_product62_true-unreach-call.cil.c true .40 .40 44 wit - -
minepump_spec2_product63_true-unreach-call.cil.c timeout 900    900    4800 wit - -
minepump_spec2_product64_true-unreach-call.cil.c timeout 900    900    4600 wit - -
minepump_spec3_product33_true-unreach-call.cil.c true .20 .20 31 wit - -
minepump_spec3_product34_true-unreach-call.cil.c true .20 .20 31 wit - -
minepump_spec3_product37_true-unreach-call.cil.c true .23 .24 34 wit - -
minepump_spec3_product38_true-unreach-call.cil.c true .26 .27 35 wit - -
minepump_spec3_product41_true-unreach-call.cil.c true .23 .24 35 wit - -
minepump_spec3_product42_true-unreach-call.cil.c true .17 .17 35 wit - -
minepump_spec3_product45_true-unreach-call.cil.c true .30 .30 36 wit - -
minepump_spec3_product46_true-unreach-call.cil.c true .26 .27 36 wit - -
minepump_spec3_product49_true-unreach-call.cil.c true 6.5  6.5  110 wit - -
minepump_spec3_product50_true-unreach-call.cil.c true 5.8  5.8  110 wit - -
minepump_spec3_product53_true-unreach-call.cil.c true 8.2  8.3  150 wit - -
minepump_spec3_product54_true-unreach-call.cil.c true 8.6  8.6  150 wit - -
minepump_spec3_product57_true-unreach-call.cil.c timeout 900    900    4600 wit - -
minepump_spec3_product58_true-unreach-call.cil.c timeout 900    900    4800 wit - -
minepump_spec3_product61_true-unreach-call.cil.c timeout 900    900    4900 wit - -
minepump_spec3_product62_true-unreach-call.cil.c timeout 900    900    5000 wit - -
minepump_spec4_product01_true-unreach-call.cil.c true .15 .16 30 wit - -
minepump_spec4_product02_true-unreach-call.cil.c true .15 .16 30 wit - -
minepump_spec4_product03_true-unreach-call.cil.c true .19 .19 31 wit - -
minepump_spec4_product04_true-unreach-call.cil.c true .16 .16 29 wit - -
minepump_spec4_product05_true-unreach-call.cil.c true .18 .19 30 wit - -
minepump_spec4_product06_true-unreach-call.cil.c true .20 .21 30 wit - -
minepump_spec4_product07_true-unreach-call.cil.c true .17 .18 30 wit - -
minepump_spec4_product08_true-unreach-call.cil.c true .23 .23 30 wit - -
minepump_spec4_product09_true-unreach-call.cil.c true .13 .14 28 wit - -
minepump_spec4_product10_true-unreach-call.cil.c true .16 .16 30 wit - -
minepump_spec4_product11_true-unreach-call.cil.c true .16 .16 31 wit - -
minepump_spec4_product12_true-unreach-call.cil.c true .16 .16 29 wit - -
minepump_spec4_product13_true-unreach-call.cil.c true .17 .18 30 wit - -
minepump_spec4_product14_true-unreach-call.cil.c true .20 .20 30 wit - -
minepump_spec4_product15_true-unreach-call.cil.c true .18 .18 32 wit - -
minepump_spec4_product16_true-unreach-call.cil.c true .22 .22 32 wit - -
minepump_spec4_product17_true-unreach-call.cil.c true .22 .23 30 wit - -
minepump_spec4_product18_true-unreach-call.cil.c true .19 .19 33 wit - -
minepump_spec4_product19_true-unreach-call.cil.c true .21 .22 31 wit - -
minepump_spec4_product20_true-unreach-call.cil.c true .21 .21 32 wit - -
minepump_spec4_product21_true-unreach-call.cil.c true .23 .23 32 wit - -
minepump_spec4_product22_true-unreach-call.cil.c true .22 .23 35 wit - -
minepump_spec4_product23_true-unreach-call.cil.c true .18 .19 33 wit - -
minepump_spec4_product24_true-unreach-call.cil.c true .27 .27 34 wit - -
minepump_spec4_product25_true-unreach-call.cil.c true .19 .19 32 wit - -
minepump_spec4_product26_true-unreach-call.cil.c true .18 .19 31 wit - -
minepump_spec4_product27_true-unreach-call.cil.c true .22 .22 31 wit - -
minepump_spec4_product28_true-unreach-call.cil.c true .19 .20 31 wit - -
minepump_spec4_product29_true-unreach-call.cil.c true .27 .27 34 wit - -
minepump_spec4_product30_true-unreach-call.cil.c true .26 .26 33 wit - -
minepump_spec4_product31_true-unreach-call.cil.c true .26 .26 34 wit - -
minepump_spec4_product32_true-unreach-call.cil.c true .17 .18 35 wit - -
minepump_spec4_product49_true-unreach-call.cil.c true 4.1  4.1  100 wit - -
minepump_spec4_product50_true-unreach-call.cil.c true 5.0  5.0  110 wit - -
minepump_spec4_product51_true-unreach-call.cil.c timeout 900    900    4600 wit - -
minepump_spec4_product52_true-unreach-call.cil.c timeout 900    900    4400 wit - -
minepump_spec4_product53_true-unreach-call.cil.c true 7.9  7.9  150 wit - -
minepump_spec4_product54_true-unreach-call.cil.c true 9.3  9.3  150 wit - -
minepump_spec4_product55_true-unreach-call.cil.c timeout 900    900    5000 wit - -
minepump_spec4_product56_true-unreach-call.cil.c timeout 900    900    4800 wit - -
minepump_spec4_product57_true-unreach-call.cil.c true 7.5  7.5  140 wit - -
minepump_spec4_product58_true-unreach-call.cil.c true 7.1  7.1  140 wit - -
minepump_spec4_product59_true-unreach-call.cil.c timeout 900    900    4700 wit - -
minepump_spec4_product60_true-unreach-call.cil.c timeout 900    900    4500 wit - -
minepump_spec4_product61_true-unreach-call.cil.c true 10    10    170 wit - -
minepump_spec4_product62_true-unreach-call.cil.c true 10    10    170 wit - -
minepump_spec4_product63_true-unreach-call.cil.c timeout 900    900    5000 wit - -
minepump_spec4_product64_true-unreach-call.cil.c timeout 900    900    4800 wit - -
minepump_spec5_product01_true-unreach-call.cil.c true .13 .13 29 wit - -
minepump_spec5_product02_true-unreach-call.cil.c true .19 .19 29 wit - -
minepump_spec5_product03_true-unreach-call.cil.c true .17 .17 29 wit - -
minepump_spec5_product04_true-unreach-call.cil.c true .17 .17 29 wit - -
minepump_spec5_product05_true-unreach-call.cil.c true .23 .23 30 wit - -
minepump_spec5_product06_true-unreach-call.cil.c true .18 .18 32 wit - -
minepump_spec5_product07_true-unreach-call.cil.c true .14 .15 32 wit - -
minepump_spec5_product08_true-unreach-call.cil.c true .20 .21 30 wit - -
minepump_spec5_product09_true-unreach-call.cil.c true .17 .17 29 wit - -
minepump_spec5_product10_true-unreach-call.cil.c true .17 .18 29 wit - -
minepump_spec5_product11_true-unreach-call.cil.c true .16 .17 29 wit - -
minepump_spec5_product12_true-unreach-call.cil.c true .13 .13 29 wit - -
minepump_spec5_product13_true-unreach-call.cil.c true .18 .18 30 wit - -
minepump_spec5_product14_true-unreach-call.cil.c true .20 .20 31 wit - -
minepump_spec5_product15_true-unreach-call.cil.c true .22 .23 30 wit - -
minepump_spec5_product16_true-unreach-call.cil.c true .18 .18 32 wit - -
minepump_spec5_product17_true-unreach-call.cil.c true .19 .19 32 wit - -
minepump_spec5_product18_true-unreach-call.cil.c true .15 .15 33 wit - -
minepump_spec5_product19_true-unreach-call.cil.c true .22 .23 31 wit - -
minepump_spec5_product20_true-unreach-call.cil.c true .24 .25 32 wit - -
minepump_spec5_product21_true-unreach-call.cil.c true .23 .23 32 wit - -
minepump_spec5_product22_true-unreach-call.cil.c true .30 .31 33 wit - -
minepump_spec5_product23_true-unreach-call.cil.c true .18 .19 34 wit - -
minepump_spec5_product24_true-unreach-call.cil.c true .23 .23 34 wit - -
minepump_spec5_product25_true-unreach-call.cil.c true .19 .19 31 wit - -
minepump_spec5_product26_true-unreach-call.cil.c true .21 .22 31 wit - -
minepump_spec5_product27_true-unreach-call.cil.c true .20 .20 31 wit - -
minepump_spec5_product28_true-unreach-call.cil.c true .23 .24 33 wit - -
minepump_spec5_product29_true-unreach-call.cil.c true .23 .23 32 wit - -
minepump_spec5_product30_true-unreach-call.cil.c true .23 .23 34 wit - -
minepump_spec5_product31_true-unreach-call.cil.c true .23 .24 33 wit - -
minepump_spec5_product32_true-unreach-call.cil.c true .23 .23 34 wit - -
minepump_spec5_product33_true-unreach-call.cil.c true 3.3  3.3  68 wit - -
minepump_spec5_product34_true-unreach-call.cil.c true 3.8  3.8  80 wit - -
minepump_spec5_product35_true-unreach-call.cil.c true 3.1  3.1  75 wit - -
minepump_spec5_product36_true-unreach-call.cil.c timeout 900    900    4000 wit - -
minepump_spec5_product37_true-unreach-call.cil.c true 5.2  5.2  100 wit - -
minepump_spec5_product38_true-unreach-call.cil.c true 3.6  3.7  92 wit - -
minepump_spec5_product39_true-unreach-call.cil.c timeout 900    900    4400 wit - -
minepump_spec5_product40_true-unreach-call.cil.c timeout 900    900    4400 wit - -
minepump_spec5_product41_true-unreach-call.cil.c timeout 900    900    4600 wit - -
minepump_spec5_product42_true-unreach-call.cil.c timeout 900    900    4400 wit - -
minepump_spec5_product43_true-unreach-call.cil.c timeout 900    900    4500 wit - -
minepump_spec5_product44_true-unreach-call.cil.c timeout 900    900    4300 wit - -
minepump_spec5_product45_true-unreach-call.cil.c timeout 900    900    4100 wit - -
minepump_spec5_product46_true-unreach-call.cil.c timeout 900    900    4200 wit - -
minepump_spec5_product47_true-unreach-call.cil.c timeout 900    900    4300 wit - -
minepump_spec5_product48_true-unreach-call.cil.c timeout 900    900    4300 wit - -
minepump_spec5_product49_true-unreach-call.cil.c true 5.2  5.2  110 wit - -
minepump_spec5_product50_true-unreach-call.cil.c true 4.6  4.6  100 wit - -
minepump_spec5_product51_true-unreach-call.cil.c true 9.8  9.8  160 wit - -
minepump_spec5_product52_true-unreach-call.cil.c timeout 900    900    4700 wit - -
minepump_spec5_product53_true-unreach-call.cil.c true 7.9  7.9  150 wit - -
minepump_spec5_product54_true-unreach-call.cil.c true 9.0  9.1  150 wit - -
minepump_spec5_product55_true-unreach-call.cil.c true 17    17    220 wit - -
minepump_spec5_product56_true-unreach-call.cil.c timeout 900    900    5200 wit - -
minepump_spec5_product57_true-unreach-call.cil.c timeout 900    900    4600 wit - -
minepump_spec5_product58_true-unreach-call.cil.c timeout 900    900    4700 wit - -
minepump_spec5_product59_true-unreach-call.cil.c timeout 900    900    4600 wit - -
minepump_spec5_product60_true-unreach-call.cil.c timeout 900    900    5000 wit - -
minepump_spec5_product61_true-unreach-call.cil.c timeout 900    900    4900 wit - -
minepump_spec5_product62_true-unreach-call.cil.c timeout 900    900    4900 wit - -
minepump_spec5_product63_true-unreach-call.cil.c timeout 900    900    4900 wit - -
minepump_spec5_product64_true-unreach-call.cil.c timeout 900    900    5000 wit - -
minepump_spec5_productSimulator_true-unreach-call.cil.c timeout 900    900    4800 wit - -
../../sv-benchmarks/c/product-lines/ 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 597 130000 130000 710000 597 5200   2900   200000   597 5700   3200   120000  
    correct results 400 13000 13000 120000 165 3000   1700   120000   167 4100   2300   81000  
        correct true 233 4500 4500 40000 128 0   0   0   1 0   0   0  
        correct false 167 8500 8500 84000 37 3000   1700   120000   166 4100   2300   81000  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (597 tasks, max score: 929) 633
Run set sv-comp16.ProductLines