feat(smtsolver): added debugging and nra_solver suggestions for variable selection

feat(smtsolver): added debugging and nra_solver suggestions for variable selection

feat(heuristics): added variable selection heuristic based upon mode paths

feat(dsolvers): variable selection heuristic for bmc

fix(dReach): Merged dReach scripts into one

fix(heuristics): Cleanup BMC heuristic code

cleanup(smtsolver): cleanup unnecessary diffs

Conflicts:
	src/opensmt/smtsolvers/CoreSMTSolver.C
	src/opensmt/smtsolvers/SMTConfig.C
	src/opensmt/smtsolvers/SMTConfig.h
feat(benchmarks): added start of multiple battery scheduling problem
fix(dReach): fixed flag for dReach
chore(dsolvers): rename bmc_heuristic to nra_bmc_heuristic
fix(CMakeLists.txt): add "--disable-minidebuginfo" to configure libunwind

Dan had a link error without it and this option resolved the issue.
chore(CMakeLists.txt): fix dependencies between libs
fix(opensmt): fix #include
feat(util/scoped_vec): add operator[]
feat(realpaver/rp_constraint): implement 'used' field
feat(dsolver/icp_solver): support int type
feat(dsolver/icp_solver): implement simple build_explanation

For the literals in m_stack, we only choose the ones used by ICP solver
and return to NRA solver as an explanation for the conflict (UNSAT)
fix(CMakeLists.txt): disable glog shared lib
fix(tools/basic/type.ml): use "%g" for printing numbers
fix(CMakeLists.txt): print EGLIBC message only in Linux
fix(CMakeLists.txt): clean up external dir structure; use NDEBUG for gflag
fix(util/git_sha1): add copyright, wrap with namespace
fix(main): cmd-line parsing

 - move cmd-line parsing from SMTConfig to main.
 - run gflags first, update argc and argv. Then call SMTConfig with the
   updated ones.
 - check whether a given file exists or not.

This closes dreal/dreal#39
fix(opensmt/smtsolvers/SMTConfig): fix nra_json_out_name
doc(*): update OCaml version dep (>=4.01.0)

[skip ci]
fix(CMakeLists.txt): use libunwind only for 64-bit linux