Tool symbiotic KLEE:7f3c74aa-dg:96e851cf-symbiotic:69a1d8e6-minisat:3db58943-stp:39fa956f-LLVMInstrumentation:f750b24a
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-13 11:10:58 CET
Run set sv-comp17.ReachSafety-ProductLines
Options --witness witness.graphml
../../sv-benchmarks/c/product-lines/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu wall energy mem validator uautomizer violation t<90s status cpu wall energy mem validator cpachecker correctness t<900s status cpu wall energy mem validator uautomizer correctness t<900s status cpu wall energy mem
elevator_spec14_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .36 .36 5.0 19   .21  0      - - - -
elevator_spec14_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .36 .36 4.2 19   .22  0      - - - -
elevator_spec14_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .36 .35 4.2 19   .22  0      - - - -
elevator_spec14_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 .38 4.7 20   .22  0      - - - -
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .43 .43 5.2 24   .23  0      - - - -
elevator_spec1_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .38 .38 4.6 19   .22  0      - - - -
elevator_spec1_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .38 .38 5.6 19   .22  0      - - - -
elevator_spec1_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 .39 4.3 19   .22  0      - - - -
elevator_spec1_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .38 .37 4.7 20   .23  0      - - - -
elevator_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 .39 4.9 20   .22  0      - - - -
elevator_spec1_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .40 .40 4.5 20   .22  0      - - - -
elevator_spec1_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .40 .40 4.2 20   .22  0      - - - -
elevator_spec1_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .40 .39 5.5 21   .23  0      - - - -
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .44 .43 4.7 25   .25  0      - - - -
elevator_spec2_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .37 .37 4.2 19   .22  0      - - - -
elevator_spec2_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .40 .39 4.4 20   .22  .074  - - - -
elevator_spec2_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 .39 4.3 19   .22  0      - - - -
elevator_spec2_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .40 .40 4.3 20   .23  .32   - - - -
elevator_spec2_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .40 .52 4.7 28   .22  8.9    - - - -
elevator_spec2_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .37 .37 4.5 20   .22  0      - - - -
elevator_spec2_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .37 .36 4.8 20   .22  0      - - - -
elevator_spec2_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .40 .40 4.4 21   .23  0      - - - -
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .42 .42 5.3 25   .25  0      - - - -
elevator_spec3_product03_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .36 .36 4.5 20   .22  0      - - - -
elevator_spec3_product11_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .40 .39 4.1 21   .22  0      - - - -
elevator_spec3_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .37 .36 4.2 21   .22  0      - - - -
elevator_spec3_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .41 .40 5.1 22   .22  0      - - - -
elevator_spec3_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 .39 4.4 22   .23  .32   - - - -
elevator_spec3_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .42 .41 6.2 23   .23  0      - - - -
elevator_spec3_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .37 .37 4.5 22   .22  0      - - - -
elevator_spec3_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .48 .60 4.6 31   .22  9.0    - - - -
elevator_spec3_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .41 .41 4.8 23   .23  0      - - - -
elevator_spec3_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 .39 4.4 24   .23  .32   - - - -
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .43 .43 4.8 28   .25  0      - - - -
elevator_spec9_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 .39 4.5 20   .22  0      - - - -
elevator_spec9_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .40 .39 4.5 21   .22  0      - - - -
elevator_spec9_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .40 .39 4.6 21   .22  0      - - - -
elevator_spec9_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .40 .40 4.4 21   .23  0      - - - -
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .45 .44 5.5 25   .25  0      - - - -
elevator_spec13_product21_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 880    930    11000   15000   .22  7.7    - - - -
elevator_spec13_product22_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    910    12000   15000   .22  0      - - - -
elevator_spec13_product23_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 890    930    12000   15000   .22  .0041 - - - -
elevator_spec13_product24_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 890    930    12000   15000   .22  0      - - - -
elevator_spec13_product29_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 890    930    12000   15000   .22  0      - - - -
elevator_spec13_product30_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    910    12000   15000   .22  .074  - - - -
elevator_spec13_product31_true-unreach-call_false-termination.cil.c - 0 wit inspect - - - -
elevator_spec13_product32_true-unreach-call_false-termination.cil.c - 0 wit inspect - - - -
elevator_spec13_productSimulator_true-unreach-call_true-termination.cil.c timeout (timeout) 0 wit inspect 890    930    12000   15000   .24  0      - - - -
elevator_spec14_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 .37 3.8 17   .21  0      - - - -
elevator_spec14_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect .35 .35 4.6 18   .21  0      - - - -
elevator_spec14_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect .35 .35 4.6 18   .21  0      - - - -
elevator_spec14_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 .36 5.0 19   .22  0      - - - -
elevator_spec14_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect .38 .38 5.1 19   .21  0      - - - -
elevator_spec14_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 .36 4.7 20   .22  0      - - - -
elevator_spec1_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 .36 3.8 17   .22  0      - - - -
elevator_spec1_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect .35 .35 4.1 18   .22  0      - - - -
elevator_spec1_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect .35 .35 3.9 18   .22  0      - - - -
elevator_spec1_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 .36 4.6 19   .22  0      - - - -
elevator_spec1_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 .36 3.9 18   .22  0      - - - -
elevator_spec1_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 .36 4.1 19   .22  0      - - - -
elevator_spec1_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 .37 4.2 19   .22  0      - - - -
elevator_spec1_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 .36 4.1 19   .23  0      - - - -
elevator_spec1_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 .35 4.2 19   .22  0      - - - -
elevator_spec1_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect .38 .38 5.2 19   .22  0      - - - -
elevator_spec1_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 .36 4.3 20   .22  0      - - - -
elevator_spec1_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 .37 4.4 20   .23  0      - - - -
elevator_spec2_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 .37 4.3 18   .22  0      - - - -
elevator_spec2_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 .36 4.7 18   .22  .0041 - - - -
elevator_spec2_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 .35 4.7 18   .22  0      - - - -
elevator_spec2_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect .44 .56 4.5 27   .22  9.0    - - - -
elevator_spec2_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 .36 5.2 18   .22  0      - - - -
elevator_spec2_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 .35 4.6 19   .22  0      - - - -
elevator_spec2_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect .38 .38 4.4 19   .22  0      - - - -
elevator_spec2_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 .36 4.3 20   .23  0      - - - -
elevator_spec2_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect .38 .38 5.0 19   .22  .32   - - - -
elevator_spec2_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 .36 4.7 20   .22  0      - - - -
elevator_spec2_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect .39 .39 4.6 20   .22  0      - - - -
elevator_spec2_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect .40 .40 4.2 20   .23  0      - - - -
elevator_spec3_product01_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 .37 4.0 20   .22  .32   - - - -
elevator_spec3_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 .36 4.2 20   .22  0      - - - -
elevator_spec3_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 .35 4.4 21   .22  0      - - - -
elevator_spec3_product18_true-unreach-call_true-termination.cil.c true 2 wit inspect .38 .38 4.2 21   .22  0      - - - -
elevator_spec3_product21_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 .36 4.9 21   .22  0      - - - -
elevator_spec3_product22_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 .37 4.5 22   .22  .32   - - - -
elevator_spec3_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect .37 .36 4.6 22   .22  0      - - - -
elevator_spec3_product26_true-unreach-call_true-termination.cil.c true 2 wit inspect .38 .37 4.6 22   .22  0      - - - -
elevator_spec3_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect .39 .39 4.2 22   .22  0      - - - -
elevator_spec3_product30_true-unreach-call_true-termination.cil.c true 2 wit inspect .39 .38 5.7 23   .22  0      - - - -
elevator_spec9_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect .38 .38 4.3 19   .22  0      - - - -
elevator_spec9_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect .38 .38 4.8 19   .22  0      - - - -
elevator_spec9_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 .36 5.5 19   .22  0      - - - -
elevator_spec9_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect .39 .38 4.2 20   .22  0      - - - -
elevator_spec9_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect .36 .36 4.2 20   .22  0      - - - -
elevator_spec9_product31_true-unreach-call_true-termination.cil.c true 2 wit inspect .38 .37 4.2 21   .23  0      - - - -
email_spec0_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .37 .37 4.4 16   .19  0      - - - -
email_spec0_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .41 .41 4.5 19   .20  0      - - - -
email_spec0_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .41 .41 5.2 17   .20  0      - - - -
email_spec0_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .42 .42 4.7 20   .20  0      - - - -
email_spec0_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .41 .41 4.1 18   .20  0      - - - -
email_spec0_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .41 .41 6.2 19   .20  0      - - - -
email_spec0_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .41 .40 4.9 21   .20  0      - - - -
email_spec0_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .46 .45 5.6 22   .20  0      - - - -
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.5  1.5  18   45   .22  0      - - - -
email_spec11_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .36 .36 5.1 16   .19  0      - - - -
email_spec11_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .38 .37 4.7 18   .20  0      - - - -
email_spec11_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 .39 4.4 17   .20  0      - - - -
email_spec11_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .42 .42 5.1 19   .20  0      - - - -
email_spec11_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 .39 5.5 17   .20  0      - - - -
email_spec11_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 .39 5.0 19   .20  0      - - - -
email_spec11_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 .38 4.7 19   .20  0      - - - -
email_spec11_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .42 .41 5.1 22   .20  0      - - - -
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .82 .81 10   28   .22  0      - - - -
email_spec1_product14_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .42 .42 4.8 17   .20  0      - - - -
email_spec1_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .48 .48 5.9 16   .20  0      - - - -
email_spec1_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .43 .43 4.9 16   .20  0      - - - -
email_spec1_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .44 .44 5.7 18   .20  0      - - - -
email_spec1_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .41 .40 5.1 18   .20  0      - - - -
email_spec1_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .46 .45 5.4 17   .20  0      - - - -
email_spec1_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .45 .45 6.3 20   .20  0      - - - -
email_spec1_product29_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .42 .42 5.3 19   .20  0      - - - -
email_spec1_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .51 .51 5.8 17   .20  0      - - - -
email_spec1_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .51 .62 5.5 26   .20  8.1    - - - -
email_spec1_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .48 .48 5.8 20   .20  .32   - - - -
email_spec1_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .51 .51 6.7 19   .20  0      - - - -
email_spec1_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .44 .44 6.3 21   .20  0      - - - -
email_spec1_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .49 .49 5.0 22   .21  0      - - - -
email_spec1_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.4  1.4  17   44   .22  0      - - - -
email_spec27_product17_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .61 .61 6.5 19   .20  0      - - - -
email_spec27_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .62 .62 7.9 21   .20  0      - - - -
email_spec27_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .44 .44 5.7 17   .20  0      - - - -
email_spec27_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .69 .68 7.7 22   .20  .32   - - - -
email_spec27_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .50 .50 5.8 17   .20  0      - - - -
email_spec27_product25_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .47 .47 5.5 19   .20  0      - - - -
email_spec27_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .52 .52 6.2 20   .20  0      - - - -
email_spec27_product29_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .66 .66 9.3 21   .20  0      - - - -
email_spec27_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .72 .72 8.1 24   .20  0      - - - -
email_spec27_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .47 .47 5.5 18   .20  0      - - - -
email_spec27_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .79 .78 9.8 25   .20  0      - - - -
email_spec27_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .54 .54 6.3 19   .20  0      - - - -
email_spec27_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .51 .50 5.5 21   .20  0      - - - -
email_spec27_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .53 .53 6.9 22   .21  0      - - - -
email_spec27_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 2.0  2.0  28   61   .22  0      - - - -
email_spec3_product13_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .37 .36 4.5 15   .20  0      - - - -
email_spec3_product17_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .40 .40 5.2 18   .20  0      - - - -
email_spec3_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .37 .37 5.2 16   .20  0      - - - -
email_spec3_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 .39 4.5 17   .20  0      - - - -
email_spec3_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .41 .40 4.5 19   .20  0      - - - -
email_spec3_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .40 .40 4.3 18   .20  0      - - - -
email_spec3_product25_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .41 .41 4.5 20   .20  0      - - - -
email_spec3_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .42 .41 4.8 20   .20  0      - - - -
email_spec3_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .40 .40 4.4 17   .20  0      - - - -
email_spec3_product29_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .42 .41 5.5 19   .20  0      - - - -
email_spec3_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .42 .41 4.7 18   .20  0      - - - -
email_spec3_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 .39 4.8 19   .20  0      - - - -
email_spec3_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .44 .43 5.0 20   .21  0      - - - -
email_spec3_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .40 .40 5.8 20   .20  0      - - - -
email_spec3_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .41 .41 5.1 21   .21  0      - - - -
email_spec3_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .42 .42 5.9 23   .21  0      - - - -
email_spec3_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .62 .62 8.5 28   .22  0      - - - -
email_spec4_product18_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 .38 4.5 16   .20  0      - - - -
email_spec4_product19_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .37 .36 4.7 16   .20  0      - - - -
email_spec4_product23_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .40 .40 4.2 18   .20  0      - - - -
email_spec4_product24_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 .39 3.9 17   .20  0      - - - -
email_spec4_product25_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .38 .38 4.5 19   .20  0      - - - -
email_spec4_product27_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .41 .41 4.3 20   .20  0      - - - -
email_spec4_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 .39 3.9 17   .20  0      - - - -
email_spec4_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .38 .38 4.8 18   .20  0      - - - -
email_spec4_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 .39 4.5 20   .20  0      - - - -
email_spec4_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .38 .38 4.9 19   .20  0      - - - -
email_spec4_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .40 .40 4.8 21   .20  0      - - - -
email_spec4_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .40 .40 5.8 22   .21  0      - - - -
email_spec4_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .83 .82 11   28   .22  0      - - - -
email_spec6_product12_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .35 .35 5.2 15   .20  0      - - - -
email_spec6_product14_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 .38 4.5 17   .20  0      - - - -
email_spec6_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .37 .37 4.9 16   .20  0      - - - -
email_spec6_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .36 .36 4.5 17   .20  0      - - - -
email_spec6_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .41 .41 4.9 18   .20  0      - - - -
email_spec6_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .37 .37 5.2 19   .20  0      - - - -
email_spec6_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .41 .40 4.6 18   .20  0      - - - -
email_spec6_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .41 .41 5.1 20   .20  0      - - - -
email_spec6_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .37 .37 5.3 16   .20  0      - - - -
email_spec6_product29_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 .38 4.7 19   .20  0      - - - -
email_spec6_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .38 .38 4.8 18   .20  0      - - - -
email_spec6_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .42 .42 4.7 19   .20  0      - - - -
email_spec6_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .40 .40 4.6 20   .21  .45   - - - -
email_spec6_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .41 .40 4.8 20   .20  0      - - - -
email_spec6_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .40 .39 5.3 21   .21  0      - - - -
email_spec6_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .41 .41 5.2 22   .21  0      - - - -
email_spec6_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .56 .56 8.3 28   .22  .32   - - - -
email_spec7_product28_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 .39 4.3 16   .20  0      - - - -
email_spec7_product29_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 .38 5.1 18   .20  0      - - - -
email_spec7_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .40 .40 4.2 17   .20  0      - - - -
email_spec7_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .38 .38 5.4 18   .20  0      - - - -
email_spec7_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .39 .39 4.4 19   .20  0      - - - -
email_spec7_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .41 .41 4.3 19   .20  0      - - - -
email_spec7_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .42 .42 4.4 21   .20  0      - - - -
email_spec7_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .42 .42 5.5 22   .20  0      - - - -
email_spec7_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .57 .57 7.3 28   .22  0      - - - -
email_spec8_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .50 .50 5.7 16   .20  0      - - - -
email_spec8_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .44 .43 4.8 16   .20  0      - - - -
email_spec8_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .52 .52 7.2 18   .20  0      - - - -
email_spec8_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .43 .42 5.2 19   .20  0      - - - -
email_spec8_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .46 .46 5.6 17   .20  0      - - - -
email_spec8_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .48 .48 6.2 20   .20  0      - - - -
email_spec8_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .53 .53 7.4 17   .20  0      - - - -
email_spec8_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .43 .43 5.5 19   .20  0      - - - -
email_spec8_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .55 .55 6.1 20   .20  0      - - - -
email_spec8_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .48 .48 7.1 19   .20  0      - - - -
email_spec8_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .49 .48 6.1 21   .20  0      - - - -
email_spec8_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .53 .53 7.1 22   .21  0      - - - -
email_spec8_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.8  1.8  23   55   .22  0      - - - -
email_spec9_product15_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .51 .50 6.1 16   .20  0      - - - -
email_spec9_product16_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .44 .56 6.1 25   .20  8.8    - - - -
email_spec9_product20_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .53 .53 7.6 18   .20  0      - - - -
email_spec9_product21_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .45 .45 5.8 19   .20  .32   - - - -
email_spec9_product22_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .46 .45 5.2 17   .20  0      - - - -
email_spec9_product26_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .50 .50 5.7 20   .20  0      - - - -
email_spec9_product30_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .51 .51 7.1 17   .20  0      - - - -
email_spec9_product31_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .47 .46 5.5 18   .20  0      - - - -
email_spec9_product32_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .60 .72 7.1 28   .20  8.9    - - - -
email_spec9_product33_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .51 .51 5.9 20   .20  0      - - - -
email_spec9_product34_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .48 .48 5.5 21   .20  0      - - - -
email_spec9_product35_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect .51 .51 6.6 22   .21  0      - - - -
email_spec9_productSimulator_false-unreach-call_true-termination.cil.c false(unreach-call) 1 wit inspect 1.8  1.8  20   56   .22  0      - - - -
email_spec0_product05_true-unreach-call_true-termination.cil.c true 2 wit inspect .28 .28 3.6 11   .17  0      - - - -
email_spec0_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect .34 .45 4.7 19   .17  7.9    - - - -
email_spec0_product10_true-unreach-call_true-termination.cil.c true 2 wit inspect .29 .29 3.4 11   .17  0      - - - -
email_spec0_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect .33 .33 3.5 12   .18  0      - - - -
email_spec0_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect .34 .34 4.1 12   .20  0      - - - -
email_spec0_product24_true-unreach-call_true-termination.cil.c true 2 wit inspect .34 .34 3.7 12   .20  0      - - - -
email_spec0_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect .31 .31 3.3 12   .20  0      - - - -
email_spec0_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect .35 .34 3.8 12   .20  0      - - - -
email_spec0_product36_true-unreach-call_true-termination.cil.c true 2 wit inspect .30 .30 3.3 12   .18  0      - - - -
email_spec0_product37_true-unreach-call_true-termination.cil.c true 2 wit inspect .30 .30 3.5 12   .18  0      - - - -
email_spec0_product38_true-unreach-call_true-termination.cil.c true 2 wit inspect .33 .33 4.0 12   .18  0      - - - -
email_spec0_product40_true-unreach-call_true-termination.cil.c true 2 wit inspect .33 .33 4.1 12   .20  0      - - - -
email_spec11_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect .29 .28 3.4 11   .17  0      - - - -
email_spec11_product07_true-unreach-call_true-termination.cil.c true 2 wit inspect .31 .30 3.7 11   .18  0      - - - -
email_spec11_product08_true-unreach-call_true-termination.cil.c true 2 wit inspect .30 .30 3.4 12   .18  0      - - - -
email_spec11_product10_true-unreach-call_true-termination.cil.c true 2 wit inspect .32 .32 3.5 11   .17  0      - - - -
email_spec11_product18_true-unreach-call_true-termination.cil.c true 2 wit inspect .33 .32 3.2 12   .20  0      - - - -
email_spec11_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect .32 .32 4.3 12   .20  0      - - - -
email_spec11_product24_true-unreach-call_true-termination.cil.c true 2 wit inspect .31 .31 4.4 12   .20  0      - - - -
email_spec11_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect .34 .34 3.7 12   .20  .0041 - - - -
email_spec11_product36_true-unreach-call_true-termination.cil.c true 2 wit inspect .32 .32 3.5 12   .18  .32   - - - -
email_spec11_product37_true-unreach-call_true-termination.cil.c true 2 wit inspect .33 .33 3.8 11   .18  0      - - - -
email_spec11_product39_true-unreach-call_true-termination.cil.c true 2 wit inspect .32 .32 3.4 12   .18  0      - - - -
email_spec11_product40_true-unreach-call_true-termination.cil.c true 2 wit inspect .32 .33 4.4 11   .20  .32   - - - -
email_spec1_product12_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.4  3.4  45   57   .18  0      - - - -
email_spec1_product28_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.7  3.7  51   65   .20  0      - - - -
email_spec27_product13_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.6  3.6  42   62   .18  0      - - - -
email_spec27_product28_true-unreach-call_true-termination.cil.c true 2 wit inspect 4.1  4.1  52   77   .20  0      - - - -
email_spec4_product13_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.0  3.0  43   46   .18  0      - - - -
email_spec4_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.2  3.2  43   56   .20  0      - - - -
email_spec4_product28_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.0  3.0  39   47   .20  0      - - - -
email_spec4_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.3  3.3  39   57   .20  0      - - - -
email_spec7_product13_true-unreach-call_true-termination.cil.c true 2 wit inspect .31 .30 3.7 12   .18  0      - - - -
email_spec7_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect .31 .31 4.1 12   .20  0      - - - -
email_spec7_product18_true-unreach-call_true-termination.cil.c true 2 wit inspect .31 .31 3.6 12   .20  0      - - - -
email_spec7_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect .33 .32 3.9 12   .20  0      - - - -
email_spec7_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect .40 .55 4.2 25   .20  14      - - - -
email_spec7_product24_true-unreach-call_true-termination.cil.c true 2 wit inspect .31 .31 3.5 12   .20  0      - - - -
email_spec7_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect .31 .31 3.5 12   .20  0      - - - -
email_spec7_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect .34 .33 4.0 13   .20  0      - - - -
email_spec8_product12_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.4  3.4  41   55   .19  0      - - - -
email_spec8_product14_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.8  3.8  48   68   .20  0      - - - -
email_spec8_product28_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.7  3.7  54   64   .20  0      - - - -
email_spec8_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 4.2  4.2  58   78   .20  0      - - - -
email_spec9_product12_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.4  3.6  40   64   .19  8.8    - - - -
email_spec9_product14_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.9  3.9  46   68   .20  0      - - - -
email_spec9_product28_true-unreach-call_true-termination.cil.c true 2 wit inspect 3.7  3.7  43   64   .20  0      - - - -
email_spec9_product29_true-unreach-call_true-termination.cil.c true 2 wit inspect 4.2  4.2  53   78   .20  0      - - - -
minepump_spec1_product33_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .23 .23 2.5 10   .061 0      - - - -
minepump_spec1_product34_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .21 .21 2.6 9.8 .061 0      - - - -
minepump_spec1_product35_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .23 .22 2.4 9.8 .061 0      - - - -
minepump_spec1_product36_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .21 .21 2.7 9.9 .061 0      - - - -
minepump_spec1_product37_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .23 .22 2.2 10   .061 0      - - - -
minepump_spec1_product38_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .24 .24 2.4 10   .061 .32   - - - -
minepump_spec1_product39_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .24 .23 2.4 9.9 .061 0      - - - -
minepump_spec1_product40_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .21 .21 3.1 9.8 .061 0      - - - -
minepump_spec1_product41_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .21 .21 3.0 9.8 .061 0      - - - -
minepump_spec1_product42_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .24 .24 2.3 9.8 .061 0      - - - -
minepump_spec1_product43_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .25 .25 2.6 10   .061 0      - - - -
minepump_spec1_product44_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .25 .25 2.3 9.9 .061 0      - - - -
minepump_spec1_product49_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .21 .20 2.5 9.9 .061 0      - - - -
minepump_spec1_product50_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .24 .23 2.3 9.9 .061 0      - - - -
minepump_spec1_product51_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .21 .21 2.4 9.8 .061 0      - - - -
minepump_spec1_product52_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .21 .21 2.7 10   .061 0      - - - -
minepump_spec1_product53_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .21 .21 2.7 10   .061 0      - - - -
minepump_spec1_product54_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .32 .43 2.5 17   .061 8.1    - - - -
minepump_spec1_product55_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .21 .21 2.8 10   .061 0      - - - -
minepump_spec1_product56_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .22 .21 2.7 9.9 .061 0      - - - -
minepump_spec1_productSimulator_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .28 .28 3.0 10   .074 0      - - - -
minepump_spec2_product33_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .23 .23 2.3 10   .061 0      - - - -
minepump_spec2_product34_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .21 .21 2.8 10   .061 0      - - - -
minepump_spec2_product35_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .24 .24 2.4 9.9 .061 0      - - - -
minepump_spec2_product36_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .23 .22 2.6 9.9 .061 0      - - - -
minepump_spec2_product41_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .22 .21 2.9 10   .061 0      - - - -
minepump_spec2_product42_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .30 .29 3.2 12   .061 0      - - - -
minepump_spec2_product43_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .38 .38 4.3 15   .061 0      - - - -
minepump_spec2_product44_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .38 .38 5.2 15   .061 0      - - - -
minepump_spec2_productSimulator_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 1.8  1.8  23   56   .074 0      - - - -
minepump_spec3_product01_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .21 .20 2.5 9.7 .053 0      - - - -
minepump_spec3_product02_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .23 .23 2.2 9.9 .061 0      - - - -
minepump_spec3_product03_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .20 .20 2.2 9.7 .061 0      - - - -
minepump_spec3_product04_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .21 .20 2.1 9.9 .061 .32   - - - -
minepump_spec3_product05_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .21 .20 2.4 9.9 .061 0      - - - -
minepump_spec3_product06_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .21 .21 2.7 9.8 .061 .32   - - - -
minepump_spec3_product07_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .21 .21 2.4 9.8 .061 0      - - - -
minepump_spec3_product08_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .21 .20 2.3 9.9 .061 0      - - - -
minepump_spec3_product09_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .23 .23 2.4 9.8 .061