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