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