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