Fix unit test (compile error) for new SatSolver interface
Change TPTP parser to not use the STRING type; this necessary to repurpose strings for the upcoming string theory
fixed getModelValue to only query the value of leaves and evaluate more complex bv terms
Added check for infinite lemma loop
Fixes for getModelVal in bv theory
Improved speed of no redundant lemma assertion by using hash set
flatten or nodes
generalize to handle and
boolean flatten rewrite: dont re-rewrite
boolean flatten: bug fix in dfs search

(this is not intended to (and doesn't) address the issue with
NodeBuilder limit)
innd examples are solved fast, but destruction assertion fail
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
Merge branch 'master' of https://github.com/CVC4/CVC4
added some bv rewrite rules