Merge branch '1.4.x'

Conflicts:
NEWS

Fix output of integer-valued real constants in SMT-LIB models (thanks Christoph Sticksel for reporting).

Add some (so far trivial) regressions for constant arrays.

Improve error in CVC parser in presence of unrecognized command name.

More array constants and parsing: better error messages, extend to CVC presentation language.

Minor fixes to CVC printer.

SMT-LIB parser support for array constants (Z3 syntax).

Merge branch '1.4.x'

Note array const support in NEWS

Fix unit test for ArrayStoreAll.

Added internal support for constant arrays.

Merge branch '1.4.x'.

Added option for developer use only

More model-based combination for arrays

Better getEqualityStatus for arrays, smarter combination of theories

Update AUTHORS affiliations and add Martin.

Fix comment in SmtEngine.

Merge pull request #54 from kbansal/bugfix_setssegfault

fix getModelValue(<non-preregistered term>)

fix getModelValue(<non-preregistered term>)

Fix for an array-of-record model generation assert-fail (assert was too strong).

Option for more aggressive merging in UEE.

Merge branch '1.4.x'

Fix improper #inclusion of private header outside library.

Fix a command-replay bug in tear-down-incremental mode.  Thanks to Christoph Sticksel for the report.

Proofs- and cores-related segfault fixes (mainly a usability issue), thanks Christoph Sticksel for reporting these.

Add option for aggressive model filtering in conjecture generator (enumerate ground terms).

Merge branch '1.4.x'

Fix infinite loop in --bitblast-aig/--bv-aig-simp options.

Merge branch '1.4.x'

Fix bv options doc.

Fix some configuration-related oddness.

Clarify some licensing-related things.

Finer-grained resource-limiting in quantifiers.

Fix AIG bitblaster for unsat cores.

fix unit test for new fair datatype enumeration

Fair datatype enumeration.

Fix infinite loop in datatypes enumerator.  Minor work on conjecture generator.

Refactor option for uf+cardinality constraints solver.

Partial support for codatatype models.

Support :no-pattern.

Do not throw error when codatatype is not well-founded.  Add option for disabling codatatype reasoning.  Minor cleanup.

Resource spending support in theories (and especially in quantifiers).

cvc4terminate infinite loop fix

cvc4terminate infinite loop fix

Merge branch '1.4.x' while ignoring commit 8d5eb49.

Fix fix. There are no unsat cores in 1.4

Merge branch '1.4.x'

Fix (push) and (pop). Thanks to Christoph Sticksel for the bug report.

Fix soundness bug for quantifier macros involving Int/Real.

Refactor entailment filtering for conjecture generator.  Other minor cleanup.

More refactoring of conjecture generation.  Term generation into own class.

Bug fix variable triggers with --inst-max-level : use term in EQC with minimal instantiation level.

Refactoring of conjecture generator.  Determine subgoals are non-canonical based on ground equalities.  Add filtering options to options file.

Fix bug for variable term triggers within multi-triggers.

Accept user-provided triggers with variable terms.  Flush lemmas before quantifiers check.  Minor fix for conjecture generation.

Update command_executor_portfolio.cpp

Merge remote-tracking branch 'origin/master'

check() optimization

Details of testing here:
http://church.cims.nyu.edu/wiki/User:Kshitij/theorycheckoptimization

Implement and enable --dt-var-exp-quant, cleanup trace messages, minor changes for relevant term filtering.

Work on conjecture generator : do not generalize subterms with concrete values, filter conjectures with ground substitutions whose equality is unknown, simplify generalization depth calculation.  Print --dump-instantiations on sat/unknown.

Set instantiation level on skolemized bodies of quantifiers.  Rename inst-level attribute to quant-inst-max-level

Do not use pure theory terms as single triggers.  Minor cleanup.

fixing bug580 caused by bad bv inequality explanation

fixing bug580 caused by bad bv inequality explanation

Fix assertion in rep_set.cpp, avoid full check in datatypes when in conflict.

Improved SMT-LIBv2 language support for unsat cores.

Bug fixes for --purify-triggers, --dt-force-assignment.

Fix build rule.

Fix Win32 builds.

New option --purify-triggers.  Refactoring of InstMatchGenerator.

remove some debugging code

(it can be brought back from version control, if needed)

improvements to sets sharing

* Add TheorySets::getEqualityStatus(TNode, TNode)
* Add TheorySets::getModelValue(TNode)

fix option alias (minor)

fix type in sets_translate

Unsat core printing.

Some fixes for dump- and get-unsat-core.

Quieter finish to build.

Unit test fix.

One small thing forgotten in core commit.

Java-side interface improvements for unsat cores.

Unsat core infrastruture and API (SMT-LIB compliance to come).

Merge branch '1.4.x'

Fix incorrectly-labeled test.

Merge branch '1.4.x'

Fix operator-printing issue in SMT2.

Fix SMT1 parser :extrasorts/:extrapreds.

Avoid doing work in quantifiers engine when no quantifiers are asserted.

Fix --inst-max-level for strategies that use arbitrary representative terms.

Update bv proof signature and example, after discussions with Liana.

Add option for inductive strengthening based on well-founded induction for integers (default schema).

Merge branch '1.4.x'

Produce error for bad indexed function names in SMT-LIB, remove antlr warning.

Making getEqualityStatus more powerful for bit-vector theory.

Merge branch '1.4.x'

Conflicts:
test/regress/regress0/Makefile.am

Revert a8e0ce67 and add test case (resolves bug #578).

This reverts commit a8e0ce673ba00533a663804cf74500e4d9a3a5cb.

Add support for quantifier-specific instantiation levels.  Add option for setting inst-level 0 only for input terms.

Update smt_engine.cpp

Code changed but comment didn't, might as well get rid of it.

To avoid confusion, permit --enable-staticbinary as an alias for --enable-static-binary.

Fix a build issue for some configurations, thanks Tianyi.

Add draft of BV proof signature (incomplete) and example proof.