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