boolean flatten: bug fix in dfs search

(this is not intended to (and doesn't) address the issue with
NodeBuilder limit)
bool flatten: node num_children workaround
fixing destruction order in SmtEngine
making sure sat context is zero when user context is popped to 0 in SmtEngine destructor
add bit0 and bit1 constants to smt-lib v1 parser
Re-enable predicate subtyping, reversing commit 8f9f549 (needed for Kind integration)
fix for lambdas in relation to subtypes
fixup for miplib trick (related to lambda fix for subtypes)
subrange-related fix
new --tear-down-incremental mode
new --force-logic option that overrides what the input says