feat(cpack): add bmc into cpack
feat(cpack): strip binaries
fix(opensmt/egraph/Enode.C): fix number output in print_infix

The previous patch using "fixed" notation has a problem. For instance,
when "x = 0.7000", it outputs "0.700001" and it changes result for some
benchmarks, for instance, cardiac_to1_good_3_0.smt2.

This fix is to reuse a string representation if it is already fixed
notation. Only if it is in scientific notation such as 5.0E-3, we
convert it to '0.005'.

We had this problem because CAPD doesn't accept a number in scientific
notation. Qinsi Wang reported this problem and I added a test,
'tests/nra_ode/killerred_3_0.smt2'.
feat(*): add "--debug" option

add another option --debug which will activate DREAL_LOG_DEBUG. The idea
is to use DREAL_LOG_DEBUG most of places instead of DREAL_LOG_INFO.

We expect that users use "--verbose" option while dReal devs use
"--debug" option:

 - Using --verbose activates DREAL_LOG_INFO.
 - Using --debug activates both DREAL_LOG_INFO and DREAL_LOG_DEBUG.
test(nra/sk.smt2): add Stefan Kiefer's example (at Oxford)

Read: https://github.com/dreal/dreal/issues/15
tests(nra_ode/bouncing-ball-alpha): remove random and random-no-ode
feat(realpaver/rp_propagator): check feasibility before returning SAT
feat(realpaver): add strict inequality to realpaver
fix(dsolvers): fix log messages
tests(nra_ode) add expected results for normal-*
feat(realpaver): add delta to rp_constraint
fix(dsolver/icp_solver): remove get_var_split_delta1
fix(dsolver/icp_solver): fix constraint_width

- For a constraint "lhs rop rhs", we used to eval "lhs + rhs" and check
  its width. We need to check the width of "lhs - rhs".

- Previously, we compare the current box width with 2 * delta. I change
  it to compare the current box width with delta (instead of 2 * delta).
feat(dsolvers/icp_solver): add the final feasibility check before returning SAT
fix(.travis.osx.yml): use homebrew's gcc(4.8.3), update OSX ver(10.9.2)