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