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