fixing bug580 caused by bad bv inequality explanation
Refactoring of conjecture generator.  Determine subgoals are non-canonical based on ground equalities.  Add filtering options to options file.
Bug fix variable triggers with --inst-max-level : use term in EQC with minimal instantiation level.
More refactoring of conjecture generation.  Term generation into own class.
Refactor entailment filtering for conjecture generator.  Other minor cleanup.
Fix soundness bug for quantifier macros involving Int/Real.
Fix (push) and (pop). Thanks to Christoph Sticksel for the bug report.
Merge branch '1.4.x'
Fix fix. There are no unsat cores in 1.4
Merge branch '1.4.x' while ignoring commit 8d5eb49.
cvc4terminate infinite loop fix
cvc4terminate infinite loop fix
Resource spending support in theories (and especially in quantifiers).
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