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 0      - - - -
minepump_spec3_product10_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .22 .22 2.4 9.9 .061 0      - - - -
minepump_spec3_product11_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .21 .20 2.6 9.8 .061 0      - - - -
minepump_spec3_product12_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .23 .23 2.3 9.8 .061 0      - - - -
minepump_spec3_product13_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .23 .23 2.4 9.8 .061 0      - - - -
minepump_spec3_product14_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .23 .23 2.4 9.9 .061 0      - - - -
minepump_spec3_product15_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .20 .20 2.3 9.9 .061 0      - - - -
minepump_spec3_product16_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .24 .23 2.6 9.8 .061 .32   - - - -
minepump_spec3_product17_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .23 .23 2.4 9.9 .061 0      - - - -
minepump_spec3_product18_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .24 .23 2.4 9.9 .061 0      - - - -
minepump_spec3_product19_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .23 .23 2.3 9.9 .061 0      - - - -
minepump_spec3_product20_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .21 .20 3.0 10   .061 0      - - - -
minepump_spec3_product21_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .22 .22 2.9 9.9 .061 0      - - - -
minepump_spec3_product22_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .23 .23 2.5 9.7 .061 0      - - - -
minepump_spec3_product23_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .24 .23 2.2 9.9 .061 0      - - - -
minepump_spec3_product24_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .24 .23 2.5 9.8 .061 0      - - - -
minepump_spec3_product25_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .20 .20 2.7 10   .061 0      - - - -
minepump_spec3_product26_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .21 .21 2.8 9.9 .061 0      - - - -
minepump_spec3_product27_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .24 .23 2.4 9.9 .061 0      - - - -
minepump_spec3_product28_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .23 .23 2.6 10   .061 .32   - - - -
minepump_spec3_product29_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .25 .36 2.7 17   .061 7.6    - - - -
minepump_spec3_product30_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .21 .21 2.9 9.9 .061 0      - - - -
minepump_spec3_product31_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .21 .21 2.8 9.9 .061 0      - - - -
minepump_spec3_product32_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .24 .24 2.3 10   .061 0      - - - -
minepump_spec3_product35_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .25 .37 4.1 18   .061 8.6    - - - -
minepump_spec3_product36_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .21 .21 2.7 9.7 .061 0      - - - -
minepump_spec3_product39_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .24 .24 2.5 9.9 .061 0      - - - -
minepump_spec3_product40_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .21 .21 2.5 9.9 .061 0      - - - -
minepump_spec3_product43_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .21 .21 2.8 9.8 .061 0      - - - -
minepump_spec3_product44_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .23 .23 2.3 10   .061 0      - - - -
minepump_spec3_product47_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .21 .21 2.6 9.9 .061 0      - - - -
minepump_spec3_product48_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .24 .24 2.4 9.9 .061 .32   - - - -
minepump_spec3_product51_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .24 .24 2.4 10   .061 .32   - - - -
minepump_spec3_product52_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .22 .22 2.6 9.7 .061 0      - - - -
minepump_spec3_product55_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .22 .21 2.8 9.9 .061 0      - - - -
minepump_spec3_product56_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .21 .21 2.7 9.7 .061 0      - - - -
minepump_spec3_product59_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .24 .24 2.6 9.9 .061 0      - - - -
minepump_spec3_product60_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .24 .24 2.5 9.9 .061 .32   - - - -
minepump_spec3_product63_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .22 .22 2.6 9.9 .061 0      - - - -
minepump_spec3_product64_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .24 .24 2.9 10   .061 0      - - - -
minepump_spec3_productSimulator_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .26 .26 2.8 10   .074 0      - - - -
minepump_spec4_product33_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .23 .23 2.6 10   .061 0      - - - -
minepump_spec4_product34_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .24 .24 2.4 9.8 .061 0      - - - -
minepump_spec4_product35_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .24 .24 2.6 9.9 .061 .45   - - - -
minepump_spec4_product36_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .23 .22 3.2 9.9 .061 0      - - - -
minepump_spec4_product37_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .24 .23 2.7 9.8 .061 0      - - - -
minepump_spec4_product38_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .30 .29 3.7 12   .061 0      - - - -
minepump_spec4_product39_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .42 .41 4.8 16   .061 0      - - - -
minepump_spec4_product40_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .38 .38 4.3 15   .061 0      - - - -
minepump_spec4_product41_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .21 .21 2.4 9.9 .061 0      - - - -
minepump_spec4_product42_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .26 .26 3.7 11   .061 0      - - - -
minepump_spec4_product43_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .31 .30 3.4 13   .061 0      - - - -
minepump_spec4_product44_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .34 .33 4.1 14   .061 0      - - - -
minepump_spec4_product45_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .22 .21 2.4 9.7 .061 0      - - - -
minepump_spec4_product46_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .29 .29 3.4 12   .061 0      - - - -
minepump_spec4_product47_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .42 .42 5.2 16   .061 0      - - - -
minepump_spec4_product48_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect .46 .46 5.6 18   .061 0      - - - -
minepump_spec4_productSimulator_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 9.7  9.7  130   270   .074 0      - - - -
minepump_spec1_product01_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7300   4900   .053 0      - - - -
minepump_spec1_product02_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8300   5100   .053 0      - - - -
minepump_spec1_product03_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8600   4300   .061 0      - - - -
minepump_spec1_product04_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9900   4600   .061 0      - - - -
minepump_spec1_product05_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    6400   4800   .061 7.7    - - - -
minepump_spec1_product06_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7400   4500   .061 0      - - - -
minepump_spec1_product07_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8400   4400   .061 0      - - - -
minepump_spec1_product08_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8700   4600   .061 0      - - - -
minepump_spec1_product09_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    11000   5000   .061 0      - - - -
minepump_spec1_product10_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7200   4700   .061 0      - - - -
minepump_spec1_product11_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8000   4300   .061 0      - - - -
minepump_spec1_product12_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8400   4500   .061 0      - - - -
minepump_spec1_product13_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8000   5400   .061 0      - - - -
minepump_spec1_product14_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8500   4400   .061 0      - - - -
minepump_spec1_product15_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7700   4300   .061 0      - - - -
minepump_spec1_product16_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8000   4500   .061 0      - - - -
minepump_spec1_product17_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7600   5400   .061 0      - - - -
minepump_spec1_product18_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8400   4900   .061 0      - - - -
minepump_spec1_product19_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    10000   4900   .061 0      - - - -
minepump_spec1_product20_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8200   4600   .061 0      - - - -
minepump_spec1_product21_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7300   4500   .061 0      - - - -
minepump_spec1_product22_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8800   4100   .061 0      - - - -
minepump_spec1_product23_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8900   4400   .061 0      - - - -
minepump_spec1_product24_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8000   4300   .061 0      - - - -
minepump_spec1_product25_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8700   5200   .061 0      - - - -
minepump_spec1_product26_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    11000   4800   .061 0      - - - -
minepump_spec1_product27_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9000   4900   .061 0      - - - -
minepump_spec1_product28_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8400   5100   .061 0      - - - -
minepump_spec1_product29_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9000   4000   .061 0      - - - -
minepump_spec1_product30_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7400   4100   .061 0      - - - -
minepump_spec1_product31_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7700   4100   .061 0      - - - -
minepump_spec1_product32_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    11000   4100   .061 0      - - - -
minepump_spec1_product45_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8900   5700   .061 0      - - - -
minepump_spec1_product46_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7500   5100   .061 0      - - - -
minepump_spec1_product47_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8200   4900   .061 0      - - - -
minepump_spec1_product48_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7800   4800   .061 0      - - - -
minepump_spec1_product57_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7600   5300   .061 0      - - - -
minepump_spec1_product58_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8200   5000   .061 0      - - - -
minepump_spec1_product59_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8900   4700   .061 0      - - - -
minepump_spec1_product60_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9200   5100   .061 0      - - - -
minepump_spec1_product61_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7100   5600   .061 0      - - - -
minepump_spec1_product62_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7900   5200   .061 0      - - - -
minepump_spec1_product63_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9900   4500   .061 7.7    - - - -
minepump_spec1_product64_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9100   4800   .061 0      - - - -
minepump_spec2_product01_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7200   4900   .061 0      - - - -
minepump_spec2_product02_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7500   5100   .061 0      - - - -
minepump_spec2_product03_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7200   4400   .061 0      - - - -
minepump_spec2_product04_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    11000   4800   .061 0      - - - -
minepump_spec2_product05_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    11000   6000   .061 0      - - - -
minepump_spec2_product06_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8100   5000   .061 0      - - - -
minepump_spec2_product07_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7100   4800   .061 0      - - - -
minepump_spec2_product08_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8700   4400   .061 0      - - - -
minepump_spec2_product09_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7800   5000   .061 8.4    - - - -
minepump_spec2_product10_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7400   4900   .061 0      - - - -
minepump_spec2_product11_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7500   4600   .061 0      - - - -
minepump_spec2_product12_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7800   4600   .061 0      - - - -
minepump_spec2_product13_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8500   5600   .061 0      - - - -
minepump_spec2_product14_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    11000   5000   .061 0      - - - -
minepump_spec2_product15_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    6900   4700   .061 0      - - - -
minepump_spec2_product16_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    11000   4700   .061 0      - - - -
minepump_spec2_product17_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8100   5100   .061 0      - - - -
minepump_spec2_product18_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7000   5100   .061 0      - - - -
minepump_spec2_product19_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    11000   4700   .061 0      - - - -
minepump_spec2_product20_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9500   4800   .061 0      - - - -
minepump_spec2_product21_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    6400   4600   .061 0      - - - -
minepump_spec2_product22_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    11000   4600   .061 0      - - - -
minepump_spec2_product23_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    11000   4800   .061 0      - - - -
minepump_spec2_product24_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    12000   4800   .061 0      - - - -
minepump_spec2_product25_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9100   5000   .061 0      - - - -
minepump_spec2_product26_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8000   5100   .061 0      - - - -
minepump_spec2_product27_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7500   4600   .061 0      - - - -
minepump_spec2_product28_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9800   5100   .061 0      - - - -
minepump_spec2_product29_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7000   4700   .061 0      - - - -
minepump_spec2_product30_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9000   4700   .061 0      - - - -
minepump_spec2_product31_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9100   4500   .061 0      - - - -
minepump_spec2_product32_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8200   4700   .061 0      - - - -
minepump_spec2_product37_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7800   5900   .061 12      - - - -
minepump_spec2_product38_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8000   4800   .061 0      - - - -
minepump_spec2_product39_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9900   5100   .061 0      - - - -
minepump_spec2_product40_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8500   4600   .061 0      - - - -
minepump_spec2_product45_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7400   5300   .061 0      - - - -
minepump_spec2_product46_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9200   5200   .061 0      - - - -
minepump_spec2_product47_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7700   4900   .061 0      - - - -
minepump_spec2_product48_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8600   5300   .061 0      - - - -
minepump_spec2_product49_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7700   5700   .061 0      - - - -
minepump_spec2_product50_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7500   5100   .061 0      - - - -
minepump_spec2_product51_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7300   4700   .061 0      - - - -
minepump_spec2_product52_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8900   4900   .061 0      - - - -
minepump_spec2_product53_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    6200   5200   .061 0      - - - -
minepump_spec2_product54_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9900   5500   .061 0      - - - -
minepump_spec2_product55_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7200   5000   .061 0      - - - -
minepump_spec2_product56_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9800   5300   .061 0      - - - -
minepump_spec2_product57_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7800   5700   .061 .020  - - - -
minepump_spec2_product58_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9400   5100   .061 0      - - - -
minepump_spec2_product59_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7800   4600   .061 7.4    - - - -
minepump_spec2_product60_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8700   4900   .061 0      - - - -
minepump_spec2_product61_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7800   5700   .061 0      - - - -
minepump_spec2_product62_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7900   5200   .061 0      - - - -
minepump_spec2_product63_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    10000   4700   .061 0      - - - -
minepump_spec2_product64_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7700   4800   .061 0      - - - -
minepump_spec3_product33_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8500   4600   .061 0      - - - -
minepump_spec3_product34_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7400   4900   .061 0      - - - -
minepump_spec3_product37_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8900   5400   .061 0      - - - -
minepump_spec3_product38_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7400   5200   .061 0      - - - -
minepump_spec3_product41_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9000   4800   .061 0      - - - -
minepump_spec3_product42_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8400   5000   .061 0      - - - -
minepump_spec3_product45_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7900   5700   .061 .0041 - - - -
minepump_spec3_product46_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    11000   5400   .061 0      - - - -
minepump_spec3_product49_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8200   5100   .061 0      - - - -
minepump_spec3_product50_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8700   4900   .061 0      - - - -
minepump_spec3_product53_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7100   5700   .061 0      - - - -
minepump_spec3_product54_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7100   5100   .061 0      - - - -
minepump_spec3_product57_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    6900   5400   .061 0      - - - -
minepump_spec3_product58_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7700   5100   .061 0      - - - -
minepump_spec3_product61_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    6900   5600   .061 7.5    - - - -
minepump_spec3_product62_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7300   4900   .061 7.7    - - - -
minepump_spec4_product01_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    10000   5200   .053 0      - - - -
minepump_spec4_product02_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8000   4900   .053 0      - - - -
minepump_spec4_product03_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    6900   4400   .061 0      - - - -
minepump_spec4_product04_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7400   4400   .061 0      - - - -
minepump_spec4_product05_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8400   5400   .061 0      - - - -
minepump_spec4_product06_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    6600   4900   .061 0      - - - -
minepump_spec4_product07_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8100   4700   .061 0      - - - -
minepump_spec4_product08_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9300   5100   .061 0      - - - -
minepump_spec4_product09_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7100   5200   .053 0      - - - -
minepump_spec4_product10_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8300   5200   .061 0      - - - -
minepump_spec4_product11_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7600   4600   .061 0      - - - -
minepump_spec4_product12_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    11000   4500   .061 0      - - - -
minepump_spec4_product13_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    6700   4900   .061 0      - - - -
minepump_spec4_product14_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9700   4800   .061 0      - - - -
minepump_spec4_product15_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    11000   4900   .061 0      - - - -
minepump_spec4_product16_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7500   4900   .061 0      - - - -
minepump_spec4_product17_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7900   5200   .061 0      - - - -
minepump_spec4_product18_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9000   4600   .061 0      - - - -
minepump_spec4_product19_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9000   4300   .061 0      - - - -
minepump_spec4_product20_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8700   4500   .061 0      - - - -
minepump_spec4_product21_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    11000   4600   .061 0      - - - -
minepump_spec4_product22_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7600   4300   .061 0      - - - -
minepump_spec4_product23_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7400   4300   .061 0      - - - -
minepump_spec4_product24_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9000   4600   .061 0      - - - -
minepump_spec4_product25_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7800   5300   .061 0      - - - -
minepump_spec4_product26_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    10000   4800   .061 0      - - - -
minepump_spec4_product27_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9300   4600   .061 0      - - - -
minepump_spec4_product28_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7700   4300   .061 0      - - - -
minepump_spec4_product29_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9600   4700   .061 0      - - - -
minepump_spec4_product30_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    11000   4600   .061 0      - - - -
minepump_spec4_product31_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8600   4500   .061 0      - - - -
minepump_spec4_product32_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7200   4400   .061 0      - - - -
minepump_spec4_product49_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    6500   6300   .061 0      - - - -
minepump_spec4_product50_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    11000   5400   .061 0      - - - -
minepump_spec4_product51_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7100   4500   .061 0      - - - -
minepump_spec4_product52_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7700   5100   .061 0      - - - -
minepump_spec4_product53_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7300   5500   .061 0      - - - -
minepump_spec4_product54_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7900   5100   .061 0      - - - -
minepump_spec4_product55_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8300   4900   .061 0      - - - -
minepump_spec4_product56_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7800   4900   .061 0      - - - -
minepump_spec4_product57_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7900   5000   .061 0      - - - -
minepump_spec4_product58_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8000   4900   .061 0      - - - -
minepump_spec4_product59_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9000   4600   .061 0      - - - -
minepump_spec4_product60_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7700   5000   .061 0      - - - -
minepump_spec4_product61_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7200   5400   .061 0      - - - -
minepump_spec4_product62_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9400   5200   .061 0      - - - -
minepump_spec4_product63_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8100   4600   .061 0      - - - -
minepump_spec4_product64_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7700   4500   .061 0      - - - -
minepump_spec5_product01_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7500   5500   .061 0      - - - -
minepump_spec5_product02_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9200   5400   .061 0      - - - -
minepump_spec5_product03_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    6800   4800   .061 0      - - - -
minepump_spec5_product04_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7000   4800   .061 0      - - - -
minepump_spec5_product05_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7600   5000   .061 0      - - - -
minepump_spec5_product06_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    6400   4900   .061 0      - - - -
minepump_spec5_product07_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9600   4700   .061 0      - - - -
minepump_spec5_product08_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8200   4900   .061 0      - - - -
minepump_spec5_product09_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7800   5800   .061 0      - - - -
minepump_spec5_product10_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7400   5700   .061 0      - - - -
minepump_spec5_product11_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8500   4900   .061 0      - - - -
minepump_spec5_product12_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8400   4900   .061 0      - - - -
minepump_spec5_product13_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7100   5200   .061 0      - - - -
minepump_spec5_product14_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7700   4900   .061 0      - - - -
minepump_spec5_product15_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8000   4800   .061 0      - - - -
minepump_spec5_product16_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9600   5000   .061 0      - - - -
minepump_spec5_product17_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    6700   6000   .061 0      - - - -
minepump_spec5_product18_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7800   5400   .061 0      - - - -
minepump_spec5_product19_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    12000   5200   .061 0      - - - -
minepump_spec5_product20_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8400   5100   .061 0      - - - -
minepump_spec5_product21_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8300   4800   .061 0      - - - -
minepump_spec5_product22_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    11000   4700   .061 0      - - - -
minepump_spec5_product23_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8300   4300   .061 0      - - - -
minepump_spec5_product24_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8600   4700   .061 0      - - - -
minepump_spec5_product25_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7800   6200   .061 0      - - - -
minepump_spec5_product26_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7300   5000   .061 0      - - - -
minepump_spec5_product27_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7900   4700   .061 0      - - - -
minepump_spec5_product28_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8900   4600   .061 0      - - - -
minepump_spec5_product29_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7000   4800   .061 0      - - - -
minepump_spec5_product30_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9100   4400   .061 0      - - - -
minepump_spec5_product31_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8200   4500   .061 0      - - - -
minepump_spec5_product32_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8100   4400   .061 0      - - - -
minepump_spec5_product33_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    10000   7100   .061 0      - - - -
minepump_spec5_product34_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    6700   5600   .061 0      - - - -
minepump_spec5_product35_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7500   4800   .061 0      - - - -
minepump_spec5_product36_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7500   4900   .061 0      - - - -
minepump_spec5_product37_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7400   5700   .061 0      - - - -
minepump_spec5_product38_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    10000   5500   .061 0      - - - -
minepump_spec5_product39_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8700   4800   .061 0      - - - -
minepump_spec5_product40_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    11000   5200   .061 0      - - - -
minepump_spec5_product41_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9900   5000   .061 0      - - - -
minepump_spec5_product42_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8500   5100   .061 0      - - - -
minepump_spec5_product43_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8300   4900   .061 0      - - - -
minepump_spec5_product44_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7600   4600   .061 0      - - - -
minepump_spec5_product45_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    11000   5700   .061 0      - - - -
minepump_spec5_product46_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8500   4900   .061 0      - - - -
minepump_spec5_product47_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7500   4900   .061 0      - - - -
minepump_spec5_product48_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7900   5100   .061 0      - - - -
minepump_spec5_product49_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8900   6900   .061 0      - - - -
minepump_spec5_product50_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    6700   5400   .061 0      - - - -
minepump_spec5_product51_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    6800   4800   .061 0      - - - -
minepump_spec5_product52_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7700   5200   .061 0      - - - -
minepump_spec5_product53_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8300   5700   .061 0      - - - -
minepump_spec5_product54_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7200   5100   .061 0      - - - -
minepump_spec5_product55_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8800   5000   .061 0      - - - -
minepump_spec5_product56_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8200   4700   .061 0      - - - -
minepump_spec5_product57_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9000   5500   .061 0      - - - -
minepump_spec5_product58_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9700   5300   .061 0      - - - -
minepump_spec5_product59_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8500   4600   .061 0      - - - -
minepump_spec5_product60_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    9600   4500   .061 0      - - - -
minepump_spec5_product61_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    6700   5300   .061 0      - - - -
minepump_spec5_product62_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8900   5100   .061 0      - - - -
minepump_spec5_product63_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    7900   4700   .061 0      - - - -
minepump_spec5_product64_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    11000   5200   .061 0      - - - -
minepump_spec5_productSimulator_true-unreach-call_false-termination.cil.c timeout (timeout) 0 wit inspect 900    900    8500   4800   .074 0      - - - -
../../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
total 595 453 210000 210000 2000000 1200000 76 180 595 595 595 595
    correct results 359 453 200 200 2500 7200 60 110 0 0 0 0
        correct true 94 188 85 85 1100 2300 19 41 0 0 0 0
        correct false 265 265 120 120 1400 4900 41 74 0 0 0 0
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (597 tasks, max score: 929) 453
Run set sv-comp17.ReachSafety-ProductLines