chore(proofcheck/checker/lexer.mll): fix space
fix(proofcheck/checker/smt2_cmd): skip assertion for trivial cases

 - (x <= +inf)
 - (-inf <= y)
chore(proofcheck/checker/smt2_cmd): open Basic
fix(proofcheck/checker/ptree): verbose error msg for pruning
fix(proofcheck/checker/parser): add support inf
fix(proofcheck/checker/failhandler): handle special cases of find mid point of (-inf, inf)
fix(tools/proofcheck/checker/basic): output format
feat(opensmt/parsers/smt2/smt2parser): allow "(term)"
fix(code_bmc.ml): fix mode index in variable name
fix(opensmt/smtsolvers): rename short_sat => nra_short_sat
feat(opensmt/smtsolvers): add --model option

When the result is SAT, it create a file <XXX.smt2.model> which
contains a model (satisfying assignment).
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