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