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