cvc4terminate infinite loop fix
Do not throw error when codatatype is not well-founded.  Add option for disabling codatatype reasoning.  Minor cleanup.
Support :no-pattern.
Partial support for codatatype models.
Refactor option for uf+cardinality constraints solver.
Fix infinite loop in datatypes enumerator.  Minor work on conjecture generator.
Fair datatype enumeration.
fix unit test for new fair datatype enumeration
Fix AIG bitblaster for unsat cores.
Finer-grained resource-limiting in quantifiers.
Clarify some licensing-related things.
Fix some configuration-related oddness.
Fix bv options doc.
Merge branch '1.4.x'
Fix infinite loop in --bitblast-aig/--bv-aig-simp options.
Merge branch '1.4.x'
Add option for aggressive model filtering in conjecture generator (enumerate ground terms).
Proofs- and cores-related segfault fixes (mainly a usability issue), thanks Christoph Sticksel for reporting these.
Fix a command-replay bug in tear-down-incremental mode.  Thanks to Christoph Sticksel for the report.
Fix improper #inclusion of private header outside library.