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