Fix typo in bitvectors example; thanks to Adam Gashlin for reporting the issue.
Valuation::entailmentCheck() proxy for TheoryEngine version.  Signature and contract is the same as for TheoryEngine version.
Improving documentation for glpk-cut-log switch.
add constant regular expression check for intersection.
fix a bug in replace and contains
First draft of ambqi_builder (new implementation of MBQI based on disjoint sets).
Fixes to ambqi, now solution-sound.
add splits
add splits
Merge branch 'master' of github.com:tiliang/CVC4
fix a bug in contain
patch to the last commit: add a single character case
Adding encoding of sha1 collision for the hashing example
Basic optimizations for ambqi : only normalize UF applied to variables, direct handling of NOT
Fixes to quantifiers rewriter to prevent miniscoping nested quantifiers.  Minor fixes to ambqi.  Preparation for CASC proof output.  Add NNF option.
Major simplifications to macros module.
Add variable ordering to ambqi.  Bug fix to macros. More preparation for CASC proofs.
Initial draft of run scripts for CASC j7
Fix for example installation.
Bug fixes to CBQI.  Add first draft of CASC j7 TFF script.  Add regression, minor changes.