Merge branch '1.3.x'

gmp is again default, not cln, for build ID (reverting due to license discussion at Monday meeting)

Another way to handle negative contain

Merge branch '1.3.x'

Conflicts:
COPYING
NEWS
config/cvc4.m4

Switch license default back to BSD, and add --best and --enable-gpl options.

Cache apt packages on Travis.

clean some code

Fix LogicInfo parsing for string logics

Fix LogicInfo parsing for string logics

remove a warning in strings

minor fix, bring back the assertion.

string contain changes

Removing and consolidating options for uf-ss and quantifiers.  Bug fix for inst gen-style MBQI.

Added support for proof production in Equality Engine.  Cleaned up existing proof signatures and added proof signature for theory of arrays.  Added new MBQI technique based on interval abstraction.  Cleaned up option names.  Improved symmetry breaking for uf strong solver.  Other minor cleanup.

Merge branch '1.3.x'

Update copyright year.

Merge branch 'master' of github.com:tiliang/CVC4

minor fix

minor fix

Merge branch '1.3.x'

Fix for ANTLR warning.

new functions in strings

Merge branch 'master' of https://github.com/CVC4/CVC4

fix for some nightly build failures

Cleanup related to output language fix.

Merge branch '1.3.x'

Conflicts:
NEWS

Better automatic handling of output language setting.

Better get-value parse error message for common user error.

Minor code cleanup.

Merge branch '1.3.x'

Java datatype API fixups, datatype API examples

cln now default w.r.t. build ID string

Proof-checking code; fixups of segfaults and missing functionality in proof generation; fix bug 285.

* segfaults/assert-fails in proof-generation fixed, including bug 285
* added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present)
* proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals)
* proofs are *not* yet supported in incremental mode
* added --dump-proofs to dump out proofs, like --dump-models
* run_regression script now runs with --check-proofs where appropriate
* options scripts now support :link-smt for SMT options, like :link for command-line

Merge branch '1.3.x'

Fix to interactive mode determination.

Fix option specification.

Merge branch 'master' of https://github.com/CVC4/CVC4

Merge branch '1.3.x'

[skip ci]

Fix an autoconf issue with CLN in some configurations; also clarification re: license issues

[skip ci]

Merge branch '1.3.x'

Fix configure handling for CLN (should fix win32 nightly builds)

Merge branch '1.3.x'

Reduce autoconf version for dependence (should fix 32-bit builds).

Add missing regression-results directory.

Merge branch 'master' of https://github.com/CVC4/CVC4

Merge branch '1.3.x'

configure --with-portfolio disables CLN.

Merge branch 'master' of https://github.com/CVC4/CVC4

Merge branch '1.3.x'

Conflicts:
COPYING
NEWS

some config changes: new --bsd option, readline gives warning, default build is now production.

First attempt at incorporating LFSC proof checker into CVC4.

Merge branch '1.3.x'

Send Travis-CI emails to everyone

Merge branch '1.3.x'

Fix for bug 544.

resolve merge issue.

Merge branch 'master' of github.com:tiliang/CVC4

Conflicts:
NEWS

Merge branch '1.3.x'

Another fix for clang.

Merge branch '1.3.x'

Fix stack size on in-tree regressions.

cleanup

Merge branch '1.3.x'

Fix link error when using clang.

Fix to Travis-CI config.

Fix to Travis-CI config.

Merge branch '1.3.x'

Travis-CI configuration.

Some minor cleanup.

Update NEWS.

Merge branch '1.3.x'

Fix timer statistics to report correct time even on process abort.

Whitespace.

Fix warning.

Remove "NodeValue width" output

GLPK build identifier, license warnings.

Fix timer statistics to report correct time even on process abort.

Whitespace.

Fix warning.

Remove "NodeValue width" output

GLPK build identifier, license warnings.

mv prp to regress1

fix bug 542

Initializing master for next version.

Initializing 1.3.x branch.

Cutting release 1.3.

Merge branch '1.3.x'

mv prp to regress1

Merge branch '1.3.x'

fix bug 542

Initializing master for next version.

Initializing 1.3.x branch.

Cutting release 1.3.

disable substring in default mode

Fix NodeValue bitfields for 32-bit; fix comment.

Minor cleanup.

Update copyrights, add missing file-level documentation; fix perms.

Fixes related to parametric datatype printing.

Fix Boolean terms w.r.t. parametric datatypes (e.g., (Pair Bool Bool) now works).

Script fixes; when determining authorship of source files, don't count copyright-updating commits.